------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of permutations using setoid equality (on Maybe elements)
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe where

open import Relation.Binary.Core using (_Preserves_⟶_)
open import Relation.Binary.Bundles using (Setoid)

open import Level using (Level)
open import Function.Base using (_∘_; _$_)

open import Data.List.Base using (catMaybes; mapMaybe)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
import Data.List.Relation.Binary.Permutation.Setoid as Permutation
open import Data.List.Relation.Binary.Permutation.Setoid.Properties

open import Data.Maybe using (Maybe; nothing; just)
open import Data.Maybe.Relation.Binary.Pointwise using (nothing; just)
  renaming (setoid to setoidᴹ)

private
  variable
    a b ℓ ℓ′ : Level

------------------------------------------------------------------------
-- catMaybes

module _ (sᴬ : Setoid a ℓ) where
  open Setoid sᴬ using (_≈_)
  open Permutation sᴬ

  private sᴹ = setoidᴹ sᴬ
  open Setoid sᴹ using () renaming (_≈_ to _≈ᴹ_)
  open Permutation sᴹ using () renaming (_↭_ to _↭ᴹ_)

  catMaybes-↭ : ∀ {xs ys} → xs ↭ᴹ ys → catMaybes xs ↭ catMaybes ys
  catMaybes-↭ (refl p) = refl (pointwise p)
    where
    pointwise : ∀ {xs ys} → Pointwise _≈ᴹ_ xs ys →
                Pointwise _≈_ (catMaybes xs) (catMaybes ys)
    pointwise []             = []
    pointwise (just p  ∷ ps) = p ∷ pointwise ps
    pointwise (nothing ∷ ps) = pointwise ps
  catMaybes-↭ (trans xs↭ ↭ys)              = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys)
  catMaybes-↭ (prep nothing    xs↭)        = catMaybes-↭ xs↭
  catMaybes-↭ (prep (just x~y) xs↭)        = prep x~y $ catMaybes-↭ xs↭
  catMaybes-↭ (swap nothing  nothing  xs↭) = catMaybes-↭ xs↭
  catMaybes-↭ (swap nothing  (just y) xs↭) = prep y $ catMaybes-↭ xs↭
  catMaybes-↭ (swap (just x) nothing  xs↭) = prep x $ catMaybes-↭ xs↭
  catMaybes-↭ (swap (just x) (just y) xs↭) = swap x y $ catMaybes-↭ xs↭

------------------------------------------------------------------------
-- mapMaybe

module _ (sᴬ : Setoid a ℓ) (sᴮ : Setoid b ℓ′) where
  open Setoid sᴬ using () renaming (_≈_ to _≈ᴬ_)
  open Permutation sᴬ using () renaming (_↭_ to _↭ᴬ_)
  open Permutation sᴮ using () renaming (_↭_ to _↭ᴮ_)

  private sᴹᴮ = setoidᴹ sᴮ
  open Setoid sᴹᴮ using () renaming (_≈_ to _≈ᴹᴮ_)

  mapMaybe-↭ : ∀ {f} → f Preserves _≈ᴬ_ ⟶ _≈ᴹᴮ_ →
               ∀ {xs ys} → xs ↭ᴬ ys → mapMaybe f xs ↭ᴮ mapMaybe f ys
  mapMaybe-↭ pres = catMaybes-↭ sᴮ ∘ map⁺ sᴬ sᴹᴮ pres