From 98ad1ae2831c3136d7ff3c56869272323625a111 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 14 Mar 2025 16:54:34 -0700
Subject: [PATCH 1/8] feat(delate): Tracing tags
---
Pantograph/Delate.lean | 26 +++++++++++++++-----------
1 file changed, 15 insertions(+), 11 deletions(-)
diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index ad923aa..44c09a9 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -85,13 +85,13 @@ This function ensures any metavariable in the result is either
1. Delayed assigned with its pending mvar not assigned in any form
2. Not assigned (delay or not)
-/
-partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
+partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr :=
--let padding := String.join $ List.replicate level "│ "
- --IO.println s!"{padding}Starting {toString eOrig}"
+ withTraceNode `Pantograph.Delate (λ _ex => return m!":= {← Meta.ppExpr eOrig}") do
let mut result ← Meta.transform (← instantiateMVars eOrig)
(pre := fun e => e.withApp fun f args => do
let .mvar mvarId := f | return .continue
- --IO.println s!"{padding}├V {e}"
+ trace[Pantograph.Delate] "V {e}"
let mvarDecl ← mvarId.getDecl
-- This is critical to maintaining the interdependency of metavariables.
@@ -109,12 +109,13 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
if let .some assign ← getExprMVarAssignment? mvarId then
- --IO.println s!"{padding}├A ?{mvarId.name}"
+ trace[Pantograph.Delate] "A ?{mvarId.name}"
assert! !(← mvarId.isDelayedAssigned)
return .visit (mkAppN assign args)
else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
- --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
- --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
+ if ← isTracingEnabledFor `Pantograph.Delate then
+ let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
+ trace[Pantograph.Delate]"MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
if args.size < fvars.size then
throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
@@ -124,18 +125,18 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
--if !args.isEmpty then
--IO.println s!"{padding}├── Arguments End"
if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
- --IO.println s!"{padding}├T1"
+ trace[Pantograph.Delate] "T1"
let result := mkAppN f args
return .done result
let pending ← mvarIdPending.withContext do
let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
- --IO.println s!"{padding}├Pre: {inner}"
+ trace[Pantograph.Delate] "Pre: {inner}"
pure <| (← inner.abstractM fvars).instantiateRev args
-- Tail arguments
let result := mkAppRange pending fvars.size args.size args
- --IO.println s!"{padding}├MD {result}"
+ trace[Pantograph.Delate] "MD {result}"
return .done result
else
assert! !(← mvarId.isAssigned)
@@ -146,9 +147,9 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
--if !args.isEmpty then
-- IO.println s!"{padding}├── Arguments End"
- --IO.println s!"{padding}├M ?{mvarId.name}"
+ trace[Pantograph.Delate] "M ?{mvarId.name}"
return .done (mkAppN f args))
- --IO.println s!"{padding}└Result {result}"
+ trace[Pantoraph.Delate] "Result {result}"
return result
where
self e := instantiateDelayedMVars e --(level := level + 1)
@@ -594,4 +595,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
| other => s!"[{other}]"
parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
+initialize
+ registerTraceClass `Pantograph.Delate
+
end Pantograph
From 78485ae6e23ee1d5a4e2bb15c610b5543c2535d3 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 14 Mar 2025 20:07:31 -0700
Subject: [PATCH 2/8] doc(frontend): Update documentation for
`frontend.process`
---
Pantograph/Protocol.lean | 5 ++---
doc/repl.md | 7 ++++---
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 164b72a..7924db7 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -346,10 +346,9 @@ structure FrontendProcess where
-- One of these two must be supplied: Either supply the file name or the content.
fileName?: Option String := .none
file?: Option String := .none
- -- If set to true, read the header (otherwise discards the header)
+ -- Whether to read the header
readHeader : Bool := false
- -- If set to true, Pantograph's environment will be altered to whatever is
- -- after the compilation units.
+ -- Alter the REPL environment after the compilation units.
inheritEnv : Bool := false
-- collect tactic invocations
invocations: Bool := false
diff --git a/doc/repl.md b/doc/repl.md
index a86c01b..93eb6ab 100644
--- a/doc/repl.md
+++ b/doc/repl.md
@@ -46,14 +46,15 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
Save/Load a goal state to/from a file. The environment is not carried with the
state. The user is responsible to ensure the sender/receiver instances share
the same environment.
-* `frontend.process { ["fileName": <fileName>,] ["file": <str>], invocations:
+* `frontend.process { ["fileName": <fileName>,] ["file": <str>], readHeader: <bool>, inheritEnv: <bool>, invocations:
<bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
Executes the Lean frontend on a file, collecting the tactic invocations
(`"invocations": true`), the sorrys and type errors into goal states
(`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
`sorrys`, this command additionally outputs the position of each captured
- `sorry`. Warning: Behaviour is unstable in case of multiple `sorry`s. Use the
- draft tactic if possible.
+ `sorry`. Conditionally inherit the environment from executing the file.
+ Warning: Behaviour is unstable in case of multiple `sorry`s. Use the draft
+ tactic if possible.
## Errors
From dc29d48b774cc32c3f67219746a6b4539348c700 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 17 Mar 2025 09:31:39 -0700
Subject: [PATCH 3/8] chore: Remove IO.println for trace
---
Pantograph/Delate.lean | 18 +++++++++---------
Pantograph/Frontend/MetaTranslate.lean | 9 ++++++---
2 files changed, 15 insertions(+), 12 deletions(-)
diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 44c09a9..2fff009 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -119,11 +119,11 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr :=
if args.size < fvars.size then
throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
- --if !args.isEmpty then
- --IO.println s!"{padding}├── Arguments Begin"
+ if !args.isEmpty then
+ trace[Pantograph.Delate] "─ Arguments Begin"
let args ← args.mapM self
- --if !args.isEmpty then
- --IO.println s!"{padding}├── Arguments End"
+ if !args.isEmpty then
+ trace[Pantograph.Delate] "─ Arguments End"
if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
trace[Pantograph.Delate] "T1"
let result := mkAppN f args
@@ -141,18 +141,18 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr :=
else
assert! !(← mvarId.isAssigned)
assert! !(← mvarId.isDelayedAssigned)
- --if !args.isEmpty then
- -- IO.println s!"{padding}├── Arguments Begin"
+ if !args.isEmpty then
+ trace[Pantograph.Delate] "─ Arguments Begin"
let args ← args.mapM self
- --if !args.isEmpty then
- -- IO.println s!"{padding}├── Arguments End"
+ if !args.isEmpty then
+ trace[Pantograph.Delate] "─ Arguments End"
trace[Pantograph.Delate] "M ?{mvarId.name}"
return .done (mkAppN f args))
trace[Pantoraph.Delate] "Result {result}"
return result
where
- self e := instantiateDelayedMVars e --(level := level + 1)
+ self e := instantiateDelayedMVars e
/--
Convert an expression to an equiavlent form with
diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean
index c6592d2..8067d17 100644
--- a/Pantograph/Frontend/MetaTranslate.lean
+++ b/Pantograph/Frontend/MetaTranslate.lean
@@ -62,7 +62,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
let sourceMCtx ← getSourceMCtx
-- We want to create as few mvars as possible
let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr
- --IO.println s!"Transform src: {srcExpr}"
+ trace[Pantograph.Frontend.MetaTranslate] "Transform src: {srcExpr}"
let result ← Core.transform srcExpr λ e => do
let state ← get
match e with
@@ -100,10 +100,10 @@ partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalD
addTranslatedFVar srcLocalDecl.fvarId fvarId
match srcLocalDecl with
| .cdecl index _ userName type bi kind => do
- --IO.println s!"[CD] {userName} {toString type}"
+ trace[Pantograph.Frontend.MetaTranslate] "[CD] {userName} {toString type}"
return .cdecl index fvarId userName (← translateExpr type) bi kind
| .ldecl index _ userName type value nonDep kind => do
- --IO.println s!"[LD] {toString type} := {toString value}"
+ trace[Pantograph.Frontend.MetaTranslate] "[LD] {toString type} := {toString value}"
return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind
partial def translateLCtx : MetaTranslateM LocalContext := do
@@ -162,4 +162,7 @@ end MetaTranslate
export MetaTranslate (MetaTranslateM)
+initialize
+ registerTraceClass `Pantograph.Frontend.MetaTranslate
+
end Pantograph.Frontend
From a28ad9b239553ed9cd9d776daf14ef8e10f5954d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 17 Mar 2025 10:47:11 -0700
Subject: [PATCH 4/8] feat(delate): Expand matcher applications
---
Pantograph/Delate.lean | 9 ++++++++-
Test/Common.lean | 4 ++--
Test/Delate.lean | 13 ++++++++++---
3 files changed, 20 insertions(+), 6 deletions(-)
diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 2fff009..1a4af5d 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -66,7 +66,7 @@ def exprProjToApp (env: Environment) (e: Expr): Expr :=
def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-@[export pantograph_unfold_aux_lemmas]
+@[export pantograph_unfold_aux_lemmas_m]
def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
@@ -164,6 +164,13 @@ Convert an expression to an equiavlent form with
def instantiateAll (e: Expr): MetaM Expr := do
let e ← instantiateDelayedMVars e
let e ← unfoldAuxLemmas e
+ let e ← Core.transform e λ e' => do
+ match ← Meta.matchMatcherApp? e' with
+ | .none => return .continue e'
+ | .some mapp =>
+ let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist"
+ let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList
+ return .visit (f.betaRev e'.getAppRevArgs (useZeta := true))
return e
structure DelayedMVarInvocation where
diff --git a/Test/Common.lean b/Test/Common.lean
index 5274bad..c32d62d 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -108,7 +108,7 @@ def strToTermSyntax (s: String): CoreM Syntax := do
(input := s)
(fileName := ← getFileName) | panic! s!"Failed to parse {s}"
return stx
-def parseSentence (s: String): Elab.TermElabM Expr := do
+def parseSentence (s : String) (expectedType? : Option Expr := .none) : Elab.TermElabM Expr := do
let stx ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
@@ -116,7 +116,7 @@ def parseSentence (s: String): Elab.TermElabM Expr := do
(fileName := ← getFileName) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
- Elab.Term.elabTerm (stx := stx) .none
+ Elab.Term.elabTerm (stx := stx) expectedType?
def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
diff --git a/Test/Delate.lean b/Test/Delate.lean
index 517a394..7c5eec3 100644
--- a/Test/Delate.lean
+++ b/Test/Delate.lean
@@ -3,10 +3,9 @@ import Pantograph.Delate
import Test.Common
import Lean
-open Lean
-namespace Pantograph.Test.Delate
+open Lean Pantograph
-open Pantograph
+namespace Pantograph.Test.Delate
deriving instance Repr, DecidableEq for Protocol.BoundExpression
@@ -113,6 +112,13 @@ def test_projection_exists (env: Environment) : IO LSpec.TestSeq:= runTest do
checkEq "numParams" numParams 2
checkEq "numFields" numFields 2
+def test_matcher : TestT Elab.TermElabM Unit := do
+ let t ← parseSentence "Nat → Nat"
+ let e ← parseSentence "fun (n : Nat) => match n with | 0 => 0 | k => k" (.some t)
+ let .some _ ← Meta.matchMatcherApp? e.bindingBody! | fail "Must be a matcher app"
+ let e' ← instantiateAll e
+ checkTrue "ok" <| ← Meta.isTypeCorrect e'
+
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("serializeName", do pure test_serializeName),
@@ -123,6 +129,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
("Instance", test_instance env),
("Projection Prod", test_projection_prod env),
("Projection Exists", test_projection_exists env),
+ ("Matcher", runTestTermElabM env test_matcher),
]
end Pantograph.Test.Delate
From 3b4b196a302c3c74c0ebabea0435fa8e1e602950 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 17 Mar 2025 11:20:38 -0700
Subject: [PATCH 5/8] feat(delate): Add mdata annotation for matcher
---
Pantograph/Delate.lean | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 1a4af5d..5060d25 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -170,7 +170,8 @@ def instantiateAll (e: Expr): MetaM Expr := do
| .some mapp =>
let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist"
let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList
- return .visit (f.betaRev e'.getAppRevArgs (useZeta := true))
+ let mdata := KVMap.empty.insert `matcher (DataValue.ofName mapp.matcherName)
+ return .visit $ .mdata mdata (f.betaRev e'.getAppRevArgs (useZeta := true))
return e
structure DelayedMVarInvocation where
From 4643992c3bb18b4a96b1cf755b709123b6137f63 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 17 Mar 2025 11:26:13 -0700
Subject: [PATCH 6/8] refactor(delate): Unfold matchers into function
---
Pantograph/Delate.lean | 32 +++++++++++++++++---------------
1 file changed, 17 insertions(+), 15 deletions(-)
diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 5060d25..3ef2c35 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -67,8 +67,17 @@ def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
@[export pantograph_unfold_aux_lemmas_m]
-def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
- Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
+def unfoldAuxLemmas : Expr → CoreM Expr :=
+ (Lean.Meta.deltaExpand · Lean.Name.isAuxLemma)
+/-- Unfold all matcher applications -/
+@[export pantograph_unfold_matchers_m]
+def unfoldMatchers (expr : Expr) : CoreM Expr :=
+ Core.transform expr λ e' => do
+ let .some mapp ← Meta.matchMatcherApp? e' | return .continue e'
+ let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist"
+ let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList
+ let mdata := KVMap.empty.insert `matcher (DataValue.ofName mapp.matcherName)
+ return .visit $ .mdata mdata (f.betaRev e'.getAppRevArgs (useZeta := true))
/--
Force the instantiation of delayed metavariables even if they cannot be fully
@@ -157,28 +166,21 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr :=
/--
Convert an expression to an equiavlent form with
1. No nested delayed assigned mvars
-2. No aux lemmas
+2. No aux lemmas or matchers
3. No assigned mvars
-/
@[export pantograph_instantiate_all_m]
-def instantiateAll (e: Expr): MetaM Expr := do
+def instantiateAll (e : Expr) : MetaM Expr := do
let e ← instantiateDelayedMVars e
let e ← unfoldAuxLemmas e
- let e ← Core.transform e λ e' => do
- match ← Meta.matchMatcherApp? e' with
- | .none => return .continue e'
- | .some mapp =>
- let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist"
- let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList
- let mdata := KVMap.empty.insert `matcher (DataValue.ofName mapp.matcherName)
- return .visit $ .mdata mdata (f.betaRev e'.getAppRevArgs (useZeta := true))
+ let e ← unfoldMatchers e
return e
structure DelayedMVarInvocation where
- mvarIdPending: MVarId
- args: Array (FVarId × (Option Expr))
+ mvarIdPending : MVarId
+ args : Array (FVarId × (Option Expr))
-- Extra arguments applied to the result of this substitution
- tail: Array Expr
+ tail : Array Expr
-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
@[export pantograph_to_delayed_mvar_invocation_m]
From 678cc9b3c0d7dc759791b6934a4d8c0df859aa26 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 17 Mar 2025 11:30:24 -0700
Subject: [PATCH 7/8] chore: Code cleanup
---
Pantograph/Delate.lean | 19 +++++++++----------
1 file changed, 9 insertions(+), 10 deletions(-)
diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 3ef2c35..6e47799 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -37,7 +37,7 @@ def analyzeProjection (env: Environment) (e: Expr): Projection :=
def anonymousLevel : Level := .mvar ⟨.anonymous⟩
@[export pantograph_expr_proj_to_app]
-def exprProjToApp (env: Environment) (e: Expr): Expr :=
+def exprProjToApp (env : Environment) (e : Expr) : Expr :=
let anon : Expr := .mvar ⟨.anonymous⟩
match analyzeProjection env e with
| .field projector numParams =>
@@ -72,12 +72,12 @@ def unfoldAuxLemmas : Expr → CoreM Expr :=
/-- Unfold all matcher applications -/
@[export pantograph_unfold_matchers_m]
def unfoldMatchers (expr : Expr) : CoreM Expr :=
- Core.transform expr λ e' => do
- let .some mapp ← Meta.matchMatcherApp? e' | return .continue e'
+ Core.transform expr λ e => do
+ let .some mapp ← Meta.matchMatcherApp? e | return .continue e
let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist"
let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList
let mdata := KVMap.empty.insert `matcher (DataValue.ofName mapp.matcherName)
- return .visit $ .mdata mdata (f.betaRev e'.getAppRevArgs (useZeta := true))
+ return .visit $ .mdata mdata (f.betaRev e.getAppRevArgs (useZeta := true))
/--
Force the instantiation of delayed metavariables even if they cannot be fully
@@ -94,10 +94,9 @@ This function ensures any metavariable in the result is either
1. Delayed assigned with its pending mvar not assigned in any form
2. Not assigned (delay or not)
-/
-partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr :=
- --let padding := String.join $ List.replicate level "│ "
- withTraceNode `Pantograph.Delate (λ _ex => return m!":= {← Meta.ppExpr eOrig}") do
- let mut result ← Meta.transform (← instantiateMVars eOrig)
+partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
+ withTraceNode `Pantograph.Delate (λ _ex => return m!":= {← Meta.ppExpr expr}") do
+ let mut result ← Meta.transform (← instantiateMVars expr)
(pre := fun e => e.withApp fun f args => do
let .mvar mvarId := f | return .continue
trace[Pantograph.Delate] "V {e}"
@@ -127,7 +126,7 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr :=
trace[Pantograph.Delate]"MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
if args.size < fvars.size then
- throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
+ throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString expr}"
if !args.isEmpty then
trace[Pantograph.Delate] "─ Arguments Begin"
let args ← args.mapM self
@@ -139,7 +138,7 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr :=
return .done result
let pending ← mvarIdPending.withContext do
- let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
+ let inner ← instantiateDelayedMVars (.mvar mvarIdPending)
trace[Pantograph.Delate] "Pre: {inner}"
pure <| (← inner.abstractM fvars).instantiateRev args
From cb1082c7c7eea7d117fd17940a4f172278372280 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 17 Mar 2025 12:14:16 -0700
Subject: [PATCH 8/8] chore: More code cleanup
---
Pantograph/Delate.lean | 110 ++++++++++++++++++++---------------------
1 file changed, 55 insertions(+), 55 deletions(-)
diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 6e47799..efb1008 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -68,7 +68,7 @@ def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
@[export pantograph_unfold_aux_lemmas_m]
def unfoldAuxLemmas : Expr → CoreM Expr :=
- (Lean.Meta.deltaExpand · Lean.Name.isAuxLemma)
+ (Meta.deltaExpand · Lean.Name.isAuxLemma)
/-- Unfold all matcher applications -/
@[export pantograph_unfold_matchers_m]
def unfoldMatchers (expr : Expr) : CoreM Expr :=
@@ -97,66 +97,66 @@ This function ensures any metavariable in the result is either
partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
withTraceNode `Pantograph.Delate (λ _ex => return m!":= {← Meta.ppExpr expr}") do
let mut result ← Meta.transform (← instantiateMVars expr)
- (pre := fun e => e.withApp fun f args => do
- let .mvar mvarId := f | return .continue
- trace[Pantograph.Delate] "V {e}"
- let mvarDecl ← mvarId.getDecl
+ λ e => e.withApp fun f args => do
+ let .mvar mvarId := f | return .continue
+ trace[Pantograph.Delate] "V {e}"
+ let mvarDecl ← mvarId.getDecl
- -- This is critical to maintaining the interdependency of metavariables.
- -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
- -- system will not make the necessary delayed assigned mvars in case of
- -- nested mvars.
- mvarId.setKind .syntheticOpaque
+ -- This is critical to maintaining the interdependency of metavariables.
+ -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
+ -- system will not make the necessary delayed assigned mvars in case of
+ -- nested mvars.
+ mvarId.setKind .syntheticOpaque
- mvarId.withContext do
- let lctx ← MonadLCtx.getLCtx
- if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
- let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
- | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
- | .none => acc) []
- panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
+ mvarId.withContext do
+ let lctx ← MonadLCtx.getLCtx
+ if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
+ let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
+ | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
+ | .none => acc) []
+ panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
- if let .some assign ← getExprMVarAssignment? mvarId then
- trace[Pantograph.Delate] "A ?{mvarId.name}"
- assert! !(← mvarId.isDelayedAssigned)
- return .visit (mkAppN assign args)
- else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
- if ← isTracingEnabledFor `Pantograph.Delate then
- let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
- trace[Pantograph.Delate]"MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
+ if let .some assign ← getExprMVarAssignment? mvarId then
+ trace[Pantograph.Delate] "A ?{mvarId.name}"
+ assert! !(← mvarId.isDelayedAssigned)
+ return .visit (mkAppN assign args)
+ else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
+ if ← isTracingEnabledFor `Pantograph.Delate then
+ let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
+ trace[Pantograph.Delate]"MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
- if args.size < fvars.size then
- throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString expr}"
- if !args.isEmpty then
- trace[Pantograph.Delate] "─ Arguments Begin"
- let args ← args.mapM self
- if !args.isEmpty then
- trace[Pantograph.Delate] "─ Arguments End"
- if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
- trace[Pantograph.Delate] "T1"
- let result := mkAppN f args
- return .done result
-
- let pending ← mvarIdPending.withContext do
- let inner ← instantiateDelayedMVars (.mvar mvarIdPending)
- trace[Pantograph.Delate] "Pre: {inner}"
- pure <| (← inner.abstractM fvars).instantiateRev args
-
- -- Tail arguments
- let result := mkAppRange pending fvars.size args.size args
- trace[Pantograph.Delate] "MD {result}"
+ if args.size < fvars.size then
+ throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString expr}"
+ if !args.isEmpty then
+ trace[Pantograph.Delate] "─ Arguments Begin"
+ let args ← args.mapM self
+ if !args.isEmpty then
+ trace[Pantograph.Delate] "─ Arguments End"
+ if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
+ trace[Pantograph.Delate] "T1"
+ let result := mkAppN f args
return .done result
- else
- assert! !(← mvarId.isAssigned)
- assert! !(← mvarId.isDelayedAssigned)
- if !args.isEmpty then
- trace[Pantograph.Delate] "─ Arguments Begin"
- let args ← args.mapM self
- if !args.isEmpty then
- trace[Pantograph.Delate] "─ Arguments End"
- trace[Pantograph.Delate] "M ?{mvarId.name}"
- return .done (mkAppN f args))
+ let pending ← mvarIdPending.withContext do
+ let inner ← instantiateDelayedMVars (.mvar mvarIdPending)
+ trace[Pantograph.Delate] "Pre: {inner}"
+ pure <| (← inner.abstractM fvars).instantiateRev args
+
+ -- Tail arguments
+ let result := mkAppRange pending fvars.size args.size args
+ trace[Pantograph.Delate] "MD {result}"
+ return .done result
+ else
+ assert! !(← mvarId.isAssigned)
+ assert! !(← mvarId.isDelayedAssigned)
+ if !args.isEmpty then
+ trace[Pantograph.Delate] "─ Arguments Begin"
+ let args ← args.mapM self
+ if !args.isEmpty then
+ trace[Pantograph.Delate] "─ Arguments End"
+
+ trace[Pantograph.Delate] "M ?{mvarId.name}"
+ return .done (mkAppN f args)
trace[Pantoraph.Delate] "Result {result}"
return result
where