feat: reactivate extendJoinPointContext at mono phase

closes #1686 cc @hargoniX
leanprover · Oct 7, 2022 · 4597422 · 4597422
1 parent 15ad525
commit 4597422
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 5 deletions.
diff --git a/src/Lean/Compiler/LCNF/JoinPoints.lean b/src/Lean/Compiler/LCNF/JoinPoints.lean
@@ -534,7 +534,7 @@ def Decl.extendJoinPointContext (decl : Decl) : CompilerM Decl := do
   JoinPointContextExtender.extend decl
 
 def extendJoinPointContext : Pass :=
-  .mkPerDeclaration `extendJoinPointContext Decl.extendJoinPointContext .base
+  .mkPerDeclaration `extendJoinPointContext Decl.extendJoinPointContext .mono
 
 builtin_initialize
   registerTraceClass `Compiler.extendJoinPointContext (inherited := true)

diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean
@@ -55,6 +55,10 @@ def builtinPassManager : PassManager := {
     cse,
     saveBase, -- End of base phase
     toMono,
+    simp (occurrence := 3) (phase := .mono),
+    reduceJpArity (phase := .mono),
+    extendJoinPointContext,
+    simp (occurrence := 4) (phase := .mono),
     -- TODO: lambda lifting, reduce function arity
     saveMono  -- End of mono phase
   ]

diff --git a/src/Lean/Compiler/LCNF/ReduceJpArity.lean b/src/Lean/Compiler/LCNF/ReduceJpArity.lean
@@ -70,8 +70,8 @@ def Decl.reduceJpArity (decl : Decl) : CompilerM Decl := do
   let value ← reduce decl.value |>.run {}
   return { decl with value }
 
-def reduceJpArity : Pass :=
-  .mkPerDeclaration `reduceJpArity Decl.reduceJpArity .base
+def reduceJpArity (phase := Phase.base) : Pass :=
+  .mkPerDeclaration `reduceJpArity Decl.reduceJpArity phase
 
 builtin_initialize
   registerTraceClass `Compiler.reduceJpArity (inherited := true)

diff --git a/src/Lean/Compiler/LCNF/Simp.lean b/src/Lean/Compiler/LCNF/Simp.lean
@@ -56,8 +56,8 @@ where
     else
       return decl
 
-def simp (config : Config := {}) (occurrence : Nat := 0) : Pass :=
-  .mkPerDeclaration `simp (Decl.simp · config) .base (occurrence := occurrence)
+def simp (config : Config := {}) (occurrence : Nat := 0) (phase := Phase.base) : Pass :=
+  .mkPerDeclaration `simp (Decl.simp · config) phase (occurrence := occurrence)
 
 builtin_initialize
   registerTraceClass `Compiler.simp (inherited := true)

diff --git a/tests/lean/run/1686.lean b/tests/lean/run/1686.lean
@@ -0,0 +1,7 @@
+import Lean
+open Lean Meta
+
+def substIssue (hLocalDecl : LocalDecl) : MetaM Unit := do
+  let error {α} _ : MetaM α := throwError "{hLocalDecl.type}"
+  let some (_, lhs, rhs) ← matchEq? hLocalDecl.type | error ()
+  error ()