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] 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