------------------------------------------------------------------------
-- The Agda standard library
--
-- Maybe-related properties
------------------------------------------------------------------------

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

module Data.Maybe.Properties where

open import Algebra.Bundles using (Semigroup; Monoid)
import Algebra.Structures as Structures
import Algebra.Definitions as Definitions
open import Data.Maybe.Base using (Maybe; just; nothing; map; _<∣>_;
  maybe; maybe′)
open import Data.Maybe.Relation.Unary.All using (All; just; nothing)
open import Data.Product.Base using (_,_)
open import Function.Base using (_∋_; id; _∘_; _∘′_)
open import Function.Definitions using (Injective)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; cong; cong₂; _≗_)
open import Relation.Binary.PropositionalEquality.Properties
  using (isEquivalence)
open import Relation.Binary.Definitions using (DecidableEquality)
open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Nullary.Decidable using (map′)

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

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

just-injective :  {x y}  (Maybe A  just x)  just y  x  y
just-injective refl = refl

≡-dec : DecidableEquality A  DecidableEquality (Maybe A)
≡-dec _≟_ nothing  nothing  = yes refl
≡-dec _≟_ (just x) nothing  = no λ()
≡-dec _≟_ nothing  (just y) = no λ()
≡-dec _≟_ (just x) (just y) = map′ (cong just) just-injective (x  y)

------------------------------------------------------------------------
-- map

map-id : map id  id {A = Maybe A}
map-id (just x) = refl
map-id nothing  = refl

map-id-local :  {f : A  A} {mx}  All  x  f x  x) mx  map f mx  mx
map-id-local (just eq) = cong just eq
map-id-local nothing   = refl

map-<∣> :  (f : A  B) mx my 
  map f (mx <∣> my)  map f mx <∣> map f my
map-<∣> f (just x) my = refl
map-<∣> f nothing  my = refl

map-cong : {f g : A  B}  f  g  map f  map g
map-cong f≗g (just x) = cong just (f≗g x)
map-cong f≗g nothing  = refl

map-cong-local :  {f g : A  B} {mx} 
  All  x  f x  g x) mx  map f mx  map g mx
map-cong-local (just eq) = cong just eq
map-cong-local nothing   = refl

map-injective :  {f : A  B}  Injective _≡_ _≡_ f  Injective _≡_ _≡_ (map f)
map-injective f-inj {nothing} {nothing} p = refl
map-injective f-inj {just x} {just y} p = cong just (f-inj (just-injective p))

map-∘ : {g : B  C} {f : A  B}  map (g  f)  map g  map f
map-∘ (just x) = refl
map-∘ nothing  = refl

map-nothing :  {f : A  B} {ma}  ma  nothing  map f ma  nothing
map-nothing refl = refl

map-just :  {f : A  B} {ma a}  ma  just a  map f ma  just (f a)
map-just refl = refl

------------------------------------------------------------------------
-- maybe

maybe-map :  {C : Maybe B  Set c}
            (j : (x : B)  C (just x)) (n : C nothing) (f : A  B) ma 
            maybe {B = C} j n (map f ma)  maybe {B = C  map f} (j  f) n ma
maybe-map j n f (just x) = refl
maybe-map j n f nothing  = refl

maybe′-map :  j (n : C) (f : A  B) ma 
             maybe′ j n (map f ma)  maybe′ (j ∘′ f) n ma
maybe′-map = maybe-map

------------------------------------------------------------------------
-- _<∣>_

module _ {A : Set a} where

  open Definitions {A = Maybe A} _≡_

  <∣>-assoc : Associative _<∣>_
  <∣>-assoc (just x) y z = refl
  <∣>-assoc nothing  y z = refl

  <∣>-identityˡ : LeftIdentity nothing _<∣>_
  <∣>-identityˡ (just x) = refl
  <∣>-identityˡ nothing  = refl

  <∣>-identityʳ : RightIdentity nothing _<∣>_
  <∣>-identityʳ (just x) = refl
  <∣>-identityʳ nothing  = refl

  <∣>-identity : Identity nothing _<∣>_
  <∣>-identity = <∣>-identityˡ , <∣>-identityʳ

  <∣>-idem : Idempotent _<∣>_
  <∣>-idem (just x) = refl
  <∣>-idem nothing = refl

module _ (A : Set a) where

  open Structures {A = Maybe A} _≡_

  <∣>-isMagma : IsMagma _<∣>_
  <∣>-isMagma = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = cong₂ _<∣>_
    }

  <∣>-isSemigroup : IsSemigroup _<∣>_
  <∣>-isSemigroup = record
    { isMagma = <∣>-isMagma
    ; assoc   = <∣>-assoc
    }

  <∣>-isMonoid : IsMonoid _<∣>_ nothing
  <∣>-isMonoid = record
    { isSemigroup = <∣>-isSemigroup
    ; identity    = <∣>-identity
    }

  <∣>-semigroup : Semigroup a a
  <∣>-semigroup = record
    { isSemigroup = <∣>-isSemigroup
    }

  <∣>-monoid : Monoid a a
  <∣>-monoid = record
    { isMonoid = <∣>-isMonoid
    }

------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

map-id₂ = map-id-local
{-# WARNING_ON_USAGE map-id₂
"Warning: map-id₂ was deprecated in v2.0.
Please use map-id-local instead."
#-}

map-cong₂ = map-cong-local
{-# WARNING_ON_USAGE map-id₂
"Warning: map-cong₂ was deprecated in v2.0.
Please use map-cong-local instead."
#-}

map-compose = map-∘
{-# WARNING_ON_USAGE map-compose
"Warning: map-compose was deprecated in v2.0.
Please use map-∘ instead."
#-}

map-<∣>-commute = map-<∣>
{-# WARNING_ON_USAGE map-<∣>-commute
"Warning: map-<∣>-commute was deprecated in v2.0.
Please use map-<∣> instead."
#-}