git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2 from dpmulligan/master

Additions to Idris Prelude

commit6a5d1fc2b66704c2faccdb239588e891545c4005 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 21 Jan 2012, 07:48 (15 years ago) parentb63e9bb5570cee
2 files changed+114−5
compare with master
unifiedsplit
lib/prelude/either.idr+52−2 lib/prelude/maybe.idr+62−3
lib/prelude/either.idr+52−2
@@ -2,12 +2,62 @@ module prelude.either
22
33import builtins
44
5−data Either a b = Left a | Right b
5+import prelude.maybe
6+import prelude.list
7+
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+--------------------------------------------------------------------------------
627
728choose : (b : Bool) -> Either (so b) (so (not b))
8−choose True = Left oh
29+choose True = Left oh
930choose False = Right oh
1031
1132either : Either a b -> (a -> c) -> (b -> c) -> c
1233either (Left x) l r = l x
1334either (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 @@
11module prelude.maybe
22
3−data Maybe a = Nothing | Just a
3+import builtins
4+import prelude.list
5+import prelude.monad
6+
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+--------------------------------------------------------------------------------
438
539maybe : |(def : b) -> (a -> b) -> Maybe a -> b
640maybe n j Nothing = n
741maybe n j (Just x) = j x
842
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+
969maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b
10−maybe_bind Nothing k = Nothing
70+maybe_bind Nothing k = Nothing
1171maybe_bind (Just x) k = k x
12−