diff --git a/library/Init/Lean/Compiler/IR/Default.lean b/library/Init/Lean/Compiler/IR/Default.lean index 7cd3b19e5e..8c183cb254 100644 --- a/library/Init/Lean/Compiler/IR/Default.lean +++ b/library/Init/Lean/Compiler/IR/Default.lean @@ -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; diff --git a/library/Init/Lean/Compiler/IR/UnreachBranches.lean b/library/Init/Lean/Compiler/IR/UnreachBranches.lean index 3c128d30a9..d62db15521 100644 --- a/library/Init/Lean/Compiler/IR/UnreachBranches.lean +++ b/library/Init/Lean/Compiler/IR/UnreachBranches.lean @@ -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;