← Back to branch summary

~ubuntu-branches/ubuntu/maverick/agda-stdlib/maverick

« back to all changes in this revision

Viewing changes to src/Data/Maybe.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Maybe.agda
 
1
------------------------------------------------------------------------
 
2
-- The Maybe type
 
3
------------------------------------------------------------------------
 
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
 
7
module Data.Maybe where
 
8
 
 
9
open import Level
 
10
 
 
11
------------------------------------------------------------------------
 
12
-- The type
 
13
 
 
14
open import Data.Maybe.Core public
 
15
 
 
16
------------------------------------------------------------------------
 
17
-- Some operations
 
18
 
 
19
open import Data.Bool using (Bool; true; false)
 
20
open import Data.Unit using (⊤)
 
21
 
 
22
boolToMaybe : Bool → Maybe ⊤
 
23
boolToMaybe true  = just _
 
24
boolToMaybe false = nothing
 
25
 
 
26
maybeToBool : ∀ {a} {A : Set a} → Maybe A → Bool
 
27
maybeToBool (just _) = true
 
28
maybeToBool nothing  = false
 
29
 
 
30
-- A non-dependent eliminator.
 
31
 
 
32
maybe : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Maybe A → B
 
33
maybe j n (just x) = j x
 
34
maybe j n nothing  = n
 
35
 
 
36
------------------------------------------------------------------------
 
37
-- Maybe monad
 
38
 
 
39
open import Data.Function
 
40
open import Category.Functor
 
41
open import Category.Monad
 
42
open import Category.Monad.Identity
 
43
 
 
44
functor : RawFunctor Maybe
 
45
functor = record
 
46
  { _<$>_ = λ f → maybe (just ∘ f) nothing
 
47
  }
 
48
 
 
49
monadT : ∀ {M} → RawMonad M → RawMonad (λ A → M (Maybe A))
 
50
monadT M = record
 
51
  { return = M.return ∘ just
 
52
  ; _>>=_  = λ m f → M._>>=_ m (maybe f (M.return nothing))
 
53
  }
 
54
  where module M = RawMonad M
 
55
 
 
56
monad : RawMonad Maybe
 
57
monad = monadT IdentityMonad
 
58
 
 
59
monadZero : RawMonadZero Maybe
 
60
monadZero = record
 
61
  { monad = monad
 
62
  ; ∅     = nothing
 
63
  }
 
64
 
 
65
monadPlus : RawMonadPlus Maybe
 
66
monadPlus = record
 
67
  { monadZero = monadZero
 
68
  ; _∣_       = _∣_
 
69
  }
 
70
  where
 
71
  _∣_ : ∀ {a : Set} → Maybe a → Maybe a → Maybe a
 
72
  nothing ∣ y = y
 
73
  just x  ∣ y = just x
 
74
 
 
75
------------------------------------------------------------------------
 
76
-- Equality
 
77
 
 
78
open import Relation.Nullary
 
79
open import Relation.Binary
 
80
open import Relation.Binary.PropositionalEquality as PropEq
 
81
  using (_≡_; refl)
 
82
 
 
83
drop-just : ∀ {A : Set} {x y : A} → just x ≡ just y → x ≡ y
 
84
drop-just refl = refl
 
85
 
 
86
decSetoid : {A : Set} → Decidable (_≡_ {A = A}) → DecSetoid _ _
 
87
decSetoid {A} _A-≟_ = PropEq.decSetoid _≟_
 
88
  where
 
89
  _≟_ : Decidable (_≡_ {A = Maybe A})
 
90
  just x  ≟ just y  with x A-≟ y
 
91
  just x  ≟ just .x | yes refl = yes refl
 
92
  just x  ≟ just y  | no  x≢y    = no (x≢y ∘ drop-just)
 
93
  just x  ≟ nothing = no λ()
 
94
  nothing ≟ just y  = no λ()
 
95
  nothing ≟ nothing = yes refl
 
96
 
 
97
------------------------------------------------------------------------
 
98
-- Any and All
 
99
 
 
100
open import Data.Product using (_,_)
 
101
open import Data.Empty using (⊥)
 
102
import Relation.Nullary.Decidable as Dec
 
103
 
 
104
data Any {a} {A : Set a} (P : A → Set a) : Maybe A → Set a where
 
105
  just : ∀ {x} (px : P x) → Any P (just x)
 
106
 
 
107
data All {a} {A : Set a} (P : A → Set a) : Maybe A → Set a where
 
108
  just    : ∀ {x} (px : P x) → All P (just x)
 
109
  nothing : All P nothing
 
110
 
 
111
IsJust : ∀ {A : Set} → Maybe A → Set
 
112
IsJust = Any (λ _ → ⊤)
 
113
 
 
114
IsNothing : ∀ {A} → Maybe A → Set
 
115
IsNothing = All (λ _ → ⊥)
 
116
 
 
117
private
 
118
 
 
119
  drop-just-Any : ∀ {A} {P : A → Set} {x} → Any P (just x) → P x
 
120
  drop-just-Any (just px) = px
 
121
 
 
122
  drop-just-All : ∀ {A} {P : A → Set} {x} → All P (just x) → P x
 
123
  drop-just-All (just px) = px
 
124
 
 
125
anyDec : ∀ {A} {P : A → Set} →
 
126
         (∀ x → Dec (P x)) → (x : Maybe A) → Dec (Any P x)
 
127
anyDec p nothing  = no λ()
 
128
anyDec p (just x) = Dec.map (just , drop-just-Any) (p x)
 
129
 
 
130
allDec : ∀ {A} {P : A → Set} →
 
131
         (∀ x → Dec (P x)) → (x : Maybe A) → Dec (All P x)
 
132
allDec p nothing  = yes nothing
 
133
allDec p (just x) = Dec.map (just , drop-just-All) (p x)