-- The Agda standard library
-- Maybes where all the elements satisfy a given property

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

module Data.Maybe.Relation.Unary.All where

open import Effect.Applicative
open import Effect.Monad
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Maybe.Relation.Unary.Any using (Any; just)
open import Data.Product.Base as Prod using (_,_)
open import Function.Base using (id; _∘′_)
open import Function.Bundles using (_⇔_; mk⇔)
open import Level
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong)
open import Relation.Unary
open import Relation.Nullary hiding (Irrelevant)
import Relation.Nullary.Decidable as Dec

-- Definition

data All {a p} {A : Set a} (P : Pred A p) : Pred (Maybe A) (a  p) where
  just    :  {x}  P x  All P (just x)
  nothing : All P nothing

-- Basic operations

module _ {a p} {A : Set a} {P : Pred A p} where

  drop-just :  {x}  All P (just x)  P x
  drop-just (just px) = px

  just-equivalence :  {x}  P x  All P (just x)
  just-equivalence = mk⇔ just drop-just

  map :  {q} {Q : Pred A q}  P  Q  All P  All Q
  map f (just px) = just (f px)
  map f nothing   = nothing

  fromAny : Any P  All P
  fromAny (just px) = just px

-- (un/)zip(/With)

module _ {a p q r} {A : Set a} {P : Pred A p} {Q : Pred A q} {R : Pred A r} where

  zipWith : P  Q  R  All P  All Q  All R
  zipWith f (just px , just qx) = just (f (px , qx))
  zipWith f (nothing , nothing) = nothing

  unzipWith : P  Q  R  All P  All Q  All R
  unzipWith f (just px) = Prod.map just just (f px)
  unzipWith f nothing   = nothing , nothing

module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where

  zip : All P  All Q  All (P  Q)
  zip = zipWith id

  unzip : All (P  Q)  All P  All Q
  unzip = unzipWith id

-- Traversable-like functions

module _ {a f} p {A : Set a} {P : Pred A (a  p)} {F}
         (App : RawApplicative {a  p} {f} F) where

  open RawApplicative App

  sequenceA : All (F ∘′ P)  F ∘′ All P
  sequenceA nothing   = pure nothing
  sequenceA (just px) = just <$> px

  mapA :  {q} {Q : Pred A q}  (Q  F ∘′ P)  All Q  (F ∘′ All P)
  mapA f = sequenceA ∘′ map f

  forA :  {q} {Q : Pred A q} {xs}  All Q xs  (Q  F ∘′ P)  F (All P xs)
  forA qxs f = mapA f qxs

module _ {a f} p {A : Set a} {P : Pred A (a  p)} {M}
         (Mon : RawMonad {a  p} {f} M) where

  private App = RawMonad.rawApplicative Mon

  sequenceM : All (M ∘′ P)  M ∘′ All P
  sequenceM = sequenceA p App

  mapM :  {q} {Q : Pred A q}  (Q  M ∘′ P)  All Q  (M ∘′ All P)
  mapM = mapA p App

  forM :  {q} {Q : Pred A q} {xs}  All Q xs  (Q  M ∘′ P)  M (All P xs)
  forM = forA p App

-- Seeing All as a predicate transformer

module _ {a p} {A : Set a} {P : Pred A p} where

  dec : Decidable P  Decidable (All P)
  dec P-dec nothing  = yes nothing
  dec P-dec (just x) = Dec.map just-equivalence (P-dec x)

  universal : Universal P  Universal (All P)
  universal P-universal (just x) = just (P-universal x)
  universal P-universal nothing  = nothing

  irrelevant : Irrelevant P  Irrelevant (All P)
  irrelevant P-irrelevant (just p) (just q) = cong just (P-irrelevant p q)
  irrelevant P-irrelevant nothing  nothing  = P.refl

  satisfiable : Satisfiable (All P)
  satisfiable = nothing , nothing