chore: port LambdaLifting.lean

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -98,7 +98,7 @@ def findLetExpr? (fvarId : FVarId) : CompilerM (Option LetExpr) := do
 
 def isConstructorApp (fvarId : FVarId) : CompilerM Bool := do
   let some (.const declName _ _) ← findLetExpr? fvarId | return false
-  return (← getConstInfo declName) matches .ctorInfo ..
+  return (← getEnv).find? declName matches some (.ctorInfo ..)
 
 def Arg.isConstructorApp (arg : Arg) : CompilerM Bool := do
   let .fvar fvarId := arg | return false

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -12,9 +12,6 @@ import Lean.Compiler.LCNF.Internalize
 import Lean.Compiler.LCNF.Level
 import Lean.Compiler.LCNF.AuxDeclCache
 
-set_option warningAsError false
-#exit
-
 namespace Lean.Compiler.LCNF
 namespace LambdaLifting
 
@@ -101,7 +98,7 @@ def mkAuxDecl (closure : Array Param) (decl : FunDecl) : LiftM LetDecl := do
   | .alreadyCached declName =>
     auxDecl.erase
     pure declName
-  let value := mkAppN (.const auxDeclName us) (closure.map (mkFVar ·.fvarId))
+  let value := .const auxDeclName us (closure.map (.fvar ·.fvarId))
   /- We reuse `decl`s `fvarId` to avoid substitution -/
   let declNew := { fvarId := decl.fvarId, binderName := decl.binderName, type := decl.type, value }
   modifyLCtx fun lctx => lctx.addLetDecl declNew
@@ -197,4 +194,3 @@ builtin_initialize
   registerTraceClass `Compiler.lambdaLifting (inherited := true)
 
 end Lean.Compiler.LCNF
-

src/Lean/Compiler/LCNF/Passes.lean

@@ -44,8 +44,7 @@ def builtinPassManager : PassManager := {
   passes := #[
     init,
     pullInstances,
-    cse
-/-
+    cse,
     simp,
     floatLetIn,
     findJoinPoints,
@@ -53,10 +52,14 @@ def builtinPassManager : PassManager := {
     reduceJpArity,
     simp { etaPoly := true, inlinePartial := true, implementedBy := true } (occurrence := 1),
     eagerLambdaLifting,
-    specialize,
+    -- specialize,
     simp (occurrence := 2),
     cse (occurrence := 1),
     saveBase, -- End of base phase
+    -- TODO
+    saveMono  -- End of mono phase
+
+/-
     toMono,
     simp (occurrence := 3) (phase := .mono),
     reduceJpArity (phase := .mono),

src/Lean/Compiler/LCNF/Simp/DiscrM.lean

@@ -56,7 +56,7 @@ def findCtor? (fvarId : FVarId) : DiscrM (Option CtorInfo) := do
   | some { value := .value (.natVal n), .. } =>
     return some <| .natVal n
   | some { value := .const declName _ args, .. } =>
-    let .ctorInfo val ← getConstInfo declName | return none
+    let some (.ctorInfo val) := (← getEnv).find? declName | return none
     return some <| .ctor val args
   | some _ => return none
   | none => return (← read).discrCtorMap.find? fvarId

src/Lean/Compiler/LCNF/Simp/InlineProj.lean

@@ -53,7 +53,7 @@ where
     | .proj _ i s => visit s (i :: projs)
     | .fvar .. | .value .. | .erased => failure
     | .const declName us args =>
-      if let .ctorInfo ctorVal ← getConstInfo declName then
+      if let some (.ctorInfo ctorVal) := (← getEnv).find? declName then
         let i :: projs := projs | unreachable!
         let arg := args[ctorVal.numParams + i]!
         let .fvar fvarId := arg | unreachable!

src/Lean/Compiler/LCNF/Simp/SimpValue.lean

@@ -37,7 +37,7 @@ def simpAppApp? (e : LetExpr) : OptionT SimpM LetExpr := do
 
 def simpCtorDiscr? (e : LetExpr) : OptionT SimpM LetExpr := do
   let .const declName _ _ := e | failure
-  let .ctorInfo _ ← getConstInfo declName | failure
+  let some (.ctorInfo _) := (← getEnv).find? declName | failure
   let some fvarId ← simpCtorDiscrCore? e.toExpr | failure
   return .fvar fvarId #[]