feat: Prograde tactics #83

Merged
aniva merged 24 commits from tactic/eval into dev 2024-08-31 20:04:39 -07:00
3 changed files with 59 additions and 12 deletions
Showing only changes of commit 6ddde2963d - Show all commits

View File

@ -488,12 +488,5 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: Strin
| .ok syn => pure syn
| .error error => return .parseError error
state.execute goalId (tacticM := Tactic.noConfuse eq)
protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Name) (expr: String) :
Elab.TermElabM TacticResult := do
state.restoreElabM
let expr ← match (← Compile.parseTermM expr) with
| .ok syn => pure syn
| .error error => return .parseError error
state.execute goalId (tacticM := Tactic.evaluate binderName expr)
end Pantograph

View File

@ -188,13 +188,13 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
state.restoreElabM
state.execute goalId (Tactic.«have» binderName.toName type)
@[export pantograph_goal_evaluate_m]
protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do
let type ← match (← Compile.parseTermM type) with
protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do
let expr ← match (← Compile.parseTermM expr) with
| .ok syn => pure syn
| .error error => return .parseError error
runTermElabM do
state.restoreElabM
state.execute goalId (Tactic.evaluate binderName.toName type)
state.execute goalId (Tactic.evaluate binderName.toName expr)
@[export pantograph_goal_let_m]
def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
runTermElabM <| state.tryLet goalId binderName type

View File

@ -50,7 +50,60 @@ def test_eval : TestT Elab.TermElabM Unit := do
})
addTest $ LSpec.test "assign" ((← getExprMVarAssignment? goal.mvarId!) == .some (.mvar newGoal))
def test_have : TestT Elab.TermElabM Unit := do
def test_proof_eval : TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
let state0 ← GoalState.create rootExpr
let tactic := "intro p q h"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p q) p q"])
let expr := "Or.inl (Or.inl h)"
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
#[])
let evalBind := "y"
let evalExpr := "Or.inl h"
let state2 ← match ← state1.tryEvaluate (goalId := 0) (binderName := evalBind) (expr := evalExpr) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!"eval {evalBind} := {evalExpr}" ((← state2.serializeGoals).map (·.devolatilize) =
#[{
target := { pp? := .some "(p q) p q"},
vars := #[
{ userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
{ userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
{ userName := "h", type? := .some { pp? := .some "p" }, isInaccessible? := .some false },
{ userName := "y",
type? := .some { pp? := .some "p ?m.25" },
value? := .some { pp? := .some "Or.inl h" },
isInaccessible? := .some false }
]
}])
let expr := "Or.inl y"
let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
#[])
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
def test_proof_have : TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
let state0 ← GoalState.create rootExpr
let tactic := "intro p q h"
@ -113,7 +166,8 @@ def test_have : TestT Elab.TermElabM Unit := do
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("eval", test_eval),
("have", test_have),
("Proof eval", test_proof_eval),
("Proof have", test_proof_have),
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
end Pantograph.Test.Tactic.Prograde