aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 14 Pull Requests 2 Packages Projects Releases Wiki Activity

Merge pull request 'fix(tactic): Erase finished calc goal' (#228) from fix/calc-erase-goal into dev 

Reviewed-on: #228
This commit is contained in:
Leni Aniva 2025-07-07 14:49:10 -07:00
parent aef8276c99 92befda2ff
commit 60dc07e559
2 changed files with 5 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Pantograph/Tactic/Fragment.lean
View File

@ -144,11 +144,12 @@ protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String) (
unless ← Meta.isDefEq proofType target do throwFailed unless ← Meta.isDefEq proofType target do throwFailed
remainder? := .some lastStepGoal.mvarId! remainder? := .some lastStepGoal.mvarId!
goal.assign proof goal.assign proof
let map := map.erase goal
let goals := [ mvarBranch ] ++ remainder?.toList let goals := [ mvarBranch ] ++ remainder?.toList
Elab.Tactic.setGoals goals Elab.Tactic.setGoals goals
match remainder? with match remainder? with
| .some goal => return map.erase goal |>.insert goal $ .calc (.some rhs) | .some goal => return map.insert goal $ .calc (.some rhs)
| .none => return map | .none => return map
| .conv .. => do | .conv .. => do
throwError "Direct operation on conversion tactic parent goal is not allowed" throwError "Direct operation on conversion tactic parent goal is not allowed"

5
Test/Tactic/Fragment.lean
View File

@ -126,8 +126,8 @@ def test_conv_simple: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check tactic ((← stateF.serializeGoals).map (·.devolatilize) = checkEq tactic ((← stateF.serializeGoals).map (·.devolatilize)) #[]
#[]) checkEq "fragments" stateF.fragments.size 0
where where
h := "b + a + c1 = b + a + c2" h := "b + a + c1 = b + a + c2"
@ -180,6 +180,7 @@ def test_conv_unshielded : TestM Unit := do
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed" let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
let root? := state.rootExpr? let root? := state.rootExpr?
checkTrue "root" root?.isSome checkTrue "root" root?.isSome
checkEq "fragments" state.fragments.size 0
where where
interiorGoal (free: List (String × String)) (target: String) := interiorGoal (free: List (String × String)) (target: String) :=
let free := [("p", "Prop"), ("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("hp", "p"), ("hi", "p → x = y")] ++ free let free := [("p", "Prop"), ("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("hp", "p"), ("hi", "p → x = y")] ++ free