max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: invoke inferCtorSummaries from IR compiler

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-07 13:10:54 -07:00
parent 3f62957c8f
commit f8bf68a9af
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Lean/Compiler/IR/Default.lean
View file

@ -18,6 +18,7 @@ import Init.Lean.Compiler.IR.Boxing
import Init.Lean.Compiler.IR.RC
import Init.Lean.Compiler.IR.ExpandResetReuse
import Init.Lean.Compiler.IR.UnboxResult
import Init.Lean.Compiler.IR.UnreachBranches
import Init.Lean.Compiler.IR.EmitC
namespace Lean
@ -27,6 +28,7 @@ private def compileAux (decls : Array Decl) : CompilerM Unit :=
do
logDecls `init decls;
checkDecls decls;
inferCtorSummaries decls;
let decls := decls.map Decl.pushProj;
logDecls `push_proj decls;
let decls := decls.map Decl.insertResetReuse;

3
library/Init/Lean/Compiler/IR/UnreachBranches.lean
View file

@ -222,8 +222,9 @@ def inferStep : M Bool :=
do ctx ← read;
ctx.decls.size.mfold (fun idx modified => do
match ctx.decls.get! idx with
| Decl.fdecl _ ys _ b => do
| Decl.fdecl fid ys _ b => do
s ← get;
-- dbgTrace (">> " ++ toString fid) $ fun _ =>
let currVals := s.funVals.get! idx;
adaptReader (fun (ctx : InterpContext) => { currFnIdx := idx, .. ctx }) $ do
ys.mfor $ fun y => updateVarAssignment y.x top;