------------------------------------------------------------------------
-- The Agda standard library
--
-- AVL trees
------------------------------------------------------------------------
-- AVL trees are balanced binary search trees.
-- The search tree invariant is specified using the technique
-- described by Conor McBride in his talk "Pivotal pragmatism".
-- See README.Data.Tree.AVL for examples of how to use AVL trees.
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (StrictTotalOrder)
module Data.Tree.AVL
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
where
open import Data.Bool.Base using (Bool)
import Data.DifferenceList as DiffList
open import Data.List.Base as List using (List; []; _∷_)
open import Data.Maybe.Base using (Maybe; nothing; just; is-just)
open import Data.Nat.Base using (ℕ; suc)
open import Data.Product.Base hiding (map)
open import Function.Base as F
open import Level using (Level; _⊔_)
open import Relation.Unary using (IUniversal; _⇒_)
private
variable
l : Level
A : Set l
open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
import Data.Tree.AVL.Indexed strictTotalOrder as Indexed
open Indexed using (⊥⁺; ⊤⁺; ⊥⁺<⊤⁺; ⊥⁺<[_]<⊤⁺; ⊥⁺<[_]; [_]<⊤⁺)
------------------------------------------------------------------------
-- Re-export some core definitions publically
open Indexed using (K&_;_,_; toPair; fromPair; Value; MkValue; const) public
------------------------------------------------------------------------
-- Types and functions with hidden indices
data Tree {v} (V : Value v) : Set (a ⊔ v ⊔ ℓ₂) where
tree : ∀ {h} → Indexed.Tree V ⊥⁺ ⊤⁺ h → Tree V
module _ {v} {V : Value v} where
private
Val = Value.family V
empty : Tree V
empty = tree $′ Indexed.empty ⊥⁺<⊤⁺
singleton : (k : Key) → Val k → Tree V
singleton k v = tree (Indexed.singleton k v ⊥⁺<[ k ]<⊤⁺)
insert : (k : Key) → Val k → Tree V → Tree V
insert k v (tree t) = tree $′ proj₂ $ Indexed.insert k v t ⊥⁺<[ k ]<⊤⁺
insertWith : (k : Key) → (Maybe (Val k) → Val k) →
Tree V → Tree V
insertWith k f (tree t) = tree $′ proj₂ $ Indexed.insertWith k f t ⊥⁺<[ k ]<⊤⁺
delete : Key → Tree V → Tree V
delete k (tree t) = tree $′ proj₂ $ Indexed.delete k t ⊥⁺<[ k ]<⊤⁺
lookup : Tree V → (k : Key) → Maybe (Val k)
lookup (tree t) k = Indexed.lookup t k ⊥⁺<[ k ]<⊤⁺
module _ {v w} {V : Value v} {W : Value w} where
private
Val = Value.family V
Wal = Value.family W
map : ∀[ Val ⇒ Wal ] → Tree V → Tree W
map f (tree t) = tree $ Indexed.map f t
module _ {v} {V : Value v} where
private
Val = Value.family V
member : Key → Tree V → Bool
member k t = is-just (lookup t k)
headTail : Tree V → Maybe (K& V × Tree V)
headTail (tree (Indexed.leaf _)) = nothing
headTail (tree {h = suc _} t) with (k , _ , _ , t′) ← Indexed.headTail t
= just (k , tree (Indexed.castˡ ⊥⁺<[ _ ] t′))
initLast : Tree V → Maybe (Tree V × K& V)
initLast (tree (Indexed.leaf _)) = nothing
initLast (tree {h = suc _} t) with (k , _ , _ , t′) ← Indexed.initLast t
= just (tree (Indexed.castʳ t′ [ _ ]<⊤⁺) , k)
foldr : (∀ {k} → Val k → A → A) → A → Tree V → A
foldr cons nil (tree t) = Indexed.foldr cons nil t
-- The input does not need to be ordered.
fromList : List (K& V) → Tree V
fromList = List.foldr (uncurry insert ∘′ toPair) empty
-- Returns an ordered list.
toList : Tree V → List (K& V)
toList (tree t) = DiffList.toList (Indexed.toDiffList t)
size : Tree V → ℕ
size (tree t) = Indexed.size t
------------------------------------------------------------------------
-- Naive implementation of union
module _ {v w} {V : Value v} {W : Value w} where
private
Val = Value.family V
Wal = Value.family W
unionWith : (∀ {k} → Val k → Maybe (Wal k) → Wal k) →
-- left → right → result.
Tree V → Tree W → Tree W
unionWith f t₁ t₂ = foldr (λ {k} v → insertWith k (f v)) t₂ t₁
module _ {v} {V : Value v} where
private Val = Value.family V
-- Left-biased.
union : Tree V → Tree V → Tree V
union = unionWith F.const
unionsWith : (∀ {k} → Val k → Maybe (Val k) → Val k) → List (Tree V) → Tree V
unionsWith f ts = List.foldr (unionWith f) empty ts
-- Left-biased.
unions : List (Tree V) → Tree V
unions = unionsWith F.const
------------------------------------------------------------------------
-- Naive implementation of intersection
module _ {v w x} {V : Value v} {W : Value w} {X : Value x} where
private
Val = Value.family V
Wal = Value.family W
Xal = Value.family X
intersectionWith : (∀ {k} → Val k → Wal k → Xal k) →
Tree V → Tree W → Tree X
intersectionWith f t₁ t₂ = foldr cons empty t₁ where
cons : ∀ {k} → Val k → Tree X → Tree X
cons {k} v = case lookup t₂ k of λ where
nothing → id
(just w) → insert k (f v w)
module _ {v} {V : Value v} where
private
Val = Value.family V
-- Left-biased.
intersection : Tree V → Tree V → Tree V
intersection = intersectionWith F.const
intersectionsWith : (∀ {k} → Val k → Val k → Val k) →
List (Tree V) → Tree V
intersectionsWith f [] = empty
intersectionsWith f (t ∷ ts) = List.foldl (intersectionWith f) t ts
-- We are using foldl so that we are indeed forming t₁ ∩ ⋯ ∩ tₙ for
-- the input list [t₁,⋯,tₙ]. If we were to use foldr, we would form
-- t₂ ∩ ⋯ ∩ tₙ ∩ t₁ instead!
-- Left-biased.
intersections : List (Tree V) → Tree V
intersections = intersectionsWith F.const
------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.0
infixl 4 _∈?_
_∈?_ : ∀ {v} {V : Value v} → Key → Tree V → Bool
_∈?_ = member
{-# WARNING_ON_USAGE _∈?_
"Warning: _∈?_ was deprecated in v2.0.
Please use member instead."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4