aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 15 Pull Requests 3 Packages Projects Releases Wiki Activity

feat(goal): Trace messages for replay

This commit is contained in:
Leni Aniva 2025-06-24 13:37:49 -07:00
parent 9d4b1ae755
commit 9b0d96f422
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
1 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Pantograph/Goal.lean
View File

@ -190,12 +190,15 @@ its assignment cannot change. -/
protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM GoalState := do protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM GoalState := do
let srcNGen := src.coreState.ngen let srcNGen := src.coreState.ngen
let srcNGen' := src'.coreState.ngen let srcNGen' := src'.coreState.ngen
let dstNGen := dst.coreState.ngen
assert! srcNGen.namePrefix == srcNGen'.namePrefix assert! srcNGen.namePrefix == srcNGen'.namePrefix
assert! srcNGen.namePrefix == dst.coreState.ngen.namePrefix assert! srcNGen.namePrefix == dstNGen.namePrefix
assert! src.mctx.depth == src'.mctx.depth assert! src.mctx.depth == src'.mctx.depth
assert! src.mctx.depth == dst.mctx.depth assert! src.mctx.depth == dst.mctx.depth
let diffNGenIdx := dst.coreState.ngen.idx - srcNGen.idx let diffNGenIdx := dst.coreState.ngen.idx - srcNGen.idx
trace[Pantograph.GoalState.replay] "Merging ngen {srcNGen.idx} -> ({srcNGen'.idx}, {dstNGen.idx})"
-- True if the name is generated after `src` -- True if the name is generated after `src`
let isNewName : Name → Bool let isNewName : Name → Bool
| .num pref n => | .num pref n =>
@ -231,6 +234,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
return ldecl return ldecl
let { term := savedTerm@{ meta := savedMeta@{ core, meta := meta@{ mctx, .. } }, .. }, .. } := dst.savedState let { term := savedTerm@{ meta := savedMeta@{ core, meta := meta@{ mctx, .. } }, .. }, .. } := dst.savedState
trace[Pantograph.GoalState.replay] "Merging mvars {src.mctx.mvarCounter} -> ({src'.mctx.mvarCounter}, {dst.mctx.mvarCounter})"
let mctx := { let mctx := {
mctx with mctx with
mvarCounter := mctx.mvarCounter + (src'.mctx.mvarCounter - src.mctx.mvarCounter), mvarCounter := mctx.mvarCounter + (src'.mctx.mvarCounter - src.mctx.mvarCounter),
@ -307,6 +311,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
continue continue
let .some l ← getLevelMVarAssignment? lmvarId | continue let .some l ← getLevelMVarAssignment? lmvarId | continue
let l' := mapLevel l' let l' := mapLevel l'
trace[Pantograph.GoalState.replay] "Merging level assignments on {lmvarId.name}"
unless ← Meta.isLevelDefEq l l' do unless ← Meta.isLevelDefEq l l' do
throwError "Conflicting assignment of level metavariable {lmvarId.name}" throwError "Conflicting assignment of level metavariable {lmvarId.name}"
for (mvarId, e') in src'.mctx.eAssignment do for (mvarId, e') in src'.mctx.eAssignment do
@ -316,6 +321,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
throwError "Conflicting assignment of expr metavariable (e != d) {mvarId.name}" throwError "Conflicting assignment of expr metavariable (e != d) {mvarId.name}"
let .some e ← getExprMVarAssignment? mvarId | continue let .some e ← getExprMVarAssignment? mvarId | continue
let e' ← mapExpr e' let e' ← mapExpr e'
trace[Pantograph.GoalState.replay] "Merging expr assignments on {mvarId.name}"
unless ← Meta.isDefEq e e' do unless ← Meta.isDefEq e e' do
throwError "Conflicting assignment of expr metavariable (e != e) {mvarId.name}" throwError "Conflicting assignment of expr metavariable (e != e) {mvarId.name}"
for (mvarId, d') in src'.mctx.dAssignment do for (mvarId, d') in src'.mctx.dAssignment do
@ -324,6 +330,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
if ← mvarId.isAssigned then if ← mvarId.isAssigned then
throwError "Conflicting assignment of expr metavariable (d != e) {mvarId.name}" throwError "Conflicting assignment of expr metavariable (d != e) {mvarId.name}"
let .some d ← getDelayedMVarAssignment? mvarId | continue let .some d ← getDelayedMVarAssignment? mvarId | continue
trace[Pantograph.GoalState.replay] "Merging expr (delayed) assignments on {mvarId.name}"
unless d == d' do unless d == d' do
throwError "Conflicting assignment of expr metavariable (d != d) {mvarId.name}" throwError "Conflicting assignment of expr metavariable (d != d) {mvarId.name}"
@ -544,4 +551,7 @@ protected def GoalState.tryCalc (state : GoalState) (goal : MVarId) (pred : Stri
fragments, fragments,
} }
initialize
registerTraceClass `Pantograph.GoalState.replay
end Pantograph end Pantograph