16
16
------------------------------------------------------------------------
19
open import Data.Bool using (Bool; true; false)
19
open import Data.Bool using (Bool; true; false; not)
20
20
open import Data.Unit using (⊤)
22
open import Relation.Nullary
22
24
boolToMaybe : Bool → Maybe ⊤
23
25
boolToMaybe true = just _
24
26
boolToMaybe false = nothing
26
maybeToBool : ∀ {a} {A : Set a} → Maybe A → Bool
27
maybeToBool (just _) = true
28
maybeToBool nothing = false
28
is-just : ∀ {a} {A : Set a} → Maybe A → Bool
29
is-just (just _) = true
30
is-just nothing = false
32
is-nothing : ∀ {a} {A : Set a} → Maybe A → Bool
33
is-nothing = not ∘ is-just
35
decToMaybe : ∀ {a} {A : Set a} → Dec A → Maybe A
36
decToMaybe (yes x) = just x
37
decToMaybe (no _) = nothing
30
39
-- A dependent eliminator.
53
62
------------------------------------------------------------------------
57
65
open import Category.Functor
58
66
open import Category.Monad
59
67
open import Category.Monad.Identity
69
map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Maybe A → Maybe B
70
map f = maybe (just ∘ f) nothing
61
72
functor : ∀ {f} → RawFunctor (Maybe {a = f})
63
{ _<$>_ = λ f → maybe (just ∘ f) nothing
66
77
monadT : ∀ {f} {M : Set f → Set f} →
149
159
------------------------------------------------------------------------
162
open Data.Bool using (T)
152
163
open import Data.Empty using (⊥)
153
164
import Relation.Nullary.Decidable as Dec
154
165
open import Relation.Unary as U
156
data Any {a} {A : Set a} (P : A → Set a) : Maybe A → Set a where
167
data Any {a p} {A : Set a} (P : A → Set p) : Maybe A → Set (a ⊔ p) where
157
168
just : ∀ {x} (px : P x) → Any P (just x)
159
data All {a} {A : Set a} (P : A → Set a) : Maybe A → Set a where
170
data All {a p} {A : Set a} (P : A → Set p) : Maybe A → Set (a ⊔ p) where
160
171
just : ∀ {x} (px : P x) → All P (just x)
161
172
nothing : All P nothing
163
IsJust : ∀ {a} {A : Set a} → Maybe A → Set a
164
IsJust = Any (λ _ → Lift ⊤)
166
IsNothing : ∀ {a} {A : Set a} → Maybe A → Set a
167
IsNothing = All (λ _ → Lift ⊥)
171
drop-just-Any : ∀ {A} {P : A → Set} {x} → Any P (just x) → P x
172
drop-just-Any (just px) = px
174
drop-just-All : ∀ {A} {P : A → Set} {x} → All P (just x) → P x
175
drop-just-All (just px) = px
177
anyDec : ∀ {A} {P : A → Set} → U.Decidable P → U.Decidable (Any P)
174
Is-just : ∀ {a} {A : Set a} → Maybe A → Set a
175
Is-just = Any (λ _ → ⊤)
177
Is-nothing : ∀ {a} {A : Set a} → Maybe A → Set a
178
Is-nothing = All (λ _ → ⊥)
180
to-witness : ∀ {p} {P : Set p} {m : Maybe P} → Is-just m → P
181
to-witness (just {x = p} _) = p
183
to-witness-T : ∀ {p} {P : Set p} (m : Maybe P) → T (is-just m) → P
184
to-witness-T (just p) _ = p
185
to-witness-T nothing ()
187
anyDec : ∀ {a p} {A : Set a} {P : A → Set p} →
188
U.Decidable P → U.Decidable (Any P)
178
189
anyDec p nothing = no λ()
179
anyDec p (just x) = Dec.map′ just drop-just-Any (p x)
190
anyDec p (just x) = Dec.map′ just (λ { (Any.just px) → px }) (p x)
181
allDec : ∀ {A} {P : A → Set} → U.Decidable P → U.Decidable (All P)
192
allDec : ∀ {a p} {A : Set a} {P : A → Set p} →
193
U.Decidable P → U.Decidable (All P)
182
194
allDec p nothing = yes nothing
183
allDec p (just x) = Dec.map′ just drop-just-All (p x)
195
allDec p (just x) = Dec.map′ just (λ { (All.just px) → px }) (p x)
added
removed
src/Data/Maybe.agda
