open import Lattice
open import Data.Unit using (⊤)

-- Due to universe levels, it becomes relatively annoying to handle the case
-- where the levels of A and B are not the same. For the time being, constrain
-- them to be the same.

module Lattice.IterProd {a} (A B : Set a)
    {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set a}
    {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
    {_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B}
    {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (dummy : ⊤) where

open import Agda.Primitive using (lsuc)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)
open import Utils using (iterate)
open import Chain using (Height)

open IsLattice lA renaming (FixedHeight to FixedHeight₁)
open IsLattice lB renaming (FixedHeight to FixedHeight₂)

IterProd : ℕ → Set a
IterProd k = iterate k (λ t → A × t) B

-- To make iteration more convenient, package the definitions in Lattice
-- records, perform the recursion, and unpackage.
--

-- If we prove isLattice and isFiniteHeightLattice by induction separately,
-- we lose the connection between the operations (which should be the same)
-- that are built up by the two iterations. So, do everything in one iteration.
-- This requires some odd code.

build : A → B → (k : ℕ) → IterProd k
build _ b zero = b
build a b (suc s) = (a , build a b s)

private
    record RequiredForFixedHeight : Set (lsuc a) where
        field
            {{≈₁-Decidable}} : IsDecidable _≈₁_
            {{≈₂-Decidable}} : IsDecidable _≈₂_
            h₁ h₂ : ℕ
            {{fhA}} : FixedHeight₁ h₁
            {{fhB}} : FixedHeight₂ h₂

        ⊥₁ : A
        ⊥₁ = Height.⊥ fhA

        ⊥₂ : B
        ⊥₂ = Height.⊥ fhB

        ⊥k : ∀ (k : ℕ) → IterProd k
        ⊥k = build ⊥₁ ⊥₂

    record IsFiniteHeightWithBotAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) (⊥ : A) : Set (lsuc a) where
        field
            height : ℕ
            fixedHeight : IsLattice.FixedHeight isLattice height
            ≈-Decidable : IsDecidable _≈_

            ⊥-correct : Height.⊥ fixedHeight ≡ ⊥

    record Everything (k : ℕ) : Set (lsuc a) where
        T = IterProd k

        field
            _≈_ : T → T → Set a
            _⊔_ : T → T → T
            _⊓_ : T → T → T

            isLattice : IsLattice T _≈_ _⊔_ _⊓_
            isFiniteHeightIfSupported :
                ∀ (req : RequiredForFixedHeight) →
                IsFiniteHeightWithBotAndDecEq isLattice (RequiredForFixedHeight.⊥k req k)

    everything : ∀ (k : ℕ) → Everything k
    everything 0 = record
        { _≈_ = _≈₂_
        ; _⊔_ = _⊔₂_
        ; _⊓_ = _⊓₂_
        ; isLattice = lB
        ; isFiniteHeightIfSupported = λ req → record
            { height = RequiredForFixedHeight.h₂ req
            ; fixedHeight = RequiredForFixedHeight.fhB req
            ; ≈-Decidable = RequiredForFixedHeight.≈₂-Decidable req
            ; ⊥-correct = refl
            }
        }
    everything (suc k') = record
        { _≈_ = P._≈_
        ; _⊔_ = P._⊔_
        ; _⊓_ = P._⊓_
        ; isLattice = P.isLattice
        ; isFiniteHeightIfSupported = λ req →
            let
                fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
            in
                record
                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
                    ; fixedHeight =
                        P.fixedHeight
                            {{≈₂-Decidable = IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest}}
                            {{fhB = IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest}}
                    ; ≈-Decidable = P.≈-Decidable {{≈₂-Decidable = IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest}}
                    ; ⊥-correct =
                        cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
                             (IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
                    }
        }
        where
            everythingRest = everything k'
            import Lattice.Prod A (IterProd k') {{lB = Everything.isLattice everythingRest}} as P

module _ {k : ℕ} where
    open Everything (everything k) using (_≈_; _⊔_; _⊓_) public
    open Lattice.IsLattice (Everything.isLattice (everything k)) public

    instance
        isLattice = Everything.isLattice (everything k)

        lattice : Lattice (IterProd k)
        lattice = record
            { _≈_ = _≈_
            ; _⊔_ = _⊔_
            ; _⊓_ = _⊓_
            ; isLattice = isLattice
            }

    module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}}
             {h₁ h₂ : ℕ}
             {{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where

        private
            isFiniteHeightWithBotAndDecEq =
                Everything.isFiniteHeightIfSupported (everything k)
                    record
                        { ≈₁-Decidable = ≈₁-Decidable
                        ; ≈₂-Decidable = ≈₂-Decidable
                        ; h₁ = h₁
                        ; h₂ = h₂
                        ; fhA = fhA
                        ; fhB = fhB
                        }
        open IsFiniteHeightWithBotAndDecEq isFiniteHeightWithBotAndDecEq using (height; ⊥-correct)

        instance
            fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight isFiniteHeightWithBotAndDecEq

            isFiniteHeightLattice = record
                { isLattice = isLattice
                ; fixedHeight = fixedHeight
                }

            finiteHeightLattice : FiniteHeightLattice (IterProd k)
            finiteHeightLattice = record
                { height = height
                ; _≈_ = _≈_
                ; _⊔_ = _⊔_
                ; _⊓_ = _⊓_
                ; isFiniteHeightLattice = isFiniteHeightLattice
                }

        ⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
        ⊥-built = ⊥-correct