feat: Bindings for the `have` tactic

This commit is contained in:
Leni Aniva 2024-04-06 16:40:22 -07:00
parent ace2ddf478
commit 951c2cec19
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
4 changed files with 24 additions and 7 deletions

View File

@ -114,12 +114,15 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => do
let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
| .some tactic, .none => do
let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr?, args.have? with
| .some tactic, .none, .none => do
pure ( Except.ok (← goalTactic goalState args.goalId tactic))
| .none, .some expr => do
pure ( Except.ok (← goalTryAssign goalState args.goalId expr))
| _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
| .none, .some expr, .none => do
pure ( Except.ok (← goalAssign goalState args.goalId expr))
| .none, .none, .some type => do
let binderName := args.binderName?.getD ""
pure ( Except.ok (← goalHave goalState args.goalId binderName type))
| _, _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr, have} must be supplied")
match nextGoalState? with
| .error error => return .error error
| .ok (.success nextGoalState) =>

View File

@ -1,3 +1,8 @@
/-
Functions for handling metavariables
All the functions starting with `try` resume their inner monadic state.
-/
import Pantograph.Protocol
import Lean

View File

@ -162,10 +162,14 @@ def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
runTermElabM <| GoalState.tryTactic state goalId tactic
@[export pantograph_goal_try_assign_m]
def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
@[export pantograph_goal_assign_m]
def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
runTermElabM <| GoalState.tryAssign state goalId expr
@[export pantograph_goal_have_m]
def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult :=
runTermElabM <| GoalState.tryHave state goalId binderName type
@[export pantograph_goal_continue]
def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
target.continue branch

View File

@ -201,6 +201,11 @@ structure GoalTactic where
-- One of the fields here must be filled
tactic?: Option String := .none
expr?: Option String := .none
have?: Option String := .none
-- In case of the `have` tactic, the new free variable name
binderName?: Option String := .none
deriving Lean.FromJson
structure GoalTacticResult where
-- The next goal state id. Existence of this field shows success