@@ -2,72 +2,73 @@ module Data.SortedMap
22
33-- TODO: write merge and split
44
5−data Tree : Nat -> Type -> Type -> Type where
6− Leaf : k -> v -> Tree Z k v
7− Branch2 : Tree n k v -> k -> Tree n k v -> Tree (S n) k v
8− Branch3 : Tree n k v -> k -> Tree n k v -> k -> Tree n k v -> Tree (S n) k v
5+private
6+data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where
7+ Leaf : k -> v -> Tree Z k v o
8+ Branch2 : Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o
9+ Branch3 : Tree n k v o -> k -> Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o
910
1011branch4 :
11− Tree n k v -> k ->
12− Tree n k v -> k ->
13− Tree n k v -> k ->
14− Tree n k v ->
15− Tree (S (S n)) k v
12+ Tree n k v o -> k ->
13+ Tree n k v o -> k ->
14+ Tree n k v o -> k ->
15+ Tree n k v o ->
16+ Tree (S (S n)) k v o
1617branch4 a b c d e f g =
1718 Branch2 (Branch2 a b c) d (Branch2 e f g)
1819
1920branch5 :
20− Tree n k v -> k ->
21− Tree n k v -> k ->
22− Tree n k v -> k ->
23− Tree n k v -> k ->
24− Tree n k v ->
25− Tree (S (S n)) k v
21+ Tree n k v o -> k ->
22+ Tree n k v o -> k ->
23+ Tree n k v o -> k ->
24+ Tree n k v o -> k ->
25+ Tree n k v o ->
26+ Tree (S (S n)) k v o
2627branch5 a b c d e f g h i =
2728 Branch2 (Branch2 a b c) d (Branch3 e f g h i)
2829
2930branch6 :
30− Tree n k v -> k ->
31− Tree n k v -> k ->
32− Tree n k v -> k ->
33− Tree n k v -> k ->
34− Tree n k v -> k ->
35− Tree n k v ->
36− Tree (S (S n)) k v
31+ Tree n k v o -> k ->
32+ Tree n k v o -> k ->
33+ Tree n k v o -> k ->
34+ Tree n k v o -> k ->
35+ Tree n k v o -> k ->
36+ Tree n k v o ->
37+ Tree (S (S n)) k v o
3738branch6 a b c d e f g h i j k =
3839 Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)
3940
4041branch7 :
41− Tree n k v -> k ->
42− Tree n k v -> k ->
43− Tree n k v -> k ->
44− Tree n k v -> k ->
45− Tree n k v -> k ->
46− Tree n k v -> k ->
47− Tree n k v ->
48− Tree (S (S n)) k v
42+ Tree n k v o -> k ->
43+ Tree n k v o -> k ->
44+ Tree n k v o -> k ->
45+ Tree n k v o -> k ->
46+ Tree n k v o -> k ->
47+ Tree n k v o -> k ->
48+ Tree n k v o ->
49+ Tree (S (S n)) k v o
4950branch7 a b c d e f g h i j k l m =
5051 Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)
5152
52−merge1 : Tree n k v -> k -> Tree (S n) k v -> k -> Tree (S n) k v -> Tree (S (S n)) k v
53+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 o
5354merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
5455merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
5556merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k
5657merge1 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
5758
58−merge2 : Tree (S n) k v -> k -> Tree n k v -> k -> Tree (S n) k v -> Tree (S (S n)) k v
59+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 o
5960merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
6061merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
6162merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k
6263merge2 (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
6364
64−merge3 : Tree (S n) k v -> k -> Tree (S n) k v -> k -> Tree n k v -> Tree (S (S n)) k v
65+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 o
6566merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
6667merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k
6768merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k
6869merge3 (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
6970
70−treeLookup : Ord k => k -> Tree n k v -> Maybe v
71+treeLookup : k -> Tree n k v o -> Maybe v
7172treeLookup k (Leaf k' v) =
7273 if k == k' then
7374 Just v
@@ -86,7 +87,7 @@ treeLookup k (Branch3 t1 k1 t2 k2 t3) =
8687 else
8788 treeLookup k t3
8889
89−treeInsert' : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree n k v, k, Tree n k v)
90+treeInsert' : k -> v -> Tree n k v o -> Either (Tree n k v o) (Tree n k v o, k, Tree n k v o)
9091treeInsert' k v (Leaf k' v') =
9192 case compare k k' of
9293 LT => Right (Leaf k v, k, Leaf k' v')
@@ -116,17 +117,17 @@ treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
116117 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
117118 Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)
118119
119−treeInsert : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree (S n) k v)
120+treeInsert : k -> v -> Tree n k v o -> Either (Tree n k v o) (Tree (S n) k v o)
120121treeInsert k v t =
121122 case treeInsert' k v t of
122123 Left t' => Left t'
123124 Right (a, b, c) => Right (Branch2 a b c)
124125
125−delType : Nat -> Type -> Type -> Type
126−delType Z k v = ()
127−delType (S n) k v = Tree n k v
126+delType : Nat -> (k : Type) -> Type -> Ord k -> Type
127+delType Z k v o = ()
128+delType (S n) k v o = Tree n k v o
128129
129−treeDelete : Ord k => k -> Tree n k v -> Either (Tree n k v) (delType n k v)
130+treeDelete : k -> Tree n k v o -> Either (Tree n k v o) (delType n k v o)
130131treeDelete k (Leaf k' v) =
131132 if k == k' then
132133 Right ()
@@ -183,33 +184,38 @@ treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =
183184 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
184185 Right t3' => Left (merge3 t1 k1 t2 k2 t3')
185186
186−treeToList : Tree n k v -> List (k, v)
187+treeToList : Tree n k v o -> List (k, v)
187188treeToList = treeToList' (:: [])
188189 where
189− treeToList' : ((k, v) -> List (k, v)) -> Tree n k v -> List (k, v)
190+ treeToList' : ((k, v) -> List (k, v)) -> Tree n k v o -> List (k, v)
190191 treeToList' cont (Leaf k v) = cont (k, v)
191192 treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
192193 treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
193194
195+abstract
194196data SortedMap : Type -> Type -> Type where
195− Empty : SortedMap k v
196− M : (n:Nat) -> Tree n k v -> SortedMap k v
197+ Empty : Ord k => SortedMap k v
198+ M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v
197199
198−empty : SortedMap k v
200+public
201+empty : Ord k => SortedMap k v
199202empty = Empty
200203
201−lookup : Ord k => k -> SortedMap k v -> Maybe v
204+public
205+lookup : k -> SortedMap k v -> Maybe v
202206lookup _ Empty = Nothing
203207lookup k (M _ t) = treeLookup k t
204208
205−insert : Ord k => k -> v -> SortedMap k v -> SortedMap k v
209+public
210+insert : k -> v -> SortedMap k v -> SortedMap k v
206211insert k v Empty = M Z (Leaf k v)
207212insert k v (M _ t) =
208213 case treeInsert k v t of
209214 Left t' => (M _ t')
210215 Right t' => (M _ t')
211216
212−delete : Ord k => k -> SortedMap k v -> SortedMap k v
217+public
218+delete : k -> SortedMap k v -> SortedMap k v
213219delete _ Empty = Empty
214220delete k (M Z t) =
215221 case treeDelete k t of
@@ -220,18 +226,23 @@ delete k (M (S _) t) =
220226 Left t' => (M _ t')
221227 Right t' => (M _ t')
222228
229+public
223230fromList : Ord k => List (k, v) -> SortedMap k v
224231fromList l = foldl (flip (uncurry insert)) empty l
225232
233+public
226234toList : SortedMap k v -> List (k, v)
227235toList Empty = []
228236toList (M _ t) = treeToList t
229237
230−instance Functor (Tree n k) where
231− map f (Leaf k v) = Leaf k (f v)
232− map f (Branch2 t1 k t2) = Branch2 (map f t1) k (map f t2)
233− map f (Branch3 t1 k1 t2 k2 t3) = Branch3 (map f t1) k1 (map f t2) k2 (map f t3)
238+public
239+treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
240+treeMap f (Leaf k v) = Leaf k (f v)
241+treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
242+treeMap f (Branch3 t1 k1 t2 k2 t3)
243+ = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)
234244
235245instance Functor (SortedMap k) where
236246 map _ Empty = Empty
237− map f (M n t) = M _ (map f t)
247+ map f (M n t) = M _ (treeMap f t)
248+