
    0 | ||| Linear Relaxed Radix Balanced Vectors (RRBVector1)
    1 | module Data.RRBVector1.Unsized
    2 | 
    3 | import public Data.RRBVector1.Unsized.Internal
    4 | 
    5 | import Data.Array.Core
    6 | import Data.Array.Index
    7 | import Data.Array.Indexed
    8 | import Data.Array.Mutable
    9 | import Data.Bits
   10 | import Data.Maybe
   11 | import Data.Linear.Ref1
   12 | import Data.List
   13 | import Data.List1
   14 | import Data.SnocList
   15 | import Data.Vect
   16 | import Data.Zippable
   17 | 
   18 | %hide Data.Array.Core.take
   19 | %hide Data.Array.Indexed.drop
   20 | %hide Data.Linear.splitAt
   21 | %hide Data.Linear.(::)
   22 | %hide Data.List.drop
   23 | %hide Data.List.lookup
   24 | %hide Data.List.take
   25 | %hide Data.List.singleton
   26 | %hide Data.List1.singleton
   27 | %hide Data.Vect.drop
   28 | %hide Data.Vect.lookup
   29 | %hide Data.Vect.splitAt
   30 | %hide Data.Vect.take
   31 | %hide Data.Vect.Stream.take
   32 | %hide Data.Vect.(::)
   33 | %hide Prelude.null
   34 | %hide Prelude.take
   35 | %hide Prelude.(|>)
   36 | %hide Prelude.Ops.infixr.(<|)
   37 | %hide Prelude.Ops.infixl.(|>)
   38 | %hide Prelude.Stream.(::)
   39 | 
   40 | %default total
   41 | 
   42 | --------------------------------------------------------------------------------
   43 | --          Fixity
   44 | --------------------------------------------------------------------------------
   45 | 
   46 | export
   47 | infixr 5 ><
   48 | 
   49 | export
   50 | infixr 5 <|
   51 | 
   52 | export
   53 | infixl 5 |>
   54 | 
   55 | --------------------------------------------------------------------------------
   56 | --          Creating linear RRB-Vectors
   57 | --------------------------------------------------------------------------------
   58 | 
   59 | ||| The empty vector. O(1)
   60 | export
   61 | empty : F1 s (RRBVector1 s a)
   62 | empty t =
   63 |   Empty # t
   64 | 
   65 | ||| A vector with a single element. O(1)
   66 | export
   67 | singleton :  a
   68 |           -> F1 s (RRBVector1 s a)
   69 | singleton x t =
   70 |   let newarr # t := marray1 1 x t
   71 |     in Root 1 0 (Leaf {lsize=1} (1 ** newarr)) # t
   72 | 
   73 | ||| Create a new vector from a list. O(n)
   74 | export
   75 | fromList :  List a
   76 |          -> F1 s (RRBVector1 s a)
   77 | fromList []  t = empty t
   78 | fromList [x] t = singleton x t
   79 | fromList xs  t =
   80 |   let trees # t := nodes xs Lin t
   81 |     in case trees of
   82 |          [tree] =>
   83 |            let treesize # t := treeSize 0 tree t
   84 |              in (Root treesize 0 tree) # t
   85 |          xs'    =>
   86 |            assert_smaller xs (iterateNodes blockshift xs' t)
   87 |   where
   88 |     nodes :  List a
   89 |           -> SnocList (Tree1 s a)
   90 |           -> F1 s (List (Tree1 s a))
   91 |     nodes l sl with (splitAt blocksize l) | ((length (fst (splitAt blocksize l))) <= (length l)) proof eq
   92 |       _ | (cl, cl') | True  = \t =>
   93 |         let trees'  # t := unsafeMArray1 (length l) t
   94 |             ()      # t := writeList trees' l t
   95 |             trees'' # t := mtake trees' (length (fst (splitAt blocksize l))) @{lteOpReflectsLTE _ _ eq} t
   96 |           in case cl' of
   97 |                []   =>
   98 |                  let trees''' := Leaf {lsize=(length (fst (splitAt blocksize l)))} ((length (fst (splitAt blocksize l))) ** trees'')
   99 |                      sl'      := sl :< trees'''
  100 |                    in (sl' <>> []) # t
  101 |                cl'' =>
  102 |                  let trees''' := Leaf {lsize=(length (fst (splitAt blocksize l)))} ((length (fst (splitAt blocksize l))) ** trees'')
  103 |                      sl'      := sl :< trees'''
  104 |                    in (nodes (assert_smaller l cl'') sl') t
  105 |       _ | _         | False = \t =>
  106 |         (assert_total $ idris_crash "Data.RRBVector1.fromList.nodes: index out of bounds") # t
  107 |     nodes' :  Nat
  108 |            -> List (Tree1 s a)
  109 |            -> SnocList (Tree1 s a)
  110 |            -> F1 s (List (Tree1 s a))
  111 |     nodes' sh l sl with (splitAt blocksize l) | ((length (fst (splitAt blocksize l))) <= (length l)) proof eq
  112 |       _ | (cl, cl') | True  = \t =>
  113 |         let trees'  # t := unsafeMArray1 (length l) t
  114 |             ()      # t := writeList trees' l t
  115 |             trees'' # t := mtake trees' (length (fst (splitAt blocksize l))) @{lteOpReflectsLTE _ _ eq} t
  116 |           in case cl' of
  117 |                []   =>
  118 |                  let trees''' := Balanced {bsize=(length (fst (splitAt blocksize l)))} ((length (fst (splitAt blocksize l))) ** trees'')
  119 |                      sl'      := sl :< trees'''
  120 |                    in (sl' <>> []) # t
  121 |                cl'' =>
  122 |                  let trees''' := Balanced {bsize=(length (fst (splitAt blocksize l)))} ((length (fst (splitAt blocksize l))) ** trees'')
  123 |                      sl'      := sl :< trees'''
  124 |                    in (nodes' sh (assert_smaller l cl'') sl') t
  125 |       _ | _         | False = \t =>
  126 |         (assert_total $ idris_crash "Data.RRBVector1.fromList.nodes': index out of bounds") # t
  127 |     iterateNodes :  Nat
  128 |                  -> List (Tree1 s a)
  129 |                  -> F1 s (RRBVector1 s a)
  130 |     iterateNodes sh trees t =
  131 |       let trees' # t := nodes' sh trees Lin t
  132 |         in case trees' of
  133 |              [tree]  =>
  134 |                let treesize # t := treeSize sh tree t
  135 |                  in (Root treesize sh tree) # t
  136 |              trees'' =>
  137 |                iterateNodes (up sh) (assert_smaller trees trees'') t
  138 | 
  139 | ||| Creates a vector of length n with every element set to x. O(log n)
  140 | export
  141 | replicate :  Nat
  142 |           -> a
  143 |           -> F1 s (RRBVector1 s a)
  144 | replicate n x t =
  145 |   case compare n 0 of
  146 |     LT =>
  147 |       Empty # t
  148 |     EQ =>
  149 |       Empty # t
  150 |     GT =>
  151 |       case compare n blocksize of
  152 |         LT =>
  153 |           let newarr # t := marray1 n x t
  154 |             in Root n 0 (Leaf {lsize=n} (n ** newarr)) # t
  155 |         EQ =>
  156 |           let newarr # t := marray1 n x t
  157 |             in Root n 0 (Leaf {lsize=n} (n ** newarr)) # t
  158 |         GT =>
  159 |           let size'       := integerToNat ((natToInteger $ minus n 1) .&. (natToInteger $ plus blockmask 1))
  160 |               newarr1 # t := marray1 blocksize x t
  161 |               newarr2 # t := marray1 size' x t
  162 |               tree1       := Leaf {lsize=blocksize} (blocksize ** newarr1)
  163 |               tree2       := Leaf {lsize=size'} (size' ** newarr2)
  164 |             in iterateNodes blockshift
  165 |                             tree1
  166 |                             tree2
  167 |                             t
  168 |   where
  169 |     iterateNodes :  (sh : Shift)
  170 |                  -> (full : Tree1 s a)
  171 |                  -> (rest : Tree1 s a)
  172 |                  -> F1 s (RRBVector1 s a)
  173 |     iterateNodes sh full rest t =
  174 |       let subtreesm1   := (natToInteger $ minus n 1) `shiftR` sh
  175 |           restsize     := integerToNat (subtreesm1 .&. (natToInteger blockmask))
  176 |           mappend1 # t := marray1 restsize full t
  177 |           mappend2 # t := marray1 1 rest t
  178 |           rest'    # t := mappend mappend1 mappend2 t
  179 |           rest''       := Balanced {bsize=plus restsize 1} ((plus restsize 1) ** rest')
  180 |         in case compare subtreesm1 (natToInteger blocksize) of
  181 |              LT =>
  182 |                (Root n sh rest'') # t
  183 |              EQ =>
  184 |                let newarr # t := marray1 blocksize full t
  185 |                    full'      := Balanced {bsize=blocksize} (blocksize ** newarr)
  186 |                  in iterateNodes (up sh)
  187 |                                  (assert_smaller full full')
  188 |                                  (assert_smaller rest rest'')
  189 |                                  t
  190 |              GT =>
  191 |                let newarr # t := marray1 blocksize full t
  192 |                    full'      := Balanced {bsize=blocksize} (blocksize ** newarr)
  193 |                  in iterateNodes (up sh)
  194 |                                  (assert_smaller full full')
  195 |                                  (assert_smaller rest rest'')
  196 |                                  t
  197 | 
  198 | --------------------------------------------------------------------------------
  199 | --          Creating linear lists from linear RRB-Vectors
  200 | --------------------------------------------------------------------------------
  201 | 
  202 | private
  203 | treeToList :  (n ** MArray s n (Tree1 s a))
  204 |            -> F1 s (List a)
  205 | treeToList (n ** arr) t =
  206 |   go 0 n Lin t
  207 |   where
  208 |     go :  (m, x : Nat)
  209 |        -> (sl : SnocList a)
  210 |        -> {auto v : Ix x n}
  211 |        -> F1 s (List a)
  212 |     go m Z     sl t =
  213 |       (sl <>> []) # t
  214 |     go m (S j) sl t =
  215 |       let j' # t := getIx arr j t
  216 |         in case j' of
  217 |              (Balanced (b ** arr'))     =>
  218 |                let arr'' # t := assert_total $ treeToList (b ** arr') t
  219 |                    sl'       := sl <>< arr''
  220 |                  in go (S m) j sl' t
  221 |              (Unbalanced (u ** arr') _) =>
  222 |                let arr'' # t := assert_total $ treeToList (u ** arr') t
  223 |                    sl'       := sl <>< arr''
  224 |                  in go (S m) j sl' t
  225 |              (Leaf (_ ** arr'))         =>
  226 |                let arr'' # t := freeze arr' t
  227 |                    arr'''    := toList arr''
  228 |                    sl'       := sl <>< arr'''
  229 |                  in go (S m) j sl' t
  230 | 
  231 | ||| Convert a vector to a list. O(n)
  232 | export
  233 | toList :  RRBVector1 s a
  234 |        -> F1 s (List a)
  235 | toList Empty                                t =
  236 |   [] # t
  237 | toList (Root _ _ (Balanced (b ** arr)))     t =
  238 |   treeToList (b ** arr) t
  239 | toList (Root _ _ (Unbalanced (u ** arr) _)) t =
  240 |   treeToList (u ** arr) t
  241 | toList (Root _ _ (Leaf (_ ** arr)))         t =
  242 |   let arr' # t := freeze arr t
  243 |     in toList arr' # t
  244 | 
  245 | --------------------------------------------------------------------------------
  246 | --          Query
  247 | --------------------------------------------------------------------------------
  248 | 
  249 | ||| Is the vector empty? O(1)
  250 | export
  251 | null :  RRBVector1 s a
  252 |      -> F1 s Bool
  253 | null Empty t =
  254 |   True # t
  255 | null _     t =
  256 |   False # t
  257 | 
  258 | ||| Return the size of a vector. O(1)
  259 | export
  260 | length :  RRBVector1 s a
  261 |        -> F1 s Nat
  262 | length Empty        t =
  263 |   0 # t
  264 | length (Root s _ _) t =
  265 |   s # t
  266 | 
  267 | --------------------------------------------------------------------------------
  268 | --          Indexing
  269 | --------------------------------------------------------------------------------
  270 | 
  271 | ||| The element at the index or Nothing if the index is out of range. O(log n)
  272 | export
  273 | lookup :  Nat
  274 |        -> RRBVector1 s a
  275 |        -> F1 s (Maybe a)
  276 | lookup _ Empty               t = Nothing # t
  277 | lookup i (Root size sh tree) t =
  278 |   case compare i 0 of
  279 |     LT =>
  280 |       Nothing # t -- index out of range
  281 |     GT =>
  282 |       case compare i size of
  283 |         EQ =>
  284 |           Nothing # t -- index out of range
  285 |         GT =>
  286 |           Nothing # t -- index out of range
  287 |         LT =>
  288 |           let lookup' # t := lookupTree i sh tree t
  289 |             in Just lookup' # t
  290 |     EQ =>
  291 |       case compare i size of
  292 |         EQ =>
  293 |           Nothing # t -- index out of range
  294 |         GT =>
  295 |           Nothing # t -- index out of range
  296 |         LT =>
  297 |           let lookup' # t := lookupTree i sh tree t
  298 |             in Just lookup' # t
  299 |   where
  300 |     lookupTree :  Nat
  301 |                -> Nat
  302 |                -> Tree1 s a
  303 |                -> F1 s a
  304 |     lookupTree i sh (Balanced (_ ** arr))         t =
  305 |       case tryNatToFin (radixIndex i sh) of
  306 |         Nothing =>
  307 |           (assert_total $ idris_crash "Data.RRBVector.lookup.lookupTree: can't convert Nat to Fin") # t
  308 |         Just i' =>
  309 |           let i'' # t := get arr i' t
  310 |             in assert_total $ lookupTree i (down sh) i'' t
  311 |     lookupTree i sh (Unbalanced (_ ** arr) sizes) t =
  312 |       let (idx, subidx) := relaxedRadixIndex sizes i sh
  313 |         in case tryNatToFin idx of
  314 |              Nothing =>
  315 |                (assert_total $ idris_crash "Data.RRBVector.lookup.lookupTree: can't convert Nat to Fin") # t
  316 |              Just i' =>
  317 |                let i'' # t := get arr i' t
  318 |                  in assert_total $ lookupTree subidx (down sh) i'' t
  319 |     lookupTree i _  (Leaf (_ ** arr))             t =
  320 |       let i' = integerToNat ((natToInteger i) .&. (natToInteger blockmask))
  321 |         in case tryNatToFin i' of
  322 |              Nothing  =>
  323 |                (assert_total $ idris_crash "Data.RRBVector.lookup.lookupTree: can't convert Nat to Fin") # t
  324 |              Just i'' =>
  325 |                let i''' # t := get arr i'' t
  326 |                  in i''' # t
  327 | 
  328 | ||| The element at the index.
  329 | ||| Calls 'idris_crash' if the index is out of range. O(log n)
  330 | export
  331 | index :  Nat
  332 |       -> RRBVector1 s a
  333 |       -> F1 s a
  334 | index i v t =
  335 |   let lookup' # t := lookup i v t
  336 |     in case lookup' of
  337 |          Nothing       =>
  338 |            (assert_total $ idris_crash "Data.RRBVector.index: index out of range") # t
  339 |          Just lookup'' =>
  340 |            lookup'' # t
  341 | 
  342 | ||| A flipped version of lookup. O(log n)
  343 | export
  344 | (!?) :  RRBVector1 s a
  345 |      -> Nat
  346 |      -> F1 s (Maybe a)
  347 | (!?) t = flip lookup t
  348 | 
  349 | ||| A flipped version of index. O(log n)
  350 | export
  351 | (!!) :  RRBVector1 s a
  352 |      -> Nat
  353 |      -> F1 s a
  354 | (!!) t = flip index t
  355 | 
  356 | ||| Update the element at the index with a new element.
  357 | ||| If the index is out of range, the original vector is returned. O(log n)
  358 | export
  359 | update :  Nat
  360 |        -> a
  361 |        -> RRBVector1 s a
  362 |        -> F1 s (RRBVector1 s a)
  363 | update _ _ Empty                 t = Empty # t
  364 | update i x v@(Root size sh tree) t =
  365 |   case compare i 0 of
  366 |     LT =>
  367 |       v # t -- index out of range
  368 |     GT =>
  369 |       case compare i size of
  370 |         EQ =>
  371 |           v # t -- index out of range
  372 |         GT =>
  373 |           v # t -- index out of range
  374 |         LT =>
  375 |           let update' # t := updateTree i sh tree t
  376 |             in ( Root size
  377 |                       sh
  378 |                       update'
  379 |                ) # t
  380 |     EQ =>
  381 |       case compare i size of
  382 |         EQ =>
  383 |           v # t -- index out of range
  384 |         GT =>
  385 |           v # t -- index out of range
  386 |         LT =>
  387 |           let update' # t := updateTree i sh tree t
  388 |             in ( Root size
  389 |                       sh
  390 |                       update'
  391 |                ) # t
  392 |   where
  393 |     updateTree :  Nat
  394 |                -> Nat
  395 |                -> Tree1 s a
  396 |                -> F1 s (Tree1 s a)
  397 |     updateTree i sh (Balanced (b ** arr))         t =
  398 |       case tryNatToFin (radixIndex i sh) of
  399 |         Nothing =>
  400 |           (assert_total $ idris_crash "Data.RRBVector.update.updateTree: can't convert Nat to Fin") # t
  401 |         Just i' =>
  402 |           let newtree  # t := get arr i' t
  403 |               newtree' # t := assert_total $ updateTree i (down sh) newtree t
  404 |               ()       # t := casswap arr i' newtree' t
  405 |             in (Balanced {bsize=b} (b ** arr)) # t
  406 |     updateTree i sh (Unbalanced (u ** arr) sizes) t =
  407 |       let (idx, subidx) := relaxedRadixIndex sizes i sh
  408 |         in case tryNatToFin idx of
  409 |              Nothing   =>
  410 |                (assert_total $ idris_crash "Data.RRBVector.update.updateTree: can't convert Nat to Fin") # t
  411 |              Just idx' =>
  412 |                let newtree  # t := get arr idx' t
  413 |                    newtree' # t := assert_total $ updateTree subidx (down sh) newtree t
  414 |                    ()       # t := casswap arr idx' newtree' t
  415 |                  in (Unbalanced (u ** arr) sizes) # t
  416 |     updateTree i _  (Leaf (l ** arr))             t =
  417 |       let i' = integerToNat ((natToInteger i) .&. (natToInteger blockmask))
  418 |         in case tryNatToFin i' of
  419 |              Nothing =>
  420 |                (assert_total $ idris_crash "Data.RRBVector.update: can't convert Nat to Fin") # t
  421 |              Just i'' =>
  422 |                let () # t := casswap arr i'' x t
  423 |                  in (Leaf {lsize=l} (l ** arr)) # t
  424 | 
  425 | ||| Adjust the element at the index by applying the function to it.
  426 | ||| If the index is out of range, the original vector is returned. O(log n)
  427 | export
  428 | adjust :  Nat
  429 |        -> (a -> a)
  430 |        -> RRBVector1 s a
  431 |        -> F1 s (RRBVector1 s a)
  432 | adjust _ _ Empty                 t = Empty # t
  433 | adjust i f v@(Root size sh tree) t =
  434 |   case compare i 0 of
  435 |     LT =>
  436 |       v # t -- index out of range
  437 |     GT =>
  438 |       case compare i size of
  439 |         EQ =>
  440 |           v # t -- index out of range
  441 |         GT =>
  442 |           v # t -- index out of range
  443 |         LT =>
  444 |           let adjust' # t := adjustTree i sh tree t
  445 |             in ( Root size
  446 |                       sh
  447 |                       adjust'
  448 |                ) # t
  449 |     EQ =>
  450 |       case compare i size of
  451 |         EQ =>
  452 |           v # t -- index out of range
  453 |         GT =>
  454 |           v # t -- index out of range
  455 |         LT =>
  456 |           let adjust' # t := adjustTree i sh tree t
  457 |             in ( Root size
  458 |                       sh
  459 |                       adjust'
  460 |                ) # t
  461 |   where
  462 |     adjustTree :  Nat
  463 |                -> Nat
  464 |                -> Tree1 s a
  465 |                -> F1 s (Tree1 s a)
  466 |     adjustTree i sh (Balanced (b ** arr))         t =
  467 |       case tryNatToFin (radixIndex i sh) of
  468 |         Nothing =>
  469 |           (assert_total $ idris_crash "Data.RRBVector.adjust: can't convert Nat to Fin") # t
  470 |         Just i' =>
  471 |           let newtree  # t := get arr i' t
  472 |               newtree' # t := assert_total $ adjustTree i (down sh) newtree t
  473 |               ()       # t := casswap arr i' newtree' t
  474 |             in (Balanced {bsize=b} (b ** arr)) # t
  475 |     adjustTree i sh (Unbalanced (u ** arr) sizes) t =
  476 |       let (idx, subidx) := relaxedRadixIndex sizes i sh
  477 |         in case tryNatToFin idx of
  478 |              Nothing   =>
  479 |                (assert_total $ idris_crash "Data.RRBVector.adjust: can't convert Nat to Fin") # t
  480 |              Just idx' =>
  481 |                let newtree  # t := get arr idx' t
  482 |                    newtree' # t := assert_total $ adjustTree subidx (down sh) newtree t
  483 |                    ()       # t := casswap arr idx' newtree' t
  484 |                  in (Unbalanced (u ** arr) sizes) # t
  485 |     adjustTree i _  (Leaf (l ** arr))             t =
  486 |       let i' = integerToNat ((natToInteger i) .&. (natToInteger blockmask))
  487 |         in case tryNatToFin i' of
  488 |              Nothing =>
  489 |                (assert_total $ idris_crash "Data.RRBVector.adjust: can't convert Nat to Fin") # t
  490 |              Just i'' =>
  491 |                let () # t := modify arr i'' f t
  492 |                  in (Leaf {lsize=l} (l ** arr)) # t
  493 | 
  494 | private
  495 | normalize :  RRBVector1 s a
  496 |           -> F1 s (RRBVector1 s a)
  497 | normalize v@(Root size sh (Balanced (b ** arr)))         t =
  498 |   case compare b 1 of
  499 |     LT =>
  500 |       v # t
  501 |     EQ =>
  502 |       case tryNatToFin 0 of
  503 |         Nothing   =>
  504 |           (assert_total $ idris_crash "Data.RRBVector.normalize: can't convert Nat to Fin") # t
  505 |         Just zero =>
  506 |           let arr' # t := get arr zero t
  507 |             in assert_total $ (normalize (Root size (down sh) arr') t)
  508 |     GT =>
  509 |       v # t
  510 | normalize v@(Root size sh (Unbalanced (u ** arr) sizes)) t =
  511 |   case compare u 1 of
  512 |     LT =>
  513 |       v # t
  514 |     EQ =>
  515 |       case tryNatToFin 0 of
  516 |         Nothing   =>
  517 |           (assert_total $ idris_crash "Data.RRBVector.normalize: can't convert Nat to Fin") # t
  518 |         Just zero =>
  519 |           let arr' # t := get arr zero t
  520 |             in assert_total $ (normalize (Root size (down sh) arr') t)
  521 |     GT =>
  522 |       v # t
  523 | normalize v                                                 t =
  524 |   v # t
  525 | 
  526 | ||| The initial i is n - 1 (the index of the last element in the new tree).
  527 | private
  528 | takeTree :  Nat
  529 |          -> Shift
  530 |          -> Tree1 s a
  531 |          -> F1 s (Tree1 s a)
  532 | takeTree i sh (Balanced (b ** arr)) with (radixIndex i sh) | ((plus (radixIndex i sh) 1) <= b) proof eq
  533 |   _ | i' | True  = \t =>
  534 |     case tryNatToFin i' of
  535 |       Nothing  =>
  536 |         (assert_total $ idris_crash "Data.RRBVector1.takeTree: can't convert Nat to Fin") # t
  537 |       Just i'' =>
  538 |         let arr'     # t := mtake arr (plus (radixIndex i sh) 1) @{lteOpReflectsLTE _ _ eq} t
  539 |             newtree  # t := get arr' i'' t
  540 |             newtree' # t := assert_total $ takeTree i (down sh) newtree t
  541 |             ()       # t := casswap arr' i'' newtree' t
  542 |           in (Balanced {bsize=(plus (radixIndex i sh) 1)} ((plus (radixIndex i sh) 1) ** arr')) # t
  543 |   _ | _  | False = \t =>
  544 |     (assert_total $ idris_crash "Data.RRBVector1.takeTree: index out of bounds") # t
  545 | takeTree i sh (Unbalanced (u ** arr) sizes) with (relaxedRadixIndex sizes i sh) | ((plus (fst (relaxedRadixIndex sizes i sh)) 1) <= u) proof eq
  546 |   _ | (idx, subidx) | True  = \t =>
  547 |     case tryNatToFin idx of
  548 |       Nothing   =>
  549 |         (assert_total $ idris_crash "Data.RRBVector1.takeTree: can't convert Nat to Fin") # t
  550 |       Just idx' =>
  551 |         let arr'      # t := mtake arr (plus (fst (relaxedRadixIndex sizes i sh)) 1) @{lteOpReflectsLTE _ _ eq} t
  552 |             newtree   # t := get arr' idx' t
  553 |             newtree'  # t := assert_total $ takeTree subidx (down sh) newtree t
  554 |             ()        # t := casswap arr' idx' newtree' t
  555 |             newtree'' # t := computeSizes sh arr' t
  556 |           in newtree'' # t
  557 |   _ | _             | False = \t =>
  558 |     (assert_total $ idris_crash "Data.RRBVector1.takeTree: index out of bounds") # t
  559 | takeTree i _ (Leaf (l ** arr)) with (integerToNat (((natToInteger i) .&. (natToInteger blockmask)) + 1) <= l) proof eq
  560 |   _ | True  = \t =>
  561 |     case ((integerToNat (((natToInteger i) .&. (natToInteger blockmask)) + 1)) <= l) of
  562 |       True  =>
  563 |         let arr' # t := mtake arr (integerToNat (((natToInteger i) .&. (natToInteger blockmask)) + 1)) @{lteOpReflectsLTE _ _ eq} t
  564 |           in (Leaf {lsize=(integerToNat (((natToInteger i) .&. (natToInteger blockmask)) + 1))} ((integerToNat (((natToInteger i) .&. (natToInteger blockmask)) + 1)) ** arr')) # t
  565 |       False =>
  566 |         (assert_total $ idris_crash "Data.RRBVector1.takeTree: index out of bounds") # t
  567 |   _ | False = \t =>
  568 |     (assert_total $ idris_crash "Data.RRBVector1.takeTree: index out of bounds") # t
  569 | 
  570 | private
  571 | dropTree :  Nat
  572 |          -> Shift
  573 |          -> Tree1 s a
  574 |          -> F1 s (Tree1 s a)
  575 | dropTree n sh (Balanced (b ** arr))         t =
  576 |   let idx := radixIndex n sh
  577 |     in case tryNatToFin 0 of
  578 |          Nothing   =>
  579 |            (assert_total $ idris_crash "Data.RRBVector.dropTree: can't convert Nat to Fin") # t
  580 |          Just zero =>
  581 |            let arr'      # t := mdrop idx arr t
  582 |                newtree   # t := get arr' zero t
  583 |                newtree'  # t := assert_total $ dropTree n (down sh) newtree t
  584 |                ()        # t := casswap arr' zero newtree' t
  585 |                newtree'' # t := computeSizes sh arr' t
  586 |              in newtree'' # t
  587 | dropTree n sh (Unbalanced (u ** arr) sizes) t =
  588 |   let (idx, subidx) := relaxedRadixIndex sizes n sh
  589 |     in case tryNatToFin 0 of
  590 |          Nothing   =>
  591 |            (assert_total $ idris_crash "Data.RRBVector.dropTree: can't convert Nat to Fin") # t
  592 |          Just zero =>
  593 |            let arr'      # t := mdrop idx arr t
  594 |                newtree   # t := get arr' zero t
  595 |                newtree'  # t := assert_total $ dropTree subidx (down sh) newtree t
  596 |                ()        # t := casswap arr' zero newtree' t
  597 |                newtree'' # t := computeSizes sh arr' t
  598 |              in newtree'' # t
  599 | dropTree n _  (Leaf (l ** arr))             t =
  600 |   let n'       := integerToNat ((natToInteger n) .&. (natToInteger blockmask))
  601 |       arr' # t := mdrop n' arr t
  602 |     in (Leaf {lsize=minus l n'} ((minus l n') ** arr')) # t
  603 | 
  604 | ||| The first i elements of the vector.
  605 | ||| If the vector contains less than or equal to i elements, the whole vector is returned. O(log n)
  606 | export
  607 | take :  Nat
  608 |      -> RRBVector1 s a
  609 |      -> F1 s (RRBVector1 s a)
  610 | take _ Empty                 t = empty t
  611 | take n v@(Root size sh tree) t =
  612 |   case compare n 0 of
  613 |     LT =>
  614 |       empty t
  615 |     EQ =>
  616 |       empty t
  617 |     GT =>
  618 |       case compare n size of
  619 |         LT =>
  620 |           let tt # t := takeTree (minus n 1) sh tree t
  621 |             in normalize (Root n sh tt) t
  622 |         EQ =>
  623 |           v # t
  624 |         GT =>
  625 |           v # t
  626 | 
  627 | ||| The vector without the first i elements.
  628 | ||| If the vector contains less than or equal to i elements, the empty vector is returned. O(log n)
  629 | export
  630 | drop :  Nat
  631 |      -> RRBVector1 s a
  632 |      -> F1 s (RRBVector1 s a)
  633 | drop _ Empty                 t = empty t
  634 | drop n v@(Root size sh tree) t =
  635 |   case compare n 0 of
  636 |     LT =>
  637 |       v # t
  638 |     EQ =>
  639 |       v # t
  640 |     GT =>
  641 |       case compare n size of
  642 |         LT =>
  643 |           let dt # t := dropTree n sh tree t
  644 |             in normalize (Root (size `minus` n) sh dt) t
  645 |         EQ =>
  646 |           empty t
  647 |         GT =>
  648 |           empty t
  649 | 
  650 | ||| Split the vector at the given index. O(log n)
  651 | export
  652 | splitAt :  Nat
  653 |         -> RRBVector1 s a
  654 |         -> F1 s (RRBVector1 s a, RRBVector1 s a)
  655 | splitAt _ Empty                 t = (Empty, Empty) # t
  656 | splitAt n v@(Root size sh tree) t =
  657 |   case compare n 0 of
  658 |     LT =>
  659 |       (Empty, v) # t
  660 |     EQ =>
  661 |       (Empty, v) # t
  662 |     GT =>
  663 |       case compare n size of
  664 |         LT =>
  665 |           let dt    # t := dropTree n sh tree t
  666 |               tt    # t := takeTree (minus n 1) sh tree t
  667 |               left  # t := normalize (Root n sh tt) t
  668 |               right # t := normalize (Root (size `minus` n) sh dt) t
  669 |             in (left, right) # t
  670 |         EQ =>
  671 |           (v, Empty) # t
  672 |         GT =>
  673 |           (v, Empty) # t
  674 | 
  675 | --------------------------------------------------------------------------------
  676 | --          Deconstruction
  677 | --------------------------------------------------------------------------------
  678 | 
  679 | ||| The first element and the vector without the first element, or 'Nothing' if the vector is empty. O(log n)
  680 | export
  681 | viewl :  RRBVector1 s a
  682 |       -> F1 s (Maybe (a, RRBVector1 s a))
  683 | viewl Empty             t = Nothing # t
  684 | viewl v@(Root _ _ tree) t =
  685 |   let tail # t := drop 1 v t
  686 |       head # t := headTree tree t
  687 |     in (Just (head, tail)) # t
  688 |   where
  689 |     headTree :  Tree1 s a
  690 |              -> F1 s a
  691 |     headTree (Balanced (_ ** arr))     t =
  692 |       case tryNatToFin 0 of
  693 |         Nothing   =>
  694 |           (assert_total $ idris_crash "Data.RRBVector.viewl: can't convert Nat to Fin") # t
  695 |         Just zero =>
  696 |           let headtree # t := get arr zero t
  697 |             in assert_total $ headTree headtree t
  698 |     headTree (Unbalanced (_ ** arr) _) t =
  699 |       case tryNatToFin 0 of
  700 |         Nothing   =>
  701 |           (assert_total $ idris_crash "Data.RRBVector.viewl: can't convert Nat to Fin") # t
  702 |         Just zero =>
  703 |           let headtree # t := get arr zero t
  704 |             in assert_total $ headTree headtree t
  705 |     headTree (Leaf (_ ** arr))         t =
  706 |       case tryNatToFin 0 of
  707 |         Nothing   =>
  708 |           (assert_total $ idris_crash "Data.RRBVector.viewl: can't convert Nat to Fin") # t
  709 |         Just zero =>
  710 |           get arr zero t
  711 | 
  712 | ||| The vector without the last element and the last element, or 'Nothing' if the vector is empty. O(log n)
  713 | export
  714 | viewr :  RRBVector1 s a
  715 |       -> F1 s (Maybe (RRBVector1 s a, a))
  716 | viewr Empty                t = Nothing # t
  717 | viewr v@(Root size _ tree) t =
  718 |   let init # t := take (minus size 1) v t
  719 |       last # t := lastTree tree t
  720 |     in (Just (init, last)) # t
  721 |   where
  722 |     lastTree :  Tree1 s a
  723 |              -> F1 s a
  724 |     lastTree (Balanced (_ ** arr))     t =
  725 |       case tryNatToFin (minus size 1) of
  726 |         Nothing   =>
  727 |           (assert_total $ idris_crash "Data.RRBVector.viewr: can't convert Nat to Fin") # t
  728 |         Just last =>
  729 |           let lasttree # t := get arr last t
  730 |             in assert_total $ lastTree lasttree t
  731 |     lastTree (Unbalanced (_ ** arr) _) t =
  732 |       case tryNatToFin (minus size 1) of
  733 |         Nothing   =>
  734 |           (assert_total $ idris_crash "Data.RRBVector.viewr: can't convert Nat to Fin") # t
  735 |         Just last =>
  736 |           let lasttree # t := get arr last t
  737 |             in assert_total $ lastTree lasttree t
  738 |     lastTree (Leaf (_ ** arr))         t =
  739 |       case tryNatToFin (minus size 1) of
  740 |         Nothing   =>
  741 |           (assert_total $ idris_crash "Data.RRBVector.viewr: can't convert Nat to Fin") # t
  742 |         Just last =>
  743 |           get arr last t
  744 | 
  745 | --------------------------------------------------------------------------------
  746 | --          Transformation
  747 | --------------------------------------------------------------------------------
  748 | 
  749 | private
  750 | mapTree :  {n : Nat}
  751 |         -> (a -> a)
  752 |         -> (arr : MArray s n (Tree1 s a))
  753 |         -> F1 s (MArray s n (Tree1 s a))
  754 | mapTree f arr t =
  755 |   go 0 n arr t
  756 |   where
  757 |     go :  (m, x : Nat)
  758 |        -> (arr' : MArray s n (Tree1 s a))
  759 |        -> {auto v : Ix x n}
  760 |        -> F1 s (MArray s n (Tree1 s a))
  761 |     go m Z     arr' t =
  762 |       arr' # t
  763 |     go m (S j) arr' t =
  764 |       let j' # t := getIx arr j t
  765 |         in case j' of
  766 |              (Balanced (b ** arr''))         =>
  767 |                case tryNatToFin m of
  768 |                  Nothing =>
  769 |                    (assert_total $ idris_crash "Data.RRBVector.mapTree: can't convert Nat to Fin") # t
  770 |                  Just m' =>
  771 |                    let arr''' # t := assert_total $ mapTree f arr'' t
  772 |                        arr''''    := Balanced {bsize=b} (b ** arr''')
  773 |                        ()     # t := casswap arr' m' arr'''' t
  774 |                      in go (S m) j arr' t
  775 |              (Unbalanced (u ** arr'') sizes) =>
  776 |                case tryNatToFin m of
  777 |                  Nothing =>
  778 |                    (assert_total $ idris_crash "Data.RRBVector.mapTree.go: can't convert Nat to Fin") # t
  779 |                  Just m' =>
  780 |                    let arr''' # t := assert_total $ mapTree f arr'' t
  781 |                        arr''''    := Unbalanced (u ** arr''') sizes
  782 |                        ()     # t := casswap arr' m' arr'''' t
  783 |                      in go (S m) j arr' t
  784 |              (Leaf (l ** arr''))             =>
  785 |                case tryNatToFin m of
  786 |                  Nothing =>
  787 |                    (assert_total $ idris_crash "Data.RRBVector.mapTree.go: can't convert Nat to Fin") # t
  788 |                  Just m' =>
  789 |                    let ()     # t := mupdate f arr'' t
  790 |                        arr'''     := Leaf {lsize=l} (l ** arr'')
  791 |                        ()     # t := casswap arr' m' arr''' t
  792 |                      in go (S m) j arr' t
  793 | 
  794 | ||| Apply the function to every element. O(n)
  795 | export
  796 | map :  (a -> a)
  797 |     -> RRBVector1 s a
  798 |     -> F1 s (RRBVector1 s a)
  799 | map _ Empty                                        t =
  800 |   empty t
  801 | map f (Root size sh (Balanced (b ** arr)))         t =
  802 |   let arr' # t := mapTree f arr t
  803 |       arr''    := Balanced {bsize=b} (b ** arr')
  804 |     in (Root size sh arr'') # t
  805 | map f (Root size sh (Unbalanced (u ** arr) sizes)) t =
  806 |   let arr' # t := mapTree f arr t
  807 |       arr''    := Unbalanced (u ** arr') sizes
  808 |     in (Root size sh arr'') # t
  809 | map f (Root size sh (Leaf (l ** arr)))             t =
  810 |   let ()  # t := mupdate f arr t
  811 |       arr'    := Leaf {lsize=l} (l ** arr)
  812 |     in (Root size sh arr') # t
  813 | 
  814 | --------------------------------------------------------------------------------
  815 | --          Concatenation
  816 | --------------------------------------------------------------------------------
  817 | 
  818 | ||| Create a new tree with shift sh.
  819 | private
  820 | newBranch :  a
  821 |           -> Shift
  822 |           -> F1 s (Tree1 s a)
  823 | newBranch x 0  t =
  824 |   let x' # t := Data.RRBVector1.Unsized.Internal.singleton x t
  825 |     in (Leaf {lsize=1} (1 ** x')) # t
  826 | newBranch x sh t =
  827 |   let branch # t := assert_total $ newBranch x (down sh) t
  828 |       x'     # t := Data.RRBVector1.Unsized.Internal.singleton' branch t
  829 |     in (Balanced {bsize=1} (1 ** x')) # t
  830 | 
  831 | ||| Create a new tree with shift sh.
  832 | private
  833 | newBranch' :  Tree1 s a
  834 |            -> Shift
  835 |            -> F1 s (Tree1 s (Tree1 s a))
  836 | newBranch' tree 0  t =
  837 |   (assert_total $ idris_crash "Data.RRBVector1.newBranch': impossible zero shift with a (Tree1 s a).") # t
  838 | newBranch' tree sh t =
  839 |   let branch  # t := assert_total $ newBranch' tree (down sh) t
  840 |       tree'   # t := Data.RRBVector1.Unsized.Internal.singleton' branch t
  841 |     in (Balanced {bsize=1} (1 ** tree')) # t
  842 | 
  843 | ||| Add an element to the left end of the vector. O(log n)
  844 | export
  845 | (<|) :  a
  846 |      -> RRBVector1 s a
  847 |      -> F1 s (RRBVector1 s a)
  848 | (x <| Empty)               t =
  849 |   singleton x t
  850 | (x <| (Root size sh tree)) t =
  851 |   let sh' # t := insertshift t
  852 |     in case compare sh' sh of
  853 |          LT =>
  854 |            let constree # t := consTree sh tree t
  855 |              in (Root (plus size 1) sh constree) # t
  856 |          EQ =>
  857 |            let constree # t := consTree sh tree t
  858 |              in (Root (plus size 1) sh constree) # t
  859 |          GT =>
  860 |            let newtree # t := newBranch x sh t
  861 |                newlist     := [newtree, tree]
  862 |                new     # t := unsafeMArray1 (length newlist) t
  863 |                ()      # t := writeList new newlist t
  864 |                new'    # t := computeSizes sh' new t
  865 |              in (Root (plus size 1) sh' new') # t
  866 |   where
  867 |     -- compute the shift at which the new branch needs to be inserted (0 means there is space in the leaf)
  868 |     -- the size is computed for efficient calculation of the shift in a balanced subtree
  869 |     computeShift :  Nat
  870 |                  -> Nat
  871 |                  -> Nat
  872 |                  -> Tree1 s a
  873 |                  -> F1 s Nat
  874 |     computeShift sz sh min (Balanced _)                  t =
  875 |       -- sz - 1 is the index of the last element
  876 |       let comp     := mult (log2 (minus sz 1) `div` blockshift) blockshift -- the shift of the root when normalizing
  877 |           hishift  := case compare comp 0 of
  878 |                         LT =>
  879 |                           0
  880 |                         EQ =>
  881 |                           0
  882 |                         GT =>
  883 |                           comp
  884 |           hi       := (natToInteger $ minus sz 1) `shiftR` hishift -- the length of the root node when normalizing minus 1
  885 |           newshift := case compare hi (natToInteger blockmask) of
  886 |                         LT =>
  887 |                           hishift
  888 |                         EQ =>
  889 |                           plus hishift blockshift
  890 |                         GT =>
  891 |                           plus hishift blockshift
  892 |         in case compare newshift sh of
  893 |              LT =>
  894 |                newshift # t
  895 |              EQ =>
  896 |                newshift # t
  897 |              GT =>
  898 |                min # t
  899 |     computeShift _  sh min (Unbalanced (u ** arr) sizes) t =
  900 |       case tryNatToFin 0 of
  901 |         Nothing   =>
  902 |           (assert_total $ idris_crash "Data.RRBVector1.(<|).computeShift.Unbalanced: can't convert Nat to Fin") # t
  903 |         Just zero =>
  904 |           let newtree # t := get arr zero t
  905 |             in case tryNatToFin 0 of
  906 |                  Nothing    =>
  907 |                    (assert_total $ idris_crash "Data.RRBVector1.(<|).computeShift.Unbalanced: can't convert Nat to Fin") # t
  908 |                  Just zero' =>
  909 |                    let sz' := at sizes zero'
  910 |                      in case compare u blocksize of
  911 |                           LT =>
  912 |                             assert_total $ computeShift sz' (down sh) sh newtree t
  913 |                           EQ =>
  914 |                             assert_total $ computeShift sz' (down sh) min newtree t
  915 |                           GT =>
  916 |                             assert_total $ computeShift sz' (down sh) min newtree t
  917 |     computeShift _  _  min (Leaf (l ** _))               t =
  918 |       case compare l blocksize of
  919 |         LT =>
  920 |           0 # t
  921 |         EQ =>
  922 |           min # t
  923 |         GT =>
  924 |           min # t
  925 |     insertshift : F1 s Nat
  926 |     insertshift t =
  927 |       computeShift size sh (up sh) tree t
  928 |     consTree :  Nat
  929 |              -> Tree1 s a
  930 |              -> F1 s (Tree1 s a)
  931 |     consTree sh (Balanced (_ ** arr))     t =
  932 |       let sh' # t := insertshift t
  933 |         in case compare sh sh' of
  934 |              LT =>
  935 |                case tryNatToFin 0 of
  936 |                  Nothing   =>
  937 |                    (assert_total $ idris_crash "Data.RRBVector1.(<|).consTree.Balanced: can't convert Nat to Fin") # t
  938 |                  Just zero =>
  939 |                    let newtree   # t := get arr zero t
  940 |                        newtree'  # t := assert_total $ consTree (down sh) newtree t
  941 |                        ()        # t := casswap arr zero newtree' t
  942 |                        newtree'' # t := computeSizes sh arr t
  943 |                      in newtree'' # t
  944 |              EQ =>
  945 |                let newtree   # t := newBranch x (down sh) t
  946 |                    arr'      # t := marray1 1 newtree t
  947 |                    arr''     # t := mappend arr' arr t
  948 |                    newtree'' # t := computeSizes sh arr'' t
  949 |                  in newtree'' # t
  950 |              GT =>
  951 |                case tryNatToFin 0 of
  952 |                  Nothing   =>
  953 |                    (assert_total $ idris_crash "Data.RRBVector1.(<|).consTree.Balanced: can't convert Nat to Fin") # t
  954 |                  Just zero =>
  955 |                    let newtree   # t := get arr zero t
  956 |                        newtree'  # t := assert_total $ consTree (down sh) newtree t
  957 |                        ()        # t := casswap arr zero newtree' t
  958 |                        newtree'' # t := computeSizes sh arr t
  959 |                      in newtree'' # t
  960 |     consTree sh (Unbalanced (_ ** arr) _) t =
  961 |       let sh' # t := insertshift t
  962 |         in case compare sh sh' of
  963 |              LT =>
  964 |                case tryNatToFin 0 of
  965 |                  Nothing   =>
  966 |                    (assert_total $ idris_crash "Data.RRBVector1.(<|).consTree.Unbalanced: can't convert Nat to Fin") # t
  967 |                  Just zero =>
  968 |                    let newtree   # t := get arr zero t
  969 |                        newtree'  # t := assert_total $ consTree (down sh) newtree t
  970 |                        ()        # t := casswap arr zero newtree' t
  971 |                        newtree'' # t := computeSizes sh arr t
  972 |                      in newtree'' # t
  973 |              EQ =>
  974 |                let newtree   # t := newBranch x (down sh) t
  975 |                    arr'      # t := marray1 1 newtree t
  976 |                    arr''     # t := mappend arr' arr t
  977 |                    newtree'' # t := computeSizes sh arr'' t
  978 |                  in newtree'' # t
  979 |              GT =>
  980 |                case tryNatToFin 0 of
  981 |                  Nothing   =>
  982 |                    (assert_total $ idris_crash "Data.RRBVector1.(<|).consTree.Unbalanced: can't convert Nat to Fin") # t
  983 |                  Just zero =>
  984 |                    let newtree   # t := get arr zero t
  985 |                        newtree'  # t := assert_total $ consTree (down sh) newtree t
  986 |                        ()        # t := casswap arr zero newtree' t
  987 |                        newtree'' # t := computeSizes sh arr t
  988 |                      in newtree'' # t
  989 |     consTree _  (Leaf (l ** arr))         t =
  990 |       let arr'  # t := marray1 1 x t
  991 |           arr'' # t := mappend arr' arr t
  992 |         in (Leaf {lsize=(S l)} ((S l) ** arr'')) # t
  993 | 
  994 | ||| Add an element to the right end of the vector. O(log n)
  995 | export
  996 | (|>) :  RRBVector1 s a
  997 |      -> a
  998 |      -> F1 s (RRBVector1 s a)
  999 | (Empty |> x)             t =
 1000 |   singleton x t
 1001 | (Root size sh tree |> x) t =
 1002 |   let sh' # t := insertshift t
 1003 |     in case compare sh' sh of
 1004 |          LT =>
 1005 |            let snoctree # t := snocTree sh tree t
 1006 |              in (Root (plus size 1) sh snoctree) # t
 1007 |          EQ =>
 1008 |            let snoctree # t := snocTree sh tree t
 1009 |              in (Root (plus size 1) sh snoctree) # t
 1010 |          GT =>
 1011 |            let newtree # t := newBranch x sh t
 1012 |                newlist     := [tree, newtree]
 1013 |                new     # t := unsafeMArray1 (length newlist) t
 1014 |                ()      # t := writeList new newlist t
 1015 |                new'    # t := computeSizes sh' new t
 1016 |              in (Root (plus size 1) sh' new') # t
 1017 |   where
 1018 |     -- compute the shift at which the new branch needs to be inserted (0 means there is space in the leaf)
 1019 |     -- the size is computed for efficient calculation of the shift in a balanced subtree
 1020 |     computeShift :  Nat
 1021 |                  -> Nat
 1022 |                  -> Nat
 1023 |                  -> Tree1 s a
 1024 |                  -> F1 s Nat
 1025 |     computeShift sz sh min (Balanced _)                  t =
 1026 |       -- sz - 1 is the index of the last element
 1027 |       let newshift := mult (countTrailingZeros sz `div` blockshift) blockshift
 1028 |         in case compare newshift sh of
 1029 |              LT =>
 1030 |                newshift # t
 1031 |              EQ =>
 1032 |                newshift # t
 1033 |              GT =>
 1034 |                min # t
 1035 |     computeShift _  sh min (Unbalanced (u ** arr) sizes) t =
 1036 |       case tryNatToFin $ minus u 1 of
 1037 |         Nothing       =>
 1038 |           (assert_total $ idris_crash "Data.RRBVector1.(|>).computeShift.Unbalanced: can't convert Nat to Fin") # t
 1039 |         Just lastidx' =>
 1040 |           let newtree # t := get arr lastidx' t
 1041 |             in case tryNatToFin $ minus u 1 of
 1042 |                  Nothing       =>
 1043 |                    (assert_total $ idris_crash "Data.RRBVector1.(|>).computeShift.Unbalanced: can't convert Nat to Fin") # t
 1044 |                  Just lastidx' =>
 1045 |                    let sizes' := at sizes lastidx'
 1046 |                      in case tryNatToFin $ minus (minus u 1) 1 of
 1047 |                           Nothing    =>
 1048 |                             (assert_total $ idris_crash "Data.RRBVector1.(|>).computeShift.Unbalanced: can't convert Nat to Fin") # t
 1049 |                           Just lastidx'' =>
 1050 |                             let sizes''     := at sizes lastidx''
 1051 |                                 sz'         := minus sizes' sizes''
 1052 |                               in case compare u blocksize of
 1053 |                                    LT =>
 1054 |                                      assert_total $ computeShift sz' (down sh) sh newtree t
 1055 |                                    EQ =>
 1056 |                                      assert_total $ computeShift sz' (down sh) min newtree t
 1057 |                                    GT =>
 1058 |                                      assert_total $ computeShift sz' (down sh) min newtree t
 1059 |     computeShift _  _  min (Leaf (l ** arr))             t =
 1060 |       case compare l blocksize of
 1061 |         LT =>
 1062 |           0 # t
 1063 |         EQ =>
 1064 |           min # t
 1065 |         GT =>
 1066 |           min # t
 1067 |     insertshift : F1 s Nat
 1068 |     insertshift t =
 1069 |       computeShift size sh (up sh) tree t
 1070 |     snocTree :  Nat
 1071 |              -> Tree1 s a
 1072 |              -> F1 s (Tree1 s a)
 1073 |     snocTree sh (Balanced (b ** arr))     t =
 1074 |       let sh' # t := insertshift t
 1075 |         in case compare sh sh' of
 1076 |              LT =>
 1077 |                case tryNatToFin $ minus b 1 of
 1078 |                  Nothing      =>
 1079 |                    (assert_total $ idris_crash "Data.RRBVector1.(|>).snocTree.Balanced: can't convert Nat to Fin") # t
 1080 |                  Just lastidx =>
 1081 |                    let newtree   # t := get arr lastidx t
 1082 |                        newtree'  # t := assert_total $ snocTree (down sh) newtree t
 1083 |                        ()        # t := casswap arr lastidx newtree' t
 1084 |                        in (Balanced {bsize=b} (b ** arr)) # t
 1085 |              EQ => -- the current subtree is fully balanced
 1086 |                let newtree   # t := newBranch x (down sh) t
 1087 |                    arr'      # t := marray1 1 newtree t
 1088 |                    arr''     # t := mappend arr' arr t
 1089 |                  in (Balanced {bsize=(S b)} ((S b) ** arr'')) # t
 1090 |              GT =>
 1091 |                case tryNatToFin $ minus b 1 of
 1092 |                  Nothing      =>
 1093 |                    (assert_total $ idris_crash "Data.RRBVector1.(|>).snocTree.Balanced: can't convert Nat to Fin") # t
 1094 |                  Just lastidx =>
 1095 |                    let newtree   # t := get arr lastidx t
 1096 |                        newtree'  # t := assert_total $ snocTree (down sh) newtree t
 1097 |                        ()        # t := casswap arr lastidx newtree' t
 1098 |                      in (Balanced {bsize=b} (b ** arr)) # t
 1099 |     snocTree sh (Unbalanced (u ** arr) sizes) t =
 1100 |       let sh' # t := insertshift t
 1101 |         in case compare sh sh' of
 1102 |              LT =>
 1103 |                case tryNatToFin $ minus u 1 of
 1104 |                  Nothing       =>
 1105 |                    (assert_total $ idris_crash "Data.RRBVector1.(|>).snocTree.Unbalanced: can't convert Nat to Fin") # t
 1106 |                  Just lastidxa =>
 1107 |                    let newtree  # t := get arr lastidxa t
 1108 |                        newtree' # t := assert_total $ snocTree (down sh) newtree t
 1109 |                        ()       # t := casswap arr lastidxa newtree' t
 1110 |                      in case tryNatToFin $ minus u 1 of
 1111 |                           Nothing       =>
 1112 |                             (assert_total $ idris_crash "Data.RRBVector1.(|>).snocTree.Unbalanced: can't convert Nat to Fin") # t
 1113 |                           Just lastidxs =>
 1114 |                             let lastsize    := plus (at sizes lastidxs) 1
 1115 |                                 sizes'  # t := thaw sizes t
 1116 |                                 ()      # t := casswap sizes' lastidxs lastsize t
 1117 |                                 sizes'' # t := freeze sizes' t
 1118 |                               in (Unbalanced (u ** arr)
 1119 |                                              sizes''
 1120 |                                  ) # t
 1121 |              EQ =>
 1122 |                 case tryNatToFin $ minus u 1 of
 1123 |                   Nothing      =>
 1124 |                     (assert_total $ idris_crash "Data.RRBVector1.(|>).snocTree.Unbalanced: can't convert Nat to Fin") # t
 1125 |                   Just lastidx =>
 1126 |                     let lastsize      := plus (at sizes lastidx) 1
 1127 |                         newtree   # t := newBranch x (down sh) t
 1128 |                         arr'      # t := marray1 1 newtree t
 1129 |                         arr''     # t := mappend arr arr' t
 1130 |                       in (Unbalanced ((plus u 1) ** arr'')
 1131 |                                      (append sizes (fill 1 lastsize))
 1132 |                          ) # t
 1133 |              GT =>
 1134 |                case tryNatToFin $ minus u 1 of
 1135 |                  Nothing       =>
 1136 |                    (assert_total $ idris_crash "Data.RRBVector1.(|>).snocTree.Unbalanced: can't convert Nat to Fin") # t
 1137 |                  Just lastidxa =>
 1138 |                    let newtree  # t := get arr lastidxa t
 1139 |                        newtree' # t := assert_total $ snocTree (down sh) newtree t
 1140 |                        ()       # t := casswap arr lastidxa newtree' t
 1141 |                      in case tryNatToFin $ minus u 1 of
 1142 |                           Nothing       =>
 1143 |                             (assert_total $ idris_crash "Data.RRBVector1.(|>).snocTree.Unbalanced: can't convert Nat to Fin") # t
 1144 |                           Just lastidxs =>
 1145 |                             let lastsize    := plus (at sizes lastidxs) 1
 1146 |                                 sizes'  # t := thaw sizes t
 1147 |                                 ()      # t := casswap sizes' lastidxs lastsize t
 1148 |                                 sizes'' # t := freeze sizes' t
 1149 |                               in (Unbalanced (u ** arr)
 1150 |                                              sizes''
 1151 |                                  ) # t
 1152 |     snocTree _  (Leaf (l ** arr))         t =
 1153 |       let arr'  # t := marray1 1 x t
 1154 |           arr'' # t := mappend arr arr' t
 1155 |         in (Leaf {lsize=(plus l 1)} ((plus l 1) ** arr'')) # t
 1156 | 
 1157 | ||| Concatenates two vectors. O(log(max(n1,n2)))
 1158 | export
 1159 | (><) :  RRBVector1 s a
 1160 |      -> RRBVector1 s a
 1161 |      -> F1 s (RRBVector1 s a)
 1162 | (Empty                >< v)                    t =
 1163 |   v # t
 1164 | (v                    >< Empty)                t =
 1165 |   v # t
 1166 | (Root size1 sh1 tree1 >< Root size2 sh2 tree2) t =
 1167 |   let upmaxshift := case compare sh1 sh2 of
 1168 |                       LT =>
 1169 |                         up sh2
 1170 |                       EQ =>
 1171 |                         up sh1
 1172 |                       GT =>
 1173 |                         up sh1
 1174 |       (_ ** arr) # t := mergeTrees tree1 sh1 tree2 sh2 t
 1175 |       arr'       # t := computeSizes upmaxshift arr t
 1176 |       arr''          := Root (plus size1 size2) upmaxshift arr'
 1177 |     in normalize arr'' t
 1178 |   where
 1179 |     viewlArr :  {n : Nat}
 1180 |              -> MArray s n (Tree1 s a)
 1181 |              -> F1 s (Tree1 s a, MArray s (n `minus` 1) (Tree1 s a))
 1182 |     viewlArr arr t =
 1183 |       case tryNatToFin 0 of
 1184 |         Nothing   =>
 1185 |           (assert_total $ idris_crash "Data.RRBVector1.(><).viewlArr: can't convert Nat to Fin") # t
 1186 |         Just zero =>
 1187 |           let arr'  # t := get arr zero t
 1188 |               arr'' # t := mdrop 1 arr t
 1189 |             in (arr', arr'') # t
 1190 |     viewrArr :  {n : Nat}
 1191 |              -> MArray s n (Tree1 s a)
 1192 |              -> F1 s (MArray s (n `minus` 1) (Tree1 s a), Tree1 s a)
 1193 |     viewrArr arr with ((minus n 1) <= n) proof eq
 1194 |       _ | True  = \t =>
 1195 |         case tryNatToFin $ minus n 1 of
 1196 |           Nothing   =>
 1197 |             (assert_total $ idris_crash "Data.RRBVector.(><).viewrArr: can't convert Nat to Fin") # t
 1198 |           Just last =>
 1199 |             let arr'  # t := get arr last t
 1200 |                 arr'' # t := mtake arr (minus n 1) @{lteOpReflectsLTE _ _ eq} t
 1201 |               in (arr'', arr') # t
 1202 |       _ | False = \t =>
 1203 |         (assert_total $ idris_crash "Data.RRBVector1.(><).viewrArr: index out of bounds") # t
 1204 |     takeArr :  {n : Nat}
 1205 |             -> {blocksize : Nat}
 1206 |             -> MArray s n a
 1207 |             -> F1 s (MArray s blocksize a)
 1208 |     takeArr arr with (blocksize <= n) proof eq
 1209 |       _ | True  = \t =>
 1210 |         mtake arr blocksize @{lteOpReflectsLTE _ _ eq} t
 1211 |       _ | False = \t =>
 1212 |         (assert_total $ idris_crash "Data.RRBVector1.(><).takeArr: index out of bounds") # t
 1213 |     mergeRebalanceInternalGo' :  (x : Nat)
 1214 |                               -> (sh : Shift)
 1215 |                               -> MArray s n (Tree1 s a)
 1216 |                               -> (o ** MArray s o (Tree1 s a))
 1217 |                               -> (p ** MArray s p (Tree1 s a))
 1218 |                               -> (q ** MArray s q (Tree1 s a))
 1219 |                               -> {auto v : Ix x n}
 1220 |                               -> F1 s ((o' ** MArray s o' (Tree1 s a)), (p' ** MArray s p' (Tree1 s a)), (q' ** MArray s q' (Tree1 s a)))
 1221 |     mergeRebalanceInternalGo' Z      _  _    (o ** newnode'') (p ** newsubtree'') (q ** newroot'') t =
 1222 |       ((o ** newnode''), (p ** newsubtree''), (q ** newroot'')) # t
 1223 |     mergeRebalanceInternalGo' (S j') sh arr' (o ** newnode'') (p ** newsubtree'') (q ** newroot'') t =
 1224 |       case o == blocksize of
 1225 |         True  =>
 1226 |           case p == blocksize of
 1227 |             True  =>
 1228 |               let newnode'''       # t := computeSizes (down sh) newnode'' t
 1229 |                   newnode''''      # t := marray1 1 newnode''' t
 1230 |                   newsubtree'''    # t := mappend newsubtree'' newnode'''' t
 1231 |                   newnode'''''     # t := unsafeMArray1 0 t
 1232 |                   newsubtree''''   # t := computeSizes sh newsubtree''' t
 1233 |                   newsubtree'''''  # t := marray1 1 newsubtree'''' t
 1234 |                   newroot'''       # t := mappend newroot'' newsubtree''''' t
 1235 |                   newsubtree'''''' # t := unsafeMArray1 0 t
 1236 |                   j''              # t := getIx arr' j' t
 1237 |                   newnode''''''    # t := marray1 1 j'' t
 1238 |                   newnode'''''''   # t := mappend newnode''''' newnode'''''' t
 1239 |                 in mergeRebalanceInternalGo' j' sh arr' (1 ** newnode''''''') (0  ** newsubtree'''''') ((plus q 1) ** newroot''') t
 1240 |             False =>
 1241 |               let newnode'''       # t := computeSizes (down sh) newnode'' t
 1242 |                   newnode''''      # t := marray1 1 newnode''' t
 1243 |                   newsubtree'''    # t := mappend newsubtree'' newnode'''' t
 1244 |                   newnode'''''     # t := unsafeMArray1 0 t
 1245 |                   j''              # t := getIx arr' j' t
 1246 |                   newnode''''''    # t := marray1 1 j'' t
 1247 |                   newnode'''''''   # t := mappend newnode''''' newnode'''''' t
 1248 |                 in mergeRebalanceInternalGo' j' sh arr' (1 ** newnode''''''') ((plus p 1) ** newsubtree''') (q ** newroot'') t
 1249 |         False =>
 1250 |           let j''           # t := getIx arr' j' t
 1251 |               newnode'''    # t := marray1 1 j'' t
 1252 |               newnode''''   # t := mappend newnode'' newnode''' t
 1253 |             in mergeRebalanceInternalGo' j' sh arr' ((plus o 1) ** newnode'''') (p ** newsubtree'') (q ** newroot'') t
 1254 |     mergeRebalanceInternalGo :  (x : Nat)
 1255 |                              -> (sh : Shift)
 1256 |                              -> MArray s n (Tree1 s a)
 1257 |                              -> (o ** MArray s o (Tree1 s a))
 1258 |                              -> (p ** MArray s p (Tree1 s a))
 1259 |                              -> (q ** MArray s q (Tree1 s a))
 1260 |                              -> {auto v : Ix x n}
 1261 |                              -> F1 s (r ** MArray s r (Tree1 s a))
 1262 |     mergeRebalanceInternalGo Z     sh arr (_ ** newnode') (_ ** newsubtree') (q ** newroot') t =
 1263 |       let newnode''      # t := computeSizes (down sh) newnode' t
 1264 |           newnode'''     # t := marray1 1 newnode'' t
 1265 |           newsubtree''   # t := mappend newsubtree' newnode''' t
 1266 |           newsubtree'''  # t := computeSizes sh newsubtree'' t
 1267 |           newsubtree'''' # t := marray1 1 newsubtree''' t
 1268 |           newroot''      # t := mappend newroot' newsubtree'''' t
 1269 |         in ((plus q 1) ** newroot'') # t
 1270 |     mergeRebalanceInternalGo (S j) sh arr (o ** newnode') (p ** newsubtree') (q ** newroot') t =
 1271 |       let j'  # t := getIx arr j t
 1272 |           j''     := treeToArray j'
 1273 |         in case j'' of
 1274 |              Left  (b ** arr') =>
 1275 |                let ((o' ** newnode''), (p' ** newsubtree''), (q' ** newroot'')) # t := mergeRebalanceInternalGo' b sh arr' (o ** newnode') (p ** newsubtree') (q ** newroot') t
 1276 |                  in mergeRebalanceInternalGo j sh arr (o' ** newnode'') (p' ** newsubtree'') (q' ** newroot'') t
 1277 |              Right (u ** arr') =>
 1278 |                let ((o' ** newnode''), (p' ** newsubtree''), (q' ** newroot'')) # t := mergeRebalanceInternalGo' u sh arr' (o ** newnode') (p ** newsubtree') (q ** newroot') t
 1279 |                  in mergeRebalanceInternalGo j sh arr (o' ** newnode'') (p' ** newsubtree'') (q' ** newroot'') t
 1280 |     mergeRebalanceInternal' :  {n : Nat}
 1281 |                             -> Shift
 1282 |                             -> MArray s n (Tree1 s a)
 1283 |                             -> F1 s (r ** MArray s r (Tree1 s a))
 1284 |     mergeRebalanceInternal' sh lcr t =
 1285 |       let newnode        # t := unsafeMArray1 0 t
 1286 |           newsubtree     # t := unsafeMArray1 0 t
 1287 |           newroot        # t := unsafeMArray1 0 t
 1288 |         in mergeRebalanceInternalGo n sh lcr (0 ** newnode) (0 ** newsubtree) (0 ** newroot) t
 1289 |     mergeRebalance' :  {n : Nat}
 1290 |                     -> {m : Nat}
 1291 |                     -> {o : Nat}
 1292 |                     -> Shift
 1293 |                     -> MArray s n (Tree1 s a)
 1294 |                     -> MArray s m (Tree1 s a)
 1295 |                     -> MArray s o (Tree1 s a)
 1296 |                     -> F1 s (r ** MArray s r (Tree1 s a))
 1297 |     mergeRebalance' sh left center right t =
 1298 |       let centerright     # t := mappend center right t
 1299 |           leftcenterright # t := mappend left centerright t
 1300 |         in mergeRebalanceInternal' sh
 1301 |                                    leftcenterright
 1302 |                                    t
 1303 |     mergeRebalanceInternalGo''' :  (x : Nat)
 1304 |                                 -> (sh : Shift)
 1305 |                                 -> MArray s n a
 1306 |                                 -> (o ** MArray s o a)
 1307 |                                 -> (p ** MArray s p (Tree1 s a))
 1308 |                                 -> (q ** MArray s q (Tree1 s a))
 1309 |                                 -> {auto v : Ix x n}
 1310 |                                 -> F1 s ((o' ** MArray s o' a), (p' ** MArray s p' (Tree1 s a)), (q' ** MArray s q' (Tree1 s a)))
 1311 |     mergeRebalanceInternalGo''' Z      _  _    (o ** newnode'') (p ** newsubtree'') (q ** newroot'') t =
 1312 |       ((o ** newnode''), (p ** newsubtree''), (q ** newroot'')) # t
 1313 |     mergeRebalanceInternalGo''' (S j') sh arr' (o ** newnode'') (p ** newsubtree'') (q ** newroot'') t =
 1314 |       case o == blocksize of
 1315 |         True  =>
 1316 |           case p == blocksize of
 1317 |             True  =>
 1318 |               let newnode'''           := Leaf {lsize=0} (o ** newnode'')
 1319 |                   newnode''''      # t := marray1 1 newnode''' t
 1320 |                   newsubtree'''    # t := mappend newsubtree'' newnode'''' t
 1321 |                   newnode'''''     # t := unsafeMArray1 0 t
 1322 |                   newsubtree''''   # t := computeSizes sh newsubtree''' t
 1323 |                   newsubtree'''''  # t := marray1 1 newsubtree'''' t
 1324 |                   newroot'''       # t := mappend newroot'' newsubtree''''' t
 1325 |                   newsubtree'''''' # t := unsafeMArray1 0 t
 1326 |                   j''              # t := getIx arr' j' t
 1327 |                   newnode''''''    # t := marray1 1 j'' t
 1328 |                   newnode'''''''   # t := mappend newnode''''' newnode'''''' t
 1329 |                 in mergeRebalanceInternalGo''' j' sh arr' (1 ** newnode''''''') (0  ** newsubtree'''''') ((plus q 1) ** newroot''') t
 1330 |             False =>
 1331 |               let newnode'''           := Leaf {lsize=0} (o ** newnode'')
 1332 |                   newnode''''      # t := marray1 1 newnode''' t
 1333 |                   newsubtree'''    # t := mappend newsubtree'' newnode'''' t
 1334 |                   newnode'''''     # t := unsafeMArray1 0 t
 1335 |                   j''              # t := getIx arr' j' t
 1336 |                   newnode''''''    # t := marray1 1 j'' t
 1337 |                   newnode'''''''   # t := mappend newnode''''' newnode'''''' t
 1338 |                 in mergeRebalanceInternalGo''' j' sh arr' (1 ** newnode''''''') ((plus p 1) ** newsubtree''') (q ** newroot'') t
 1339 |         False =>
 1340 |           let j''           # t := getIx arr' j' t
 1341 |               newnode'''    # t := marray1 1 j'' t
 1342 |               newnode''''   # t := mappend newnode'' newnode''' t
 1343 |             in mergeRebalanceInternalGo''' j' sh arr' ((plus o 1) ** newnode'''') (p ** newsubtree'') (q ** newroot'') t
 1344 |     mergeRebalanceInternalGo'' :  (x : Nat)
 1345 |                                -> (sh : Shift)
 1346 |                                -> MArray s n (Tree1 s a)
 1347 |                                -> (o ** MArray s o a)
 1348 |                                -> (p ** MArray s p (Tree1 s a))
 1349 |                                -> (q ** MArray s q (Tree1 s a))
 1350 |                                -> {auto v : Ix x n}
 1351 |                                -> F1 s (r ** MArray s r (Tree1 s a))
 1352 |     mergeRebalanceInternalGo'' Z     sh arr (o ** newnode') (_ ** newsubtree') (q ** newroot') t =
 1353 |       let newnode''          := Leaf {lsize=o} (o ** newnode')
 1354 |           newnode'''     # t := marray1 1 newnode'' t
 1355 |           newsubtree''   # t := mappend newsubtree' newnode''' t
 1356 |           newsubtree'''  # t := computeSizes sh newsubtree'' t
 1357 |           newsubtree'''' # t := marray1 1 newsubtree''' t
 1358 |           newroot''      # t := mappend newroot' newsubtree'''' t
 1359 |         in ((plus q 1) ** newroot'') # t
 1360 |     mergeRebalanceInternalGo'' (S j) sh arr (o ** newnode') (p ** newsubtree') (q ** newroot') t =
 1361 |       let j'                                                           # t := getIx arr j t
 1362 |           (l ** arr')                                                      := treeToArray' j'
 1363 |           ((o' ** newnode''), (p' ** newsubtree''), (q' ** newroot'')) # t := mergeRebalanceInternalGo''' l sh arr' (o ** newnode') (p ** newsubtree') (q ** newroot') t
 1364 |         in mergeRebalanceInternalGo'' j sh arr (o' ** newnode'') (p' ** newsubtree'') (q' ** newroot'') t
 1365 |     mergeRebalanceInternal'' :  {n : Nat}
 1366 |                              -> Shift
 1367 |                              -> MArray s n (Tree1 s a)
 1368 |                              -> F1 s (r ** MArray s r (Tree1 s a))
 1369 |     mergeRebalanceInternal'' sh lcr t =
 1370 |       let newnode        # t := unsafeMArray1 0 t
 1371 |           newsubtree     # t := unsafeMArray1 0 t
 1372 |           newroot        # t := unsafeMArray1 0 t
 1373 |         in mergeRebalanceInternalGo'' n sh lcr (0 ** newnode) (0 ** newsubtree) (0 ** newroot) t
 1374 |     mergeRebalance'' :  {n : Nat}
 1375 |                      -> {m : Nat}
 1376 |                      -> {o : Nat}
 1377 |                      -> Shift
 1378 |                      -> MArray s n (Tree1 s a)
 1379 |                      -> MArray s m (Tree1 s a)
 1380 |                      -> MArray s o (Tree1 s a)
 1381 |                      -> F1 s (r ** MArray s r (Tree1 s a))
 1382 |     mergeRebalance'' sh left center right t =
 1383 |       let centerright     # t := mappend center right t
 1384 |           leftcenterright # t := mappend left centerright t
 1385 |         in mergeRebalanceInternal'' sh
 1386 |                                     leftcenterright
 1387 |                                     t
 1388 |     mergeRebalance :  {n : Nat}
 1389 |                    -> {m : Nat}
 1390 |                    -> {o : Nat}
 1391 |                    -> Shift
 1392 |                    -> MArray s n (Tree1 s a)
 1393 |                    -> MArray s m (Tree1 s a)
 1394 |                    -> MArray s o (Tree1 s a)
 1395 |                    -> F1 s (r ** MArray s r (Tree1 s a))
 1396 |     mergeRebalance sh left center right t =
 1397 |       case compare sh blockshift of
 1398 |         LT =>
 1399 |           mergeRebalance' sh left center right t
 1400 |         EQ =>
 1401 |           mergeRebalance'' sh left center right t
 1402 |         GT =>
 1403 |           mergeRebalance' sh left center right t
 1404 |     mergeTrees :  Tree1 s a
 1405 |                -> Nat
 1406 |                -> Tree1 s a
 1407 |                -> Nat
 1408 |                -> F1 s (r ** MArray s r (Tree1 s a))
 1409 |     mergeTrees tree1@(Leaf (l1 ** arr1)) _   tree2@(Leaf (l2 ** arr2)) _   t =
 1410 |       case compare l1 blocksize of
 1411 |         LT =>
 1412 |           let arr' # t := mappend arr1 arr2 t
 1413 |             in case compare (plus l1 l2) blocksize of
 1414 |                  LT =>
 1415 |                    let newtree   := Leaf {lsize=(plus l1 l2)} ((plus l1 l2) ** arr')
 1416 |                        arr'' # t := singleton' newtree t
 1417 |                      in (1 ** arr'') # t
 1418 |                  EQ =>
 1419 |                    let newtree   := Leaf {lsize=(plus l1 l2)} ((plus l1 l2) ** arr')
 1420 |                        arr'' # t := singleton' newtree t
 1421 |                      in (1 ** arr'') # t
 1422 |                  GT =>
 1423 |                    let left  # t := takeArr arr' t
 1424 |                        right # t := mdrop blocksize arr' t
 1425 |                        lefttree  := Leaf {lsize=blocksize} (blocksize ** left)
 1426 |                        righttree := Leaf {lsize=(minus (plus l1 l2) blocksize)} ((minus (plus l1 l2) blocksize) ** right)
 1427 |                        newlist   := [lefttree, righttree]
 1428 |                        arr'' # t := unsafeMArray1 (length newlist) t
 1429 |                        ()    # t := writeList arr'' newlist t
 1430 |                      in ((length newlist) ** arr'') # t
 1431 |         EQ =>
 1432 |           let newlist   := [tree1, tree2]
 1433 |               arr'' # t := unsafeMArray1 (length newlist) t
 1434 |               ()    # t := writeList arr'' newlist t
 1435 |             in ((length newlist) ** arr'') # t
 1436 |         GT =>
 1437 |           let arr' # t := mappend arr1 arr2 t
 1438 |             in case compare (plus l1 l2) blocksize of
 1439 |                  LT =>
 1440 |                    let newtree   := Leaf {lsize=(plus l1 l2)} ((plus l1 l2) ** arr')
 1441 |                        arr'' # t := singleton' newtree t
 1442 |                      in (1 ** arr'') # t
 1443 |                  EQ =>
 1444 |                    let newtree   := Leaf {lsize=(plus l1 l2)} ((plus l1 l2) ** arr')
 1445 |                        arr'' # t := singleton' newtree t
 1446 |                      in (1 ** arr'') # t
 1447 |                  GT =>
 1448 |                    let left  # t := takeArr arr' t
 1449 |                        right # t := mdrop blocksize arr' t
 1450 |                        lefttree  := Leaf {lsize=blocksize} (blocksize ** left)
 1451 |                        righttree := Leaf {lsize=(minus (plus l1 l2) blocksize)} ((minus (plus l1 l2) blocksize) ** right)
 1452 |                        newlist   := [lefttree, righttree]
 1453 |                        arr'' # t := unsafeMArray1 (length newlist) t
 1454 |                        ()    # t := writeList arr'' newlist t
 1455 |                      in ((length newlist) ** arr'') # t
 1456 |     mergeTrees tree1                     sh1 tree2                     sh2 t =
 1457 |       case compare sh1 sh2 of
 1458 |         LT =>
 1459 |           let right := treeToArray tree2
 1460 |             in case right of
 1461 |                  Left  (_ ** arr) =>
 1462 |                    let (righthead, righttail) # t := viewlArr arr t
 1463 |                        (_ ** merged)          # t := assert_total $ mergeTrees tree1 sh1 righthead (down sh2) t
 1464 |                        emptyarr               # t := unsafeMArray1 0 t
 1465 |                      in mergeRebalance sh2 emptyarr merged righttail t
 1466 |                  Right (_ ** arr) =>
 1467 |                    let (righthead, righttail) # t := viewlArr arr t
 1468 |                        (_ ** merged)          # t := assert_total $ mergeTrees tree1 sh1 righthead (down sh2) t
 1469 |                        emptyarr               # t := unsafeMArray1 0 t
 1470 |                      in mergeRebalance sh2 emptyarr merged righttail t
 1471 |         EQ =>
 1472 |           let left := treeToArray tree1
 1473 |             in case left of
 1474 |                  Left  (_ ** arr) =>
 1475 |                    let right := treeToArray tree2
 1476 |                      in case right of
 1477 |                           Left  (_ ** arr') =>
 1478 |                             let (leftinit, leftlast)   # t := viewrArr arr t
 1479 |                                 (righthead, righttail) # t := viewlArr arr' t
 1480 |                                 (_ ** merged)          # t := assert_total $ mergeTrees leftlast (down sh1) righthead (down sh2) t
 1481 |                               in mergeRebalance sh1 leftinit merged righttail t
 1482 |                           Right (_ ** arr') =>
 1483 |                             let (leftinit, leftlast)   # t := viewrArr arr t
 1484 |                                 (righthead, righttail) # t := viewlArr arr' t
 1485 |                                 (_ ** merged)          # t := assert_total $ mergeTrees leftlast (down sh1) righthead (down sh2) t
 1486 |                               in mergeRebalance sh1 leftinit merged righttail t
 1487 |                  Right (_ ** arr) =>
 1488 |                    let right := treeToArray tree2
 1489 |                      in case right of
 1490 |                           Left  (_ ** arr') =>
 1491 |                             let (leftinit, leftlast)   # t := viewrArr arr t
 1492 |                                 (righthead, righttail) # t := viewlArr arr' t
 1493 |                                 (_ ** merged)          # t := assert_total $ mergeTrees leftlast (down sh1) righthead (down sh2) t
 1494 |                               in mergeRebalance sh1 leftinit merged righttail t
 1495 |                           Right (_ ** arr') =>
 1496 |                             let (leftinit, leftlast)   # t := viewrArr arr t
 1497 |                                 (righthead, righttail) # t := viewlArr arr' t
 1498 |                                 (_ ** merged)          # t := assert_total $ mergeTrees leftlast (down sh1) righthead (down sh2) t
 1499 |                               in mergeRebalance sh1 leftinit merged righttail t
 1500 |         GT =>
 1501 |           let left := treeToArray tree1
 1502 |             in case left of
 1503 |                  Left  (_ ** arr) =>
 1504 |                    let (leftinit, leftlast) # t := viewrArr arr t
 1505 |                        (_ ** merged)        # t := assert_total $ mergeTrees leftlast (down sh1) tree2 sh2 t
 1506 |                        emptyarr             # t := unsafeMArray1 0 t
 1507 |                      in mergeRebalance sh1 leftinit merged emptyarr t
 1508 |                  Right (_ ** arr) =>
 1509 |                    let (leftinit, leftlast) # t := viewrArr arr t
 1510 |                        (_ ** merged)        # t := assert_total $ mergeTrees leftlast (down sh1) tree2 sh2 t
 1511 |                        emptyarr             # t := unsafeMArray1 0 t
 1512 |                      in mergeRebalance sh1 leftinit merged emptyarr t
 1513 | 
 1514 | ||| Insert an element at the given index, shifting the rest of the vector over.
 1515 | ||| If the index is negative, add the element to the left end of the vector.
 1516 | ||| 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)
 1517 | export
 1518 | insertAt :  Nat
 1519 |          -> a
 1520 |          -> RRBVector1 s a
 1521 |          -> F1 s (RRBVector1 s a)
 1522 | insertAt i x v t =
 1523 |   let (left, right) # t := Data.RRBVector1.Unsized.splitAt i v t
 1524 |       left'         # t := ((|>) left x) t
 1525 |     in (><) left' right t
 1526 | 
 1527 | ||| Delete the element at the given index.
 1528 | ||| If the index is out of range, return the original vector. O(log n)
 1529 | export
 1530 | deleteAt :  Nat
 1531 |          -> RRBVector1 s a
 1532 |          -> F1 s (RRBVector1 s a)
 1533 | deleteAt i v t =
 1534 |   let (left, right) # t := Data.RRBVector1.Unsized.splitAt (plus i 1) v t
 1535 |       left'         # t := take i left t
 1536 |     in (><) left' right t
 1537 |