------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists where all elements satisfy a given property
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.List.Relation.Unary.All where
 
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
open import Data.List.Membership.Propositional renaming (_∈_ to _∈ₚ_)
import Data.List.Membership.Setoid as SetoidMembership
open import Data.Product.Base as Product
  using (∃; -,_; _×_; _,_; proj₁; proj₂; uncurry)
open import Data.Sum.Base as Sum using (inj₁; inj₂)
open import Effect.Applicative
open import Effect.Monad
open import Function.Base using (_∘_; _∘′_; id; const)
open import Level using (Level; _⊔_)
open import Relation.Nullary hiding (Irrelevant)
import Relation.Nullary.Decidable as Dec
open import Relation.Unary hiding (_∈_)
import Relation.Unary.Properties as Unary
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions using (_Respects_)
open import Relation.Binary.PropositionalEquality.Core as ≡
import Relation.Binary.PropositionalEquality.Properties as ≡
 
private
  variable
    a b p q r ℓ : Level
    A : Set a
    B : Set b
    P Q R : Pred A p
    x : A
    xs : List A
 
------------------------------------------------------------------------
-- Definitions
 
-- Given a predicate P, then All P xs means that every element in xs
-- satisfies P. See `Relation.Unary` for an explanation of predicates.
 
infixr  _∷_
 
data All {A : Set a} (P : Pred A p) : Pred (List A) (a ⊔ p) where
  []  : All P []
  _∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → All P (x ∷ xs)
 
-- All P xs is a finite map from indices x ∈ xs to content P x.
-- Relation pxs [ i ]= px states that, in map pxs, key i : x ∈ xs points
-- to value px.
 
infix  _[_]=_
 
data _[_]=_ {A : Set a} {P : Pred A p} :
            ∀ {x xs} → All P xs → x ∈ₚ xs → P x → Set (a ⊔ p) where
 
  here  : ∀ {x xs} {px : P x} {pxs : All P xs} →
          px ∷ pxs [ here refl ]= px
 
  there : ∀ {x xs y} {px : P x} {pxs : All P xs} {py : P y} {i : x ∈ₚ xs} →
          pxs [ i ]= px →
          py ∷ pxs [ there i ]= px
 
-- A list is empty if having an element is impossible.
 
Null : Pred (List A) _
Null = All ∅
 
------------------------------------------------------------------------
-- Operations on All
 
uncons : All P (x ∷ xs) → P x × All P xs
uncons (px ∷ pxs) = px , pxs
 
head : All P (x ∷ xs) → P x
head = proj₁ ∘ uncons
 
tail : All P (x ∷ xs) → All P xs
tail = proj₂ ∘ uncons
 
reduce : (f : ∀ {x} → P x → B) → All P xs → List B
reduce f []         = []
reduce f (px ∷ pxs) = f px ∷ reduce f pxs
 
construct : (f : B → ∃ P) (xs : List B) → ∃ (All P)
construct f []       = [] , []
construct f (x ∷ xs) = Product.zip _∷_ _∷_ (f x) (construct f xs)
 
fromList : (xs : List (∃ P)) → All P (List.map proj₁ xs)
fromList []              = []
fromList ((x , p) ∷ xps) = p ∷ fromList xps
 
toList : All P xs → List (∃ P)
toList pxs = reduce (λ {x} px → x , px) pxs
 
map : P ⊆ Q → All P ⊆ All Q
map g []         = []
map g (px ∷ pxs) = g px ∷ map g pxs
 
zipWith : P ∩ Q ⊆ R → All P ∩ All Q ⊆ All R
zipWith f ([] , [])             = []
zipWith f (px ∷ pxs , qx ∷ qxs) = f (px , qx) ∷ zipWith f (pxs , qxs)
 
unzipWith : R ⊆ P ∩ Q → All R ⊆ All P ∩ All Q
unzipWith f []         = [] , []
unzipWith f (rx ∷ rxs) = Product.zip _∷_ _∷_ (f rx) (unzipWith f rxs)
 
zip : All P ∩ All Q ⊆ All (P ∩ Q)
zip = zipWith id
 
unzip : All (P ∩ Q) ⊆ All P ∩ All Q
unzip = unzipWith id
 
module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
  open Setoid S renaming (refl to ≈-refl)
  open SetoidMembership S
 
  tabulateₛ : (∀ {x} → x ∈ xs → P x) → All P xs
  tabulateₛ {[]}    hyp = []
  tabulateₛ {_ ∷ _} hyp = hyp (here ≈-refl) ∷ tabulateₛ (hyp ∘ there)
 
tabulate : (∀ {x} → x ∈ₚ xs → P x) → All P xs
tabulate = tabulateₛ (≡.setoid _)
 
self : ∀ {xs} → All (const A) xs
self = tabulate (λ {x} _ → x)
 
------------------------------------------------------------------------
-- (weak) updateAt
 
infixl  _[_]%=_ _[_]≔_
 
updateAt : x ∈ₚ xs → (P x → P x) → All P xs → All P xs
updateAt () f []
updateAt (here refl) f (px ∷ pxs) = f px ∷ pxs
updateAt (there i)   f (px ∷ pxs) =   px ∷ updateAt i f pxs
 
_[_]%=_ : All P xs → x ∈ₚ xs → (P x → P x) → All P xs
pxs [ i ]%= f = updateAt i f pxs
 
_[_]≔_ : All P xs → x ∈ₚ xs → P x → All P xs
pxs [ i ]≔ px = pxs [ i ]%= const px
 
------------------------------------------------------------------------
-- Traversable-like functions
 
module _ (p : Level) {A : Set a} {P : Pred A (a ⊔ p)}
         {F : Set (a ⊔ p) → Set (a ⊔ p)}
         (App : RawApplicative F)
         where
 
  open RawApplicative App
 
  sequenceA : All (F ∘′ P) ⊆ F ∘′ All P
  sequenceA []       = pure []
  sequenceA (x ∷ xs) = _∷_ <$> x <*> sequenceA xs
 
  mapA : ∀ {Q : Pred A q} → (Q ⊆ F ∘′ P) → All Q ⊆ (F ∘′ All P)
  mapA f = sequenceA ∘′ map f
 
  forA : ∀ {Q : Pred A q} → All Q xs → (Q ⊆ F ∘′ P) → F (All P xs)
  forA qxs f = mapA f qxs
 
module _ (p : Level) {A : Set a} {P : Pred A (a ⊔ p)}
         {M : Set (a ⊔ p) → Set (a ⊔ p)}
         (Mon : RawMonad M)
         where
 
  private App = RawMonad.rawApplicative Mon
 
  sequenceM : All (M ∘′ P) ⊆ M ∘′ All P
  sequenceM = sequenceA p App
 
  mapM : ∀ {Q : Pred A q} → (Q ⊆ M ∘′ P) → All Q ⊆ (M ∘′ All P)
  mapM = mapA p App
 
  forM : ∀ {Q : Pred A q} → All Q xs → (Q ⊆ M ∘′ P) → M (All P xs)
  forM = forA p App
 
------------------------------------------------------------------------
-- Generalised lookup based on a proof of Any
 
lookupAny : All P xs → (i : Any Q xs) → (P ∩ Q) (Any.lookup i)
lookupAny (px ∷ pxs) (here qx) = px , qx
lookupAny (px ∷ pxs) (there i) = lookupAny pxs i
 
lookupWith : ∀[ P ⇒ Q ⇒ R ] → All P xs → (i : Any Q xs) → R (Any.lookup i)
lookupWith f pxs i = Product.uncurry f (lookupAny pxs i)
 
lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x)
lookup pxs = lookupWith (λ { px refl → px }) pxs
 
module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
  open Setoid S renaming (sym to ≈-sym)
  open SetoidMembership S
 
  lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
  lookupₛ resp pxs = lookupWith (λ py x≈y → resp (≈-sym x≈y) py) pxs
 
------------------------------------------------------------------------
-- Properties of predicates preserved by All
 
all? : Decidable P → Decidable (All P)
all? p []       = yes []
all? p (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (p x ×-dec all? p xs)
 
universal : Universal P → Universal (All P)
universal u []       = []
universal u (x ∷ xs) = u x ∷ universal u xs
 
universal-U : Universal (All {A = A} U)
universal-U = universal Unary.U-Universal
 
irrelevant : Irrelevant P → Irrelevant (All P)
irrelevant irr []           []           = ≡.refl
irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
  ≡.cong₂ _∷_ (irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)
 
satisfiable : Satisfiable (All P)
satisfiable = [] , []
 
------------------------------------------------------------------------
-- Generalised decidability procedure
 
decide :  Π[ P ∪ Q ] → Π[ All P ∪ Any Q ]
decide p∪q [] = inj₁ []
decide p∪q (x ∷ xs) with p∪q x
... | inj₂ qx = inj₂ (here qx)
... | inj₁ px = Sum.map (px ∷_) there (decide p∪q xs)
 
------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
 
-- Version 1.4
 
all = all?
{-# WARNING_ON_USAGE all
"Warning: all was deprecated in v1.4.
Please use all? instead."
#-}