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