------------------------------------------------------------------------
-- The Agda standard library
--
-- The Maybe type and some operations
------------------------------------------------------------------------

-- The definitions in this file are reexported by Data.Maybe.

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Maybe.Base where

open import Level
open import Data.Bool.Base using (Bool; true; false; not)
open import Data.Unit.Base using (⊤)
open import Data.These.Base using (These; this; that; these)
open import Data.Product as Prod using (_×_; _,_)
open import Function.Base
open import Relation.Nullary.Reflects
open import Relation.Nullary.Decidable.Core

private
  variable
    a b c : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Definition

open import Agda.Builtin.Maybe public
  using (Maybe; just; nothing)

------------------------------------------------------------------------
-- Some operations

boolToMaybe : Bool → Maybe ⊤
boolToMaybe true  = just _
boolToMaybe false = nothing

is-just : Maybe A → Bool
is-just (just _) = true
is-just nothing  = false

is-nothing : Maybe A → Bool
is-nothing = not ∘ is-just

decToMaybe : Dec A → Maybe A
decToMaybe ( true because [a]) = just (invert [a])
decToMaybe (false because  _ ) = nothing

-- A dependent eliminator.

maybe : ∀ {A : Set a} {B : Maybe A → Set b} →
        ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x
maybe j n (just x) = j x
maybe j n nothing  = n

-- A non-dependent eliminator.

maybe′ : (A → B) → B → Maybe A → B
maybe′ = maybe

-- A defaulting mechanism

fromMaybe : A → Maybe A → A
fromMaybe = maybe′ id

-- A safe variant of "fromJust". If the value is nothing, then the
-- return type is the unit type.

module _ {a} {A : Set a} where

  From-just : Maybe A → Set a
  From-just (just _) = A
  From-just nothing  = Lift a ⊤

  from-just : (x : Maybe A) → From-just x
  from-just (just x) = x
  from-just nothing  = _

-- Functoriality: map

map : (A → B) → Maybe A → Maybe B
map f = maybe (just ∘ f) nothing

-- Applicative: ap

ap : Maybe (A → B) → Maybe A → Maybe B
ap nothing  = const nothing
ap (just f) = map f

-- Monad: bind

infixl  _>>=_
_>>=_ : Maybe A → (A → Maybe B) → Maybe B
nothing >>= f = nothing
just a  >>= f = f a

-- Alternative: <∣>

infixr  _<∣>_
_<∣>_ : Maybe A → Maybe A → Maybe A
just x  <∣> my = just x
nothing <∣> my = my

-- Just when the boolean is true

when : Bool → A → Maybe A
when b c = map (const c) (boolToMaybe b)

------------------------------------------------------------------------
-- Aligning and zipping

alignWith : (These A B → C) → Maybe A → Maybe B → Maybe C
alignWith f (just a) (just b) = just (f (these a b))
alignWith f (just a) nothing  = just (f (this a))
alignWith f nothing  (just b) = just (f (that b))
alignWith f nothing  nothing  = nothing

zipWith : (A → B → C) → Maybe A → Maybe B → Maybe C
zipWith f (just a) (just b) = just (f a b)
zipWith _ _        _        = nothing

align : Maybe A → Maybe B → Maybe (These A B)
align = alignWith id

zip : Maybe A → Maybe B → Maybe (A × B)
zip = zipWith _,_

------------------------------------------------------------------------
-- Injections.

thisM : A → Maybe B → These A B
thisM a = maybe′ (these a) (this a)

thatM : Maybe A → B → These A B
thatM = maybe′ these that