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 | public export
 54 | decToMaybe : Dec a -> Maybe a
 55 | decToMaybe (Yes a) = Just a
 56 | decToMaybe (No _)  = Nothing
 57 |
 58 | export
 59 | Injective Just where
 60 |   injective Refl = Refl
 61 |
 62 | ||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case
 63 | ||| that the `Maybe` value is `Nothing`.
 64 | public export
 65 | lowerMaybe : Monoid a => Maybe a -> a
 66 | lowerMaybe Nothing = neutral
 67 | lowerMaybe (Just x) = x
 68 |
 69 | ||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.
 70 | export
 71 | raiseToMaybe : Monoid a => Eq a => a -> Maybe a
 72 | raiseToMaybe x = if x == neutral then Nothing else Just x
 73 |
 74 | public export
 75 | filter : (a -> Bool) -> Maybe a -> Maybe a
 76 | filter _ Nothing = Nothing
 77 | filter f (Just x) = toMaybe (f x) x
 78 |
 79 | namespace Semigroup
 80 |
 81 |   public export
 82 |   [Deep] Semigroup a => Semigroup (Maybe a) where
 83 |     Nothing <+> Nothing = Nothing
 84 |     Just l  <+> Nothing = Just l
 85 |     Nothing <+> Just r  = Just r
 86 |     Just l  <+> Just r  = Just $ l <+> r
 87 |
 88 | namespace Monoid
 89 |
 90 |   public export
 91 |   [Deep] Semigroup a => Monoid (Maybe a) using Semigroup.Deep where
 92 |     neutral = Nothing
 93 |
 94 | public export
 95 | Zippable Maybe where
 96 |   zipWith f x y = [| f x y |]
 97 |   zipWith3 f x y z = [| f x y z |]
 98 |
 99 |   unzipWith f Nothing  = (Nothing, Nothing)
100 |   unzipWith f (Just x) = let (a, b) = f x in (Just a, Just b)
101 |
102 |   unzipWith3 f Nothing  = (Nothing, Nothing, Nothing)
103 |   unzipWith3 f (Just x) = let (a, b, c) = f x in (Just a, Just b, Just c)
104 |
105 | --------------------------------------------------------------------------------
106 | -- Proof helpers
107 | --------------------------------------------------------------------------------
108 |
109 | %inline
110 | public export
111 | maybeCong : (f : a -> b) -> Maybe (x = y) -> Maybe (f x = f y)
112 | maybeCong f = map (\eq => cong f eq)
113 |
114 | %inline
115 | public export
116 | maybeCong2 : (f : a -> b -> c) -> Maybe (x = y) -> Maybe (v = w) -> Maybe (f x v = f y w)
117 | maybeCong2 f mxy mvw = (\xy, vw => cong2 f xy vw) <$> mxy <*> mvw
118 |