0 | module FS.Internal.Bytes
  1 |
  2 | import Data.Bits
  3 | import Data.ByteString
  4 | import Data.ByteVect
  5 | import Derive.Prelude
  6 |
  7 | %default total
  8 | %language ElabReflection
  9 |
 10 | public export
 11 | 0 SnocBytes : Type
 12 | SnocBytes = SnocList ByteString
 13 |
 14 | public export
 15 | 0 Bytes : Type
 16 | Bytes = List ByteString
 17 |
 18 | export
 19 | concatSnoc : SnocBytes -> ByteString
 20 | concatSnoc [<]  = empty
 21 | concatSnoc [<x] = x
 22 | concatSnoc sx   = fastConcat (sx <>> [])
 23 |
 24 | export
 25 | nl : ByteString
 26 | nl = singleton 0x0a
 27 |
 28 | ls : SnocBytes -> (n : Nat) -> ByteVect n -> (Maybe Bytes, ByteString)
 29 | ls sb n bs = case breakNL bs of
 30 |   MkBreakRes l1 0      b1 _  prf => (Just $ sb <>> [], BS l1 b1)
 31 |   MkBreakRes l1 (S l2) b1 b2 prf =>
 32 |     ls (sb :< BS l1 b1) (assert_smaller n l2) (tail b2)
 33 |
 34 | export
 35 | splitNL : ByteString -> ByteString -> (Maybe Bytes, ByteString)
 36 | splitNL x (BS n bs) =
 37 |   case breakNL bs of
 38 |     MkBreakRes l1 0      b1 _  prf => (Nothing, x <+> BS l1 b1)
 39 |     MkBreakRes l1 (S l2) b1 b2 prf => ls [<x <+> BS l1 b1] l2 (tail b2)
 40 |
 41 | export
 42 | breakLastNL : ByteString -> ByteString -> (Maybe ByteString, ByteString)
 43 | breakLastNL x (BS n bs) =
 44 |   case breakEnd (0x0a ==) bs of
 45 |     MkBreakRes 0      l2 b1 b2 prf => (Nothing, x <+> BS l2 b2)
 46 |     MkBreakRes (S l1) l2 b1 b2 prf => (Just (x <+> BS _ (init b1)), BS l2 b2)
 47 |
 48 | namespace UTF8
 49 |   ||| The number of continuation bytes following a UTF-8 leading byte.
 50 |   |||
 51 |   ||| See [Wikipedia](https://en.wikipedia.org/wiki/UTF-8#Description)
 52 |   ||| for a description of the magic numbers used in the implementation
 53 |   ||| and the UTF-8 encoding in general.
 54 |   export
 55 |   continuationBytes : Bits8 -> Maybe Nat
 56 |   continuationBytes b =
 57 |     -- we use binary notation for the magic constants to make
 58 |     -- them easily comparable with the values in the table on Wikipedia
 59 |     if      (b .&. 0b1000_0000) == 0b0000_0000 then Just 0
 60 |     else if (b .&. 0b1110_0000) == 0b1100_0000 then Just 1
 61 |     else if (b .&. 0b1111_0000) == 0b1110_0000 then Just 2
 62 |     else if (b .&. 0b1111_1000) == 0b1111_0000 then Just 3
 63 |     else                                            Nothing
 64 |
 65 |   -- splits a bytestring at the last UTF-8 leading byte.
 66 |   splitLeading :
 67 |        {n : Nat}
 68 |     -> (k : Nat)
 69 |     -> ByteVect n
 70 |     -> {auto 0 p : LTE k n}
 71 |     -> (Maybe ByteString,ByteString)
 72 |   splitLeading 0     x = (Nothing, BS _ x)
 73 |   splitLeading (S k) x =
 74 |     case continuationBytes (atNat x k) of
 75 |       Nothing  => splitLeading k x
 76 |       Just y   =>
 77 |         if S k + y == n
 78 |            then (nonEmpty $ BS _ x, empty)
 79 |            else (nonEmpty $ BS _ $ take k x, BS _ $ drop k x)
 80 |
 81 |   ||| Breaks a list of byte vectors at the last incomplete UTF-8 codepoint
 82 |   ||| The first list is a concatenation of all the complete UTF-8 strings,
 83 |   ||| while the second list contains the last incomplete codepoint (in case
 84 |   ||| of a valid UTF-8 string, the second list holds at most 3 bytes).
 85 |   export
 86 |   breakAtLastIncomplete : ByteString -> ByteString -> (Maybe ByteString, ByteString)
 87 |   breakAtLastIncomplete pre cur =
 88 |     let BS sz bv := pre <+> cur
 89 |      in splitLeading sz bv
 90 |
 91 | --------------------------------------------------------------------------------
 92 | -- Breaking at Substrings
 93 | --------------------------------------------------------------------------------
 94 |
 95 | ||| Result of splitting a byte string at a given substring
 96 | public export
 97 | data BSSRes : Type where
 98 |   ||| Input was too short. Will be passed on as a whole.
 99 |   TooShort : ByteString -> BSSRes
100 |
101 |   ||| Substring not found. `pst` is one shorter than the substring in question,
102 |   ||| because it might still end on a prefix of the substring.
103 |   NoSS     : (pre,pst : ByteString) -> BSSRes
104 |
105 |   ||| Substring was found between `pre` and `pst`.
106 |   SS       : (pre,pst : ByteString) -> BSSRes
107 |
108 | %runElab derive "BSSRes" [Show,Eq]
109 |
110 | export
111 | breakAtSS : (ss, cur : ByteString) -> BSSRes
112 | breakAtSS ss cur =
113 |   case size cur < size ss of
114 |     True  => TooShort cur
115 |     False => case breakAtSubstring ss cur of
116 |       (pre, BS 0 _) =>
117 |         let ln := S (size pre) `minus` size ss
118 |          in NoSS (take ln pre) (drop ln pre)
119 |       (pre, pst)    => SS pre (drop ss.size pst)
120 |