{-# OPTIONS --with-K #-}
module Prelude.Maps.Examples where

open import Prelude.Init; open SetAsType
open import Prelude.DecEq
open import Prelude.Semigroup
open import Prelude.Monoid
open import Prelude.FromList

private
  module Implementation1 {K V : Type} ⦃ _ : DecEq K ⦄ where
    open import Prelude.Maps.Abstract.Interface
    import Prelude.Maps.AsPartialFunctions {K = K} {V = V} as Imp
    imp : FinMapᴵ K V 0ℓ
    imp = record {mapᴵ = record {Imp}; Imp}
    open FinMapᴵ imp public

  module Implementation2 {K V : Type} ⦃ _ : DecEq K ⦄ ⦃ _ : DecEq V ⦄ where
    open import Prelude.Maps.Abstract.Interface
    import Prelude.Maps.AsSets {K = K} {V = V} as Imp
    imp : Mapᴵ K V 0ℓ
    imp = record {Imp; ♯-comm = λ {x}{y} → Imp.♯-comm {x}{y}}
    open Mapᴵ imp public

  module Implementation3 where
    open import Prelude.Maps.AsSortedUniqueLists
    open import Prelude.ToList; open import Prelude.FromList
    open import Prelude.Ord; open import Prelude.Irrelevance

    _ = toList (Map⟨ ℕ ↦ ℕ ⟩ ∋ fromList
        (( , ) ∷ ( , ) ∷ ( , ) ∷ ( , ) ∷ []))
      ≡ (( , ) ∷ ( , ) ∷ ( , ) ∷ [])
      ∋ refl

    -- T0D0: cover abstract signature
    -- open import Prelude.Maps.Abstract.Interface
    -- import Prelude.Maps.AsSortedUniqueLists as Imp

  module GeneralExample where
    open import Prelude.Maps

    _ = Map⟨ String ↦ ℕ ⟩
      ∋ singleton ("one" , ) ∪ singleton ("two" , )

    _ = Map
      ∋ singleton ("one" , ) ◇ singleton ("one" , )
      where instance _ = Semigroup-ℕ-+; _ = SemigroupLaws-ℕ-+
            instance _ = Monoid-ℕ-+;    _ = MonoidLaws-ℕ-+

  module AbstractExample where
    open import Prelude.Maps.Abstract

    K = ℕ; V = String

    _ = Map ∋ m ∪ ∅
      where postulate m : Map⟨ K ↦ V ⟩

    _ = Map ∋ buildMap (const nothing) ∪ buildMap (λ k → just (f k))
      where postulate f : K → V

    _ = Map ∋ singleton (k , v) ∪ singleton (k , v)
      where postulate k : K; v : V

  module ConcreteExample where
    open import Prelude.Maps

    k = ; k′ = 
    k↦_  = (ℕ → Map⟨ ℕ ↦ ℕ ⟩) ∋ singleton ∘ (k ,_)
    k′↦_ = (ℕ → Map⟨ ℕ ↦ ℕ ⟩) ∋ singleton ∘ (k′ ,_)

    -- ** singleton

    _ = singleton (k , ) ≡ fromList [ k ,  ]
      ∋ refl

    -- ** _∪_

    _ = (k↦  ∪ k′↦ ) ≡ fromList ((k , ) ∷ (k′ , ) ∷ [])
      ∋ refl

    _ = (k↦  ∪ k↦ ) ≡ singleton (k , )
      ∋ refl

    -- ** insert/insertWith

    _ = insert (k′ , ) (k↦ ) ≡ (k↦  ∪ k′↦ )
      ∋ refl
    _ = insert (k , ) (k↦ ) ≡ k↦ 
      ∋ refl

    _ = insertWith _+_ (k′ , ) (k↦ ) ≡ (k↦  ∪ k′↦ )
      ∋ refl
    _ = insertWith _+_ (k , ) (k↦ ) ≡ (k↦ )
      ∋ refl

    _ = (k↦  ◇ k↦ ) ≡ (k↦ )
      ∋ refl
      where instance _ = Semigroup-ℕ-+

    postulate v v′ v″ : ℕ

    _ = singleton (k , v) ≡ fromList [ k , v ]
      ∋ refl

    k↦v   = k↦  v; k↦v′  = k↦  v′; k↦v″  = k↦  v″
    k′↦v′ = k′↦ v′

    _ = (k↦v ∪ k′↦v′) ≡ fromList ((k , v) ∷ (k′ , v′) ∷ [])
      ∋ refl

    m₁ = Map
       ∋ singleton (k , v) ∪ singleton (k , v)