From 2772a394cc1ab5333fc275359af1395c40493dcb Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 22 May 2023 00:49:37 -0700
Subject: [PATCH] Add default arguments for Json

---
 Main.lean                | 13 ++++++++-----
 Pantograph/Commands.lean |  8 ++++----
 README.md                |  2 +-
 3 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/Main.lean b/Main.lean
index 5fbb411..40bb875 100644
--- a/Main.lean
+++ b/Main.lean
@@ -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 =>
diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean
index 358b937..a4d6a8e 100644
--- a/Pantograph/Commands.lean
+++ b/Pantograph/Commands.lean
@@ -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
diff --git a/README.md b/README.md
index 3a11a34..b60886e 100644
--- a/README.md
+++ b/README.md
@@ -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}