------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing how the AVL tree module can be used
------------------------------------------------------------------------

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

module README.Data.Tree.AVL where

------------------------------------------------------------------------
-- Setup

-- AVL trees are defined in Data.Tree.AVL.

import Data.Tree.AVL

-- This module is parametrised by keys, which have to form a (strict)
-- total order, and values, which are indexed by keys. Let us use
-- natural numbers as keys and vectors of strings as values.

open import Data.Nat.Properties using (<-strictTotalOrder)
open import Data.Product.Base as Product using (_,_; _,′_)
open import Data.String.Base using (String)
open import Data.Vec.Base using (Vec; _∷_; [])
open import Relation.Binary.PropositionalEquality

open Data.Tree.AVL <-strictTotalOrder renaming (Tree to Tree′)
Tree = Tree′ (MkValue (Vec String) (subst (Vec String)))

-- The first argument to `MkValue` should be a function from a key
-- (a `ℕ` in this case) to a value type (a `String` vector type).
-- Since `(Vec String)` is missing `Vec`'s second parameter, a `ℕ`,
-- it's equivalent to `λ n → Vec String n`.

-- The second argument to `MkValue` is a function that can accept
-- a proof that two keys are equal, and then substitute a unique key
-- for an equivalent key that is passed in.  Applying `subst` to the
-- key-to-value-type function passed as `MkValue`'s first argument is
-- a normal way to create such a function.

-- Note that there is no need to define the type of keys separately:
-- passing a key-to-value-type function to `MkValue` and providing
-- the result of `MkValue` to `Data.Tree.AVL.Tree` is enough.

------------------------------------------------------------------------
-- Construction of trees

-- Some values.

v₁  = "cepa" ∷ []
v₁′ = "depa" ∷ []
v₂  = "apa" ∷ "bepa" ∷ []

-- Empty and singleton trees.

t₀ : Tree
t₀ = empty

t₁ : Tree
t₁ = singleton 2 v₂

-- Insertion of a key-value pair into a tree.

t₂ = insert 1 v₁ t₁

-- If you insert a key-value pair and the key already exists in the
-- tree, then the old value is thrown away.

t₂′ = insert 1 v₁′ t₂

-- Deletion of the mapping for a certain key.

t₃ = delete 2 t₂

-- Conversion of a list of key-value mappings to a tree.

open import Data.List.Base using (_∷_; [])

t₄ : Tree
t₄ = fromList ((2 , v₂) ∷ (1 , v₁) ∷ [])

------------------------------------------------------------------------
-- Queries

-- Let us formulate queries as unit tests.

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

-- Searching for a key.

open import Data.Bool.Base using (true; false)
open import Data.Maybe.Base as Maybe using (just; nothing)

q₀ : lookup t₂ 2 ≡ just v₂
q₀ = refl

q₁ : lookup t₃ 2 ≡ nothing
q₁ = refl

q₂ : (3 ∈? t₂) ≡ false
q₂ = refl

q₃ : (1 ∈? t₄) ≡ true
q₃ = refl

-- Turning a tree into a sorted list of key-value pairs.

q₄ : toList t₁ ≡ (2 , v₂) ∷ []
q₄ = refl

q₅ : toList t₂ ≡ (1 , v₁) ∷ (2 , v₂) ∷ []
q₅ = refl

q₅′ : toList t₂′ ≡ (1 , v₁′) ∷ (2 , v₂) ∷ []
q₅′ = refl

------------------------------------------------------------------------
-- Views

-- Partitioning a tree into the smallest element plus the rest, or the
-- largest element plus the rest.

open import Function.Base using (id)

v₆ : headTail t₀ ≡ nothing
v₆ = refl

v₇ : Maybe.map (Product.map₂ toList) (headTail t₂) ≡
     just ((1 , v₁) , ((2 , v₂) ∷ []))
v₇ = refl

v₈ : initLast t₀ ≡ nothing
v₈ = refl

v₉ : Maybe.map (Product.map₁ toList) (initLast t₄) ≡
     just (((1 , v₁) ∷ []) ,′ (2 , v₂))
v₉ = refl

------------------------------------------------------------------------
-- Further reading

-- Variations of the AVL tree module are available:

-- • Finite maps in which types of values don't depend on keys.

import Data.Tree.AVL.Map

-- • Finite maps with indexed keys and values.

import Data.Tree.AVL.IndexedMap

-- • Finite sets.

import Data.Tree.AVL.Sets