module Data.NameMap import Core.Name -- Hand specialised map, for efficiency... %default covering Key : TypeKey = Name -- 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 Show v => Show (Tree n v) where  show (Leaf k v) = "Leaf: " ++ show k ++ " -> " ++ show v ++ "\n"  show (Branch2 t1 k t2) = "Branch2: " ++ show t1 ++ "\n < " ++ show k ++ "\n" ++ show t2 ++ "\n"  show (Branch3 t1 k1 t2 k2 t3) = "Branch3: " ++ show t1 ++ "\n < " ++ show k1 ++ "\n" ++ show t2 ++ "\n < " ++ show k2 ++ "\n" ++ show t3 ++ "\n" 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 NameMap : Type -> Type where  Empty : NameMap v  M : (n : Nat) -> Tree n v -> NameMap v exportShow v => Show (NameMap v) where  show Empty = "Empty NameMap"  show (M n t) = "NameMap M(" ++ show n ++ "):\n" ++ show t exportempty : NameMap vempty = Empty exportlookup : Name -> NameMap v -> Maybe vlookup _ Empty = Nothinglookup k (M _ t) = treeLookup k t exportinsert : Name -> v -> NameMap v -> NameMap 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 (Name, v) -> NameMap v -> NameMap vinsertFrom = flip $ foldl $ flip $ uncurry insert exportdelete : Name -> NameMap v -> NameMap 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 (Name, v) -> NameMap vfromList l = foldl (flip (uncurry insert)) empty l exporttoList : NameMap v -> List (Name, v)toList Empty = []toList (M _ t) = treeToList t ||| Gets the Keys of the map.exportkeys : NameMap v -> List Namekeys = map fst . toList ||| Gets the values of the map. Could contain duplicates.exportvalues : NameMap 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 NameMap 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) -> NameMap v -> NameMap v -> NameMap 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 => NameMap v -> NameMap v -> NameMap vmerge = mergeWith (<+>) ||| Left-biased merge, also keeps the ordering specified  by the left map.exportmergeLeft : NameMap v -> NameMap v -> NameMap 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 (NameMap v) where  (<+>) = merge export(Semigroup v) => Monoid (NameMap v) where  neutral = empty