git.iko.soy/Idris-dev
on master help sign in
Added more to prelude, specifically in the files either.idr and maybe.idr. Ported most of the (total functions from) the Haskell Prelude relating to these types, as well as commonly used auxilliary functions found in third-party libraries on Hackage.
34b88d6Dominic Mulligan
lib/prelude/either.idr+52−2
compare with master
unifiedsplit
@@ -2,12 +2,62 @@ module prelude.either
2
2
3import builtins
3import builtins
4
4
5+import prelude.maybe
6+import prelude.list
7+
5−data Either a b = Left a | Right b
8+data Either a b
9+ = Left a
10+ | Right b
11+
12+--------------------------------------------------------------------------------
13+-- Syntactic tests
14+--------------------------------------------------------------------------------
15+
16+isLeft : Either a b -> Bool
17+isLeft (Left l) = True
18+isLeft (Right r) = False
19+
20+isRight : Either a b -> Bool
21+isRight (Left l) = False
22+isRight (Right r) = True
23+
24+--------------------------------------------------------------------------------
25+-- Misc.
26+--------------------------------------------------------------------------------
6
27
7choose : (b : Bool) -> Either (so b) (so (not b))
28choose : (b : Bool) -> Either (so b) (so (not b))
8−choose True = Left oh
29+choose True = Left oh
9choose False = Right oh
30choose False = Right oh
10
31
11either : Either a b -> (a -> c) -> (b -> c) -> c
32either : Either a b -> (a -> c) -> (b -> c) -> c
12either (Left x) l r = l x
33either (Left x) l r = l x
13either (Right x) l r = r x
34either (Right x) l r = r x
35+
36+lefts : List (Either a b) -> List a
37+lefts [] = []
38+lefts (x::xs) =
39+ case x of
40+ Left l => l :: lefts xs
41+ Right r => lefts xs
42+
43+rights : List (Either a b) -> List b
44+rights [] = []
45+rights (x::xs) =
46+ case x of
47+ Left l => rights xs
48+ Right r => r :: rights xs
49+
50+partitionEithers : List (Either a b) -> (List a, List b)
51+partitionEithers l = (lefts l, rights l)
52+
53+fromEither : Either a a -> a
54+fromEither (Left l) = l
55+fromEither (Right r) = r
56+
57+--------------------------------------------------------------------------------
58+-- Conversions
59+--------------------------------------------------------------------------------
60+
61+maybeToEither : e -> Maybe a -> Either e a
62+maybeToEither def (Just j) = Right j
63+maybeToEither def Nothing = Left def
lib/prelude/maybe.idr+69−4
@@ -1,12 +1,77 @@
1module prelude.maybe
1module prelude.maybe
2
2
3+import builtins
4+import prelude.list
5+import prelude.monad
6+
3−data Maybe a = Nothing | Just a
7+data Maybe a
8+ = Nothing
9+ | Just a
10+
11+--------------------------------------------------------------------------------
12+-- Syntactic tests
13+--------------------------------------------------------------------------------
14+
15+isNothing : Maybe a -> Bool
16+isNothing Nothing = True
17+isNothing (Just j) = False
18+
19+isJust : Maybe a -> Bool
20+isJust Nothing = False
21+isJust (Just j) = True
22+
23+--------------------------------------------------------------------------------
24+-- Conversions
25+--------------------------------------------------------------------------------
26+
27+maybeToList : Maybe a -> List a
28+maybeToList Nothing = []
29+maybeToList (Just j) = [j]
30+
31+listToMaybe : List a -> Maybe a
32+listToMaybe [] = Nothing
33+listToMaybe (x::xs) = Just x
34+
35+--------------------------------------------------------------------------------
36+-- Misc
37+--------------------------------------------------------------------------------
4
38
5maybe : |(def : b) -> (a -> b) -> Maybe a -> b
39maybe : |(def : b) -> (a -> b) -> Maybe a -> b
6maybe n j Nothing = n
40maybe n j Nothing = n
7maybe n j (Just x) = j x
41maybe n j (Just x) = j x
8
42
9−maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b
43+fromMaybe : |(def: a) -> Maybe a -> a
10−maybe_bind Nothing k = Nothing
44+fromMaybe def Nothing = def
11−maybe_bind (Just x) k = k x
45+fromMaybe def (Just j) = j
46+
47+toMaybe : Bool -> a -> Maybe a
48+toMaybe True j = Just j
49+toMaybe False j = Nothing
50+
51+catMaybes : List (Maybe a) -> List a
52+catMaybes [] = []
53+catMaybes (x::xs) =
54+ case x of
55+ Left l => catMaybes xs
56+ Right r => r :: catMaybes xs
57+
58+mapMaybe : (a -> Maybe b) -> List a -> List b
59+mapMaybe f [] = []
60+mapMaybe f (x::xs) =
61+ case f x of
62+ Nothing => mapMaybe f xs
63+ Just j => j :: mapMaybe f xs
64+
65+--------------------------------------------------------------------------------
66+-- Class instances
67+--------------------------------------------------------------------------------
68+
69+instance Functor Maybe where
70+ fmap f Nothing = Nothing
71+ fmap f (Just j) = Just (f j)
72+
73+instance Monad Maybe where
74+ return = Just
12
75
76+ (>>=) Nothing m = Nothing
77+ (>>=) (Just j) m = m j