Pantograph/Tactic/Fragment.lean

@@ -4,6 +4,13 @@ Here, a unified system handles all fragments.
 
 Inside a tactic fragment, the parser category may be different. An incomplete
 fragmented tactic may not be elaboratable..
+
+In line with continuation/resumption paradigms, the exit function of a fragment
+tactic is responsible for resuming incomplete goals with fragments. For example,
+when a conversion tactic finishes, the sentinels should resume the root of the
+conversion tactic goal. The user cannot be expected to execute this resumption,
+since the root is automatically dormanted at the entry of the conversion tactic
+mode.
 -/
 import Lean.Meta
 import Lean.Elab
@@ -17,7 +24,7 @@ inductive Fragment where
   | conv (rhs : MVarId)
   -- This goal is spawned from a `conv`
   | convSentinel (parent : MVarId)
-  deriving BEq
+  deriving BEq, Inhabited
 abbrev FragmentMap := Std.HashMap MVarId Fragment
 def FragmentMap.empty : FragmentMap := Std.HashMap.emptyWithCapacity 2
 
@@ -45,7 +52,7 @@ protected def Fragment.enterConv : Elab.Tactic.TacticM FragmentMap := do
     |>.insert goal (.conv rhs)
     |>.insert newGoal (.convSentinel goal)
 
-protected def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : FragmentMap)
+protected partial def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : FragmentMap)
   : Elab.Tactic.TacticM FragmentMap :=
   match fragment with
   | .calc .. => do
@@ -59,18 +66,25 @@ protected def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : F
     -- Close all existing goals with `refl`
     for mvarId in goals do
       liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
-    Elab.Tactic.pruneSolvedGoals
     unless (← goals.filterM (·.isAssignedOrDelayedAssigned)).isEmpty do
       throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (goals)}"
 
-    Elab.Tactic.replaceMainGoal [goal]
+    -- Ensure the meta tactic runs on `goal` even if its dormant by forcing resumption
+    Elab.Tactic.setGoals $ goal :: (← Elab.Tactic.getGoals)
     let targetNew ← instantiateMVars (.mvar rhs)
     let proof ← instantiateMVars (.mvar goal)
 
     Elab.Tactic.liftMetaTactic1 (·.replaceTargetEq targetNew proof)
+
+    -- Try to solve maiinline by rfl
+    let mvarId ← Elab.Tactic.getMainGoal
+    liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
+    Elab.Tactic.pruneSolvedGoals
+    -- FIXME: Erase all sibling fragments
     return fragments.erase goal
-  | .convSentinel _ =>
+  | .convSentinel parent =>
-    return fragments.erase goal
+    let parentFragment := fragments[parent]!
+    parentFragment.exit parent (fragments.erase goal)
 
 protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String) (map : FragmentMap)
   : Elab.Tactic.TacticM FragmentMap := goal.withContext do
@@ -143,14 +157,25 @@ protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String) (
     let oldGoals ← Elab.Tactic.getGoals
     -- Label newly generated goals as conv sentinels
     Elab.Tactic.evalTactic tactic
-    let newGoals ← (← Elab.Tactic.getUnsolvedGoals).filterM λ g => do
+    let newConvGoals ← (← Elab.Tactic.getUnsolvedGoals).filterM λ g => do
       -- conv tactic might generate non-conv goals
       if oldGoals.contains g then
         return false
-      let target ← g.getType
       return isLHSGoal? (← g.getType) |>.isSome
-    -- FIXME: Conclude the conv by exiting the parent fragment if new goals is empty
+    -- Conclude the conv by exiting the parent fragment if new goals is empty
-    return newGoals.foldl (init := map) λ acc g =>
+    if newConvGoals.isEmpty then
+      let hasSiblingFragment := map.fold (init := false) λ flag _ fragment =>
+        if flag then
+          true
+        else match fragment with
+          | .convSentinel parent' => parent == parent'
+          | _ => false
+      if ¬ hasSiblingFragment then
+        -- This fragment must exist since we have conv goals
+        let parentFragment := map[parent]!
+        -- All descendants exhausted. Exit from the parent conv.
+        return ← parentFragment.exit parent map
+    return newConvGoals.foldl (init := map) λ acc g =>
       acc.insert g fragment
 
 end Pantograph

Test/Common.lean

@@ -71,8 +71,6 @@ def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
 def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
 def GoalState.tacticOn' (state: GoalState) (goalId: Nat) (tactic: TSyntax `tactic) :=
   state.tryTacticM (state.get! goalId) (Elab.Tactic.evalTactic tactic) true
-def GoalState.tryTacticOnMain (state : GoalState) (tactic : String) :=
-  state.tryTactic (.prefer state.goals[0]!) tactic
 
 def TacticResult.toString : TacticResult → String
   | .success state _messages => s!".success ({state.goals.length} goals)"

Test/Tactic/Fragment.lean

@@ -26,7 +26,7 @@ example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (
     . rfl
   exact h
 
-def test_conv: TestM Unit := do
+def test_conv_simple: TestM Unit := do
   let rootTarget ← parseSentence "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2"
   let state0 ← GoalState.create rootTarget
 
@@ -103,19 +103,21 @@ def test_conv: TestM Unit := do
       return ()
 
   let convTactic := "rfl"
-  let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
+  let state1_1 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
     | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check s!"  · {convTactic}" ((← state6.serializeGoals).map (·.devolatilize) =
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state1_1.serializeGoals).map (·.devolatilize) =
-    #[])
+    #[interiorGoal [] "b + a + c1 = b + a + c2"])
 
+  /-
   let state1_1 ← match ← state6.fragmentExit goalConv with
     | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
+  -/
 
   let tactic := "exact h"
   let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
@@ -151,19 +153,19 @@ def test_conv_unshielded : TestM Unit := do
   let tactic := "apply And.intro"
   let .success state _ ← state.tacticOn 0 tactic | fail "apply failed"
   let .success state _ ← state.convEnter (.prefer state.goals[0]!) | fail "Cannot enter conversion tactic mode"
-  let .success state _ ← state.tryTacticOnMain "rhs" | fail "rhs failed"
+  let .success state _ ← state.tryTactic .unfocus "rhs" | fail "rhs failed"
   let tactic := "arg 1"
-  let .success state _ ← state.tryTacticOnMain tactic | fail s!"{tactic} failed"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
   checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
     #[
       { interiorGoal [] "y" with isConversion := true },
       { interiorGoal [] "p" with userName? := "right", },
     ]
   let tactic := "rw [←hi]"
-  let .success state _ ← state.tryTacticOnMain tactic | fail s!"{tactic} failed"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
   checkEq s!"  {tactic}" state.goals.length 3
   let tactic := "rfl"
-  let .success state _ ← state.tryTacticOnMain tactic | fail s!"{tactic} failed"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
   checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
     #[
       interiorGoal [] "p",
@@ -171,9 +173,9 @@ def test_conv_unshielded : TestM Unit := do
     ]
   checkEq "  (n goals)" state.goals.length 2
   let tactic := "exact hp"
-  let .success state _ ← state.tryTacticOnMain tactic | fail s!"{tactic} failed"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
   let tactic := "exact hp"
-  let .success state _ ← state.tryTacticOnMain tactic | fail s!"{tactic} failed"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
   let root? := state.rootExpr?
   checkTrue "root" root?.isSome
   where
@@ -181,6 +183,59 @@ def test_conv_unshielded : TestM Unit := do
     let free := [("p", "Prop"), ("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("hp", "p"), ("hi", "p → x = y")] ++ free
     buildGoal free target
 
+example : ∀ (x y z w : Nat), y = z → x + z = w → x + y = w := by
+  intro x y z w hyz hxzw
+  conv =>
+    lhs
+    arg 2
+    rw [hyz]
+    rfl
+  exact hxzw
+
+def test_conv_unfinished : TestM Unit := do
+  let rootTarget ← parseSentence "∀ (x y z w : Nat), y = z → x + z = w → x + y = w"
+  let state ← GoalState.create rootTarget
+  let tactic := "intro x y z w hyz hxzw"
+  let .success state _ ← state.tacticOn 0 tactic | fail "intro failed"
+  let convParent := state.goals[0]!
+  let .success state _ ← state.convEnter (.prefer convParent) | fail "Cannot enter conversion tactic mode"
+  let .success state _ ← state.tryTactic .unfocus "lhs" | fail "rhs failed"
+  let tactic := "arg 2"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      { interiorGoal [] "y" with isConversion := true },
+    ]
+  let tactic := "rw [hyz]"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      { interiorGoal [] "z" with isConversion := true },
+    ]
+  checkTrue "  (fragment)" $ state.fragments.contains state.mainGoal?.get!
+  checkTrue "  (fragment parent)" $ state.fragments.contains convParent
+  checkTrue "  (main goal)" state.mainGoal?.isSome
+  let tactic := "rfl"
+  let state? ← state.tryTactic .unfocus tactic
+  let state ← match state? with
+    | .success state _ => pure state
+    | .failure messages => fail s!"rfl {messages}"; return
+    | .invalidAction messages => fail s!"rfl {messages}"; return
+    | .parseError messages => fail s!"rfl {messages}"; return
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      interiorGoal [] "x + z = w",
+    ]
+  checkEq s!"  {tactic}" state.goals.length 1
+  let tactic := "exact hxzw"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  let root? := state.rootExpr?
+  checkTrue "root" root?.isSome
+  where
+  interiorGoal (free: List (String × String)) (target: String) :=
+    let free := [("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("w", "Nat"), ("hyz", "y = z"), ("hxzw", "x + z = w")] ++ free
+    buildGoal free target
+
 example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
   intro a b c d h1 h2
   calc a + b = b + c := by apply h1
@@ -249,8 +304,9 @@ def test_calc: TestM Unit := do
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("conv", test_conv),
+    ("conv simple", test_conv_simple),
     ("conv unshielded", test_conv_unshielded),
+    ("conv unfinished", test_conv_unfinished),
     ("calc", test_calc),
   ] |>.map (λ (name, t) => (name, runTestTermElabM env t))