Add default arguments for Json

This commit is contained in:
Leni Aniva 2023-05-22 00:49:37 -07:00
parent 147079816d
commit 2772a394cc
3 changed files with 13 additions and 10 deletions

View File

@ -144,13 +144,13 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
| .error error => throw <| Lean.toJson <| errorIndex error
| .ok env => pure env
let tree := Meta.createProofTree
(name := args.name)
(name := args.name.getD "Untitled")
(env := env)
(coreContext := context.coreContext)
let expr: Lean.Expr ← match args.expr, args.copyFrom with
| "", "" =>
| .none, .none =>
throw <| Lean.toJson ({ error := "arguments", desc := "At least one of {expr, copyFrom} must be supplied" }: InteractionError)
| expr, "" =>
| .some expr, .none =>
let syn ← match Serial.syntax_from_str env expr with
| .error str => throw <| Lean.toJson ({ error := "parsing", desc := str }: InteractionError)
| .ok syn => pure syn
@ -158,7 +158,7 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
| .error str => throw <| Lean.toJson ({ error := "elab", desc := str }: InteractionError)
| .ok expr => pure expr
pure expr
| "", copyFrom =>
| .none, .some copyFrom =>
match Serial.expr_from_const env (name := str_to_name copyFrom) with
| .error str =>
IO.println "Symbol not found"
@ -180,7 +180,10 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
match state.proofTrees.get? args.treeId with
| .none => return Lean.toJson <| errorIndex "Invalid tree index {args.treeId}"
| .some tree =>
let (result, nextTree) ← Meta.ProofM.execute args.stateId args.goalId args.tactic |>.run tree
let (result, nextTree) ← Meta.ProofM.execute
(stateId := args.stateId)
(goalId := args.goalId.getD 0)
(tactic := args.tactic) |>.run tree
match result with
| .invalid message => return Lean.toJson <| errorIndex message
| .success nextId goals =>

View File

@ -50,10 +50,10 @@ structure InspectResult where
structure ProofStart where
id: Nat -- Environment id
name: String := "Untitled" -- Identifier of the proof
name: Option String -- Identifier of the proof
-- Only one of the fields below may be populated.
expr: String := "" -- Proof expression
copyFrom: String := "" -- Theorem name
expr: Option String -- Proof expression
copyFrom: Option String -- Theorem name
deriving Lean.FromJson
structure ProofStartResult where
error: String := ""
@ -63,7 +63,7 @@ structure ProofStartResult where
structure ProofTactic where
treeId: Nat
stateId: Nat
goalId: Nat := 0
goalId: Option Nat -- defaults to 0
tactic: String
deriving Lean.FromJson
structure ProofTacticResultSuccess where

View File

@ -48,7 +48,7 @@ Example proving a theorem: (alternatively use `proof.start {"id": 0, "name": "aa
```
$ lake env build/bin/Pantograph
create {"imports": ["Init"]}
proof.start {"id": 0, "name": "aa", "copyFrom": "", "expr": "∀ (n m : Nat), n + m = m + n"}
proof.start {"id": 0, "expr": "∀ (n m : Nat), n + m = m + n"}
proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro n m"}
proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"}
proof.printTree {"treeId": 0}