Add WellFoundedStreams module from batteries PR#1331

Parser/Basic.lean

@@ -129,13 +129,21 @@ def test (p : ParserT ε σ τ m α) : ParserT ε σ τ m Bool :=
 
 /-- `foldr f p q` -/
 @[inline]
-partial def foldr (f : α → β → β) (p : ParserT ε σ τ m α) (q : ParserT ε σ τ m β) :
-  ParserT ε σ τ m β :=
-  try
-    let x ← withBacktracking p
-    let y ← foldr f p q
-    return f x y
-  catch _ => q
+def foldr (f : α → β → β) (p : ParserT ε σ τ m α) (q : ParserT ε σ τ m β) :
+  ParserT ε σ τ m β := fun s => foldrAux s
+where
+  foldrAux (s : σ) : m (Parser.Result ε σ β) :=
+    let savePos := Stream.getPosition s
+    p s >>= fun
+    | .ok s' x =>
+      if _h : Stream.remaining s' < Stream.remaining s then
+        foldrAux s' >>= fun
+        | .ok s'' y => return .ok s'' (f x y)
+        | .error s'' e => return .error s'' e
+      else
+        q (Stream.setPosition s' savePos)
+    | .error s' _ => q (Stream.setPosition s' savePos)
+  termination_by Stream.remaining s
 
 /-! ### `take` family -/
 
@@ -194,15 +202,25 @@ def takeManyN (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array
 array of returned values of `p` and the output of `stop`. If `p` fails before `stop` is encountered,
 the error from `p` is reported and no input is consumed.
 -/
-partial def takeUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) :
+def takeUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) :
   ParserT ε σ τ m (Array α × β) :=
   have := Inhabited.mk do return ((#[] : Array α), (← stop))
-  withBacktracking do rest #[]
+  withBacktracking fun s => rest #[] s
 where
-  rest [Inhabited (ParserT ε σ τ m (Array α × β))] (acc : Array α) := do
-    match ← option? stop with
-    | some y => return (acc, y)
-    | none => rest <| acc.push (← p)
+  rest [Inhabited (ParserT ε σ τ m (Array α × β))] (acc : Array α) (s : σ) :
+      m (Parser.Result ε σ (Array α × β)) :=
+    (option? stop) s >>= fun
+    | .ok s' (some y) => return .ok s' (acc, y)
+    | .ok s' none =>
+      p s' >>= fun
+      | .ok s'' x =>
+        if _h : Stream.remaining s'' < Stream.remaining s then
+          rest (acc.push x) s''
+        else
+          return .error s'' (Error.unexpected (Stream.getPosition s'') none)
+      | .error s'' e => return .error s'' e
+    | .error s' e => return .error s' e
+  termination_by Stream.remaining s
 
 /-! ### `drop` family -/
 
@@ -256,13 +274,22 @@ def dropManyN (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit :
 outputs from `p`. If `p` fails before encountering `stop` then the error from  `p` is reported
 and no input is consumed.
 -/
-partial def dropUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m β :=
-  withBacktracking loop
+def dropUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) : ParserT ε σ τ m β :=
+  withBacktracking fun s => loop s
 where
-  loop := do
-    match ← option? stop with
-    | some s => return s
-    | none => p *> loop
+  loop (s : σ) : m (Parser.Result ε σ β) :=
+    (option? stop) s >>= fun
+    | .ok s' (some v) => return .ok s' v
+    | .ok s' none =>
+      p s' >>= fun
+      | .ok s'' _ =>
+        if _h : Stream.remaining s'' < Stream.remaining s then
+          loop s''
+        else
+          return .error s'' (Error.unexpected (Stream.getPosition s'') none)
+      | .error s'' e => return .error s'' e
+    | .error s' e => return .error s' e
+  termination_by Stream.remaining s
 
 /-! `count` family -/
 
@@ -271,7 +298,7 @@ where
 successes.
 -/
 @[inline]
-partial def count (p : ParserT ε σ τ m α) : ParserT ε σ τ m Nat :=
+def count (p : ParserT ε σ τ m α) : ParserT ε σ τ m Nat :=
   foldl (fun n _ => n+1) 0 p
 
 /--
@@ -294,15 +321,25 @@ where
 the count of successes and the output of `stop`. If `p` fails before encountering `stop` then the
 error from  `p` is reported and no input is consumed.
 -/
-partial def countUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) :
+def countUntil (stop : ParserT ε σ τ m β) (p : ParserT ε σ τ m α) :
   ParserT ε σ τ m (Nat × β) := do
   let _ := Inhabited.mk do return (0, ← stop)
-  withBacktracking do loop 0
+  withBacktracking fun s => loop 0 s
 where
-  loop [Inhabited (ParserT ε σ τ m (Nat × β))] (ct : Nat) := do
-    match ← option? stop with
-    | some s => return (ct, s)
-    | none => p *> loop (ct+1)
+  loop [Inhabited (ParserT ε σ τ m (Nat × β))] (ct : Nat) (s : σ) :
+      m (Parser.Result ε σ (Nat × β)) :=
+    (option? stop) s >>= fun
+    | .ok s' (some v) => return .ok s' (ct, v)
+    | .ok s' none =>
+      p s' >>= fun
+      | .ok s'' _ =>
+        if _h : Stream.remaining s'' < Stream.remaining s then
+          loop (ct+1) s''
+        else
+          return .error s'' (Error.unexpected (Stream.getPosition s'') none)
+      | .error s'' e => return .error s'' e
+    | .error s' e => return .error s' e
+  termination_by Stream.remaining s
 
 /-! ### `endBy` family -/
 

Parser/Parser.lean

@@ -186,15 +186,20 @@ def withErrorMessage (msg : String) (p : ParserT ε σ τ m α) : ParserT ε σ
 /-! ### `foldl` family -/
 
 @[specialize]
-private partial def efoldlPAux [Inhabited ε] [Inhabited σ] [Inhabited β]
+private def efoldlPAux [Inhabited ε] [Inhabited σ] [Inhabited β]
   (f : β → α → ParserT ε σ τ m β) (p : ParserT ε σ τ m α) (y : β) (s : σ) :
   m (Parser.Result ε σ (β × ε × Bool)) :=
   let savePos := Stream.getPosition s
   p s >>= fun
-    | .ok s x => f y x s >>= fun
-      | .ok s y => efoldlPAux f p y s
-      | .error s e => return .ok (Stream.setPosition s savePos) (y, e, true)
-    | .error s e => return .ok (Stream.setPosition s savePos) (y, e, false)
+    | .ok s' x => f y x s' >>= fun
+      | .ok s'' y =>
+        if _h : Stream.remaining s'' < Stream.remaining s then
+          efoldlPAux f p y s''
+        else
+          return .ok (Stream.setPosition s'' savePos) (y, default, true)
+      | .error s' e => return .ok (Stream.setPosition s' savePos) (y, e, true)
+    | .error s' e => return .ok (Stream.setPosition s' savePos) (y, e, false)
+termination_by Stream.remaining s
 
 /--
 `foldlP f init p` folds the parser function `f` from left to right using `init` as an intitial

Parser/Stream.lean

@@ -36,6 +36,15 @@ protected class Parser.Stream (σ : Type _) (τ : outParam (Type _)) extends Std
   Position : Type _
   getPosition : σ → Position
   setPosition : σ → Position → σ
+  /-- Returns a natural number measure of remaining input.
+
+  This is used by fold combinators as a termination measure to guarantee totality.
+  Each call to `next?` that returns `some` must strictly decrease `remaining`.
+
+  Fold combinators check at runtime that `remaining` decreases after each parser
+  iteration, so even an incorrect implementation cannot cause non-termination.
+  However, an incorrect implementation may cause folds to terminate prematurely. -/
+  remaining : σ → Nat
 attribute [reducible, inherit_doc Parser.Stream] Parser.Stream.Position
 attribute [inherit_doc Parser.Stream] Parser.Stream.getPosition Parser.Stream.setPosition
 
@@ -64,12 +73,14 @@ instance (σ τ) [self : Std.Stream σ τ] : Parser.Stream (mkDefault σ τ) τ
   Position := σ
   getPosition s := s
   setPosition _ p := p
+  remaining _ := 0 -- fold combinators will not function with mkDefault
 
 @[reducible]
 instance : Parser.Stream String.Slice Char where
   Position := String.Slice
   getPosition s := s
   setPosition _ s := s
+  remaining s := s.utf8ByteSize
 
 @[reducible]
 instance : Parser.Stream Substring.Raw Char where
@@ -80,6 +91,7 @@ instance : Parser.Stream Substring.Raw Char where
       { s with startPos := p }
     else
       { s with startPos := s.stopPos }
+  remaining s := s.bsize
 
 @[reducible]
 instance (τ) : Parser.Stream (Subarray τ) τ where
@@ -90,12 +102,14 @@ instance (τ) : Parser.Stream (Subarray τ) τ where
       ⟨{ s.internalRepresentation with start := p, start_le_stop := h }⟩
     else
       ⟨{ s.internalRepresentation with start := s.stop, start_le_stop := Nat.le_refl s.stop }⟩
+  remaining s := s.stop - s.start
 
 @[reducible]
 instance : Parser.Stream ByteSlice UInt8 where
   Position := Nat
   getPosition s := s.start
   setPosition s p := s.slice p
+  remaining s := s.size
 
 /-- `OfList` is a view of a list stream that keeps track of consumed tokens. -/
 structure OfList (τ : Type _) where
@@ -133,5 +147,6 @@ instance (τ) : Parser.Stream (OfList τ) τ where
     match s with
     | ⟨x :: rest, past⟩ => some (x, ⟨rest, x :: past⟩)
     | _ => none
+  remaining s := s.next.length
 
 end Parser.Stream

WellFoundedStreams.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2025 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+
+Adapted from batteries PR#1331 (https://github.com/leanprover-community/batteries/pull/1331)
+for inclusion in lean4-parser as a self-contained component.
+-/
+
+import WellFoundedStreams.Basic
+import WellFoundedStreams.Finite