git.iko.soy/Idris-dev
on master help sign in
Guarantee coherence of Ord in SortedMap/Set
09a0a8dEdwin Brady
libs/contrib/Data/SortedMap.idr+64−53
compare with master
unifiedsplit
@@ -2,72 +2,73 @@ module Data.SortedMap
2
2
3-- TODO: write merge and split
3-- TODO: write merge and split
4
4
5+private
5−data Tree : Nat -> Type -> Type -> Type where
6+data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where
6− Leaf : k -> v -> Tree Z k v
7+ Leaf : k -> v -> Tree Z k v o
7− Branch2 : Tree n k v -> k -> Tree n k v -> Tree (S n) k v
8+ Branch2 : Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o
8− Branch3 : Tree n k v -> k -> Tree n k v -> k -> Tree n k v -> Tree (S n) k v
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
9
10
10branch4 :
11branch4 :
11− Tree n k v -> k ->
12+ Tree n k v o -> k ->
12− Tree n k v -> k ->
13+ Tree n k v o -> k ->
13− Tree n k v -> k ->
14+ Tree n k v o -> k ->
14− Tree n k v ->
15+ Tree n k v o ->
15− Tree (S (S n)) k v
16+ Tree (S (S n)) k v o
16branch4 a b c d e f g =
17branch4 a b c d e f g =
17 Branch2 (Branch2 a b c) d (Branch2 e f g)
18 Branch2 (Branch2 a b c) d (Branch2 e f g)
18
19
19branch5 :
20branch5 :
20− Tree n k v -> k ->
21+ Tree n k v o -> k ->
21− Tree n k v -> k ->
22+ Tree n k v o -> k ->
22− Tree n k v -> k ->
23+ Tree n k v o -> k ->
23− Tree n k v -> k ->
24+ Tree n k v o -> k ->
24− Tree n k v ->
25+ Tree n k v o ->
25− Tree (S (S n)) k v
26+ Tree (S (S n)) k v o
26branch5 a b c d e f g h i =
27branch5 a b c d e f g h i =
27 Branch2 (Branch2 a b c) d (Branch3 e f g h i)
28 Branch2 (Branch2 a b c) d (Branch3 e f g h i)
28
29
29branch6 :
30branch6 :
30− Tree n k v -> k ->
31+ Tree n k v o -> k ->
31− Tree n k v -> k ->
32+ Tree n k v o -> k ->
32− Tree n k v -> k ->
33+ Tree n k v o -> k ->
33− Tree n k v -> k ->
34+ Tree n k v o -> k ->
34− Tree n k v -> k ->
35+ Tree n k v o -> k ->
35− Tree n k v ->
36+ Tree n k v o ->
36− Tree (S (S n)) k v
37+ Tree (S (S n)) k v o
37branch6 a b c d e f g h i j k =
38branch6 a b c d e f g h i j k =
38 Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)
39 Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)
39
40
40branch7 :
41branch7 :
41− Tree n k v -> k ->
42+ Tree n k v o -> k ->
42− Tree n k v -> k ->
43+ Tree n k v o -> k ->
43− Tree n k v -> k ->
44+ Tree n k v o -> k ->
44− Tree n k v -> k ->
45+ Tree n k v o -> k ->
45− Tree n k v -> k ->
46+ Tree n k v o -> k ->
46− Tree n k v -> k ->
47+ Tree n k v o -> k ->
47− Tree n k v ->
48+ Tree n k v o ->
48− Tree (S (S n)) k v
49+ Tree (S (S n)) k v o
49branch7 a b c d e f g h i j k l m =
50branch7 a b c d e f g h i j k l m =
50 Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)
51 Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)
51
52
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
53merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
54merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
54merge1 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
55merge1 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
55merge1 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
56merge1 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
56merge1 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
57merge1 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
57
58
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
59merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
60merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
60merge2 (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
61merge2 (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
61merge2 (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
62merge2 (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
62merge2 (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
63merge2 (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
63
64
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
65merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
66merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
66merge3 (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
67merge3 (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
67merge3 (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
68merge3 (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
68merge3 (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
69merge3 (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
69
70
70−treeLookup : Ord k => k -> Tree n k v -> Maybe v
71+treeLookup : k -> Tree n k v o -> Maybe v
71treeLookup k (Leaf k' v) =
72treeLookup k (Leaf k' v) =
72 if k == k' then
73 if k == k' then
73 Just v
74 Just v
@@ -86,7 +87,7 @@ treeLookup k (Branch3 t1 k1 t2 k2 t3) =
86 else
87 else
87 treeLookup k t3
88 treeLookup k t3
88
89
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)
90treeInsert' k v (Leaf k' v') =
91treeInsert' k v (Leaf k' v') =
91 case compare k k' of
92 case compare k k' of
92 LT => Right (Leaf k v, k, Leaf k' v')
93 LT => Right (Leaf k v, k, Leaf k' v')
@@ -116,17 +117,17 @@ treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
116 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
117 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
117 Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)
118 Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)
118
119
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)
120treeInsert k v t =
121treeInsert k v t =
121 case treeInsert' k v t of
122 case treeInsert' k v t of
122 Left t' => Left t'
123 Left t' => Left t'
123 Right (a, b, c) => Right (Branch2 a b c)
124 Right (a, b, c) => Right (Branch2 a b c)
124
125
125−delType : Nat -> Type -> Type -> Type
126+delType : Nat -> (k : Type) -> Type -> Ord k -> Type
126−delType Z k v = ()
127+delType Z k v o = ()
127−delType (S n) k v = Tree n k v
128+delType (S n) k v o = Tree n k v o
128
129
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)
130treeDelete k (Leaf k' v) =
131treeDelete k (Leaf k' v) =
131 if k == k' then
132 if k == k' then
132 Right ()
133 Right ()
@@ -183,33 +184,38 @@ treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =
183 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
184 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
184 Right t3' => Left (merge3 t1 k1 t2 k2 t3')
185 Right t3' => Left (merge3 t1 k1 t2 k2 t3')
185
186
186−treeToList : Tree n k v -> List (k, v)
187+treeToList : Tree n k v o -> List (k, v)
187treeToList = treeToList' (:: [])
188treeToList = treeToList' (:: [])
188 where
189 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)
190 treeToList' cont (Leaf k v) = cont (k, v)
191 treeToList' cont (Leaf k v) = cont (k, v)
191 treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
192 treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
192 treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
193 treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
193
194
195+abstract
194data SortedMap : Type -> Type -> Type where
196data SortedMap : Type -> Type -> Type where
195− Empty : SortedMap k v
197+ Empty : Ord k => SortedMap k v
196− M : (n:Nat) -> Tree n k v -> SortedMap k v
198+ M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v
197
199
200+public
198−empty : SortedMap k v
201+empty : Ord k => SortedMap k v
199empty = Empty
202empty = Empty
200
203
204+public
201−lookup : Ord k => k -> SortedMap k v -> Maybe v
205+lookup : k -> SortedMap k v -> Maybe v
202lookup _ Empty = Nothing
206lookup _ Empty = Nothing
203lookup k (M _ t) = treeLookup k t
207lookup k (M _ t) = treeLookup k t
204
208
209+public
205−insert : Ord k => k -> v -> SortedMap k v -> SortedMap k v
210+insert : k -> v -> SortedMap k v -> SortedMap k v
206insert k v Empty = M Z (Leaf k v)
211insert k v Empty = M Z (Leaf k v)
207insert k v (M _ t) =
212insert k v (M _ t) =
208 case treeInsert k v t of
213 case treeInsert k v t of
209 Left t' => (M _ t')
214 Left t' => (M _ t')
210 Right t' => (M _ t')
215 Right t' => (M _ t')
211
216
217+public
212−delete : Ord k => k -> SortedMap k v -> SortedMap k v
218+delete : k -> SortedMap k v -> SortedMap k v
213delete _ Empty = Empty
219delete _ Empty = Empty
214delete k (M Z t) =
220delete k (M Z t) =
215 case treeDelete k t of
221 case treeDelete k t of
@@ -220,18 +226,23 @@ delete k (M (S _) t) =
220 Left t' => (M _ t')
226 Left t' => (M _ t')
221 Right t' => (M _ t')
227 Right t' => (M _ t')
222
228
229+public
223fromList : Ord k => List (k, v) -> SortedMap k v
230fromList : Ord k => List (k, v) -> SortedMap k v
224fromList l = foldl (flip (uncurry insert)) empty l
231fromList l = foldl (flip (uncurry insert)) empty l
225
232
233+public
226toList : SortedMap k v -> List (k, v)
234toList : SortedMap k v -> List (k, v)
227toList Empty = []
235toList Empty = []
228toList (M _ t) = treeToList t
236toList (M _ t) = treeToList t
229
237
230−instance Functor (Tree n k) where
238+public
239+treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
231− map f (Leaf k v) = Leaf k (f v)
240+treeMap f (Leaf k v) = Leaf k (f v)
232− map f (Branch2 t1 k t2) = Branch2 (map f t1) k (map f t2)
241+treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
233− map f (Branch3 t1 k1 t2 k2 t3) = Branch3 (map f t1) k1 (map f t2) k2 (map f t3)
242+treeMap f (Branch3 t1 k1 t2 k2 t3)
243+ = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)
234
244
235instance Functor (SortedMap k) where
245instance Functor (SortedMap k) where
236 map _ Empty = Empty
246 map _ Empty = Empty
237− map f (M n t) = M _ (map f t)
247+ map f (M n t) = M _ (treeMap f t)
248+
libs/contrib/Data/SortedSet.idr+11−4
@@ -4,23 +4,30 @@ import Data.SortedMap
4
4
5-- TODO: add intersection, union, difference
5-- TODO: add intersection, union, difference
6
6
7+abstract
7data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
8data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
8
9
10+public
9−empty : SortedSet k
11+empty : Ord k => SortedSet k
10empty = SetWrapper Data.SortedMap.empty
12empty = SetWrapper Data.SortedMap.empty
11
13
14+public
12−insert : Ord k => k -> SortedSet k -> SortedSet k
15+insert : k -> SortedSet k -> SortedSet k
13insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
16insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
14
17
18+public
15−delete : Ord k => k -> SortedSet k -> SortedSet k
19+delete : k -> SortedSet k -> SortedSet k
16delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
20delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
17
21
22+public
18−contains : Ord k => k -> SortedSet k -> Bool
23+contains : k -> SortedSet k -> Bool
19contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
24contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
20
25
26+public
21fromList : Ord k => List k -> SortedSet k
27fromList : Ord k => List k -> SortedSet k
22fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
28fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
23
29
30+public
24toList : SortedSet k -> List k
31toList : SortedSet k -> List k
25toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
32toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
26
33