James Eversole
e8ab61dbaa
Reorder recursive byte-stream consumers so the consumed input is inspected before loop-control arguments can drive evaluation. Previously, partially applying `readBytes` to a known count, such as `readBytes 2`, allowed the evaluator to specialize the recursive worker using known counter values while the byte stream was still abstract. This caused symbolic recursion over unknown input and produced an enormous normal form. The recursive worker now takes the byte stream first and immediately case-analyzes it. As a result, partial application blocks at the input boundary instead of unrolling the counter loop. This preserves the fully-applied behavior of `readBytes`, while making partial application such as `readBytes 2` normalize safely.
88 lines
1.9 KiB
Plaintext
88 lines
1.9 KiB
Plaintext
!import "base.tri" !Local
|
|
!import "list.tri" !Local
|
|
!import "bytes.tri" !Local
|
|
|
|
errUnexpectedEof = 1
|
|
errUnexpectedBytes = 2
|
|
errUnexpectedByte = 3
|
|
|
|
ok = value rest : pair true (pair value rest)
|
|
err = code rest : pair false (pair code rest)
|
|
|
|
matchResult = (errCase okCase result :
|
|
matchPair
|
|
(tag payload :
|
|
matchPair
|
|
(value rest :
|
|
matchBool
|
|
(okCase value rest)
|
|
(errCase value rest)
|
|
tag)
|
|
payload)
|
|
result)
|
|
|
|
readU8 = (bytes : matchList
|
|
(err errUnexpectedEof t)
|
|
(h r : ok h r)
|
|
bytes)
|
|
|
|
readBytes_ = y (self bs n i original acc :
|
|
matchList
|
|
(matchBool
|
|
(ok (reverse acc) bs)
|
|
(err errUnexpectedEof original)
|
|
(equal? i n))
|
|
(h r :
|
|
matchBool
|
|
(ok (reverse acc) bs)
|
|
(self r n (succ i) original (pair h acc))
|
|
(equal? i n))
|
|
bs)
|
|
|
|
readBytes = (n bs : readBytes_ bs n 0 bs t)
|
|
|
|
unit = t
|
|
|
|
expectBytes_ = y (self expected bs original :
|
|
matchList
|
|
(ok unit bs)
|
|
(expectedByte expectedRest :
|
|
matchResult
|
|
(code rest : err code original)
|
|
(actual rest :
|
|
matchBool
|
|
(self expectedRest rest original)
|
|
(err errUnexpectedBytes original)
|
|
(byteEq? actual expectedByte))
|
|
(readU8 bs))
|
|
expected)
|
|
|
|
expectBytes = (expected bs : expectBytes_ expected bs bs)
|
|
|
|
expectU8 = (expected bs :
|
|
matchResult
|
|
(code rest : err code bs)
|
|
(actual rest :
|
|
matchBool
|
|
(ok unit rest)
|
|
(err errUnexpectedByte bs)
|
|
(byteEq? actual expected))
|
|
(readU8 bs))
|
|
|
|
mapResult = (f result :
|
|
matchResult
|
|
(code rest : err code rest)
|
|
(value rest : ok (f value) rest)
|
|
result)
|
|
|
|
bindResult = (result f :
|
|
matchResult
|
|
(code rest : err code rest)
|
|
(value rest : f value rest)
|
|
result)
|
|
|
|
read2 = (bs : readBytes 2 bs)
|
|
read4 = (bs : readBytes 4 bs)
|
|
readU16BEBytes = (bs : read2 bs)
|
|
readU32BEBytes = (bs : read4 bs)
|