Data-first recursive consumers in readBytes
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.
This commit is contained in:
@@ -9,11 +9,14 @@ readArborixMagic = (bs : expectBytes arborixMagic bs)
|
||||
|
||||
readArborixHeader = (bs :
|
||||
bindResult (readArborixMagic bs)
|
||||
(_ r0 :
|
||||
bindResult (readU16BEBytes r0)
|
||||
(major r1 :
|
||||
bindResult (readU16BEBytes r1)
|
||||
(minor r2 :
|
||||
bindResult (readU32BEBytes r2)
|
||||
(sections r3 :
|
||||
ok (pair major (pair minor sections)) r3)))))
|
||||
(_ afterMagic :
|
||||
bindResult (readBytes 2 afterMagic)
|
||||
(majorVersion afterMajor :
|
||||
bindResult (readBytes 2 afterMajor)
|
||||
(minorVersion afterMinor :
|
||||
bindResult (readBytes 4 afterMinor)
|
||||
(sectionCount afterSectionCount :
|
||||
ok
|
||||
(pair majorVersion
|
||||
(pair minorVersion sectionCount))
|
||||
afterSectionCount)))))
|
||||
|
||||
@@ -26,26 +26,38 @@ readU8 = (bytes : matchList
|
||||
(h r : ok h r)
|
||||
bytes)
|
||||
|
||||
readBytesTaken = n bytes : bytesTake n bytes
|
||||
readBytesRest = n bytes : bytesDrop n bytes
|
||||
readBytesEnough? = n bytes : equal? (bytesLength (readBytesTaken n bytes)) n
|
||||
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 bytes : matchBool
|
||||
(ok (readBytesTaken n bytes) (readBytesRest n bytes))
|
||||
(err errUnexpectedEof bytes)
|
||||
(readBytesEnough? n bytes))
|
||||
readBytes = (n bs : readBytes_ bs n 0 bs t)
|
||||
|
||||
unit = t
|
||||
|
||||
expectBytes = (expected bs :
|
||||
matchResult
|
||||
(code rest : err code bs)
|
||||
(taken rest :
|
||||
matchBool
|
||||
(ok unit rest)
|
||||
(err errUnexpectedBytes bs)
|
||||
(bytesEq? taken expected))
|
||||
(readBytes (bytesLength expected) bs))
|
||||
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
|
||||
@@ -57,9 +69,6 @@ expectU8 = (expected bs :
|
||||
(byteEq? actual expected))
|
||||
(readU8 bs))
|
||||
|
||||
read2 = (bs : readBytes 2 bs)
|
||||
read4 = (bs : readBytes 4 bs)
|
||||
|
||||
mapResult = (f result :
|
||||
matchResult
|
||||
(code rest : err code rest)
|
||||
@@ -72,5 +81,7 @@ bindResult = (result f :
|
||||
(value rest : f value rest)
|
||||
result)
|
||||
|
||||
read2 = (bs : readBytes 2 bs)
|
||||
read4 = (bs : readBytes 4 bs)
|
||||
readU16BEBytes = (bs : read2 bs)
|
||||
readU32BEBytes = (bs : read4 bs)
|
||||
|
||||
Reference in New Issue
Block a user