open import Lattice

-- 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 _≈₂_ _⊔₂_ _⊓₂_) where

open import Agda.Primitive using (lsuc)
open import Data.Nat using (ℕ; suc; _+_)
open import Data.Product using (_×_)
open import Utils using (iterate)

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.

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

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

    record Everything (A : Set a) : Set (lsuc a) where
        field
            _≈_ : A → A → Set a
            _⊔_ : A → A → A
            _⊓_ : A → A → A

            isLattice : IsLattice A _≈_ _⊔_ _⊓_
            isFiniteHeightIfSupported : RequiredForFixedHeight → IsFiniteHeightAndDecEq isLattice

    everything : ∀ (k : ℕ) → Everything (IterProd k)
    everything 0 = record
        { _≈_ = _≈₂_
        ; _⊔_ = _⊔₂_
        ; _⊓_ = _⊓₂_
        ; isLattice = lB
        ; isFiniteHeightIfSupported = λ req → record
            { height = RequiredForFixedHeight.h₂ req
            ; fixedHeight = RequiredForFixedHeight.fhB req
            ; ≈-dec = RequiredForFixedHeight.≈₂-dec req
            }
        }
    everything (suc k') = record
        { _≈_ = P._≈_
        ; _⊔_ = P._⊔_
        ; _⊓_ = P._⊓_
        ; isLattice = P.isLattice
        ; isFiniteHeightIfSupported = λ req →
            let
                fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
            in
                record
                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightAndDecEq.height fhlRest
                    ; fixedHeight =
                        P.fixedHeight
                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightAndDecEq.height fhlRest)
                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightAndDecEq.fixedHeight fhlRest)
                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
                    }
        }
        where
            everythingRest = everything k'

            import Lattice.Prod
                _≈₁_ (Everything._≈_ everythingRest)
                _⊔₁_ (Everything._⊔_ everythingRest)
                _⊓₁_ (Everything._⊓_ everythingRest)
                lA  (Everything.isLattice everythingRest) as P

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

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

    module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
             (h₁ h₂ : ℕ)
             (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where

        private
            required : RequiredForFixedHeight
            required = record
                { ≈₁-dec = ≈₁-dec
                ; ≈₂-dec = ≈₂-dec
                ; h₁ = h₁
                ; h₂ = h₂
                ; fhA = fhA
                ; fhB = fhB
                }

        isFiniteHeightLattice = record
            { isLattice = isLattice
            ; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
            }

        finiteHeightLattice : FiniteHeightLattice (IterProd k)
        finiteHeightLattice = record
            { height = IsFiniteHeightAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
            ; _≈_ = _≈_
            ; _⊔_ = _⊔_
            ; _⊓_ = _⊓_
            ; isFiniteHeightLattice = isFiniteHeightLattice
            }