From 4d7b7dd8e66c366a2ba7bbc31a85cdf3e6ed15c8 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 27 Apr 2026 11:23:36 +0200 Subject: [PATCH] feat: support `while let` in `do` blocks via unified condition syntax (#13534) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR generalizes the `while` syntax in `do` blocks so that the condition can be any `doIfCond`, the same condition form already accepted by `if`. As a result, `while let pat := e do …` and `while let pat ← e do …` are now supported in addition to `while cond do …` and `while h : cond do …`. The previously separate `doWhile` and `doWhileH` parsers and their accompanying macros are unified into a single `doWhile` parser whose macro delegates to the existing `doIf` desugaring. --- src/Lean/Elab/BuiltinDo/Repeat.lean | 6 +-- src/Lean/Parser/Do.lean | 4 +- stage0/src/stdlib_flags.h | 1 + tests/elab/whileRepeat.lean | 68 +++++++++++++++++++++++++++++ 4 files changed, 71 insertions(+), 8 deletions(-) diff --git a/src/Lean/Elab/BuiltinDo/Repeat.lean b/src/Lean/Elab/BuiltinDo/Repeat.lean index e3714abaf5..1ab6907157 100644 --- a/src/Lean/Elab/BuiltinDo/Repeat.lean +++ b/src/Lean/Elab/BuiltinDo/Repeat.lean @@ -36,12 +36,8 @@ remove the following code without breaking the do block's type. 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) + | `(doElem| while%$tk $cond:doIfCond do $seq) => `(doElem| repeat%$tk if $cond:doIfCond then $seq else break) | _ => Macro.throwUnsupported @[builtin_macro Lean.Parser.Term.doRepeatUntil] def expandDoRepeatUntil : Macro diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 3e785f4ae9..6a18fc424b 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -275,10 +275,8 @@ with debug assertions enabled (see the `debugAssertions` option). @[builtin_doElem_parser] def doRepeat := leading_parser "repeat " >> doSeq -@[builtin_doElem_parser] def doWhileH := leading_parser - "while " >> ident >> " : " >> withForbidden "do" termParser >> " do " >> doSeq @[builtin_doElem_parser] def doWhile := leading_parser - "while " >> withForbidden "do" termParser >> " do " >> doSeq + "while " >> withForbidden "do" doIfCond >> " do " >> doSeq @[builtin_doElem_parser] def doRepeatUntil := leading_parser "repeat " >> doSeq >> ppDedent ppLine >> "until " >> termParser diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e444447049..a814500e6b 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -26,6 +26,7 @@ options get_default_options() { // Temporary, core-only flags for editing (i.e. must be part of stage0/bin/lean). Must be synced // with `LEAN_EXTRA_MAKE_OPTS` build flags in src/CMakeLists.txt. opts = opts.update({"backward", "do", "legacy"}, false); + // trigger stage0 update: unify `while` parser via `doIfCond` #endif return opts; } diff --git a/tests/elab/whileRepeat.lean b/tests/elab/whileRepeat.lean index bde2de6ada..91ab0c9d4b 100644 --- a/tests/elab/whileRepeat.lean +++ b/tests/elab/whileRepeat.lean @@ -48,3 +48,71 @@ test3 done 12 -/ #guard_msgs in #eval test3 + +-- `while let pat := e do ...` exits when the pattern fails to match. +def testWhileLet : IO Unit := do + let mut xs := [0, 1, 2, 3] + while let x :: rest := xs do + println! "{x}" + xs := rest + println! "done {xs.length}" + +/-- +info: 0 +1 +2 +3 +done 0 +-/ +#guard_msgs in +#eval testWhileLet + +-- `while let pat ← e do ...` evaluates the bind on each iteration. +def testWhileLetBind : IO Unit := do + let mut xs := [0, 1, 2, 3] + while let some x ← pure xs.head? do + println! "{x}" + xs := xs.tail + println! "done" + +/-- +info: 0 +1 +2 +3 +done +-/ +#guard_msgs in +#eval testWhileLetBind + +-- Pops entries from an `IO.Ref`-backed list to show that the bound expression +-- in `while let pat ← e do ...` is re-evaluated each iteration. +def testWhileLetBindRef : IO Unit := do + let r ← IO.mkRef [0, 1, 2, 3] + while let x :: rest ← r.get do + println! "{x}" + r.set rest + println! "done {(← r.get).length}" + +/-- +info: 0 +1 +2 +3 +done 0 +-/ +#guard_msgs in +#eval testWhileLetBindRef + +-- Unified `while` keeps supporting the `while h : cond do ...` form. +def testWhileH (xs : Array Nat) : Nat := Id.run do + let mut i := 0 + let mut sum := 0 + while h : i < xs.size do + sum := sum + xs[i] + i := i + 1 + return sum + +/-- info: 6 -/ +#guard_msgs in +#eval testWhileH #[1, 2, 3]