6dcf2f2087adef04a9b60330563c58c782ab51678622fafdbd7c7a6b14d20483.tri (5001B)
1 !import base * 2 !export * 3 4 errUnexpectedEof = 1 5 errUnexpectedBytes = 2 6 errUnexpectedByte = 3 7 8 unit = t 9 10 -- Byte streams are proper lists of canonical naturals in 0..255. 11 -- Prefix readers inspect only consumed cells; readBytes 0 never inspects input. 12 errInvalidBinaryInput = 15 13 errInvalidCount = 16 14 binaryByte? byte = and? (isNat? byte) (lte_? byte 255) 15 binaryBytes? bytes = case bytes of 16 [] = true 17 [byte | rest] = and? (binaryByte? byte) (binaryBytes? rest) 18 _ = false 19 20 readU8 bytes = case bytes of 21 [] = err errUnexpectedEof bytes 22 [byte | rest] = (lazyBool 23 (_ : ok byte rest) 24 (_ : err errInvalidBinaryInput bytes) 25 (binaryByte? byte)) 26 _ = err errInvalidBinaryInput bytes 27 28 readBytes n bytes = (lazyBool 29 (_ : let rec 30 walk count remaining reversed = (lazyBool 31 (_ : ok (reverse reversed) remaining) 32 (_ : matchResult 33 (code _ : err code bytes) 34 (byte rest : walk (pred_ count) rest (pair byte reversed)) 35 (readU8 remaining)) 36 (isZero_? count)) 37 in walk n bytes []) 38 (_ : err errInvalidCount bytes) 39 (isNat? n)) 40 41 expectBytes expected bytes = (let rec 42 walk wanted remaining = (case wanted of 43 [] = ok unit remaining 44 [byte | tail] = (bindResult (readU8 remaining) 45 (actual rest : lazyBool 46 (_ : walk tail rest) 47 (_ : err errUnexpectedBytes bytes) 48 (equal? actual byte))) 49 _ = err errInvalidBinaryInput bytes) 50 in matchResult (code _ : err code bytes) ok (walk expected bytes)) 51 52 expectU8 expected bytes = (matchResult 53 (code _ : err code bytes) 54 (actual rest : lazyBool (_ : ok unit rest) (_ : err errUnexpectedByte bytes) (equal? actual expected)) 55 (readU8 bytes)) 56 57 read2 = (bs : readBytes 2 bs) 58 read4 = (bs : readBytes 4 bs) 59 readU32BEBytes = (bs : read4 bs) 60 61 -- --------------------------------------------------------------------------- 62 -- Parser combinators 63 -- --------------------------------------------------------------------------- 64 65 pureParser = value bs : ok value bs 66 failParser = code bs : err code bs 67 68 mapParser = f p bs : mapResult f (p bs) 69 bindParser = p f bs : bindResult (p bs) f 70 thenParser = p q bs : bindResult (p bs) (_ : q) 71 72 orParser = (p q bs : 73 matchResult 74 (_ _ : q bs) 75 (value rest : ok value rest) 76 (p bs)) 77 78 -- Exact counted repetition; callers must choose sensible counts for parsers 79 -- that do not consume input. Wire record parsers consume fixed-size prefixes. 80 repeatParser count parser bytes = (lazyBool 81 (_ : let rec 82 walk n remaining reversed = (lazyBool 83 (_ : ok (reverse reversed) remaining) 84 (_ : bindResult (parser remaining) 85 (value rest : walk (pred_ n) rest (pair value reversed))) 86 (isZero_? n)) 87 in walk count bytes []) 88 (_ : err errInvalidCount bytes) 89 (isNat? count)) 90 91 readWhile predicate bytes = (let rec 92 walk remaining reversed = (case remaining of 93 [] = ok (reverse reversed) [] 94 _ = (bindResult (readU8 remaining) 95 (value rest : lazyBool 96 (_ : walk rest (pair value reversed)) 97 (_ : ok (reverse reversed) remaining) 98 (predicate value)))) 99 in walk bytes []) 100 101 readUntil predicate = readWhile (value : not? (predicate value)) 102 readRemaining bytes = lazyBool (_ : ok bytes []) (_ : err errInvalidBinaryInput bytes) (binaryBytes? bytes) 103 peekU8 bytes = bindResult (readU8 bytes) (value _ : ok value bytes) 104 eof? bytes = case bytes of 105 [] = ok unit bytes 106 _ = err errUnexpectedBytes bytes 107 expectAscii = expectBytes 108 109 -- RFC 3629: shortest UTF-8 only, excluding surrogates and values above U+10FFFF. 110 -- This is validation, not decoding; callers retain their original octets. 111 binaryUtf8? bytes = (and? (binaryBytes? bytes) 112 (let 113 between value low high = and? (gte_? value low) (lte_? value high) 114 continuation value = between value 128 191 115 in let rec 116 walk remaining = (case remaining of 117 [] = true 118 [first | rest] = (lazyBool 119 (_ : walk rest) 120 (_ : lazyBool 121 (_ : case rest of 122 [second | tail] = and? (continuation second) (walk tail) 123 _ = false) 124 (_ : lazyBool 125 (_ : case rest of 126 [second third | tail] = (and? (continuation second) 127 (and? (continuation third) 128 (and? (or? (not? (equal? first 224)) (gte_? second 160)) 129 (and? (or? (not? (equal? first 237)) (lte_? second 159)) (walk tail))))) 130 _ = false) 131 (_ : case rest of 132 [second third fourth | tail] = (and? (between first 240 244) 133 (and? (continuation second) (and? (continuation third) 134 (and? (continuation fourth) 135 (and? (or? (not? (equal? first 240)) (gte_? second 144)) 136 (and? (or? (not? (equal? first 244)) (lte_? second 143)) (walk tail))))))) 137 _ = false) 138 (between first 224 239)) 139 (between first 194 223)) 140 (lte_? first 127)) 141 _ = false) 142 in walk bytes))