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

feat: Let tactic in REPL

This commit is contained in:
Leni Aniva 2024-10-12 16:17:21 -07:00
parent e0ba65a7cd
commit 645d9c9250
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 12 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Pantograph/Protocol.lean
View File

@ -219,6 +219,7 @@ structure GoalTactic where
tactic?: Option String := .none tactic?: Option String := .none
expr?: Option String := .none expr?: Option String := .none
have?: Option String := .none have?: Option String := .none
let?: Option String := .none
calc?: Option String := .none calc?: Option String := .none
-- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored. -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
conv?: Option Bool := .none conv?: Option Bool := .none

19
Repl.lean
View File

@ -124,21 +124,24 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let .some goal := goalState.goals.get? args.goalId | let .some goal := goalState.goals.get? args.goalId |
return .error $ errorIndex s!"Invalid goal index {args.goalId}" return .error $ errorIndex s!"Invalid goal index {args.goalId}"
let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv? with
| .some tactic, .none, .none, .none, .none => do | .some tactic, .none, .none, .none, .none, .none => do
pure <| Except.ok <| ← goalState.tryTactic goal tactic pure <| Except.ok <| ← goalState.tryTactic goal tactic
| .none, .some expr, .none, .none, .none => do | .none, .some expr, .none, .none, .none, .none => do
pure <| Except.ok <| ← goalState.tryAssign goal expr pure <| Except.ok <| ← goalState.tryAssign goal expr
| .none, .none, .some type, .none, .none => do | .none, .none, .some type, .none, .none, .none => do
let binderName := args.binderName?.getD "" let binderName := args.binderName?.getD ""
pure <| Except.ok <| ← goalState.tryHave goal binderName type pure <| Except.ok <| ← goalState.tryHave goal binderName type
| .none, .none, .none, .some pred, .none => do | .none, .none, .none, .some type, .none, .none => do
let binderName := args.binderName?.getD ""
pure <| Except.ok <| ← goalState.tryLet goal binderName type
| .none, .none, .none, .none, .some pred, .none => do
pure <| Except.ok <| ← goalState.tryCalc goal pred pure <| Except.ok <| ← goalState.tryCalc goal pred
| .none, .none, .none, .none, .some true => do | .none, .none, .none, .none, .none, .some true => do
pure <| Except.ok <| ← goalState.conv goal pure <| Except.ok <| ← goalState.conv goal
| .none, .none, .none, .none, .some false => do | .none, .none, .none, .none, .none, .some false => do
pure <| Except.ok <| ← goalState.convExit pure <| Except.ok <| ← goalState.convExit
| _, _, _, _, _ => | _, _, _, _, _, _ =>
let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied" let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
pure $ Except.error $ error pure $ Except.error $ error
match nextGoalState? with match nextGoalState? with