
   0 | ||| Immutable strings of raw bytes.
   1 | module Data.ByteString
   2 | 
   3 | import Data.Buffer
   4 | import Data.Buffer.Builder
   5 | import Data.Buffer.Mutable
   6 | import Data.List
   7 | import Data.Maybe0
   8 | import Data.Nat.BSExtra
   9 | import Data.String
  10 | 
  11 | import System.File
  12 | 
  13 | import public Data.ByteVect as BV
  14 | 
  15 | %default total
  16 | 
  17 | --------------------------------------------------------------------------------
  18 | --          ByteString
  19 | --------------------------------------------------------------------------------
  20 | 
  21 | export
  22 | null : ByteString -> Bool
  23 | null (BS Z _) = True
  24 | null _        = False
  25 | 
  26 | export %inline
  27 | length : ByteString -> Nat
  28 | length (BS n _) = n
  29 | 
  30 | ||| Tries to read the value of a `ByteString` at the given position
  31 | export
  32 | index : (x : Nat) -> ByteString -> Maybe Bits8
  33 | index x (BS n repr) = at repr <$> tryNatToFin x
  34 | 
  35 | --------------------------------------------------------------------------------
  36 | --          Making ByteStrings
  37 | --------------------------------------------------------------------------------
  38 | 
  39 | ||| The empty `ByteString`.
  40 | export %inline
  41 | empty : ByteString
  42 | empty = BS 0 empty
  43 | 
  44 | ||| Converts a list of `Bits8` values to a `ByteString`.
  45 | export %inline
  46 | pack : (as : List Bits8) -> ByteString
  47 | pack as = BS _ $ pack as
  48 | 
  49 | ||| Creates a `ByteString` holding a single `Bits8` value.
  50 | export %inline
  51 | singleton : Bits8 -> ByteString
  52 | singleton v = pack [v]
  53 | 
  54 | ||| Convert a `ByteString` to a list of values using
  55 | ||| the given conversion function.
  56 | export %inline
  57 | toList : (Bits8 -> a) -> ByteString -> List a
  58 | toList f (BS _ bs) = toList f bs
  59 | 
  60 | ||| Converts a `ByteString` to a list of `Bits8` values. O(n).
  61 | export %inline
  62 | unpack : ByteString -> List Bits8
  63 | unpack = toList id
  64 | 
  65 | ||| Converts a `ByteString` to a UTF-8 encoded string
  66 | export
  67 | toString : ByteString -> String
  68 | toString (BS _ bs) = toString bs
  69 | 
  70 | export %inline
  71 | Interpolation ByteString where interpolate = toString
  72 | 
  73 | ||| Converts a `ByteString` to a String. All characters
  74 | ||| will be in the range [0,255], so this does not perform
  75 | ||| any character decoding.
  76 | export %inline
  77 | Show ByteString where
  78 |   show (BS _ bs) = show bs
  79 | 
  80 | export %inline
  81 | Eq ByteString where
  82 |   BS _ bs1 == BS _ bs2 = heq bs1 bs2
  83 | 
  84 | export %inline
  85 | Ord ByteString where
  86 |   compare (BS _ bs1) (BS _ bs2) = hcomp bs1 bs2
  87 | 
  88 | export
  89 | FromString ByteString where
  90 |   fromString s = BS _ $ fromString s
  91 | 
  92 | export %inline
  93 | Cast String ByteString where
  94 |   cast = fromString
  95 | 
  96 | export %inline
  97 | Cast (List Bits8) ByteString where
  98 |   cast = pack
  99 | 
 100 | export %inline
 101 | Cast Bits8 ByteString where
 102 |   cast = singleton
 103 | 
 104 | export %inline
 105 | Cast Char ByteString where
 106 |   cast = cast {from = String} . singleton
 107 | 
 108 | export %inline
 109 | {n : _} -> Cast (ByteVect n) ByteString where
 110 |   cast = BS n
 111 | 
 112 | export %inline
 113 | {n : _} -> Cast (IBuffer n) ByteString where
 114 |   cast = cast . fromIBuffer
 115 | 
 116 | export %inline
 117 | Cast AnyBuffer ByteString where
 118 |   cast (AB _ ib) = cast ib
 119 | 
 120 | --------------------------------------------------------------------------------
 121 | --          Core Functionality
 122 | --------------------------------------------------------------------------------
 123 | 
 124 | export %inline
 125 | generate : (n : Nat) -> (Fin n -> Bits8) -> ByteString
 126 | generate n f = BS n (generate n f)
 127 | 
 128 | export
 129 | replicate : (n : Nat) -> Bits8 -> ByteString
 130 | replicate n = generate n . const
 131 | 
 132 | export
 133 | unsafeByteString : (n : Nat) -> Buffer -> ByteString
 134 | unsafeByteString n buf = BS n (BV (unsafeMakeBuffer buf) 0 reflexive)
 135 | 
 136 | ||| Copy the given `ByteString` and write its content to a freshly
 137 | ||| allocated buffer.
 138 | export
 139 | toBuffer : ByteString -> IO Buffer
 140 | toBuffer (BS n (BV b o lt)) =
 141 |   alloc n $ \r,t =>
 142 |     let _ # t := icopy b o 0 n r t
 143 |      in pure (unsafeFromMBuffer r) # t
 144 | 
 145 | ||| Wrappes an immutable buffer in a `ByteString`
 146 | export
 147 | fromIBuffer : {n : _} -> IBuffer n -> ByteString
 148 | fromIBuffer b = BS n $ fromIBuffer b
 149 | 
 150 | --------------------------------------------------------------------------------
 151 | --          Concatenating ByteStrings
 152 | --------------------------------------------------------------------------------
 153 | 
 154 | public export
 155 | TotLength : List ByteString -> Nat
 156 | TotLength []             = 0
 157 | TotLength (BS n _ :: xs) = n + TotLength xs
 158 | 
 159 | export
 160 | copyMany :
 161 |      (ps  : List ByteString)
 162 |   -> (pos : Nat)
 163 |   -> {auto 0 prf : pos + TotLength ps === n}
 164 |   -> (r   : MBuffer s n)
 165 |   -> F1' s
 166 | copyMany []                      pos r t = () # t
 167 | copyMany (BS k (BV b o lt):: xs) pos r t =
 168 |   let _ # t := icopy b o pos k @{lt} @{rewrite sym prf in concatLemma1} r t
 169 |    in copyMany xs (pos + k) @{concatLemma2 prf} r t
 170 | 
 171 | ||| Concatenate a list of `ByteString`. This allocates
 172 | ||| a buffer of sufficient size in advance, so it is much
 173 | ||| faster than `concat`, or `concatMap` for large `ByteString`s.
 174 | export
 175 | fastConcat :  (bs : List ByteString) -> ByteString
 176 | fastConcat []  = empty
 177 | fastConcat [b] = b
 178 | fastConcat bs  =
 179 |   alloc (TotLength bs) $ \r,t =>
 180 |     let _ # t := copyMany bs 0 r t in unsafeFreezeByteString r t
 181 | 
 182 | ||| Concatenates a list of bytestrings, separating them with the
 183 | ||| given separator `sep`.
 184 | export %inline
 185 | concatSep : (sep : ByteString) -> (bs : List ByteString) -> ByteString
 186 | concatSep sep = fastConcat . intersperse sep
 187 | 
 188 | ||| Concatenates a list of bytestrings, using the given byte to
 189 | ||| separate them.
 190 | export %inline
 191 | concatSep1 : (sep : Bits8) -> (bs : List ByteString) -> ByteString
 192 | concatSep1 = concatSep . singleton
 193 | 
 194 | ||| Concatenates the given list of bytestring by interspersing them
 195 | ||| with Unix linebreaks (byte `0x0A`).
 196 | export %inline
 197 | unixUnlines : List ByteString -> ByteString
 198 | unixUnlines = concatSep1 0x0A
 199 | 
 200 | ||| Concatenate two `ByteString`s. O(n + m).
 201 | export
 202 | append : ByteString -> ByteString -> ByteString
 203 | append (BS 0 _)   b2         = b2
 204 | append b1         (BS 0 _)   = b1
 205 | append (BS m bv1) (BS n bv2) = BS _ $ append bv1 bv2
 206 | 
 207 | ||| Prepend a single `Bits8` to a `ByteString`. O(n).
 208 | export %inline
 209 | cons : Bits8 -> ByteString -> ByteString
 210 | cons = append . singleton
 211 | 
 212 | ||| Append a single `Bits8` to a `ByteString`. O(n).
 213 | export %inline
 214 | snoc : Bits8 -> ByteString -> ByteString
 215 | snoc w bs = bs `append` singleton w
 216 | 
 217 | export %inline
 218 | Semigroup ByteString where
 219 |   (<+>) = append
 220 | 
 221 | export %inline
 222 | Monoid ByteString where
 223 |   neutral = empty
 224 | 
 225 | export
 226 | padLeft : Nat -> Bits8 -> ByteString -> ByteString
 227 | padLeft n b bs = replicate (n `minus` bs.size) b <+> bs
 228 | 
 229 | export
 230 | padRight : Nat -> Bits8 -> ByteString -> ByteString
 231 | padRight n b bs = bs <+> replicate (n `minus` bs.size) b
 232 | 
 233 | --------------------------------------------------------------------------------
 234 | --          Inspecting ByteStrings
 235 | --------------------------------------------------------------------------------
 236 | 
 237 | ||| Read the first element of a `ByteString`. O(1).
 238 | export %inline
 239 | head : ByteString -> Maybe Bits8
 240 | head = index 0
 241 | 
 242 | ||| Drop the first `Bits8` from a `ByteString`. O(1).
 243 | export
 244 | tail : ByteString -> Maybe ByteString
 245 | tail (BS (S k) bs) = Just (BS k $ tail bs)
 246 | tail _             = Nothing
 247 | 
 248 | ||| Split the first `Bits8` from a `ByteString`. O(1).
 249 | export
 250 | uncons : ByteString -> Maybe (Bits8, ByteString)
 251 | uncons (BS (S k) bs) = let (b,bs2) := uncons bs in Just (b, BS k bs2)
 252 | uncons _             = Nothing
 253 | 
 254 | ||| Read the last `Bits8` from a `ByteString`. O(1).
 255 | export
 256 | last : ByteString -> Maybe Bits8
 257 | last (BS (S k) bs) = Just $ last bs
 258 | last _             = Nothing
 259 | 
 260 | ||| Drop the last `Bits8` from a `ByteString`. O(1).
 261 | export
 262 | init : ByteString -> Maybe ByteString
 263 | init (BS (S k) bs) = Just (BS k $ init bs)
 264 | init _             = Nothing
 265 | 
 266 | ||| Split the last `Bits8` from a `ByteString`. O(1).
 267 | export
 268 | unsnoc : ByteString -> Maybe (Bits8, ByteString)
 269 | unsnoc (BS (S k) bs) = let (b,bs2) := unsnoc bs in Just (b, BS k bs2)
 270 | unsnoc _             = Nothing
 271 | 
 272 | --------------------------------------------------------------------------------
 273 | --          Mapping ByteStrings
 274 | --------------------------------------------------------------------------------
 275 | 
 276 | ||| Converts every `Bits8` in a `ByteString` by applying the given
 277 | ||| function. O(n).
 278 | export %inline
 279 | map : (Bits8 -> Bits8) -> ByteString -> ByteString
 280 | map f (BS n bs) = BS n $ map f bs
 281 | 
 282 | ||| Interpreting the values stored in a `ByteString` as 8 bit characters,
 283 | ||| convert every lower-case character to its upper-case form.
 284 | export %inline
 285 | toUpper : ByteString -> ByteString
 286 | toUpper = map toUpper
 287 | 
 288 | ||| Interpreting the values stored in a `ByteString` as 8 bit characters,
 289 | ||| convert every upper-case character to its lower-case form.
 290 | export %inline
 291 | toLower : ByteString -> ByteString
 292 | toLower = map toLower
 293 | 
 294 | export %inline
 295 | reverse : ByteString -> ByteString
 296 | reverse (BS n bs) = BS n $ reverse bs
 297 | 
 298 | ||| True, if the predicate holds for all bytes in the given `ByteString`
 299 | export %inline
 300 | all : (Bits8 -> Bool) -> ByteString -> Bool
 301 | all p (BS n bs) = all p bs
 302 | 
 303 | ||| True, if the predicate holds for at least one byte
 304 | ||| in the given `ByteString`
 305 | export %inline
 306 | any : (Bits8 -> Bool) -> ByteString -> Bool
 307 | any p (BS n bs) = any p bs
 308 | 
 309 | ||| True, if the given `Bits8` appears in the `ByteString`.
 310 | export %inline
 311 | elem : Bits8 -> ByteString -> Bool
 312 | elem b = any (b ==)
 313 | 
 314 | export %inline
 315 | foldl : (a -> Bits8 -> a) -> a -> ByteString -> a
 316 | foldl f ini (BS n bs) = foldl f ini bs
 317 | 
 318 | export %inline
 319 | foldr : (Bits8 -> a -> a) -> a -> ByteString -> a
 320 | foldr f ini (BS n bs) = foldr f ini bs
 321 | 
 322 | ||| The `findIndex` function takes a predicate and a `ByteString` and
 323 | ||| returns the index of the first element in the ByteString
 324 | ||| satisfying the predicate.
 325 | export %inline
 326 | findIndex : (Bits8 -> Bool) -> ByteString -> Maybe Nat
 327 | findIndex p (BS n bs) = finToNat <$> findIndex p bs
 328 | 
 329 | ||| Return the index of the first occurence of the given
 330 | ||| byte in the `ByteString`, or `Nothing`, if the byte
 331 | ||| does not appear in the ByteString.
 332 | export %inline
 333 | elemIndex : Bits8 -> ByteString -> Maybe Nat
 334 | elemIndex c = findIndex (c ==)
 335 | 
 336 | export %inline
 337 | find : (Bits8 -> Bool) -> ByteString -> Maybe Bits8
 338 | find p (BS n bs) = find p bs
 339 | 
 340 | export %inline
 341 | isInfixOf : ByteString -> ByteString -> Bool
 342 | isInfixOf (BS _ bv1) (BS _ bv2) = isInfixOf bv1 bv2
 343 | 
 344 | export %inline
 345 | isPrefixOf : ByteString -> ByteString -> Bool
 346 | isPrefixOf (BS _ bv1) (BS _ bv2) = isPrefixOf bv1 bv2
 347 | 
 348 | export %inline
 349 | isSuffixOf : ByteString -> ByteString -> Bool
 350 | isSuffixOf (BS _ bv1) (BS _ bv2) = isSuffixOf bv1 bv2
 351 | 
 352 | --------------------------------------------------------------------------------
 353 | --          Substrings
 354 | --------------------------------------------------------------------------------
 355 | 
 356 | ||| Like `substr` for `String`, this extracts a substring
 357 | ||| of the given `ByteString` at the given start position
 358 | ||| and of the given length.
 359 | export
 360 | substring : (start,length : Nat) -> ByteString -> ByteString
 361 | substring s l (BS n bs) =
 362 |   case tryLTE (s+l) of
 363 |     Just0 p  => BS l (substring s l bs)
 364 |     Nothing0 => case tryLTE s of
 365 |       Just0 p  => BS (n `minus` s) (drop s bs)
 366 |       Nothing0 => empty
 367 | 
 368 | export
 369 | mapMaybe : (Bits8 -> Maybe Bits8) -> ByteString -> ByteString
 370 | mapMaybe f (BS n bs) = mapMaybe f bs
 371 | 
 372 | export
 373 | filter : (Bits8 -> Bool) -> ByteString -> ByteString
 374 | filter p (BS n bs) = filter p bs
 375 | 
 376 | ||| Return a `ByteString` with the first `n` values of
 377 | ||| the input string. Returns the whole string if
 378 | ||| `k` is larger than the bytestring. O(1)
 379 | export
 380 | take : Nat -> ByteString -> ByteString
 381 | take k (BS n bs) =
 382 |   case tryLTE k of
 383 |     Just0 p  => BS k (take k bs)
 384 |     Nothing0 => BS n bs
 385 | 
 386 | ||| Return a `ByteString` with the last `n` values of
 387 | ||| the input string. O(1)
 388 | export
 389 | takeEnd : Nat -> ByteString -> ByteString
 390 | takeEnd k (BS n bs) =
 391 |   case tryLTE k of
 392 |     Just0 p  => BS k (takeEnd k bs)
 393 |     Nothing0 => BS n bs
 394 | 
 395 | ||| Remove the first `n` values from a `ByteString`. O(1)
 396 | export
 397 | drop : Nat -> ByteString -> ByteString
 398 | drop k (BS n bs) =
 399 |   case tryLTE k of
 400 |     Just0 p  => BS (n `minus` k) (drop k bs)
 401 |     Nothing0 => empty
 402 | 
 403 | ||| Remove the last `n` values from a `ByteString`. O(1)
 404 | export
 405 | dropEnd : Nat -> ByteString -> ByteString
 406 | dropEnd k (BS n bs) =
 407 |   case tryLTE k of
 408 |     Just0 p  => BS (n `minus` k) (dropEnd k bs)
 409 |     Nothing0 => empty
 410 | 
 411 | export
 412 | splitAt : (k : Nat) -> ByteString -> Maybe (ByteString,ByteString)
 413 | splitAt k (BS n bs) =
 414 |   case tryLTE k of
 415 |     Just0 p  =>
 416 |       let (bs1,bs2) := splitAt k bs
 417 |        in Just (BS k bs1, BS (n `minus` k) bs2)
 418 |     Nothing0 => Nothing
 419 | 
 420 | ||| Extracts the longest prefix of elements satisfying the
 421 | ||| predicate.
 422 | export %inline
 423 | takeWhile : (Bits8 -> Bool) -> ByteString -> ByteString
 424 | takeWhile p (BS n bs) = takeWhile p bs
 425 | 
 426 | ||| Returns the longest (possibly empty) suffix of elements
 427 | ||| satisfying the predicate.
 428 | export %inline
 429 | takeWhileEnd : (Bits8 -> Bool) -> ByteString -> ByteString
 430 | takeWhileEnd p (BS n bs) = takeWhileEnd p bs
 431 | 
 432 | ||| Drops the longest (possibly empty) prefix of elements
 433 | ||| satisfying the predicate and returns the remainder.
 434 | export %inline
 435 | dropWhile : (Bits8 -> Bool) -> ByteString -> ByteString
 436 | dropWhile p (BS n bs) = dropWhile p bs
 437 | 
 438 | ||| Drops the longest (possibly empty) suffix of elements
 439 | ||| satisfying the predicate and returns the remainder.
 440 | export %inline
 441 | dropWhileEnd : (Bits8 -> Bool) -> ByteString -> ByteString
 442 | dropWhileEnd p (BS n bs) = dropWhileEnd p bs
 443 | 
 444 | ||| Returns the longest (possibly empty) prefix of elements which do not
 445 | ||| satisfy the predicate and the remainder of the string.
 446 | export
 447 | break : (Bits8 -> Bool) -> ByteString -> (ByteString,ByteString)
 448 | break p (BS n bs) =
 449 |   let MkBreakRes n1 n2 bs1 bs2 _ := break p bs
 450 |    in (BS n1 bs1, BS n2 bs2)
 451 | 
 452 | ||| Returns the longest (possibly empty) suffix of elements which do not
 453 | ||| satisfy the predicate and the remainder of the string.
 454 | export
 455 | breakEnd : (Bits8 -> Bool) -> ByteString -> (ByteString,ByteString)
 456 | breakEnd p (BS n bs) =
 457 |   let MkBreakRes n1 n2 bs1 bs2 _ := breakEnd p bs
 458 |    in (BS n1 bs1, BS n2 bs2)
 459 | 
 460 | ||| Returns the longest (possibly empty) prefix of elements
 461 | ||| satisfying the predicate and the remainder of the string.
 462 | export %inline
 463 | span : (Bits8 -> Bool) -> ByteString -> (ByteString,ByteString)
 464 | span p = break (not . p)
 465 | 
 466 | ||| Returns the longest (possibly empty) suffix of elements
 467 | ||| satisfying the predicate and the remainder of the string.
 468 | export
 469 | spanEnd : (Bits8 -> Bool) -> ByteString -> (ByteString,ByteString)
 470 | spanEnd p (BS n bs) =
 471 |   let MkBreakRes n1 n2 bs1 bs2 _ := spanEnd p bs
 472 |    in (BS n1 bs1, BS n2 bs2)
 473 | 
 474 | ||| Remove leading whitespace from a `ByteString`
 475 | export %inline
 476 | trimLeft : ByteString -> ByteString
 477 | trimLeft (BS _ bv) = trimLeft bv
 478 | 
 479 | ||| Remove trailing whitespace from a `ByteString`
 480 | export %inline
 481 | trimRight : ByteString -> ByteString
 482 | trimRight (BS _ bv) = trimRight bv
 483 | 
 484 | ||| Remove all leading and trailing whitespace from a `ByteString`
 485 | export %inline
 486 | trim : ByteString -> ByteString
 487 | trim (BS _ bv) = trim bv
 488 | 
 489 | ||| Splits a 'ByteString' into components delimited by
 490 | ||| separators, where the predicate returns True for a separator element.
 491 | ||| The resulting components do not contain the separators. Two adjacent
 492 | ||| separators result in an empty component in the output. eg.
 493 | export
 494 | splitWith : (Bits8 -> Bool) -> ByteString -> List ByteString
 495 | splitWith p (BS n bs) = splitWith p bs
 496 | 
 497 | ||| Like `splitWith`, but removes empty components.
 498 | export %inline
 499 | splitWithNonEmpty : (Bits8 -> Bool) -> ByteString -> List ByteString
 500 | splitWithNonEmpty p = filter (not . null) . splitWith p
 501 | 
 502 | ||| Break a `ByteString` into pieces separated by the byte
 503 | ||| argument, consuming the delimiter.
 504 | |||
 505 | ||| As for all splitting functions in this library, this function does
 506 | ||| not copy the substrings, it just constructs new `ByteString`s that
 507 | ||| are slices of the original.
 508 | export %inline
 509 | split : Bits8 -> ByteString -> List ByteString
 510 | split b = splitWith (b ==)
 511 | 
 512 | ||| Like `splitWith`, but removes empty components.
 513 | export %inline
 514 | splitNonEmpty : Bits8 -> ByteString -> List ByteString
 515 | splitNonEmpty p = filter (not . null) . split p
 516 | 
 517 | ||| Returns the longest (possibly empty) prefix of a
 518 | ||| bytestring that does not contain the given substring
 519 | ||| plus the remainder of the byte vector.
 520 | export %inline
 521 | breakAtSubstring : (sep,val : ByteString) -> (ByteString,ByteString)
 522 | breakAtSubstring (BS _ s) (BS _ v) =
 523 |   let MkBreakRes _ _ x y _ := breakAtSubstring s v
 524 |    in (BS _ x, BS _ y)
 525 | 
 526 | ||| Like `breakAtSubstring` but removes the
 527 | ||| substring from the remainder
 528 | export
 529 | breakDropAtSubstring : (pat,target : ByteString) -> (ByteString,ByteString)
 530 | breakDropAtSubstring pat = map (drop $ size pat) . breakAtSubstring pat
 531 | 
 532 | ||| Splits the second bytestring whenever the first called
 533 | ||| `sep` occurs.
 534 | |||
 535 | ||| The bytestrings in the result no longer contain `sep` as
 536 | ||| a substring.
 537 | |||
 538 | ||| Note: If `sep` is the empty bytestring, `[val]` is returned
 539 | |||       as the result.
 540 | export %inline
 541 | splitAtSubstring : (sep, val : ByteString) -> List ByteString
 542 | splitAtSubstring (BS _ s) (BS _ v) = splitAtSubstring s v
 543 | 
 544 | ||| Breakes the given bytestring at Unix linebreaks (byte `0x0A`).
 545 | export %inline
 546 | unixLines : ByteString -> List ByteString
 547 | unixLines (BS _ bv) = lines bv
 548 | 
 549 | --------------------------------------------------------------------------------
 550 | --          (Replacing) Substrings
 551 | --------------------------------------------------------------------------------
 552 | 
 553 | ||| Extracts the string encountered between `start` and `end`
 554 | ||| returning a triple containing the prefix, string in the middle,
 555 | ||| and suffix.
 556 | |||
 557 | ||| Note: The `start` and `end` tag will *not*
 558 | |||       be included in the resulting triple.
 559 | |||
 560 | ||| Returns `Nothing` in case the prefix or suffix was the empty string.
 561 | ||| In particular, this will return `Nothing` in case `start` or `end`
 562 | ||| is the empty string.
 563 | export
 564 | breakAround :
 565 |      (start,end,target : ByteString)
 566 |   -> Maybe (ByteString,ByteString,ByteString)
 567 | breakAround s e t =
 568 |   if s.size == 0 || e.size == 0 then Nothing else
 569 |     case breakAtSubstring s t of
 570 |       (_,BS 0 _) => Nothing
 571 |       (pre,suf)  => case breakAtSubstring e (drop s.size suf) of
 572 |         (_,BS 0 _) => Nothing
 573 |         (mid,end)  => Just (pre,mid, drop e.size end)
 574 | 
 575 | ||| Extracts the string encountered between `start` and `end`.
 576 | |||
 577 | ||| This will look for the *first* occurrence of `start` and
 578 | ||| will take everything until (but not including) the *first*
 579 | ||| occurrence of `end` after `start`.
 580 | |||
 581 | ||| Returns `Nothing` if `end` or `start` is the empty string or
 582 | ||| either of the two was not found.
 583 | export %inline
 584 | between : (start,end,target : ByteString) -> Maybe ByteString
 585 | between s e = map (fst . snd) . breakAround s e
 586 | 
 587 | ||| Returns the given byte string wrapped in a `Just` if and only if
 588 | ||| it is non-empty.
 589 | export
 590 | nonEmpty : ByteString -> Maybe ByteString
 591 | nonEmpty (BS 0 _) = Nothing
 592 | nonEmpty bs       = Just bs
 593 | 
 594 | ||| Extracts *all* occurrences of strings encountered between
 595 | ||| the given `start` and `end` tags.
 596 | |||
 597 | ||| Returns an empty list if the start or end tag is the empty
 598 | ||| bytestring.
 599 | export
 600 | manyBetween : (start,end : ByteString) -> ByteString -> List ByteString
 601 | manyBetween s e = go [<]
 602 |   where
 603 |     go : SnocList ByteString -> ByteString -> List ByteString
 604 |     go sb bs =
 605 |       case breakAround s e bs of
 606 |         Just (x,y,z) => go (sb:<y) (assert_smaller bs z)
 607 |         Nothing      => sb <>> []
 608 | 
 609 | ||| Like `between` but returns `Nothing` in case the resulting
 610 | ||| bytestring would be empty.
 611 | export %inline
 612 | betweenNonEmpty : (start,end,target : ByteString) -> Maybe ByteString
 613 | betweenNonEmpty s e t = between s e t >>= nonEmpty
 614 | 
 615 | ||| Replaces the first byte sequence in the target string
 616 | ||| found between the given `start` and `end` tag by
 617 | ||| applying the given function.
 618 | |||
 619 | ||| In case `start` or `end` is the empty string, this will return
 620 | ||| the unmodified bytestring.
 621 | export
 622 | modBetween :
 623 |      (start,end : ByteString)
 624 |   -> (f         : ByteString -> ByteString)
 625 |   -> (target    : ByteString)
 626 |   -> ByteString
 627 | modBetween s e f t =
 628 |   case breakAround s e t of
 629 |     Just (x,y,z) => fastConcat [x,s,f y,e,z]
 630 |     Nothing      => t
 631 | 
 632 | ||| Replaces all byte sequences in the target string
 633 | ||| found between the given `start` and `end` tag by
 634 | ||| applying the given function to each of them.
 635 | |||
 636 | ||| In case `start` or `end` is the empty string, this will return
 637 | ||| the unmodified bytestring.
 638 | export
 639 | modBetweenAll :
 640 |      (start,end : ByteString)
 641 |   -> (f         : ByteString -> ByteString)
 642 |   -> (target    : ByteString)
 643 |   -> ByteString
 644 | modBetweenAll s e f = go [<]
 645 | 
 646 |   where
 647 |     go : SnocList ByteString -> ByteString -> ByteString
 648 |     go sb bs =
 649 |       case breakAround s e bs of
 650 |         Just (x,y,z) => go (sb:<x:<s:<f y:<e) (assert_smaller bs z)
 651 |         Nothing      => fastConcat (sb <>> [bs])
 652 | 
 653 | --------------------------------------------------------------------------------
 654 | --          Parsing Numbers
 655 | --------------------------------------------------------------------------------
 656 | 
 657 | ||| Parse a natural number in the given base.
 658 | export %inline
 659 | parseAnyNat :
 660 |      (base : Nat)
 661 |   -> {auto 0 p1 : LTE 2 base}
 662 |   -> {auto 0 p2 : LTE base 16}
 663 |   -> ByteString
 664 |   -> Maybe Nat
 665 | parseAnyNat base (BS _ bv) = parseAnyNat base bv
 666 | 
 667 | ||| Parses a natural number in decimal notation.
 668 | export %inline
 669 | parseDecimalNat : ByteString -> Maybe Nat
 670 | parseDecimalNat (BS _ bv) = parseDecimalNat bv
 671 | 
 672 | export %inline
 673 | parseHexadecimalNat : ByteString -> Maybe Nat
 674 | parseHexadecimalNat (BS _ bv) = parseHexadecimalNat bv
 675 | 
 676 | export %inline
 677 | parseOctalNat : ByteString -> Maybe Nat
 678 | parseOctalNat (BS _ bv) = parseOctalNat bv
 679 | 
 680 | export %inline
 681 | parseBinaryNat : ByteString -> Maybe Nat
 682 | parseBinaryNat (BS _ bv) = parseBinaryNat bv
 683 | 
 684 | export %inline
 685 | parseInteger : ByteString -> Maybe Integer
 686 | parseInteger (BS _ bv) = parseInteger bv
 687 | 
 688 | export %inline
 689 | parseDouble : ByteString -> Maybe Double
 690 | parseDouble (BS _ bv) = parseDouble bv
 691 | 
 692 | --------------------------------------------------------------------------------
 693 | --          Reading and Writing Files
 694 | --------------------------------------------------------------------------------
 695 | 
 696 | export
 697 | readByteString : HasIO io => Nat -> File -> io (Either FileError ByteString)
 698 | readByteString max f = do
 699 |   Right (n ** ib) <- readIBuffer max f | Left x => pure (Left x)
 700 |   pure . Right $ BS n (BV ib 0 reflexive)
 701 | 
 702 | export %inline
 703 | writeByteVect :
 704 |      {n : _}
 705 |   -> {auto _ : HasIO io}
 706 |   -> File
 707 |   -> ByteVect n
 708 |   -> io (Either (FileError,Int) ())
 709 | writeByteVect h (BV buf o _) = writeIBuffer h o n buf
 710 | 
 711 | export %inline
 712 | writeByteString :
 713 |      {auto _ : HasIO io}
 714 |   -> File
 715 |   -> ByteString
 716 |   -> io (Either (FileError,Int) ())
 717 | writeByteString h (BS n bs) = writeByteVect h bs
 718 | 
 719 | --------------------------------------------------------------------------------
 720 | -- Using Builders
 721 | --------------------------------------------------------------------------------
 722 | 
 723 | export %inline
 724 | putByteString : Builder q => ByteString -> F1' q
 725 | putByteString (BS _ bv) = putByteVect bv
 726 | 
 727 | export %inline
 728 | getByteString : Builder q => F1 q ByteString
 729 | getByteString t = let ab # t := getBytes t in cast ab # t
 730 |