From 704df340cb4d42e6b56765e1d46ec1b96b5a675b Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 17 Apr 2026 17:19:59 +0200 Subject: [PATCH] feat: make `repeat` and `while` syntax builtin (#13442) This PR promotes the `repeat`, `while`, and `repeat ... until` parsers from `syntax` declarations in `Init.While` to `@[builtin_doElem_parser]` definitions in `Lean.Parser.Do`, alongside the other do-element parsers. The `while` variants and `repeat ... until` get `@[builtin_macro]` expansions; `repeat` itself gets a `@[builtin_doElem_elab]` so a follow-up can extend it with an option-driven choice between `Loop.mk` and a well-founded `Repeat.mk`. The new builtin parsers are registered at `low` priority so that the bootstrapping `syntax` declarations in `Init.While` (still needed for stage0 compatibility) take precedence during the transition. After the next stage0 update, the `Init.While` syntax and macros can be removed. --- src/Init/Data/Nat/Basic.lean | 8 ++++---- src/Lean/Elab/BuiltinDo/Repeat.lean | 23 +++++++++++++++++------ src/Lean/Elab/Do/Legacy.lean | 2 +- src/Lean/Parser/Do.lean | 12 ++++++++++++ stage0/src/stdlib_flags.h | 1 + 5 files changed, 35 insertions(+), 11 deletions(-) diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index bd28e4a437..0632ed9213 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -59,9 +59,9 @@ Examples: * `Nat.repeat f 3 a = f <| f <| f <| a` * `Nat.repeat (· ++ "!") 4 "Hello" = "Hello!!!!"` -/ -@[specialize, expose] def repeat {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α +@[specialize, expose] def «repeat» {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α | 0, a => a - | succ n, a => f (repeat f n a) + | succ n, a => f («repeat» f n a) /-- Applies a function to a starting value the specified number of times. @@ -1221,9 +1221,9 @@ theorem not_lt_eq (a b : Nat) : (¬ (a < b)) = (b ≤ a) := theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) := not_lt_eq b a -@[csimp] theorem repeat_eq_repeatTR : @repeat = @repeatTR := +@[csimp] theorem repeat_eq_repeatTR : @«repeat» = @repeatTR := funext fun α => funext fun f => funext fun n => funext fun init => - let rec go : ∀ m n, repeatTR.loop f m (repeat f n init) = repeat f (m + n) init + let rec go : ∀ m n, repeatTR.loop f m («repeat» f n init) = «repeat» f (m + n) init | 0, n => by simp [repeatTR.loop] | succ m, n => by rw [repeatTR.loop, succ_add]; exact go m (succ n) (go n 0).symm diff --git a/src/Lean/Elab/BuiltinDo/Repeat.lean b/src/Lean/Elab/BuiltinDo/Repeat.lean index b33a94a1c4..298177682d 100644 --- a/src/Lean/Elab/BuiltinDo/Repeat.lean +++ b/src/Lean/Elab/BuiltinDo/Repeat.lean @@ -17,17 +17,28 @@ namespace Lean.Elab.Do open Lean.Parser.Term /-- -Builtin do-element elaborator for `repeat` (syntax kind `Lean.doRepeat`). +Builtin do-element elaborator for `repeat` (syntax kind `Lean.Parser.Term.doRepeat`). -Expands to `for _ in Loop.mk do ...`. A follow-up PR will drop the fallback macro -in `Init.While` (which currently preempts this elaborator) and extend this +Expands to `for _ in Loop.mk do ...`. A follow-up change will extend this elaborator to choose between `Loop.mk` and a well-founded `Repeat.mk` based on a configuration option. -/ -@[builtin_doElem_elab Lean.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do - let `(doElem| repeat $seq) := stx | throwUnsupportedSyntax - let expanded ← `(doElem| for _ in Loop.mk do $seq) +@[builtin_doElem_elab Lean.Parser.Term.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do + let `(doElem| repeat%$tk $seq) := stx | throwUnsupportedSyntax + let expanded ← `(doElem| for%$tk _ in Loop.mk do $seq) Term.withMacroExpansion stx expanded <| withRef expanded <| elabDoElem ⟨expanded⟩ dec +@[builtin_macro Lean.Parser.Term.doWhileH] def expandDoWhileH : Macro + | `(doElem| while%$tk $h : $cond do $seq) => `(doElem| repeat%$tk if $h:ident : $cond then $seq else break) + | _ => Macro.throwUnsupported + +@[builtin_macro Lean.Parser.Term.doWhile] def expandDoWhile : Macro + | `(doElem| while%$tk $cond do $seq) => `(doElem| repeat%$tk if $cond then $seq else break) + | _ => Macro.throwUnsupported + +@[builtin_macro Lean.Parser.Term.doRepeatUntil] def expandDoRepeatUntil : Macro + | `(doElem| repeat%$tk $seq until $cond) => `(doElem| repeat%$tk do $seq:doSeq; if $cond then break) + | _ => Macro.throwUnsupported + end Lean.Elab.Do diff --git a/src/Lean/Elab/Do/Legacy.lean b/src/Lean/Elab/Do/Legacy.lean index c9a9cd282d..f9297cb30b 100644 --- a/src/Lean/Elab/Do/Legacy.lean +++ b/src/Lean/Elab/Do/Legacy.lean @@ -1782,7 +1782,7 @@ mutual doIfToCode doElem doElems else if k == ``Parser.Term.doUnless then doUnlessToCode doElem doElems - else if k == `Lean.doRepeat then + else if k == ``Parser.Term.doRepeat then let seq := doElem[1] let expanded ← `(doElem| for _ in Loop.mk do $seq) doSeqToCode (expanded :: doElems) diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index ee36e9a415..a498e3b420 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -273,6 +273,18 @@ with debug assertions enabled (see the `debugAssertions` option). @[builtin_doElem_parser] def doDebugAssert := leading_parser:leadPrec "debug_assert! " >> termParser +-- Lower priority than the bootstrapping `syntax` declarations in `Init.While` so that, during the +-- transition period where both exist, only the `Init.While` parser fires (no `choice` ambiguity). +-- After the next stage0 update, `Init.While` syntax will be removed and these become sole parsers. +@[builtin_doElem_parser low] def doRepeat := leading_parser + "repeat " >> doSeq +@[builtin_doElem_parser low] def doWhileH := leading_parser + "while " >> ident >> " : " >> withForbidden "do" termParser >> " do " >> doSeq +@[builtin_doElem_parser low] def doWhile := leading_parser + "while " >> withForbidden "do" termParser >> " do " >> doSeq +@[builtin_doElem_parser low] def doRepeatUntil := leading_parser + "repeat " >> doSeq >> ppDedent ppLine >> "until " >> termParser + /- We use `notFollowedBy` to avoid counterintuitive behavior. diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e444447049..adeb8df639 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,6 @@ #include "util/options.h" +// bump namespace lean { options get_default_options() { options opts;