Skip to content

Commit 52079a7

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(idris2): tighten Ephapax.Parse.Lexer to %default total (#93)
## Summary Fourth file in the `%default partial` → `%default total` chain. Companions: PR #89 (SExpr), #90 (Stream), #91 (Util). `Ephapax.Parse.Lexer.lex.go : Pos -> List Char -> List Token -> ...` is a hand-written tokeniser that slices the input via `span` / pattern destructuring and recurses on the tail. Idris2 can't track that each branch's `tail` / `more` / `rest3` is structurally smaller than the original list, so the totality checker rejects `go` (and `lex` transitively). Fix: add a Nat fuel parameter to `go`. Fuel = `length (unpack input)` at entry (set in `lex`). Every recursive call decrements fuel by 1 and consumes ≥ 1 character of input — the well-formed assumption every Lexer branch already satisfies. All 57 recursive `go`-call sites updated mechanically (bulk sed within the `where`-block, then spot-fixed two pattern-declaration over-applications). `readString.goStr` is already structurally total (recurses on the tail of a pattern-match list) and required no fuel. `advanceN` likewise. ## Soundness On every well-formed input, fuel exhausts *at or after* the input list does — so behaviour is identical to the partial original. A degenerate non-consuming branch (which Lexer does not contain) would loop forever in the partial form and return truncated output in the fueled form — strictly safer. No `assert_total` / `assert_smaller` / `believe_me` escapes. ## Verification ``` $ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Parse/Lexer.idr 1/1: Building Ephapax.Parse.Lexer (Ephapax/Parse/Lexer.idr) $ idris2 --check Ephapax/Parse/Parser.idr # downstream 6/6: Building Ephapax.Parse.Parser (Ephapax/Parse/Parser.idr) ``` ## Refs - `#124` (proof-debt audit epic) - `#134` (ephapax totality sub-issue) - Companions: PR `#89` (SExpr), `#90` (Stream), `#91` (Util) ## Test plan - [x] `idris2 --check Ephapax/Parse/Lexer.idr` builds green under `%default total` - [x] Downstream `Ephapax.Parse.Parser` (transitive Stream / Util) still builds - [ ] CI green - [ ] No `assert_*` / `believe_me` introduced (verified — inspect the diff) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent e9453c6 commit 52079a7

1 file changed

Lines changed: 64 additions & 61 deletions

File tree

‎idris2/src/Ephapax/Parse/Lexer.idr‎

Lines changed: 64 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ module Ephapax.Parse.Lexer
22

33
import Data.List
44

5-
%default partial
5+
%default total
66

77
public export
88
record Pos where
@@ -128,7 +128,9 @@ Show LexError where
128128

129129
public export
130130
lex : String -> Either LexError (List Token)
131-
lex input = go (MkPos 1 1) (unpack input) []
131+
lex input =
132+
let cs = unpack input in
133+
go (length cs) (MkPos 1 1) cs []
132134
where
133135
isSpaceChar : Char -> Bool
134136
isSpaceChar ch = ch == ' ' || ch == '\t' || ch == '\r'
@@ -176,176 +178,177 @@ lex input = go (MkPos 1 1) (unpack input) []
176178
goStr pos' (unescape c :: acc) rest
177179
goStr pos acc (c :: rest) = goStr (advance pos c) (c :: acc) rest
178180

179-
go : Pos -> List Char -> List Token -> Either LexError (List Token)
180-
go _ [] acc = Right (reverse acc)
181-
go pos ('-' :: '-' :: rest) acc =
181+
go : Nat -> Pos -> List Char -> List Token -> Either LexError (List Token)
182+
go Z _ _ acc = Right (reverse acc)
183+
go (S k) _ [] acc = Right (reverse acc)
184+
go (S k) pos ('-' :: '-' :: rest) acc =
182185
let (skipped, more) = span (/= '\n') rest in
183186
let (consumed, tail) = case more of
184187
'\n' :: tail' => (skipped ++ ['\n'], tail')
185188
_ => (skipped, more)
186-
in go (advanceN pos ('-' :: '-' :: consumed)) tail acc
187-
go pos (c :: rest) acc =
188-
if isSpaceChar c then go (advance pos c) rest acc
189+
in go k (advanceN pos ('-' :: '-' :: consumed)) tail acc
190+
go (S k) pos (c :: rest) acc =
191+
if isSpaceChar c then go k (advance pos c) rest acc
189192
else if c == '\n' then
190193
let nextPos = advance pos c in
191-
go nextPos rest (MkToken TkSemi pos :: acc)
194+
go k nextPos rest (MkToken TkSemi pos :: acc)
192195
else if isAlphaChar c || c == '_' then
193196
let (identChars, more) = span isIdentChar (c :: rest) in
194197
let ident = pack identChars in
195198
let tokPos = pos in
196199
let nextPos = advanceN pos identChars in
197200
case ident of
198-
"true" => go nextPos more (MkToken (TkBool True) tokPos :: acc)
199-
"false" => go nextPos more (MkToken (TkBool False) tokPos :: acc)
201+
"true" => go k nextPos more (MkToken (TkBool True) tokPos :: acc)
202+
"false" => go k nextPos more (MkToken (TkBool False) tokPos :: acc)
200203
"let" =>
201204
case more of
202205
'!' :: tail =>
203206
let nextPos2 = advance nextPos '!' in
204-
go nextPos2 tail (MkToken (TkKw "let!") tokPos :: acc)
205-
_ => go nextPos more (MkToken (TkKw "let") tokPos :: acc)
206-
"fn" => go nextPos more (MkToken (TkKw "fn") tokPos :: acc)
207-
"if" => go nextPos more (MkToken (TkKw "if") tokPos :: acc)
208-
"then" => go nextPos more (MkToken (TkKw "then") tokPos :: acc)
209-
"else" => go nextPos more (MkToken (TkKw "else") tokPos :: acc)
210-
"in" => go nextPos more (MkToken (TkKw "in") tokPos :: acc)
211-
"region" => go nextPos more (MkToken (TkKw "region") tokPos :: acc)
212-
"drop" => go nextPos more (MkToken (TkKw "drop") tokPos :: acc)
213-
"copy" => go nextPos more (MkToken (TkKw "copy") tokPos :: acc)
214-
"inl" => go nextPos more (MkToken (TkKw "inl") tokPos :: acc)
215-
"inr" => go nextPos more (MkToken (TkKw "inr") tokPos :: acc)
216-
"case" => go nextPos more (MkToken (TkKw "case") tokPos :: acc)
217-
"of" => go nextPos more (MkToken (TkKw "of") tokPos :: acc)
218-
"type" => go nextPos more (MkToken (TkKw "type") tokPos :: acc)
207+
go k nextPos2 tail (MkToken (TkKw "let!") tokPos :: acc)
208+
_ => go k nextPos more (MkToken (TkKw "let") tokPos :: acc)
209+
"fn" => go k nextPos more (MkToken (TkKw "fn") tokPos :: acc)
210+
"if" => go k nextPos more (MkToken (TkKw "if") tokPos :: acc)
211+
"then" => go k nextPos more (MkToken (TkKw "then") tokPos :: acc)
212+
"else" => go k nextPos more (MkToken (TkKw "else") tokPos :: acc)
213+
"in" => go k nextPos more (MkToken (TkKw "in") tokPos :: acc)
214+
"region" => go k nextPos more (MkToken (TkKw "region") tokPos :: acc)
215+
"drop" => go k nextPos more (MkToken (TkKw "drop") tokPos :: acc)
216+
"copy" => go k nextPos more (MkToken (TkKw "copy") tokPos :: acc)
217+
"inl" => go k nextPos more (MkToken (TkKw "inl") tokPos :: acc)
218+
"inr" => go k nextPos more (MkToken (TkKw "inr") tokPos :: acc)
219+
"case" => go k nextPos more (MkToken (TkKw "case") tokPos :: acc)
220+
"of" => go k nextPos more (MkToken (TkKw "of") tokPos :: acc)
221+
"type" => go k nextPos more (MkToken (TkKw "type") tokPos :: acc)
219222
_ =>
220223
case more of
221224
'.' :: rest2 =>
222225
let (tailChars, rest3) = span isIdentChar rest2 in
223226
let full = identChars ++ ['.'] ++ tailChars in
224227
let fullStr = pack full in
225228
let nextPos2 = advanceN pos full in
226-
go nextPos2 rest3 (MkToken (TkIdent fullStr) tokPos :: acc)
227-
_ => go nextPos more (MkToken (TkIdent ident) tokPos :: acc)
229+
go k nextPos2 rest3 (MkToken (TkIdent fullStr) tokPos :: acc)
230+
_ => go k nextPos more (MkToken (TkIdent ident) tokPos :: acc)
228231
else if isDigitChar c then
229232
let (numChars, more) = span isNumChar (c :: rest) in
230233
let tokPos = pos in
231234
let nextPos = advanceN pos numChars in
232235
if elem '.' numChars
233-
then go nextPos more (MkToken (TkFloat (pack numChars)) tokPos :: acc)
234-
else go nextPos more (MkToken (TkInt (pack numChars)) tokPos :: acc)
236+
then go k nextPos more (MkToken (TkFloat (pack numChars)) tokPos :: acc)
237+
else go k nextPos more (MkToken (TkInt (pack numChars)) tokPos :: acc)
235238
else case c of
236239
'(' =>
237240
case rest of
238241
')' :: tail =>
239242
let nextPos = advanceN pos ['(', ')'] in
240-
go nextPos tail (MkToken TkUnit pos :: acc)
243+
go k nextPos tail (MkToken TkUnit pos :: acc)
241244
_ =>
242245
let nextPos = advance pos '(' in
243-
go nextPos rest (MkToken TkLParen pos :: acc)
246+
go k nextPos rest (MkToken TkLParen pos :: acc)
244247
')' =>
245248
let nextPos = advance pos ')' in
246-
go nextPos rest (MkToken TkRParen pos :: acc)
249+
go k nextPos rest (MkToken TkRParen pos :: acc)
247250
'{' =>
248251
let nextPos = advance pos '{' in
249-
go nextPos rest (MkToken TkLBrace pos :: acc)
252+
go k nextPos rest (MkToken TkLBrace pos :: acc)
250253
'}' =>
251254
let nextPos = advance pos '}' in
252-
go nextPos rest (MkToken TkRBrace pos :: acc)
255+
go k nextPos rest (MkToken TkRBrace pos :: acc)
253256
'[' =>
254257
let nextPos = advance pos '[' in
255-
go nextPos rest (MkToken TkLBracket pos :: acc)
258+
go k nextPos rest (MkToken TkLBracket pos :: acc)
256259
']' =>
257260
let nextPos = advance pos ']' in
258-
go nextPos rest (MkToken TkRBracket pos :: acc)
261+
go k nextPos rest (MkToken TkRBracket pos :: acc)
259262
',' =>
260263
let nextPos = advance pos ',' in
261-
go nextPos rest (MkToken TkComma pos :: acc)
264+
go k nextPos rest (MkToken TkComma pos :: acc)
262265
':' =>
263266
let nextPos = advance pos ':' in
264-
go nextPos rest (MkToken TkColon pos :: acc)
267+
go k nextPos rest (MkToken TkColon pos :: acc)
265268
';' =>
266269
let nextPos = advance pos ';' in
267-
go nextPos rest (MkToken TkSemi pos :: acc)
270+
go k nextPos rest (MkToken TkSemi pos :: acc)
268271
'@' =>
269272
let nextPos = advance pos '@' in
270-
go nextPos rest (MkToken TkAt pos :: acc)
273+
go k nextPos rest (MkToken TkAt pos :: acc)
271274
'.' =>
272275
let nextPos = advance pos '.' in
273-
go nextPos rest (MkToken TkDot pos :: acc)
276+
go k nextPos rest (MkToken TkDot pos :: acc)
274277
'=' =>
275278
case rest of
276279
'=' :: tail =>
277280
let nextPos = advanceN pos ['=', '='] in
278-
go nextPos tail (MkToken TkEqEq pos :: acc)
281+
go k nextPos tail (MkToken TkEqEq pos :: acc)
279282
_ =>
280283
let nextPos = advance pos '=' in
281-
go nextPos rest (MkToken TkEq pos :: acc)
284+
go k nextPos rest (MkToken TkEq pos :: acc)
282285
'!' =>
283286
case rest of
284287
'=' :: tail =>
285288
let nextPos = advanceN pos ['!', '='] in
286-
go nextPos tail (MkToken TkNe pos :: acc)
289+
go k nextPos tail (MkToken TkNe pos :: acc)
287290
_ =>
288291
let nextPos = advance pos '!' in
289-
go nextPos rest (MkToken TkBang pos :: acc)
292+
go k nextPos rest (MkToken TkBang pos :: acc)
290293
'<' =>
291294
case rest of
292295
'=' :: tail =>
293296
let nextPos = advanceN pos ['<', '='] in
294-
go nextPos tail (MkToken TkLe pos :: acc)
297+
go k nextPos tail (MkToken TkLe pos :: acc)
295298
_ =>
296299
let nextPos = advance pos '<' in
297-
go nextPos rest (MkToken TkLt pos :: acc)
300+
go k nextPos rest (MkToken TkLt pos :: acc)
298301
'>' =>
299302
case rest of
300303
'=' :: tail =>
301304
let nextPos = advanceN pos ['>', '='] in
302-
go nextPos tail (MkToken TkGe pos :: acc)
305+
go k nextPos tail (MkToken TkGe pos :: acc)
303306
_ =>
304307
let nextPos = advance pos '>' in
305-
go nextPos rest (MkToken TkGt pos :: acc)
308+
go k nextPos rest (MkToken TkGt pos :: acc)
306309
'&' =>
307310
case rest of
308311
'&' :: tail =>
309312
let nextPos = advanceN pos ['&', '&'] in
310-
go nextPos tail (MkToken TkAndAnd pos :: acc)
313+
go k nextPos tail (MkToken TkAndAnd pos :: acc)
311314
_ =>
312315
let nextPos = advance pos '&' in
313-
go nextPos rest (MkToken TkAmp pos :: acc)
316+
go k nextPos rest (MkToken TkAmp pos :: acc)
314317
'|' =>
315318
case rest of
316319
'|' :: tail =>
317320
let nextPos = advanceN pos ['|', '|'] in
318-
go nextPos tail (MkToken TkOrOr pos :: acc)
321+
go k nextPos tail (MkToken TkOrOr pos :: acc)
319322
_ => Left (UnexpectedChar '|' pos)
320323
'+' =>
321324
let nextPos = advance pos '+' in
322-
go nextPos rest (MkToken TkPlus pos :: acc)
325+
go k nextPos rest (MkToken TkPlus pos :: acc)
323326
'-' =>
324327
case rest of
325328
'>' :: tail =>
326329
let nextPos = advanceN pos ['-', '>'] in
327-
go nextPos tail (MkToken TkArrow pos :: acc)
330+
go k nextPos tail (MkToken TkArrow pos :: acc)
328331
_ =>
329332
let nextPos = advance pos '-' in
330-
go nextPos rest (MkToken TkMinus pos :: acc)
333+
go k nextPos rest (MkToken TkMinus pos :: acc)
331334
'*' =>
332335
let nextPos = advance pos '*' in
333-
go nextPos rest (MkToken TkStar pos :: acc)
336+
go k nextPos rest (MkToken TkStar pos :: acc)
334337
'/' =>
335338
case rest of
336339
'/' :: tail =>
337340
let (comment, more) = span (\ch => ch /= '\n') tail in
338341
let skipped = '/' :: '/' :: comment in
339342
let nextPos = advanceN pos skipped in
340-
go nextPos more acc
343+
go k nextPos more acc
341344
_ =>
342345
let nextPos = advance pos '/' in
343-
go nextPos rest (MkToken TkSlash pos :: acc)
346+
go k nextPos rest (MkToken TkSlash pos :: acc)
344347
'%' =>
345348
let nextPos = advance pos '%' in
346-
go nextPos rest (MkToken TkPercent pos :: acc)
349+
go k nextPos rest (MkToken TkPercent pos :: acc)
347350
'"' =>
348351
case readString pos rest of
349352
Left err => Left err
350-
Right (s, more, nextPos) => go nextPos more (MkToken (TkString s) pos :: acc)
353+
Right (s, more, nextPos) => go k nextPos more (MkToken (TkString s) pos :: acc)
351354
_ => Left (UnexpectedChar c pos)

0 commit comments

Comments
 (0)