tricu

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

text.tri (8415B)

      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 -- Native reads produce proper byte lists. Counting that spine needs no
     73 -- transforming collection contract; raw octets still reach strict UTF-8 decode.
     74 sourceChunkLength [] = 0
     75 sourceChunkLength [_ | rest] = N.successor (sourceChunkLength rest)
     76 sourceChunkLength _ = 0
     77 readLoop reader limit remaining carry first rawChunks textChunks =
     78   IO.bind (IO.readSome reader (readCount remaining)) (received : case received of
     79     ((t t), (("eof", t), t)) = IO.bind (IO.decodeUTF8 1 carry) (decoded : case decoded of
     80       ((t t), ([[] []], t)) = IO.pure (B.ok (B.pair (flatten rawChunks) (flatten textChunks)) t)
     81       (t, (cause, t)) = readFailure (N.subtract limit remaining) cause
     82       _ = IO.fail "Invalid UTF-8 final reply")
     83     ((t t), (("data", bytes), t)) = let count = sourceChunkLength bytes in
     84       case N.lte count remaining of
     85         (t t) = IO.bind (IO.decodeUTF8 0 (B.append carry bytes)) (decoded : case decoded of
     86           ((t t), ([text pending], t)) = case first of
     87             1 = case text of
     88               [] = readLoop reader limit (N.subtract remaining count) pending 1 (B.pair bytes rawChunks) textChunks
     89               [65279 | _] = readFailure (N.add (N.subtract limit remaining) count)
     90                 (problem "text/read-source" "initial source BOM is not permitted" "none")
     91               _ = readLoop reader limit (N.subtract remaining count) pending 0 (B.pair bytes rawChunks) (B.pair text textChunks)
     92             _ = readLoop reader limit (N.subtract remaining count) pending 0 (B.pair bytes rawChunks) (B.pair text textChunks)
     93           (t, (cause, t)) = readFailure (N.add (N.subtract limit remaining) count) cause
     94           _ = IO.fail "Invalid UTF-8 decode reply")
     95         _ = readFailure (N.add (N.subtract limit remaining) count)
     96           ["invalid-bound" "text/read-source" "source exceeds byte limit" "none"]
     97     (t, (cause, t)) = readFailure (N.subtract limit remaining) cause
     98     _ = IO.fail "Invalid source read reply")
     99 readSource reader limit = checkedLimit limit (count : readLoop reader count count [] 1 [] [])
    100 
    101 -- Single-consumer source cursor represented as a source value. Thread the
    102 -- returned cursor forward, serialize its use with all reads on the underlying
    103 -- reader, and retire it on read failure. Read-ahead is bounded to 4093 bytes.
    104 lineCursor reader = [reader [] 0]
    105 
    106 -- The byte budget counts line content; LF delimits lines. CR, BOM and NUL
    107 -- remain content.
    108 -- Scan before decoding: malformed bytes after LF belong to the NEXT line.
    109 lineSplit [] = [[] [] 0]
    110 lineSplit [10 | rest] = [[] rest 1]
    111 lineSplit [byte | rest] = case lineSplit rest of
    112   [prefix after ended] = [(B.pair byte prefix) after ended]
    113   _ = []
    114 lineSplit _ = []
    115 lineFailure consumed cause = IO.pure (B.err ["read-line" consumed cause] t)
    116 lineReady reader after ending chunks = IO.pure
    117   (B.ok [["line" (flatten chunks) ending] [reader after 0]] t)
    118 lineEOF reader consumed carry chunks = IO.bind (IO.decodeUTF8 1 carry) (decoded : case decoded of
    119   ((t t), ([[] []], t)) = case consumed of
    120     0 = IO.pure (B.ok [["eof"] [reader [] 1]] t)
    121     _ = IO.pure (B.ok [["line" (flatten chunks) "eof"] [reader [] 1]] t)
    122   (t, (cause, t)) = lineFailure consumed cause
    123   _ = IO.fail "Invalid line final UTF-8 reply")
    124 lineLoop reader limit remaining carry chunks buffered = forceCount remaining (_ : case buffered of
    125   [] = IO.bind (IO.readSome reader 4093) (received : case received of
    126     ((t t), (("eof", t), t)) = lineEOF reader (N.subtract limit remaining) carry chunks
    127     ((t t), (("data", bytes), t)) = lineLoop reader limit remaining carry chunks bytes
    128     (t, (cause, t)) = lineFailure (N.subtract limit remaining) cause
    129     _ = IO.fail "Invalid line read reply")
    130   _ = case lineSplit buffered of
    131     [part after ended] = let count = B.length part in
    132       case N.lte count remaining of
    133         (t t) = IO.bind (IO.decodeUTF8 ended (B.append carry part)) (decoded : case decoded of
    134           ((t t), ([text pending], t)) = case ended of
    135             1 = lineReady reader after "lf" (B.pair text chunks)
    136             _ = lineLoop reader limit (N.subtract remaining count) pending (B.pair text chunks) []
    137           (t, (cause, t)) = lineFailure (N.add (N.subtract limit remaining) count) cause
    138           _ = IO.fail "Invalid line UTF-8 reply")
    139         _ = lineFailure (N.add (N.subtract limit remaining) count)
    140           ["invalid-bound" "text/read-line" "line exceeds byte limit" "none"]
    141     _ = IO.fail "Invalid line cursor bytes")
    142 readLine cursor limit = checkedLimit limit (count : case cursor of
    143   [reader buffered 0] = lineLoop reader count count [] [] buffered
    144   [reader [] 1] = IO.pure (B.ok [["eof"] cursor] t)
    145   _ = IO.pure (B.err ["invalid-argument" "text/read-line" "invalid line cursor" "none"] t))
    146 
    147 -- Generic bounded whole-text convenience preserving an initial BOM as content.
    148 -- It uses the shared incremental decoder with this text policy.
    149 readText reader limit = checkedLimit limit (count : IO.onOk
    150   (readLoop reader count count [] 0 [] [])
    151   (received : case received of
    152     (_, text) = IO.pure (B.ok text t)
    153     _ = IO.fail "Invalid text read result"))