------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite maps with indexed keys and values, based on AVL trees
------------------------------------------------------------------------

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

open import Data.Product.Base
  using (map₁; map₂; ∃; _×_; Σ-syntax; proj₁; _,_; -,_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Structures using (IsStrictTotalOrder)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
import Data.Tree.AVL.Value

module Data.Tree.AVL.IndexedMap
  {i k v ℓ}
  {Index : Set i} {Key : Index → Set k}  (Value : Index → Set v)
  {_<_ : Rel (∃ Key) ℓ}
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
  where

import Data.Tree.AVL
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 Function.Base
open import Level using (Level; _⊔_)

private
  variable
    a : Level
    A : Set a

-- 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.Tree.AVL (record { isStrictTotalOrder = isStrictTotalOrder })
    using () renaming (Tree to Map′)

Map = Map′ (AVL.MkValue (Value ∘ proj₁) (subst Value ∘′ cong proj₁))

-- 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} → Map → Key i → Maybe (Value i)
lookup m k = AVL.lookup m (-, k)

member : ∀ {i} → Key i → Map → Bool
member k = AVL.member (-, k)

headTail : Map → Maybe (KV × Map)
headTail m = Maybe.map (map₁ (toKV ∘′ AVL.toPair)) (AVL.headTail m)

initLast : Map → Maybe (Map × KV)
initLast m = Maybe.map (map₂ (toKV ∘′ AVL.toPair)) (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 (AVL.fromPair ∘′ fromKV)

toList : Map → List KV
toList = List.map (toKV ∘′ AVL.toPair) ∘ AVL.toList

size : Map → ℕ
size = AVL.size


------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

infixl  _∈?_
_∈?_ : ∀ {i} → Key i → Map → Bool
_∈?_ = member
{-# WARNING_ON_USAGE _∈?_
"Warning: _∈?_ was deprecated in v2.0.
Please use member instead."
#-}