tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

binary.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))