0 | module Data.ByteVect

  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

  9 | import public Data.Buffer.Core

 10 | import public Data.Buffer.Indexed

 11 | import public Data.Byte

 13 | %default total

 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

 31 | export %inline

 32 | fromIBuffer : IBuffer n -> ByteVect n

 33 | fromIBuffer b = BV b 0 reflexive

 41 | toIBuffer : {n : _} -> ByteVect n -> IBuffer n

 42 | toIBuffer (BV b 0 _) = take n b

 43 | toIBuffer (BV b o _) =

 44 |   run1 $ \t =>

 45 |    let mb # t := mbuffer1 n t

 46 |        _  # t := icopy b o 0 n mb t

 47 |     in unsafeFreeze mb t

 51 | public export

 52 | record ByteString where

 53 |   constructor BS

 54 |   size : Nat

 55 |   repr : ByteVect size

 58 | conv : {n : _} -> R1 rs (IBuffer n) -@ R1 rs ByteString

 59 | conv (v # t) = BS n (BV v 0 reflexive) # t

 63 | freezeByteString : {n : _} -> WithMBuffer n ByteString

 64 | freezeByteString r t = conv $ freeze r t

 71 | unsafeFreezeByteString : {n : _} -> WithMBuffer n ByteString

 72 | unsafeFreezeByteString r t = conv $ unsafeFreeze r t

 76 | freezeByteStringLTE : (m : Nat) -> (0 p : LTE m n) => WithMBuffer n ByteString

 77 | freezeByteStringLTE m r t = conv $ freezeLTE @{p} r m t

 84 | unsafeFreezeByteStringLTE : (m : Nat) -> (0 p : LTE m n) => WithMBuffer n ByteString

 85 | unsafeFreezeByteStringLTE m r t = conv $ unsafeFreezeLTE @{p} r m t

 88 | export %inline

 89 | at : ByteVect n -> Fin n -> Bits8

 90 | at (BV buf o lte) x = atOffset buf x o

 93 | export %inline

 94 | ix : ByteVect n -> (0 m : Nat) -> {auto x: Ix (S m) n} -> Bits8

 95 | ix bv _ = at bv (ixToFin x)

 98 | export %inline

 99 | atNat : ByteVect n -> (m : Nat) -> {auto 0 lt : LT m n} -> Bits8

100 | atNat bv x = at bv (natToFinLT x)

103 | fromEnd : {n : _} -> ByteVect n -> (m : Nat) -> {auto 0 lt : LT m n} -> Bits8

104 | fromEnd bs m = atNat bs (n `minus` S m) @{minusLT _ _ lt}

112 | empty : ByteVect 0

113 | empty = BV empty 0 %search

118 | pack : (as : List Bits8) -> ByteVect (length as)

119 | pack as = BV (bufferL as) 0 reflexive

124 | fromString : (s : String) -> ByteVect (cast $ stringByteLength s)

125 | fromString s = BV (fromString s) 0 reflexive

129 | toString : {n : _} -> ByteVect n -> String

130 | toString (BV buf o _) = toString buf o n

132 | export %inline

133 | {n : _} -> Interpolation (ByteVect n) where interpolate = toString

136 | export %inline

137 | singleton : Bits8 -> ByteVect 1

138 | singleton v = pack [v]

143 | toList : {n : _} -> (Bits8 -> a) -> ByteVect n -> List a

144 | toList f bs     = go Nil n

146 |   where

147 |     go : List a -> (x : Nat) -> (0 prf : LTE x n) => List a

148 |     go xs 0     = xs

149 |     go xs (S j) = go (f (atNat bs j) :: xs) j

152 | export %inline

153 | unpack : {n : _} -> ByteVect n -> List Bits8

154 | unpack = toList id

159 | export %inline

160 | {n : Nat} -> Show (ByteVect n) where

161 |   showPrec p bs = showCon p "pack" (showArg $ toList id bs)

169 | hcomp : {m,n : Nat} -> ByteVect m -> ByteVect n -> Ordering

170 | hcomp b1 b2 = go m n

172 |   where

173 |     go : (k,l : Nat) -> {auto a1 : Ix k m} -> {auto a2 : Ix l n} -> Ordering

174 |     go 0     0     = EQ

175 |     go 0     (S _) = LT

176 |     go (S _) 0     = GT

177 |     go (S k) (S j) = case compare (ix b1 k) (ix b2 j) of

178 |       EQ => go k j

179 |       r  => r

183 | heq : {m,n : Nat} -> ByteVect m -> ByteVect n -> Bool

184 | heq bs1 bs2 = hcomp bs1 bs2 == EQ

186 | export %inline

187 | {n : _} -> Eq (ByteVect n) where (==) = heq

189 | export %inline

190 | {n : _} -> Ord (ByteVect n) where compare = hcomp

197 | generate : (n : Nat) -> (Fin n -> Bits8) -> ByteVect n

198 | generate n f = BV (generate n f) 0 refl

201 | replicate : (n : Nat) -> Bits8 -> ByteVect n

202 | replicate n = generate n . const

210 | append : {m,n : _} -> ByteVect m -> ByteVect n -> ByteVect (m + n)

211 | append (BV src1 o1 lte1) (BV src2 o2 lte2) =

212 |   let buf := alloc (m+n) $ \r,t =>

213 |               let _ # t := icopy {n = m+n} src1 o1 0 m @{lte1} @{lteAddRight _} r t

214 |                   _ # t := icopy src2 o2 m n @{lte2} @{reflexive} r t

215 |                in unsafeFreeze r t

216 |    in BV buf 0 reflexive

219 | export %inline

220 | cons : {n : _} -> Bits8 -> ByteVect n -> ByteVect (S n)

221 | cons = append . singleton

224 | export %inline

225 | snoc : {n : _} -> Bits8 -> ByteVect n -> ByteVect (n + 1)

226 | snoc w bs = bs `append` singleton w

234 | head : ByteVect (S n) -> Bits8

235 | head bv = atNat bv 0

239 | tail : ByteVect (S n) -> ByteVect n

240 | tail (BV buf o p) = BV buf (S o) (ltePlusSuccRight p)

244 | uncons : ByteVect (S n) -> (Bits8, ByteVect n)

245 | uncons bs = (head bs, tail bs)

249 | last : {n : _} -> ByteVect (S n) -> Bits8

250 | last bs = atNat bs n

254 | init : ByteVect (S n) -> ByteVect n

255 | init (BV buf o p) = BV buf o (lteSuccLeft $ ltePlusSuccRight p)

259 | unsnoc : {n : _} -> ByteVect (S n) -> (Bits8, ByteVect n)

260 | unsnoc bs = (last bs, init bs)

269 | map : {n : _} -> (Bits8 -> Bits8) -> ByteVect n -> ByteVect n

270 | map f bs = generate n (\x => f $ at bs x)

274 | export %inline

275 | toUpper : {n : _} -> ByteVect n -> ByteVect n

276 | toUpper = map toUpper

280 | export %inline

281 | toLower : {n : _} -> ByteVect n -> ByteVect n

282 | toLower = map toLower

286 | reverse : {n : _} -> ByteVect n -> ByteVect n

287 | reverse bs = generate n (\x => fromEnd bs (finToNat x) @{finToNatLT _})

292 | all : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> Bool

293 | all p bv = go n

295 |   where

296 |     go : (c : Nat) -> (x : Ix c n) => Bool

297 |     go 0     = True

298 |     go (S k) = if p (ix bv k) then go k else False

303 | any : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> Bool

304 | any p bv = go n

306 |   where

307 |     go : (c : Nat) -> (x : Ix c n) => Bool

308 |     go 0     = False

309 |     go (S k) = if p (ix bv k) then True else go k

312 | export %inline

313 | elem : {n : _} -> Bits8 -> ByteVect n -> Bool

314 | elem b = any (b ==)

318 | foldl : {n : _} -> (a -> Bits8 -> a) -> a -> ByteVect n -> a

319 | foldl f ini bv = go n ini

321 |   where

322 |     go : (c : Nat) -> (v : a) -> (x : Ix c n) => a

323 |     go 0     v = v

324 |     go (S k) v = go k (f v $ ix bv k)

328 | foldr : {n : _} -> (Bits8 -> a -> a) -> a -> ByteVect n -> a

329 | foldr f ini bs = go n ini

331 |   where

332 |     go : (k : Nat) -> (v : a) -> (0 lt : LTE k n) => a

333 |     go 0     v = v

334 |     go (S k) v = go k (f (atNat bs k) v)

340 | findIndex : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> Maybe (Fin n)

341 | findIndex p bv = go n

343 |   where

344 |     go : (c : Nat) -> {auto x : Ix c n} -> Maybe (Fin n)

345 |     go 0     = Nothing

346 |     go (S k) = if p (ix bv k) then Just (ixToFin x) else go k

352 | elemIndex : {n : _} -> Bits8 -> ByteVect n -> Maybe (Fin n)

353 | elemIndex c = findIndex (c ==)

358 | find : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> Maybe Bits8

359 | find p bs = at bs <$> findIndex p bs

362 | isPrefixOf : {m,n : _} -> ByteVect m -> ByteVect n -> Bool

363 | isPrefixOf bv1 bv2 = go m n

365 |   where

366 |     go : (c1,c2 : Nat) -> {auto _ : Ix c1 m} -> {auto _ : Ix c2 n} -> Bool

367 |     go 0     _     = True

368 |     go _     0     = False

369 |     go (S x) (S y) = if ix bv1 x == ix bv2 y then go x y else False

372 | isSuffixOf : {m,n : _} -> ByteVect m -> ByteVect n -> Bool

373 | isSuffixOf bv1 bv2 = go m n

375 |   where

376 |     go : (o1,o2 : Nat) -> (0 _ : LTE o1 m) => (0 _ : LTE o2 n) => Bool

377 |     go 0     _     = True

378 |     go _     0     = False

379 |     go (S x) (S y) = if atNat bv1 x == atNat bv2 y then go x y else False

385 | findIndexOrLength : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> SubLength n

386 | findIndexOrLength p bv = go n

388 |   where

389 |     go : (c : Nat) -> {auto x : Ix c n} -> SubLength n

390 |     go 0     = fromIx x

391 |     go (S k) = if p (ix bv k) then fromIx x else go k

393 | findIndexOrLengthNL : {n : _} -> ByteVect n -> SubLength n

394 | findIndexOrLengthNL bv = go n

396 |   where

397 |     go : (c : Nat) -> {auto x : Ix c n} -> SubLength n

398 |     go 0     = fromIx x

399 |     go (S k) = case ix bv k of 10 => fromIx x; _ => go k

401 | findFromEndUntil : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> SubLength n

402 | findFromEndUntil p bv = go n

404 |   where

405 |     go : (k : Nat) -> (0 lt : LTE k n) => SubLength n

406 |     go 0     = Element 0 LTEZero

407 |     go (S k) = if p (atNat bv k) then (Element (S k) lt) else go k

409 | 0 substrPrf : LTE (s + l) n -> LTE (o + n) n2 -> LTE ((o + s) + l) n2

410 | substrPrf p q =

411 |   let pp := rewrite sym (plusAssociative o s l) in ltePlusRight o p

412 |    in transitive pp q

417 | export %inline

418 | substring :

419 |      (start,length : Nat)

420 |   -> ByteVect n

421 |   -> {auto 0 inBounds : LTE (start + length) n}

422 |   -> ByteVect length

426 | substring start len (BV buf o p) =

427 |   BV buf (o + start) (substrPrf inBounds p)

432 | substringFromTill :

433 |      (from, till : Nat)

434 |   -> {auto 0 lt1 : LTE from till}

435 |   -> {auto 0 lt2 : LTE till n}

436 |   -> ByteVect n

437 |   -> ByteVect (till `minus` from)

438 | substringFromTill f t bv =

439 |   substring f (t `minus` f) bv @{transitive (plusMinusLTE _ _ lt1) lt2}

444 | substringFromTo :

445 |      (from, to : Nat)

446 |   -> {auto 0 lte : LTE from to}

447 |   -> {auto 0 lt  : LT to n}

448 |   -> ByteVect n

449 |   -> ByteVect (S to `minus` from)

450 | substringFromTo f t bv = substringFromTill f (S t) bv

453 | generateMaybe : (n : Nat) -> (Fin n -> Maybe Bits8) -> ByteString

454 | generateMaybe n f = alloc n (go n n)

456 |   where

457 |     go : (k,m : Nat) -> (x : Ix k n) => (y : Ix m n) => WithMBuffer n ByteString

458 |     go (S k) (S m) r t =

459 |       case f (ixToFin x) of

460 |         Nothing => go k (S m) r t

461 |         Just v  => let _ # t := setIx r m v t in go k m r t

462 |     go _ _ r t = unsafeFreezeByteStringLTE (ixToNat y) @{ixLTE y} r t

465 | mapMaybe : {n : _} -> (Bits8 -> Maybe Bits8) -> ByteVect n -> ByteString

466 | mapMaybe f bv = generateMaybe n (f . at bv)

469 | filter : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> ByteString

470 | filter p = mapMaybe (\b => if p b then Just b else Nothing)

475 | take : (0 k : Nat) -> (0 lt : LTE k n) => ByteVect n -> ByteVect k

476 | take k (BV buf o p) =

477 |   -- p        : o + n <= bufLen

478 |   -- lt       : k     <= n

479 |   -- required : o + k <= bufLen

480 |   BV buf o (transitive (ltePlusRight o lt) p)

485 | takeEnd :

486 |      {n : _}

487 |   -> (k : Nat)

488 |   -> {auto 0 lt : LTE k n}

489 |   -> ByteVect n

490 |   -> ByteVect k

491 | takeEnd k (BV buf o p) =

492 |   -- p        : o + n             <= bufLen

493 |   -- lt       : k                 <= n

494 |   -- required : ((o + n) - k) + k <= bufLen

495 |   let 0 q := plusMinus' k (o + n) (lteAddLeft o lt)

496 |    in BV buf ((o + n) `minus` k) (rewrite q in p)

500 | drop : (k : Nat) -> (0 lt : LTE k n) => ByteVect n -> ByteVect (n `minus` k)

501 | drop k (BV buf o p) =

502 |   -- p        : o + n             <= bufLen

503 |   -- lt       : k                 <= n

504 |   -- required : (o + k) + (n - k) <= bufLen

505 |   let 0 q := cong (o +) (plusMinus k n lt)

506 |       0 r := plusAssociative o k (n `minus` k)

507 |    in BV buf (o + k) (rewrite (trans (sym r) q) in p)

511 | dropEnd :

512 |      (0 k : Nat)

513 |   -> {auto 0 lt : LTE k n}

514 |   -> ByteVect n

515 |   -> ByteVect (n `minus` k)

516 | dropEnd k (BV buf o p) =

517 |   -- p        : o + n       <= bufLen

518 |   -- lt       : k           <= n

519 |   -- required : o + (n - k) <= bufLen

520 |   BV buf o (transitive (ltePlusRight o $ minusLTE n k) p)

523 | splitAt :

524 |      {n : _}

525 |   -> (k : Nat)

526 |   -> {auto 0 lte : LTE k n}

527 |   -> ByteVect n

528 |   -> (ByteVect k, ByteVect (n `minus` k))

529 | splitAt k bs = (take k bs, drop k bs)

534 | takeWhile : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> ByteString

535 | takeWhile p bs =

536 |   let Element k _ = findIndexOrLength (not . p) bs

537 |    in BS k $ take k bs

542 | takeWhileEnd : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> ByteString

543 | takeWhileEnd f bs =

544 |   let Element k _ = findFromEndUntil (not . f) bs

545 |    in BS _ $ drop k bs

550 | dropWhile : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> ByteString

551 | dropWhile f bs =

552 |   let Element k _ = findIndexOrLength (not . f) bs

553 |    in BS _ $ drop k bs

558 | dropWhileEnd : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> ByteString

559 | dropWhileEnd f bs =

560 |   let Element k _ = findFromEndUntil (not . f) bs

561 |    in BS k $ take k bs

565 | trimLeft : {n : _} -> ByteVect n -> ByteString

566 | trimLeft = dropWhile isSpace

570 | trimRight : {n : _} -> ByteVect n -> ByteString

571 | trimRight = dropWhileEnd isSpace

575 | trim : {n : _} -> ByteVect n -> ByteString

576 | trim bs = let BS k bs' := trimLeft bs in trimRight bs'

578 | public export

579 | record BreakRes (n : Nat) where

580 |   constructor MkBreakRes

581 |   lenFst : Nat

582 |   lenSnd : Nat

583 |   fst    : ByteVect lenFst

584 |   snd    : ByteVect lenSnd

585 |   0 prf  : LTE (lenFst + lenSnd) n

588 | breakRes : {n : _} -> ByteVect n -> SubLength n -> BreakRes n

589 | breakRes bs (Element k p) =

590 |   let bs1 := take k bs

591 |       bs2 := drop k bs

592 |    in MkBreakRes k (n `minus` k) bs1 bs2 (plusMinusLTE k n p)

596 | export %inline

597 | break : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> BreakRes n

598 | break p bs = breakRes bs (findIndexOrLength p bs)

601 | export %inline

602 | breakNL : {n : _} -> ByteVect n -> BreakRes n

603 | breakNL bs = breakRes bs (findIndexOrLengthNL bs)

607 | export %inline

608 | breakEnd : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> BreakRes n

609 | breakEnd  p bs = breakRes bs (findFromEndUntil p bs)

613 | export %inline

614 | span : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> BreakRes n

615 | span p = break (not . p)

619 | export %inline

620 | spanEnd : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> BreakRes n

621 | spanEnd p bs = breakRes bs (findFromEndUntil (not . p) bs)

626 | substringIndex : {k,n : _} -> ByteVect k -> ByteVect n -> SubLength n

627 | substringIndex sep bv = go n

629 |   where

630 |     go : (c : Nat) -> {auto x : Ix c n} -> SubLength n

631 |     go 0     = fromIx x

632 |     go (S k) =

633 |       if isPrefixOf sep (drop (ixToNat x) @{ixLTE x} bv) then fromIx x else go k

638 | export %inline

639 | breakAtSubstring : {k,n : _} -> ByteVect k -> ByteVect n -> BreakRes n

640 | breakAtSubstring sep bs = breakRes bs (substringIndex sep bs)

647 | splitWith : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> List ByteString

648 | splitWith p bs = go Lin n bs (sizeAccessible n)

650 |   where

651 |     go :

652 |          SnocList ByteString

653 |       -> (m : Nat)

654 |       -> ByteVect m

655 |       -> (0 acc : SizeAccessible m)

656 |       -> List ByteString

657 |     go sb m bs' (Access rec) = case break p bs' of

658 |       MkBreakRes l1 0      b1 _  p => sb <>> [BS l1 b1]

659 |       MkBreakRes l1 (S l2) b1 b2 p =>

660 |         go (sb :< BS l1 b1) l2 (tail b2) (rec l2 $ ltPlusSuccRight' _ p)

664 | splitWithNonEmpty : {n : _} -> (Bits8 -> Bool) -> ByteVect n -> List ByteString

665 | splitWithNonEmpty p = filter ((/= Z) . size) . splitWith p

673 | export %inline

674 | split : {n : _} -> Bits8 -> ByteVect n -> List ByteString

675 | split b = splitWith (b ==)

679 | splitNonEmpty : {n : _} -> Bits8 -> ByteVect n -> List ByteString

680 | splitNonEmpty p = filter ((/= Z) . size) . split p

683 | lines : {n : _} -> ByteVect n -> List ByteString

684 | lines bs = go Lin n bs (sizeAccessible n)

686 |   where

687 |     go :

688 |          SnocList ByteString

689 |       -> (m : Nat)

690 |       -> ByteVect m

691 |       -> (0 acc : SizeAccessible m)

692 |       -> List ByteString

693 |     go sb m bs' (Access rec) = case breakNL bs' of

694 |       MkBreakRes l1 0      b1 _  p => sb <>> [BS l1 b1]

695 |       MkBreakRes l1 (S l2) b1 b2 p =>

696 |         go (sb :< BS l1 b1) l2 (tail b2) (rec l2 $ ltPlusSuccRight' _ p)

698 | 0 blocksLemma1 : (m,n : Nat) -> LT (S n `minus` S m) (S n)

699 | blocksLemma1 m n = LTESucc $ minusLTE _ _

701 | 0 blocksLemma2 : (m,n : Nat) -> LTE (S k) n -> LT (n `minus` S m) n

702 | blocksLemma2 m (S _) (LTESucc _) = blocksLemma1 m _

713 | splitAtSubstring :

714 |      {k,n : _}

715 |   -> (sep : ByteVect k)

716 |   -> (val : ByteVect n)

717 |   -> List ByteString

718 | splitAtSubstring {k = 0}   sep bv = [BS _ bv]

719 | splitAtSubstring {k = S m} sep bv = go [<] bv (sizeAccessible n)

720 |   where

721 |     go : {o : _}

722 |       -> SnocList ByteString

723 |       -> (body  : ByteVect o)

724 |       -> (0 acc : SizeAccessible o)

725 |       -> List ByteString

726 |     go sb body (Access rec) =

727 |       let MkBreakRes l1 l2 b1 b2 p1 := breakAtSubstring sep body

728 |        in case tryLTE {n = l2} (S m) of

729 |             Nothing0 => sb <>> [BS l1 b1]

730 |             Just0 p2  =>

731 |               let 0 p3 := lteAddLeft {m = l2} l1 reflexive

732 |                   0 p4 := blocksLemma2 m l2 p2

733 |                   0 p5 := transitive (transitive p4 p3) p1

734 |                in go (sb :< BS l1 b1) (drop (S m) b2) (rec _ p5)

737 | isInfixOf : {m,n : _} -> ByteVect m -> ByteVect n -> Bool

738 | isInfixOf bv1 bv2 = m == 0 || go n

740 |   where

741 |     go : (c : Nat) -> (x : Ix c n) => Bool

742 |     go 0     = False

743 |     go (S k) = isPrefixOf bv1 (drop (ixToNat x) @{ixLTE x} bv2) || go k

751 | parseAnyNat :

752 |      {n : _}

753 |   -> (base : Nat)

754 |   -> {auto 0 p1 : LTE 2 base}

755 |   -> {auto 0 p2 : LTE base 16}

756 |   -> ByteVect n

757 |   -> Maybe Nat

758 | parseAnyNat {n = Z} _    bv = Nothing

759 | parseAnyNat         base bv = go n 0

761 |   where

762 |     go : (c,res : Nat) -> (x : Ix c n) => Maybe Nat

763 |     go 0     res = Just res

764 |     go (S k) res =

765 |       let Just n := fromHexDigit $ ix bv k | Nothing => Nothing

766 |        in if n < base then go k (res * base + n) else Nothing

769 | export %inline

770 | parseDecimalNat : {n : _} -> ByteVect n -> Maybe Nat

771 | parseDecimalNat {n = Z} bv = Nothing

772 | parseDecimalNat         bv = go n 0

774 |   where

775 |     go : (c,res : Nat) -> (x : Ix c n) => Maybe Nat

776 |     go 0     res = Just res

777 |     go (S k) res =

778 |       let Just n := fromDigit $ ix bv k | Nothing => Nothing

779 |        in go k (res * 10 + n)

781 | export %inline

782 | parseHexadecimalNat : {n : _} -> ByteVect n -> Maybe Nat

783 | parseHexadecimalNat = parseAnyNat 10

785 | export %inline

786 | parseOctalNat : {n : _} -> ByteVect n -> Maybe Nat

787 | parseOctalNat = parseAnyNat 8

789 | export %inline

790 | parseBinaryNat : {n : _} -> ByteVect n -> Maybe Nat

791 | parseBinaryNat = parseAnyNat 2

794 | parseInteger : {n : _} -> ByteVect n -> Maybe Integer

795 | parseInteger {n = Z}   _  = Nothing

796 | parseInteger {n = S _} bv = case head bv of

797 |   43 => cast          <$> parseDecimalNat (tail bv) -- '+'

798 |   45 => negate . cast <$> parseDecimalNat (tail bv) -- '-'

799 |   _  => cast <$> parseDecimalNat bv

804 | isE : Bits8 -> Bool

805 | isE 69  = True

806 | isE 101 = True

807 | isE _   = False

809 | fract : {n : _} -> ByteVect n -> Maybe Double

810 | fract bv =

811 |   let Just k := parseDecimalNat bv | Nothing => Nothing

812 |    in Just (cast k / (pow 10 $ cast n))

814 | exp : {n : _} -> ByteVect n -> Maybe Double

815 | exp bv =

816 |   let Just exp := parseInteger bv | Nothing => Nothing

817 |    in Just $ pow 10.0 (cast exp)

819 | parseDotted : {n : _} -> ByteVect n -> Maybe Double

820 | parseDotted bv = go 0 0 n

821 |   where

822 |     go : (v,exp,c : Nat) -> (x : Ix c n) => Maybe Double

823 |     go v exp 0     = case exp of

824 |       0 => Just $ cast v

825 |       _ => Just $ cast v / cast exp

826 |     go v exp (S k) =

827 |       case ix bv k of

828 |         48 => go (v * 10 + 0) (exp * 10) k

829 |         49 => go (v * 10 + 1) (exp * 10) k

830 |         50 => go (v * 10 + 2) (exp * 10) k

831 |         51 => go (v * 10 + 3) (exp * 10) k

832 |         52 => go (v * 10 + 4) (exp * 10) k

833 |         53 => go (v * 10 + 5) (exp * 10) k

834 |         54 => go (v * 10 + 6) (exp * 10) k

835 |         55 => go (v * 10 + 7) (exp * 10) k

836 |         56 => go (v * 10 + 8) (exp * 10) k

837 |         57 => go (v * 10 + 9) (exp * 10) k

838 |         46 => case exp of

839 |           0 => go v 1 k

840 |           _ => Nothing

841 |         _  => Nothing

843 | parsePosDbl : {n : _} -> ByteVect n -> Maybe Double

844 | parsePosDbl bv = case parseDotted bv of

845 |   Just v  => Just v

846 |   Nothing => case break isE bv of

847 |     MkBreakRes lf (S _) dotStr expStr _ =>

848 |       let Just fract := parseDotted dotStr | Nothing => Nothing

849 |           Just e     := exp (tail expStr)  | Nothing => Nothing

850 |        in Just $ fract * e

851 |     MkBreakRes _ 0 _ _ _ => Nothing

854 | parseDouble : {n : _} -> ByteVect n -> Maybe Double

855 | parseDouble {n = Z}   _  = Nothing

856 | parseDouble {n = S _} bv = case head bv of

857 |   43 => parsePosDbl (tail bv)             -- '+'

858 |   45 => negate  <$> parsePosDbl (tail bv) -- '-'

859 |   _  => parsePosDbl bv

865 | export %inline

866 | putByteVect : Builder q => {n : _} -> ByteVect n -> F1' q

867 | putByteVect (BV buf off _) = putBytesFrom off n buf