From 19bde89b84619defc2a822c3bf96bdca9c97eee7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 28 Jun 2023 12:16:10 +0200
Subject: Reorganize backends/lean/Base

---
 backends/lean/Base/Diverge/ElabBase.lean | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 backends/lean/Base/Diverge/ElabBase.lean

(limited to 'backends/lean/Base/Diverge/ElabBase.lean')

diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
new file mode 100644
index 00000000..e693dce2
--- /dev/null
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -0,0 +1,9 @@
+import Lean
+
+namespace Diverge
+
+open Lean
+
+initialize registerTraceClass `Diverge.divRecursion (inherited := true)
+
+end Diverge
-- 
cgit v1.2.3


From a6de153f3bfda7feb27d16fcdf2131d37f99c7a3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 29 Jun 2023 11:22:32 +0200
Subject: Start working on Elab.lean

---
 backends/lean/Base/Diverge/ElabBase.lean | 75 +++++++++++++++++++++++++++++++-
 1 file changed, 73 insertions(+), 2 deletions(-)

(limited to 'backends/lean/Base/Diverge/ElabBase.lean')

diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
index e693dce2..84b73a30 100644
--- a/backends/lean/Base/Diverge/ElabBase.lean
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -2,8 +2,79 @@ import Lean
 
 namespace Diverge
 
-open Lean
+open Lean Elab Term Meta
 
-initialize registerTraceClass `Diverge.divRecursion (inherited := true)
+initialize registerTraceClass `Diverge.elab (inherited := true)
+initialize registerTraceClass `Diverge.def (inherited := true)
+
+-- TODO: move
+-- TODO: small helper
+def explore_term (incr : String) (e : Expr) : TermElabM Unit :=
+  match e with
+  | .bvar _ => do logInfo m!"{incr}bvar: {e}"; return ()
+  | .fvar _ => do logInfo m!"{incr}fvar: {e}"; return ()
+  | .mvar _ => do logInfo m!"{incr}mvar: {e}"; return ()
+  | .sort _ => do logInfo m!"{incr}sort: {e}"; return ()
+  | .const _ _ => do logInfo m!"{incr}const: {e}"; return ()
+  | .app fn arg => do
+    logInfo m!"{incr}app: {e}"
+    explore_term (incr ++ "  ") fn
+    explore_term (incr ++ "  ") arg
+  | .lam _bName bTy body _binfo => do
+    logInfo m!"{incr}lam: {e}"
+    explore_term (incr ++ "  ") bTy
+    explore_term (incr ++ "  ") body
+  | .forallE _bName bTy body _bInfo => do
+    logInfo m!"{incr}forallE: {e}"
+    explore_term (incr ++ "  ") bTy
+    explore_term (incr ++ "  ") body
+  | .letE _dName ty val body _nonDep => do
+    logInfo m!"{incr}letE: {e}"
+    explore_term (incr ++ "  ") ty
+    explore_term (incr ++ "  ") val
+    explore_term (incr ++ "  ") body
+  | .lit _ => do logInfo m!"{incr}lit: {e}"; return ()
+  | .mdata _ e => do
+    logInfo m!"{incr}mdata: {e}"
+    explore_term (incr ++ "  ") e
+  | .proj _ _ struct => do
+    logInfo m!"{incr}proj: {e}"
+    explore_term (incr ++ "  ") struct
+
+def explore_decl (n : Name) : TermElabM Unit := do
+  logInfo m!"Name: {n}"
+  let env ← getEnv
+  let decl := env.constants.find! n
+  match decl with
+  | .defnInfo val =>
+     logInfo m!"About to explore defn: {decl.name}"
+     logInfo m!"# Type:"
+     explore_term "" val.type
+     logInfo m!"# Value:"
+     explore_term "" val.value
+  | .axiomInfo _  => throwError m!"axiom: {n}"
+  | .thmInfo _    => throwError m!"thm: {n}"
+  | .opaqueInfo _ => throwError m!"opaque: {n}"
+  | .quotInfo _   => throwError m!"quot: {n}"
+  | .inductInfo _ => throwError m!"induct: {n}"
+  | .ctorInfo _   => throwError m!"ctor: {n}"
+  | .recInfo _    => throwError m!"rec: {n}"
+
+syntax (name := printDecl) "print_decl " ident : command
+
+open Lean.Elab.Command
+
+@[command_elab printDecl] def elabPrintDecl : CommandElab := fun stx => do
+  liftTermElabM do
+    let id := stx[1]
+    addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
+    let cs ← resolveGlobalConstWithInfos id
+    explore_decl cs[0]!
+
+private def test1 : Nat := 0
+private def test2 (x : Nat) : Nat := x
+
+print_decl test1
+print_decl test2
 
 end Diverge
-- 
cgit v1.2.3


From fdc8693772ecb1978873018c790061854f00a015 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 29 Jun 2023 23:15:20 +0200
Subject: Write function to compute the input/output types

---
 backends/lean/Base/Diverge/ElabBase.lean | 1 +
 1 file changed, 1 insertion(+)

(limited to 'backends/lean/Base/Diverge/ElabBase.lean')

diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
index 84b73a30..441b25f0 100644
--- a/backends/lean/Base/Diverge/ElabBase.lean
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -5,6 +5,7 @@ namespace Diverge
 open Lean Elab Term Meta
 
 initialize registerTraceClass `Diverge.elab (inherited := true)
+initialize registerTraceClass `Diverge.def.sigmas (inherited := true)
 initialize registerTraceClass `Diverge.def (inherited := true)
 
 -- TODO: move
-- 
cgit v1.2.3


From 1c9331ce92b68b9a83c601212149a6c24591708f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 30 Jun 2023 15:53:39 +0200
Subject: Generate the fixed-point bodies in Elab.lean

---
 backends/lean/Base/Diverge/ElabBase.lean | 47 +++++++++++++++++++++++++++++---
 1 file changed, 43 insertions(+), 4 deletions(-)

(limited to 'backends/lean/Base/Diverge/ElabBase.lean')

diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
index 441b25f0..82f79f94 100644
--- a/backends/lean/Base/Diverge/ElabBase.lean
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -4,13 +4,14 @@ namespace Diverge
 
 open Lean Elab Term Meta
 
-initialize registerTraceClass `Diverge.elab (inherited := true)
-initialize registerTraceClass `Diverge.def.sigmas (inherited := true)
-initialize registerTraceClass `Diverge.def (inherited := true)
+initialize registerTraceClass `Diverge.elab
+initialize registerTraceClass `Diverge.def
+initialize registerTraceClass `Diverge.def.sigmas
+initialize registerTraceClass `Diverge.def.genBody
 
 -- TODO: move
 -- TODO: small helper
-def explore_term (incr : String) (e : Expr) : TermElabM Unit :=
+def explore_term (incr : String) (e : Expr) : MetaM Unit :=
   match e with
   | .bvar _ => do logInfo m!"{incr}bvar: {e}"; return ()
   | .fvar _ => do logInfo m!"{incr}fvar: {e}"; return ()
@@ -78,4 +79,42 @@ private def test2 (x : Nat) : Nat := x
 print_decl test1
 print_decl test2
 
+-- We adapted this from AbstractNestedProofs.visit
+-- A map visitor function for expressions
+partial def mapVisit (k : Expr → MetaM Expr) (e : Expr) : MetaM Expr := do
+  let mapVisitBinders (xs : Array Expr) (k2 : MetaM Expr) : MetaM Expr := do
+    let localInstances ← getLocalInstances
+    let mut lctx ← getLCtx
+    for x in xs do
+      let xFVarId := x.fvarId!
+      let localDecl ← xFVarId.getDecl
+      let type      ← mapVisit k localDecl.type
+      let localDecl := localDecl.setType type
+      let localDecl ← match localDecl.value? with
+         | some value => let value ← mapVisit k value; pure <| localDecl.setValue value
+         | none       => pure localDecl
+      lctx :=lctx.modifyLocalDecl xFVarId fun _ => localDecl
+    withLCtx lctx localInstances k2
+  -- TODO: use a cache? (Lean.checkCache)
+  -- Explore
+  let e ← k e
+  match e with
+  | .bvar _
+  | .fvar _
+  | .mvar _
+  | .sort _
+  | .lit _
+  | .const _ _ => pure e
+  | .app .. => do e.withApp fun f args => return mkAppN f (← args.mapM (mapVisit k))
+  | .lam .. =>
+    lambdaLetTelescope e fun xs b =>
+      mapVisitBinders xs do mkLambdaFVars xs (← mapVisit k b) (usedLetOnly := false)
+  | .forallE .. => do
+    forallTelescope e fun xs b => mapVisitBinders xs do mkForallFVars xs (← mapVisit k b)
+  | .letE .. => do
+    lambdaLetTelescope e fun xs b => mapVisitBinders xs do
+      mkLambdaFVars xs (← mapVisit k b) (usedLetOnly := false)
+  | .mdata _ b => return e.updateMData! (← mapVisit k b)
+  | .proj _ _ b => return e.updateProj! (← mapVisit k b)
+
 end Diverge
-- 
cgit v1.2.3


From 37e5d5501e024869037bf0ea1559229a8be62da7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 3 Jul 2023 16:24:44 +0200
Subject: Generate the proofs of validity in Elab.lean

---
 backends/lean/Base/Diverge/ElabBase.lean | 1 +
 1 file changed, 1 insertion(+)

(limited to 'backends/lean/Base/Diverge/ElabBase.lean')

diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
index 82f79f94..281dbd6c 100644
--- a/backends/lean/Base/Diverge/ElabBase.lean
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -8,6 +8,7 @@ initialize registerTraceClass `Diverge.elab
 initialize registerTraceClass `Diverge.def
 initialize registerTraceClass `Diverge.def.sigmas
 initialize registerTraceClass `Diverge.def.genBody
+initialize registerTraceClass `Diverge.def.valid
 
 -- TODO: move
 -- TODO: small helper
-- 
cgit v1.2.3


From 9214484c471ad931924865855687f9a2ffe255dd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 3 Jul 2023 18:02:52 +0200
Subject: Automate the proofs of the unfolding theorems for Diverge

---
 backends/lean/Base/Diverge/ElabBase.lean | 1 +
 1 file changed, 1 insertion(+)

(limited to 'backends/lean/Base/Diverge/ElabBase.lean')

diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
index 281dbd6c..fd95291e 100644
--- a/backends/lean/Base/Diverge/ElabBase.lean
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -9,6 +9,7 @@ initialize registerTraceClass `Diverge.def
 initialize registerTraceClass `Diverge.def.sigmas
 initialize registerTraceClass `Diverge.def.genBody
 initialize registerTraceClass `Diverge.def.valid
+initialize registerTraceClass `Diverge.def.unfold
 
 -- TODO: move
 -- TODO: small helper
-- 
cgit v1.2.3


From 4fd17e4bb91eb46d4704643dfbfbbf0874837b07 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jul 2023 12:49:37 +0200
Subject: Make Diverge use Primitives

---
 backends/lean/Base/Diverge/ElabBase.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'backends/lean/Base/Diverge/ElabBase.lean')

diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
index fd95291e..1c1062c0 100644
--- a/backends/lean/Base/Diverge/ElabBase.lean
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -4,6 +4,7 @@ namespace Diverge
 
 open Lean Elab Term Meta
 
+-- We can't define and use trace classes in the same file
 initialize registerTraceClass `Diverge.elab
 initialize registerTraceClass `Diverge.def
 initialize registerTraceClass `Diverge.def.sigmas
@@ -11,8 +12,8 @@ initialize registerTraceClass `Diverge.def.genBody
 initialize registerTraceClass `Diverge.def.valid
 initialize registerTraceClass `Diverge.def.unfold
 
--- TODO: move
--- TODO: small helper
+-- Useful helper to explore definitions and figure out the variant
+-- of their sub-expressions.
 def explore_term (incr : String) (e : Expr) : MetaM Unit :=
   match e with
   | .bvar _ => do logInfo m!"{incr}bvar: {e}"; return ()
@@ -81,8 +82,7 @@ private def test2 (x : Nat) : Nat := x
 print_decl test1
 print_decl test2
 
--- We adapted this from AbstractNestedProofs.visit
--- A map visitor function for expressions
+-- A map visitor function for expressions (adapted from `AbstractNestedProofs.visit`)
 partial def mapVisit (k : Expr → MetaM Expr) (e : Expr) : MetaM Expr := do
   let mapVisitBinders (xs : Array Expr) (k2 : MetaM Expr) : MetaM Expr := do
     let localInstances ← getLocalInstances
-- 
cgit v1.2.3


From 442caaf62e4a217b9a10116c4e529c49f83c4efd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jul 2023 22:45:02 +0200
Subject: Fix an issue with mkSigmasVal

---
 backends/lean/Base/Diverge/ElabBase.lean | 47 ++++++++++++++++++--------------
 1 file changed, 26 insertions(+), 21 deletions(-)

(limited to 'backends/lean/Base/Diverge/ElabBase.lean')

diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
index 1c1062c0..aaaea6f7 100644
--- a/backends/lean/Base/Diverge/ElabBase.lean
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -83,7 +83,10 @@ print_decl test1
 print_decl test2
 
 -- A map visitor function for expressions (adapted from `AbstractNestedProofs.visit`)
-partial def mapVisit (k : Expr → MetaM Expr) (e : Expr) : MetaM Expr := do
+-- The continuation takes as parameters:
+-- - the current depth of the expression (useful for printing/debugging)
+-- - the expression to explore
+partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr := do
   let mapVisitBinders (xs : Array Expr) (k2 : MetaM Expr) : MetaM Expr := do
     let localInstances ← getLocalInstances
     let mut lctx ← getLCtx
@@ -98,25 +101,27 @@ partial def mapVisit (k : Expr → MetaM Expr) (e : Expr) : MetaM Expr := do
       lctx :=lctx.modifyLocalDecl xFVarId fun _ => localDecl
     withLCtx lctx localInstances k2
   -- TODO: use a cache? (Lean.checkCache)
-  -- Explore
-  let e ← k e
-  match e with
-  | .bvar _
-  | .fvar _
-  | .mvar _
-  | .sort _
-  | .lit _
-  | .const _ _ => pure e
-  | .app .. => do e.withApp fun f args => return mkAppN f (← args.mapM (mapVisit k))
-  | .lam .. =>
-    lambdaLetTelescope e fun xs b =>
-      mapVisitBinders xs do mkLambdaFVars xs (← mapVisit k b) (usedLetOnly := false)
-  | .forallE .. => do
-    forallTelescope e fun xs b => mapVisitBinders xs do mkForallFVars xs (← mapVisit k b)
-  | .letE .. => do
-    lambdaLetTelescope e fun xs b => mapVisitBinders xs do
-      mkLambdaFVars xs (← mapVisit k b) (usedLetOnly := false)
-  | .mdata _ b => return e.updateMData! (← mapVisit k b)
-  | .proj _ _ b => return e.updateProj! (← mapVisit k b)
+  let rec visit (i : Nat) (e : Expr) : MetaM Expr := do
+    -- Explore
+    let e ← k i e
+    match e with
+    | .bvar _
+    | .fvar _
+    | .mvar _
+    | .sort _
+    | .lit _
+    | .const _ _ => pure e
+    | .app .. => do e.withApp fun f args => return mkAppN f (← args.mapM (visit (i + 1)))
+    | .lam .. =>
+      lambdaLetTelescope e fun xs b =>
+        mapVisitBinders xs do mkLambdaFVars xs (← visit (i + 1) b) (usedLetOnly := false)
+    | .forallE .. => do
+      forallTelescope e fun xs b => mapVisitBinders xs do mkForallFVars xs (← visit (i + 1) b)
+    | .letE .. => do
+      lambdaLetTelescope e fun xs b => mapVisitBinders xs do
+        mkLambdaFVars xs (← visit (i + 1) b) (usedLetOnly := false)
+    | .mdata _ b => return e.updateMData! (← visit (i + 1) b)
+    | .proj _ _ b => return e.updateProj! (← visit (i + 1) b)
+  visit 0 e
 
 end Diverge
-- 
cgit v1.2.3


From 0d1ac53f88f947ae94f6afb57b2a7e18a77460a7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 9 Jul 2023 10:11:13 +0200
Subject: Make progress on the int tactic

---
 backends/lean/Base/Diverge/ElabBase.lean | 112 -------------------------------
 1 file changed, 112 deletions(-)

(limited to 'backends/lean/Base/Diverge/ElabBase.lean')

diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
index aaaea6f7..fedb1c74 100644
--- a/backends/lean/Base/Diverge/ElabBase.lean
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -12,116 +12,4 @@ initialize registerTraceClass `Diverge.def.genBody
 initialize registerTraceClass `Diverge.def.valid
 initialize registerTraceClass `Diverge.def.unfold
 
--- Useful helper to explore definitions and figure out the variant
--- of their sub-expressions.
-def explore_term (incr : String) (e : Expr) : MetaM Unit :=
-  match e with
-  | .bvar _ => do logInfo m!"{incr}bvar: {e}"; return ()
-  | .fvar _ => do logInfo m!"{incr}fvar: {e}"; return ()
-  | .mvar _ => do logInfo m!"{incr}mvar: {e}"; return ()
-  | .sort _ => do logInfo m!"{incr}sort: {e}"; return ()
-  | .const _ _ => do logInfo m!"{incr}const: {e}"; return ()
-  | .app fn arg => do
-    logInfo m!"{incr}app: {e}"
-    explore_term (incr ++ "  ") fn
-    explore_term (incr ++ "  ") arg
-  | .lam _bName bTy body _binfo => do
-    logInfo m!"{incr}lam: {e}"
-    explore_term (incr ++ "  ") bTy
-    explore_term (incr ++ "  ") body
-  | .forallE _bName bTy body _bInfo => do
-    logInfo m!"{incr}forallE: {e}"
-    explore_term (incr ++ "  ") bTy
-    explore_term (incr ++ "  ") body
-  | .letE _dName ty val body _nonDep => do
-    logInfo m!"{incr}letE: {e}"
-    explore_term (incr ++ "  ") ty
-    explore_term (incr ++ "  ") val
-    explore_term (incr ++ "  ") body
-  | .lit _ => do logInfo m!"{incr}lit: {e}"; return ()
-  | .mdata _ e => do
-    logInfo m!"{incr}mdata: {e}"
-    explore_term (incr ++ "  ") e
-  | .proj _ _ struct => do
-    logInfo m!"{incr}proj: {e}"
-    explore_term (incr ++ "  ") struct
-
-def explore_decl (n : Name) : TermElabM Unit := do
-  logInfo m!"Name: {n}"
-  let env ← getEnv
-  let decl := env.constants.find! n
-  match decl with
-  | .defnInfo val =>
-     logInfo m!"About to explore defn: {decl.name}"
-     logInfo m!"# Type:"
-     explore_term "" val.type
-     logInfo m!"# Value:"
-     explore_term "" val.value
-  | .axiomInfo _  => throwError m!"axiom: {n}"
-  | .thmInfo _    => throwError m!"thm: {n}"
-  | .opaqueInfo _ => throwError m!"opaque: {n}"
-  | .quotInfo _   => throwError m!"quot: {n}"
-  | .inductInfo _ => throwError m!"induct: {n}"
-  | .ctorInfo _   => throwError m!"ctor: {n}"
-  | .recInfo _    => throwError m!"rec: {n}"
-
-syntax (name := printDecl) "print_decl " ident : command
-
-open Lean.Elab.Command
-
-@[command_elab printDecl] def elabPrintDecl : CommandElab := fun stx => do
-  liftTermElabM do
-    let id := stx[1]
-    addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
-    let cs ← resolveGlobalConstWithInfos id
-    explore_decl cs[0]!
-
-private def test1 : Nat := 0
-private def test2 (x : Nat) : Nat := x
-
-print_decl test1
-print_decl test2
-
--- A map visitor function for expressions (adapted from `AbstractNestedProofs.visit`)
--- The continuation takes as parameters:
--- - the current depth of the expression (useful for printing/debugging)
--- - the expression to explore
-partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr := do
-  let mapVisitBinders (xs : Array Expr) (k2 : MetaM Expr) : MetaM Expr := do
-    let localInstances ← getLocalInstances
-    let mut lctx ← getLCtx
-    for x in xs do
-      let xFVarId := x.fvarId!
-      let localDecl ← xFVarId.getDecl
-      let type      ← mapVisit k localDecl.type
-      let localDecl := localDecl.setType type
-      let localDecl ← match localDecl.value? with
-         | some value => let value ← mapVisit k value; pure <| localDecl.setValue value
-         | none       => pure localDecl
-      lctx :=lctx.modifyLocalDecl xFVarId fun _ => localDecl
-    withLCtx lctx localInstances k2
-  -- TODO: use a cache? (Lean.checkCache)
-  let rec visit (i : Nat) (e : Expr) : MetaM Expr := do
-    -- Explore
-    let e ← k i e
-    match e with
-    | .bvar _
-    | .fvar _
-    | .mvar _
-    | .sort _
-    | .lit _
-    | .const _ _ => pure e
-    | .app .. => do e.withApp fun f args => return mkAppN f (← args.mapM (visit (i + 1)))
-    | .lam .. =>
-      lambdaLetTelescope e fun xs b =>
-        mapVisitBinders xs do mkLambdaFVars xs (← visit (i + 1) b) (usedLetOnly := false)
-    | .forallE .. => do
-      forallTelescope e fun xs b => mapVisitBinders xs do mkForallFVars xs (← visit (i + 1) b)
-    | .letE .. => do
-      lambdaLetTelescope e fun xs b => mapVisitBinders xs do
-        mkLambdaFVars xs (← visit (i + 1) b) (usedLetOnly := false)
-    | .mdata _ b => return e.updateMData! (← visit (i + 1) b)
-    | .proj _ _ b => return e.updateProj! (← visit (i + 1) b)
-  visit 0 e
-
 end Diverge
-- 
cgit v1.2.3

