From 4b02d733740056d644625500e299862bbac9c754 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 26 Jun 2025 11:37:14 -0700 Subject: [PATCH] fix: Tactic fragments inline with C/R paradigm --- Pantograph/Tactic/Fragment.lean | 45 ++++++++++++++----- Test/Common.lean | 2 - Test/Tactic/Fragment.lean | 78 ++++++++++++++++++++++++++++----- 3 files changed, 102 insertions(+), 23 deletions(-) diff --git a/Pantograph/Tactic/Fragment.lean b/Pantograph/Tactic/Fragment.lean index 2138801..132f023 100644 --- a/Pantograph/Tactic/Fragment.lean +++ b/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 _ => - return fragments.erase goal + | .convSentinel parent => + 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 - return newGoals.foldl (init := map) λ acc g => + -- Conclude the conv by exiting the parent fragment if new goals is empty + 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 diff --git a/Test/Common.lean b/Test/Common.lean index bbc8725..34ce07b 100644 --- a/Test/Common.lean +++ b/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)" diff --git a/Test/Tactic/Fragment.lean b/Test/Tactic/Fragment.lean index e4431c7..26b14b4 100644 --- a/Test/Tactic/Fragment.lean +++ b/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))