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

feat(goal): Add unshielded tactic execution mode #219

Merged
aniva merged 12 commits from goal/automatic-mode into dev 2025-06-26 15:52:17 -07:00
Conversation 0 Commits 12 Files Changed 14 +6 -7
1 changed files with 6 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 425825bf20 - Show all commits

13
Test/Tactic/Fragment.lean
View File

@ -110,6 +110,7 @@ def test_conv_simple: TestM Unit := do
return () return ()
addTest $ LSpec.check s!" · {convTactic}" ((← state1_1.serializeGoals).map (·.devolatilize) = addTest $ LSpec.check s!" · {convTactic}" ((← state1_1.serializeGoals).map (·.devolatilize) =
#[interiorGoal [] "b + a + c1 = b + a + c2"]) #[interiorGoal [] "b + a + c1 = b + a + c2"])
checkEq "(fragments)" state1_1.fragments.size 0
/- /-
let state1_1 ← match ← state6.fragmentExit goalConv with let state1_1 ← match ← state6.fragmentExit goalConv with
@ -171,7 +172,8 @@ def test_conv_unshielded : TestM Unit := do
interiorGoal [] "p", interiorGoal [] "p",
{ interiorGoal [] "p" with userName? := "right", }, { interiorGoal [] "p" with userName? := "right", },
] ]
checkEq " (n goals)" state.goals.length 2 checkEq "(n goals)" state.goals.length 2
checkEq "(fragments)" state.fragments.size 0
let tactic := "exact hp" let tactic := "exact hp"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed" let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
let tactic := "exact hp" let tactic := "exact hp"
@ -216,16 +218,12 @@ def test_conv_unfinished : TestM Unit := do
checkTrue " (fragment parent)" $ state.fragments.contains convParent checkTrue " (fragment parent)" $ state.fragments.contains convParent
checkTrue " (main goal)" state.mainGoal?.isSome checkTrue " (main goal)" state.mainGoal?.isSome
let tactic := "rfl" let tactic := "rfl"
let state? ← state.tryTactic .unfocus tactic let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
let state ← match state? with
| .success state _ => pure state
| .failure messages => fail s!"rfl {messages}"; return
| .invalidAction messages => fail s!"rfl {messages}"; return
| .parseError messages => fail s!"rfl {messages}"; return
checkEq s!" {tactic}" ((← state.serializeGoals).map (·.devolatilize)) checkEq s!" {tactic}" ((← state.serializeGoals).map (·.devolatilize))
#[ #[
interiorGoal [] "x + z = w", interiorGoal [] "x + z = w",
] ]
checkEq "(fragments)" state.fragments.size 0
checkEq s!" {tactic}" state.goals.length 1 checkEq s!" {tactic}" state.goals.length 1
let tactic := "exact hxzw" let tactic := "exact hxzw"
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed" let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
@ -295,6 +293,7 @@ def test_calc: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
checkEq "(fragments)" state4m.fragments.size 0
addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
where where
interiorGoal (free: List (String × String)) (target: String) := interiorGoal (free: List (String × String)) (target: String) :=