1 | module Data.RRBVector

   3 | import public Data.RRBVector.Internal

   5 | import Data.Array

   6 | import Data.Array.Core

   7 | import Data.Array.Index

   8 | import Data.Array.Indexed

   9 | import Data.Bits

  10 | import Data.Linear.Ref1

  11 | import Data.Linear.Traverse1

  12 | import Data.List

  13 | import Data.List1

  14 | import Data.Maybe

  15 | import Data.SnocList

  16 | import Data.Vect

  17 | import Data.Zippable

  18 | import Syntax.T1 as T1

  20 | %hide Prelude.null

  21 | %hide Prelude.Ops.infixr.(<|)

  22 | %hide Prelude.Ops.infixl.(|>)

  24 | %default total

  31 | infixr 5 ><

  34 | infixr 5 <|

  37 | infixl 5 |>

  50 | castIArray :  {m, n : Nat}

  51 |            -> (0 prf : m = n)

  52 |            -> IArray m a

  53 |            -> IArray n a

  54 | castIArray Refl arr =

  55 |   arr

  62 | 0 lteReflNat :  (n : Nat)

  63 |              -> LTE n n

  64 | lteReflNat Z     =

  65 |   LTEZero

  66 | lteReflNat (S n) =

  67 |   LTESucc (lteReflNat n)

  72 | 0 plusOneRight :  (n : Nat)

  73 |                -> plus n 1 = S n

  74 | plusOneRight Z     =

  75 |   Refl

  76 | plusOneRight (S n) =

  77 |   cong S (plusOneRight n)

  86 | childrenSnoc :  {n : Nat}

  87 |              -> IArray n (Tree a)

  88 |              -> Tree a

  89 |              -> Children a

  90 | childrenSnoc {n} xs x =

  91 |   let arr  : IArray (plus n 1) (Tree a)

  92 |       arr  = append xs (fill 1 x)

  93 |       arr' : IArray (S n) (Tree a)

  94 |       arr' = castIArray (plusOneRight n) arr

  95 |     in MkChildren {n = S n} {nonEmpty = LTESucc LTEZero} {withinBlock = believe_me ()} arr'

 106 | childrenCons :  {n : Nat}

 107 |              -> Tree a

 108 |              -> IArray n (Tree a)

 109 |              -> Children a

 110 | childrenCons {n} x xs =

 111 |   MkChildren {n = S n} {nonEmpty = LTESucc LTEZero} {withinBlock = believe_me ()} (append (fill 1 x) xs)

 120 | childrenFromArray :  Array (Tree a)

 121 |                   -> Children a

 122 | childrenFromArray (A Z _) =

 123 |   assert_total (idris_crash "Data.RRBVector.childrenFromArray: empty child array")

 124 | childrenFromArray (A (S n) arr) =

 125 |   MkChildren {nonEmpty = LTESucc LTEZero} {withinBlock = believe_me ()} arr

 129 | private %inline

 130 | lastFin :  {n : Nat}

 131 |         -> Fin (S n)

 132 | lastFin {n = Z} =

 133 |   FZ

 134 | lastFin {n = S k} =

 135 |   FS lastFin

 144 | empty : RRBVector a

 145 | empty = Empty

 150 | singleton :  a

 151 |           -> RRBVector a

 152 | singleton x = Root 1 0 (Leaf $ A 1 $ fill 1 x)

 161 | fromList :

 162 |      List a

 163 |   -> RRBVector a

 164 | fromList []  =

 165 |   Empty

 166 | fromList [x] =

 167 |   singleton x

 168 | fromList xs  =

 169 |   case nodes Leaf xs of

 170 |     [tree] =>

 171 |       Root (treeSize 0 tree) 0 tree

 172 |     xs' =>

 173 |       assert_smaller xs (iterateNodes blockshift xs')

 174 |   where

 175 |     ||| Build leaf-sized nodes from a list.

 181 |     nodes :  (Array a -> Tree a)

 182 |           -> List a

 183 |           -> List (Tree a)

 184 |     nodes f trees =

 185 |       let (tree, rest) = unsafeAlloc blocksize (go {n = blocksize} blocksize f trees)

 186 |         in case rest of

 187 |             [] =>

 188 |               [tree]

 189 |             rest' =>

 190 |               tree :: nodes f (assert_smaller trees rest')

 191 |       where

 192 |         ||| Fill one array from left to right.

 201 |         go :  {n : Nat}

 202 |            -> (remaining : Nat)

 203 |            -> {auto pos : Ix remaining n}

 204 |            -> (Array a -> Tree a)

 205 |            -> List a

 206 |            -> WithMArray n a (Tree a, List a)

 207 |         go {n} remaining {pos} f [] r      = T1.do

 208 |           res <- unsafeFreeze r

 209 |           let written : Nat

 210 |               written = ixToNat pos

 211 |           pure

 212 |             ( f $

 213 |                 force $

 214 |                   take written $

 215 |                     A n res

 216 |             , []

 217 |             )

 218 |         go {n} Z         {pos} f xs        r = T1.do

 219 |           res <- unsafeFreeze r

 220 |           pure

 221 |             ( f $ A n res

 222 |             , xs

 223 |             )

 224 |         go {n} (S k)     {pos} f (x :: xs) r =

 225 |           let idx : Fin n

 226 |               idx = ixToFin pos

 227 |            in T1.do

 228 |                 set r idx x

 229 |                 assert_total (go {n} k {pos = IS pos} f xs r)

 230 |     ||| Build internal RRB nodes from a list of child trees.

 235 |     nodes' :  (Array (Tree a) -> Tree a)

 236 |            -> List (Tree a)

 237 |            -> List (Tree a)

 238 |     nodes' f trees =

 239 |       let (tree, rest) =

 240 |             unsafeAlloc blocksize (go {n = blocksize} blocksize f trees)

 241 |        in case rest of

 242 |             [] =>

 243 |               [tree]

 244 |             rest' =>

 245 |               tree :: nodes' f (assert_smaller trees rest')

 246 |       where

 247 |         ||| Fill one internal-node child array from left to right.

 249 |         go :  {n : Nat}

 250 |            -> (remaining : Nat)

 251 |            -> {auto pos : Ix remaining n}

 252 |            -> (Array (Tree a) -> Tree a)

 253 |            -> List (Tree a)

 254 |            -> WithMArray n (Tree a) (Tree a, List (Tree a))

 255 |         go {n} remaining {pos} f []        r = T1.do

 256 |           res <- unsafeFreeze r

 257 |           let written : Nat

 258 |               written = ixToNat pos

 259 |           pure

 260 |             ( f $

 261 |                 force $

 262 |                   take written $

 263 |                     A n res

 264 |             , []

 265 |             )

 266 |         go {n} Z         {pos} f xs        r = T1.do

 267 |           res <- unsafeFreeze r

 268 |           pure

 269 |             ( f $ A n res

 270 |             , xs

 271 |             )

 272 |         go {n} (S k)     {pos} f (x :: xs) r =

 273 |           let idx : Fin n

 274 |               idx = ixToFin pos

 275 |            in T1.do

 276 |                 set r idx x

 277 |                 assert_total (go {n} k {pos = IS pos} f xs r)

 278 |     ||| Repeatedly group child trees into balanced internal nodes until only a

 281 |     iterateNodes :  Shift

 282 |                  -> List (Tree a)

 283 |                  -> RRBVector a

 284 |     iterateNodes sh trees =

 285 |       case nodes' (\arr => Balanced (childrenFromArray arr)) trees of

 286 |         [tree] =>

 287 |           Root (treeSize sh tree) sh tree

 288 |         trees' =>

 289 |           iterateNodes (up sh) (assert_smaller trees trees')

 294 | replicate :  Nat

 295 |           -> a

 296 |           -> RRBVector a

 297 | replicate n x =

 298 |   case compare n 0 of

 299 |     LT =>

 300 |       Empty

 301 |     EQ =>

 302 |       Empty

 303 |     GT =>

 304 |       case compare n blocksize of

 305 |         LT =>

 306 |           Root n 0 (Leaf $ A n $ fill n x)

 307 |         EQ =>

 308 |           Root n 0 (Leaf $ A n $ fill n x)

 309 |         GT =>

 310 |           let size' = integerToNat $ (natToInteger $ minus n 1) .&. (natToInteger $ plus blockmask 1)

 311 |             in iterateNodes blockshift (Leaf $ A blocksize $ fill blocksize x) (Leaf $ A size' $ fill size' x)

 312 |   where

 313 |     iterateNodes :  Shift

 314 |                  -> Tree a

 315 |                  -> Tree a

 316 |                  -> RRBVector a

 317 |     iterateNodes sh full rest =

 318 |       let subtreesm1   = (natToInteger $ minus n 1) `shiftR` sh

 319 |           restsize     = integerToNat $ subtreesm1 .&. natToInteger blockmask

 320 |           restchildren : Children a

 321 |           restchildren = childrenSnoc (fill restsize full) rest

 322 |           rest'        : Tree a

 323 |           rest'        = Balanced restchildren

 324 |        in case compare subtreesm1 (natToInteger blocksize) of

 325 |             LT =>

 326 |               Root n sh rest'

 327 |             EQ =>

 328 |               let fullchildren : Children a

 329 |                   fullchildren = MkChildren {n = blocksize} {nonEmpty = believe_me ()} {withinBlock = lteReflNat blocksize} (fill blocksize full)

 330 |                   full'        = Balanced fullchildren

 331 |                 in iterateNodes (up sh) (assert_smaller full full') (assert_smaller rest rest')

 332 |             GT =>

 333 |               let fullchildren : Children a

 334 |                   fullchildren = MkChildren {n = blocksize} {nonEmpty = believe_me ()} {withinBlock = lteReflNat blocksize} (fill blocksize full)

 335 |                   full'        = Balanced fullchildren

 336 |                 in iterateNodes (up sh) (assert_smaller full full') (assert_smaller rest rest')

 345 | toList :  RRBVector a

 346 |        -> List a

 347 | toList Empty           =

 348 |   []

 349 | toList (Root _ _ tree) =

 350 |   treeToList tree

 351 |   where

 352 |     treeToList :  Tree a

 353 |                -> List a

 354 |     treeToList (Balanced (MkChildren {n} trees))            =

 355 |       assert_total (concat (map treeToList (toList (A n trees))))

 356 |     treeToList (Unbalanced (MkRelaxedChildren {n} trees _)) =

 357 |       assert_total (concat (map treeToList (toList (A n trees))))

 358 |     treeToList (Leaf arr)                                   =

 359 |       toList arr

 366 | foldl :  (b -> a -> b)

 367 |       -> b

 368 |       -> RRBVector a

 369 |       -> b

 370 | foldl f acc = go

 371 |   where

 372 |     foldlTree :  b

 373 |               -> Tree a

 374 |               -> b

 375 |     foldlTree acc' (Balanced (MkChildren {n} trees))            =

 376 |       assert_total (foldl foldlTree acc' (A n trees))

 377 |     foldlTree acc' (Unbalanced (MkRelaxedChildren {n} trees _)) =

 378 |       assert_total (foldl foldlTree acc' (A n trees))

 379 |     foldlTree acc' (Leaf arr)                                   =

 380 |       assert_total (foldl f acc' arr)

 381 |     go :  RRBVector a

 382 |        -> b

 383 |     go Empty           =

 384 |       acc

 385 |     go (Root _ _ tree) =

 386 |       assert_total (foldlTree acc tree)

 389 | foldr :  (a -> b -> b)

 390 |       -> b

 391 |       -> RRBVector a

 392 |       -> b

 393 | foldr f acc = go

 394 |   where

 395 |     foldrTree :  Tree a

 396 |               -> b

 397 |               -> b

 398 |     foldrTree (Balanced (MkChildren {n} trees))            acc' =

 399 |       assert_total (foldr foldrTree acc' (A n trees))

 400 |     foldrTree (Unbalanced (MkRelaxedChildren {n} trees _)) acc' =

 401 |       assert_total (foldr foldrTree acc' (A n trees))

 402 |     foldrTree (Leaf arr)                                   acc' =

 403 |       assert_total (foldr f acc' arr)

 404 |     go :  RRBVector a

 405 |        -> b

 406 |     go Empty           =

 407 |       acc

 408 |     go (Root _ _ tree) =

 409 |       assert_total (foldrTree tree acc)

 418 | null :  RRBVector a

 419 |      -> Bool

 420 | null Empty = True

 421 | null _     = False

 426 | length :  RRBVector a

 427 |        -> Nat

 428 | length Empty        = 0

 429 | length (Root s _ _) = s

 438 | lookup :  Nat

 439 |        -> RRBVector a

 440 |        -> Maybe a

 441 | lookup _ Empty               =

 442 |   Nothing

 443 | lookup i (Root size sh tree) =

 444 |   case i < size of

 445 |     False =>

 446 |       Nothing

 447 |     True =>

 448 |       Just (lookupTree i sh tree)

 449 |   where

 450 |     lookupTree :  Nat

 451 |                -> Shift

 452 |                -> Tree a

 453 |                -> a

 454 |     lookupTree i sh (Balanced (MkChildren {n} children))                           =

 455 |       let childidx : Nat

 456 |           childidx = radixIndex i sh

 457 |           0 childLT : LT childidx n

 458 |           childLT = believe_me ()

 459 |           child : Fin n

 460 |           child = natToFinLT childidx @{childLT}

 461 |         in assert_total (lookupTree i (down sh) (at children child))

 462 |     lookupTree i sh (Unbalanced (MkRelaxedChildren {n} {nonEmpty} children sizes)) =

 463 |       let MkRelaxedIndex child offset = relaxedRadixIndex {n} {nonEmpty} sizes i sh

 464 |         in assert_total (lookupTree offset (down sh) (at children child))

 465 |     lookupTree i _  (Leaf (A n elems))                                             =

 466 |       let leafidx  : Nat

 467 |           leafidx  = integerToNat ((natToInteger i) .&. natToInteger blockmask)

 468 |           0 leafLT : LT leafidx n

 469 |           leafLT   = believe_me ()

 470 |         in atNat elems leafidx @{leafLT}

 475 | (!?) :  RRBVector a

 476 |      -> Nat

 477 |      -> Maybe a

 478 | (!?) = flip lookup

 485 | update :  Nat

 486 |        -> a

 487 |        -> RRBVector a

 488 |        -> RRBVector a

 489 | update _ _ Empty                 =

 490 |   Empty

 491 | update i x v@(Root size sh tree) =

 492 |   case i < size of

 493 |     False =>

 494 |       v

 495 |     True =>

 496 |       Root size sh (updateTree i sh tree)

 497 |   where

 498 |     updateTree :  Nat

 499 |                -> Shift

 500 |                -> Tree a

 501 |                -> Tree a

 502 |     updateTree i sh (Balanced (MkChildren {n} {nonEmpty} {withinBlock} children))                =

 503 |       let childidx  : Nat

 504 |           childidx  = radixIndex i sh

 505 |           0 childLT : LT childidx n

 506 |           childLT   = believe_me ()

 507 |           child     : Fin n

 508 |           child     = natToFinLT childidx @{childLT}

 509 |           children' = updateAt child (updateTree i (down sh)) children

 510 |         in assert_total (Balanced (MkChildren {nonEmpty = nonEmpty} {withinBlock = withinBlock} children'))

 511 |     updateTree i sh (Unbalanced (MkRelaxedChildren {n} {nonEmpty} {withinBlock} children sizes)) =

 512 |       let MkRelaxedIndex child offset = relaxedRadixIndex {n} {nonEmpty} sizes i sh

 513 |           children'                   = updateAt child (updateTree offset (down sh)) children

 514 |         in assert_total (Unbalanced (MkRelaxedChildren {nonEmpty = nonEmpty} {withinBlock = withinBlock} children' sizes))

 515 |     updateTree i _  (Leaf (A n elems))                                                           =

 516 |       let leafidx  : Nat

 517 |           leafidx  = integerToNat ((natToInteger i) .&. natToInteger blockmask)

 518 |           0 leafLT : LT leafIdx n

 519 |           leafLT   = believe_me ()

 520 |           idx      : Fin n

 521 |           idx      = natToFinLT leafidx @{leafLT}

 522 |         in Leaf (A n (setAt idx x elems))

 529 | adjust :  Nat

 530 |        -> (a -> a)

 531 |        -> RRBVector a

 532 |        -> RRBVector a

 533 | adjust _ _ Empty                 =

 534 |   Empty

 535 | adjust i f v@(Root size sh tree) =

 536 |   case i < size of

 537 |     False =>

 538 |       v

 539 |     True  =>

 540 |       Root size sh (adjustTree i sh tree)

 541 |   where

 542 |     adjustTree :  Nat

 543 |                -> Shift

 544 |                -> Tree a

 545 |                -> Tree a

 546 |     adjustTree i sh (Balanced (MkChildren {n} {nonEmpty} {withinBlock} children))                =

 547 |       let childidx  : Nat

 548 |           childidx  = radixIndex i sh

 549 |           0 childLT : LT childidx n

 550 |           childLT   = believe_me ()

 551 |           child     : Fin n

 552 |           child     = natToFinLT childidx @{childLT}

 553 |           children' = updateAt child (adjustTree i (down sh)) children

 554 |         in assert_total (Balanced (MkChildren {nonEmpty = nonEmpty} {withinBlock = withinBlock} children'))

 555 |     adjustTree i sh (Unbalanced (MkRelaxedChildren {n} {nonEmpty} {withinBlock} children sizes)) =

 556 |       let MkRelaxedIndex child offset = relaxedRadixIndex {n} {nonEmpty} sizes i sh

 557 |           children'                   = updateAt child (adjustTree offset (down sh)) children

 558 |         in assert_total (Unbalanced (MkRelaxedChildren {nonEmpty = nonEmpty} {withinBlock = withinBlock} children' sizes))

 559 |     adjustTree i _  (Leaf (A n elems))                                                           =

 560 |       let leafidx  : Nat

 561 |           leafidx  = integerToNat ((natToInteger i) .&. natToInteger blockmask)

 562 |           0 leafLT : LT leafidx n

 563 |           leafLT   = believe_me ()

 564 |           idx      : Fin n

 565 |           idx      = natToFinLT leafidx @{leafLT}

 566 |         in Leaf (A n (updateAt idx f elems))

 569 | normalize :  RRBVector a

 570 |           -> RRBVector a

 571 | normalize (Root size sh (Balanced (MkChildren {n = 1} children)))            =

 572 |   assert_total (normalize (Root size (down sh) (at children FZ)))

 573 | normalize (Root size sh (Unbalanced (MkRelaxedChildren {n = 1} children _))) =

 574 |   assert_total (normalize (Root size (down sh) (at children FZ)))

 575 | normalize v =

 576 |   v

 587 | takeTree :  Nat

 588 |          -> Shift

 589 |          -> Tree a

 590 |          -> Tree a

 591 | takeTree i sh (Balanced (MkChildren {n} children))                           =

 592 |   let childidx  : Nat

 593 |       childidx  = radixIndex i sh

 594 |       0 childLT : LT childidx n

 595 |       childLT   = believe_me ()

 596 |       prefix'   : IArray (S childidx) (Tree a)

 597 |       prefix'   = force (take (S childidx) children @{childLT})

 598 |       prefix''  : IArray (S childidx) (Tree a)

 599 |       prefix''  = updateAt (lastFin {n = childidx}) (takeTree i (down sh)) prefix'

 600 |     in assert_total (Balanced (MkChildren {n = S childidx} {nonEmpty = LTESucc LTEZero} {withinBlock = believe_me ()} prefix''))

 601 | takeTree i sh (Unbalanced (MkRelaxedChildren {n} {nonEmpty} children sizes)) =

 602 |   let MkRelaxedIndex child subidx = relaxedRadixIndex {n} {nonEmpty} sizes i sh

 603 |       childidx    : Nat

 604 |       childidx    = finToNat child

 605 |       0 prefixLTE : LTE (S childidx) n

 606 |       prefixLTE   = believe_me ()

 607 |       prefix'     : IArray (S childidx) (Tree a)

 608 |       prefix'     = force (take (S childidx) children @{prefixLTE})

 609 |       prefix''    : IArray (S childidx) (Tree a)

 610 |       prefix''    = updateAt (lastFin {n = childidx}) (takeTree subidx (down sh)) prefix'

 611 |       bounded     : Children a

 612 |       bounded     = MkChildren {n = S childidx} {nonEmpty = LTESucc LTEZero} {withinBlock = believe_me ()} prefix''

 613 |     in assert_total (computeSizes sh bounded)

 614 | takeTree i _  (Leaf (A n elems))                                             =

 615 |   let leafidx    : Nat

 616 |       leafidx    = integerToNat ((natToInteger i) .&. natToInteger blockmask)

 617 |       count      : Nat

 618 |       count      = S leafidx

 619 |       0 countLTE : LTE count n

 620 |       countLTE   = believe_me ()

 621 |       elems'     : IArray count a

 622 |       elems'     = force (take count elems @{countLTE})

 623 |     in Leaf (A count elems')

 635 | dropTree :  Nat

 636 |          -> Shift

 637 |          -> Tree a

 638 |          -> Tree a

 639 | dropTree i sh (Balanced (MkChildren {n} children))                           =

 640 |   let childidx            : Nat

 641 |       childidx            = radixIndex i sh

 642 |       remaining           : Nat

 643 |       remaining           = minus n childidx

 644 |       children'           : IArray remaining (Tree a)

 645 |       children'           = force (drop childidx children)

 646 |       0 remainingpositive : LT 0 remaining

 647 |       remainingpositive   = believe_me ()

 648 |       zero                : Fin remaining

 649 |       zero                = natToFinLT 0 @{remainingpositive}

 650 |       children''          : IArray remaining (Tree a)

 651 |       children''          = updateAt zero (dropTree i (down sh)) children'

 652 |       bounded             : Children a

 653 |       bounded             = MkChildren {n = remaining} {nonEmpty = remainingpositive} {withinBlock = believe_me ()} children''

 654 |     in assert_total (computeSizes sh bounded)

 655 | dropTree i sh (Unbalanced (MkRelaxedChildren {n} {nonEmpty} children sizes)) =

 656 |   let MkRelaxedIndex child subidx = relaxedRadixIndex {n} {nonEmpty} sizes i sh

 657 |       childidx                    : Nat

 658 |       childidx                    = finToNat child

 659 |       remaining                   : Nat

 660 |       remaining                   = minus n childidx

 661 |       children'                   : IArray remaining (Tree a)

 662 |       children'                   = force (drop childidx children)

 663 |       0 remainingpositive         : LT 0 remaining

 664 |       remainingpositive           = believe_me ()

 665 |       zero                        : Fin remaining

 666 |       zero                        = natToFinLT 0 @{remainingpositive}

 667 |       children''                  : IArray remaining (Tree a)

 668 |       children''                  = updateAt zero (dropTree subidx (down sh)) children'

 669 |       bounded                     : Children a

 670 |       bounded                     = MkChildren {n = remaining} {nonEmpty = remainingpositive} {withinBlock = believe_me ()} children''

 671 |     in assert_total (computeSizes sh bounded)

 672 | dropTree i _  (Leaf (A n elems))                                             =

 673 |   let offset    : Nat

 674 |       offset    = integerToNat ((natToInteger i) .&. natToInteger blockmask)

 675 |       remaining : Nat

 676 |       remaining = minus n offset

 677 |       elems'    : IArray remaining a

 678 |       elems'    = force (drop offset elems)

 679 |     in Leaf (A remaining elems')

 685 | take :  Nat

 686 |      -> RRBVector a

 687 |      -> RRBVector a

 688 | take _ Empty                 =

 689 |   empty

 690 | take n v@(Root size sh tree) =

 691 |   case compare n 0 of

 692 |     LT =>

 693 |       empty

 694 |     EQ =>

 695 |       empty

 696 |     GT =>

 697 |       case compare n size of

 698 |         LT =>

 699 |           normalize $ Root n sh (takeTree (minus n 1) sh tree)

 700 |         EQ =>

 701 |           v

 702 |         GT =>

 703 |           v

 709 | drop :  Nat

 710 |      -> RRBVector a

 711 |      -> RRBVector a

 712 | drop _ Empty                 =

 713 |   empty

 714 | drop n v@(Root size sh tree) =

 715 |   case compare n 0 of

 716 |     LT =>

 717 |       v

 718 |     EQ =>

 719 |       v

 720 |     GT =>

 721 |       case compare n size of

 722 |         LT =>

 723 |           normalize $ Root (minus size n) sh (dropTree n sh tree)

 724 |         EQ =>

 725 |           empty

 726 |         GT =>

 727 |           empty

 732 | splitAt :  Nat

 733 |         -> RRBVector a

 734 |         -> (RRBVector a, RRBVector a)

 735 | splitAt _ Empty                 = (Empty, Empty)

 736 | splitAt n v@(Root size sh tree) =

 737 |   case compare n 0 of

 738 |     LT =>

 739 |       (empty, v)

 740 |     EQ =>

 741 |       (empty, v)

 742 |     GT =>

 743 |       case compare n size of

 744 |         LT =>

 745 |           let left  = normalize $ Root n sh (takeTree (minus n 1) sh tree)

 746 |               right = normalize $ Root (minus size n) sh (dropTree n sh tree)

 747 |             in (left, right)

 748 |         EQ =>

 749 |           (v, empty)

 750 |         GT =>

 751 |           (v, empty)

 760 | viewl :  RRBVector a

 761 |       -> Maybe (a, RRBVector a)

 762 | viewl Empty             =

 763 |   Nothing

 764 | viewl v@(Root _ _ tree) =

 765 |   let tail = drop 1 v

 766 |     in Just ( headTree tree

 767 |             , tail

 768 |             )

 769 |   where

 770 |     headTree :  Tree a

 771 |              -> a

 772 |     headTree (Balanced (MkChildren {n = S k} children))            =

 773 |       assert_total (headTree (at children FZ))

 774 |     headTree (Unbalanced (MkRelaxedChildren {n = S k} children _)) =

 775 |       assert_total (headTree (at children FZ))

 776 |     headTree (Leaf (A Z _))                                        =

 777 |       assert_total (idris_crash "Data.RRBVector.viewl: empty leaf")

 778 |     headTree (Leaf (A (S k) elems))                                =

 779 |       at elems FZ

 784 | viewr :  RRBVector a

 785 |       -> Maybe (RRBVector a, a)

 786 | viewr Empty                =

 787 |   Nothing

 788 | viewr v@(Root size _ tree) =

 789 |   let init = take (minus size 1) v

 790 |     in Just ( init

 791 |             , lastTree tree

 792 |             )

 793 |   where

 794 |     lastTree :  Tree a

 795 |              -> a

 796 |     lastTree (Balanced (MkChildren {n = S k} children))            =

 797 |       assert_total (lastTree (at children lastFin))

 798 |     lastTree (Unbalanced (MkRelaxedChildren {n = S k} children _)) =

 799 |       assert_total (lastTree (at children lastFin))

 800 |     lastTree (Leaf (A Z _))                                        =

 801 |       assert_total (idris_crash "Data.RRBVector.viewr: empty leaf")

 802 |     lastTree (Leaf (A (S k) elems))                                =

 803 |       at elems lastFin

 812 | map :  (a -> b)

 813 |     -> RRBVector a

 814 |     -> RRBVector b

 815 | map _ Empty               =

 816 |   Empty

 817 | map f (Root size sh tree) =

 818 |   Root size sh (mapTree tree)

 819 |   where

 820 |     mapTree :  Tree a

 821 |             -> Tree b

 822 |     mapTree (Balanced (MkChildren {n} {nonEmpty} {withinBlock} children))                =

 823 |       assert_total (Balanced (MkChildren {n} {nonEmpty = nonEmpty} {withinBlock = withinBlock} (map mapTree children)))

 824 |     mapTree (Unbalanced (MkRelaxedChildren {n} {nonEmpty} {withinBlock} children sizes)) =

 825 |       assert_total (Unbalanced (MkRelaxedChildren {n} {nonEmpty = nonEmpty} {withinBlock = withinBlock} (map mapTree children) sizes))

 826 |     mapTree (Leaf arr)                                                                   =

 827 |       Leaf (map f arr)

 832 | reverse :  RRBVector a

 833 |         -> RRBVector a

 834 | reverse v =

 835 |   case compare (length v) 1 of

 836 |     LT =>

 837 |       v

 838 |     EQ =>

 839 |       v

 840 |     GT =>

 841 |       case fromList $ toList v of

 842 |         Nothing =>

 843 |           assert_total $ idris_crash "Data.RRBVector.reverse: can't convert to List1"

 844 |         Just v' =>

 845 |           fromList $ forget $ reverse v'

 851 | zip :  RRBVector a

 852 |     -> RRBVector b

 853 |     -> RRBVector (a, b)

 854 | zip v1 v2 =

 855 |   case fromList $ toList v1 of

 856 |     Nothing  =>

 857 |       assert_total $ idris_crash "Data.RRBVector.zip: can't convert to List1"

 858 |     Just v1' =>

 859 |       case fromList $ toList v2 of

 860 |         Nothing  =>

 861 |           assert_total $ idris_crash "Data.RRBVector.zip: can't convert to List1"

 862 |         Just v2' =>

 863 |           fromList $ forget $ zip v1' v2'

 872 | newBranch :  a

 873 |           -> Shift

 874 |           -> Tree a

 875 | newBranch x Z  =

 876 |   Leaf (singleton x)

 877 | newBranch x sh =

 878 |   assert_total (Balanced (MkChildren {n = 1} {nonEmpty = LTESucc LTEZero} {withinBlock = believe_me ()} (fill 1 (newBranch x (down sh)))))

 883 | (<|) :  a

 884 |      -> RRBVector a

 885 |      -> RRBVector a

 886 | x <| Empty             =

 887 |   singleton x

 888 | x <| Root size sh tree =

 889 |   case compare insertshift sh of

 890 |     LT =>

 891 |       Root (S size) sh (consTree sh tree)

 892 |     EQ =>

 893 |       Root (S size) sh (consTree sh tree)

 894 |     GT =>

 895 |       let children : IArray 2 (Tree a)

 896 |           children =

 897 |             array ( fromList

 898 |                       [ newBranch x sh

 899 |                       , tree

 900 |                       ]

 901 |                   )

 902 |           rootChildren : Children a

 903 |           rootChildren =

 904 |             MkChildren {n = 2} {nonEmpty = believe_me ()} {withinBlock = believe_me ()} children

 905 |         in Root (S size) insertshift (computeSizes insertshift rootChildren)

 906 |   where

 907 |     ||| Compute the shift at which the new branch must be inserted.

 909 |     computeShift :  Nat

 910 |                  -> Shift

 911 |                  -> Shift

 912 |                  -> Tree a

 913 |                  -> Shift

 914 |     computeShift sz sh min (Balanced _)                                             =

 915 |       let hishift  =

 916 |             let comp = mult (log2 (minus sz 1) `div` blockshift) blockshift

 917 |               in case compare comp 0 of

 918 |                    LT =>

 919 |                      0

 920 |                    EQ =>

 921 |                      0

 922 |                    GT =>

 923 |                      comp

 924 |           hi       = (natToInteger $ minus sz 1) `shiftR` hishift

 925 |           newshift = case compare hi (natToInteger blockmask) of

 926 |                        LT =>

 927 |                          hishift

 928 |                        EQ =>

 929 |                          plus hishift blockshift

 930 |                        GT =>

 931 |                          plus hishift blockshift

 932 |         in case compare newshift sh of

 933 |              LT =>

 934 |                newshift

 935 |              EQ =>

 936 |                newshift

 937 |              GT =>

 938 |                min

 939 |     computeShift _ sh min (Unbalanced (MkRelaxedChildren {n = S k} children sizes)) =

 940 |       let sz'     : Nat

 941 |           sz'     = at sizes FZ

 942 |           newtree : Tree a

 943 |           newtree = at children FZ

 944 |           newmin  : Shift

 945 |           newmin  = case compare (S k) blocksize of

 946 |                       LT =>

 947 |                         sh

 948 |                       EQ =>

 949 |                         min

 950 |                       GT =>

 951 |                         min

 952 |         in assert_total (computeShift sz' (down sh) newmin newtree)

 953 |     computeShift _ _ min (Leaf arr) =

 954 |       case compare arr.size blocksize of

 955 |         LT =>

 956 |           0

 957 |         EQ =>

 958 |           min

 959 |         GT =>

 960 |           min

 961 |     insertshift : Shift

 962 |     insertshift = computeShift size sh (up sh) tree

 963 |     consTree :  Shift

 964 |              -> Tree a

 965 |              -> Tree a

 966 |     consTree sh (Balanced (MkChildren {n = S k} {nonEmpty} {withinBlock} children))            =

 967 |       case compare sh insertshift of

 968 |         LT =>

 969 |           assert_total (computeSizes sh (MkChildren {n = S k} {nonEmpty = nonEmpty} {withinBlock = withinBlock} (updateAt FZ (consTree $ down sh) children)))

 970 |         EQ =>

 971 |           let children' = append (fill 1 (newBranch x $ down sh)) children

 972 |             in computeSizes sh (MkChildren {n = S (S k)} {nonEmpty = believe_me ()} {withinBlock = believe_me ()} children')

 973 |         GT =>

 974 |           assert_total (computeSizes sh (MkChildren {n = S k} {nonEmpty = nonEmpty} {withinBlock = withinBlock} (updateAt FZ (consTree $ down sh) children)))

 975 |     consTree sh (Unbalanced (MkRelaxedChildren {n = S k} {nonEmpty} {withinBlock} children _)) =

 976 |       case compare sh insertshift of

 977 |         LT =>

 978 |           assert_total (computeSizes sh (MkChildren {n = S k} {nonEmpty = nonEmpty} {withinBlock = withinBlock} (updateAt FZ (consTree $ down sh) children)))

 979 |         EQ =>

 980 |           let children' = append (fill 1 (newBranch x $ down sh)) children

 981 |             in computeSizes sh (MkChildren {n = S (S k)} {nonEmpty = believe_me ()} {withinBlock = believe_me ()} children')

 982 |         GT =>

 983 |           assert_total (computeSizes sh (MkChildren {n = S k} {nonEmpty = nonEmpty} {withinBlock = withinBlock} (updateAt FZ (consTree $ down sh) children)))

 984 |     consTree _ (Leaf arr)                                                                      =

 985 |       Leaf (A (S arr.size) (append (fill 1 x) arr.arr))

 990 | (|>) :  RRBVector a

 991 |      -> a

 992 |      -> RRBVector a

 993 | Empty |> x =

 994 |   singleton x

 995 | Root size sh tree |> x =

 996 |   case compare insertshift sh of

 997 |     LT =>

 998 |       Root (S size) sh (snocTree sh tree)

 999 |     EQ =>

1000 |       Root (S size) sh (snocTree sh tree)

1001 |     GT =>

1002 |       let children     : IArray 2 (Tree a)

1003 |           children     = array ( fromList

1004 |                                    [ tree

1005 |                                    , newBranch x sh

1006 |                                    ]

1007 |                                )

1008 |           rootChildren : Children a

1009 |           rootChildren = MkChildren {n = 2} {nonEmpty = believe_me ()} {withinBlock = believe_me ()} children

1010 |         in Root (S size) insertshift (computeSizes insertshift rootChildren)

1011 |   where

1012 |     ||| Compute the shift at which the new right-hand branch must be inserted.

1014 |     computeShift :  Nat

1015 |                  -> Shift

1016 |                  -> Shift

1017 |                  -> Tree a

1018 |                  -> Shift

1019 |     computeShift sz sh min (Balanced _)                                                  =

1020 |       let newshift = mult (countTrailingZeros sz `div` blockshift) blockshift

1021 |         in case compare newshift sh of

1022 |              LT =>

1023 |                newshift

1024 |              EQ =>

1025 |                newshift

1026 |              GT =>

1027 |                min

1028 |     computeShift _  sh min (Unbalanced (MkRelaxedChildren {n = 1} children sizes))       =

1029 |       let sz' : Nat

1030 |           sz' = lastAt sizes

1031 |           newtree : Tree a

1032 |           newtree = lastAt children

1033 |           newmin : Shift

1034 |           newmin = case compare 1 blocksize of

1035 |                      LT =>

1036 |                        sh

1037 |                      EQ =>

1038 |                        min

1039 |                      GT =>

1040 |                        min

1041 |         in assert_total (computeShift sz' (down sh) newmin newtree)

1042 |     computeShift _  sh min (Unbalanced (MkRelaxedChildren {n = S (S k)} children sizes)) =

1043 |       let totalsize   : Nat

1044 |           totalsize   = lastAt sizes

1045 |           previousidx : Fin (S (S k))

1046 |           previousidx = weaken (lastFin {n = k})

1047 |           previous    : Nat

1048 |           previous    = at sizes previousidx

1049 |           sz'         : Nat

1050 |           sz'         = minus totalsize previous

1051 |           newtree     : Tree a

1052 |           newtree     = lastAt children

1053 |           newmin      : Shift

1054 |           newmin      = case compare (S (S k)) blocksize of

1055 |                           LT =>

1056 |                             sh

1057 |                           EQ =>

1058 |                             min

1059 |                           GT =>

1060 |                             min

1061 |         in assert_total (computeShift sz' (down sh) newmin newtree)

1062 |     computeShift _  _  min (Leaf arr)                                                    =

1063 |       case compare arr.size blocksize of

1064 |         LT =>

1065 |           0

1066 |         EQ =>

1067 |           min

1068 |         GT =>

1069 |           min

1070 |     insertshift : Shift

1071 |     insertshift = computeShift size sh (up sh) tree

1072 |     snocTree :  Shift

1073 |              -> Tree a

1074 |              -> Tree a

1075 |     snocTree sh (Balanced (MkChildren {n = S k} {nonEmpty} {withinBlock} children))                =

1076 |       case compare sh insertshift of

1077 |         LT =>

1078 |           assert_total (Balanced (MkChildren {n = S k} {nonEmpty = nonEmpty} {withinBlock = withinBlock} (updateAt lastFin (snocTree $ down sh) children)))

1079 |         EQ =>

1080 |           let children' = append children (fill 1 (newBranch x (down sh)))

1081 |             in Balanced (MkChildren {n = plus (S k) 1} {nonEmpty = believe_me ()} {withinBlock = believe_me ()} children')

1082 |         GT =>

1083 |           assert_total (Balanced (MkChildren {n = S k} {nonEmpty = nonEmpty} {withinBlock = withinBlock} (updateAt lastFin (snocTree $ down sh) children)))

1084 |     snocTree sh (Unbalanced (MkRelaxedChildren {n = S k} {nonEmpty} {withinBlock} children sizes)) =

1085 |       case compare sh insertshift of

1086 |         LT =>

1087 |           let lastsize : Nat

1088 |               lastsize = plus (lastAt sizes) 1

1089 |             in assert_total (Unbalanced (MkRelaxedChildren {n = S k} {nonEmpty = nonEmpty} {withinBlock = withinBlock} (updateAt lastFin (snocTree $ down sh) children) (setAt lastFin lastsize sizes)))

1090 |         EQ =>

1091 |           let lastsize  : Nat

1092 |               lastsize  = plus (lastAt sizes) 1

1093 |               children' = append children (fill 1 (newBranch x (down sh)))

1094 |               sizes'    = append sizes (fill 1 lastsize)

1095 |             in Unbalanced (MkRelaxedChildren {n = plus (S k) 1} {nonEmpty = believe_me ()} {withinBlock = believe_me ()} children' sizes')

1096 |         GT =>

1097 |           let lastsize : Nat

1098 |               lastsize = plus (lastAt sizes) 1

1099 |             in assert_total (Unbalanced (MkRelaxedChildren {n = S k} {nonEmpty = nonEmpty} {withinBlock = withinBlock} (updateAt lastFin (snocTree $ down sh) children) (setAt lastFin lastsize sizes)))

1100 |     snocTree _  (Leaf arr)                                                                         =

1101 |       Leaf (A (plus arr.size 1) (append arr.arr (fill 1 x)))

1106 | (><) :  RRBVector a

1107 |      -> RRBVector a

1108 |      -> RRBVector a

1109 | Empty                >< v                    = v

1110 | v                    >< Empty                = v

1111 | Root size1 sh1 tree1 >< Root size2 sh2 tree2 =

1112 |   let upmaxshift   = case compare sh1 sh2 of

1113 |                        LT =>

1114 |                          up sh2

1115 |                        EQ =>

1116 |                          up sh1

1117 |                        GT =>

1118 |                          up sh1

1119 |       newarr       = mergeTrees tree1 sh1 tree2 sh2

1120 |       rootchildren : Children a

1121 |       rootchildren = childrenFromArray newarr

1122 |     in normalize (Root (plus size1 size2) upmaxshift (computeSizes upmaxshift rootchildren))

1123 |   where

1124 |     ||| Remove and return the first child of a nonempty tree array.

1129 |     viewlArr :  Array (Tree a)

1130 |              -> (Tree a, Array (Tree a))

1131 |     viewlArr (A Z _)       =

1132 |       assert_total (idris_crash "Data.RRBVector.(><).viewlArr: empty internal array")

1133 |     viewlArr (A (S n) arr) =

1134 |       let tail : IArray (minus n 0) (Tree a)

1135 |           tail = force (drop 1 arr)

1136 |         in ( at arr FZ

1137 |            , A (minus n 0) tail

1138 |            )

1139 |     ||| Remove and return the final child of a nonempty tree array.

1144 |     viewrArr :  Array (Tree b)

1145 |              -> (Array (Tree b), Tree b)

1146 |     viewrArr (A Z _)       =

1147 |       assert_total (idris_crash "Data.RRBVector.(><).viewrArr: empty internal array")

1148 |     viewrArr (A (S n) arr) =

1149 |       let 0 initLTE : LTE n (S n)

1150 |           initLTE   = believe_me ()

1151 |           init      : IArray n (Tree b)

1152 |           init      = force (take n arr @{initLTE})

1153 |         in ( A n init

1154 |            , at arr (lastFin {n})

1155 |            )

1156 |     mergeRebalance' :  Shift

1157 |                     -> Array (Tree a)

1158 |                     -> Array (Tree a)

1159 |                     -> Array (Tree a)

1160 |                     -> (Tree a -> Array (Tree a))

1161 |                     -> (Array (Tree a) -> Tree a)

1162 |                     -> Array (Tree a)

1163 |     mergeRebalance' sh left center right extract construct =

1164 |       run1 $ \t =>

1165 |         let nodecounter    # t := ref1 Z t

1166 |             subtreecounter # t := ref1 Z t

1167 |             newnode        # t := ref1 Lin t