-- Because iterated products currently require both A and B to be of the same
-- universe, and the FiniteMap is written in a universe-polymorphic way,
-- specialize the FiniteMap module with Set-typed types only.

open import Lattice
open import Equivalence
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Definitions using (Decidable)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
open import Function.Definitions using (Inverseˡ; Inverseʳ)

module Lattice.FiniteValueMap (A : Set) (B : Set)
    (_≈₂_ : B → B → Set)
    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
    (≈-dec-A : Decidable (_≡_ {_} {A}))
    (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where

open import Data.List using (List; length; []; _∷_)
open import Utils using (Unique; push; empty)
open import Data.Product using (_,_)
open import Data.List.Properties using (∷-injectiveʳ)

open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB public

module IterProdIsomorphism where
    open import Data.Unit using (⊤; tt)
    open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ)
    open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ as IP using (IterProd)

    from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks)
    from {[]} (([] , _) , _) = tt
    from {k ∷ ks'} (((k' , v) ∷ kvs' , push _ uks') , refl) = (v , from ((kvs' , uks'), refl))

    to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks
    to {[]} _ ⊤ = (([] , empty) , refl)
    to {k ∷ ks'} (push k≢ks' uks') (v , rest)
        with to uks' rest
    ...   | ((kvs' , ukvs') , refl) = (((k , v) ∷ kvs' , push k≢ks' ukvs') , refl)


    private
        _≈ᵐ_ : ∀ {ks : List A} → FiniteMap ks → FiniteMap ks → Set
        _≈ᵐ_ {ks} = _≈_ ks

        _≈ⁱᵖ_ : ∀ {ks : List A} → IterProd (length ks) → IterProd (length ks) → Set
        _≈ⁱᵖ_ {ks} = IP._≈_ (length ks)

    from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
                      Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- from (to x) = x
    from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
    from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest)
        with ((kvs' , ukvs') , refl) ← to uks' rest in p rewrite sym p =
            (IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest)
            -- the rewrite here is needed because the IH is in terms of `to uks' rest`,
            -- but we end up with the 'unpacked' form (kvs', ...). So, put it back
            -- in the 'packed' form after we've performed enough inspection
            -- to know we take the cons branch of `to`.