open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P

module KV
(Key Value : Set)
(isDecEquivalence : IsDecEquivalence {A = Key} _≡_)
where

open import Relation.Nullary
open import Data.Empty
open import Data.Sum renaming ([_,_] to [[_,,_]])
open import Data.Product
open import Data.List
open import Data.Maybe
open import Function

open IsDecEquivalence isDecEquivalence

mutual
  data KV : Set where
    [] : KV
    _⇒_∷_⊣_ : (k : Key)(v : Value)(kv : KV) -> ¬(k keyOf kv) -> KV

  _keyOf_ : Key -> KV -> Set
  k keyOf [] = ⊥
  k₁ keyOf (k₂ ⇒ v ∷ kv ⊣  w) = k₁ ≡ k₂ ⊎ k₁ keyOf kv

_⇒_∈_ : Key -> Value -> KV -> Set
k ⇒ v ∈ [] = ⊥
k₁ ⇒ v₁ ∈ (k₂ ⇒ v₂ ∷ kv ⊣ y) = k₁ ≡ k₂ × v₁ ≡ v₂ ⊎ k₁ ⇒ v₁ ∈ kv

strip : ∀ {k v kv} -> k ⇒ v ∈ kv -> k keyOf kv
strip {kv = []} ()
strip {kv = k ⇒ v ∷ kv ⊣ y} (inj₁ x) = inj₁ (proj₁ x)
strip {kv = k ⇒ v ∷ kv ⊣ y} (inj₂ x) = inj₂ (strip x)

find : ∀ {k} kv -> k keyOf kv -> ∃ λ v -> k ⇒ v ∈ kv
find [] ()
find (k ⇒ v ∷ kv ⊣ y) (inj₁ x) = v , inj₁ (x , P.refl)
find (k ⇒ v ∷ kv ⊣ y) (inj₂ x) with find kv x
find (k ⇒ v ∷ kv ⊣ y) (inj₂ x) | v' , p = v' , inj₂ p

toList : KV -> List (Key × Value)
toList [] = []
toList (k ⇒ v ∷ kv ⊣ y) = (k , v) ∷ toList kv

_keyOf?_ : Decidable _keyOf_
k keyOf? [] = no id
k₁ keyOf? (k₂ ⇒ v ∷ kv ⊣ y) with k₁ ≟ k₂
k₁ keyOf? (k₂ ⇒ v ∷ kv ⊣ y) | yes p = yes (inj₁ p)
k₁ keyOf? (k₂ ⇒ v ∷ kv ⊣ y) | no ¬p with k₁ keyOf? kv
k₁ keyOf? (k₂ ⇒ v ∷ kv ⊣ y) | no ¬p | yes q = yes (inj₂ q)
k₁ keyOf? (k₂ ⇒ v ∷ kv ⊣ y) | no ¬p | no ¬q = no [[ ¬p ,, ¬q ]]

data Lookup : Key -> KV -> Set where
  not-found : ∀{k kv} -> ¬(k keyOf kv) -> Lookup k kv
  found : ∀ {k kv} -> (∃ λ v -> k ⇒ v ∈ kv) -> Lookup k kv

lookup : (k : Key)(kv : KV) -> Lookup k kv
lookup k kv with k keyOf? kv
lookup k kv | yes p = found (find kv p)
lookup k kv | no ¬p = not-found ¬p