Skip to content

Instantly share code, notes, and snippets.

@clayrat

clayrat/KVList.agda

Created September 24, 2024 21:01
Show Gist options
  • Save clayrat/8dad6a8efd7a78c38b68feed6737c554 to your computer and use it in GitHub Desktop.
Save clayrat/8dad6a8efd7a78c38b68feed6737c554 to your computer and use it in GitHub Desktop.
Download ZIP
KV lists
Raw
KVList.agda
open import Prelude
open import Data.Empty
open import Data.Bool
open import Data.Maybe
open import Data.List
open import Data.List.Correspondences.Unary.All
open import Data.List.Correspondences.Unary.Related
open import Data.Reflects
open import Data.Tri renaming (elim to elimᵗ ; rec to recᵗ)
open import Order.Strict
open import Order.Trichotomous
module KVList
{o ℓᵏ ℓᵛ : Level}
{K : StrictPoset o ℓᵏ}
{V : 𝒰 ℓᵛ}
⦃ d : is-trichotomous K ⦄
where
open StrictPoset K public
lookup-kv : List (Ob × V) → Ob → Maybe V
lookup-kv [] k = nothing
lookup-kv ((x , v) ∷ l) k =
caseᵗ k >=< x
lt⇒ nothing
eq⇒ just v
gt⇒ lookup-kv l k
upsert-kv : List (Ob × V) → Ob → (V → V) → V → List (Ob × V) × Maybe V
upsert-kv [] k f v = (k , v) ∷ [] , nothing
upsert-kv l0@((x , w) ∷ l) k f v =
caseᵗ k >=< x
lt⇒ ((k , v) ∷ l0 , nothing)
eq⇒ ((k , f w) ∷ l , just w)
gt⇒ (first ((x , w) ∷_) (upsert-kv l k f v))
remove-kv : List (Ob × V) → Ob → List (Ob × V) × Maybe V
remove-kv [] k = [] , nothing
remove-kv l0@((x , w) ∷ l) k =
caseᵗ k >=< x
lt⇒ (l0 , nothing)
eq⇒ (l , just w)
gt⇒ (first ((x , w) ∷_) (remove-kv l k))
keys : List (Ob × V) → List Ob
keys = map fst
values : List (Ob × V) → List V
values = map snd
keys-++ : ∀ {xs ys} → keys (xs ++ ys) ＝ keys xs ++ keys ys
keys-++ {xs} {ys} = map-++ fst xs ys
lookup-empty : lookup-kv [] ＝ λ _ → nothing
lookup-empty = refl
lookup-related : ∀ {k xs}
→ Related _<_ k (keys xs) → lookup-kv xs k ＝ nothing {- is-nothing? -}
lookup-related {xs = []} r = refl
lookup-related {k} {xs = (x , v) ∷ xs} (rx ∷ʳ r) =
caseᵗ k >=< x
return (λ q → recᵗ nothing (just v) (lookup-kv xs k) q ＝ nothing)
of λ where
(lt _ _ _) → refl
(eq x≮y _ _) → absurd (x≮y rx)
(gt x≮y _ _) → absurd (x≮y rx)
lookup-sorted-cat-cons-cat : ∀ {xs ys k k′ v′}
→ Sorted _<_ (keys (xs ++ (k′ , v′) ∷ ys))
→ lookup-kv (xs ++ (k′ , v′) ∷ ys) k ＝ (if ⌊ d .is-trichotomous.trisect k k′ ⌋<
then lookup-kv xs k
else lookup-kv ((k′ , v′) ∷ ys) k)
lookup-sorted-cat-cons-cat {xs = []} {ys} {k} {k′} {v′} s =
caseᵗ k >=< k′
return (λ q → recᵗ nothing (just v′) (lookup-kv ys k) q
＝ (if ⌊ q ⌋< then nothing else recᵗ nothing (just v′) (lookup-kv ys k) q))
of λ where
(lt x<y x≠y y≮x) → refl
(eq x≮y x=y y≮x) → refl
(gt x≮y x≠y y<x) → refl
lookup-sorted-cat-cons-cat {xs = (x , v) ∷ xs} {ys} {k} {k′} {v′} (∷ˢ r) =
let a = related→all (record { _∙_ = <-trans }) $ subst (λ q → Related _<_ x q) (keys-++ {xs = xs}) r
a0 , a′ = all-split {xs = keys xs} a
x<k′ , a1 = all-uncons a′
in
caseᵗ k >=< x
return (λ q → recᵗ nothing (just v) (lookup-kv (xs ++ (k′ , v′) ∷ ys) k) q
＝ (if ⌊ d .is-trichotomous.trisect k k′ ⌋<
then recᵗ nothing (just v) (lookup-kv xs k) q
else recᵗ nothing (just v′) (lookup-kv ys k) (d .is-trichotomous.trisect k k′)))
of λ where
(lt k<x k≠x x≮k) →
given-lt <-trans k<x x<k′
return (λ q → nothing ＝ (if ⌊ q ⌋< then nothing else recᵗ nothing (just v′) (lookup-kv ys k) q))
then refl
(eq k≮x k=x y≮x) →
given-lt subst (_< k′) (k=x ⁻¹) x<k′
return (λ q → just v ＝ (if ⌊ q ⌋< then just v else recᵗ nothing (just v′) (lookup-kv ys k) q))
then refl
(gt k≮x k≠x x<k) →
lookup-sorted-cat-cons-cat (related→sorted r)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment