tricu

A lazy functional language based on Tree Calculus
Log | Files | Refs | README | LICENSE

1ca2682e6a35d949196ff3b1d2aabed47af57e7ef43b8e32b2b7b19ca004f64f.tri (8136B)

      1 !import base as B
      2 !import native_math as N
      3 !import io_v2 as IO
      4 !export readSource
      5 !export readText
      6 !export encodeText
      7 !export writeText
      8 !export lineCursor
      9 !export readLine
     10 
     11 problem operation detail progress = ["invalid-data" operation detail progress]
     12 -- base.foldr supplies the accumulator first.
     13 flatten chunks = B.foldr (suffix chunk : B.append chunk suffix) [] (B.reverse chunks)
     14 
     15 checkedLimit limit next = case B.checkContract B.nat? limit of
     16   ((t t), (count, t)) = case N.lte count 9223372036854775807 of
     17     (t t) = next count
     18     _ = IO.pure (B.err ["invalid-bound" "text/limit" "invalid text byte limit" "none"] t)
     19   _ = IO.pure (B.err ["invalid-bound" "text/limit" "invalid text byte limit" "none"] t)
     20 
     21 -- Split a bounded prefix; native encode validates its scalars before producing
     22 -- bytes. [] signals an improper character spine.
     23 split 0 rest = [[] rest]
     24 split _ [] = [[] []]
     25 split count [c | rest] = case split (N.predecessor count) rest of
     26   [prefix after] = [(B.pair c prefix) after]
     27   _ = []
     28 split _ _ = []
     29 
     30 encodeLoop remaining text chunks = case split 1024 text of
     31   [[] []] = IO.pure (B.ok (flatten chunks) t)
     32   [part rest] = do IO.onOk
     33     bytes <- IO.encodeUTF8 part
     34     case N.lte (B.length bytes) remaining of
     35       (t t) = encodeLoop (N.subtract remaining (B.length bytes)) rest (B.pair bytes chunks)
     36       _ = IO.pure (B.err ["invalid-bound" "text/encode" "encoded text exceeds byte limit" "none"] t)
     37   _ = IO.pure (B.err (problem "text/encode" "improper scalar list" "none") t)
     38 encodeText limit text = checkedLimit limit (remaining : encodeLoop remaining text [])
     39 
     40 -- Force the small acknowledged-byte counter before the next request, without
     41 -- retaining arithmetic that depends on previously emitted chunks.
     42 forceCount t next = next t
     43 forceCount (t bit rest) next = case bit of
     44   t = forceCount rest next
     45   (t t) = forceCount rest next
     46   _ = IO.fail "Invalid text counter"
     47 forceCount _ _ = IO.fail "Invalid text counter"
     48 writeFailure confirmed cause = IO.pure (B.err ["write-text" confirmed cause] t)
     49 writeLoop writer text confirmed = forceCount confirmed (_ : case split 1024 text of
     50   [[] []] = IO.pure (B.ok t t)
     51   [part rest] = IO.bind (IO.encodeUTF8 part) (encoded : case encoded of
     52     ((t t), (bytes, t)) = IO.bind (IO.writeAll writer bytes) (written : case written of
     53       ((t t), (t, t)) = writeLoop writer rest (N.add confirmed (B.length bytes))
     54       (t, (cause, t)) = writeFailure confirmed cause
     55       _ = IO.fail "Invalid text write reply")
     56     (t, (cause, t)) = writeFailure confirmed cause
     57     _ = IO.fail "Invalid UTF-8 encode reply")
     58   _ = writeFailure confirmed (problem "text/write" "improper scalar list" "none"))
     59 writeText writer text = writeLoop writer text 0
     60 
     61 -- Whole-source convenience retaining the exact received octets and decoded
     62 -- scalars. Source policy rejects an initial BOM. A one-byte EOF probe detects
     63 -- excess input at the budget boundary. Callers serialize use of this cursor
     64 -- across the complete operation; native leases cover individual reads.
     65 -- Composite failure retains confirmed input
     66 -- bytes (before any uncertain failing read) plus the unchanged native problem.
     67 readFailure consumed cause = IO.pure (B.err ["read-source" consumed cause] t)
     68 readCount 0 = 1
     69 readCount remaining = case N.lte remaining 4093 of
     70   (t t) = remaining
     71   _ = 4093
     72 readLoop reader limit remaining carry first rawChunks textChunks =
     73   IO.bind (IO.readSome reader (readCount remaining)) (received : case received of
     74     ((t t), (("eof", t), t)) = IO.bind (IO.decodeUTF8 1 carry) (decoded : case decoded of
     75       ((t t), ([[] []], t)) = IO.pure (B.ok (B.pair (flatten rawChunks) (flatten textChunks)) t)
     76       (t, (cause, t)) = readFailure (N.subtract limit remaining) cause
     77       _ = IO.fail "Invalid UTF-8 final reply")
     78     ((t t), (("data", bytes), t)) = let count = B.length bytes in
     79       case N.lte count remaining of
     80         (t t) = IO.bind (IO.decodeUTF8 0 (B.append carry bytes)) (decoded : case decoded of
     81           ((t t), ([text pending], t)) = case first of
     82             1 = case text of
     83               [] = readLoop reader limit (N.subtract remaining count) pending 1 (B.pair bytes rawChunks) textChunks
     84               [65279 | _] = readFailure (N.add (N.subtract limit remaining) count)
     85                 (problem "text/read-source" "initial source BOM is not permitted" "none")
     86               _ = readLoop reader limit (N.subtract remaining count) pending 0 (B.pair bytes rawChunks) (B.pair text textChunks)
     87             _ = readLoop reader limit (N.subtract remaining count) pending 0 (B.pair bytes rawChunks) (B.pair text textChunks)
     88           (t, (cause, t)) = readFailure (N.add (N.subtract limit remaining) count) cause
     89           _ = IO.fail "Invalid UTF-8 decode reply")
     90         _ = readFailure (N.add (N.subtract limit remaining) count)
     91           ["invalid-bound" "text/read-source" "source exceeds byte limit" "none"]
     92     (t, (cause, t)) = readFailure (N.subtract limit remaining) cause
     93     _ = IO.fail "Invalid source read reply")
     94 readSource reader limit = checkedLimit limit (count : readLoop reader count count [] 1 [] [])
     95 
     96 -- Single-consumer source cursor represented as a source value. Thread the
     97 -- returned cursor forward, serialize its use with all reads on the underlying
     98 -- reader, and retire it on read failure. Read-ahead is bounded to 4093 bytes.
     99 lineCursor reader = [reader [] 0]
    100 
    101 -- The byte budget counts line content; LF delimits lines. CR, BOM and NUL
    102 -- remain content.
    103 -- Scan before decoding: malformed bytes after LF belong to the NEXT line.
    104 lineSplit [] = [[] [] 0]
    105 lineSplit [10 | rest] = [[] rest 1]
    106 lineSplit [byte | rest] = case lineSplit rest of
    107   [prefix after ended] = [(B.pair byte prefix) after ended]
    108   _ = []
    109 lineSplit _ = []
    110 lineFailure consumed cause = IO.pure (B.err ["read-line" consumed cause] t)
    111 lineReady reader after ending chunks = IO.pure
    112   (B.ok [["line" (flatten chunks) ending] [reader after 0]] t)
    113 lineEOF reader consumed carry chunks = IO.bind (IO.decodeUTF8 1 carry) (decoded : case decoded of
    114   ((t t), ([[] []], t)) = case consumed of
    115     0 = IO.pure (B.ok [["eof"] [reader [] 1]] t)
    116     _ = IO.pure (B.ok [["line" (flatten chunks) "eof"] [reader [] 1]] t)
    117   (t, (cause, t)) = lineFailure consumed cause
    118   _ = IO.fail "Invalid line final UTF-8 reply")
    119 lineLoop reader limit remaining carry chunks buffered = forceCount remaining (_ : case buffered of
    120   [] = IO.bind (IO.readSome reader 4093) (received : case received of
    121     ((t t), (("eof", t), t)) = lineEOF reader (N.subtract limit remaining) carry chunks
    122     ((t t), (("data", bytes), t)) = lineLoop reader limit remaining carry chunks bytes
    123     (t, (cause, t)) = lineFailure (N.subtract limit remaining) cause
    124     _ = IO.fail "Invalid line read reply")
    125   _ = case lineSplit buffered of
    126     [part after ended] = let count = B.length part in
    127       case N.lte count remaining of
    128         (t t) = IO.bind (IO.decodeUTF8 ended (B.append carry part)) (decoded : case decoded of
    129           ((t t), ([text pending], t)) = case ended of
    130             1 = lineReady reader after "lf" (B.pair text chunks)
    131             _ = lineLoop reader limit (N.subtract remaining count) pending (B.pair text chunks) []
    132           (t, (cause, t)) = lineFailure (N.add (N.subtract limit remaining) count) cause
    133           _ = IO.fail "Invalid line UTF-8 reply")
    134         _ = lineFailure (N.add (N.subtract limit remaining) count)
    135           ["invalid-bound" "text/read-line" "line exceeds byte limit" "none"]
    136     _ = IO.fail "Invalid line cursor bytes")
    137 readLine cursor limit = checkedLimit limit (count : case cursor of
    138   [reader buffered 0] = lineLoop reader count count [] [] buffered
    139   [reader [] 1] = IO.pure (B.ok [["eof"] cursor] t)
    140   _ = IO.pure (B.err ["invalid-argument" "text/read-line" "invalid line cursor" "none"] t))
    141 
    142 -- Generic bounded whole-text convenience preserving an initial BOM as content.
    143 -- It uses the shared incremental decoder with this text policy.
    144 readText reader limit = checkedLimit limit (count : IO.onOk
    145   (readLoop reader count count [] 0 [] [])
    146   (received : case received of
    147     (_, text) = IO.pure (B.ok text t)
    148     _ = IO.fail "Invalid text read result"))