tricu

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

9acae0f91625a1f6e13601276f2e11b319d346d872e85d758377fd649da5d5d8.tri (8264B)

      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 accumulator first, unlike the conventional Haskell API.
     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 -- A bounded split, not a scalar validator: native encode validates the complete
     22 -- prefix before it can produce 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, not a constant-memory text stream. Retain the exact
     62 -- received octets and decoded scalars without normalization or BOM stripping.
     63 -- A one-byte EOF probe detects excess input at the budget boundary. Callers must
     64 -- not share this cursor concurrently; the individual reads are leased, not the
     65 -- entire source convenience operation. 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. Thread ONLY the returned cursor forward; do not
     97 -- interleave raw reads, duplicate/reuse a cursor, or resume it after read failure.
     98 -- Read-ahead is bounded to 4093 bytes. This is not a native resource or a lock.
     99 lineCursor reader = [reader [] 0]
    100 
    101 -- LF is framing, not part of the line budget. CR, BOM and NUL remain content.
    102 -- Scan before decoding: malformed bytes after LF belong to the NEXT line.
    103 lineSplit [] = [[] [] 0]
    104 lineSplit [10 | rest] = [[] rest 1]
    105 lineSplit [byte | rest] = case lineSplit rest of
    106   [prefix after ended] = [(B.pair byte prefix) after ended]
    107   _ = []
    108 lineSplit _ = []
    109 lineFailure consumed cause = IO.pure (B.err ["read-line" consumed cause] t)
    110 lineReady reader after ending chunks = IO.pure
    111   (B.ok [["line" (flatten chunks) ending] [reader after 0]] t)
    112 lineEOF reader consumed carry chunks = IO.bind (IO.decodeUTF8 1 carry) (decoded : case decoded of
    113   ((t t), ([[] []], t)) = case consumed of
    114     0 = IO.pure (B.ok [["eof"] [reader [] 1]] t)
    115     _ = IO.pure (B.ok [["line" (flatten chunks) "eof"] [reader [] 1]] t)
    116   (t, (cause, t)) = lineFailure consumed cause
    117   _ = IO.fail "Invalid line final UTF-8 reply")
    118 lineLoop reader limit remaining carry chunks buffered = forceCount remaining (_ : case buffered of
    119   [] = IO.bind (IO.readSome reader 4093) (received : case received of
    120     ((t t), (("eof", t), t)) = lineEOF reader (N.subtract limit remaining) carry chunks
    121     ((t t), (("data", bytes), t)) = lineLoop reader limit remaining carry chunks bytes
    122     (t, (cause, t)) = lineFailure (N.subtract limit remaining) cause
    123     _ = IO.fail "Invalid line read reply")
    124   _ = case lineSplit buffered of
    125     [part after ended] = let count = B.length part in
    126       case N.lte count remaining of
    127         (t t) = IO.bind (IO.decodeUTF8 ended (B.append carry part)) (decoded : case decoded of
    128           ((t t), ([text pending], t)) = case ended of
    129             1 = lineReady reader after "lf" (B.pair text chunks)
    130             _ = lineLoop reader limit (N.subtract remaining count) pending (B.pair text chunks) []
    131           (t, (cause, t)) = lineFailure (N.add (N.subtract limit remaining) count) cause
    132           _ = IO.fail "Invalid line UTF-8 reply")
    133         _ = lineFailure (N.add (N.subtract limit remaining) count)
    134           ["invalid-bound" "text/read-line" "line exceeds byte limit" "none"]
    135     _ = IO.fail "Invalid line cursor bytes")
    136 readLine cursor limit = checkedLimit limit (count : case cursor of
    137   [reader buffered 0] = lineLoop reader count count [] [] buffered
    138   [reader [] 1] = IO.pure (B.ok [["eof"] cursor] t)
    139   _ = IO.pure (B.err ["invalid-argument" "text/read-line" "invalid line cursor" "none"] t))
    140 
    141 -- Generic bounded whole-text convenience. Unlike readSource, initial BOM is
    142 -- ordinary content. It shares the incremental decoder, not the source policy.
    143 readText reader limit = checkedLimit limit (count : IO.onOk
    144   (readLoop reader count count [] 0 [] [])
    145   (received : case received of
    146     (_, text) = IO.pure (B.ok text t)
    147     _ = IO.fail "Invalid text read result"))