Remove the obsolete name field from proof tree structure

This commit is contained in:
Leni Aniva 2023-08-23 13:19:38 -07:00 committed by Leni Aniva
parent 51edc701fe
commit 81702d12ef
4 changed files with 3 additions and 10 deletions

View File

@ -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 }

View File

@ -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

View File

@ -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!]

View File

@ -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)