module Data.SortedMap -- TODO: write split privatedata Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where  Leaf : k -> v -> Tree Z k v o  Branch2 : Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o  Branch3 : Tree n k v o -> k -> Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o branch4 :  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o ->  Tree (S (S n)) k v obranch4 a b c d e f g =  Branch2 (Branch2 a b c) d (Branch2 e f g) branch5 :  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o ->  Tree (S (S n)) k v obranch5 a b c d e f g h i =  Branch2 (Branch2 a b c) d (Branch3 e f g h i) branch6 :  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o ->  Tree (S (S n)) k v obranch6 a b c d e f g h i j k =  Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k) branch7 :  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o -> k ->  Tree n k v o ->  Tree (S (S n)) k v obranch7 a b c d e f g h i j k l m =  Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m) merge1 : Tree n k v o -> k -> Tree (S n) k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v omerge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h imerge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j kmerge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j kmerge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m merge2 : Tree (S n) k v o -> k -> Tree n k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v omerge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h imerge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j kmerge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j kmerge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m merge3 : Tree (S n) k v o -> k -> Tree (S n) k v o -> k -> Tree n k v o -> Tree (S (S n)) k v omerge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h imerge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j kmerge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j kmerge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m treeLookup : Ord k => k -> Tree n k v o -> Maybe vtreeLookup k (Leaf k' v) =  if k == k' then    Just v  else    NothingtreeLookup k (Branch2 t1 k' t2) =  if k <= k' then    treeLookup k t1  else    treeLookup k t2treeLookup k (Branch3 t1 k1 t2 k2 t3) =  if k <= k1 then    treeLookup k t1  else if k <= k2 then    treeLookup k t2  else    treeLookup k t3 treeInsert' : Ord k => k -> v -> Tree n k v o -> Either (Tree n k v o) (Tree n k v o, k, Tree n k v o)treeInsert' k v (Leaf k' v') =  case compare k k' of    LT => Right (Leaf k v, k, Leaf k' v')    EQ => Left (Leaf k v)    GT => Right (Leaf k' v', k', Leaf k v)treeInsert' k v (Branch2 t1 k' t2) =  if k <= k' then    case treeInsert' k v t1 of      Left t1' => Left (Branch2 t1' k' t2)      Right (a, b, c) => Left (Branch3 a b c k' t2)  else    case treeInsert' k v t2 of      Left t2' => Left (Branch2 t1 k' t2')      Right (a, b, c) => Left (Branch3 t1 k' a b c)treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =  if k <= k1 then    case treeInsert' k v t1 of      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)      Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3)  else    if k <= k2 then      case treeInsert' k v t2 of        Left t2' => Left (Branch3 t1 k1 t2' k2 t3)        Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3)    else      case treeInsert' k v t3 of        Left t3' => Left (Branch3 t1 k1 t2 k2 t3')        Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c) treeInsert : Ord k => k -> v -> Tree n k v o -> Either (Tree n k v o) (Tree (S n) k v o)treeInsert k v t =  case treeInsert' k v t of    Left t' => Left t'    Right (a, b, c) => Right (Branch2 a b c) delType : Nat -> (k : Type) -> Type -> Ord k -> TypedelType Z k v o = ()delType (S n) k v o = Tree n k v o treeDelete : Ord k => (n : Nat) -> k -> Tree n k v o -> Either (Tree n k v o) (delType n k v o)treeDelete _ k (Leaf k' v) =  if k == k' then    Right ()  else    Left (Leaf k' v)treeDelete (S Z) k (Branch2 t1 k' t2) =  if k <= k' then    case treeDelete Z k t1 of      Left t1' => Left (Branch2 t1' k' t2)      Right () => Right t2  else    case treeDelete Z k t2 of      Left t2' => Left (Branch2 t1 k' t2')      Right () => Right t1treeDelete (S Z) k (Branch3 t1 k1 t2 k2 t3) =  if k <= k1 then    case treeDelete Z k t1 of      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)      Right () => Left (Branch2 t2 k2 t3)  else if k <= k2 then    case treeDelete Z k t2 of      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)      Right () => Left (Branch2 t1 k1 t3)  else    case treeDelete Z k t3 of      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')      Right () => Left (Branch2 t1 k1 t2)treeDelete (S (S n)) k (Branch2 t1 k' t2) =  if k <= k' then    case treeDelete (S n) k t1 of      Left t1' => Left (Branch2 t1' k' t2)      Right t1' =>        case t2 of          Branch2 a b c => Right (Branch3 t1' k' a b c)          Branch3 a b c d e => Left (branch4 t1' k' a b c d e)  else    case treeDelete (S n) k t2 of      Left t2' => Left (Branch2 t1 k' t2')      Right t2' =>        case t1 of          Branch2 a b c => Right (Branch3 a b c k' t2')          Branch3 a b c d e => Left (branch4 a b c d e k' t2')treeDelete (S (S n)) k (Branch3 t1 k1 t2 k2 t3) =  if k <= k1 then    case treeDelete (S n) k t1 of      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)      Right t1' => Left (merge1 t1' k1 t2 k2 t3)  else if k <= k2 then    case treeDelete (S n) k t2 of      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)      Right t2' => Left (merge2 t1 k1 t2' k2 t3)  else    case treeDelete (S n) k t3 of      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')      Right t3' => Left (merge3 t1 k1 t2 k2 t3') treeToList : Tree n k v o -> List (k, v)treeToList = treeToList' (:: [])  where    -- explicit quantification to avoid conflation with {n} from treeToList    treeToList' : {0 n : Nat} -> ((k, v) -> List (k, v)) -> Tree n k v o -> List (k, v)    treeToList' cont (Leaf k v) = cont (k, v)    treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1    treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1 exportdata SortedMap : Type -> Type -> Type where  Empty : Ord k => SortedMap k v  M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v exportempty : Ord k => SortedMap k vempty = Empty exportlookup : k -> SortedMap k v -> Maybe vlookup _ Empty = Nothinglookup k (M _ t) = treeLookup k t exportinsert : k -> v -> SortedMap k v -> SortedMap k vinsert k v Empty = M Z (Leaf k v)insert k v (M _ t) =  case treeInsert k v t of    Left t' => (M _ t')    Right t' => (M _ t') exportinsertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k vinsertFrom = flip $ foldl $ flip $ uncurry insert exportdelete : k -> SortedMap k v -> SortedMap k vdelete _ Empty = Emptydelete k (M Z t) =  case treeDelete Z k t of    Left t' => (M _ t')    Right () => Emptydelete k (M (S n) t) =  case treeDelete (S n) k t of    Left t' => (M _ t')    Right t' => (M _ t') exportfromList : Ord k => List (k, v) -> SortedMap k vfromList l = foldl (flip (uncurry insert)) empty l exporttoList : SortedMap k v -> List (k, v)toList Empty = []toList (M _ t) = treeToList t ||| Gets the keys of the map.exportkeys : SortedMap k v -> List kkeys = map fst . toList ||| Gets the values of the map. Could contain duplicates.exportvalues : SortedMap k v -> List vvalues = map snd . toList exportnull : SortedMap k v -> Boolnull Empty = Truenull (M _ _) = False treeMap : (a -> b) -> Tree n k a o -> Tree n k b otreeMap f (Leaf k v) = Leaf k (f v)treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)treeMap f (Branch3 t1 k1 t2 k2 t3)    = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3) treeTraverse : Applicative f => (a -> f b) -> Tree n k a o -> f (Tree n k b o)treeTraverse f (Leaf k v) = Leaf k <$> f vtreeTraverse f (Branch2 t1 k t2) =  Branch2    <$> treeTraverse f t1    <*> pure k    <*> treeTraverse f t2treeTraverse f (Branch3 t1 k1 t2 k2 t3) =  Branch3    <$> treeTraverse f t1    <*> pure k1    <*> treeTraverse f t2    <*> pure k2    <*> treeTraverse f t3 exportimplementation Functor (SortedMap k) where  map _ Empty = Empty  map f (M n t) = M _ (treeMap f t) exportimplementation Foldable (SortedMap k) where  foldr f z = foldr f z . values exportimplementation Traversable (SortedMap k) where  traverse _ Empty = pure Empty  traverse f (M n t) = M _ <$> treeTraverse f t ||| Merge two maps. When encountering duplicate keys, using a function to combine the values.||| Uses the ordering of the first map given.exportmergeWith : (v -> v -> v) -> SortedMap k v -> SortedMap k v -> SortedMap k vmergeWith f x y = insertFrom inserted x where  inserted : List (k, v)  inserted = do    (k, v) <- toList y    let v' = (maybe id f $ lookup k x) v    pure (k, v') ||| Merge two maps using the Semigroup (and by extension, Monoid) operation.||| Uses mergeWith internally, so the ordering of the left map is kept.exportmerge : Semigroup v => SortedMap k v -> SortedMap k v -> SortedMap k vmerge = mergeWith (<+>) ||| Left-biased merge, also keeps the ordering specified  by the left map.exportmergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k vmergeLeft = mergeWith const export(Show k, Show v) => Show (SortedMap k v) where   show m = "fromList " ++ (show $ toList m) -- TODO: is this the right variant of merge to use for this? I think it is, but-- I could also see the advantages of using `mergeLeft`. The current approach is-- strictly more powerful I believe, because `mergeLeft` can be emulated with-- the `First` monoid. However, this does require more code to do the same-- thing.exportSemigroup v => Semigroup (SortedMap k v) where  (<+>) = merge ||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.||| However, semantically, it should be equal.export(Ord k, Semigroup v) => Monoid (SortedMap k v) where  neutral = empty