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
| 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
|
