Pantograph/Goal.lean

@@ -50,6 +50,8 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
     newMVars := SSet.insert .empty root,
     parentMVar := .none,
   }
+protected def GoalState.isConv (state: GoalState): Bool :=
+  state.convMVar.isSome
 protected def GoalState.goals (state: GoalState): List MVarId :=
   state.savedState.tactic.goals
 protected def GoalState.mctx (state: GoalState): MetavarContext :=
@@ -116,7 +118,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
   goal.checkNotAssigned `GoalState.tryTactic
   let tactic ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
-    (catName := `tactic)
+    (catName := if state.isConv then `conv else `tactic)
     (input := tactic)
     (fileName := filename) with
     | .ok stx => pure $ stx
@@ -284,39 +286,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
-/-- Execute a tactic in conv mode -/
-protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTactic: String):
-      Elab.TermElabM TacticResult := do
-  let _ ← match state.convMVar with
-    | .some mvar => pure mvar
-    | .none => return .invalidAction "Not in conv state"
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  let convTactic ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `conv)
-    (input := convTactic)
-    (fileName := filename) with
-    | .ok stx => pure $ stx
-    | .error error => return .parseError error
-  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
-    state.restoreTacticM goal
-    Elab.Tactic.evalTactic convTactic
-    MonadBacktrack.saveState
-  try
-    let prevMCtx := state.mctx
-    let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-    let nextMCtx := nextSavedState.term.meta.meta.mctx
-    return .success {
-      state with
-      savedState := nextSavedState
-      newMVars := newMVarSet prevMCtx nextMCtx,
-      parentMVar := .some goal,
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
-
+/-- 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, savedGoals) ← match state.convMVar with

Test/Proofs.lean

@@ -396,7 +396,7 @@ def test_conv: TestM Unit := do
     #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
 
   let convTactic := "rhs"
-  let state3R ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with
+  let state3R ← match ← state2.tryTactic (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -405,7 +405,7 @@ def test_conv: TestM Unit := do
     #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
 
   let convTactic := "lhs"
-  let state3L ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with
+  let state3L ← match ← state2.tryTactic (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -414,7 +414,7 @@ def test_conv: TestM Unit := do
     #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
 
   let convTactic := "congr"
-  let state4 ← match ← state3L.tryConvTactic (goalId := 0) (convTactic := convTactic) with
+  let state4 ← match ← state3L.tryTactic (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -426,7 +426,7 @@ def test_conv: TestM Unit := do
     ])
 
   let convTactic := "rw [Nat.add_comm]"
-  let state5_1 ← match ← state4.tryConvTactic (goalId := 0) (convTactic := convTactic) with
+  let state5_1 ← match ← state4.tryTactic (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -435,7 +435,7 @@ def test_conv: TestM Unit := do
     #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
 
   let convTactic := "rfl"
-  let state6_1 ← match ← state5_1.tryConvTactic (goalId := 0) (convTactic := convTactic) with
+  let state6_1 ← match ← state5_1.tryTactic (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -450,7 +450,7 @@ def test_conv: TestM Unit := do
       return ()
 
   let convTactic := "rfl"
-  let state6 ← match ← state4_1.tryConvTactic (goalId := 0) (convTactic := convTactic) with
+  let state6 ← match ← state4_1.tryTactic (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString