git.iko.soy/Idris-dev
on master help sign in
Renamed Map and Set to SortedMap and SortedSet
d17df01Daniel Waterworth
lib/Data/Set.idrdeleted−25
compare with master
unifiedsplit
@@ -1,25 +0,0 @@
1−module Data.Set
2−
3−import Data.Map
4−
5−-- TODO: add intersection, union, difference
6−
7−data Set k = SetWrapper (Data.Map.Map k ())
8−
9−empty : Set k
10−empty = SetWrapper Data.Map.empty
11−
12−insert : Ord k => k -> Set k -> Set k
13−insert k (SetWrapper m) = SetWrapper (Data.Map.insert k () m)
14−
15−delete : Ord k => k -> Set k -> Set k
16−delete k (SetWrapper m) = SetWrapper (Data.Map.delete k m)
17−
18−contains : Ord k => k -> Set k -> Bool
19−contains k (SetWrapper m) = isJust (Data.Map.lookup k m)
20−
21−fromList : Ord k => List k -> Set k
22−fromList l = SetWrapper (Data.Map.fromList (map (\i => (i, ())) l))
23−
24−toList : Ord k => Set k -> List k
25−toList (SetWrapper m) = map (\(i, _) => i) (Data.Map.toList m)
lib/Data/Map.idr → lib/Data/SortedMap.idrrenamed+11−11
@@ -1,4 +1,4 @@
1−module Data.Map
1+module Data.SortedMap
2
2
3-- TODO: write merge and split
3-- TODO: write merge and split
4
4
@@ -189,25 +189,25 @@ treeToList (Leaf k v) = [(k, v)]
189treeToList (Branch2 t1 _ t2) = treeToList t1 ++ treeToList t2
189treeToList (Branch2 t1 _ t2) = treeToList t1 ++ treeToList t2
190treeToList (Branch3 t1 _ t2 _ t3) = treeToList t1 ++ treeToList t2 ++ treeToList t3
190treeToList (Branch3 t1 _ t2 _ t3) = treeToList t1 ++ treeToList t2 ++ treeToList t3
191
191
192−data Map : Type -> Type -> Type where
192+data SortedMap : Type -> Type -> Type where
193− Empty : Map k v
193+ Empty : SortedMap k v
194− M : (n:Nat) -> Tree n k v -> Map k v
194+ M : (n:Nat) -> Tree n k v -> SortedMap k v
195
195
196−empty : Map k v
196+empty : SortedMap k v
197empty = Empty
197empty = Empty
198
198
199−lookup : Ord k => k -> Map k v -> Maybe v
199+lookup : Ord k => k -> SortedMap k v -> Maybe v
200lookup _ Empty = Nothing
200lookup _ Empty = Nothing
201lookup k (M _ t) = treeLookup k t
201lookup k (M _ t) = treeLookup k t
202
202
203−insert : Ord k => k -> v -> Map k v -> Map k v
203+insert : Ord k => k -> v -> SortedMap k v -> SortedMap k v
204insert k v Empty = M O (Leaf k v)
204insert k v Empty = M O (Leaf k v)
205insert k v (M _ t) =
205insert k v (M _ t) =
206 case treeInsert k v t of
206 case treeInsert k v t of
207 Left t' => (M _ t')
207 Left t' => (M _ t')
208 Right t' => (M _ t')
208 Right t' => (M _ t')
209
209
210−delete : Ord k => k -> Map k v -> Map k v
210+delete : Ord k => k -> SortedMap k v -> SortedMap k v
211delete _ Empty = Empty
211delete _ Empty = Empty
212delete k (M O t) =
212delete k (M O t) =
213 case treeDelete k t of
213 case treeDelete k t of
@@ -218,10 +218,10 @@ delete k (M (S _) t) =
218 Left t' => (M _ t')
218 Left t' => (M _ t')
219 Right t' => (M _ t')
219 Right t' => (M _ t')
220
220
221−fromList : Ord k => List (k, v) -> Map k v
221+fromList : Ord k => List (k, v) -> SortedMap k v
222fromList l = foldl (flip (uncurry insert)) empty l
222fromList l = foldl (flip (uncurry insert)) empty l
223
223
224−toList : Ord k => Map k v -> List (k, v)
224+toList : Ord k => SortedMap k v -> List (k, v)
225toList Empty = []
225toList Empty = []
226toList (M _ t) = treeToList t
226toList (M _ t) = treeToList t
227
227
@@ -230,6 +230,6 @@ instance Functor (Tree n k) where
230 fmap f (Branch2 t1 k t2) = Branch2 (fmap f t1) k (fmap f t2)
230 fmap f (Branch2 t1 k t2) = Branch2 (fmap f t1) k (fmap f t2)
231 fmap f (Branch3 t1 k1 t2 k2 t3) = Branch3 (fmap f t1) k1 (fmap f t2) k2 (fmap f t3)
231 fmap f (Branch3 t1 k1 t2 k2 t3) = Branch3 (fmap f t1) k1 (fmap f t2) k2 (fmap f t3)
232
232
233−instance Functor (Map k) where
233+instance Functor (SortedMap k) where
234 fmap _ Empty = Empty
234 fmap _ Empty = Empty
235 fmap f (M _ t) = M _ (fmap f t)
235 fmap f (M _ t) = M _ (fmap f t)
lib/Data/SortedSet.idrnew file+25
@@ -0,0 +1,25 @@
1+module Data.SortedSet
2+
3+import Data.SortedMap
4+
5+-- TODO: add intersection, union, difference
6+
7+data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
8+
9+empty : SortedSet k
10+empty = SetWrapper Data.SortedMap.empty
11+
12+insert : Ord k => k -> SortedSet k -> SortedSet k
13+insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
14+
15+delete : Ord k => k -> SortedSet k -> SortedSet k
16+delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
17+
18+contains : Ord k => k -> SortedSet k -> Bool
19+contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
20+
21+fromList : Ord k => List k -> SortedSet k
22+fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
23+
24+toList : Ord k => SortedSet k -> List k
25+toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
lib/base.ipkg+2−2
@@ -21,8 +21,8 @@ modules = Builtins, Prelude, IO, System,
21
21
22 Language.Reflection,
22 Language.Reflection,
23
23
24− Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign, Data.Map,
24+ Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,
25− Data.Set,
25+ Data.SortedMap, Data.SortedSet,
26
26
27 Control.Monad.Identity, Control.Monad.State, Control.Category,
27 Control.Monad.Identity, Control.Monad.State, Control.Category,
28 Control.Arrow,
28 Control.Arrow,