2 | module Data.DMap

   4 | import Control.Monad.State

   5 | import Data.Maybe

   7 | import public Data.DFunctor

   8 | import public Data.DFoldable

   9 | import public Data.DSum

  10 | import public Data.DOrd

  11 | import public Data.DEq

  12 | import public Data.Some

  14 | import Hedgehog

  16 | error : String -> a

  17 | error msg = assert_total $ idris_crash msg

  20 | public export

  21 | ShowS : Type

  22 | ShowS = String -> String

  25 | showString : String -> ShowS

  26 | showString = (++)

  48 | data DMap : (k : a -> Type) -> (f : a -> Type) -> Type where

  49 |     Tip : DMap k f

  50 |     Bin : (sz    : Int)

  51 |        -> (key   : k v)

  52 |        -> (value : f v)

  53 |        -> (left  : DMap k f)

  54 |        -> (right : DMap k f)

  55 |        -> DMap k f

  68 | empty : DMap k f

  69 | empty = Tip

  78 | singleton : {0 v : a} -> k v -> f v -> DMap k f

  79 | singleton k x = Bin 1 k x Tip Tip

  87 | null : DMap k f -> Bool

  88 | null Tip              = True

  89 | null (Bin _ _ _ _ _)  = False

  93 | size : DMap k f -> Int

  94 | size Tip                = 0

  95 | size (Bin n _ _ _ _)    = n

 102 | lookup : (impl : DOrd k) => k v -> DMap k f -> Maybe (f v)

 103 | lookup k Tip = Nothing

 104 | lookup k (Bin _ kx x l r) = case dcompare k kx @{impl} of

 105 |   DLT => lookup k l

 106 |   DGT => lookup k r

 107 |   DEQ => Just x

 110 | lookupAssoc : (impl : DOrd k) => Some k -> DMap k f -> Maybe (DSum k f)

 111 | lookupAssoc sk = withSome sk $ \key =>

 112 |   let

 113 |     go : DMap k f -> Maybe (DSum k f)

 114 |     go Tip = Nothing

 115 |     go (Bin _ kx x l r) =

 116 |         case dcompare key kx @{impl} of

 117 |             DLT => go l

 118 |             DGT => go r

 119 |             DEQ => Just (kx :=> x)

 120 |   in go

 151 | delta, ratio : Int

 152 | delta = 4

 153 | ratio = 2

 160 | bin : {0 v : a} -> k v -> f v -> DMap k f -> DMap k f -> DMap k f

 161 | bin k x l r

 162 |   = Bin (size l + size r + 1) k x l r

 168 | singleL, singleR : {0 v : a} -> k v -> f v -> DMap k f -> DMap k f -> DMap k f

 169 | singleL k1 x1 t1 (Bin _ k2 x2 t2 t3)  = bin k2 x2 (bin k1 x1 t1 t2) t3

 170 | singleL _ _ _ Tip = error "error: singleL Tip"

 171 | singleR k1 x1 (Bin _ k2 x2 t1 t2) t3  = bin k2 x2 t1 (bin k1 x1 t2 t3)

 172 | singleR _ _ Tip _ = error "error: singleR Tip"

 175 | doubleL, doubleR : {0 v : a} -> k v -> f v -> DMap k f -> DMap k f -> DMap k f

 176 | doubleL k1 x1 t1 (Bin _ k2 x2 (Bin _ k3 x3 t2 t3) t4) = bin k3 x3 (bin k1 x1 t1 t2) (bin k2 x2 t3 t4)

 177 | doubleL _ _ _ _ = error "error: doubleL"

 178 | doubleR k1 x1 (Bin _ k2 x2 t1 (Bin _ k3 x3 t2 t3)) t4 = bin k3 x3 (bin k2 x2 t1 t2) (bin k1 x1 t3 t4)

 179 | doubleR _ _ _ _ = error "error: doubleR"

 184 | rotateL : {0 v : a} -> k v -> f v -> DMap k f -> DMap k f -> DMap k f

 185 | rotateL k x l r@(Bin _ _ _ ly ry)

 186 |   = if size ly < ratio*size ry then singleL k x l r

 187 |                                else doubleL k x l r

 188 | rotateL _ _ _ Tip = error "error: rotateL Tip"

 191 | rotateR : {0 v : a} -> k v -> f v -> DMap k f -> DMap k f -> DMap k f

 192 | rotateR k x l@(Bin _ _ _ ly ry) r

 193 |   = if size ry < ratio*size ly then singleR k x l r

 194 |                                else doubleR k x l r

 195 | rotateR _ _ Tip _ = error "error: rotateR Tip"

 229 | balance : {0 v : a} -> k v -> f v -> DMap k f -> DMap k f -> DMap k f

 230 | balance k x l r

 231 |   =    if sizeL + sizeR <= 1   then Bin sizeX k x l r

 232 |   else if sizeR >= delta*sizeL then rotateL k x l r

 233 |   else if sizeL >= delta*sizeR then rotateR k x l r

 234 |   else                              Bin sizeX k x l r

 236 |   where

 237 |     sizeL, sizeR, sizeX : Int

 238 |     sizeL = size l

 239 |     sizeR = size r

 240 |     sizeX = sizeL + sizeR + 1

 249 | insertMax, insertMin : {0 v : a} -> k v -> f v -> DMap k f -> DMap k f

 250 | insertMax kx x t

 251 |   = case t of

 252 |       Tip => singleton kx x

 253 |       Bin _ ky y l r

 254 |           => balance ky y l (insertMax kx x r)

 256 | insertMin kx x t

 257 |   = case t of

 258 |       Tip => singleton kx x

 259 |       Bin _ ky y l r

 260 |           => balance ky y (insertMin kx x l) r

 263 | combine : DOrd k => k v -> f v -> DMap k f -> DMap k f -> DMap k f

 264 | combine kx x Tip r  = insertMin kx x r

 265 | combine kx x l Tip  = insertMax kx x l

 266 | combine kx x l@(Bin sizeL ky y ly ry) r@(Bin sizeR kz z lz rz)

 267 |   =    if delta*sizeL <= sizeR then balance kz z (combine kx x l lz) rz

 268 |   else if delta*sizeR <= sizeL then balance ky y ly (combine kx x ry r)

 269 |   else                              bin kx x l r

 274 | minViewWithKey : DMap k f -> Maybe (DSum k f, DMap k f)

 275 | minViewWithKey Tip = Nothing

 276 | minViewWithKey (Bin _ k0 x0 l0 r0) = Just $ go k0 x0 l0 r0

 277 |   where

 278 |     go : {0 k, f : a -> Type} -> k v -> f v -> DMap k f -> DMap k f -> (DSum k f, DMap k f)

 279 |     go k x Tip r = (k :=> x, r)

 280 |     go k x (Bin _ kl xl ll lr) r =

 281 |       let (km, l') = go kl xl ll lr

 282 |       in (km, balance k x l' r)

 287 | maxViewWithKey : DMap k f -> Maybe (DSum k f, DMap k f)

 288 | maxViewWithKey Tip = Nothing

 289 | maxViewWithKey (Bin _ k0 x0 l0 r0) = Just $ go k0 x0 l0 r0

 290 |   where

 291 |     go : k v -> f v -> DMap k f -> DMap k f -> (DSum k f, DMap k f)

 292 |     go k x l Tip = (k :=> x, l)

 293 |     go k x l (Bin _ kr xr rl rr) =

 294 |       let (km, r') = go kr xr rl rr

 295 |       in (km, balance k x l r')

 305 | deleteFindMax : DMap k f -> (DSum k f, DMap k f)

 306 | deleteFindMax t

 307 |   = case t of

 308 |       Bin _ k x l Tip => (k :=> x,l)

 309 |       Bin _ k x l r   => let (km,r') = deleteFindMax r in (km,balance k x l r')

 310 |       Tip             => (error "DMap.deleteFindMax: can not return the maximal element of an empty map", Tip)

 320 | deleteFindMin : DMap k f -> (DSum k f, DMap k f)

 321 | deleteFindMin t = case minViewWithKey t of

 322 |   Nothing => (error "DMap.deleteFindMin: can not return the minimal element of an empty map", Tip)

 323 |   Just p => p

 330 | glue : DMap k f -> DMap k f -> DMap k f

 331 | glue Tip r = r

 332 | glue l Tip = l

 333 | glue l r =

 334 |   if size l > size r then case deleteFindMax l of (km :=> m, l') => balance km m l' r

 335 |                      else case deleteFindMin r of (km :=> m, r') => balance km m l r'

 341 | merge : DMap k f -> DMap k f -> DMap k f

 342 | merge Tip r   = r

 343 | merge l Tip   = l

 344 | merge l@(Bin sizeL kx x lx rx) r@(Bin sizeR ky y ly ry)

 345 |   =    if delta*sizeL <= sizeR then balance ky y (merge l ly) ry

 346 |   else if delta*sizeR <= sizeL then balance kx x lx (merge rx r)

 347 |   else                              glue l r

 373 | trim : (Some k -> Ordering) -> (Some k -> Ordering) -> DMap k f -> DMap k f

 374 | trim _     _     Tip = Tip

 375 | trim cmplo cmphi t@(Bin _ kx _ l r)

 376 |   = case cmplo (MkSome kx) of

 377 |       LT => case cmphi (MkSome kx) of

 378 |               GT => t

 379 |               _  => trim cmplo cmphi l

 380 |       _  => trim cmplo cmphi r

 383 | trimLookupLo : DOrd k => Some k -> (Some k -> Ordering) -> DMap k f -> (Maybe (DSum k f), DMap k f)

 384 | trimLookupLo _  _     Tip = (Nothing,Tip)

 385 | trimLookupLo lo cmphi t@(Bin _ kx x l r)

 386 |   = case compare lo (MkSome kx) of

 387 |       LT => case cmphi (MkSome kx) of

 388 |               GT => (lookupAssoc lo t, t)

 389 |               _  => trimLookupLo lo cmphi l

 390 |       GT => trimLookupLo lo cmphi r

 391 |       EQ => (Just (kx :=> x), trim (compare lo) cmphi r)

 398 | filterGt : DOrd k => (Some k -> Ordering) -> DMap k f -> DMap k f

 399 | filterGt cmp = go

 400 |   where

 401 |     go : DMap k f -> DMap k f

 402 |     go Tip              = Tip

 403 |     go (Bin _ kx x l r) = case cmp (MkSome kx) of

 404 |               LT => combine kx x (go l) r

 405 |               GT => go r

 406 |               EQ => r

 409 | filterLt : DOrd k => (Some k -> Ordering) -> DMap k f -> DMap k f

 410 | filterLt cmp = go

 411 |   where

 412 |     go : DMap k f -> DMap k f

 413 |     go Tip              = Tip

 414 |     go (Bin _ kx x l r) = case cmp (MkSome kx) of

 415 |           LT => go l

 416 |           GT => combine kx x l (go r)

 417 |           EQ => l

 431 | member : DOrd k => k a -> DMap k f -> Bool

 432 | member k = isJust . lookup k

 436 | notMember : DOrd k => k v -> DMap k f -> Bool

 437 | notMember k m = not (member k m)

 443 | find : DOrd k => k v -> DMap k f -> f v

 444 | find k m = case lookup k m of

 445 |     Nothing => error "DMap.find: element not in the map"

 446 |     Just v  => v

 452 | findWithDefault : DOrd k => f v -> k v -> DMap k f -> f v

 453 | findWithDefault def k m = case lookup k m of

 454 |     Nothing => def

 455 |     Just v  => v

 466 | insert : (impl : DOrd k) => k v -> f v -> DMap k f -> DMap k f

 467 | insert kx x = evalState False . go

 468 |   where

 469 |     go : DMap k f -> State Bool (DMap k f)

 470 |     go Tip = put True >> pure (singleton kx x)

 471 |     go t@(Bin sz ky y l r) = case dcompare kx ky @{impl} of

 472 |       DLT => do

 473 |         l' <- go l

 474 |         sizeChange <- get

 475 |         -- originally pointer equality was used to see if the tree was modified

 476 |         if sizeChange then pure (balance ky y l' r)

 477 |                       else pure (Bin sz ky y l' r)

 478 |       DGT => do

 479 |         r' <- go r

 480 |         sizeChange <- get

 481 |         -- as above

 482 |         if sizeChange then pure (balance ky y l r')

 483 |                       else pure (Bin sz ky y l r')

 484 |       DEQ => pure (Bin sz kx x l r)

 490 | insertR : (impl : DOrd k) => k v -> f v -> DMap k f -> DMap k f

 491 | insertR kx x = go

 492 |     where

 493 |         go : DMap k f -> DMap k f

 494 |         go Tip = singleton kx x

 495 |         go (Bin sz ky y l r) = case dcompare kx ky @{impl} of

 496 |             DLT => let l' = go l

 497 |                    -- pointer equality used before on trees

 498 |                    in if size l' == size l

 499 |                       then Bin sz ky y l' r

 500 |                       else balance ky y l' r

 501 |             DGT => let r' = go r

 502 |                    -- as above

 503 |                    in if size r' == size r

 504 |                    then Bin sz ky y l r'

 505 |                    else balance ky y l r'

 506 |             DEQ => Bin sz ky y l r

 515 | insertWithKey : (impl : DOrd k) => (k v -> f v -> f v -> f v) -> k v -> f v -> DMap k f -> DMap k f

 516 | insertWithKey func kx x = go

 517 |   where

 518 |     go : DMap k f -> DMap k f

 519 |     go Tip = singleton kx x

 520 |     go (Bin sy ky y l r) =

 521 |         case dcompare kx ky @{impl} of

 522 |             DLT => balance ky y (go l) r

 523 |             DGT => balance ky y l (go r)

 524 |             DEQ => Bin sy kx (func kx x y) l r

 532 | insertWith : DOrd k => (f v -> f v -> f v) -> k v -> f v -> DMap k f -> DMap k f

 533 | insertWith f = insertWithKey (\_ => \x' => \y' => f x' y')

 539 | insertLookupWithKey : (impl : DOrd k)

 540 |                    => (k v -> f v -> f v -> f v)

 541 |                    -> k v

 542 |                    -> f v

 543 |                    -> DMap k f

 544 |                    -> (Maybe (f v), DMap k f)

 545 | insertLookupWithKey func kx x = go

 546 |   where

 547 |     go : DMap k f -> (Maybe (f v), DMap k f)

 548 |     go Tip = (Nothing, singleton kx x)

 549 |     go (Bin sy ky y l r) =

 550 |         case dcompare kx ky @{impl} of

 551 |             DLT => let (found, l') = go l

 552 |                   in (found, balance ky y l' r)

 553 |             DGT => let (found, r') = go r

 554 |                   in (found, balance ky y l r')

 555 |             DEQ => (Just y, Bin sy kx (func kx x y) l r)

 566 | delete : (impl : DOrd k) => k v -> DMap k f -> DMap k f

 567 | delete k' = go

 568 |   where

 569 |     go : DMap k f -> DMap k f

 570 |     go Tip = Tip

 571 |     go (Bin _ kx x l r) =

 572 |         case dcompare k' kx @{impl} of

 573 |             DLT => balance kx x (go l) r

 574 |             DGT => balance kx x l (go r)

 575 |             DEQ => glue l r

 579 | adjustWithKey : (impl : DOrd k) => (k v -> f v -> f v) -> k v -> DMap k f -> DMap k f

 580 | adjustWithKey f0 k0 = go f0 k0

 581 |   where

 582 |     go : (k v -> f v -> f v) -> k v -> DMap k f -> DMap k f

 583 |     go f k Tip = Tip

 584 |     go f k (Bin sx kx x l r) =

 585 |       case dcompare k kx @{impl} of

 586 |         DLT => Bin sx kx x (go f k l) r

 587 |         DGT => Bin sx kx x l (go f k r)

 588 |         DEQ => Bin sx kx (f kx x) l r

 593 | adjust : DOrd k => (f v -> f v) -> k v -> DMap k f -> DMap k f

 594 | adjust f = adjustWithKey (\_ => \x => f x)

 601 | updateWithKey : (impl : DOrd k) => (k v -> f v -> Maybe (f v)) -> k v -> DMap k f -> DMap k f

 602 | updateWithKey func key = go

 603 |   where

 604 |     go : DMap k f -> DMap k f

 605 |     go Tip = Tip

 606 |     go (Bin sx kx x l r) =

 607 |         case dcompare key kx @{impl} of

 608 |            DLT => balance kx x (go l) r

 609 |            DGT => balance kx x l (go r)

 610 |            DEQ => case func kx x of

 611 |                    Just x' => Bin sx kx x' l r

 612 |                    Nothing => glue l r

 618 | update : DOrd k => (f v -> Maybe (f v)) -> k v -> DMap k f -> DMap k f

 619 | update f = updateWithKey (\_ => \x => f x)

 625 | updateLookupWithKey : (impl : DOrd k) => (k v -> f v -> Maybe (f v)) -> k v -> DMap k f -> (Maybe (f v), DMap k f)

 626 | updateLookupWithKey func key = go

 627 |  where

 628 |    go : DMap k f -> (Maybe (f v), DMap k f)

 629 |    go Tip = (Nothing,Tip)

 630 |    go (Bin sx kx x l r) =

 631 |           case dcompare key kx @{impl} of

 632 |                DLT => let (found,l') = go l in (found,balance kx x l' r)

 633 |                DGT => let (found,r') = go r in (found,balance kx x l r')

 634 |                DEQ => case func kx x of

 635 |                        Just x' => (Just x',Bin sx kx x' l r)

 636 |                        Nothing => (Just x,glue l r)

 642 | alter : (impl : DOrd k) => (Maybe (f v) -> Maybe (f v)) -> k v -> DMap k f -> DMap k f

 643 | alter func key = go

 644 |   where

 645 |     go : DMap k f -> DMap k f

 646 |     go Tip = case func Nothing of

 647 |                Nothing => Tip

 648 |                Just x  => singleton key x

 650 |     go (Bin sx kx x l r) = case dcompare key kx @{impl} of

 651 |                DLT => balance kx x (go l) r

 652 |                DGT => balance kx x l (go r)

 653 |                DEQ => case func (Just x) of

 654 |                        Just x' => Bin sx kx x' l r

 655 |                        Nothing => glue l r

 660 | alterF : (impl : DOrd k) => Functor f => k v -> (Maybe (g v) -> f (Maybe (g v))) -> DMap k g -> f (DMap k g)

 661 | alterF key func = go

 662 |   where

 663 |     go : DMap k g -> f (DMap k g)

 664 |     go Tip = maybe Tip (singleton key) <$> func Nothing

 666 |     go (Bin sx kx x l r) = case dcompare key kx @{impl} of

 667 |       DLT => (\l' => balance kx x l' r) <$> go l

 668 |       DGT => (\r' => balance kx x l r') <$> go r

 669 |       DEQ => maybe (glue l r) (\x' => Bin sx kx x' l r) <$> func (Just x)

 678 | lookupIndex : (impl : DOrd k) => k v -> DMap k f -> Maybe Int

 679 | lookupIndex key = go 0

 680 |   where

 681 |     go : Int -> DMap k f -> Maybe Int

 682 |     go idx Tip  = Nothing

 683 |     go idx (Bin _ kx _ l r)

 684 |       = case dcompare key kx @{impl} of

 685 |           DLT => go idx l

 686 |           DGT => go (idx + size l + 1) r

 687 |           DEQ => Just (idx + size l)

 693 | findIndex : DOrd k => k v -> DMap k f -> Int

 694 | findIndex k t

 695 |   = case lookupIndex k t of

 696 |       Nothing  => error "DMap.findIndex: element is not in the map"

 697 |       Just idx => idx

 702 | elemAt : Int -> DMap k f -> DSum k f

 703 | elemAt _ Tip = error "DMap.elemAt: index out of range"

 704 | elemAt i (Bin _ kx x l r)

 705 |   = case compare i sizeL of

 706 |       LT => elemAt i l

 707 |       GT => elemAt (i - sizeL - 1) r

 708 |       EQ => kx :=> x

 709 |   where

 710 |     sizeL : Int

 711 |     sizeL = size l

 716 | updateAt : ({0 v : a} -> k v -> f v -> Maybe (f v)) -> Int -> DMap k f -> DMap k f

 717 | updateAt func i0 t = go i0 t

 718 |  where

 719 |     go : Int -> DMap k f -> DMap k f

 720 |     go _ Tip  = Tip

 721 |     go i (Bin sx kx x l r) = case compare i sizeL of

 722 |       LT => balance kx x (go i l) r

 723 |       GT => balance kx x l (go (i-sizeL-1) r)

 724 |       EQ => case func kx x of

 725 |               Just x' => Bin sx kx x' l r

 726 |               Nothing => glue l r

 727 |       where

 728 |         sizeL : Int

 729 |         sizeL = size l

 734 | deleteAt : Int -> DMap k f -> DMap k f

 735 | deleteAt i m

 736 |   = updateAt (\_ => \_ => Nothing) i m

 743 | lookupMin : DMap k f -> Maybe (DSum k f)

 744 | lookupMin m = case m of

 745 |       Tip => Nothing

 746 |       Bin _ kx x l _ => Just $ go kx x l

 747 |   where

 748 |     go : k v -> f v -> DMap k f -> DSum k f

 749 |     go kx x Tip = kx :=> x

 750 |     go _  _ (Bin _ kx x l _) = go kx x l

 754 | findMin : DMap k f -> DSum k f

 755 | findMin m = case lookupMin m of

 756 |   Just x => x

 757 |   Nothing => error "DMap.findMin: empty map has no minimal element"

 760 | lookupMax : DMap k f -> Maybe (DSum k f)

 761 | lookupMax m = case m of

 762 |       Tip => Nothing

 763 |       Bin _ kx x _ r => Just $ go kx x r

 764 |   where

 765 |     go : k v -> f v -> DMap k f -> DSum k f

 766 |     go kx x Tip = kx :=> x

 767 |     go _  _ (Bin _ kx x _ r) = go kx x r

 771 | findMax : DMap k f -> DSum k f

 772 | findMax m = case lookupMax m of

 773 |   Just x => x

 774 |   Nothing => error "DMap.findMax: empty map has no maximal element"

 778 | deleteMin : DMap k f -> DMap k f

 779 | deleteMin (Bin _ _  _ Tip r)  = r

 780 | deleteMin (Bin _ kx x l r)    = balance kx x (deleteMin l) r

 781 | deleteMin Tip                 = Tip

 785 | deleteMax : DMap k f -> DMap k f

 786 | deleteMax (Bin _ _  _ l Tip)  = l

 787 | deleteMax (Bin _ kx x l r)    = balance kx x l (deleteMax r)

 788 | deleteMax Tip                 = Tip

 792 | updateMinWithKey : ({0 v : a} -> k v -> f v -> Maybe (f v)) -> DMap k f -> DMap k f

 793 | updateMinWithKey func = go

 794 |  where

 795 |   go : DMap k f -> DMap k f

 796 |   go (Bin sx kx x Tip r) = case func kx x of

 797 |                             Nothing => r

 798 |                             Just x' => Bin sx kx x' Tip r

 799 |   go (Bin _ kx x l r)    = balance kx x (go l) r

 800 |   go Tip                 = Tip

 804 | updateMaxWithKey : ({0 v : a} -> k v -> f v -> Maybe (f v)) -> DMap k f -> DMap k f

 805 | updateMaxWithKey func = go

 806 |  where

 807 |   go : DMap k f -> DMap k f

 808 |   go (Bin sx kx x l Tip) = case func kx x of

 809 |                             Nothing => l

 810 |                             Just x' => Bin sx kx x' l Tip

 811 |   go (Bin _ kx x l r)    = balance kx x l (go r)

 812 |   go Tip                 = Tip

 822 | split : (impl : DOrd k) => k v -> DMap k f -> (DMap k f, DMap k f)

 823 | split key = go

 824 |   where

 825 |     go : DMap k f -> (DMap k f, DMap k f)

 826 |     go Tip              = (Tip, Tip)

 827 |     go (Bin _ kx x l r) = case dcompare key kx @{impl} of

 828 |           DLT => let (lt, gt) = go l in (lt, combine kx x gt r)

 829 |           DGT => let (lt, gt) = go r in (combine kx x l lt, gt)

 830 |           DEQ => (l, r)

 835 | splitLookup : (impl : DOrd k) => k v -> DMap k f -> (DMap k f, Maybe (f v), DMap k f)

 836 | splitLookup key = go

 837 |   where

 838 |     go : DMap k f -> (DMap k f, Maybe (f v), DMap k f)

 839 |     go Tip              = (Tip, Nothing, Tip)

 840 |     go (Bin _ kx x l r) = case dcompare key kx @{impl} of

 841 |       DLT => let (lt, z, gt) = go l in (lt, z, combine kx x gt r)

 842 |       DGT => let (lt, z, gt) = go r in (combine kx x l lt, z, gt)

 843 |       DEQ => (l, Just x, r)

 848 | splitMember : (impl : DOrd k) => k v -> DMap k f -> (DMap k f, Bool, DMap k f)

 849 | splitMember key = go

 850 |   where

 851 |     go : DMap k f -> (DMap k f, Bool, DMap k f)

 852 |     go Tip              = (Tip, False, Tip)

 853 |     go (Bin _ kx x l r) = case dcompare key kx @{impl} of

 854 |       DLT => let (lt, z, gt) = go l in (lt, z, combine kx x gt r)

 855 |       DGT => let (lt, z, gt) = go r in (combine kx x l lt, z, gt)

 856 |       DEQ => (l, True, r)

 860 | splitLookupWithKey : (impl : DOrd k) => k v -> DMap k f -> (DMap k f, Maybe (k v, f v), DMap k f)

 861 | splitLookupWithKey key = go

 862 |   where

 863 |     go : DMap k f -> (DMap k f, Maybe (k v, f v), DMap k f)

 864 |     go Tip              = (Tip, Nothing, Tip)

 865 |     go (Bin _ kx x l r) = case dcompare key kx @{impl} of

 866 |       DLT => let (lt, z, gt) = go l in (lt, z, combine kx x gt r)

 867 |       DGT => let (lt, z, gt) = go r in (combine kx x l lt, z, gt)

 868 |       DEQ => (l, Just (kx, x), r)

 879 | union : DOrd k => DMap k f -> DMap k f -> DMap k f

 880 | union t1 Tip  = t1

 881 | union t1 (Bin _ kx x Tip Tip) = insertR kx x t1

 882 | union Tip t2  = t2

 883 | union (Bin _ kx x Tip Tip) t2 = insert kx x t2

 884 | union t1@(Bin _ k1 x1 l1 r1) t2 = case split k1 t2 of

 885 |   (l2, r2) => combine k1 x1 (l1 `union` l2) (r1 `union` r2)

 890 | unions : DOrd k => List (DMap k f) -> DMap k f

 891 | unions ts = foldl union empty ts

 898 | implementation (DOrd k) => Semigroup (DMap k f) where

 899 |   (<+>) = union

 902 | implementation (DOrd k) => Monoid (DMap k f) where

 903 |     neutral = empty

 912 | unionWithKey : DOrd k => ({0 v : a} -> k v -> f v -> f v -> f v) -> DMap k f -> DMap k f -> DMap k f

 913 | unionWithKey _ t1 Tip  = t1

 914 | unionWithKey _ Tip t2  = t2

 915 | unionWithKey f (Bin _ k1 x1 l1 r1) t2 = case splitLookup k1 t2 of

 916 |   (l2, mx2, r2) => let

 917 |       l1l2 = unionWithKey f l1 l2

 918 |       r1r2 = unionWithKey f r1 r2

 919 |     in case mx2 of

 920 |       Nothing => combine k1 x1 l1l2 r1r2

 921 |       Just x2 => combine k1 (f k1 x1 x2) l1l2 r1r2

 926 | unionsWithKey : DOrd k => ({0 v : a} -> k v -> f v -> f v -> f v) -> List (DMap k f) -> DMap k f

 927 | unionsWithKey f ts = foldl (unionWithKey f) empty ts

 936 | difference : DOrd k => DMap k f -> DMap k g -> DMap k f

 937 | difference Tip _   = Tip

 938 | difference t1 Tip  = t1

 939 | difference t1 (Bin _ k2 x2 l2 r2) = case split k2 t1 of

 940 |   (l1, r1) => let

 941 |       l1l2 = l1 `difference` l2

 942 |       r1r2 = r1 `difference` r2

 943 |     in if size t1 == size l1l2 + size r1r2 then t1

 944 |                                            else merge l1l2 r1r2

 951 | differenceWithKey : (impl : DOrd k)

 952 |                  => ({0 v : a} -> k v -> f v -> g v -> Maybe (f v))

 953 |                  -> DMap k f

 954 |                  -> DMap k g

 955 |                  -> DMap k f

 956 | differenceWithKey _ Tip _   = Tip

 957 | differenceWithKey _ t1 Tip  = t1

 958 | differenceWithKey f (Bin _ k1 x1 l1 r1) t2 = case splitLookup k1 t2 of

 959 |   (l2, mx2, r2) => let

 960 |       l1l2 = differenceWithKey f l1 l2

 961 |       r1r2 = differenceWithKey f r1 r2

 962 |     in case mx2 of

 963 |       Nothing => combine k1 x1 l1l2 r1r2

 964 |       Just x2 => case f k1 x1 x2 of

 965 |         Nothing   => merge l1l2 r1r2

 966 |         Just x1x2 => combine k1 x1x2 l1l2 r1r2

 977 | intersection : DOrd k => DMap k f -> DMap k f -> DMap k f

 978 | intersection Tip _ = Tip

 979 | intersection _ Tip = Tip

 980 | intersection t1@(Bin s1 k1 x1 l1 r1) t2 =

 981 |   let (l2, found, r2) = splitMember k1 t2

 982 |       l1l2 = intersection l1 l2

 983 |       r1r2 = intersection r1 r2

 984 |   in if found

 985 |      then if size l1l2 == size l1 && size r1r2 == size r1

 986 |           then t1

 987 |           else combine k1 x1 l1l2 r1r2

 988 |      else merge l1l2 r1r2

 993 | intersectionWithKey : DOrd k => ({0 v : a} -> k v -> f v -> g v -> h v) -> DMap k f -> DMap k g -> DMap k h

 994 | intersectionWithKey _ Tip _ = Tip

 995 | intersectionWithKey _ _ Tip = Tip

 996 | intersectionWithKey f (Bin s1 k1 x1 l1 r1) t2 =

 997 |   let (l2, found, r2) = splitLookup k1 t2

 998 |       l1l2 = intersectionWithKey f l1 l2

 999 |       r1r2 = intersectionWithKey f r1 r2

1000 |   in case found of

1001 |        Nothing => merge l1l2 r1r2

1002 |        Just x2 => combine k1 (f k1 x1 x2) l1l2 r1r2

1008 | submap' : DOrd k => ({0 v : a} -> k v -> k v -> f v -> g v -> Bool) -> DMap k f -> DMap k g -> Bool

1009 | submap' _ Tip _ = True

1010 | submap' _ _ Tip = False

1011 | submap' f (Bin _ kx x l r) t

1012 |   = let

1013 |       (lt, found, gt) = splitLookupWithKey kx t

1014 |     in case found of

1015 |       Nothing => False

1016 |       Just (ky, y) => f kx ky x y && submap' f l lt && submap' f r gt

1023 | isSubmapOfBy : DOrd k => ({0 v : a} -> k v -> k v -> f v -> g v -> Bool) -> DMap k f -> DMap k g -> Bool

1024 | isSubmapOfBy f t1 t2 = (size t1 <= size t2) && (submap' f t1 t2)

1044 | isProperSubmapOfBy : DOrd k => ({0 v : a} -> k v -> k v -> f v -> g v -> Bool) -> DMap k f -> DMap k g -> Bool