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

feat: Add support for the have, conv, and calc tactics #59

Merged
aniva merged 22 commits from goal/have-conv-calc into dev 2024-04-11 15:36:20 -07:00
Conversation 0 Commits 22 Files Changed 9 +10 -40
2 changed files with 10 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 73bdcb6be6 - Show all commits

38
Pantograph/Goal.lean
View File

@ -50,6 +50,8 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
newMVars := SSet.insert .empty root, newMVars := SSet.insert .empty root,
parentMVar := .none, parentMVar := .none,
} }
protected def GoalState.isConv (state: GoalState): Bool :=
state.convMVar.isSome
protected def GoalState.goals (state: GoalState): List MVarId := protected def GoalState.goals (state: GoalState): List MVarId :=
state.savedState.tactic.goals state.savedState.tactic.goals
protected def GoalState.mctx (state: GoalState): MetavarContext := protected def GoalState.mctx (state: GoalState): MetavarContext :=
@ -116,7 +118,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
goal.checkNotAssigned `GoalState.tryTactic goal.checkNotAssigned `GoalState.tryTactic
let tactic ← match Parser.runParserCategory let tactic ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv) (env := ← MonadEnv.getEnv)
(catName := `tactic) (catName := if state.isConv then `conv else `tactic)
(input := tactic) (input := tactic)
(fileName := filename) with (fileName := filename) with
| .ok stx => pure $ stx | .ok stx => pure $ stx
@ -284,39 +286,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
catch exception => catch exception =>
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
/-- Execute a tactic in conv mode -/ /-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTactic: String):
Elab.TermElabM TacticResult := do
let _ ← match state.convMVar with
| .some mvar => pure mvar
| .none => return .invalidAction "Not in conv state"
let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal
| .none => return .indexError goalId
let convTactic ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `conv)
(input := convTactic)
(fileName := filename) with
| .ok stx => pure $ stx
| .error error => return .parseError error
let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
state.restoreTacticM goal
Elab.Tactic.evalTactic convTactic
MonadBacktrack.saveState
try
let prevMCtx := state.mctx
let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
let nextMCtx := nextSavedState.term.meta.meta.mctx
return .success {
state with
savedState := nextSavedState
newMVars := newMVarSet prevMCtx nextMCtx,
parentMVar := .some goal,
}
catch exception =>
return .failure #[← exception.toMessageData.toString]
protected def GoalState.convExit (state: GoalState): protected def GoalState.convExit (state: GoalState):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
let (convRhs, convGoal, savedGoals) ← match state.convMVar with let (convRhs, convGoal, savedGoals) ← match state.convMVar with

12
Test/Proofs.lean
View File

@ -396,7 +396,7 @@ def test_conv: TestM Unit := do
#[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }]) #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
let convTactic := "rhs" let convTactic := "rhs"
let state3R ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with let state3R ← match ← state2.tryTactic (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -405,7 +405,7 @@ def test_conv: TestM Unit := do
#[{ interiorGoal [] "b + a + c2" with isConversion := true }]) #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
let convTactic := "lhs" let convTactic := "lhs"
let state3L ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with let state3L ← match ← state2.tryTactic (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -414,7 +414,7 @@ def test_conv: TestM Unit := do
#[{ interiorGoal [] "a + b + c1" with isConversion := true }]) #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
let convTactic := "congr" let convTactic := "congr"
let state4 ← match ← state3L.tryConvTactic (goalId := 0) (convTactic := convTactic) with let state4 ← match ← state3L.tryTactic (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -426,7 +426,7 @@ def test_conv: TestM Unit := do
]) ])
let convTactic := "rw [Nat.add_comm]" let convTactic := "rw [Nat.add_comm]"
let state5_1 ← match ← state4.tryConvTactic (goalId := 0) (convTactic := convTactic) with let state5_1 ← match ← state4.tryTactic (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -435,7 +435,7 @@ def test_conv: TestM Unit := do
#[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }]) #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
let convTactic := "rfl" let convTactic := "rfl"
let state6_1 ← match ← state5_1.tryConvTactic (goalId := 0) (convTactic := convTactic) with let state6_1 ← match ← state5_1.tryTactic (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -450,7 +450,7 @@ def test_conv: TestM Unit := do
return () return ()
let convTactic := "rfl" let convTactic := "rfl"
let state6 ← match ← state4_1.tryConvTactic (goalId := 0) (convTactic := convTactic) with let state6 ← match ← state4_1.tryTactic (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString