0 | module Data.Maybe
 1 |
 2 | import Control.Function
 3 |
 4 | import Data.Zippable
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | isNothing : Maybe a -> Bool
10 | isNothing Nothing  = True
11 | isNothing (Just _) = False
12 |
13 | public export
14 | isJust : Maybe a -> Bool
15 | isJust Nothing  = False
16 | isJust (Just _) = True
17 |
18 | ||| Proof that some `Maybe` is actually `Just`
19 | public export
20 | data IsJust : Maybe a -> Type where
21 |   ItIsJust : IsJust (Just x)
22 |
23 | export
24 | Uninhabited (IsJust Nothing) where
25 |   uninhabited ItIsJust impossible
26 |
27 | ||| Decide whether a 'Maybe' is 'Just'
28 | public export
29 | isItJust : (v : Maybe a) -> Dec (IsJust v)
30 | isItJust (Just _) = Yes ItIsJust
31 | isItJust Nothing = No absurd
32 |
33 | ||| Convert a `Maybe a` value to an `a` value by providing a default `a` value
34 | ||| in the case that the `Maybe` value is `Nothing`.
35 | public export
36 | fromMaybe : (Lazy a) -> Maybe a -> a
37 | fromMaybe def Nothing  = def
38 | fromMaybe _   (Just j) = j
39 |
40 | ||| Returns the `a` value of a `Maybe a` which is proved `Just`.
41 | public export
42 | fromJust : (v : Maybe a) -> (0 _ : IsJust v) => a
43 | fromJust (Just x) = x
44 | fromJust Nothing impossible
45 |
46 | ||| Returns `Just` the given value if the conditional is `True`
47 | ||| and `Nothing` if the conditional is `False`.
48 | public export
49 | toMaybe : Bool -> Lazy a -> Maybe a
50 | toMaybe True  j = Just j
51 | toMaybe False _ = Nothing
52 |
53 | export
54 | Injective Just where
55 |   injective Refl = Refl
56 |
57 | ||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case
58 | ||| that the `Maybe` value is `Nothing`.
59 | public export
60 | lowerMaybe : Monoid a => Maybe a -> a
61 | lowerMaybe Nothing = neutral
62 | lowerMaybe (Just x) = x
63 |
64 | ||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.
65 | export
66 | raiseToMaybe : Monoid a => Eq a => a -> Maybe a
67 | raiseToMaybe x = if x == neutral then Nothing else Just x
68 |
69 | public export
70 | filter : (a -> Bool) -> Maybe a -> Maybe a
71 | filter _ Nothing = Nothing
72 | filter f (Just x) = toMaybe (f x) x
73 |
74 | namespace Semigroup
75 |
76 |   public export
77 |   [Deep] Semigroup a => Semigroup (Maybe a) where
78 |     Nothing <+> Nothing = Nothing
79 |     Just l  <+> Nothing = Just l
80 |     Nothing <+> Just r  = Just r
81 |     Just l  <+> Just r  = Just $ l <+> r
82 |
83 | namespace Monoid
84 |
85 |   public export
86 |   [Deep] Semigroup a => Monoid (Maybe a) using Semigroup.Deep where
87 |     neutral = Nothing
88 |
89 | public export
90 | Zippable Maybe where
91 |   zipWith f x y = [| f x y |]
92 |   zipWith3 f x y z = [| f x y z |]
93 |
94 |   unzipWith f Nothing  = (Nothing, Nothing)
95 |   unzipWith f (Just x) = let (a, b) = f x in (Just a, Just b)
96 |
97 |   unzipWith3 f Nothing  = (Nothing, Nothing, Nothing)
98 |   unzipWith3 f (Just x) = let (a, b, c) = f x in (Just a, Just b, Just c)
99 |