open import Data.Nat as Nat using (ℕ; suc; _+_; _≤_)
open import Lattice

module Fixedpoint {a} {A : Set a}
                  {h : ℕ}
                  {_≈_ : A → A → Set a}
                  {_⊔_ : A → A → A} {_⊓_ : A → A → A}
                  (≈-dec : IsDecidable _≈_)
                  (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
                  (f : A → A)
                  (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
                                          (IsFiniteHeightLattice._≼_ flA) f) where

open import Data.Nat.Properties using (+-suc; +-comm)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Empty using (⊥-elim)
open import Relation.Binary.PropositionalEquality using (_≡_; sym)
open import Relation.Nullary using (Dec; ¬_; yes; no)

open IsFiniteHeightLattice flA

import Chain
module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong

private
    open ChainA.Height fixedHeight
        using ()
        renaming
            ( ⊥ to ⊥ᴬ
            ; longestChain to longestChainᴬ
            ; bounded to boundedᴬ
            )


    ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
    ⊥ᴬ≼ a with ≈-dec a ⊥ᴬ
    ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
    ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
    ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))
    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
                    where
                        ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
                        ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))

                        x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ
                        x≺⊥ᴬ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a)) , ⊥ᴬ⊓a̷≈⊥ᴬ)

    -- using 'g', for gas, here helps make sure the function terminates.
    -- since A forms a fixed-height lattice, we must find a solution after
    -- 'h' steps at most. Gas is set up such that as soon as it runs
    -- out, we have exceeded h steps, which shouldn't be possible.

    doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a)
    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
    doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
        with ≈-dec a₂ (f a₂)
    ...   | yes a₂≈fa₂ = (a₂ , a₂≈fa₂)
    ...   | no  a₂̷≈fa₂ = doStep g' (suc hᶜ) a₁ (f a₂) c' g+hᶜ≡sh (Monotonicᶠ a₂≼fa₂)
                where
                    a₂≺fa₂ : a₂ ≺ f a₂
                    a₂≺fa₂ = (a₂≼fa₂ , a₂̷≈fa₂)

                    c' : ChainA.Chain a₁ (f a₂) (suc hᶜ)
                    c' rewrite +-comm 1 hᶜ = ChainA.concat c (ChainA.step a₂≺fa₂ ≈-refl (ChainA.done (≈-refl {f a₂})))

    fix : Σ A (λ a → a ≈ f a)
    fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))

aᶠ : A
aᶠ = proj₁ fix

aᶠ≈faᶠ : aᶠ ≈ f aᶠ
aᶠ≈faᶠ = proj₂ fix

private
    stepPreservesLess : ∀ (g hᶜ : ℕ) (a₁ a₂ a : A) (a≈fa : a ≈ f a) (a₂≼a : a₂ ≼ a)
                     (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h)
                     (a₂≼fa₂ : a₂ ≼ f a₂) →
                     proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ a
    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
    stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
        with ≈-dec a₂ (f a₂)
    ...   | yes _ = a₂≼a
    ...   | no  _ = stepPreservesLess g' _ _ _ a a≈fa (≼-cong ≈-refl (≈-sym a≈fa) (Monotonicᶠ a₂≼a)) _ _ _

aᶠ≼ : ∀ (a : A) → a ≈ f a → aᶠ ≼ a
aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))