d17df01 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Renamed Map and Set to SortedMap and SortedSet

commitd17df01328a06a8e69d969218f9a0245758c07b5 authorDaniel Waterworth <Da.Waterworth@gmail.com> dateSun 14 Apr 2013, 13:16 (14 years ago) parente287680

4 files changed+38−38

compare with master

unifiedsplit

lib/Data/Set.idr−25 lib/Data/Map.idr → lib/Data/SortedMap.idr+11−11 lib/Data/SortedSet.idr+25 lib/base.ipkg+2−2

lib/Data/Set.idrdeleted−25

@@ -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

33-- TODO: write merge and split

@@ -189,25 +189,25 @@ treeToList (Leaf k v) = [(k, v)]

189189treeToList (Branch2 t1 _ t2) = treeToList t1 ++ treeToList t2

190190treeToList (Branch3 t1 _ t2 _ t3) = treeToList t1 ++ treeToList t2 ++ treeToList t3

191191

192−data Map : Type -> Type -> Type where

193− Empty : Map k v

194− M : (n:Nat) -> Tree n k v -> Map k v

192+data SortedMap : Type -> Type -> Type where

193+ Empty : SortedMap k v

194+ M : (n:Nat) -> Tree n k v -> SortedMap k v

195195

196−empty : Map k v

196+empty : SortedMap k v

197197empty = Empty

198198

199−lookup : Ord k => k -> Map k v -> Maybe v

199+lookup : Ord k => k -> SortedMap k v -> Maybe v

200200lookup _ Empty = Nothing

201201lookup k (M _ t) = treeLookup k t

202202

203−insert : Ord k => k -> v -> Map k v -> Map k v

203+insert : Ord k => k -> v -> SortedMap k v -> SortedMap k v

204204insert k v Empty = M O (Leaf k v)

205205insert k v (M _ t) =

206206 case treeInsert k v t of

207207 Left t' => (M _ t')

208208 Right t' => (M _ t')

209209

210−delete : Ord k => k -> Map k v -> Map k v

210+delete : Ord k => k -> SortedMap k v -> SortedMap k v

211211delete _ Empty = Empty

212212delete k (M O t) =

213213 case treeDelete k t of

@@ -218,10 +218,10 @@ delete k (M (S _) t) =

218218 Left t' => (M _ t')

219219 Right t' => (M _ t')

220220

221−fromList : Ord k => List (k, v) -> Map k v

221+fromList : Ord k => List (k, v) -> SortedMap k v

222222fromList l = foldl (flip (uncurry insert)) empty l

223223

224−toList : Ord k => Map k v -> List (k, v)

224+toList : Ord k => SortedMap k v -> List (k, v)

225225toList Empty = []

226226toList (M _ t) = treeToList t

227227

@@ -230,6 +230,6 @@ instance Functor (Tree n k) where

230230 fmap f (Branch2 t1 k t2) = Branch2 (fmap f t1) k (fmap f t2)

231231 fmap f (Branch3 t1 k1 t2 k2 t3) = Branch3 (fmap f t1) k1 (fmap f t2) k2 (fmap f t3)

232232

233−instance Functor (Map k) where

233+instance Functor (SortedMap k) where

234234 fmap _ Empty = Empty

235235 fmap f (M _ t) = M _ (fmap f t)

lib/Data/SortedSet.idrnew file+25

@@ -0,0 +1,25 @@

1+module Data.SortedSet

3+import Data.SortedMap

5+-- TODO: add intersection, union, difference

7+data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())

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,

2121

2222 Language.Reflection,

2323

24− Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign, Data.Map,

25− Data.Set,

24+ Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,

25+ Data.SortedMap, Data.SortedSet,

2626

2727 Control.Monad.Identity, Control.Monad.State, Control.Category,

2828 Control.Arrow,