Various AVL goodies (#1371)

Author: gallais

CHANGELOG.md

@@ -485,3 +485,49 @@ Other minor additions
   linesBy : Decidable P → String → List String
   lines   : String → List String
   ```
+
+* Added new functions to `Data.Tree.AVL`:
+  ```agda
+  foldr : (∀ {k} → Val k → A → A) → A → Tree V → A
+  size  : Tree V → ℕ
+
+  intersectionWith  : (∀ {k} → Val k → Wal k → Xal k) → Tree V → Tree W → Tree X
+  intersection      : Tree V → Tree V → Tree V
+  intersectionsWith : (∀ {k} → Val k → Val k → Val k) → List (Tree V) → Tree V
+  intersections     : List (Tree V) → Tree V
+  ```
+
+* Added new functions to `Data.Tree.AVL.Indexed`:
+  ```agda
+  foldr : (∀ {k} → Val k → A → A) → A → Tree V l u h → A
+  size  : Tree V → ℕ
+  ```
+
+* Added new functions to `Data.Tree.AVL.IndexedMap` module:
+  ```agda
+  foldr : (∀ {k} → Value k → A → A) → A → Map → A
+  size : Map → ℕ
+  ```
+
+* Added new functions to `Data.Tree.AVL.Map`:
+  ```agda
+  foldr : (Key → V → A → A) → A → Map V → A
+  size  : Map V → ℕ
+
+  intersectionWith  : (V → W → X) → Map V → Map W → Map X
+  intersection      : Map V → Map V → Map V
+  intersectionsWith : (V → V → V) → List (Map V) → Map V
+  intersections     : List (Map V) → Map V
+  ```
+
+* Added new functions to `Data.Tree.AVL.Sets`:
+  ```agda
+  foldr : (A → B → B) → B → ⟨Set⟩ → B
+  size  : ⟨Set⟩ → ℕ
+
+  union  : ⟨Set⟩ → ⟨Set⟩ → ⟨Set⟩
+  unions : List ⟨Set⟩ → ⟨Set⟩
+
+  intersection  : ⟨Set⟩ → ⟨Set⟩ → ⟨Set⟩
+  intersections : List ⟨Set⟩ → ⟨Set⟩
+  ```

src/Data/Tree/AVL.agda

@@ -21,13 +21,18 @@ module Data.Tree.AVL
 
 open import Data.Bool.Base using (Bool)
 import Data.DifferenceList as DiffList
-open import Data.List.Base as List using (List)
+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.Nat.Base using (ℕ; suc)
 open import Data.Product hiding (map)
-open import Function as F
-open import Level using (_⊔_)
-open import Relation.Unary
+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
@@ -84,7 +89,6 @@ module _ {v} {V : Value v} where
 
 
   infix 4 _∈?_
-
   _∈?_ : Key → Tree V → Bool
   k ∈? t = is-just (lookup k t)
 
@@ -98,6 +102,9 @@ module _ {v} {V : Value v} where
   initLast (tree {h = suc _} t)    with Indexed.initLast t
   ... | (k , _ , _ , 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
@@ -108,32 +115,71 @@ module _ {v} {V : Value v} where
   toList : Tree V → List (K& V)
   toList (tree t) = DiffList.toList (Indexed.toDiffList t)
 
-  -- Naive implementations of union.
+  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.
+              -- left → right → result.
               Tree V → Tree W → Tree W
-  unionWith f t₁ t₂ =
-    List.foldr (uncurry $ λ k v → insertWith k (f v)) t₂ (toList t₁)
-
-  -- Left-biased.
+  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 k t₂ 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

src/Data/Tree/AVL/Indexed.agda

@@ -11,7 +11,7 @@ open import Relation.Binary using (StrictTotalOrder)
 module Data.Tree.AVL.Indexed
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where
 
-open import Level using (_⊔_)
+open import Level using (Level; _⊔_)
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Product using (Σ; ∃; _×_; _,_; proj₁)
 open import Data.Maybe.Base using (Maybe; just; nothing)
@@ -22,6 +22,11 @@ open import Relation.Unary
 open import Relation.Binary using (_Respects_; Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
+private
+  variable
+    l : Level
+    A : Set l
+
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
 
 ------------------------------------------------------------------------
@@ -244,13 +249,20 @@ module _ {v} {V : Value v} where
   -- Converts the tree to an ordered list. Linear in the size of the
   -- tree.
 
+  foldr : ∀ {l u h} → (∀ {k} → Val k → A → A) → A → Tree V l u h → A
+  foldr cons nil (leaf l<u)             = nil
+  foldr cons nil (node (_ , v) l r bal) = foldr cons (cons v (foldr cons nil r)) l
+
   toDiffList : ∀ {l u h} → Tree V l u h → DiffList (K& V)
   toDiffList (leaf _)       = []
   toDiffList (node k l r _) = toDiffList l ++ k ∷ toDiffList r
 
   toList : ∀ {l u h} → Tree V l u h → List (K& V)
   toList t = toDiffList t List.[]
 
+  size : ∀ {l u h} → Tree V l u h → ℕ
+  size = List.length ∘′ toList
+
 module _ {v w} {V : Value v} {W : Value w} where
 
   private

src/Data/Tree/AVL/IndexedMap.agda

@@ -19,11 +19,17 @@ module Data.Tree.AVL.IndexedMap
   where
 
 import Data.Tree.AVL
-open import Data.Bool.Base
+open import Data.Bool.Base using (Bool)
 open import Data.List.Base as List using (List)
-open import Data.Maybe.Base as Maybe
-open import Function
-open import Level
+open import Data.Maybe.Base as Maybe using (Maybe)
+open import Data.Nat.Base using (ℕ)
+open import Function.Base
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    a : Level
+    A : Set a
 
 -- Key/value pairs.
 
@@ -76,8 +82,14 @@ headTail m = Maybe.map (Prod.map toKV id) (AVL.headTail m)
 initLast : Map → Maybe (Map × KV)
 initLast m = Maybe.map (Prod.map id toKV) (AVL.initLast m)
 
+foldr : (∀ {k} → Value k → A → A) → A → Map → A
+foldr cons = AVL.foldr cons
+
 fromList : List KV → Map
 fromList = AVL.fromList ∘ List.map fromKV
 
 toList : Map → List KV
 toList = List.map toKV ∘ AVL.toList
+
+size : Map → ℕ
+size = AVL.size

src/Data/Tree/AVL/Map.agda

@@ -17,78 +17,100 @@ module Data.Tree.AVL.Map
 open import Data.Bool.Base using (Bool)
 open import Data.List.Base using (List)
 open import Data.Maybe.Base using (Maybe)
+open import Data.Nat.Base using (ℕ)
 open import Data.Product using (_×_)
-open import Level using (_⊔_)
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    l v w x : Level
+    A : Set l
+    V : Set v
+    W : Set w
+    X : Set x
 
 import Data.Tree.AVL strictTotalOrder as AVL
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
 
 ------------------------------------------------------------------------
 -- The map type
 
-Map : ∀ {v} → (V : Set v) → Set (a ⊔ v ⊔ ℓ₂)
-Map v = AVL.Tree (AVL.const v)
+Map : (V : Set v) → Set (a ⊔ v ⊔ ℓ₂)
+Map V = AVL.Tree (AVL.const V)
 
 ------------------------------------------------------------------------
 -- Repackaged functions
 
-module _ {v} {V : Set v} where
+empty : Map V
+empty = AVL.empty
+
+singleton : Key → V → Map V
+singleton = AVL.singleton
 
-  empty : Map V
-  empty = AVL.empty
+insert : Key → V → Map V → Map V
+insert = AVL.insert
 
-  singleton : Key → V → Map V
-  singleton = AVL.singleton
+insertWith : Key → (Maybe V → V) → Map V → Map V
+insertWith = AVL.insertWith
 
-  insert : Key → V → Map V → Map V
-  insert = AVL.insert
+delete : Key → Map V → Map V
+delete = AVL.delete
 
-  insertWith : Key → (Maybe V → V) → Map V → Map V
-  insertWith = AVL.insertWith
+lookup : Key → Map V → Maybe V
+lookup = AVL.lookup
 
-  delete : Key → Map V → Map V
-  delete = AVL.delete
+map : (V → W) → Map V → Map W
+map f = AVL.map f
 
-  lookup : Key → Map V → Maybe V
-  lookup = AVL.lookup
+infix 4 _∈?_
+_∈?_ : Key → Map V → Bool
+_∈?_ = AVL._∈?_
 
-module _ {v w} {V : Set v} {W : Set w} where
+headTail : Map V → Maybe ((Key × V) × Map V)
+headTail = AVL.headTail
 
-  map : (V → W) → Map V → Map W
-  map f = AVL.map f
+initLast : Map V → Maybe (Map V × (Key × V))
+initLast = AVL.initLast
 
-module _ {v} {V : Set v} where
+foldr : (Key → V → A → A) → A → Map V → A
+foldr cons = AVL.foldr (λ {k} → cons k)
 
-  infix 4 _∈?_
+fromList : List (Key × V) → Map V
+fromList = AVL.fromList
 
-  _∈?_ : Key → Map V → Bool
-  _∈?_ = AVL._∈?_
+toList : Map V → List (Key × V)
+toList = AVL.toList
 
-  headTail : Map V → Maybe ((Key × V) × Map V)
-  headTail = AVL.headTail
+size : Map V → ℕ
+size = AVL.size
 
-  initLast : Map V → Maybe (Map V × (Key × V))
-  initLast = AVL.initLast
+------------------------------------------------------------------------
+-- Naïve implementations of union
 
-  fromList : List (Key × V) → Map V
-  fromList = AVL.fromList
+unionWith : (V → Maybe W → W) →
+            Map V → Map W → Map W
+unionWith f = AVL.unionWith f
 
-  toList : Map V → List (Key × V)
-  toList = AVL.toList
+union : Map V → Map V → Map V
+union = AVL.union
 
-module _ {v w} {V : Set v} {W : Set w} where
+unionsWith : (V → Maybe V → V) → List (Map V) → Map V
+unionsWith f = AVL.unionsWith f
 
-  unionWith : (V → Maybe W → W) →
-              Map V → Map W → Map W
-  unionWith f = AVL.unionWith f
+unions : List (Map V) → Map V
+unions = AVL.unions
+
+------------------------------------------------------------------------
+-- Naïve implementations of intersection
 
-module _ {v} {V : Set v} where
+intersectionWith : (V → W → X) → Map V → Map W → Map X
+intersectionWith f = AVL.intersectionWith f
 
-  union : Map V → Map V → Map V
-  union = AVL.union
+intersection : Map V → Map V → Map V
+intersection = AVL.intersection
 
-  unionsWith : (V → Maybe V → V) → List (Map V) → Map V
-  unionsWith f = AVL.unionsWith f
+intersectionsWith : (V → V → V) → List (Map V) → Map V
+intersectionsWith f = AVL.intersectionsWith f
 
-  unions : List (Map V) → Map V
-  unions = AVL.unions
+intersections : List (Map V) → Map V
+intersections = AVL.intersections