-- The Agda standard library
-- Lists where at least one element satisfies a given property

module Data.List.Any {a} {A : Set a} where

open import Data.Empty
open import Data.Fin
open import Data.List.Base as List using (List; []; _∷_)
open import Data.Product as Prod using (; _,_)
open import Level using (_⊔_)
open import Relation.Nullary using (¬_; yes; no)
import Relation.Nullary.Decidable as Dec
open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_)

-- Any P xs means that at least one element in xs satisfies P.

data Any {p} (P : A  Set p) : List A  Set (a  p) where
  here  :  {x xs} (px  : P x)       Any P (x  xs)
  there :  {x xs} (pxs : Any P xs)  Any P (x  xs)

-- Map.

map :  {p q} {P : A  Set p} {Q : A  Set q}  P  Q  Any P  Any Q
map g (here px)   = here (g px)
map g (there pxs) = there (map g pxs)

-- If the head does not satisfy the predicate, then the tail will.

tail :  {p} {P : A  Set p} {x xs}  ¬ P x  Any P (x  xs)  Any P xs
tail ¬px (here  px)  = ⊥-elim (¬px px)
tail ¬px (there pxs) = pxs

-- Decides Any.

any :  {p} {P : A  Set p}  Decidable P  Decidable (Any P)
any p []       = no λ()
any p (x  xs) with p x
any p (x  xs) | yes px = yes (here px)
any p (x  xs) | no ¬px = Dec.map′ there (tail ¬px) (any p xs)

-- index x∈xs is the list position (zero-based) which x∈xs points to.

index :  {p} {P : A  Set p} {xs}  Any P xs  Fin (List.length xs)
index (here  px)  = zero
index (there pxs) = suc (index pxs)

-- If any element satisfies P, then P is satisfied.

satisfied :  {p} {P : A  Set p} {xs}  Any P xs   P
satisfied (here px) = _ , px
satisfied (there pxs) = satisfied pxs