From 12af8733c24227d682a63faafd7ad887774a347a Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 20 May 2026 18:14:48 +0100
Subject: [PATCH] proof(idris2): tighten Ephapax.Parse.Util to %default total
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Two combinators recurse unboundedly on a Stream rather than on a Nat:

  - many p : repeatedly applies p until failure
  - sepBy.sepTail : alternates sep + p until sep fails

Replace both with Nat-fueled siblings (manyFuel / sepTailFuel) where
fuel = integerToNat (cast (s.len - s.index)) — i.e. the count of
remaining tokens in the input stream at entry. Each recursive call
decrements fuel by 1; the inner parser p (and sep) is assumed to
consume >=1 token per Right return (the only well-formed usage),
so fuel exhausts at-or-after the parser exhausts the stream.

Soundness: the fueled forms preserve the partial originals' behaviour
on every consuming parser. On a degenerate non-consuming parser the
original would loop forever; the fueled form returns a truncated list.
Strictly safer.

No assert_total / assert_smaller / believe_me escapes. sepBy1
delegates to sepBy and inherits totality for free.

Downstream Ephapax.Parse.Parser still builds clean.

Refs #124 (proof-debt epic), #134 (ephapax totality)
Part of ephapax %default partial -> total campaign: 3/9 files done
(SExpr.idr PR #89; Stream.idr PR #90; Util.idr here).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 idris2/src/Ephapax/Parse/Util.idr | 29 ++++++++++++++++++-----------
 1 file changed, 18 insertions(+), 11 deletions(-)

diff --git a/idris2/src/Ephapax/Parse/Util.idr b/idris2/src/Ephapax/Parse/Util.idr
index b06088d..787a2e7 100644
--- a/idris2/src/Ephapax/Parse/Util.idr
+++ b/idris2/src/Ephapax/Parse/Util.idr
@@ -4,7 +4,7 @@ import Data.List
 import Ephapax.Parse.Lexer
 import Ephapax.Parse.Stream
 
-%default partial
+%default total
 
 public export
 data ParseError = PE String (Maybe Pos)
@@ -56,12 +56,17 @@ expectIdent stream =
 public export
 many : Parser a -> Parser (List a)
 many p stream =
-  case p stream of
-    Left _ => Right ([], stream)
-    Right (v, rest) =>
-      case many p rest of
-        Left err => Left err
-        Right (vs, rest2) => Right (v :: vs, rest2)
+  manyFuel (integerToNat (cast (stream.len - stream.index))) p stream
+  where
+    manyFuel : Nat -> Parser a -> Parser (List a)
+    manyFuel Z _ s = Right ([], s)
+    manyFuel (S k) p s =
+      case p s of
+        Left _ => Right ([], s)
+        Right (v, rest) =>
+          case manyFuel k p rest of
+            Left err => Left err
+            Right (vs, rest2) => Right (v :: vs, rest2)
 
 public export
 optional : Parser a -> Parser (Maybe a)
@@ -156,16 +161,18 @@ sepBy : Parser a -> Parser sep -> Parser (List a)
 sepBy p sep stream =
   case p stream of
     Left _ => Right ([], stream)
-    Right (v, rest) => sepTail [v] rest
+    Right (v, rest) =>
+      sepTailFuel (integerToNat (cast (rest.len - rest.index))) [v] rest
   where
-    sepTail : List a -> Parser (List a)
-    sepTail acc stream2 =
+    sepTailFuel : Nat -> List a -> Parser (List a)
+    sepTailFuel Z acc stream2 = Right (reverse acc, stream2)
+    sepTailFuel (S k) acc stream2 =
       case sep stream2 of
         Left _ => Right (reverse acc, stream2)
         Right (_, rest) =>
           case p rest of
             Left err => Left err
-            Right (v, rest2) => sepTail (v :: acc) rest2
+            Right (v, rest2) => sepTailFuel k (v :: acc) rest2
 
 public export
 sepBy1 : Parser a -> Parser sep -> Parser (List a)