KV.agda

module KV where

open import Data.Nat hiding (_⊔_)
open import Data.Unit
open import Data.List using (List; []; _∷_)
open import Data.Empty
open import Data.Maybe
open import Data.Product
open import Function
open import Relation.Binary.Core
open import Level as L using (Level; _⊔_)

⟨_⟩₃₋₁ : ∀ {a} {A B C : Set a} → (A × B × C) → A
⟨_⟩₃₋₁ (a , _ , _) = a

⟨_⟩₃₋₂ : ∀ {a} {A B C : Set a} → (A × B × C) → B
⟨_⟩₃₋₂ (_ , b , _) = b

⟨_⟩₃₋₃ : ∀ {a} {A B C : Set a} → (A × B × C) → C
⟨_⟩₃₋₃ (_ , _ , c) = c

record KV-Storage : Set₁ where
  field
    Storage : Set → Set → Set
    new-key : ∀ {K V} → Storage K V → K × Storage K V
    -- Read / Write
    _[_]   : ∀ {K V} → Storage K V → K → Maybe V
    _[_]=_ : ∀ {K V} → Storage K V → K → V → Storage K V
    -- Properties
    k-uniq : ∀ {K V} → {kvs : Storage K V} → {k : K}
           → Σ V (λ v → kvs [ k ] ≡ just v) → proj₁ (new-key kvs) ≢ k
    kv-overwrite : ∀ {K V} → {k1 k2 : K} → {v1 v2 : V} → {kvs : Storage K V}
                 → (k1 ≡ k2) → ((kvs [ k1 ]= v1) [ k2 ]= v2) [ k1 ] ≡ just v2

  add : ∀ {K E} → K → E → Storage K (E × ℕ × K) → Storage K (E × ℕ × K)
  add {K} {E} k e′ db = maybe′ (λ r → walk k db ⟨ r ⟩₃₋₂ r) db (db [ k ])
    where
      DB = Storage K (E × ℕ × K)
      walk : K → DB → ℕ → (E × ℕ × K) → DB
      walk k db (suc m) (e , n , k′) = maybe′ (walk k′ (db [ k ]= (e , suc n , k′)) m) db (db [ k′ ])
      walk k db zero    (e , n , _ ) with new-key db
      ... | (k′ , db′) = (db′ [ k′ ]= (e′ , zero , k′)) [ k ]= (e , n , k′)

  to-list : ∀ {K E} → K → Storage K (E × ℕ × K) → List E
  to-list {K} {E} k db = maybe′ (λ r → walk ⟨ r ⟩₃₋₂ k) [] (db [ k ])
    where
      walk : ℕ → K → List E
      walk zero    _ = []
      walk (suc n) k = maybe′ (λ r → ⟨ r ⟩₃₋₁ ∷ walk n ⟨ r ⟩₃₋₃) [] (db [ k ])