From 81702d12ef671c119aa6b45d184ac6a1944d30a5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 23 Aug 2023 13:19:38 -0700
Subject: [PATCH] Remove the obsolete name field from proof tree structure

---
 Pantograph.lean          | 2 +-
 Pantograph/Commands.lean | 3 +--
 Pantograph/Tactic.lean   | 6 +-----
 Test/Proofs.lean         | 2 --
 4 files changed, 3 insertions(+), 10 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index 18ead6b..525b834 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -134,7 +134,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
     match expr? with
     | .error error => return .error error
     | .ok expr =>
-      let tree ← ProofTree.create (str_to_name <| args.name.getD "Untitled") expr
+      let tree ← ProofTree.create expr
       -- Put the new tree in the environment
       let nextTreeId := state.proofTrees.size
       set { state with proofTrees := state.proofTrees.push tree }
diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean
index 8d17b0e..6e28af8 100644
--- a/Pantograph/Commands.lean
+++ b/Pantograph/Commands.lean
@@ -128,7 +128,6 @@ structure OptionsPrint where
 abbrev OptionsPrintResult := Options
 
 structure ProofStart where
-  name: Option String     -- Identifier of the proof
   -- Only one of the fields below may be populated.
   expr: Option String     -- Proof expression
   copyFrom: Option String -- Theorem name
@@ -140,7 +139,7 @@ structure ProofTactic where
   -- Identifiers for tree, state, and goal
   treeId: Nat
   stateId: Nat
-  goalId: Option Nat
+  goalId: Option Nat -- Defaults to 0
   tactic: String
   deriving Lean.FromJson
 structure ProofTacticResult where
diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean
index f661be5..50ddf3a 100644
--- a/Pantograph/Tactic.lean
+++ b/Pantograph/Tactic.lean
@@ -30,21 +30,17 @@ structure ProofState where
   parent : Option Nat := none
   parentGoalId : Nat  := 0
 structure ProofTree where
-  -- All parameters needed to run a `TermElabM` monad
-  name: Name
-
   -- Set of proof states
   states : Array ProofState := #[]
 
 abbrev M := Elab.TermElabM
 
-def ProofTree.create (name: Name) (expr: Expr): M ProofTree := do
+def ProofTree.create (expr: Expr): M ProofTree := do
   let expr ← instantiateMVars expr
   let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic))
   let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
   let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
   return {
-    name := name,
     states := #[{
       savedState := savedState,
       goals := [goal.mvarId!]
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 52a2c69..505eec9 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -22,7 +22,6 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
     match cInfo? with
     | .some cInfo =>
       let state ← ProofTree.create
-        (name := str_to_name "TestExample")
         (expr := cInfo.type)
       return (testSeq, Option.some state)
     | .none =>
@@ -43,7 +42,6 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
         return (testSeq, Option.none)
       | .ok expr =>
         let state ← ProofTree.create
-          (name := str_to_name "TestExample")
           (expr := expr)
         return (testSeq, Option.some state)