From eaade5abde63d12cc447b17ea99a4a3038b5dee0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Nov 2022 18:35:18 -0700
Subject: [PATCH] chore: port `LambdaLifting.lean`

---
 src/Lean/Compiler/LCNF/CompilerM.lean       | 2 +-
 src/Lean/Compiler/LCNF/LambdaLifting.lean   | 6 +-----
 src/Lean/Compiler/LCNF/Passes.lean          | 9 ++++++---
 src/Lean/Compiler/LCNF/Simp/DiscrM.lean     | 2 +-
 src/Lean/Compiler/LCNF/Simp/InlineProj.lean | 2 +-
 src/Lean/Compiler/LCNF/Simp/SimpValue.lean  | 2 +-
 6 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/CompilerM.lean b/src/Lean/Compiler/LCNF/CompilerM.lean
index d36f264e10..d13ff8ac68 100644
--- a/src/Lean/Compiler/LCNF/CompilerM.lean
+++ b/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
diff --git a/src/Lean/Compiler/LCNF/LambdaLifting.lean b/src/Lean/Compiler/LCNF/LambdaLifting.lean
index fdfc516265..f75dbd8807 100644
--- a/src/Lean/Compiler/LCNF/LambdaLifting.lean
+++ b/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
-
diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean
index c57b7a72f5..47144d4632 100644
--- a/src/Lean/Compiler/LCNF/Passes.lean
+++ b/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),
diff --git a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean
index f0420c3ef3..913e531766 100644
--- a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean
+++ b/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
diff --git a/src/Lean/Compiler/LCNF/Simp/InlineProj.lean b/src/Lean/Compiler/LCNF/Simp/InlineProj.lean
index 5b607f6f00..e3f0b56c67 100644
--- a/src/Lean/Compiler/LCNF/Simp/InlineProj.lean
+++ b/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!
diff --git a/src/Lean/Compiler/LCNF/Simp/SimpValue.lean b/src/Lean/Compiler/LCNF/Simp/SimpValue.lean
index 2437a0e0c9..6b7de7416c 100644
--- a/src/Lean/Compiler/LCNF/Simp/SimpValue.lean
+++ b/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 #[]