-- Finite maps as association lists
module Prelude.AssocList where

open import Prelude.Init
open import Prelude.DecEq
open import Prelude.Decidable
open import Prelude.Irrelevance
open import Prelude.Default

AssocList : Type → Type → Type
AssocList K V = List (K × V)

mapValues : ∀ {K V V′} → (V → V′) → AssocList K V → AssocList K V′
mapValues f = map (map₂ f)

module _ {K V : Type} where
  _∈ᵐ_ _∉ᵐ_ : K → AssocList K V → Type
  k ∈ᵐ m = AnyFirst ((k ≡_) ∘ proj₁) m
  k ∉ᵐ m = ·¬ (k ∈ᵐ m)

  ∈ᵐ-irrelevant : ∀ {k m} → Irrelevant (k ∈ᵐ m)
  ∈ᵐ-irrelevant = AnyFirst-irrelevant λ where refl refl → refl

  _∪_ : Op₂ (AssocList K V)
  _∪_ = _++_

  module _ ⦃ _ : DecEq K ⦄ where

    _∈ᵐ?_ = ¿ _∈ᵐ_ ¿²
    _∉ᵐ?_ = ¿ _∉ᵐ_ ¿²

    _‼_ : ∀ {k : K} (m : AssocList K V) → k ∈ᵐ m → V
    m ‼ p = L.First.satisfied p .proj₁ .proj₂

    opaque
      _⁉_ : AssocList K V → K → Maybe V
      m ⁉ k with k ∈ᵐ? m
      ... | yes p = just (m ‼ p)
      ... | no  _ = nothing

    module _ {k : K} {m : AssocList K V} where
      _∷~_ : k ∈ᵐ m → (V → V) → AssocList K V
      p ∷~ f = m [ L.First.index p ]∷= (k , f (m ‼ p))

      _∷=_ : k ∈ᵐ m → V → AssocList K V
      p ∷= v = p ∷~ const v

    module _ ⦃ _ : Default V ⦄ where

      modify : K → (V → V) → Op₁ (AssocList K V)
      modify k f m with k ∈ᵐ? m
      ... | no _  = (k , f def) ∷ m
      ... | yes p = p ∷= f (m ‼ p)

      opaque
        set : K → V → Op₁ (AssocList K V)
        set k v = modify k (const v)

      _‼d_ : AssocList K V → K → V
      m ‼d k with m ⁉ k
      ... | nothing = def
      ... | just v  = v

      postulate -- TODO: proof
        get∘set≡id : ∀ {k : K} {v : V} {m : AssocList K V}
          → set k v m ⁉ k ≡ just v

        k'≢k-get∘set : ∀ {k k' : K} {v : V} {m : AssocList K V}
          → k' ≢ k
          → set k' v m ⁉ k ≡ m ⁉ k

        k'≢k-set-assoc : ∀ {k k' : K} {v v' : V} {m : AssocList K V}
          → k' ≢ k
          → set k v (set k' v' m) ≡ set k' v' (set k v m)

      k'≢k-get∘set∘set : ∀ {k k' : K} {v v' : V} {m : AssocList K V}
        → k' ≢ k
        → set k v (set k' v' m) ⁉ k ≡ set k v m ⁉ k
      k'≢k-get∘set∘set {k} {k'} {v} {v'} {m} p =
        trans
          (cong (_⁉ k) (k'≢k-set-assoc {k} {k'} {v} {v'} {m} p))
          (k'≢k-get∘set {k} {k'} {v'} {m = set k v m} p)