From 37473b3efbec7be8e103b93ff343ad46dd0f4a35 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 6 Sep 2024 21:30:11 -0700
Subject: [PATCH] feat: Automatic mode (auto resume)

---
 Pantograph.lean      | 13 ++++++++++++-
 Pantograph/Goal.lean | 24 ++++++++++++++++++++----
 2 files changed, 32 insertions(+), 5 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index 7cedab8..004c63f 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -20,6 +20,7 @@ structure State where
 
 /-- Main state monad for executing commands -/
 abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
+
 -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
 -- certain monadic features in `MainM`
 abbrev CR α := Except Protocol.InteractionError α
@@ -145,7 +146,17 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         pure $ Except.error $ error
     match nextGoalState? with
     | .error error => return .error error
-    | .ok (.success nextGoalState) =>
+    | .ok (.success nextGoalState) => do
+      let nextGoalState ← match state.options.automaticMode, args.conv? with
+        | true, .none => do
+          let .ok result := nextGoalState.resume goalState.goals | throwError "Resuming known goals"
+          pure result
+        | true, .some true => pure nextGoalState
+        | true, .some false => do
+          let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail"
+          let .ok result := nextGoalState.resume dormantGoals | throwError "Resuming known goals"
+          pure result
+        | false, _ => pure nextGoalState
       let nextStateId := state.nextId
       set { state with
         goalStates := state.goalStates.insert state.nextId nextGoalState,
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 0df3a4b..7486103 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -27,7 +27,8 @@ structure GoalState where
   parentMVar?: Option MVarId
 
   -- Existence of this field shows that we are currently in `conv` mode.
-  convMVar?: Option (MVarId × MVarId) := .none
+  -- (convRhs, goal, dormant)
+  convMVar?: Option (MVarId × MVarId × List MVarId) := .none
   -- Previous RHS for calc, so we don't have to repeat it every time
   -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
   calcPrevRhs?: Option (MVarId × Expr) := .none
@@ -97,6 +98,20 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
     calcPrevRhs? := .none,
   }
 
+/-- Immediately bring all parent goals back into scope. Used in automatic mode -/
+@[export pantograph_goal_state_immediate_resume_parent]
+protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
+  -- Prune parents solved goals
+  let mctx := state.mctx
+  let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
+  {
+    state with
+    savedState := {
+      state.savedState with
+      tactic := { goals := state.goals ++ parentGoals },
+    },
+  }
+
 /--
 Brings into scope a list of goals
 -/
@@ -116,7 +131,6 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
         term := state.savedState.term,
         tactic := { goals := unassigned },
       },
-      calcPrevRhs? := .none,
     }
 /--
 Brings into scope all goals from `branch`
@@ -244,11 +258,13 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId):
     return (← MonadBacktrack.saveState, convMVar)
   try
     let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+    -- Other goals are now dormant
+    let otherGoals := state.goals.filter $ λ g => g != goal
     return .success {
       root := state.root,
       savedState := nextSavedState
       parentMVar? := .some goal,
-      convMVar? := .some (convRhs, goal),
+      convMVar? := .some (convRhs, goal, otherGoals),
       calcPrevRhs? := .none
     }
   catch exception =>
@@ -257,7 +273,7 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId):
 /-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
 protected def GoalState.convExit (state: GoalState):
       Elab.TermElabM TacticResult := do
-  let (convRhs, convGoal) ← match state.convMVar? with
+  let (convRhs, convGoal, _) ← match state.convMVar? with
     | .some mvar => pure mvar
     | .none => return .invalidAction "Not in conv state"
   let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do