module Data.IntMap -- Hand specialised map, for efficiency... %default covering Key : TypeKey = Int -- TODO: write split privatedata Tree : Nat -> Type -> Type where  Leaf : Key -> v -> Tree Z v  Branch2 : Tree n v -> Key -> Tree n v -> Tree (S n) v  Branch3 : Tree n v -> Key -> Tree n v -> Key -> Tree n v -> Tree (S n) v branch4 :  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v ->  Tree (S (S n)) vbranch4 a b c d e f g =  Branch2 (Branch2 a b c) d (Branch2 e f g) branch5 :  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v ->  Tree (S (S n)) vbranch5 a b c d e f g h i =  Branch2 (Branch2 a b c) d (Branch3 e f g h i) branch6 :  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v ->  Tree (S (S n)) vbranch6 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 v -> Key ->  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v -> Key ->  Tree n v ->  Tree (S (S n)) vbranch7 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 v -> Key -> Tree (S n) v -> Key -> Tree (S n) v -> Tree (S (S n)) vmerge1 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) v -> Key -> Tree n v -> Key -> Tree (S n) v -> Tree (S (S n)) vmerge2 (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) v -> Key -> Tree (S n) v -> Key -> Tree n v -> Tree (S (S n)) vmerge3 (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 : Key -> Tree n v -> 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' : Key -> v -> Tree n v -> Either (Tree n v) (Tree n v, Key, Tree n v)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 : Key -> v -> Tree n v -> Either (Tree n v) (Tree (S n) v)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 -> Type -> TypedelType Z v = ()delType (S n) v = Tree n v treeDelete : Key -> Tree n v -> Either (Tree n v) (delType n v)treeDelete k (Leaf k' v) =  if k == k' then    Right ()  else    Left (Leaf k' v)treeDelete {n=S Z} k (Branch2 t1 k' t2) =  if k <= k' then    case treeDelete k t1 of      Left t1' => Left (Branch2 t1' k' t2)      Right () => Right t2  else    case treeDelete k t2 of      Left t2' => Left (Branch2 t1 k' t2')      Right () => Right t1treeDelete {n=S Z} k (Branch3 t1 k1 t2 k2 t3) =  if k <= k1 then    case treeDelete 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 k t2 of      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)      Right () => Left (Branch2 t1 k1 t3)  else    case treeDelete k t3 of      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')      Right () => Left (Branch2 t1 k1 t2)treeDelete {n=S (S _)} k (Branch2 t1 k' t2) =  if k <= k' then    case treeDelete 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 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 {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =  if k <= k1 then    case treeDelete 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 k t2 of      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)      Right t2' => Left (merge2 t1 k1 t2' k2 t3)  else    case treeDelete k t3 of      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')      Right t3' => Left (merge3 t1 k1 t2 k2 t3') treeToList : Tree n v -> List (Key, v)treeToList = treeToList' []  where    treeToList' : List (Key, v) -> Tree n v -> List (Key, v)    treeToList' rest (Leaf k v) = (k, v) :: rest    treeToList' rest (Branch2 t1 _ t2)        = treeToList' (treeToList' rest t2) t1    treeToList' rest (Branch3 t1 _ t2 _ t3)        = treeToList' (treeToList' (treeToList' rest t3) t2) t1 exportdata IntMap : Type -> Type where  Empty : IntMap v  M : (n : Nat) -> Tree n v -> IntMap v exportempty : IntMap vempty = Empty exportlookup : Int -> IntMap v -> Maybe vlookup _ Empty = Nothinglookup k (M _ t) = treeLookup k t exportinsert : Int -> v -> IntMap v -> IntMap 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 : List (Int, v) -> IntMap v -> IntMap vinsertFrom = flip $ foldl $ flip $ uncurry insert exportdelete : Int -> IntMap v -> IntMap vdelete _ Empty = Emptydelete k (M Z t) =  case treeDelete k t of    Left t' => (M _ t')    Right () => Emptydelete k (M (S _) t) =  case treeDelete k t of    Left t' => (M _ t')    Right t' => (M _ t') exportfromList : List (Int, v) -> IntMap vfromList l = foldl (flip (uncurry insert)) empty l exporttoList : IntMap v -> List (Int, v)toList Empty = []toList (M _ t) = treeToList t ||| Gets the Keys of the map.exportkeys : IntMap v -> List Intkeys = map fst . toList ||| Gets the values of the map. Could contain duplicates.exportvalues : IntMap v -> List vvalues = map snd . toList treeMap : (a -> b) -> Tree n a -> Tree n btreeMap 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) exportimplementation Functor IntMap where  map _ Empty = Empty  map f (M n t) = M _ (treeMap 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) -> IntMap v -> IntMap v -> IntMap vmergeWith f x y = insertFrom inserted x where  inserted : List (Key, 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 => IntMap v -> IntMap v -> IntMap vmerge = mergeWith (<+>) ||| Left-biased merge, also keeps the ordering specified  by the left map.exportmergeLeft : IntMap v -> IntMap v -> IntMap vmergeLeft = mergeWith const -- 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 (IntMap v) where  (<+>) = merge export(Semigroup v) => Monoid (IntMap v) where  neutral = empty