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.
commit34b88d6e93786774692951a286b6303b679bed30 authorDominic Mulligan <dominic.p.mulligan@googlemail.com> dateThu 19 Jan 2012, 20:56 (15 years ago) parent126ab04
2 files changed+121−6
compare with master
unifiedsplit
lib/prelude/either.idr+52−2 lib/prelude/maybe.idr+69−4
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+69−4
@@ -1,12 +1,77 @@
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
9−maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b
10−maybe_bind Nothing k = Nothing
11−maybe_bind (Just x) k = k x
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+ 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
1275
76+ (>>=) Nothing m = Nothing
77+ (>>=) (Just j) m = m j