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

Merge pull request 'refactor: Use syntax tactic in unit test' (#207) from goal/tactic into dev 

Reviewed-on: #207
This commit is contained in:
Leni Aniva 2025-06-17 11:51:35 -07:00
parent ba84456f89 0bdb41635b
commit 86f69dd08c
3 changed files with 7 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Pantograph/Goal.lean
View File

@ -260,6 +260,7 @@ protected def GoalState.tryTacticM
(state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
(guardMVarErrors : Bool := false) (guardMVarErrors : Bool := false)
: Elab.TermElabM TacticResult := do : Elab.TermElabM TacticResult := do
assert! ¬ (← goal.isAssigned)
let prevMessageLength := state.coreState.messages.toList.length let prevMessageLength := state.coreState.messages.toList.length
try try
let nextState ← state.step goal tacticM guardMVarErrors let nextState ← state.step goal tacticM guardMVarErrors
@ -289,7 +290,6 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
(fileName := ← getFileName) with (fileName := ← getFileName) with
| .ok stx => pure $ stx | .ok stx => pure $ stx
| .error error => return .parseError error | .error error => return .parseError error
assert! ¬ (← goal.isAssigned)
state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true
protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String): protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):

2
Test/Common.lean
View File

@ -69,6 +69,8 @@ end Condensed
def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]! def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
def GoalState.tacticOn' (state: GoalState) (goalId: Nat) (tactic: TSyntax `tactic) :=
state.tryTacticM (state.get! goalId) (Elab.Tactic.evalTactic tactic) true
def TacticResult.toString : TacticResult → String def TacticResult.toString : TacticResult → String
| .success state _messages => s!".success ({state.goals.length} goals)" | .success state _messages => s!".success ({state.goals.length} goals)"

8
Test/Proofs.lean
View File

@ -66,15 +66,15 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
return a return a
def test_identity: TestM Unit := do def test_identity: TestM Unit := do
let state0 ← GoalState.create (expr := ← parseSentence "∀ (p: Prop), p → p") let rootTarget ← Elab.Term.elabTerm (← `(term|∀ (p: Prop), p → p)) .none
let tactic := "intro p h" let state0 ← GoalState.create (expr := rootTarget)
let state1 ← match ← state0.tacticOn 0 tactic with let state1 ← match ← state0.tacticOn' 0 (← `(tactic|intro p h)) with
| .success state _ => pure state | .success state _ => pure state
| other => do | other => do
fail other.toString fail other.toString
return () return ()
let inner := "_uniq.11" let inner := "_uniq.11"
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) = addTest $ LSpec.check "intro" ((← state1.serializeGoals (options := ← read)).map (·.name) =
#[inner]) #[inner])
let state1parent ← state1.withParentContext do let state1parent ← state1.withParentContext do
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)