Implement the fixed point algorithm

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice.agda

@@ -452,7 +452,9 @@ module FixedHeightLatticeIsBounded {a} {A : Set a} {h : ℕ}
     open IsFiniteHeightLattice lA using (_≼_; _≺_; fixedHeight; ≈-equiv; ≈-refl; ≈-sym; ≈-trans; ≼-refl; ≼-cong; ≺-cong; ≈-⊔-cong; absorb-⊔-⊓; ⊔-comm; ⊓-comm)
     open IsDecidable decA using () renaming (R-dec to ≈-dec)
     open NatProps using (+-comm; m+1+n≰m)
-    module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
+
+    private
+        module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
 
     A-BoundedBelow : Σ A (λ ⊥ᴬ → ∀ (a : A) → ⊥ᴬ ≼ a)
     A-BoundedBelow = (⊥ᴬ , ⊥ᴬ≼)
@@ -466,7 +468,7 @@ module FixedHeightLatticeIsBounded {a} {A : Set a} {h : ℕ}
             ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
             ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
             ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = (a , ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ)))
-            ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = absurd (m+1+n≰m h h+1≤h)
+            ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
                             where
                                 ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
                                 ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
@@ -474,14 +476,43 @@ module FixedHeightLatticeIsBounded {a} {A : Set a} {h : ℕ}
                                 x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ
                                 x≺⊥ᴬ = ((⊥ᴬ , ≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a))) , ⊥ᴬ⊓a̷≈⊥ᴬ)
 
-                                h+1≤h : h + 1 ≤ h
-                                h+1≤h rewrite (+-comm h 1) = proj₂ fixedHeight (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight)))
-
 module FixedPoint {a} {A : Set a}
                   (h : ℕ)
-                  (_≈_ : A → A → Set a)
+                  (_≈_ : A → A → Set a) (decA : IsDecidable _≈_)
                   (_⊔_ : A → A → A) (_⊓_ : A → A → A)
                   (isFiniteHeightLattice : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
                   (f : A → A) (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ isFiniteHeightLattice)
                                                       (IsFiniteHeightLattice._≼_ isFiniteHeightLattice) f) where
+    open IsDecidable decA using () renaming (R-dec to ≈-dec)
     open IsFiniteHeightLattice isFiniteHeightLattice
+    open FixedHeightLatticeIsBounded decA isFiniteHeightLattice
+    open NatProps using (+-suc; +-comm)
+    module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
+
+    private
+        ⊥ᴬ : A
+        ⊥ᴬ = proj₁ A-BoundedBelow
+
+        ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
+        ⊥ᴬ≼ = proj₂ A-BoundedBelow
+
+        -- using 'g', for gas, here helps make sure the function terminates.
+        -- since A forms a fixed-height lattice, we must find a solution after
+        -- enough '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 = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) 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 ⊥ᴬ))