Pantograph/Goal.lean

@@ -55,10 +55,13 @@ protected def GoalState.env (state: GoalState): Environment :=
   state.savedState.term.meta.core.env
 private def GoalState.mvars (state: GoalState): SSet MVarId :=
   state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
-private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
-  state.savedState.term.restore
 protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
   state.savedState.term.meta.restore
+private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
+  state.savedState.term.restore
+private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
+  state.savedState.restore
+  Elab.Tactic.setGoals [goal]
 
 /-- Inner function for executing tactic on goal state -/
 def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
@@ -246,6 +249,84 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
+/-- Enter conv tactic mode -/
+protected def GoalState.tryConv (state: GoalState) (goalId: Nat):
+      Elab.TermElabM TacticResult := do
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
+    state.restoreTacticM goal
+    --let mm ← Meta.matchEq? (← goal.getType)
+    --if let .some (_, _, rhs) := mm then
+    --  if rhs.getAppFn.isMVar then
+    --    IO.println "isMVar ok"
+    --  else
+    --    IO.println "isMVar failed"
+    --else
+    --  IO.println "matchEq? failed"
+    IO.println s!"Old goals: {(← Elab.Tactic.getGoals).map (λ x => x.name.toString)}"
+    --Elab.Tactic.Conv.remarkAsConvGoal
+    let goalNew ← Elab.Tactic.Conv.markAsConvGoal goal
+    -- TODO: Error if `goal == goalNew`
+    Elab.Tactic.setGoals [goalNew]
+    --Elab.Tactic.Conv.remarkAsConvGoal
+    IO.println s!"New goals: {(← Elab.Tactic.getGoals).map (λ x => x.name.toString)}"
+    MonadBacktrack.saveState
+  let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+  let prevMCtx := state.savedState.term.meta.meta.mctx
+  let nextMCtx := nextSavedState.term.meta.meta.mctx
+  -- Generate a list of mvarIds that exist in the parent state; Also test the
+  -- assertion that the types have not changed on any mvars.
+  let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
+    if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
+      assert! prevMVarDecl.type == mvarDecl.type
+      return acc
+    else
+      return acc.insert mvarId
+    ) SSet.empty
+  return .success {
+    root := state.root,
+    savedState := nextSavedState
+    newMVars,
+    parentMVar := .some goal,
+  }
+
+protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTactic: String):
+      Elab.TermElabM TacticResult := do
+  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.Conv.evalConvTactic convTactic
+    MonadBacktrack.saveState
+  let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+  let nextMCtx := nextSavedState.term.meta.meta.mctx
+  let prevMCtx := state.savedState.term.meta.meta.mctx
+  -- Generate a list of mvarIds that exist in the parent state; Also test the
+  -- assertion that the types have not changed on any mvars.
+  let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
+    if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
+      assert! prevMVarDecl.type == mvarDecl.type
+      return acc
+    else
+      return acc.insert mvarId
+    ) SSet.empty
+  return .success {
+    root := state.root,
+    savedState := nextSavedState
+    newMVars,
+    parentMVar := .some goal,
+  }
+
 
 /--
 Brings into scope a list of goals

Test/Proofs.lean

@@ -157,12 +157,13 @@ def test_arith: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intros") with
+  let tactic := "intros"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "intros" (state1.goals.length = 1)
+  addTest $ LSpec.check tactic (state1.goals.length = 1)
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
   let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
     | .success state => pure state
@@ -171,12 +172,13 @@ def test_arith: TestM Unit := do
       return ()
   addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
-  let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := "assumption") with
+  let tactic := "assumption"
+  let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.test "assumption" state3.goals.isEmpty
+  addTest $ LSpec.test tactic state3.goals.isEmpty
   addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
   return ()
 
@@ -385,14 +387,40 @@ def test_conv: TestM Unit := do
 
   -- This solves the state in one-shot
   let tactic := "conv => { lhs; congr; rw [Nat.add_comm]; rfl }"
-  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
+  let stateT ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+  addTest $ LSpec.check tactic ((← stateT.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[])
 
+  let state2 ← match ← state1.tryConv (goalId := 0) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c" with isConversion := true }])
+
+  let convTactic := "lhs"
+  let state3L ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c" with isConversion := true }])
+
+  let convTactic := "rhs"
+  let state3R ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "b + a + c" with isConversion := true }])
+
 example : ∀ (a: Nat), 1 + a + 1 = a + 2 := by
   intro a
   calc 1 + a + 1 = a + 1 + 1  := by conv =>