Edit: Look ma, no Maybe :: hpaste

Edit: Look ma, no Maybe

Title:

Author:

Language:

Channel:

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

Email: