------------------------------------------------------------------------
-- The Agda standard library
--
-- The Maybe type
------------------------------------------------------------------------

module Data.Maybe where

open import Function
open import Level
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary as B
open import Relation.Unary as U

------------------------------------------------------------------------
-- The base type and some operations

open import Data.Maybe.Base public

------------------------------------------------------------------------
-- Equality

data Eq {a } {A : Set a} (_≈_ : Rel A ) : Rel (Maybe A) (a  ) where
  just    :  {x y} (x≈y : x  y)  Eq _≈_ (just x) (just y)
  nothing : Eq _≈_ nothing nothing

drop-just :  {a } {A : Set a} {_≈_ : Rel A } {x y : A} 
            just x  Eq _≈_  just y  x  y
drop-just (just x≈y) = x≈y

Eq-refl :  {a } {A : Set a} {_≈_ : Rel A } 
       Reflexive _≈_  Reflexive (Eq _≈_)
Eq-refl refl {just x}  = just refl
Eq-refl refl {nothing} = nothing

Eq-sym :   {a } {A : Set a} {_≈_ : Rel A } 
       Symmetric _≈_  Symmetric (Eq _≈_)
Eq-sym sym (just x≈y) = just (sym x≈y)
Eq-sym sym nothing    = nothing

Eq-trans :  {a } {A : Set a} {_≈_ : Rel A } 
       Transitive _≈_  Transitive (Eq _≈_)
Eq-trans trans (just x≈y) (just y≈z) = just (trans x≈y y≈z)
Eq-trans trans nothing    nothing    = nothing

Eq-dec :  {a } {A : Set a} {_≈_ : Rel A } 
      B.Decidable _≈_  B.Decidable (Eq _≈_)
Eq-dec dec (just x) (just y)  with dec x y
...  | yes x≈y = yes (just x≈y)
...  | no  x≉y = no (x≉y  drop-just)
Eq-dec dec (just x) nothing = no λ()
Eq-dec dec nothing (just y)  = no λ()
Eq-dec dec nothing nothing = yes nothing

Eq-isEquivalence :  {a } {A : Set a} {_≈_ : Rel A }
                 IsEquivalence _≈_  IsEquivalence (Eq _≈_)
Eq-isEquivalence isEq = record
  { refl  = Eq-refl (IsEquivalence.refl isEq)
  ; sym   = Eq-sym (IsEquivalence.sym isEq)
  ; trans = Eq-trans (IsEquivalence.trans isEq)
  }

Eq-isDecEquivalence :  {a } {A : Set a} {_≈_ : Rel A }
                 IsDecEquivalence _≈_  IsDecEquivalence (Eq _≈_)
Eq-isDecEquivalence isDecEq = record
  { isEquivalence = Eq-isEquivalence
                      (IsDecEquivalence.isEquivalence isDecEq)
  ; _≟_           = Eq-dec (IsDecEquivalence._≟_ isDecEq)
  }

setoid :  {ℓ₁ ℓ₂}  Setoid ℓ₁ ℓ₂  Setoid _ _
setoid S = record {
    isEquivalence = Eq-isEquivalence (Setoid.isEquivalence S)
  }

decSetoid :  {ℓ₁ ℓ₂}  DecSetoid ℓ₁ ℓ₂  DecSetoid _ _
decSetoid D = record {
    isDecEquivalence = Eq-isDecEquivalence
                         (DecSetoid.isDecEquivalence D)
  }

------------------------------------------------------------------------
-- Any and All are preserving decidability

anyDec :  {a p} {A : Set a} {P : A  Set p} 
         U.Decidable P  U.Decidable (Any P)
anyDec p nothing  = no λ()
anyDec p (just x) = Dec.map′ just  { (Any.just px)  px }) (p x)

allDec :  {a p} {A : Set a} {P : A  Set p} 
         U.Decidable P  U.Decidable (All P)
allDec p nothing  = yes nothing
allDec p (just x) = Dec.map′ just  { (All.just px)  px }) (p x)