From eb67654ae6d5fcdfd928743a4962a2e755775fd0 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 18 Jun 2024 14:36:59 +0200
Subject: [PATCH] feat: incremental `next` and tactic `if` (#4459)

---
 src/Init/Tactics.lean                          |  4 +++-
 src/Init/TacticsExtra.lean                     | 10 +++++++---
 .../interactive/incrementalCombinator.lean     | 18 ++++++++++++++++++
 .../incrementalCombinator.lean.expected.out    |  6 ++++++
 tests/lean/run/by_cases.lean                   | 11 +++++++++++
 5 files changed, 45 insertions(+), 4 deletions(-)

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 3eb891650f..1465d575ba 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -267,7 +267,9 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
 `next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
 inaccessible names to the given names.
 -/
-macro "next " args:binderIdent* " => " tac:tacticSeq : tactic => `(tactic| case _ $args* => $tac)
+macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
+  -- Limit ref variability for incrementality; see Note [Incremental Macros]
+  withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
 
 /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
 syntax (name := allGoals) "all_goals " tacticSeq : tactic
diff --git a/src/Init/TacticsExtra.lean b/src/Init/TacticsExtra.lean
index e298e28f9b..221bf99f3d 100644
--- a/src/Init/TacticsExtra.lean
+++ b/src/Init/TacticsExtra.lean
@@ -31,15 +31,19 @@ private def expandIfThenElse
       pure (hole, #[case])
   let (posHole, posCase) ← mkCase thenTk pos `(?pos)
   let (negHole, negCase) ← mkCase elseTk neg `(?neg)
-  `(tactic| (open Classical in refine%$ifTk $(← mkIf posHole negHole); $[$(posCase ++ negCase)]*))
+  `(tactic| ((open Classical in refine%$ifTk $(← mkIf posHole negHole)); $[$(posCase ++ negCase)]*))
 
 macro_rules
   | `(tactic| if%$tk $h : $c then%$ttk $pos else%$etk $neg) =>
-    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
+    -- Limit ref variability for incrementality; see Note [Incremental Macros]
+    withRef tk do
+      expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
 
 macro_rules
   | `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) =>
-    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
+    -- Limit ref variability for incrementality; see Note [Incremental Macros]
+    withRef tk do
+      expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
 
 /--
 `iterate n tac` runs `tac` exactly `n` times.
diff --git a/tests/lean/interactive/incrementalCombinator.lean b/tests/lean/interactive/incrementalCombinator.lean
index f5d6b83886..84222fc175 100644
--- a/tests/lean/interactive/incrementalCombinator.lean
+++ b/tests/lean/interactive/incrementalCombinator.lean
@@ -41,3 +41,21 @@ def spaceHave : True := by
               --^ insert: " "
               --^ collectDiagnostics
     dbg_trace "sh"
+
+-- RESET
+def next : True := by
+  next =>
+    dbg_trace "n 0"
+    dbg_trace "n 1"
+                --^ sync
+                --^ insert: ".5"
+
+-- RESET
+def if : True := by
+  if h : True then
+    dbg_trace "i 0"
+    dbg_trace "i 1"
+                --^ sync
+                --^ insert: ".5"
+  else
+    skip
diff --git a/tests/lean/interactive/incrementalCombinator.lean.expected.out b/tests/lean/interactive/incrementalCombinator.lean.expected.out
index 73cde7a18c..6430d5b1cd 100644
--- a/tests/lean/interactive/incrementalCombinator.lean.expected.out
+++ b/tests/lean/interactive/incrementalCombinator.lean.expected.out
@@ -54,3 +54,9 @@ sh
    "fullRange":
    {"start": {"line": 1, "character": 24},
     "end": {"line": 6, "character": 18}}}]}
+n 0
+n 1
+n 1.5
+i 0
+i 1
+i 1.5
diff --git a/tests/lean/run/by_cases.lean b/tests/lean/run/by_cases.lean
index e710925d93..3289c1a7ff 100644
--- a/tests/lean/run/by_cases.lean
+++ b/tests/lean/run/by_cases.lean
@@ -7,3 +7,14 @@ example : True := by
 example (p : Prop) : True := by
   if p then ?foo else trivial
   case foo => trivial
+
+/-! Should not accidentally leak `open Classical` into branches. -/
+
+/--
+error: failed to synthesize
+  Decidable p
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+example (p : Prop) : True := by
+  if p then exact decide p else trivial