{-# 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.Decidable.Core as Dec
using (_×-dec_; yes; no; map′)
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
infixr 5 _∷_
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)
infix 4 _[_]=_
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
Null : Pred (List A) _
Null = 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)
infixl 6 _[_]%=_ _[_]≔_
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
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
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
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 = [] , []
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)
search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
search P? = decide (Sum.swap ∘ Dec.toSum ∘ P?)
all = all?
{-# WARNING_ON_USAGE all
"Warning: all was deprecated in v1.4.
Please use all? instead."
#-}