KV lists

KVList.agda

open import Prelude
open import Data.Empty
open import Data.Bool renaming (elim to elimᵇ ; rec to recᵇ)
open import Data.Maybe
open import Data.List
open import Data.List.Operations.Discrete
open import Data.List.Correspondences.Unary.All
open import Data.List.Correspondences.Unary.Has
open import Data.List.Correspondences.Unary.Related
open import Data.List.Correspondences.Binary.Perm
open import Data.Dec
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

  Is-kvlist : List (Ob × V) → 𝒰 (o ⊔ ℓᵏ)
  Is-kvlist xs = Sorted _<_ (keys xs)

  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

  Is-kvlist-empty : Is-kvlist []
  Is-kvlist-empty = []ˢ

  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′}
                             → Is-kvlist (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)

  kvlist-upsert-perm : {k : Ob} {v : V} {f : V → V} {xs : List (Ob × V)}
                     → Is-kvlist xs
                     → Perm (keys (fst (upsert-kv xs k f v)))
                            (if has ⦃ d = Tri→discrete ⦄ k (keys xs)
                               then keys xs
                               else k ∷ keys xs)
  kvlist-upsert-perm {k} {v} {f} {xs = []}             ikv = perm-refl
  kvlist-upsert-perm {k} {v} {f} {xs = (k′ , v′) ∷ xs} (∷ˢ r) = 
    caseᵗ k >=< k′
      return (λ q → Perm (keys (fst (recᵗ ((k , v) ∷ (k′ , v′) ∷ xs , nothing)
                                          ((k , f v′) ∷ xs , just v′)
                                          (first ((k′ , v′) ∷_ ) (upsert-kv xs k f v))
                                          q)))
                         (if ⌊ ⌊ q ⌋≟ ⌋ or has ⦃ d = Tri→discrete ⦄ k (keys xs)
                            then k′ ∷ keys xs
                            else k ∷ k′ ∷ keys xs))
      of λ where
            (lt _ _ k′≮k) → 
              elimᵇ {P = λ q → has ⦃ d = Tri→discrete ⦄ k (keys xs) ＝ q
                             → Perm (k ∷ k′ ∷ keys xs) 
                                    (if q then k′ ∷ keys xs else k ∷ k′ ∷ keys xs)}
                    (λ x → let hask = so→true! ⦃ Reflects-has ⦃ d = Tri→discrete ⦄ {xs = keys xs} ⦄ $ so≃is-true ⁻¹ $ x
                               all>k′ = related→all (record { _∙_ = <-trans }) r
                             in
                           absurd (k′≮k (All→∀Has all>k′ k hask)))
                    (λ _ → perm-refl)
                    (has ⦃ d = Tri→discrete ⦄ k (keys xs))
                    refl
            (eq _ k=k′ _) → pprep k=k′ perm-refl
            (gt _ _ _) →
               elimᵇ {P = λ q → Perm (keys (fst (upsert-kv xs k f v)))
                                     (if q then keys xs else k ∷ keys xs)
                              → Perm (k′ ∷ keys (fst (upsert-kv xs k f v)))
                                     (if q then k′ ∷ keys xs else k ∷ k′ ∷ keys xs)}
                      (pprep refl)
                      (λ p → ptrans (pprep refl p) (perm-cons-cat-commassoc {xs = k ∷ []}))
                      (has ⦃ d = Tri→discrete ⦄ k (keys xs))
                      (kvlist-upsert-perm {k = k} {v = v} {f = f} {xs = xs} (related→sorted r))