0 | module Data.ByteVect
  1 |
  2 | import Data.Maybe0
  3 | import Control.WellFounded
  4 | import Data.Buffer
  5 | import Data.Buffer.Builder
  6 | import Data.Buffer.Mutable
  7 | import Data.Nat.BSExtra
  8 |
  9 | import public Data.Buffer.Core
 10 | import public Data.Buffer.Indexed
 11 | import public Data.Byte
 12 |
 13 | %default total
 14 |
 15 | ||| An immutable, length-indexed byte vector.
 16 | |||
 17 | ||| Internally represented by a `Data.Buffer` together
 18 | ||| with its length and offset.
 19 | |||
 20 | ||| The internal buffer is treated as being immutable,
 21 | ||| so operations modifying a `ByteVect` will create
 22 | ||| and write to a new `Buffer`.
 23 | public export
 24 | data ByteVect : Nat -> Type where
 25 |   BV :  (buf    : IBuffer bufLen)
 26 |      -> (offset : Nat)
 27 |      -> (0 lte  : LTE (offset + len) bufLen)
 28 |      -> ByteVect len
 29 |
 30 | ||| Wrappes an immutable buffer in a `ByteVect`
 31 | export %inline
 32 | fromIBuffer : IBuffer n -> ByteVect n
 33 | fromIBuffer b = BV b 0 reflexive
 34 |
 35 | ||| An immutable string of raw bytes. For an length-indexed version,
 36 | ||| see module `ByteVect` and `Data.ByteVect`.
 37 | public export
 38 | record ByteString where
 39 |   constructor BS
 40 |   size : Nat
 41 |   repr : ByteVect size
 42 |
 43 | %inline
 44 | conv : {n : _} -> R1 rs (IBuffer n) -@ R1 rs ByteString
 45 | conv (v # t) = BS n (BV v 0 reflexive) # t
 46 |
 47 | ||| Safely wrap a mutable buffer in a `ByteString`.
 48 | export
 49 | freezeByteString : {n : _} -> WithMBuffer n ByteString
 50 | freezeByteString r t = conv $ freeze r t
 51 |
 52 | ||| Wrap a mutable buffer in a `ByteString` without copying.
 53 | |||
 54 | ||| Use this for reasons of efficiency when you are sure the buffer
 55 | ||| will not be shared otherwise.
 56 | export
 57 | unsafeFreezeByteString : {n : _} -> WithMBuffer n ByteString
 58 | unsafeFreezeByteString r t = conv $ unsafeFreeze r t
 59 |
 60 | ||| Safely wrap a mutable buffer in a `ByteString`.
 61 | export
 62 | freezeByteStringLTE : (m : Nat) -> (0 p : LTE m n) => WithMBuffer n ByteString
 63 | freezeByteStringLTE m r t = conv $ freezeLTE @{p} r m t
 64 |
 65 | ||| Wrap a mutable buffer in a `ByteString` without copying.
 66 | |||
 67 | ||| Use this for reasons of efficiency when you are sure the buffer
 68 | ||| will not be shared otherwise.
 69 | export
 70 | unsafeFreezeByteStringLTE : (m : Nat) -> (0 p : LTE m n) => WithMBuffer n ByteString
 71 | unsafeFreezeByteStringLTE m r t = conv $ unsafeFreezeLTE @{p} r m t
 72 |
 73 | ||| Reads the value of a `ByteVect` at the given position
 74 | export %inline
 75 | at : ByteVect n -> Fin n -> Bits8
 76 | at (BV buf o lte) x = atOffset buf x o
 77 |
 78 | ||| Safely access a value in an array at position `n - m`.
 79 | export %inline
 80 | ix : ByteVect n -> (0 m : Nat) -> {auto x: Ix (S m) n} -> Bits8
 81 | ix bv _ = at bv (ixToFin x)
 82 |
 83 | ||| Safely access a value in an array at the given position.
 84 | export %inline
 85 | atNat : ByteVect n -> (m : Nat) -> {auto 0 lt : LT m n} -> Bits8
 86 | atNat bv x = at bv (natToFinLT x)
 87 |
 88 | export
 89 | fromEnd : {n : _} -> ByteVect n -> (m : Nat) -> {auto 0 lt : LT m n} -> Bits8
 90 | fromEnd bs m = atNat bs (n `minus` S m) @{minusLT _ _ lt}
 91 |
 92 | --------------------------------------------------------------------------------
 93 | --          Making ByteStrings
 94 | --------------------------------------------------------------------------------
 95 |
 96 | ||| The empty `ByteVect`.
 97 | export
 98 | empty : ByteVect 0
 99 | empty = BV empty 0 %search
100 |
101 | ||| Converts a list of values to a `ByteVect` using
102 | ||| the given conversion function. O(n).
103 | export
104 | pack : (as : List Bits8) -> ByteVect (length as)
105 | pack as = BV (bufferL as) 0 reflexive
106 |
107 | ||| Converts a `String` to a `ByteVect`. Note: This will
108 | ||| correctly decode the corresponding UTF-8 string.
109 | export
110 | fromString : (s : String) -> ByteVect (cast $ stringByteLength s)
111 | fromString s = BV (fromString s) 0 reflexive
112 |
113 | ||| Converts a `ByteVect` to a UTF-8 encoded string
114 | export
115 | toString : {n : _} -> ByteVect n -> String
116 | toString (BV buf o _) = toString buf o n
117 |
118 | export %inline
119 | {n : _} -> Interpolation (ByteVect n) where interpolate = toString
120 |
121 | ||| Creates a `ByteVect` holding a single `Bits8` value.
122 | export %inline
123 | singleton : Bits8 -> ByteVect 1
124 | singleton v = pack [v]
125 |
126 | ||| Convert a `ByteVect` to a list of values using
127 | ||| the given conversion function.
128 | export
129 | toList : {n : _} -> (Bits8 -> a) -> ByteVect n -> List a
130 | toList f bs     = go Nil n
131 |
132 |   where
133 |     go : List a -> (x : Nat) -> (0 prf : LTE x n) => List a
134 |     go xs 0     = xs
135 |     go xs (S j) = go (f (atNat bs j) :: xs) j
136 |
137 | ||| Converts a `ByteVect` to a list of `Bits8` values. O(n).
138 | export %inline
139 | unpack : {n : _} -> ByteVect n -> List Bits8
140 | unpack = toList id
141 |
142 | ||| Converts a `ByteVect` to a String. All characters
143 | ||| will be in the range [0,255], so this does not perform
144 | ||| any character decoding.
145 | export %inline
146 | {n : Nat} -> Show (ByteVect n) where
147 |   showPrec p bs = showCon p "pack" (showArg $ toList id bs)
148 |
149 | --------------------------------------------------------------------------------
150 | --          Comparing ByteStrings
151 | --------------------------------------------------------------------------------
152 |
153 | ||| Lexicographic comparison of `ByteVect`s of distinct length
154 | export
155 | hcomp : {m,n : Nat} -> ByteVect m -> ByteVect n -> Ordering
156 | hcomp b1 b2 = go m n
157 |
158 |   where
159 |     go : (k,l : Nat) -> {auto a1 : Ix k m} -> {auto a2 : Ix l n} -> Ordering
160 |     go 0     0     = EQ
161 |     go 0     (S _) = LT
162 |     go (S _) 0     = GT
163 |     go (S k) (S j) = case compare (ix b1 k) (ix b2 j) of
164 |       EQ => go k j
165 |       r  => r
166 |
167 | ||| Heterogeneous equality for `ByteVect`s
168 | export
169 | heq : {m,n : Nat} -> ByteVect m -> ByteVect n -> Bool
170 | heq bs1 bs2 = hcomp bs1 bs2 == EQ
171 |
172 | --------------------------------------------------------------------------------
173 | --          Core Functionality
174 | --------------------------------------------------------------------------------
175 |
176 | export
177 | generate : (n : Nat) -> (Fin n -> Bits8) -> ByteVect n
178 | generate n f = BV (generate n f) 0 refl
179 |
180 | export
181 | replicate : (n : Nat) -> Bits8 -> ByteVect n
182 | replicate n = generate n . const
183 |
184 | --------------------------------------------------------------------------------
185 | --          Concatenating ByteStrings
186 | --------------------------------------------------------------------------------
187 |
188 | ||| Concatenate two `ByteVect`s. O(n + m).
189 | export
190 | append : {m,n : _} -> ByteVect m -> ByteVect n -> ByteVect (m + n)
191 | append (BV src1 o1 lte1) (BV src2 o2 lte2) =
192 |   let buf := alloc (m+n) $ \r,t =>
193 |               let _ # t := icopy {n = m+n} src1 o1 0 m @{lte1} @{lteAddRight _} r t
194 |                   _ # t := icopy src2 o2 m n @{lte2} @{reflexive} r t
195 |                in unsafeFreeze r t
196 |    in BV buf 0 reflexive
197 |
198 | ||| Prepend a single `Bits8` to a `ByteVect`. O(n).
199 | export %inline
200 | cons : {n : _} -> Bits8 -> ByteVect n -> ByteVect (S n)
201 | cons = append . singleton
202 |
203 | ||| Append a single `Bits8` to a `ByteVect`. O(n).
204 | export %inline
205 | snoc : {n : _} -> Bits8 -> ByteVect n -> ByteVect (n + 1)
206 | snoc w bs = bs `append` singleton w
207 |
208 | --------------------------------------------------------------------------------
209 | --          Inspecting ByteStrings
210 | --------------------------------------------------------------------------------
211 |
212 | ||| Read the first element of a `ByteVect`. O(1).
213 | export
214 | head : ByteVect (S n) -> Bits8
215 | head bv = atNat bv 0
216 |
217 | ||| Drop the first `Bits8` from a `ByteVect`. O(1).
218 | export
219 | tail : ByteVect (S n) -> ByteVect n
220 | tail (BV buf o p) = BV buf (S o) (ltePlusSuccRight p)
221 |
222 | ||| Split the first `Bits8` from a `ByteVect`. O(1).
223 | export
224 | uncons : ByteVect (S n) -> (Bits8, ByteVect n)
225 | uncons bs = (head bs, tail bs)
226 |
227 | ||| Read the last `Bits8` from a `ByteVect`. O(1).
228 | export
229 | last : {n : _} -> ByteVect (S n) -> Bits8
230 | last bs = atNat bs n
231 |
232 | ||| Drop the last `Bits8` from a `ByteVect`. O(1).
233 | export
234 | init : ByteVect (S n) -> ByteVect n
235 | init (BV buf o p) = BV buf o (lteSuccLeft $ ltePlusSuccRight p)
236 |
237 | ||| Split a `ByteVect` at the last byte. O(1).
238 | export
239 | unsnoc : {n : _} -> ByteVect (S n) -> (Bits8, ByteVect n)
240 | unsnoc bs = (last bs, init bs)
241 |
242 | --------------------------------------------------------------------------------
243 | --          Mapping ByteStrings
244 | --------------------------------------------------------------------------------
245 |
246 | ||| Converts every `Bits8` in a `ByteVect` by applying the given
247 | ||| function. O(n).
248 | export
249 | map : {n : _} -> (Bits8 -> Bits8) -> ByteVect n -> ByteVect n
250 | map f bs = generate n (\x => f $ at bs x)
251 |
252 | ||| Interpreting the values stored in a `ByteVect` as 8 bit characters,
253 | ||| convert every lower-case character to its upper-case form. O(n)
254 | export %inline
255 | toUpper : {n : _} -> ByteVect n -> ByteVect n
256 | toUpper = map toUpper
257 |
258 | ||| Interpreting the values stored in a `ByteVect` as 8 bit characters,
259 | ||| convert every upper-case character to its lower-case form. O(n)
260 | export %inline
261 | toLower : {n : _} -> ByteVect n -> ByteVect n
262 | toLower = map toLower
263 |
264 | ||| Inverse the order of bytes in a `ByteVect`. O(n)
265 | export
266 | reverse : {n : _} -> ByteVect n -> ByteVect n
267 | reverse bs = generate n (\x => fromEnd bs (finToNat x) @{finToNatLT _})
268 |
269 | ||| True, if the predicate holds for all bytes
270 | ||| in the given `ByteVect`. O(n)
271 | export
272 | all : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> Bool
273 | all p bv = go n
274 |
275 |   where
276 |     go : (c : Nat) -> (x : Ix c n) => Bool
277 |     go 0     = True
278 |     go (S k) = if p (ix bv k) then go k else False
279 |
280 | ||| True, if the predicate holds for at least one byte
281 | ||| in the given `ByteVect`. O(n)
282 | export
283 | any : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> Bool
284 | any p bv = go n
285 |
286 |   where
287 |     go : (c : Nat) -> (x : Ix c n) => Bool
288 |     go 0     = False
289 |     go (S k) = if p (ix bv k) then True else go k
290 |
291 | ||| True, if the given `Bits8` appears in the `ByteVect`. O(n)
292 | export %inline
293 | elem : {n : _} -> Bits8 -> ByteVect n -> Bool
294 | elem b = any (b ==)
295 |
296 | ||| Fold a `ByteVect` from the left. O(n)
297 | export
298 | foldl : {n : _} -> (a -> Bits8 -> a) -> a -> ByteVect n -> a
299 | foldl f ini bv = go n ini
300 |
301 |   where
302 |     go : (c : Nat) -> (v : a) -> (x : Ix c n) => a
303 |     go 0     v = v
304 |     go (S k) v = go k (f v $ ix bv k)
305 |
306 | ||| Fold a `ByteVect` from the right. O(n)
307 | export
308 | foldr : {n : _} -> (Bits8 -> a -> a) -> a -> ByteVect n -> a
309 | foldr f ini bs = go n ini
310 |
311 |   where
312 |     go : (k : Nat) -> (v : a) -> (0 lt : LTE k n) => a
313 |     go 0     v = v
314 |     go (S k) v = go k (f (atNat bs k) v)
315 |
316 | ||| The `findIndex` function takes a predicate and a `ByteVect` and
317 | ||| returns the index of the first element in the ByteVect
318 | ||| satisfying the predicate. O(n)
319 | export
320 | findIndex : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> Maybe (Fin n)
321 | findIndex p bv = go n
322 |
323 |   where
324 |     go : (c : Nat) -> {auto x : Ix c n} -> Maybe (Fin n)
325 |     go 0     = Nothing
326 |     go (S k) = if p (ix bv k) then Just (ixToFin x) else go k
327 |
328 | ||| Return the index of the first occurence of the given
329 | ||| byte in the `ByteVect`, or `Nothing`, if the byte
330 | ||| does not appear in the ByteVect. O(n)
331 | export
332 | elemIndex : {n : _} -> Bits8 -> ByteVect n -> Maybe (Fin n)
333 | elemIndex c = findIndex (c ==)
334 |
335 | ||| Returns the first value byte in a `ByteVect` fulfilling
336 | ||| the given predicate. O(n)
337 | export
338 | find : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> Maybe Bits8
339 | find p bs = at bs <$> findIndex p bs
340 |
341 | export
342 | isPrefixOf : {m,n : _} -> ByteVect m -> ByteVect n -> Bool
343 | isPrefixOf bv1 bv2 = go m n
344 |
345 |   where
346 |     go : (c1,c2 : Nat) -> {auto _ : Ix c1 m} -> {auto _ : Ix c2 n} -> Bool
347 |     go 0     _     = True
348 |     go _     0     = False
349 |     go (S x) (S y) = if ix bv1 x == ix bv2 y then go x y else False
350 |
351 | export
352 | isSuffixOf : {m,n : _} -> ByteVect m -> ByteVect n -> Bool
353 | isSuffixOf bv1 bv2 = go m n
354 |
355 |   where
356 |     go : (o1,o2 : Nat) -> (0 _ : LTE o1 m) => (0 _ : LTE o2 n) => Bool
357 |     go 0     _     = True
358 |     go _     0     = False
359 |     go (S x) (S y) = if atNat bv1 x == atNat bv2 y then go x y else False
360 |
361 | --------------------------------------------------------------------------------
362 | --          Substrings
363 | --------------------------------------------------------------------------------
364 |
365 | findIndexOrLength : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> SubLength n
366 | findIndexOrLength p bv = go n
367 |
368 |   where
369 |     go : (c : Nat) -> {auto x : Ix c n} -> SubLength n
370 |     go 0     = fromIx x
371 |     go (S k) = if p (ix bv k) then fromIx x else go k
372 |
373 | findIndexOrLengthNL : {n : _} -> ByteVect n -> SubLength n
374 | findIndexOrLengthNL bv = go n
375 |
376 |   where
377 |     go : (c : Nat) -> {auto x : Ix c n} -> SubLength n
378 |     go 0     = fromIx x
379 |     go (S k) = case ix bv k of 10 => fromIx x; _ => go k
380 |
381 | findFromEndUntil : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> SubLength n
382 | findFromEndUntil p bv = go n
383 |
384 |   where
385 |     go : (k : Nat) -> (0 lt : LTE k n) => SubLength n
386 |     go 0     = Element 0 LTEZero
387 |     go (S k) = if p (atNat bv k) then (Element (S k) lt) else go k
388 |
389 | 0 substrPrf : LTE (s + l) n -> LTE (o + n) n2 -> LTE ((o + s) + l) n2
390 | substrPrf p q =
391 |   let pp := rewrite sym (plusAssociative o s l) in ltePlusRight o p
392 |    in transitive pp q
393 |
394 | ||| Like `substr` for `String`, this extracts a substring
395 | ||| of the given `ByteVect` at the given start position
396 | ||| and of the given length. O(1).
397 | export %inline
398 | substring :
399 |      (start,length : Nat)
400 |   -> ByteVect n
401 |   -> {auto 0 inBounds : LTE (start + length) n}
402 |   -> ByteVect length
403 | -- inBounds : start + len       <= n
404 | -- p        : o + n             <= bufLen
405 | -- required : (o + start) + len <= bufLen
406 | substring start len (BV buf o p) =
407 |   BV buf (o + start) (substrPrf inBounds p)
408 |
409 | ||| Like `substring` but extracts a substring from position
410 | ||| `from` up to but not including position `till`.
411 | export
412 | substringFromTill :
413 |      (from, till : Nat)
414 |   -> {auto 0 lt1 : LTE from till}
415 |   -> {auto 0 lt2 : LTE till n}
416 |   -> ByteVect n
417 |   -> ByteVect (till `minus` from)
418 | substringFromTill f t bv =
419 |   substring f (t `minus` f) bv @{transitive (plusMinusLTE _ _ lt1) lt2}
420 |
421 | ||| Like `substring` but extracts a substring from position
422 | ||| `from` up to and including position `to`.
423 | export
424 | substringFromTo :
425 |      (from, to : Nat)
426 |   -> {auto 0 lte : LTE from to}
427 |   -> {auto 0 lt  : LT to n}
428 |   -> ByteVect n
429 |   -> ByteVect (S to `minus` from)
430 | substringFromTo f t bv = substringFromTill f (S t) bv
431 |
432 | export
433 | generateMaybe : (n : Nat) -> (Fin n -> Maybe Bits8) -> ByteString
434 | generateMaybe n f = alloc n (go n n)
435 |
436 |   where
437 |     go : (k,m : Nat) -> (x : Ix k n) => (y : Ix m n) => WithMBuffer n ByteString
438 |     go (S k) (S m) r t =
439 |       case f (ixToFin x) of
440 |         Nothing => go k (S m) r t
441 |         Just v  => let _ # t := setIx r m v t in go k m r t
442 |     go _ _ r t = unsafeFreezeByteStringLTE (ixToNat y) @{ixLTE y} r t
443 |
444 | export
445 | mapMaybe : {n : _} -> (Bits8 -> Maybe Bits8) -> ByteVect n -> ByteString
446 | mapMaybe f bv = generateMaybe n (f . at bv)
447 |
448 | export
449 | filter : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> ByteString
450 | filter p = mapMaybe (\b => if p b then Just b else Nothing)
451 |
452 | ||| Return a `ByteVect` with the first `n` values of
453 | ||| the input string. O(1)
454 | export
455 | take : (0 k : Nat) -> (0 lt : LTE k n) => ByteVect n -> ByteVect k
456 | take k (BV buf o p) =
457 |   -- p        : o + n <= bufLen
458 |   -- lt       : k     <= n
459 |   -- required : o + k <= bufLen
460 |   BV buf o (transitive (ltePlusRight o lt) p)
461 |
462 | ||| Return a `ByteVect` with the last `n` values of
463 | ||| the input string. O(1)
464 | export
465 | takeEnd :
466 |      {n : _}
467 |   -> (k : Nat)
468 |   -> {auto 0 lt : LTE k n}
469 |   -> ByteVect n
470 |   -> ByteVect k
471 | takeEnd k (BV buf o p) =
472 |   -- p        : o + n             <= bufLen
473 |   -- lt       : k                 <= n
474 |   -- required : ((o + n) - k) + k <= bufLen
475 |   let 0 q := plusMinus' k (o + n) (lteAddLeft o lt)
476 |    in BV buf ((o + n) `minus` k) (rewrite q in p)
477 |
478 | ||| Remove the first `n` values from a `ByteVect`. O(1)
479 | export
480 | drop : (k : Nat) -> (0 lt : LTE k n) => ByteVect n -> ByteVect (n `minus` k)
481 | drop k (BV buf o p) =
482 |   -- p        : o + n             <= bufLen
483 |   -- lt       : k                 <= n
484 |   -- required : (o + k) + (n - k) <= bufLen
485 |   let 0 q := cong (o +) (plusMinus k n lt)
486 |       0 r := plusAssociative o k (n `minus` k)
487 |    in BV buf (o + k) (rewrite (trans (sym r) q) in p)
488 |
489 | ||| Remove the last `n` values from a `ByteVect`. O(1)
490 | export
491 | dropEnd :
492 |      (0 k : Nat)
493 |   -> {auto 0 lt : LTE k n}
494 |   -> ByteVect n
495 |   -> ByteVect (n `minus` k)
496 | dropEnd k (BV buf o p) =
497 |   -- p        : o + n       <= bufLen
498 |   -- lt       : k           <= n
499 |   -- required : o + (n - k) <= bufLen
500 |   BV buf o (transitive (ltePlusRight o $ minusLTE n k) p)
501 |
502 | export
503 | splitAt :
504 |      {n : _}
505 |   -> (k : Nat)
506 |   -> {auto 0 lte : LTE k n}
507 |   -> ByteVect n
508 |   -> (ByteVect k, ByteVect (n `minus` k))
509 | splitAt k bs = (take k bs, drop k bs)
510 |
511 | ||| Extracts the longest prefix of elements satisfying the
512 | ||| predicate.
513 | export
514 | takeWhile : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> ByteString
515 | takeWhile p bs =
516 |   let Element k _ = findIndexOrLength (not . p) bs
517 |    in BS k $ take k bs
518 |
519 | ||| Returns the longest (possibly empty) suffix of elements
520 | ||| satisfying the predicate.
521 | export
522 | takeWhileEnd : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> ByteString
523 | takeWhileEnd f bs =
524 |   let Element k _ = findFromEndUntil (not . f) bs
525 |    in BS _ $ drop k bs
526 |
527 | ||| Drops the longest (possibly empty) prefix of elements
528 | ||| satisfying the predicate and returns the remainder.
529 | export
530 | dropWhile : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> ByteString
531 | dropWhile f bs =
532 |   let Element k _ = findIndexOrLength (not . f) bs
533 |    in BS _ $ drop k bs
534 |
535 | ||| Drops the longest (possibly empty) suffix of elements
536 | ||| satisfying the predicate and returns the remainder.
537 | export
538 | dropWhileEnd : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> ByteString
539 | dropWhileEnd f bs =
540 |   let Element k _ = findFromEndUntil (not . f) bs
541 |    in BS k $ take k bs
542 |
543 | ||| Remove leading whitespace from a `ByteString`
544 | export
545 | trimLeft : {n : _} -> ByteVect n -> ByteString
546 | trimLeft = dropWhile isSpace
547 |
548 | ||| Remove trailing whitespace from a `ByteString`
549 | export
550 | trimRight : {n : _} -> ByteVect n -> ByteString
551 | trimRight = dropWhileEnd isSpace
552 |
553 | ||| Remove all leading and trailing whitespace from a `ByteString`
554 | export
555 | trim : {n : _} -> ByteVect n -> ByteString
556 | trim bs = let BS k bs' := trimLeft bs in trimRight bs'
557 |
558 | public export
559 | record BreakRes (n : Nat) where
560 |   constructor MkBreakRes
561 |   lenFst : Nat
562 |   lenSnd : Nat
563 |   fst    : ByteVect lenFst
564 |   snd    : ByteVect lenSnd
565 |   0 prf  : LTE (lenFst + lenSnd) n
566 |
567 | export
568 | breakRes : {n : _} -> ByteVect n -> SubLength n -> BreakRes n
569 | breakRes bs (Element k p) =
570 |   let bs1 := take k bs
571 |       bs2 := drop k bs
572 |    in MkBreakRes k (n `minus` k) bs1 bs2 (plusMinusLTE k n p)
573 |
574 | ||| Returns the longest (possibly empty) prefix of elements which do not
575 | ||| satisfy the predicate and the remainder of the string.
576 | export %inline
577 | break : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> BreakRes n
578 | break p bs = breakRes bs (findIndexOrLength p bs)
579 |
580 | ||| Returns the longest (possibly empty) prefix before the first newline character
581 | export %inline
582 | breakNL : {n : _} -> ByteVect n -> BreakRes n
583 | breakNL bs = breakRes bs (findIndexOrLengthNL bs)
584 |
585 | ||| Returns the longest (possibly empty) suffix of elements which do not
586 | ||| satisfy the predicate and the remainder of the string.
587 | export %inline
588 | breakEnd : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> BreakRes n
589 | breakEnd  p bs = breakRes bs (findFromEndUntil p bs)
590 |
591 | ||| Returns the longest (possibly empty) prefix of elements
592 | ||| satisfying the predicate and the remainder of the string.
593 | export %inline
594 | span : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> BreakRes n
595 | span p = break (not . p)
596 |
597 | ||| Returns the longest (possibly empty) suffix of elements
598 | ||| satisfying the predicate and the remainder of the string.
599 | export %inline
600 | spanEnd : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> BreakRes n
601 | spanEnd p bs = breakRes bs (findFromEndUntil (not . p) bs)
602 |
603 | ||| Returns the index where the given substring occurs in the
604 | ||| given bytevector for the first time
605 | export
606 | substringIndex : {k,n : _} -> ByteVect k -> ByteVect n -> SubLength n
607 | substringIndex sep bv = go n
608 |
609 |   where
610 |     go : (c : Nat) -> {auto x : Ix c n} -> SubLength n
611 |     go 0     = fromIx x
612 |     go (S k) =
613 |       if isPrefixOf sep (drop (ixToNat x) @{ixLTE x} bv) then fromIx x else go k
614 |
615 | ||| Returns the longest (possibly empty) prefix of a
616 | ||| byte vector that does not contain the given substring
617 | ||| plus the remainder of the byte vector.
618 | export %inline
619 | breakAtSubstring : {k,n : _} -> ByteVect k -> ByteVect n -> BreakRes n
620 | breakAtSubstring sep bs = breakRes bs (substringIndex sep bs)
621 |
622 | ||| Splits a 'ByteVect' into components delimited by
623 | ||| separators, where the predicate returns True for a separator element.
624 | ||| The resulting components do not contain the separators. Two adjacent
625 | ||| separators result in an empty component in the output. eg.
626 | export
627 | splitWith : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> List ByteString
628 | splitWith p bs = go Lin n bs (sizeAccessible n)
629 |
630 |   where
631 |     go :
632 |          SnocList ByteString
633 |       -> (m : Nat)
634 |       -> ByteVect m
635 |       -> (0 acc : SizeAccessible m)
636 |       -> List ByteString
637 |     go sb m bs' (Access rec) = case break p bs' of
638 |       MkBreakRes l1 0      b1 _  p => sb <>> [BS l1 b1]
639 |       MkBreakRes l1 (S l2) b1 b2 p =>
640 |         go (sb :< BS l1 b1) l2 (tail b2) (rec l2 $ ltPlusSuccRight' _ p)
641 |
642 | ||| Like `splitWith`, but removes empty components.
643 | export
644 | splitWithNonEmpty : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> List ByteString
645 | splitWithNonEmpty p = filter ((/= Z) . size) . splitWith p
646 |
647 | ||| Break a `ByteVect` into pieces separated by the byte
648 | ||| argument, consuming the delimiter.
649 | |||
650 | ||| As for all splitting functions in this library, this function does
651 | ||| not copy the substrings, it just constructs new `ByteString`s that
652 | ||| are slices of the original.
653 | export %inline
654 | split : {n : _} -> Bits8 -> ByteVect n -> List ByteString
655 | split b = splitWith (b ==)
656 |
657 | ||| Like `split`, but removes empty components.
658 | export
659 | splitNonEmpty : {n : _} -> Bits8 -> ByteVect n -> List ByteString
660 | splitNonEmpty p = filter ((/= Z) . size) . split p
661 |
662 | export
663 | lines : {n : _} -> ByteVect n -> List ByteString
664 | lines bs = go Lin n bs (sizeAccessible n)
665 |
666 |   where
667 |     go :
668 |          SnocList ByteString
669 |       -> (m : Nat)
670 |       -> ByteVect m
671 |       -> (0 acc : SizeAccessible m)
672 |       -> List ByteString
673 |     go sb m bs' (Access rec) = case breakNL bs' of
674 |       MkBreakRes l1 0      b1 _  p => sb <>> [BS l1 b1]
675 |       MkBreakRes l1 (S l2) b1 b2 p =>
676 |         go (sb :< BS l1 b1) l2 (tail b2) (rec l2 $ ltPlusSuccRight' _ p)
677 |
678 | 0 blocksLemma1 : (m,n : Nat) -> LT (S n `minus` S m) (S n)
679 | blocksLemma1 m n = LTESucc $ minusLTE _ _
680 |
681 | 0 blocksLemma2 : (m,n : Nat) -> LTE (S k) n -> LT (n `minus` S m) n
682 | blocksLemma2 m (S _) (LTESucc _) = blocksLemma1 m _
683 |
684 | ||| Splits the second byte vector whenever the first called
685 | ||| `sep` occurs.
686 | |||
687 | ||| The bytestrings in the result no longer contain `sep` as
688 | ||| a substring.
689 | |||
690 | ||| Note: If `sep` is the empty byte vector, `[BS n val]` is returned
691 | |||       as the result.
692 | export
693 | splitAtSubstring :
694 |      {k,n : _}
695 |   -> (sep : ByteVect k)
696 |   -> (val : ByteVect n)
697 |   -> List ByteString
698 | splitAtSubstring {k = 0}   sep bv = [BS _ bv]
699 | splitAtSubstring {k = S m} sep bv = go [<] bv (sizeAccessible n)
700 |   where
701 |     go : {o : _}
702 |       -> SnocList ByteString
703 |       -> (body  : ByteVect o)
704 |       -> (0 acc : SizeAccessible o)
705 |       -> List ByteString
706 |     go sb body (Access rec) =
707 |       let MkBreakRes l1 l2 b1 b2 p1 := breakAtSubstring sep body
708 |        in case tryLTE {n = l2} (S m) of
709 |             Nothing0 => sb <>> [BS l1 b1]
710 |             Just0 p2  =>
711 |               let 0 p3 := lteAddLeft {m = l2} l1 reflexive
712 |                   0 p4 := blocksLemma2 m l2 p2
713 |                   0 p5 := transitive (transitive p4 p3) p1
714 |                in go (sb :< BS l1 b1) (drop (S m) b2) (rec _ p5)
715 |
716 | export
717 | isInfixOf : {m,n : _} -> ByteVect m -> ByteVect n -> Bool
718 | isInfixOf bv1 bv2 = m == 0 || go n
719 |
720 |   where
721 |     go : (c : Nat) -> (x : Ix c n) => Bool
722 |     go 0     = False
723 |     go (S k) = isPrefixOf bv1 (drop (ixToNat x) @{ixLTE x} bv2) || go k
724 |
725 | --------------------------------------------------------------------------------
726 | --          Parsing Numbers
727 | --------------------------------------------------------------------------------
728 |
729 | ||| Parse a natural number in the given base.
730 | export
731 | parseAnyNat :
732 |      {n : _}
733 |   -> (base : Nat)
734 |   -> {auto 0 p1 : LTE 2 base}
735 |   -> {auto 0 p2 : LTE base 16}
736 |   -> ByteVect n
737 |   -> Maybe Nat
738 | parseAnyNat {n = Z} _    bv = Nothing
739 | parseAnyNat         base bv = go n 0
740 |
741 |   where
742 |     go : (c,res : Nat) -> (x : Ix c n) => Maybe Nat
743 |     go 0     res = Just res
744 |     go (S k) res =
745 |       let Just n := fromHexDigit $ ix bv k | Nothing => Nothing
746 |        in if n < base then go k (res * base + n) else Nothing
747 |
748 | ||| Parses a natural number in decimal notation.
749 | export %inline
750 | parseDecimalNat : {n : _} -> ByteVect n -> Maybe Nat
751 | parseDecimalNat {n = Z} bv = Nothing
752 | parseDecimalNat         bv = go n 0
753 |
754 |   where
755 |     go : (c,res : Nat) -> (x : Ix c n) => Maybe Nat
756 |     go 0     res = Just res
757 |     go (S k) res =
758 |       let Just n := fromDigit $ ix bv k | Nothing => Nothing
759 |        in go k (res * 10 + n)
760 |
761 | export %inline
762 | parseHexadecimalNat : {n : _} -> ByteVect n -> Maybe Nat
763 | parseHexadecimalNat = parseAnyNat 10
764 |
765 | export %inline
766 | parseOctalNat : {n : _} -> ByteVect n -> Maybe Nat
767 | parseOctalNat = parseAnyNat 8
768 |
769 | export %inline
770 | parseBinaryNat : {n : _} -> ByteVect n -> Maybe Nat
771 | parseBinaryNat = parseAnyNat 2
772 |
773 | export
774 | parseInteger : {n : _} -> ByteVect n -> Maybe Integer
775 | parseInteger {n = Z}   _  = Nothing
776 | parseInteger {n = S _} bv = case head bv of
777 |   43 => cast          <$> parseDecimalNat (tail bv) -- '+'
778 |   45 => negate . cast <$> parseDecimalNat (tail bv) -- '-'
779 |   _  => cast <$> parseDecimalNat bv
780 |
781 |
782 | -- parsing Double
783 |
784 | isE : Bits8 -> Bool
785 | isE 69  = True
786 | isE 101 = True
787 | isE _   = False
788 |
789 | fract : {n : _} -> ByteVect n -> Maybe Double
790 | fract bv =
791 |   let Just k := parseDecimalNat bv | Nothing => Nothing
792 |    in Just (cast k / (pow 10 $ cast n))
793 |
794 | exp : {n : _} -> ByteVect n -> Maybe Double
795 | exp bv =
796 |   let Just exp := parseInteger bv | Nothing => Nothing
797 |    in Just $ pow 10.0 (cast exp)
798 |
799 | parseDotted : {n : _} -> ByteVect n -> Maybe Double
800 | parseDotted bv = go 0 0 n
801 |   where
802 |     go : (v,exp,c : Nat) -> (x : Ix c n) => Maybe Double
803 |     go v exp 0     = case exp of
804 |       0 => Just $ cast v
805 |       _ => Just $ cast v / cast exp
806 |     go v exp (S k) =
807 |       case ix bv k of
808 |         48 => go (v * 10 + 0) (exp * 10) k
809 |         49 => go (v * 10 + 1) (exp * 10) k
810 |         50 => go (v * 10 + 2) (exp * 10) k
811 |         51 => go (v * 10 + 3) (exp * 10) k
812 |         52 => go (v * 10 + 4) (exp * 10) k
813 |         53 => go (v * 10 + 5) (exp * 10) k
814 |         54 => go (v * 10 + 6) (exp * 10) k
815 |         55 => go (v * 10 + 7) (exp * 10) k
816 |         56 => go (v * 10 + 8) (exp * 10) k
817 |         57 => go (v * 10 + 9) (exp * 10) k
818 |         46 => case exp of
819 |           0 => go v 1 k
820 |           _ => Nothing
821 |         _  => Nothing
822 |
823 | parsePosDbl : {n : _} -> ByteVect n -> Maybe Double
824 | parsePosDbl bv = case parseDotted bv of
825 |   Just v  => Just v
826 |   Nothing => case break isE bv of
827 |     MkBreakRes lf (S _) dotStr expStr _ =>
828 |       let Just fract := parseDotted dotStr | Nothing => Nothing
829 |           Just e     := exp (tail expStr)  | Nothing => Nothing
830 |        in Just $ fract * e
831 |     MkBreakRes _ 0 _ _ _ => Nothing
832 |
833 | export
834 | parseDouble : {n : _} -> ByteVect n -> Maybe Double
835 | parseDouble {n = Z}   _  = Nothing
836 | parseDouble {n = S _} bv = case head bv of
837 |   43 => parsePosDbl (tail bv)             -- '+'
838 |   45 => negate  <$> parsePosDbl (tail bv) -- '-'
839 |   _  => parsePosDbl bv
840 |
841 | --------------------------------------------------------------------------------
842 | -- Using Builders
843 | --------------------------------------------------------------------------------
844 |
845 | export %inline
846 | putByteVect : Builder q => {n : _} -> ByteVect n -> F1' q
847 | putByteVect (BV buf off _) = putBytesFrom off n buf
848 |