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

module OWL2.Foundation.Maybe where

open import OWL2.Prelude

maybe :
  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
  B → (A → B) → Optional A → B
maybe fallback f absent =
  fallback
maybe fallback f (present x) =
  f x

mapOptional :
  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
  (A → B) → Optional A → Optional B
mapOptional f absent =
  absent
mapOptional f (present x) =
  present (f x)

bind :
  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
  Optional A → (A → Optional B) → Optional B
bind absent f =
  absent
bind (present x) f =
  f x

fromMaybe : ∀ {ℓ} {A : Type ℓ} → A → Optional A → A
fromMaybe fallback absent =
  fallback
fromMaybe fallback (present x) =
  x

isPresent? : ∀ {ℓ} {A : Type ℓ} → Optional A → Bool
isPresent? absent =
  false
isPresent? (present x) =
  true

toList : ∀ {ℓ} {A : Type ℓ} → Optional A → List A
toList absent =
  []
toList (present x) =
  x ∷ []

data Present {ℓ} {A : Type ℓ} : Optional A → Type ℓ where
  presentWitness :
    (value : A) → Present (present value)

presentValue :
  ∀ {ℓ} {A : Type ℓ} {value? : Optional A} →
  Present value? → A
presentValue (presentWitness value) =
  value