From a0894dedbb7e77985676e8c8f0d01b74628ed2e8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 Oct 2022 03:28:20 -0700
Subject: [PATCH] feat: add `phaseOut` field to `Pass`

We need it for passes that move the code from one phase to another.

See `toMono` pass.

cc @hargoniX
---
 src/Lean/Compiler/LCNF/Main.lean        |  2 +-
 src/Lean/Compiler/LCNF/PassManager.lean | 44 ++++++++++++++-----------
 src/Lean/Compiler/LCNF/ToMono.lean      |  7 ++--
 3 files changed, 30 insertions(+), 23 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean
index c72feda8b9..ccaafaae57 100644
--- a/src/Lean/Compiler/LCNF/Main.lean
+++ b/src/Lean/Compiler/LCNF/Main.lean
@@ -73,7 +73,7 @@ def run (declNames : Array Name) : CompilerM (Array Decl) := withAtLeastMaxRecDe
   for pass in manager.passes do
     trace[Compiler] s!"Running pass: {pass.name}"
     decls ← withPhase pass.phase <| pass.run decls
-    withPhase pass.phase <| checkpoint pass.name decls
+    withPhase pass.phaseOut <| checkpoint pass.name decls
   if (← Lean.isTracingEnabledFor `Compiler.result) then
     for decl in decls do
       -- We display the declaration saved in the environment because the names have been normalized
diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean
index 2ec91334cb..79774019a9 100644
--- a/src/Lean/Compiler/LCNF/PassManager.lean
+++ b/src/Lean/Compiler/LCNF/PassManager.lean
@@ -10,6 +10,23 @@ import Lean.Compiler.LCNF.CompilerM
 
 namespace Lean.Compiler.LCNF
 
+def Phase.toNat : Phase → Nat
+  | .base => 0
+  | .mono => 1
+  | .impure => 2
+
+instance : LT Phase where
+  lt l r := l.toNat < r.toNat
+
+instance : LE Phase where
+  le l r := l.toNat ≤ r.toNat
+
+instance {p1 p2 : Phase} : Decidable (p1 < p2) := Nat.decLt p1.toNat p2.toNat
+instance {p1 p2 : Phase} : Decidable (p1 ≤ p2) := Nat.decLe p1.toNat p2.toNat
+
+@[simp] theorem Phase.le_refl (p : Phase) : p ≤ p := by
+  cases p <;> decide
+
 /--
 A single compiler `Pass`, consisting of the actual pass function operating
 on the `Decl`s as well as meta information.
@@ -26,6 +43,11 @@ structure Pass where
   -/
   phase : Phase
   /--
+  Resulting phase.
+  -/
+  phaseOut : Phase := phase
+  phaseInv : phaseOut ≥ phase := by simp
+  /--
   The name of the `Pass`
   -/
   name : Name
@@ -33,7 +55,9 @@ structure Pass where
   The actual pass function, operating on the `Decl`s.
   -/
   run : Array Decl → CompilerM (Array Decl)
-  deriving Inhabited
+
+instance : Inhabited Pass where
+  default := { phase := .base, name := default, run := fun decls => return decls }
 
 /--
 Can be used to install, remove, replace etc. passes by tagging a declaration
@@ -56,30 +80,12 @@ structure PassManager where
   passes : Array Pass
   deriving Inhabited
 
-namespace Phase
-
-def toNat : Phase → Nat
-  | .base => 0
-  | .mono => 1
-  | .impure => 2
-
-instance : LT Phase where
-  lt l r := l.toNat < r.toNat
-
-instance : LE Phase where
-  le l r := l.toNat ≤ r.toNat
-
-instance {p1 p2 : Phase} : Decidable (p1 < p2) := Nat.decLt p1.toNat p2.toNat
-instance {p1 p2 : Phase} : Decidable (p1 ≤ p2) := Nat.decLe p1.toNat p2.toNat
-
 instance : ToString Phase where
   toString
     | .base => "base"
     | .mono => "mono"
     | .impure => "impure"
 
-end Phase
-
 namespace Pass
 
 def mkPerDeclaration (name : Name) (run : Decl → CompilerM Decl) (phase : Phase) (occurrence : Nat := 0) : Pass where
diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean
index 29a524bbab..1ca6d95a48 100644
--- a/src/Lean/Compiler/LCNF/ToMono.lean
+++ b/src/Lean/Compiler/LCNF/ToMono.lean
@@ -67,9 +67,10 @@ def Decl.toMono (decl : Decl) : CompilerM Decl := do
   return decl
 
 def toMono : Pass where
-  name  := `toMono
-  run   := fun decls => decls.mapM (·.toMono)
-  phase := .base
+  name     := `toMono
+  run      := fun decls => decls.mapM (·.toMono)
+  phase    := .base
+  phaseOut := .mono
 
 builtin_initialize
   registerTraceClass `Compiler.toMono (inherited := true)