
    0 | ||| Relaxed Radix Balanced Vectors (RRBVector)
    1 | module Data.RRBVector.Unsized
    2 | 
    3 | import public Data.RRBVector.Unsized.Internal
    4 | 
    5 | import Control.Monad.ST
    6 | import Data.Array
    7 | import Data.Array.Core
    8 | import Data.Array.Index
    9 | import Data.Array.Indexed
   10 | import Data.Bits
   11 | import Data.Maybe
   12 | import Data.List
   13 | import Data.List1
   14 | import Data.SnocList
   15 | import Data.Vect
   16 | import Data.Zippable
   17 | import Syntax.T1 as T1
   18 | 
   19 | %hide Prelude.null
   20 | %hide Prelude.Ops.infixr.(<|)
   21 | %hide Prelude.Ops.infixl.(|>)
   22 | 
   23 | %default total
   24 | 
   25 | --------------------------------------------------------------------------------
   26 | --          Fixity
   27 | --------------------------------------------------------------------------------
   28 | 
   29 | export
   30 | infixr 5 ><
   31 | 
   32 | export
   33 | infixr 5 <|
   34 | 
   35 | export
   36 | infixl 5 |>
   37 | 
   38 | --------------------------------------------------------------------------------
   39 | --          Creating RRB-Vectors
   40 | --------------------------------------------------------------------------------
   41 | 
   42 | ||| The empty vector. O(1)
   43 | export
   44 | empty : RRBVector a
   45 | empty = Empty
   46 | 
   47 | ||| A vector with a single element. O(1)
   48 | export
   49 | singleton :  a
   50 |           -> RRBVector a
   51 | singleton x = Root 1 0 (Leaf $ A 1 $ fill 1 x)
   52 | 
   53 | ||| Create a new vector from a list. O(n)
   54 | export
   55 | fromList :  List a
   56 |          -> RRBVector a
   57 | fromList []  = Empty
   58 | fromList [x] = singleton x
   59 | fromList xs  =
   60 |   case nodes Leaf xs of
   61 |     [tree] =>
   62 |       Root (treeSize 0 tree) 0 tree -- tree is a single leaf
   63 |     xs'    =>
   64 |       assert_smaller xs (iterateNodes blockshift xs')
   65 |   where
   66 |     nodes :  (Array a -> Tree a)
   67 |           -> List a
   68 |           -> List (Tree a)
   69 |     nodes f trees =
   70 |       let (trees', rest) = unsafeAlloc blocksize (go 0 blocksize f trees)
   71 |         in case rest of
   72 |              []    =>
   73 |                [trees']
   74 |              rest' =>
   75 |                (trees' :: nodes f (assert_smaller trees rest'))
   76 |       where
   77 |         go :  (cur,n : Nat)
   78 |            -> (Array a -> Tree a)
   79 |            -> List a
   80 |            -> WithMArray n a (Tree a,List a)
   81 |         go cur n f []        r = T1.do
   82 |           res <- unsafeFreeze r
   83 |           pure $ (f $ force $ take cur $ A n res,[])
   84 |         go cur n f (x :: xs) r =
   85 |           case cur == n of
   86 |             True  => T1.do
   87 |               res <- unsafeFreeze r
   88 |               pure $ (f $ A n res, x :: xs)
   89 |             False =>
   90 |               case tryNatToFin cur of
   91 |                 Nothing   =>
   92 |                   assert_total $ idris_crash "Data.RRBVector.Unsized.fromList.node: can't convert Nat to Fin"
   93 |                 Just cur' => T1.do
   94 |                   set r cur' x
   95 |                   go (S cur) n f xs r
   96 |     nodes' :  (Array (Tree a) -> Tree a)
   97 |            -> List (Tree a)
   98 |            -> List (Tree a)
   99 |     nodes' f trees =
  100 |       let (trees', rest) = unsafeAlloc blocksize (go 0 blocksize f trees)
  101 |         in case rest of
  102 |              []    =>
  103 |                [trees']
  104 |              rest' =>
  105 |                (trees' :: nodes' f (assert_smaller trees rest'))
  106 |       where
  107 |         go :  (cur,n : Nat)
  108 |            -> (Array (Tree a) -> Tree a)
  109 |            -> List (Tree a)
  110 |            -> WithMArray n (Tree a) (Tree a,List (Tree a))
  111 |         go cur n f []        r = T1.do
  112 |           res <- unsafeFreeze r
  113 |           pure $ (f $ force $ take cur $ A n res,[])
  114 |         go cur n f (x :: xs) r =
  115 |           case cur == n of
  116 |             True  => T1.do
  117 |               res <- unsafeFreeze r
  118 |               pure $ (f $ A n res, x :: xs)
  119 |             False =>
  120 |               case tryNatToFin cur of
  121 |                 Nothing   =>
  122 |                   assert_total $ idris_crash "Data.RRBVector.Unsized.fromList.node': can't convert Nat to Fin"
  123 |                 Just cur' => T1.do
  124 |                   set r cur' x
  125 |                   go (S cur) n f xs r
  126 |     iterateNodes :  Nat
  127 |                  -> List (Tree a)
  128 |                  -> RRBVector a
  129 |     iterateNodes sh trees =
  130 |       case nodes' Balanced trees of
  131 |         [tree] =>
  132 |           Root (treeSize sh tree) sh tree
  133 |         trees' =>
  134 |           iterateNodes (up sh) (assert_smaller trees trees')
  135 | 
  136 | ||| Creates a vector of length n with every element set to x. O(log n)
  137 | export
  138 | replicate :  Nat
  139 |           -> a
  140 |           -> RRBVector a
  141 | replicate n x =
  142 |   case compare n 0 of
  143 |     LT =>
  144 |       Empty
  145 |     EQ =>
  146 |       Empty
  147 |     GT =>
  148 |       case compare n blocksize of
  149 |         LT =>
  150 |           Root n 0 (Leaf $ A n $ fill n x)
  151 |         EQ =>
  152 |           Root n 0 (Leaf $ A n $ fill n x)
  153 |         GT =>
  154 |           let size' = integerToNat ((natToInteger $ minus n 1) .&. (natToInteger $ plus blockmask 1))
  155 |             in iterateNodes blockshift
  156 |                             (Leaf $ A blocksize $ fill blocksize x)
  157 |                             (Leaf $ A size' $ fill size' x)
  158 |   where
  159 |     iterateNodes :  Shift
  160 |                  -> Tree a
  161 |                  -> Tree a
  162 |                  -> RRBVector a
  163 |     iterateNodes sh full rest =
  164 |       let subtreesm1  = (natToInteger $ minus n 1) `shiftR` sh
  165 |           restsize    = integerToNat (subtreesm1 .&. (natToInteger blockmask))
  166 |           rest'       = Balanced $ A (plus restsize 1) $ append (fill restsize full) (fill 1 rest)
  167 |         in case compare subtreesm1 (natToInteger blocksize) of
  168 |              LT =>
  169 |                Root n sh rest'
  170 |              EQ =>
  171 |                let full' = Balanced (A blocksize $ fill blocksize full)
  172 |                  in iterateNodes (up sh) (assert_smaller full full') (assert_smaller rest rest')
  173 |              GT =>
  174 |                let full' = Balanced (A blocksize $ fill blocksize full)
  175 |                  in iterateNodes (up sh) (assert_smaller full full') (assert_smaller rest rest')
  176 | 
  177 | --------------------------------------------------------------------------------
  178 | --          Creating Lists from RRB-Vectors
  179 | --------------------------------------------------------------------------------
  180 | 
  181 | ||| Convert a vector to a list. O(n)
  182 | export
  183 | toList :  RRBVector a
  184 |        -> List a
  185 | toList Empty           = []
  186 | toList (Root _ _ tree) = treeToList tree
  187 |   where
  188 |     treeToList :  Tree a
  189 |                -> List a
  190 |     treeToList (Balanced trees)     = assert_total $ concat (map treeToList (toList trees))
  191 |     treeToList (Unbalanced trees _) = assert_total $ concat (map treeToList (toList trees))
  192 |     treeToList (Leaf arr)           = toList arr
  193 | 
  194 | --------------------------------------------------------------------------------
  195 | --          Folds
  196 | --------------------------------------------------------------------------------
  197 | 
  198 | export
  199 | foldl :  (b -> a -> b)
  200 |       -> b
  201 |       -> RRBVector a
  202 |       -> b
  203 | foldl f acc = go
  204 |   where
  205 |     foldlTree :  b
  206 |               -> Tree a
  207 |               -> b
  208 |     foldlTree acc' (Balanced arr)     = assert_total $ foldl foldlTree acc' arr
  209 |     foldlTree acc' (Unbalanced arr _) = assert_total $ foldl foldlTree acc' arr
  210 |     foldlTree acc' (Leaf arr)         = assert_total $ foldl f acc' arr
  211 |     go :  RRBVector a
  212 |        -> b
  213 |     go Empty           = acc
  214 |     go (Root _ _ tree) = assert_total $ foldlTree acc tree
  215 | 
  216 | export
  217 | foldr :  (a -> b -> b)
  218 |       -> b
  219 |       -> RRBVector a
  220 |       -> b
  221 | foldr f acc = go
  222 |   where
  223 |     foldrTree :  Tree a
  224 |               -> b
  225 |               -> b
  226 |     foldrTree (Balanced arr) acc'     = assert_total $ foldr foldrTree acc' arr
  227 |     foldrTree (Unbalanced arr _) acc' = assert_total $ foldr foldrTree acc' arr
  228 |     foldrTree (Leaf arr) acc'         = assert_total $ foldr f acc' arr
  229 |     go :  RRBVector a
  230 |        -> b
  231 |     go Empty           = acc
  232 |     go (Root _ _ tree) = assert_total $ foldrTree tree acc
  233 | 
  234 | --------------------------------------------------------------------------------
  235 | --          Query
  236 | --------------------------------------------------------------------------------
  237 | 
  238 | ||| Is the vector empty? O(1)
  239 | export
  240 | null :  RRBVector a
  241 |      -> Bool
  242 | null Empty = True
  243 | null _     = False
  244 | 
  245 | ||| Return the size of a vector. O(1)
  246 | export
  247 | length :  RRBVector a
  248 |        -> Nat
  249 | length Empty        = 0
  250 | length (Root s _ _) = s
  251 | 
  252 | --------------------------------------------------------------------------------
  253 | --          Indexing
  254 | --------------------------------------------------------------------------------
  255 | 
  256 | ||| The element at the index or Nothing if the index is out of range. O(log n)
  257 | export
  258 | lookup :  Nat
  259 |        -> RRBVector a
  260 |        -> Maybe a
  261 | lookup _ Empty               = Nothing
  262 | lookup i (Root size sh tree) =
  263 |   case compare i 0 of
  264 |     LT =>
  265 |       Nothing -- index out of range
  266 |     GT =>
  267 |       case compare i size of
  268 |         EQ =>
  269 |           Nothing -- index out of range
  270 |         GT =>
  271 |           Nothing -- index out of range
  272 |         LT =>
  273 |           Just $ lookupTree i sh tree
  274 |     EQ =>
  275 |       case compare i size of
  276 |         EQ =>
  277 |           Nothing -- index out of range
  278 |         GT =>
  279 |           Nothing -- index out of range
  280 |         LT =>
  281 |           Just $ lookupTree i sh tree
  282 |   where
  283 |     lookupTree :  Nat
  284 |                -> Nat
  285 |                -> Tree a
  286 |                -> a
  287 |     lookupTree i sh (Balanced arr)         =
  288 |       case tryNatToFin (radixIndex i sh) of
  289 |         Nothing =>
  290 |           assert_total $ idris_crash "Data.RRBVector.Unsized.lookup: can't convert Nat to Fin"
  291 |         Just i' =>
  292 |           assert_total $ lookupTree i (down sh) (at arr.arr i')
  293 |     lookupTree i sh (Unbalanced arr sizes) =
  294 |       let (idx, subidx) = relaxedRadixIndex sizes i sh
  295 |         in case tryNatToFin idx of
  296 |              Nothing   =>
  297 |                assert_total $ idris_crash "Data.RRBVector.Unsized.lookup: can't convert Nat to Fin"
  298 |              Just idx' =>
  299 |                assert_total $ lookupTree subidx (down sh) (at arr.arr idx')
  300 |     lookupTree i _ (Leaf arr)              =
  301 |       let i' = integerToNat ((natToInteger i) .&. (natToInteger blockmask))
  302 |         in case tryNatToFin i' of
  303 |              Nothing =>
  304 |                assert_total $ idris_crash "Data.RRBVector.Unsized.lookup: can't convert Nat to Fin"
  305 |              Just i'' =>
  306 |                at arr.arr i''
  307 | 
  308 | ||| The element at the index.
  309 | ||| Calls 'idris_crash' if the index is out of range. O(log n)
  310 | export
  311 | index :  Nat
  312 |       -> RRBVector a
  313 |       -> a
  314 | index i = fromMaybe (assert_total $ idris_crash "Data.RRBVector.Unsized.index: index out of range") . lookup i
  315 | 
  316 | ||| A flipped version of lookup. O(log n)
  317 | export
  318 | (!?) :  RRBVector a
  319 |      -> Nat
  320 |      -> Maybe a
  321 | (!?) = flip lookup
  322 | 
  323 | ||| A flipped version of index. O(log n)
  324 | export
  325 | (!!) :  RRBVector a
  326 |      -> Nat
  327 |      -> a
  328 | (!!) = flip index
  329 | 
  330 | ||| Update the element at the index with a new element.
  331 | ||| If the index is out of range, the original vector is returned. O (log n)
  332 | export
  333 | update :  Nat
  334 |        -> a
  335 |        -> RRBVector a
  336 |        -> RRBVector a
  337 | update _ _ Empty                 = Empty
  338 | update i x v@(Root size sh tree) =
  339 |   case compare i 0 of
  340 |     LT =>
  341 |       v -- index out of range
  342 |     GT =>
  343 |       case compare i size of
  344 |         EQ =>
  345 |           v -- index out of range
  346 |         GT =>
  347 |           v -- index out of range
  348 |         LT =>
  349 |           Root size sh (updateTree i sh tree)
  350 |     EQ =>
  351 |       case compare i size of
  352 |         EQ =>
  353 |           v -- index out of range
  354 |         GT =>
  355 |           v -- index out of range
  356 |         LT =>
  357 |           Root size sh (updateTree i sh tree)
  358 |   where
  359 |     updateTree :  Nat
  360 |                -> Nat
  361 |                -> Tree a
  362 |                -> Tree a
  363 |     updateTree i sh (Balanced arr)         =
  364 |       case tryNatToFin (radixIndex i sh) of
  365 |         Nothing =>
  366 |           assert_total $ idris_crash "Data.RRBVector.Unsized.update: can't convert Nat to Fin"
  367 |         Just i' =>
  368 |           assert_total $ Balanced (A arr.size (updateAt i' (updateTree i (down sh)) arr.arr))
  369 |     updateTree i sh (Unbalanced arr sizes) =
  370 |       let (idx, subidx) = relaxedRadixIndex sizes i sh
  371 |         in case tryNatToFin idx of
  372 |              Nothing   =>
  373 |                assert_total $ idris_crash "Data.RRBVector.Unsized.update: can't convert Nat to Fin"
  374 |              Just idx' =>
  375 |                assert_total $ Unbalanced (A arr.size (updateAt idx' (updateTree subidx (down sh)) arr.arr)) sizes
  376 |     updateTree i _ (Leaf arr)              =
  377 |       let i' = integerToNat ((natToInteger i) .&. (natToInteger blockmask))
  378 |         in case tryNatToFin i' of
  379 |              Nothing =>
  380 |                assert_total $ idris_crash "Data.RRBVector.Unsized.update: can't convert Nat to Fin"
  381 |              Just i'' =>
  382 |                Leaf (A arr.size (setAt i'' x arr.arr))
  383 | 
  384 | ||| Adjust the element at the index by applying the function to it.
  385 | ||| If the index is out of range, the original vector is returned. O(log n)
  386 | export
  387 | adjust :  Nat
  388 |        -> (a -> a)
  389 |        -> RRBVector a
  390 |        -> RRBVector a
  391 | adjust _ _ Empty                 = Empty
  392 | adjust i f v@(Root size sh tree) =
  393 |   case compare i 0 of
  394 |     LT =>
  395 |       v -- index out of range
  396 |     GT =>
  397 |       case compare i size of
  398 |         EQ =>
  399 |           v -- index out of range
  400 |         GT =>
  401 |           v -- index out of range
  402 |         LT =>
  403 |           Root size sh (adjustTree i sh tree)
  404 |     EQ =>
  405 |       case compare i size of
  406 |         EQ =>
  407 |           v -- index out of range
  408 |         GT =>
  409 |           v -- index out of range
  410 |         LT =>
  411 |           Root size sh (adjustTree i sh tree)
  412 |   where
  413 |     adjustTree :  Nat
  414 |                -> Nat
  415 |                -> Tree a
  416 |                -> Tree a
  417 |     adjustTree i sh (Balanced arr)         =
  418 |       case tryNatToFin (radixIndex i sh) of
  419 |         Nothing =>
  420 |           assert_total $ idris_crash "Data.RRBVector.Unsized.adjust: can't convert Nat to Fin"
  421 |         Just i' =>
  422 |           assert_total $ Balanced (A arr.size (updateAt i' (adjustTree i (down sh)) arr.arr))
  423 |     adjustTree i sh (Unbalanced arr sizes) =
  424 |       let (idx, subidx) = relaxedRadixIndex sizes i sh
  425 |         in case tryNatToFin idx of
  426 |              Nothing   =>
  427 |                assert_total $ idris_crash "Data.RRBVector.Unsized.adjust: can't convert Nat to Fin"
  428 |              Just idx' =>
  429 |                assert_total $ Unbalanced (A arr.size (updateAt idx' (adjustTree subidx (down sh)) arr.arr)) sizes
  430 |     adjustTree i _ (Leaf arr)              =
  431 |       let i' = integerToNat ((natToInteger i) .&. (natToInteger blockmask))
  432 |         in case tryNatToFin i' of
  433 |              Nothing =>
  434 |                assert_total $ idris_crash "Data.RRBVector.Unsized.adjust: can't convert Nat to Fin"
  435 |              Just i'' =>
  436 |                Leaf (A arr.size (updateAt i'' f arr.arr))
  437 | 
  438 | private
  439 | normalize :  RRBVector a
  440 |           -> RRBVector a
  441 | normalize v@(Root size sh (Balanced arr))     =
  442 |   case compare arr.size 1 of
  443 |     LT =>
  444 |       v
  445 |     EQ =>
  446 |       case tryNatToFin 0 of
  447 |         Nothing =>
  448 |           assert_total $ idris_crash "Data.RRBVector.Unsized.normalize: can't convert Nat to Fin"
  449 |         Just i  =>
  450 |           assert_total $ normalize $ Root size (down sh) (at arr.arr i)
  451 |     GT =>
  452 |       v
  453 | normalize v@(Root size sh (Unbalanced arr _)) =
  454 |   case compare arr.size 1 of
  455 |     LT =>
  456 |       v
  457 |     EQ =>
  458 |       case tryNatToFin 0 of
  459 |         Nothing =>
  460 |           assert_total $ idris_crash "Data.RRBVector.Unsized.normalize: can't convert Nat to Fin"
  461 |         Just i  =>
  462 |           assert_total $ normalize $ Root size (down sh) (at arr.arr i)
  463 |     GT =>
  464 |       v
  465 | normalize v                                   =
  466 |   v
  467 | 
  468 | ||| The initial i is n - 1 (the index of the last element in the new tree).
  469 | private
  470 | takeTree :  Nat
  471 |          -> Shift
  472 |          -> Tree a
  473 |          -> Tree a
  474 | takeTree i sh (Balanced arr) with (radixIndex i sh) | ((plus (radixIndex i sh) 1) <= arr.size) proof eq
  475 |   _ | i' | True  =
  476 |     case tryNatToFin i' of
  477 |       Nothing =>
  478 |         assert_total $ idris_crash "Data.RRBVector.Unsized.takeTree: can't convert Nat to Fin"
  479 |       Just i'' =>
  480 |         let newarr = force $ take (plus (radixIndex i sh) 1) arr.arr @{lteOpReflectsLTE _ _ eq}
  481 |           in assert_total $ Balanced (A (plus (radixIndex i sh) 1) (updateAt i'' (takeTree i (down sh)) newarr))
  482 |   _ | _  | False =
  483 |     assert_total $ idris_crash "Data.RRBVector.Unsized.takeTree: index out of bounds"
  484 | takeTree i sh (Unbalanced arr sizes) with (relaxedRadixIndex sizes i sh) | ((plus (fst (relaxedRadixIndex sizes i sh)) 1) <= arr.size) proof eq
  485 |   _ | (idx, subidx) | True  =
  486 |     case tryNatToFin idx of
  487 |       Nothing   =>
  488 |         assert_total $ idris_crash "Data.RRBVector.Unsized.takeTree: can't convert Nat to Fin"
  489 |       Just idx' =>
  490 |         let newarr = force $ take (plus (fst (relaxedRadixIndex sizes i sh)) 1) arr.arr @{lteOpReflectsLTE _ _ eq}
  491 |           in assert_total $ computeSizes sh (A (plus (fst (relaxedRadixIndex sizes i sh)) 1) (updateAt idx' (takeTree subidx (down sh)) newarr))
  492 |   _ | _             | False =
  493 |     assert_total $ idris_crash "Data.RRBVector.Unsized.takeTree: index out of bounds"
  494 | takeTree i _ (Leaf arr) with (integerToNat (((natToInteger i) .&. (natToInteger blockmask)) + 1) <= arr.size) proof eq
  495 |   _ | True  =
  496 |     let newarr = force $ take (integerToNat (((natToInteger i) .&. (natToInteger blockmask)) + 1)) arr.arr @{lteOpReflectsLTE _ _ eq}
  497 |       in Leaf (A (integerToNat (((natToInteger i) .&. (natToInteger blockmask)) + 1)) newarr)
  498 |   _ | False =
  499 |     assert_total $ idris_crash "Data.RRBVector.Unsized.takeTree: index out of bounds"
  500 | 
  501 | private
  502 | dropTree :  Nat
  503 |          -> Shift
  504 |          -> Tree a
  505 |          -> Tree a
  506 | dropTree n sh (Balanced arr) =
  507 |   case tryNatToFin 0 of
  508 |     Nothing   =>
  509 |       assert_total $ idris_crash "Data.RRBVector.Unsized.dropTree: can't convert Nat to Fin"
  510 |     Just zero =>
  511 |       let newarr = force $ drop (radixIndex n sh) arr.arr
  512 |         in assert_total $ computeSizes sh (A (minus arr.size (radixIndex n sh)) (updateAt zero (dropTree n (down sh)) newarr))
  513 | dropTree n sh (Unbalanced arr sizes) =
  514 |   case tryNatToFin 0 of
  515 |     Nothing   =>
  516 |       assert_total $ idris_crash "Data.RRBVector.Unsized.dropTree: can't convert Nat to Fin"
  517 |     Just zero =>
  518 |       let newarr = force $ drop (fst $ relaxedRadixIndex sizes n sh) arr.arr
  519 |         in assert_total $ computeSizes sh (A (minus arr.size (fst $ relaxedRadixIndex sizes n sh)) (updateAt zero (dropTree (snd $ relaxedRadixIndex sizes n sh) (down sh)) newarr))
  520 | dropTree n _  (Leaf arr) =
  521 |   let n      = integerToNat ((natToInteger n) .&. (natToInteger blockmask))
  522 |       newarr = force $ drop n arr.arr
  523 |     in Leaf (A (minus arr.size n) newarr)
  524 | 
  525 | ||| The first i elements of the vector.
  526 | ||| If the vector contains less than or equal to i elements, the whole vector is returned. O(log n)
  527 | export
  528 | take :  Nat
  529 |      -> RRBVector a
  530 |      -> RRBVector a
  531 | take _ Empty                 = Empty
  532 | take n v@(Root size sh tree) =
  533 |   case compare n 0 of
  534 |     LT =>
  535 |       empty
  536 |     EQ =>
  537 |       empty
  538 |     GT =>
  539 |       case compare n size of
  540 |         LT =>
  541 |           normalize $ Root n sh (takeTree (minus n 1) sh tree)
  542 |         EQ =>
  543 |           v
  544 |         GT =>
  545 |           v
  546 | 
  547 | ||| The vector without the first i elements.
  548 | ||| If the vector contains less than or equal to i elements, the empty vector is returned. O(log n)
  549 | export
  550 | drop :  Nat
  551 |      -> RRBVector a
  552 |      -> RRBVector a
  553 | drop _ Empty                 = Empty
  554 | drop n v@(Root size sh tree) =
  555 |   case compare n 0 of
  556 |     LT =>
  557 |       v
  558 |     EQ =>
  559 |       v
  560 |     GT =>
  561 |       case compare n size of
  562 |         LT =>
  563 |           normalize $ Root (minus size n) sh (dropTree n sh tree)
  564 |         EQ =>
  565 |           empty
  566 |         GT =>
  567 |           empty
  568 | 
  569 | ||| Split the vector at the given index. O(log n)
  570 | export
  571 | splitAt :  Nat
  572 |         -> RRBVector a
  573 |         -> (RRBVector a, RRBVector a)
  574 | splitAt _ Empty                 = (Empty, Empty)
  575 | splitAt n v@(Root size sh tree) =
  576 |   case compare n 0 of
  577 |     LT =>
  578 |       (empty, v)
  579 |     EQ =>
  580 |       (empty, v)
  581 |     GT =>
  582 |       case compare n size of
  583 |         LT =>
  584 |           let left  = normalize $ Root n sh (takeTree (minus n 1) sh tree)
  585 |               right = normalize $ Root (minus size n) sh (dropTree n sh tree)
  586 |             in (left, right)
  587 |         EQ =>
  588 |           (v, empty)
  589 |         GT =>
  590 |           (v, empty)
  591 | 
  592 | --------------------------------------------------------------------------------
  593 | --          Deconstruction
  594 | --------------------------------------------------------------------------------
  595 | 
  596 | ||| The first element and the vector without the first element, or 'Nothing' if the vector is empty. O(log n)
  597 | export
  598 | viewl :  RRBVector a
  599 |       -> Maybe (a, RRBVector a)
  600 | viewl Empty             = Nothing
  601 | viewl v@(Root _ _ tree) =
  602 |   let tail = drop 1 v
  603 |     in Just (headTree tree, tail)
  604 |   where
  605 |     headTree : Tree a -> a
  606 |     headTree (Balanced arr)     =
  607 |       case tryNatToFin 0 of
  608 |         Nothing   =>
  609 |           assert_total $ idris_crash "Data.RRBVector.Unsized.viewl: can't convert Nat to Fin"
  610 |         Just zero =>
  611 |           assert_total $ headTree (at arr.arr zero)
  612 |     headTree (Unbalanced arr _) =
  613 |       case tryNatToFin 0 of
  614 |         Nothing   =>
  615 |           assert_total $ idris_crash "Data.RRBVector.Unsized.viewl: can't convert Nat to Fin"
  616 |         Just zero =>
  617 |           assert_total $ headTree (at arr.arr zero)
  618 |     headTree (Leaf arr)         =
  619 |       case tryNatToFin 0 of
  620 |         Nothing   =>
  621 |           assert_total $ idris_crash "Data.RRBVector.Unsized.viewl: can't convert Nat to Fin"
  622 |         Just zero =>
  623 |           at arr.arr zero
  624 | 
  625 | ||| The vector without the last element and the last element, or 'Nothing' if the vector is empty. O(log n)
  626 | export
  627 | viewr :  RRBVector a
  628 |       -> Maybe (RRBVector a, a)
  629 | viewr Empty                = Nothing
  630 | viewr v@(Root size _ tree) =
  631 |   let init = take (minus size 1) v
  632 |     in Just (init, lastTree tree)
  633 |   where
  634 |     lastTree : Tree a -> a
  635 |     lastTree (Balanced arr)     =
  636 |       case tryNatToFin (minus size 1) of
  637 |         Nothing   =>
  638 |           assert_total $ idris_crash "Data.RRBVector.Unsized.viewr: can't convert Nat to Fin"
  639 |         Just last =>
  640 |           assert_total $ lastTree (at arr.arr last)
  641 |     lastTree (Unbalanced arr _) =
  642 |       case tryNatToFin (minus size 1) of
  643 |         Nothing   =>
  644 |           assert_total $ idris_crash "Data.RRBVector.Unsized.viewr: can't convert Nat to Fin"
  645 |         Just last =>
  646 |           assert_total $ lastTree (at arr.arr last)
  647 |     lastTree (Leaf arr)         =
  648 |       case tryNatToFin (minus size 1) of
  649 |         Nothing   =>
  650 |           assert_total $ idris_crash "Data.RRBVector.Unsized.viewr: can't convert Nat to Fin"
  651 |         Just last =>
  652 |           at arr.arr last
  653 | 
  654 | --------------------------------------------------------------------------------
  655 | --          Transformation
  656 | --------------------------------------------------------------------------------
  657 | 
  658 | ||| Apply the function to every element. O(n)
  659 | export
  660 | map :  (a -> b)
  661 |     -> RRBVector a
  662 |     -> RRBVector b
  663 | map _ Empty               = Empty
  664 | map f (Root size sh tree) = Root size sh (mapTree tree)
  665 |   where
  666 |     mapTree : Tree a -> Tree b
  667 |     mapTree (Balanced arr)         =
  668 |       assert_total $ Balanced (map mapTree arr)
  669 |     mapTree (Unbalanced arr sizes) =
  670 |       assert_total $ Unbalanced (map mapTree arr) sizes
  671 |     mapTree (Leaf arr)             =
  672 |       Leaf (map f arr)
  673 | 
  674 | ||| Reverse the vector. O(n)
  675 | export
  676 | reverse :  RRBVector a
  677 |         -> RRBVector a
  678 | reverse v =
  679 |   case compare (length v) 1 of
  680 |     LT =>
  681 |       v
  682 |     EQ =>
  683 |       v
  684 |     GT =>
  685 |       case fromList $ toList v of
  686 |         Nothing =>
  687 |           assert_total $ idris_crash "Data.RRBVector.Unsized.reverse: can't convert to List1"
  688 |         Just v' =>
  689 |           fromList $ forget $ reverse v'
  690 | 
  691 | ||| Take two vectors and return a vector of corresponding pairs.
  692 | ||| If one input is longer, excess elements are discarded from the right end. O(min(n1,n2))
  693 | export
  694 | zip :  RRBVector a
  695 |     -> RRBVector b
  696 |     -> RRBVector (a, b)
  697 | zip v1 v2 =
  698 |   case fromList $ toList v1 of
  699 |     Nothing  =>
  700 |       assert_total $ idris_crash "Data.RRBVector.Unsized.zip: can't convert to List1"
  701 |     Just v1' =>
  702 |       case fromList $ toList v2 of
  703 |         Nothing  =>
  704 |           assert_total $ idris_crash "Data.RRBVector.Unsized.zip: can't convert to List1"
  705 |         Just v2' =>
  706 |           fromList $ forget $ zip v1' v2'
  707 | 
  708 | --------------------------------------------------------------------------------
  709 | --          Concatenation
  710 | --------------------------------------------------------------------------------
  711 | 
  712 | ||| Create a new tree with shift sh.
  713 | private
  714 | newBranch :  a
  715 |           -> Shift
  716 |           -> Tree a
  717 | newBranch x 0  = Leaf (singleton x)
  718 | newBranch x sh = assert_total $ Balanced (singleton $ newBranch x (down sh))
  719 | 
  720 | ||| Add an element to the left end of the vector. O(log n)
  721 | export
  722 | (<|) :  a
  723 |      -> RRBVector a
  724 |      -> RRBVector a
  725 | x <| Empty             = singleton x
  726 | x <| Root size sh tree =
  727 |   case compare insertshift sh of
  728 |     LT =>
  729 |       Root (plus size 1) sh (consTree sh tree)
  730 |     EQ =>
  731 |       Root (plus size 1) sh (consTree sh tree)
  732 |     GT =>
  733 |       let new = A 2 $ array $ fromList [(newBranch x sh), tree]
  734 |         in Root (plus size 1) insertshift (computeSizes insertshift new)
  735 |   where
  736 |     -- compute the shift at which the new branch needs to be inserted (0 means there is space in the leaf)
  737 |     -- the size is computed for efficient calculation of the shift in a balanced subtree
  738 |     computeShift :  Nat
  739 |                  -> Nat
  740 |                  -> Nat
  741 |                  -> Tree a
  742 |                  -> Nat
  743 |     computeShift sz sh min (Balanced _)          =
  744 |       -- @sz - 1@ is the index of the last element
  745 |       let hishift  = let comp = mult (log2 (minus sz 1) `div` blockshift) blockshift  -- the shift of the root when normalizing
  746 |                        in case compare comp 0 of
  747 |                             LT =>
  748 |                               0
  749 |                             EQ =>
  750 |                               0
  751 |                             GT =>
  752 |                               comp
  753 |           hi       = (natToInteger $ minus sz 1) `shiftR` hishift -- the length of the root node when normalizing minus 1
  754 |           newshift = case compare hi (natToInteger blockmask) of
  755 |                        LT =>
  756 |                          hishift
  757 |                        EQ =>
  758 |                          plus hishift blockshift
  759 |                        GT =>
  760 |                          plus hishift blockshift
  761 |         in case compare newshift sh of
  762 |              LT =>
  763 |                newshift
  764 |              EQ =>
  765 |                newshift
  766 |              GT =>
  767 |                min
  768 |     computeShift _ sh min (Unbalanced arr sizes) =
  769 |       let sz'     = case tryNatToFin 0 of
  770 |                       Nothing   =>
  771 |                         assert_total $ idris_crash "Data.RRBVector.Unsized.(<|).computeShift.Unbalanced: can't convert Nat to Fin"
  772 |                       Just zero =>
  773 |                         at sizes.arr zero -- the size of the first subtree
  774 |           newtree = case tryNatToFin 0 of
  775 |                       Nothing   =>
  776 |                         assert_total $ idris_crash "Data.RRBVector.Unsized.(<|).computeShift.Unbalanced: can't convert Nat to Fin"
  777 |                       Just zero =>
  778 |                         at arr.arr zero
  779 |           newmin  = case compare arr.size blocksize of
  780 |                       LT =>
  781 |                         sh
  782 |                       EQ =>
  783 |                         min
  784 |                       GT =>
  785 |                         min
  786 |         in assert_total $ computeShift sz' (down sh) newmin newtree
  787 |     computeShift _ _ min (Leaf arr)              =
  788 |       case compare arr.size blocksize of
  789 |         LT =>
  790 |           0
  791 |         EQ =>
  792 |           min
  793 |         GT =>
  794 |           min
  795 |     insertshift : Nat
  796 |     insertshift = computeShift size sh (up sh) tree
  797 |     consTree :  Nat
  798 |              -> Tree a
  799 |              -> Tree a
  800 |     consTree sh (Balanced arr)     =
  801 |       case compare sh insertshift of
  802 |         LT =>
  803 |           case tryNatToFin 0 of
  804 |             Nothing   =>
  805 |               assert_total $ idris_crash "Data.RRBVector.Unsized.(<|).consTree.Balanced: can't convert Nat to Fin"
  806 |             Just zero =>
  807 |               assert_total $ computeSizes sh (A arr.size $ updateAt zero (consTree (down sh)) arr.arr)
  808 |         EQ =>
  809 |           computeSizes sh (A (S arr.size) (append (fill 1 (newBranch x (down sh))) arr.arr))
  810 |         GT =>
  811 |           case tryNatToFin 0 of
  812 |             Nothing   =>
  813 |               assert_total $ idris_crash "Data.RRBVector.Unsized.(<|).consTree.Balanced: can't convert Nat to Fin"
  814 |             Just zero =>
  815 |               assert_total $ computeSizes sh (A arr.size $ updateAt zero (consTree (down sh)) arr.arr)
  816 |     consTree sh (Unbalanced arr _) =
  817 |       case compare sh insertshift of
  818 |         LT =>
  819 |           case tryNatToFin 0 of
  820 |             Nothing   =>
  821 |               assert_total $ idris_crash "Data.RRBVector.Unsized.(<|).consTree.Unbalanced: can't convert Nat to Fin"
  822 |             Just zero =>
  823 |               assert_total $ computeSizes sh (A arr.size $ updateAt zero (consTree (down sh)) arr.arr)
  824 |         EQ =>
  825 |           computeSizes sh (A (S arr.size) (append (fill 1 (newBranch x (down sh))) arr.arr))
  826 |         GT =>
  827 |           case tryNatToFin 0 of
  828 |             Nothing   =>
  829 |               assert_total $ idris_crash "Data.RRBVector.Unsized.(<|).consTree.Unbalanced: can't convert Nat to Fin"
  830 |             Just zero =>
  831 |               assert_total $ computeSizes sh (A arr.size $ updateAt zero (consTree (down sh)) arr.arr)
  832 |     consTree _ (Leaf arr)          =
  833 |       Leaf (A (S arr.size) (append (fill 1 x) arr.arr))
  834 | 
  835 | ||| Add an element to the right end of the vector. O(log n)
  836 | export
  837 | (|>) :  RRBVector a
  838 |      -> a
  839 |      -> RRBVector a
  840 | Empty             |> x = singleton x
  841 | Root size sh tree |> x =
  842 |   case compare insertshift sh of
  843 |     LT =>
  844 |       Root (plus size 1) sh (snocTree sh tree)
  845 |     EQ =>
  846 |       Root (plus size 1) sh (snocTree sh tree)
  847 |     GT =>
  848 |       let new = A 2 $ array $ fromList [tree,(newBranch x sh)]
  849 |         in Root (plus size 1) insertshift (computeSizes insertshift new)
  850 |   where
  851 |     -- compute the shift at which the new branch needs to be inserted (0 means there is space in the leaf)
  852 |     -- the size is computed for efficient calculation of the shift in a balanced subtree
  853 |     computeShift :  Nat
  854 |                  -> Nat
  855 |                  -> Nat
  856 |                  -> Tree a
  857 |                  -> Nat
  858 |     computeShift sz sh min (Balanced _)          =
  859 |       -- @sz - 1@ is the index of the last element
  860 |       let newshift = mult (countTrailingZeros sz `div` blockshift) blockshift
  861 |         in case compare newshift sh of
  862 |              LT =>
  863 |                newshift
  864 |              EQ =>
  865 |                newshift
  866 |              GT =>
  867 |                min
  868 |     computeShift _ sh min (Unbalanced arr sizes) =
  869 |       let lastidx = minus arr.size 1
  870 |           sz'     = case tryNatToFin lastidx of
  871 |                       Nothing       =>
  872 |                         assert_total $ idris_crash "Data.RRBVector.Unsized.(|>).computeShift.Unbalanced: can't convert Nat to Fin"
  873 |                       Just lastidx' =>
  874 |                         case tryNatToFin $ minus lastidx 1 of
  875 |                           Nothing        =>
  876 |                             assert_total $ idris_crash "Data.RRBVector.Unsized.(|>).computeShift.Unbalanced: can't convert Nat to Fin"
  877 |                           Just lastidx'' =>
  878 |                             minus (at sizes.arr lastidx') (at sizes.arr lastidx'')
  879 |           newtree = case tryNatToFin lastidx of
  880 |                       Nothing       =>
  881 |                         assert_total $ idris_crash "Data.RRBVector.Unsized.(|>).computeShift.Unbalanced: can't convert Nat to Fin"
  882 |                       Just lastidx' =>
  883 |                         at arr.arr lastidx'
  884 |           newmin  = case compare arr.size blocksize of
  885 |                       LT =>
  886 |                         sh
  887 |                       EQ =>
  888 |                         min
  889 |                       GT =>
  890 |                         min
  891 |         in assert_total $ computeShift sz' (down sh) newmin newtree
  892 |     computeShift _ _ min (Leaf arr)              =
  893 |       case compare arr.size blocksize of
  894 |         LT =>
  895 |           0
  896 |         EQ =>
  897 |           min
  898 |         GT =>
  899 |           min
  900 |     insertshift : Nat
  901 |     insertshift = computeShift size sh (up sh) tree
  902 |     snocTree :  Nat
  903 |              -> Tree a
  904 |              -> Tree a
  905 |     snocTree sh (Balanced arr) =
  906 |       case compare sh insertshift of
  907 |         LT =>
  908 |           case tryNatToFin $ minus arr.size 1 of
  909 |             Nothing   =>
  910 |               assert_total $ idris_crash "Data.RRBVector.Unsized.(|>).snocTree.Balanced: can't convert Nat to Fin"
  911 |             Just lastidx =>
  912 |               assert_total $ Balanced (A arr.size $ updateAt lastidx (snocTree (down sh)) arr.arr)
  913 |         EQ =>
  914 |           Balanced (A (plus arr.size 1) (append arr.arr (fill 1 (newBranch x (down sh))))) -- the current subtree is fully balanced
  915 |         GT =>
  916 |           case tryNatToFin $ minus arr.size 1 of
  917 |             Nothing   =>
  918 |               assert_total $ idris_crash "Data.RRBVector.Unsized.(|>).snocTree.Balanced: can't convert Nat to Fin"
  919 |             Just lastidx =>
  920 |               assert_total $ Balanced (A arr.size $ updateAt lastidx (snocTree (down sh)) arr.arr)
  921 |     snocTree sh (Unbalanced arr sizes) =
  922 |       case compare sh insertshift of
  923 |         LT =>
  924 |           case tryNatToFin $ minus arr.size 1 of
  925 |             Nothing       =>
  926 |               assert_total $ idris_crash "Data.RRBVector.Unsized.(|>).snocTree.Unbalanced: can't convert Nat to Fin"
  927 |             Just lastidxa =>
  928 |               case tryNatToFin $ minus sizes.size 1 of
  929 |                 Nothing       =>
  930 |                   assert_total $ idris_crash "Data.RRBVector.Unsized.(|>).snocTree.Unbalanced: can't convert Nat to Fin"
  931 |                 Just lastidxs =>
  932 |                   let lastsize = plus (at sizes.arr lastidxs) 1
  933 |                     in assert_total $ Unbalanced (A arr.size (updateAt lastidxa (snocTree (down sh)) arr.arr))
  934 |                                                  (A sizes.size (setAt lastidxs lastsize sizes.arr))
  935 |         EQ =>
  936 |           case tryNatToFin $ minus sizes.size 1 of
  937 |             Nothing      =>
  938 |               assert_total $ idris_crash "Data.RRBVector.Unsized.(|>).snocTree.Unbalanced: can't convert Nat to Fin"
  939 |             Just lastidx =>
  940 |               let lastsize = plus (at sizes.arr lastidx) 1
  941 |                 in assert_total $ Unbalanced (A (plus arr.size 1) (append arr.arr (fill 1 (newBranch x (down sh)))))
  942 |                                              (A (plus sizes.size 1) (append sizes.arr (fill 1 lastsize)))
  943 |         GT =>
  944 |           case tryNatToFin $ minus arr.size 1 of
  945 |             Nothing       =>
  946 |               assert_total $ idris_crash "Data.RRBVector.Unsized.(|>).snocTree.Unbalanced: can't convert Nat to Fin"
  947 |             Just lastidxa =>
  948 |               case tryNatToFin $ minus sizes.size 1 of
  949 |                 Nothing       =>
  950 |                   assert_total $ idris_crash "Data.RRBVector.Unsized.(|>).snocTree.Unbalanced: can't convert Nat to Fin"
  951 |                 Just lastidxs =>
  952 |                   let lastsize = plus (at sizes.arr lastidxs) 1
  953 |                     in assert_total $ Unbalanced (A arr.size (updateAt lastidxa (snocTree (down sh)) arr.arr))
  954 |                                                  (A sizes.size (setAt lastidxs lastsize sizes.arr))
  955 |     snocTree _ (Leaf arr) = Leaf (A (plus arr.size 1) (append arr.arr (fill 1 x)))
  956 | 
  957 | ||| Concatenates two vectors. O(log(max(n1,n2)))
  958 | export
  959 | (><) :  RRBVector a
  960 |      -> RRBVector a
  961 |      -> RRBVector a
  962 | Empty                >< v                    = v
  963 | v                    >< Empty                = v
  964 | Root size1 sh1 tree1 >< Root size2 sh2 tree2 =
  965 |   let upmaxshift = case compare sh1 sh2 of
  966 |                      LT =>
  967 |                        up sh2
  968 |                      EQ =>
  969 |                        up sh1
  970 |                      GT =>
  971 |                        up sh1
  972 |       newarr     = mergeTrees tree1 sh1 tree2 sh2
  973 |     in normalize $ Root (plus size1 size2) upmaxshift (computeSizes upmaxshift newarr)
  974 |   where
  975 |     viewlArr : Array (Tree a) -> (Tree a, Array (Tree a))
  976 |     viewlArr arr =
  977 |       case tryNatToFin 0 of
  978 |         Nothing   =>
  979 |           assert_total $ idris_crash "Data.RRBVector.Unsized.(><).viewlArr: can't convert Nat to Fin"
  980 |         Just zero =>
  981 |           (at arr.arr zero, drop 1 arr)
  982 |     viewrArr : Array (Tree b) -> (Array (Tree b), Tree b)
  983 |     viewrArr arr =
  984 |       case tryNatToFin $ minus arr.size 1 of
  985 |         Nothing   =>
  986 |           assert_total $ idris_crash "Data.RRBVector.Unsized.(><).viewrArr: can't convert Nat to Fin"
  987 |         Just last =>
  988 |           (take (minus arr.size 1) arr, at arr.arr last)
  989 |     mergeRebalance' :  Shift
  990 |                     -> Array (Tree a)
  991 |                     -> Array (Tree a)
  992 |                     -> Array (Tree a)
  993 |                     -> (Tree a -> Array (Tree a))
  994 |                     -> (Array (Tree a) -> Tree a)
  995 |                     -> Array (Tree a)
  996 |     mergeRebalance' sh left center right extract construct =
  997 |       runST $ do
  998 |         nodecounter    <- newSTRef 0
  999 |         subtreecounter <- newSTRef 0
 1000 |         newnode        <- newSTRef Lin
 1001 |         newsubtree     <- newSTRef Lin
 1002 |         newroot        <- newSTRef Lin
 1003 |         for_ (toList left ++ toList center ++ toList right) $ \subtree =>
 1004 |           for_ (extract subtree) $ \x => do
 1005 |             nodecounter' <- readSTRef nodecounter
 1006 |             when (nodecounter' == (natToInteger blocksize)) $ do
 1007 |               newnode' <- readSTRef newnode
 1008 |               modifySTRef newsubtree (\y => y :< (construct $ A (SnocSize newnode')
 1009 |                                                                 (snocConcat newnode'))
 1010 |                                     )
 1011 |               writeSTRef newnode Lin
 1012 |               writeSTRef nodecounter 0
 1013 |               modifySTRef subtreecounter (\y => y + 1
 1014 |                                          )
 1015 |               subtreecounter' <- readSTRef subtreecounter
 1016 |               when (subtreecounter' == (natToInteger blocksize)) $ do
 1017 |                 newsubtree' <- readSTRef newsubtree
 1018 |                 modifySTRef newroot (\y => y :< (computeSizes sh (fromList $ the (List (Tree a)) (cast newsubtree')))
 1019 |                                     )
 1020 |                 writeSTRef newsubtree Lin
 1021 |                 writeSTRef subtreecounter 0
 1022 |             modifySTRef newnode (\y => y :< (fill 1 x)
 1023 |                                 )
 1024 |             modifySTRef nodecounter (\y => y + 1
 1025 |                                     )
 1026 |         newnode' <- readSTRef newnode
 1027 |         modifySTRef newsubtree (\y => y :< (construct $ A (SnocSize newnode')
 1028 |                                                           (snocConcat newnode'))
 1029 |                                            )
 1030 |         newsubtree' <- readSTRef newsubtree
 1031 |         modifySTRef newroot (\y => y :< (computeSizes sh (fromList $ the (List (Tree a)) (cast newsubtree')))
 1032 |                             )
 1033 |         newroot' <- readSTRef newroot
 1034 |         pure $ fromList $ the (List (Tree a)) (cast newroot')
 1035 |     mergeRebalance'' :  Shift
 1036 |                      -> Array (Tree a)
 1037 |                      -> Array (Tree a)
 1038 |                      -> Array (Tree a)
 1039 |                      -> (Tree a -> Array a)
 1040 |                      -> (Array a -> Tree a)
 1041 |                      -> Array (Tree a)
 1042 |     mergeRebalance'' sh left center right extract construct =
 1043 |       runST $ do
 1044 |         nodecounter    <- newSTRef 0
 1045 |         subtreecounter <- newSTRef 0
 1046 |         newnode        <- newSTRef Lin
 1047 |         newsubtree     <- newSTRef Lin
 1048 |         newroot        <- newSTRef Lin
 1049 |         for_ (toList left ++ toList center ++ toList right) $ \subtree =>
 1050 |           for_ (extract subtree) $ \x => do
 1051 |             nodecounter' <- readSTRef nodecounter
 1052 |             when (nodecounter' == (natToInteger blocksize)) $ do
 1053 |               newnode' <- readSTRef newnode
 1054 |               modifySTRef newsubtree (\y => y :< (construct $ A (SnocSize newnode')
 1055 |                                                                 (snocConcat newnode'))
 1056 |                                     )
 1057 |               writeSTRef newnode Lin
 1058 |               writeSTRef nodecounter 0
 1059 |               modifySTRef subtreecounter (\y => y + 1
 1060 |                                          )
 1061 |               subtreecounter' <- readSTRef subtreecounter
 1062 |               when (subtreecounter' == (natToInteger blocksize)) $ do
 1063 |                 newsubtree' <- readSTRef newsubtree
 1064 |                 modifySTRef newroot (\y => y :< (computeSizes sh (fromList $ the (List (Tree a)) (cast newsubtree')))
 1065 |                                     )
 1066 |                 writeSTRef newsubtree Lin
 1067 |                 writeSTRef subtreecounter 0
 1068 |             modifySTRef newnode (\y => y :< (fill 1 x)
 1069 |                                 )
 1070 |             modifySTRef nodecounter (\y => y + 1
 1071 |                                     )
 1072 |         newnode' <- readSTRef newnode
 1073 |         modifySTRef newsubtree (\y => y :< (construct $ A (SnocSize newnode')
 1074 |                                                           (snocConcat newnode'))
 1075 |                                            )
 1076 |         newsubtree' <- readSTRef newsubtree
 1077 |         modifySTRef newroot (\y => y :< (computeSizes sh (fromList $ the (List (Tree a)) (cast newsubtree')))
 1078 |                             )
 1079 |         newroot' <- readSTRef newroot
 1080 |         pure $ fromList $ the (List (Tree a)) (cast newroot')
 1081 |     mergeRebalance :  Shift
 1082 |                    -> Array (Tree a)
 1083 |                    -> Array (Tree a)
 1084 |                    -> Array (Tree a)
 1085 |                    -> Array (Tree a)
 1086 |     mergeRebalance sh left center right =
 1087 |       case compare sh blockshift of
 1088 |         LT =>
 1089 |           assert_total $ mergeRebalance' sh left center right treeToArray (computeSizes (down sh))
 1090 |         EQ =>
 1091 |           assert_total $ mergeRebalance'' sh left center right (\(Leaf arr) => arr) Leaf
 1092 |         GT =>
 1093 |           assert_total $ mergeRebalance' sh left center right treeToArray (computeSizes (down sh))
 1094 |     mergeTrees :  Tree a
 1095 |                -> Nat
 1096 |                -> Tree a
 1097 |                -> Nat
 1098 |                -> Array (Tree a)
 1099 |     mergeTrees tree1@(Leaf arr1) _   tree2@(Leaf arr2) _   =
 1100 |       case compare arr1.size blocksize of
 1101 |         LT =>
 1102 |           let arr' = A (plus arr1.size arr2.size) (append arr1.arr arr2.arr)
 1103 |             in case compare arr'.size blocksize of
 1104 |                  LT =>
 1105 |                    singleton $ Leaf arr'
 1106 |                  EQ =>
 1107 |                    singleton $ Leaf arr'
 1108 |                  GT =>
 1109 |                    let (left, right) = (take blocksize arr',drop blocksize arr')
 1110 |                        lefttree      = Leaf left
 1111 |                        righttree     = Leaf right
 1112 |                      in A 2 $ fromPairs 2 lefttree [(1,righttree)]
 1113 |         EQ =>
 1114 |           A 2 $ fromPairs 2 tree1 [(1,tree2)]
 1115 |         GT =>
 1116 |           let arr' = A (plus arr1.size arr2.size) (append arr1.arr arr2.arr)
 1117 |             in case compare arr'.size blocksize of
 1118 |                  LT =>
 1119 |                    singleton $ Leaf arr'
 1120 |                  EQ =>
 1121 |                    singleton $ Leaf arr'
 1122 |                  GT =>
 1123 |                    let (left, right) = (take blocksize arr',drop blocksize arr')
 1124 |                        lefttree      = Leaf left
 1125 |                        righttree     = Leaf right
 1126 |                      in A 2 $ fromPairs 2 lefttree [(1,righttree)]
 1127 |     mergeTrees tree1             sh1 tree2             sh2 =
 1128 |       case compare sh1 sh2 of
 1129 |         LT =>
 1130 |           let right                  = treeToArray tree2
 1131 |               (righthead, righttail) = viewlArr right
 1132 |               merged                 = assert_total $ mergeTrees tree1 sh1 righthead (down sh2)
 1133 |             in mergeRebalance sh2 empty merged righttail
 1134 |         GT =>
 1135 |           let left                 = treeToArray tree1
 1136 |               (leftinit, leftlast) = viewrArr left
 1137 |               merged               = assert_total $ mergeTrees leftlast (down sh1) tree2 sh2
 1138 |             in mergeRebalance sh1 leftinit merged empty
 1139 |         EQ =>
 1140 |           let left                   = treeToArray tree1
 1141 |               right                  = treeToArray tree2
 1142 |               (leftinit, leftlast)   = viewrArr left
 1143 |               (righthead, righttail) = viewlArr right
 1144 |               merged                 = assert_total $ mergeTrees leftlast (down sh1) righthead (down sh2)
 1145 |             in mergeRebalance sh1 leftinit merged righttail
 1146 | 
 1147 | ||| Insert an element at the given index, shifting the rest of the vector over.
 1148 | ||| If the index is negative, add the element to the left end of the vector.
 1149 | ||| If the index is bigger than or equal to the length of the vector, add the element to the right end of the vector. O(log n)
 1150 | export
 1151 | insertAt :  Nat
 1152 |          -> a
 1153 |          -> RRBVector a
 1154 |          -> RRBVector a
 1155 | insertAt i x v =
 1156 |   let (left, right) = splitAt i v
 1157 |     in (left |> x) >< right
 1158 | 
 1159 | ||| Delete the element at the given index.
 1160 | ||| If the index is out of range, return the original vector. O(log n)
 1161 | export
 1162 | deleteAt :  Nat
 1163 |          -> RRBVector a
 1164 |          -> RRBVector a
 1165 | deleteAt i v =
 1166 |   let (left, right) = splitAt (plus i 1) v
 1167 |     in take i left >< right
 1168 | 
 1169 | --------------------------------------------------------------------------------
 1170 | --          Show Utilities (RRB-Vector)
 1171 | --------------------------------------------------------------------------------
 1172 | 
 1173 | ||| Show the full representation of the vector.
 1174 | export
 1175 | showRRBVectorRep :  Show a
 1176 |                  => Show (Tree a)
 1177 |                  => Show (RRBVector a)
 1178 |                  => RRBVector a
 1179 |                  -> String
 1180 | showRRBVectorRep Empty            =
 1181 |   ""
 1182 | showRRBVectorRep (Root size sh t) =
 1183 |   "RRBVector "    ++
 1184 |   "{ "            ++
 1185 |   "Size = "       ++
 1186 |   (show size)     ++
 1187 |   ", Shift = "    ++
 1188 |   (show sh)       ++
 1189 |   ", Tree = "     ++
 1190 |   (showTreeRep t) ++
 1191 |   "}"
 1192 | 
 1193 | --------------------------------------------------------------------------------
 1194 | --          Interfaces (RRBVector)
 1195 | --------------------------------------------------------------------------------
 1196 | 
 1197 | export
 1198 | Eq a => Eq (RRBVector a) where
 1199 |   xs == ys = length xs == length ys && Data.RRBVector.Unsized.toList xs == Data.RRBVector.Unsized.toList ys
 1200 | 
 1201 | export
 1202 | Ord a => Ord (RRBVector a) where
 1203 |   compare xs ys = compare (Data.RRBVector.Unsized.toList xs) (Data.RRBVector.Unsized.toList ys)
 1204 | 
 1205 | export
 1206 | Functor RRBVector where
 1207 |   map f v = map f v
 1208 | 
 1209 | export
 1210 | Foldable RRBVector where
 1211 |   foldl f z           = Data.RRBVector.Unsized.foldl f z
 1212 |   foldr f z           = Data.RRBVector.Unsized.foldr f z
 1213 |   null                = null
 1214 | 
 1215 | export
 1216 | Applicative RRBVector where
 1217 |   pure      = singleton
 1218 |   fs <*> xs = Data.RRBVector.Unsized.foldl (\acc, f => acc >< map f xs) empty fs
 1219 | 
 1220 | export
 1221 | Semigroup (RRBVector a) where
 1222 |   (<+>) = (><)
 1223 | 
 1224 | export
 1225 | Semigroup (RRBVector a) => Monoid (RRBVector a) where
 1226 |   neutral = empty
 1227 | 
 1228 | export
 1229 | Monad RRBVector where
 1230 |   xs >>= f = Data.RRBVector.Unsized.foldl (\acc, x => acc >< f x) empty xs
 1231 |