/usr/share/agda-stdlib/Data/AVL/IndexedMap.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite maps with indexed keys and values, based on AVL trees
------------------------------------------------------------------------
open import Data.Product as Prod
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_)
module Data.AVL.IndexedMap
{i k v ℓ}
{Index : Set i} {Key : Index → Set k} (Value : Index → Set v)
{_<_ : Rel (∃ Key) ℓ}
(isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
where
open import Category.Functor
import Data.AVL
open import Data.Bool
open import Data.List as List using (List)
open import Data.Maybe as Maybe
open import Function
open import Level
open RawFunctor (Maybe.functor {f = i ⊔ k ⊔ v ⊔ ℓ})
-- Key/value pairs.
KV : Set (i ⊔ k ⊔ v)
KV = ∃ λ i → Key i × Value i
-- Conversions.
private
fromKV : KV → Σ[ ik ∶ ∃ Key ] Value (proj₁ ik)
fromKV (i , k , v) = ((i , k) , v)
toKV : Σ[ ik ∶ ∃ Key ] Value (proj₁ ik) → KV
toKV ((i , k) , v) = (i , k , v)
-- The map type.
private
open module AVL =
Data.AVL (λ ik → Value (proj₁ ik)) isStrictTotalOrder
public using () renaming (Tree to Map)
-- Repackaged functions.
empty : Map
empty = AVL.empty
singleton : ∀ {i} → Key i → Value i → Map
singleton k v = AVL.singleton (, k) v
insert : ∀ {i} → Key i → Value i → Map → Map
insert k v = AVL.insert (, k) v
delete : ∀ {i} → Key i → Map → Map
delete k = AVL.delete (, k)
lookup : ∀ {i} → Key i → Map → Maybe (Value i)
lookup k m = AVL.lookup (, k) m
_∈?_ : ∀ {i} → Key i → Map → Bool
_∈?_ k = AVL._∈?_ (, k)
headTail : Map → Maybe (KV × Map)
headTail m = Prod.map toKV id <$> AVL.headTail m
initLast : Map → Maybe (Map × KV)
initLast m = Prod.map id toKV <$> AVL.initLast m
fromList : List KV → Map
fromList = AVL.fromList ∘ List.map fromKV
toList : Map → List KV
toList = List.map toKV ∘ AVL.toList
|