git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2 from dpmulligan/master
6a5d1fcEdwin Brady
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+62−3
@@ -1,12 +1,71 @@
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
43+fromMaybe : |(def: a) -> Maybe a -> a
44+fromMaybe def Nothing = def
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+ Nothing => catMaybes xs
56+ Just j => j :: 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+
9maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b
69maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b
10−maybe_bind Nothing k = Nothing
70+maybe_bind Nothing k = Nothing
11maybe_bind (Just x) k = k x
71maybe_bind (Just x) k = k x
12−