Data.Seq.Internal


   0 | ||| This module is not intended to be imported directly.
   1 | ||| Please use Data.Seq or Data.Seq.Seq' instead.
   2 | |||
   3 | ||| The implementation of fingertree comes from
   4 | ||| <http://hackage.haskell.org/package/containers-0.2.0.1/docs/src/Data-Sequence.html>
   5 | |||
   6 | ||| The original code is under a BSD-style license, compatible with this project.
   7 | |||
   8 | ||| Original Copyrights: Copyright 2004, The University Court of the University of Glasgow
   9 | |||                      (c) Ross Paterson 2005
  10 | module Data.Seq.Internal
  11 | 
  12 | import Control.WellFounded
  13 | import Data.Zippable
  14 | 
  15 | %default total
  16 | 
  17 | err : String -> a
  18 | err s = assert_total (idris_crash s)
  19 | 
  20 | showApp : Show a => a -> String
  21 | showApp = showPrec App
  22 | 
  23 | prettyShow : Prec -> String -> String
  24 | prettyShow p s = if p >= PrefixMinus
  25 |   then "(" ++ s ++ ")"
  26 |   else s
  27 | 
  28 | -- Digit
  29 | data Digit : (e : Type) -> Type where
  30 |   One : (a : e) -> Digit e
  31 |   Two : (a : e) -> (b : e) -> Digit e
  32 |   Three : (a : e) -> (b : e) -> (c : e) -> Digit e
  33 |   Four : (a : e) -> (b : e) -> (c : e) -> (d : e) -> Digit e
  34 | 
  35 | implementation Functor Digit where
  36 |   map f (One a) = One (f a)
  37 |   map f (Two a b) = Two (f a) (f b)
  38 |   map f (Three a b c) = Three (f a) (f b) (f c)
  39 |   map f (Four a b c d) = Four (f a) (f b) (f c) (f d)
  40 | 
  41 | implementation Foldable Digit where
  42 |   foldr f z (One a) = a `f` z
  43 |   foldr f z (Two a b) = a `f` (b `f` z)
  44 |   foldr f z (Three a b c) = a `f` (b `f` (c `f` z))
  45 |   foldr f z (Four a b c d) = a `f` (b `f` (c `f` (d `f` z)))
  46 | 
  47 |   foldl f z (One a) = z `f` a
  48 |   foldl f z (Two a b) = (z `f` a) `f` b
  49 |   foldl f z (Three a b c) = ((z `f` a) `f` b) `f` c
  50 |   foldl f z (Four a b c d) = (((z `f` a) `f` b) `f` c) `f` d
  51 | 
  52 | implementation Traversable Digit where
  53 |   traverse f (One a) = [|One (f a)|]
  54 |   traverse f (Two a b) = [|Two (f a) (f b)|]
  55 |   traverse f (Three a b c) = [|Three (f a) (f b) (f c)|]
  56 |   traverse f (Four a b c d) = [|Four (f a) (f b) (f c) (f d)|]
  57 | 
  58 | implementation Sized e => Sized (Digit e) where
  59 |   size = foldr (\a, z => size a + z) 0
  60 | 
  61 | implementation Show a => Show (Digit a) where
  62 |   showPrec p (One a)        = prettyShow p $
  63 |     "One " ++ showApp a
  64 |   showPrec p (Two a b)      = prettyShow p $
  65 |     "Two " ++ showApp a ++ " " ++ showApp b
  66 |   showPrec p (Three a b c)  = prettyShow p $
  67 |     "Three " ++ showApp a ++ " " ++ showApp b ++ " " ++ showApp c
  68 |   showPrec p (Four a b c d) = prettyShow p $
  69 |     "Four " ++ showApp a ++ " " ++ showApp b ++ " " ++ showApp c ++ " " ++ showApp d
  70 | 
  71 | -- Node
  72 | data Node : (e : Type) -> Type where
  73 |   Node2 : Nat -> (a : e) -> (b : e) -> Node e
  74 |   Node3 : Nat -> (a : e) -> (b : e) -> (c : e) -> Node e
  75 | 
  76 | implementation Functor Node where
  77 |   map f (Node2 s a b)   = Node2 s (f a) (f b)
  78 |   map f (Node3 s a b c) = Node3 s (f a) (f b) (f c)
  79 | 
  80 | implementation Foldable Node where
  81 |   foldr f z (Node2 _ a b)   = a `f` (b `f` z)
  82 |   foldr f z (Node3 _ a b c) = a `f` (b `f` (c `f` z))
  83 | 
  84 |   foldl f z (Node2 _ a b)   = (z `f` a) `f` b
  85 |   foldl f z (Node3 _ a b c) = ((z `f` a) `f` b) `f` c
  86 | 
  87 | implementation Traversable Node where
  88 |   traverse f (Node2 s a b)   = Node2 s <$> f a <*> f b
  89 |   traverse f (Node3 s a b c) = Node3 s <$> f a <*> f b <*> f c
  90 | 
  91 | implementation Sized e => Sized (Node e) where
  92 |   size (Node2 s _ _)   = s
  93 |   size (Node3 s _ _ _) = s
  94 | 
  95 | implementation Show a => Show (Node a) where
  96 |   showPrec p (Node2 _ a b)   = prettyShow p $
  97 |     "Node2 " ++ showApp a ++ " " ++ showApp b
  98 |   showPrec p (Node3 _ a b c) = prettyShow p $
  99 |     "Node3 " ++ showApp a ++ " " ++ showApp b ++ " " ++ showApp c
 100 | 
 101 | -- Smart Constructors
 102 | node2 : Sized e => e -> e -> Node e
 103 | node2 a b = Node2 (size a + size b) a b
 104 | 
 105 | node3 : Sized e => e -> e -> e -> Node e
 106 | node3 a b c = Node3 (size a + size b + size c) a b c
 107 | 
 108 | -- Elem
 109 | public export
 110 | data Elem a = MkElem a
 111 | 
 112 | export
 113 | unElem : Elem a -> a
 114 | unElem (MkElem a) = a
 115 | 
 116 | public export
 117 | implementation Sized (Elem a) where
 118 |   size _ = 1
 119 | 
 120 | public export
 121 | implementation Eq a => Eq (Elem a) where
 122 |   MkElem a == MkElem b = a == b
 123 | 
 124 | public export
 125 | implementation Ord a => Ord (Elem a) where
 126 |   compare (MkElem a) (MkElem b) = compare a b
 127 | 
 128 | public export
 129 | implementation Functor Elem where
 130 |   map f (MkElem a) = MkElem (f a)
 131 | 
 132 | public export
 133 | implementation Applicative Elem where
 134 |   pure = MkElem
 135 |   MkElem f <*> MkElem a = MkElem (f a)
 136 | 
 137 | public export
 138 | implementation Show a => Show (Elem a) where
 139 |   showPrec p (MkElem a) = showPrec p a
 140 | 
 141 | 
 142 | -- FingerTree
 143 | public export
 144 | data FingerTree : (e : Type) -> Type where
 145 |   Empty : FingerTree e
 146 |   Single : (a : e) -> FingerTree e
 147 |   Deep : Nat -> Digit e -> FingerTree (Node e) -> Digit e -> FingerTree e
 148 | 
 149 | public export
 150 | implementation Sized e => Sized (FingerTree e) where
 151 |   size Empty          = 0
 152 |   size (Single a)     = size a
 153 |   size (Deep s _ _ _) = s
 154 | 
 155 | -- Smart Constructor
 156 | deep : Sized e => Digit e -> FingerTree (Node e) -> Digit e -> FingerTree e
 157 | deep d1 st d2 = Deep (size d1 + size st + size d2) d1 st d2
 158 | 
 159 | 
 160 | -- Reversing
 161 | reverseDigit : (a -> a) -> Digit a -> Digit a
 162 | reverseDigit f (One a) = One (f a)
 163 | reverseDigit f (Two a b) = Two (f b) (f a)
 164 | reverseDigit f (Three a b c) = Three (f c) (f b) (f a)
 165 | reverseDigit f (Four a b c d) = Four (f d) (f c) (f b) (f a)
 166 | 
 167 | reverseNode : (a -> a) -> Node a -> Node a
 168 | reverseNode f (Node2 s a b) = Node2 s (f b) (f a)
 169 | reverseNode f (Node3 s a b c) = Node3 s (f c) (f b) (f a)
 170 | 
 171 | export
 172 | reverseTree : (a -> a) -> FingerTree a -> FingerTree a
 173 | reverseTree _ Empty = Empty
 174 | reverseTree f (Single x) = Single (f x)
 175 | reverseTree f (Deep s pr m sf) =
 176 |   Deep s (reverseDigit f sf)
 177 |     (reverseTree (reverseNode f) m)
 178 |     (reverseDigit f pr)
 179 | 
 180 | 
 181 | -- Looking up
 182 | lookupDigit : Sized a => Nat -> Digit a -> (Nat, a)
 183 | lookupDigit i (One a) = (i, a)
 184 | lookupDigit i (Two a b) =
 185 |   let sa = size a
 186 |   in if i < sa
 187 |     then (i, a)
 188 |     else (i `minus` sa, b)
 189 | lookupDigit i (Three a b c) =
 190 |   let sa  = size a
 191 |       sab = sa + size b
 192 |   in if i < sa
 193 |     then (i, a)
 194 |     else if i < sab
 195 |       then (i `minus` sa, b)
 196 |       else ((i `minus` sa) `minus` sab, c)
 197 | lookupDigit i (Four a b c d) =
 198 |   let sa   = size a
 199 |       sab  = sa + size b
 200 |       sabc = sab + size c
 201 |   in if i < sab
 202 |     then if i < sa
 203 |       then (i, a)
 204 |       else (i `minus` sa, b)
 205 |     else if i < sabc
 206 |       then (i `minus` sab, c)
 207 |       else (i `minus` sabc, d)
 208 | 
 209 | lookupNode : Sized a => Nat -> Node a -> (Nat, a)
 210 | lookupNode i (Node2 _ a b) =
 211 |   let sa = size a
 212 |   in if i < sa
 213 |     then (i, a)
 214 |     else (i `minus` sa, b)
 215 | lookupNode i (Node3 _ a b c) =
 216 |   let sa  = size a
 217 |       sab = sa + size b
 218 |   in if i < sa
 219 |     then (i, a)
 220 |     else if i < sab
 221 |       then (i `minus` sa, b)
 222 |       else (i `minus` sab, c)
 223 | 
 224 | export
 225 | lookupTree : Sized a => Nat -> FingerTree a -> (Nat, a)
 226 | lookupTree _ Empty = err "lookupTree of empty tree"
 227 | lookupTree i (Single x) = (i, x)
 228 | lookupTree i (Deep _ pr m sf) =
 229 |   let spr = size pr
 230 |       spm = spr + size m
 231 |   in if i < spr
 232 |     then lookupDigit i pr
 233 |     else if i < spm
 234 |       then let (i', xs) = lookupTree (i `minus` spr) m
 235 |            in lookupNode i' xs
 236 |       else lookupDigit (i `minus` spm) sf
 237 | 
 238 | -- Adjusting
 239 | adjustDigit : Sized a => (Nat -> a -> a) -> Nat -> Digit a -> Digit a
 240 | adjustDigit f i (One a) = One (f i a)
 241 | adjustDigit f i (Two a b) =
 242 |   let sa = size a
 243 |   in if i < sa
 244 |     then Two (f i a) b
 245 |     else Two a (f (i `minus` sa) b)
 246 | adjustDigit f i (Three a b c) =
 247 |   let sa  = size a
 248 |       sab = sa + size b
 249 |   in if i < sa
 250 |     then Three (f i a) b c
 251 |     else if i < sab
 252 |       then Three a (f (i `minus` sa) b) c
 253 |       else Three a b (f (i `minus` sab) c)
 254 | adjustDigit f i (Four a b c d) =
 255 |   let sa   = size a
 256 |       sab  = sa + size b
 257 |       sabc = sab + size c
 258 |   in if i < sab
 259 |     then if i < sa
 260 |       then Four (f i a) b c d
 261 |       else Four a (f (i `minus` sa) b) c d
 262 |     else if i < sabc
 263 |       then Four a b (f (i `minus` sab) c) d
 264 |       else Four a b c (f (i `minus` sabc) d)
 265 | 
 266 | adjustNode : Sized a => (Nat -> a -> a) -> Nat -> Node a -> Node a
 267 | adjustNode f i (Node2 s a b) =
 268 |   let sa = size a
 269 |   in if i < sa
 270 |     then Node2 s (f i a) b
 271 |     else Node2 s a (f (i `minus` sa) b)
 272 | adjustNode f i (Node3 s a b c) =
 273 |   let sa  = size a
 274 |       sab = sa + size b
 275 |   in if i < sa
 276 |     then Node3 s (f i a) b c
 277 |     else if i < sab
 278 |       then Node3 s a (f (i `minus` sa) b) c
 279 |       else Node3 s a b (f (i `minus` sab) c)
 280 | 
 281 | export
 282 | adjustTree : Sized a => (Nat -> a -> a) -> Nat -> FingerTree a -> FingerTree a
 283 | adjustTree _ _ Empty = err "adjustTree of empty tree"
 284 | adjustTree f i (Single x) = Single (f i x)
 285 | adjustTree f i (Deep s pr m sf) =
 286 |   let spr = size pr
 287 |       spm = spr + size m
 288 |   in if i < spr
 289 |     then Deep s (adjustDigit f i pr) m sf
 290 |     else if i < spm
 291 |       then Deep s pr (adjustTree (adjustNode f) (i `minus` spr) m) sf
 292 |       else Deep s pr m (adjustDigit f (i `minus` spm) sf)
 293 | 
 294 | 
 295 | -- Casting between types
 296 | digitToTree : Sized a => Digit a -> FingerTree a
 297 | digitToTree (One a)        = Single a
 298 | digitToTree (Two a b)      = deep (One a) Empty (One b)
 299 | digitToTree (Three a b c)  = deep (Two a b) Empty (One c)
 300 | digitToTree (Four a b c d) = deep (Two a b) Empty (Two c d)
 301 | 
 302 | nodeToDigit : Node e -> Digit e
 303 | nodeToDigit (Node2 _ a b)   = Two a b
 304 | nodeToDigit (Node3 _ a b c) = Three a b c
 305 | 
 306 | 
 307 | -- Viewing
 308 | export
 309 | viewLTree  : Sized a => FingerTree a -> Maybe (a, FingerTree a)
 310 | viewLTree Empty = Nothing
 311 | viewLTree (Single a) = Just (a, Empty)
 312 | viewLTree (Deep s (One a) m sf) =
 313 |   let tr =
 314 |     case viewLTree m of
 315 |         Nothing      => digitToTree sf
 316 |         Just (b, m') => Deep (s `minus` size a) (nodeToDigit b) m' sf
 317 |   in Just (a, tr)
 318 | viewLTree (Deep s (Two a b) m sf) =
 319 |   Just (a, Deep (s `minus` size a) (One b) m sf)
 320 | viewLTree (Deep s (Three a b c) m sf) =
 321 |   Just (a, Deep (s `minus` size a) (Two b c) m sf)
 322 | viewLTree (Deep s (Four a b c d) m sf) =
 323 |   Just (a, Deep (s `minus` size a) (Three b c d) m sf)
 324 | 
 325 | export
 326 | viewRTree  : Sized a => FingerTree a -> Maybe (FingerTree a, a)
 327 | viewRTree Empty = Nothing
 328 | viewRTree (Single z) = Just (Empty, z)
 329 | viewRTree (Deep s pr m (One z)) =
 330 |   let tr =
 331 |     case viewRTree m of
 332 |         Nothing      => digitToTree pr
 333 |         Just (m', y) => Deep (s `minus` size z) pr m' (nodeToDigit y)
 334 |   in Just (tr, z)
 335 | viewRTree (Deep s pr m (Two y z)) =
 336 |   Just (Deep (s `minus` size z) pr m (One y), z)
 337 | viewRTree (Deep s pr m (Three x y z)) =
 338 |   Just (Deep (s `minus` size z) pr m (Two x y), z)
 339 | viewRTree (Deep s pr m (Four w x y z)) =
 340 |   Just (Deep (s `minus` size z) pr m (Three w x y), z)
 341 | 
 342 | 
 343 | -- Construction
 344 | export infixr 5 `consTree`
 345 | export
 346 | consTree : Sized e => (r : e) -> FingerTree e -> FingerTree e
 347 | a `consTree` Empty                       = Single a
 348 | a `consTree` Single b                    = deep (One a) Empty (One b)
 349 | a `consTree` Deep s (One b) st d2        = Deep (size a + s) (Two a b) st d2
 350 | a `consTree` Deep s (Two b c) st d2      = Deep (size a + s) (Three a b c) st d2
 351 | a `consTree` Deep s (Three b c d) st d2  = Deep (size a + s) (Four a b c d) st d2
 352 | a `consTree` Deep s (Four b c d f) st d2 = Deep (size a + s) (Two a b) (node3 c d f `consTree` st) d2
 353 | 
 354 | export infixl 5 `snocTree`
 355 | export
 356 | snocTree : Sized e => FingerTree e -> (r : e) -> FingerTree e
 357 | Empty `snocTree` a                       = Single a
 358 | Single a `snocTree` b                    = deep (One a) Empty (One b)
 359 | Deep s d1 st (One a) `snocTree` f        = Deep (s + size a) d1 st (Two a f)
 360 | Deep s d1 st (Two a b) `snocTree` f      = Deep (s + size a) d1 st (Three a b f)
 361 | Deep s d1 st (Three a b c) `snocTree` f  = Deep (s + size a) d1 st (Four a b c f)
 362 | Deep s d1 st (Four a b c d) `snocTree` f = Deep (s + size f) d1 (st `snocTree` node3 a b c) (Two d f)
 363 | 
 364 | 
 365 | -- Splitting
 366 | data Split t a = MkSplit t a t
 367 | 
 368 | splitDigit : Sized a => Nat -> Digit a -> Split (Maybe (Digit a)) a
 369 | splitDigit i (One a) = MkSplit Nothing a Nothing
 370 | splitDigit i (Two a b) =
 371 |   let sa = size a
 372 |   in if i < sa
 373 |     then MkSplit Nothing a (Just (One b))
 374 |     else MkSplit (Just (One a)) b Nothing
 375 | splitDigit i (Three a b c) =
 376 |   let sa  = size a
 377 |       sab = sa + size b
 378 |   in if i < sa
 379 |     then MkSplit Nothing a (Just (Two b c))
 380 |     else if i < sab
 381 |       then MkSplit (Just (One a)) b (Just (One c))
 382 |       else MkSplit (Just (Two a b)) c Nothing
 383 | splitDigit i (Four a b c d) =
 384 |   let sa   = size a
 385 |       sab  = sa + size b
 386 |       sabc = sab + size c
 387 |   in if i < sab
 388 |     then if i < sa
 389 |       then MkSplit Nothing a (Just (Three b c d))
 390 |       else MkSplit (Just (One a)) b (Just (Two c d))
 391 |     else if i < sabc
 392 |       then MkSplit (Just (Two a b)) c (Just (One d))
 393 |       else MkSplit (Just (Three a b c)) d Nothing
 394 | 
 395 | splitNode : Sized a => Nat -> Node a -> Split (Maybe (Digit a)) a
 396 | splitNode i (Node2 _ a b) =
 397 |   let sa = size a
 398 |   in if i < sa
 399 |     then MkSplit Nothing a (Just (One b))
 400 |     else MkSplit (Just (One a)) b Nothing
 401 | splitNode i (Node3 _ a b c) =
 402 |   let sa  = size a
 403 |       sab = sa + size b
 404 |   in if i < sa
 405 |     then MkSplit Nothing a (Just (Two b c))
 406 |     else if i < sab
 407 |       then MkSplit (Just (One a)) b (Just (One c))
 408 |       else MkSplit (Just (Two a b)) c Nothing
 409 | 
 410 | deepL : Sized a => Maybe (Digit a) -> FingerTree (Node a) -> Digit a -> FingerTree a
 411 | deepL Nothing m sf = case viewLTree m of
 412 |   Nothing      => digitToTree sf
 413 |   Just (a, m') => Deep (size m + size sf) (nodeToDigit a) m' sf
 414 | deepL (Just pr) m sf = deep pr m sf
 415 | 
 416 | deepR : Sized a => Digit a -> FingerTree (Node a) -> Maybe (Digit a) -> FingerTree a
 417 | deepR pr m Nothing = case viewRTree m of
 418 |   Nothing      => digitToTree pr
 419 |   Just (m', a) => Deep (size pr + size m) pr m' (nodeToDigit a)
 420 | deepR pr m (Just sf) = deep pr m sf
 421 | 
 422 | splitTree : Sized a => Nat -> FingerTree a -> Split (FingerTree a) a
 423 | splitTree _ Empty = err "splitTree of empty tree"
 424 | splitTree i (Single x) = MkSplit Empty x Empty
 425 | splitTree i (Deep _ pr m sf) =
 426 |   let spr = size pr
 427 |       spm = spr + size m
 428 |       im  = i `minus` spr
 429 |   in if i < spr
 430 |     then let MkSplit l x r = splitDigit i pr
 431 |          in MkSplit (maybe Empty digitToTree l) x (deepL r m sf)
 432 |     else if i < spm
 433 |       then let MkSplit ml xs mr = splitTree im m
 434 |                MkSplit l x r = splitNode (im `minus` size ml) xs
 435 |            in MkSplit (deepR pr  ml l) x (deepL r mr sf)
 436 |       else let MkSplit l x r = splitDigit (i `minus` spm) sf
 437 |            in MkSplit (deepR pr  m  l) x (maybe Empty digitToTree r)
 438 | 
 439 | export
 440 | split : Nat -> FingerTree (Elem a) -> (FingerTree (Elem a), FingerTree (Elem a))
 441 | split _ Empty = (Empty, Empty)
 442 | split i xs =
 443 |   if size xs > i
 444 |    then let MkSplit l x r = splitTree i xs in (l, x `consTree` r)
 445 |    else (xs, Empty)
 446 | 
 447 | 
 448 | -- Concatenation
 449 | mutual
 450 |   addDigits4 : Sized e => FingerTree (Node (Node e)) -> Digit (Node e) -> Node e -> Node e -> Node e -> Node e -> Digit (Node e) -> FingerTree (Node (Node e)) -> FingerTree (Node (Node e))
 451 |   addDigits4 m1 (One a) b c d e (One f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 452 |   addDigits4 m1 (One a) b c d e (Two f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 453 |   addDigits4 m1 (One a) b c d e (Three f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 454 |   addDigits4 m1 (One a) b c d e (Four f g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
 455 |   addDigits4 m1 (Two a b) c d e f (One g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 456 |   addDigits4 m1 (Two a b) c d e f (Two g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 457 |   addDigits4 m1 (Two a b) c d e f (Three g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
 458 |   addDigits4 m1 (Two a b) c d e f (Four g h i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
 459 |   addDigits4 m1 (Three a b c) d e f g (One h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 460 |   addDigits4 m1 (Three a b c) d e f g (Two h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
 461 |   addDigits4 m1 (Three a b c) d e f g (Three h i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
 462 |   addDigits4 m1 (Three a b c) d e f g (Four h i j k) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) m2
 463 |   addDigits4 m1 (Four a b c d) e f g h (One i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
 464 |   addDigits4 m1 (Four a b c d) e f g h (Two i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
 465 |   addDigits4 m1 (Four a b c d) e f g h (Three i j k) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) m2
 466 |   addDigits4 m1 (Four a b c d) e f g h (Four i j k l) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node3 g h i) (node3 j k l) m2
 467 | 
 468 |   appendTree4 : Sized e => FingerTree (Node e) -> Node e -> Node e -> Node e -> Node e -> FingerTree (Node e) -> FingerTree (Node e)
 469 |   appendTree4 Empty a b c d xs = a `consTree` b `consTree` c `consTree` d `consTree` xs
 470 |   appendTree4 xs a b c d Empty = xs `snocTree` a `snocTree` b `snocTree` c `snocTree` d
 471 |   appendTree4 (Single x) a b c d xs = x `consTree` a `consTree` b `consTree` c `consTree` d `consTree` xs
 472 |   appendTree4 xs a b c d (Single x) = xs `snocTree` a `snocTree` b `snocTree` c `snocTree` d `snocTree` x
 473 |   appendTree4 (Deep s1 pr1 m1 sf1) a b c d (Deep s2 pr2 m2 sf2) = Deep (s1 + size a + size b + size c + size d + s2) pr1 (addDigits4 m1 sf1 a b c d pr2 m2) sf2
 474 | 
 475 |   addDigits3 : Sized e => FingerTree (Node (Node e)) -> Digit (Node e) -> Node e -> Node e -> Node e -> Digit (Node e) -> FingerTree (Node (Node e)) -> FingerTree (Node (Node e))
 476 |   addDigits3 m1 (One a) b c d (One e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
 477 |   addDigits3 m1 (One a) b c d (Two e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 478 |   addDigits3 m1 (One a) b c d (Three e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 479 |   addDigits3 m1 (One a) b c d (Four e f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 480 |   addDigits3 m1 (Two a b) c d e (One f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 481 |   addDigits3 m1 (Two a b) c d e (Two f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 482 |   addDigits3 m1 (Two a b) c d e (Three f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 483 |   addDigits3 m1 (Two a b) c d e (Four f g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
 484 |   addDigits3 m1 (Three a b c) d e f (One g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 485 |   addDigits3 m1 (Three a b c) d e f (Two g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 486 |   addDigits3 m1 (Three a b c) d e f (Three g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
 487 |   addDigits3 m1 (Three a b c) d e f (Four g h i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
 488 |   addDigits3 m1 (Four a b c d) e f g (One h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 489 |   addDigits3 m1 (Four a b c d) e f g (Two h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
 490 |   addDigits3 m1 (Four a b c d) e f g (Three h i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
 491 |   addDigits3 m1 (Four a b c d) e f g (Four h i j k) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) m2
 492 | 
 493 |   appendTree3 : Sized e => FingerTree (Node e) -> Node e -> Node e -> Node e -> FingerTree (Node e) -> FingerTree (Node e)
 494 |   appendTree3 Empty a b c xs = a `consTree` b `consTree` c `consTree` xs
 495 |   appendTree3 xs a b c Empty = xs `snocTree` a `snocTree` b `snocTree` c
 496 |   appendTree3 (Single x) a b c xs = x `consTree` a `consTree` b `consTree` c `consTree` xs
 497 |   appendTree3 xs a b c (Single x) = xs `snocTree` a `snocTree` b `snocTree` c `snocTree` x
 498 |   appendTree3 (Deep s1 pr1 m1 sf1) a b c (Deep s2 pr2 m2 sf2) = Deep (s1 + size a + size b + size c + s2) pr1 (addDigits3 m1 sf1 a b c pr2 m2) sf2
 499 | 
 500 |   addDigits2 : Sized e => FingerTree (Node (Node e)) -> Digit (Node e) -> Node e -> Node e -> Digit (Node e) -> FingerTree (Node (Node e)) -> FingerTree (Node (Node e))
 501 |   addDigits2 m1 (One a) b c (One d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
 502 |   addDigits2 m1 (One a) b c (Two d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
 503 |   addDigits2 m1 (One a) b c (Three d e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 504 |   addDigits2 m1 (One a) b c (Four d e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 505 |   addDigits2 m1 (Two a b) c d (One e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
 506 |   addDigits2 m1 (Two a b) c d (Two e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 507 |   addDigits2 m1 (Two a b) c d (Three e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 508 |   addDigits2 m1 (Two a b) c d (Four e f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 509 |   addDigits2 m1 (Three a b c) d e (One f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 510 |   addDigits2 m1 (Three a b c) d e (Two f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 511 |   addDigits2 m1 (Three a b c) d e (Three f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 512 |   addDigits2 m1 (Three a b c) d e (Four f g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
 513 |   addDigits2 m1 (Four a b c d) e f (One g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 514 |   addDigits2 m1 (Four a b c d) e f (Two g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 515 |   addDigits2 m1 (Four a b c d) e f (Three g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
 516 |   addDigits2 m1 (Four a b c d) e f (Four g h i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
 517 | 
 518 |   appendTree2 : Sized e => FingerTree (Node e) -> Node e -> Node e -> FingerTree (Node e) -> FingerTree (Node e)
 519 |   appendTree2 Empty a b xs = a `consTree` b `consTree` xs
 520 |   appendTree2 xs a b Empty = xs `snocTree` a `snocTree` b
 521 |   appendTree2 (Single x) a b xs = x `consTree` a `consTree` b `consTree` xs
 522 |   appendTree2 xs a b (Single x) = xs `snocTree` a `snocTree` b `snocTree` x
 523 |   appendTree2 (Deep s1 pr1 m1 sf1) a b (Deep s2 pr2 m2 sf2) = Deep (s1 + size a + size b + s2) pr1 (addDigits2 m1 sf1 a b pr2 m2) sf2
 524 | 
 525 | mutual
 526 |   addDigits1 : Sized e => FingerTree (Node (Node e)) -> Digit (Node e) -> Node e -> Digit (Node e) -> FingerTree (Node (Node e)) -> FingerTree (Node (Node e))
 527 |   addDigits1 m1 (One a) b (One c) m2 = appendTree1 m1 (node3 a b c) m2
 528 |   addDigits1 m1 (One a) b (Two c d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
 529 |   addDigits1 m1 (One a) b (Three c d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
 530 |   addDigits1 m1 (One a) b (Four c d e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 531 |   addDigits1 m1 (Two a b) c (One d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
 532 |   addDigits1 m1 (Two a b) c (Two d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
 533 |   addDigits1 m1 (Two a b) c (Three d e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 534 |   addDigits1 m1 (Two a b) c (Four d e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 535 |   addDigits1 m1 (Three a b c) d (One e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
 536 |   addDigits1 m1 (Three a b c) d (Two e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 537 |   addDigits1 m1 (Three a b c) d (Three e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 538 |   addDigits1 m1 (Three a b c) d (Four e f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 539 |   addDigits1 m1 (Four a b c d) e (One f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 540 |   addDigits1 m1 (Four a b c d) e (Two f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 541 |   addDigits1 m1 (Four a b c d) e (Three f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 542 |   addDigits1 m1 (Four a b c d) e (Four f g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
 543 | 
 544 |   appendTree1 : Sized e => FingerTree (Node e) -> Node e -> FingerTree (Node e) -> FingerTree (Node e)
 545 |   appendTree1 Empty a xs = a `consTree` xs
 546 |   appendTree1 xs a Empty = xs `snocTree` a
 547 |   appendTree1 (Single x) a xs = x `consTree` a `consTree` xs
 548 |   appendTree1 xs a (Single x) = xs `snocTree` a `snocTree` x
 549 |   appendTree1 (Deep s1 pr1 m1 sf1) a (Deep s2 pr2 m2 sf2) = Deep (s1 + size a + s2) pr1 (addDigits1 m1 sf1 a pr2 m2) sf2
 550 | 
 551 | addDigits0 : FingerTree (Node (Elem a)) -> Digit (Elem a) -> Digit (Elem a) -> FingerTree (Node (Elem a)) -> FingerTree (Node (Elem a))
 552 | addDigits0 m1 (One a) (One b) m2 = appendTree1 m1 (node2 a b) m2
 553 | addDigits0 m1 (One a) (Two b c) m2 = appendTree1 m1 (node3 a b c) m2
 554 | addDigits0 m1 (One a) (Three b c d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
 555 | addDigits0 m1 (One a) (Four b c d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
 556 | addDigits0 m1 (Two a b) (One c) m2 = appendTree1 m1 (node3 a b c) m2
 557 | addDigits0 m1 (Two a b) (Two c d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
 558 | addDigits0 m1 (Two a b) (Three c d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
 559 | addDigits0 m1 (Two a b) (Four c d e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 560 | addDigits0 m1 (Three a b c) (One d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
 561 | addDigits0 m1 (Three a b c) (Two d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
 562 | addDigits0 m1 (Three a b c) (Three d e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 563 | addDigits0 m1 (Three a b c) (Four d e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 564 | addDigits0 m1 (Four a b c d) (One e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
 565 | addDigits0 m1 (Four a b c d) (Two e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
 566 | addDigits0 m1 (Four a b c d) (Three e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
 567 | addDigits0 m1 (Four a b c d) (Four e f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
 568 | 
 569 | export
 570 | addTree0 : FingerTree (Elem a) -> FingerTree (Elem a) -> FingerTree (Elem a)
 571 | addTree0 Empty xs = xs
 572 | addTree0 xs Empty = xs
 573 | addTree0 (Single x) xs = x `consTree` xs
 574 | addTree0 xs (Single x) = xs `snocTree` x
 575 | addTree0 (Deep s1 pr1 m1 sf1) (Deep s2 pr2 m2 sf2) = Deep (s1 + s2) pr1 (addDigits0 m1 sf1 pr2 m2) sf2
 576 | 
 577 | -- List-like
 578 | export
 579 | toList' : FingerTree (Elem a) -> List a
 580 | toList' tr = case viewLTree tr of
 581 |     Just (MkElem a, tr') => a :: assert_total (toList' tr')
 582 |     Nothing              => Nil
 583 | 
 584 | export
 585 | replicate' : Nat -> e -> FingerTree (Elem e)
 586 | replicate' n a = replicate1 n Empty
 587 |   where
 588 |     elem : Elem e
 589 |     elem = MkElem a
 590 |     replicate1 : Nat -> FingerTree (Elem e) -> FingerTree (Elem e)
 591 |     replicate1 Z tr = tr
 592 |     replicate1 (S k) tr = replicate1 k (elem `consTree` tr)
 593 | 
 594 | export
 595 | length' : FingerTree (Elem e) -> Nat
 596 | length' = size
 597 | 
 598 | -- FingerTree Implementations
 599 | public export
 600 | implementation Functor FingerTree where
 601 |   map _ Empty = Empty
 602 |   map f (Single x) = Single (f x)
 603 |   map f (Deep s d1 st d2) =
 604 |     Deep s (map f d1) (map (map f) st) (map f d2)
 605 | 
 606 | public export
 607 | implementation Foldable FingerTree where
 608 |   foldr _ z Empty            = z
 609 |   foldr f z (Single x)       = x `f` z
 610 |   foldr f z (Deep _ pr m sf) = foldr f (foldr (flip (foldr f)) (foldr f z sf) m) pr
 611 | 
 612 |   foldl _ z Empty            = z
 613 |   foldl f z (Single x)       = z `f` x
 614 |   foldl f z (Deep _ pr m sf) = foldl f (foldl (foldl f) (foldl f z pr) m) sf
 615 | 
 616 | public export
 617 | implementation Traversable FingerTree where
 618 |   traverse _ Empty            = pure Empty
 619 |   traverse f (Single x)       = Single <$> f x
 620 |   traverse f (Deep v pr m sf) =
 621 |     Deep v <$> traverse f pr <*> traverse (traverse f) m <*> traverse f sf
 622 | 
 623 | public export
 624 | implementation Show a => Show (FingerTree a) where
 625 |   showPrec _ Empty             = "Empty"
 626 |   showPrec p (Single a)        = prettyShow p $ "Single " ++ showApp a
 627 |   showPrec p (Deep _ d1 st d2) = prettyShow p $
 628 |     "Deep " ++ showApp d1 ++ " " ++ assert_total (showApp st) ++ " " ++ showApp d2
 629 | 
 630 | public export
 631 | implementation Sized a => Eq a => Eq (FingerTree a) where
 632 |   x == y = case (viewLTree x, viewLTree y) of
 633 |     (Just (x1, xs), Just (y1, ys)) => if x1 == y1
 634 |       then assert_total (xs == ys)
 635 |       else False
 636 |     (Nothing, Nothing) => True
 637 |     _                  => False
 638 | 
 639 | public export
 640 | implementation Sized a => Ord a => Ord (FingerTree a) where
 641 |   compare x y = case (viewLTree x, viewLTree y) of
 642 |     (Just (x1, xs), Just (y1, ys)) =>
 643 |       let res = compare x1 y1
 644 |       in if res == EQ
 645 |         then assert_total (compare xs ys)
 646 |         else res
 647 |     (Nothing, Nothing) => EQ
 648 |     (_      , Nothing) => GT
 649 |     (Nothing, _      ) => LT
 650 | 
 651 | 
 652 | -- Zipping
 653 | export
 654 | zipWith' : (a -> b -> c) -> FingerTree (Elem a) -> FingerTree (Elem b) -> FingerTree (Elem c)
 655 | zipWith' f x y = case (viewLTree x, viewLTree y) of
 656 |   (Just (x1, xs), Just (y1, ys)) => [|f x1 y1|] `consTree` assert_total (zipWith' f xs ys)
 657 |   _ => Empty
 658 | 
 659 | export
 660 | zipWith3' : (a -> b -> c -> d) -> FingerTree (Elem a) -> FingerTree (Elem b) -> FingerTree (Elem c) -> FingerTree (Elem d)
 661 | zipWith3' f x y z = case (viewLTree x, viewLTree y, viewLTree z) of
 662 |   (Just (x1, xs), Just (y1, ys), Just (z1, zs)) => [|f x1 y1 z1|] `consTree` assert_total (zipWith3' f xs ys zs)
 663 |   _ => Empty
 664 | 
 665 | export
 666 | unzipWith' : (a -> (b, c)) -> FingerTree (Elem a) -> (FingerTree (Elem b), FingerTree (Elem c))
 667 | unzipWith' f zs = foldr app (Empty, Empty) zs
 668 |   where
 669 |     app : Elem a -> (FingerTree (Elem b), FingerTree (Elem c)) -> (FingerTree (Elem b), FingerTree (Elem c))
 670 |     app (MkElem z) (xs, ys) = let (x, y) = f z in (MkElem x `consTree` xs, MkElem y `consTree` ys)
 671 | 
 672 | export
 673 | unzipWith3' : (a -> (b, c, d)) -> FingerTree (Elem a)
 674 |             -> (FingerTree (Elem b), FingerTree (Elem c), FingerTree (Elem d))
 675 | unzipWith3' f ws = foldr app (Empty, Empty, Empty) ws
 676 |   where
 677 |     app : Elem a -> (FingerTree (Elem b), FingerTree (Elem c), FingerTree (Elem d))
 678 |         -> (FingerTree (Elem b), FingerTree (Elem c), FingerTree (Elem d))
 679 |     app (MkElem w) (xs, ys, zs) =
 680 |       let (x, y, z) = f w
 681 |       in (MkElem x `consTree` xs, MkElem y `consTree` ys, MkElem z `consTree` zs)
 682 |