------------------------------------------------------------------------
-- The Agda standard library
--
-- Maps from keys to values, based on AVL trees
-- This modules provides a simpler map interface, without a dependency
-- between the key and value types.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (StrictTotalOrder)
module Data.Tree.AVL.Map
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
where
open import Data.Bool.Base using (Bool)
open import Data.List.Base as List using (List)
open import Data.Maybe.Base as Maybe using (Maybe)
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base as Prod using (_×_)
open import Function.Base 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 : Set v) → Set (a ⊔ v ⊔ ℓ₂)
Map V = AVL.Tree (AVL.const V)
------------------------------------------------------------------------
-- Repackaged functions
empty : Map V
empty = AVL.empty
singleton : Key → V → Map V
singleton = AVL.singleton
insert : Key → V → Map V → Map V
insert = AVL.insert
insertWith : Key → (Maybe V → V) → Map V → Map V
insertWith = AVL.insertWith
delete : Key → Map V → Map V
delete = AVL.delete
lookup : Map V → Key → Maybe V
lookup = AVL.lookup
map : (V → W) → Map V → Map W
map f = AVL.map f
member : Key → Map V → Bool
member = AVL.member
headTail : Map V → Maybe ((Key × V) × Map V)
headTail = Maybe.map (Prod.map₁ AVL.toPair) ∘′ AVL.headTail
initLast : Map V → Maybe (Map V × (Key × V))
initLast = Maybe.map (Prod.map₂ AVL.toPair) ∘′ AVL.initLast
foldr : (Key → V → A → A) → A → Map V → A
foldr cons = AVL.foldr (λ {k} → cons k)
fromList : List (Key × V) → Map V
fromList = AVL.fromList ∘′ List.map AVL.fromPair
toList : Map V → List (Key × V)
toList = List.map AVL.toPair ∘′ AVL.toList
size : Map V → ℕ
size = AVL.size
------------------------------------------------------------------------
-- Naïve implementations of union
unionWith : (V → Maybe W → W) →
Map V → Map W → Map W
unionWith f = AVL.unionWith f
union : Map V → Map V → Map V
union = AVL.union
unionsWith : (V → Maybe V → V) → List (Map V) → Map V
unionsWith f = AVL.unionsWith f
unions : List (Map V) → Map V
unions = AVL.unions
------------------------------------------------------------------------
-- Naïve implementations of intersection
intersectionWith : (V → W → X) → Map V → Map W → Map X
intersectionWith f = AVL.intersectionWith f
intersection : Map V → Map V → Map V
intersection = AVL.intersection
intersectionsWith : (V → V → V) → List (Map V) → Map V
intersectionsWith f = AVL.intersectionsWith f
intersections : List (Map V) → Map V
intersections = AVL.intersections
------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.0
infixl 4 _∈?_
_∈?_ : Key → Map 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