open import Lattice
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 Data.List using (List)

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

open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
    using (Map; ⊔-equal-keys; ⊓-equal-keys)
    renaming
        ( _≈_ to _≈ᵐ_
        ; _⊔_ to _⊔ᵐ_
        ; _⊓_ to _⊓ᵐ_
        ; ≈-equiv to ≈ᵐ-equiv
        ; ≈-⊔-cong to ≈ᵐ-⊔ᵐ-cong
        ; ⊔-assoc to ⊔ᵐ-assoc
        ; ⊔-comm to ⊔ᵐ-comm
        ; ⊔-idemp to ⊔ᵐ-idemp
        ; ≈-⊓-cong to ≈ᵐ-⊓ᵐ-cong
        ; ⊓-assoc to ⊓ᵐ-assoc
        ; ⊓-comm to ⊓ᵐ-comm
        ; ⊓-idemp to ⊓ᵐ-idemp
        ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
        ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
        )
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
open import Equivalence

module _ (ks : List A) where
    FiniteMap : Set (a ⊔ℓ b)
    FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)

    _≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b)
    _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂

    _⊔_ : FiniteMap → FiniteMap → FiniteMap
    _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊔ᵐ m₂ , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)

    _⊓_ : FiniteMap → FiniteMap → FiniteMap
    _⊓_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊓ᵐ m₂ , trans (sym (⊓-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)

    ≈-equiv : IsEquivalence FiniteMap _≈_
    ≈-equiv = record
        { ≈-refl = λ {(m , _)} → IsEquivalence.≈-refl ≈ᵐ-equiv {m}
        ; ≈-sym = λ {(m₁ , _)} {(m₂ , _)} → IsEquivalence.≈-sym ≈ᵐ-equiv {m₁} {m₂}
        ; ≈-trans = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} → IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
        }

    isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
    isUnionSemilattice = record
        { ≈-equiv = ≈-equiv
        ; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
        ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
        ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
        ; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
        }

    isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
    isIntersectSemilattice = record
        { ≈-equiv = ≈-equiv
        ; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
        ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
        ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
        ; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m
        }

    isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
    isLattice = record
        { joinSemilattice = isUnionSemilattice
        ; meetSemilattice = isIntersectSemilattice
        ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
        ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
        }

    lattice : Lattice FiniteMap
    lattice = record
        { _≈_ = _≈_
        ; _⊔_ = _⊔_
        ; _⊓_ = _⊓_
        ; isLattice = isLattice
        }