------------------------------------------------------------------------ -- 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". open import Relation.Binary open import Relation.Binary.PropositionalEquality as P using (_≡_) module Data.AVL {k v ℓ} {Key : Set k} (Value : Key → Set v) {_<_ : Rel Key ℓ} (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where open import Data.Bool import Data.DifferenceList as DiffList open import Data.Empty open import Data.List as List using (List) open import Data.Maybe hiding (map) open import Data.Nat hiding (_<_; compare; _⊔_) open import Data.Product hiding (map) open import Data.Unit open import Function open import Level using (_⊔_; Lift; lift) open IsStrictTotalOrder isStrictTotalOrder ------------------------------------------------------------------------ -- Extended keys module Extended-key where -- The key type extended with a new minimum and maximum. data Key⁺ : Set k where ⊥⁺ ⊤⁺ : Key⁺ [_] : (k : Key) → Key⁺ -- An extended strict ordering relation. infix 4 _<⁺_ _<⁺_ : Key⁺ → Key⁺ → Set ℓ ⊥⁺ <⁺ [ _ ] = Lift ⊤ ⊥⁺ <⁺ ⊤⁺ = Lift ⊤ [ x ] <⁺ [ y ] = x < y [ _ ] <⁺ ⊤⁺ = Lift ⊤ _ <⁺ _ = Lift ⊥ -- A pair of ordering constraints. infix 4 _<_<_ _<_<_ : Key⁺ → Key → Key⁺ → Set ℓ l < x < u = l <⁺ [ x ] × [ x ] <⁺ u -- _<⁺_ is transitive. trans⁺ : ∀ l {m u} → l <⁺ m → m <⁺ u → l <⁺ u trans⁺ [ l ] {m = [ m ]} {u = [ u ]} l _ _ k′ _ _ _ = joinʳ⁻ _ p lp (delete k pu) bal ... | tri≈ _ _ _ = join lp pu bal -- Looks up a key. Logarithmic in the size of the tree (assuming -- constant-time comparisons). lookup : ∀ {l u h} → (k : Key) → Tree l u h → Maybe (Value k) lookup k (leaf _) = nothing lookup k (node (k′ , v) lk′ k′u _) with compare k k′ ... | tri< _ _ _ = lookup k lk′ ... | tri> _ _ _ = lookup k k′u ... | tri≈ _ eq _ rewrite eq = just v -- Maps a function over all values in the tree. map : (∀ {k} → Value k → Value k) → ∀ {l u h} → Tree l u h → Tree l u h map f (leaf l