0 | ||| Utilities for working with streams of byte arrays.
  1 | module FS.Bytes
  2 |
  3 | import public Data.ByteString
  4 |
  5 | import Data.Buffer.Mutable
  6 | import FS.Internal.Bytes
  7 | import FS.Chunk
  8 | import FS.Pull
  9 |
 10 | %default total
 11 |
 12 | nebs : ByteString -> Maybe ByteString
 13 | nebs (BS 0 _) = Nothing
 14 | nebs bs       = Just bs
 15 |
 16 | export %inline
 17 | emitBS : ByteString -> Pull f ByteString es ()
 18 | emitBS (BS 0 _) = pure ()
 19 | emitBS bs       = emit bs
 20 |
 21 | export %inline
 22 | consBS : ByteString -> Pull f ByteString es r -> Pull f ByteString es r
 23 | consBS (BS 0 _) p = p
 24 | consBS bs       p = cons bs p
 25 |
 26 | ||| Appends a newline character (`0x0a`) to every bytestring
 27 | ||| emitted by the stream.
 28 | |||
 29 | ||| A chunk (list) of bytestring is thus concatenated to a single
 30 | ||| byte vector. See also `lines`.
 31 | export
 32 | unlines : Pull f (List ByteString) es r -> Pull f ByteString es r
 33 | unlines = mapOutput (\cs => fastConcat $ cs >>= \b => [b,nl])
 34 |
 35 | ||| Breaks the bytes emitted by a byte stream along unix newline
 36 | ||| characters (`0x0a`).
 37 | |||
 38 | ||| For reasons of efficiency, this emits the produce lines as
 39 | ||| a list of bytestrings.
 40 | export
 41 | lines : Pull f ByteString es r -> Pull f (List ByteString) es r
 42 | lines = scanFull empty splitNL (map pure . nonEmpty)
 43 |
 44 | ||| Breaks the chunks emitted by a byte stream along the last
 45 | ||| unix new-line character (`0x0a`) of each chunk.
 46 | export
 47 | breakNL : Pull f ByteString es r -> Pull f ByteString es r
 48 | breakNL = scanFull empty breakLastNL nonEmpty
 49 |
 50 | ||| Breaks the output generated by a pull at the first occurence
 51 | ||| of the given byte sequence.
 52 | |||
 53 | ||| The substring is removed from the emitted byte sequence,
 54 | ||| and the remainder of the pull returned (if any).
 55 | export
 56 | breakAtSubstring :
 57 |      (orElse : r -> Pull f ByteString es r)
 58 |   -> ByteString
 59 |   -> Pull f ByteString es r
 60 |   -> Pull f ByteString es (Pull f ByteString es r)
 61 | breakAtSubstring orElse ss = go empty
 62 |   where
 63 |     go :
 64 |          ByteString
 65 |       -> Pull f ByteString es r
 66 |       -> Pull f ByteString es (Pull f ByteString es r)
 67 |     go pre p =
 68 |       assert_total $ uncons p >>= \case
 69 |         Left v        => consBS pre (pure $ orElse v)
 70 |         Right (cur,q) => case breakAtSS ss (pre <+> cur) of
 71 |           TooShort x => go x q
 72 |           NoSS x y   => consBS x (go y q)
 73 |           SS   x y   => consBS x (pure $ emitBS y >> q)
 74 |
 75 | ||| Like `breakAtSubstring` but fails with the given error if
 76 | ||| the substring is not encountered.
 77 | export %inline
 78 | forceBreakAtSubstring :
 79 |      {auto has : Has e es}
 80 |   -> Lazy e
 81 |   -> ByteString
 82 |   -> Pull f ByteString es r
 83 |   -> Pull f ByteString es (Pull f ByteString es r)
 84 | forceBreakAtSubstring err = breakAtSubstring (const $ throw err)
 85 |
 86 | namespace UTF8
 87 |   ||| Converts the byte vectors emitted by a stream to byte vectors
 88 |   ||| that always end at whole code points.
 89 |   |||
 90 |   ||| Note: Typically, this needs to be prefixed with the outer namespace:
 91 |   |||       `UTF8.chunks`
 92 |   export
 93 |   chunks : Stream f es ByteString -> Stream f es ByteString
 94 |   chunks = scanFull empty UTF8.breakAtLastIncomplete nonEmpty
 95 |
 96 |   ||| Cuts the byte vectors emitted by a stream at the end of whole
 97 |   ||| UTF-8 code points and converts them to `String`s.
 98 |   |||
 99 |   ||| Note: Typically, this needs to be prefixed with the outer namespace:
100 |   |||       `UTF8.decode`
101 |   export %inline
102 |   decode : Stream f es ByteString -> Stream f es String
103 |   decode = mapOutput toString . UTF8.chunks
104 |
105 |   ||| Converts a stream of strings to UTF-8-encoded byte strings.
106 |   |||
107 |   ||| Note: Typically, this needs to be prefixed with the outer namespace:
108 |   |||       `UTF8.encode`
109 |   export %inline
110 |   encode : Stream f es String -> Stream f es ByteString
111 |   encode = mapOutput fromString
112 |
113 | --------------------------------------------------------------------------------
114 | -- Chunk Implementation
115 | --------------------------------------------------------------------------------
116 |
117 | breakImpl : BreakInstruction -> (Bits8 -> Bool) -> ByteString -> BreakRes ByteString
118 | breakImpl x f bs =
119 |   case break f bs of
120 |     (pre, BS 0 _)      => Keep pre
121 |     (pre, pst@(BS (S k) bv)) => case x of
122 |       PostHit => Broken (nebs pre) (Just pst)
123 |       DropHit => Broken (nebs pre) (nebs $ BS k (tail bv))
124 |       TakeHit =>
125 |         let len := S pre.size
126 |          in Broken (Just $ take len bs) (nebs $ drop len bs)
127 |
128 | splitImpl : Nat -> ByteString -> SplitRes ByteString
129 | splitImpl k bs =
130 |   case splitAt k bs of
131 |     Nothing         => All (k `minus` size bs)
132 |     Just (pre,post) =>
133 |       let Just y := nebs post | Nothing => All (k `minus` size pre)
134 |        in Middle pre y
135 |
136 | unfoldImpl :
137 |      {n : _}
138 |   -> (st -> Either r (Bits8,st))
139 |   -> st
140 |   -> MBuffer s n
141 |   -> (k : Nat)
142 |   -> {auto ix : Ix k n}
143 |   -> F1 s (UnfoldRes r st ByteString)
144 | unfoldImpl f cur buf 0 t =
145 |   let ibuf # t := unsafeFreeze buf t
146 |    in More (fromIBuffer ibuf) cur # t
147 | unfoldImpl f cur buf (S k) t =
148 |   case f cur of
149 |     Right (v,nxt) =>
150 |       let _ # t := setIx buf k v t
151 |        in unfoldImpl f nxt buf k t
152 |     Left  x =>
153 |       let ibuf # t := unsafeFreezeLTE buf (ixToNat ix) @{ixLTE ix} t
154 |        in case nebs (fromIBuffer ibuf) of
155 |             Nothing => Done x # t
156 |             Just bs => Last x bs # t
157 |
158 | export
159 | Chunk ByteString Bits8 where
160 |   filterChunk pred = nebs . filter pred
161 |
162 |   breakChunk = breakImpl
163 |
164 |   splitChunkAt = splitImpl
165 |
166 |   unconsChunk (BS (S k) bv) = Just (at bv 0, nebs (BS k $ tail bv))
167 |   unconsChunk _             = Nothing
168 |
169 |   isEmpty (BS 0 _) = True
170 |   isEmpty _        = False
171 |
172 |   replicateChunk @{CS n} v = replicate n v
173 |
174 |   unfoldChunk @{CS n} f ini = alloc n (\buf => unfoldImpl f ini buf n)
175 |