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

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

open import Relation.Binary using (StrictTotalOrder)

module Data.Tree.AVL.Relation.Unary.Any
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)

open import Data.Product as Prod using ()
open import Function.Base using (_∘_; _$_)
open import Level using (Level; _⊔_)

open import Relation.Nullary.Decidable using (map′)
open import Relation.Unary

open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
open import Data.Tree.AVL.Indexed strictTotalOrder as Indexed using (K&_; _,_)
open import Data.Tree.AVL strictTotalOrder using (Tree; tree; Value)
import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as AVLₚ

    v p q : Level
    V : Value v
    t : Tree V
    P : Pred (K& V) p
    Q : Pred (K& V) q

-- Definition

-- Given a predicate P, Any P t describes a path in t to an element that
-- satisfies P. There may be others.
-- See `Relation.Unary` for an explanation of predicates.

data Any {V : Value v} (P : Pred (K& V) p) :
         Tree V  Set (p  a  v  ℓ₂) where
  tree :  {h t}  AVLₚ.Any P t  Any P (tree {h = h} t)

-- Operations on Any

map : P  Q  Any P t  Any Q t
map f (tree p) = tree (AVLₚ.map f p)

lookup : Any {V = V} P t  K& V
lookup (tree p) = AVLₚ.lookup p

lookupKey : Any P t  Key
lookupKey (tree p) = AVLₚ.lookupKey p

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

satisfied : Any P t   P
satisfied (tree p) = AVLₚ.satisfied p

-- Properties of predicates preserved by Any

any? : Decidable P  Decidable (Any {V = V} P)
any? P? (tree p) = map′ tree  where (tree p)  p) (AVLₚ.any? P? p)

satisfiable : (k : Key)  Satisfiable (P  (k ,_))  Satisfiable (Any {V = V} P)
satisfiable k sat = Prod.map tree tree
                  $ AVLₚ.satisfiable Indexed.⊥⁺<[ k ] Indexed.[ k ]<⊤⁺ sat