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

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

open import Relation.Binary.Bundles using (StrictTotalOrder)

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

open import Data.Product.Base 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ₚ


private
  variable
    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