refactor: Use library goalStartExpr function

This commit is contained in:
Leni Aniva 2024-03-31 16:06:30 -07:00
parent 65ac0d5c58
commit 52d3283b5c
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 9 additions and 13 deletions

View File

@ -93,11 +93,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let state ← get
let env ← Lean.MonadEnv.getEnv
let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
| .some expr, .none => do
let expr ← match ← exprParse expr with
| .error e => return .error e
| .ok expr => pure $ expr
return .ok $ ← GoalState.create expr
| .some expr, .none => goalStartExpr expr
| .none, .some copyFrom =>
(match env.find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"

View File

@ -152,7 +152,7 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&
@[export pantograph_goal_start_expr_m]
def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
let termElabM: Lean.Elab.TermElabM _ := do
let expr ← match ← exprParse expr with
let expr ← match ← typeParse expr with
| .error e => return .error e
| .ok expr => pure $ expr
return .ok $ ← GoalState.create expr

View File

@ -73,22 +73,22 @@ def test_malformed_command : IO LSpec.TestSeq :=
]
def test_tactic : IO LSpec.TestSeq :=
let goal1: Protocol.Goal := {
name := "_uniq.10",
name := "_uniq.11",
target := { pp? := .some "∀ (q : Prop), x q → q x" },
vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
}
let goal2: Protocol.Goal := {
name := "_uniq.13",
name := "_uniq.14",
target := { pp? := .some "x y → y x" },
vars := #[
{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
],
}
subroutine_runner [
subroutine_step "goal.start"
[("expr", .str "∀ (p q: Prop), p q → q p")]
(Lean.toJson ({stateId := 0, root := "_uniq.8"}:
(Lean.toJson ({stateId := 0, root := "_uniq.9"}:
Protocol.GoalStartResult)),
subroutine_step "goal.tactic"
[("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
@ -100,7 +100,7 @@ def test_tactic : IO LSpec.TestSeq :=
subroutine_step "goal.print"
[("stateId", .num 1)]
(Lean.toJson ({
parent? := .some { pp? := .some "fun x => ?m.11 x" },
parent? := .some { pp? := .some "fun x => ?m.12 x" },
}:
Protocol.GoalPrintResult)),
subroutine_step "goal.tactic"