Make main run the fixed point algorithm

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

Isomorphism.agda

@@ -60,3 +60,12 @@ module TransportFiniteHeight
             { isLattice = lB
             ; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
             }
+
+    finiteHeightLattice : FiniteHeightLattice B
+    finiteHeightLattice = record
+        { height = height
+        ; _≈_ = _≈₂_
+        ; _⊔_ = _⊔₂_
+        ; _⊓_ = _⊓₂_
+        ; isFiniteHeightLattice = isFiniteHeightLattice
+        }

Lattice.agda

@@ -14,6 +14,12 @@ open import Function.Definitions using (Injective)
 IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a
 IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
 
+module _ {a b} {A : Set a} {B : Set b}
+    (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where
+
+    Monotonic : (A → B) → Set (a ⊔ℓ b)
+    Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂
+
 record IsSemilattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A) : Set a where
@@ -36,6 +42,26 @@ record IsSemilattice {a} (A : Set a)
 
     open import Relation.Binary.Reasoning.Base.Single _≈_ ≈-refl ≈-trans
 
+    ⊔-Monotonicˡ : ∀ (a₁ : A) → Monotonic _≼_ _≼_ (λ a₂ → a₁ ⊔ a₂)
+    ⊔-Monotonicˡ a {a₁} {a₂} a₁≼a₂ = ≈-trans (≈-sym lhs) (≈-⊔-cong (≈-refl {a}) a₁≼a₂)
+        where
+            lhs =
+                begin
+                    a ⊔ (a₁ ⊔ a₂)
+                ∼⟨ ≈-⊔-cong (≈-sym (⊔-idemp _)) ≈-refl ⟩
+                    (a ⊔ a) ⊔ (a₁ ⊔ a₂)
+                ∼⟨ ⊔-assoc _ _ _ ⟩
+                    a ⊔ (a ⊔ (a₁ ⊔ a₂))
+                ∼⟨ ≈-⊔-cong ≈-refl (≈-sym (⊔-assoc _ _ _)) ⟩
+                    a ⊔ ((a ⊔ a₁) ⊔ a₂)
+                ∼⟨ ≈-⊔-cong ≈-refl (≈-⊔-cong (⊔-comm _ _) ≈-refl) ⟩
+                    a ⊔ ((a₁ ⊔ a) ⊔ a₂)
+                ∼⟨ ≈-⊔-cong ≈-refl (⊔-assoc _ _ _) ⟩
+                    a ⊔ (a₁ ⊔ (a ⊔ a₂))
+                ∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
+                    (a ⊔ a₁) ⊔ (a ⊔ a₂)
+                ∎
+
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a
 
@@ -97,12 +123,6 @@ record IsFiniteHeightLattice {a} (A : Set a)
     field
         fixedHeight : FixedHeight h
 
-module _ {a b} {A : Set a} {B : Set b}
-    (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where
-
-    Monotonic : (A → B) → Set (a ⊔ℓ b)
-    Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂
-
 module ChainMapping {a b} {A : Set a} {B : Set b}
     {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
     {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}

Lattice/Bundles/FiniteValueMap.agda

@@ -0,0 +1,26 @@
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.Definitions using (Decidable)
+
+module Lattice.Bundles.FiniteValueMap (A B : Set) (≡-dec-A : Decidable (_≡_ {_} {A})) where
+
+open import Lattice
+open import Data.List using (List)
+open import Data.Nat using (ℕ)
+open import Utils using (Unique)
+
+module _ (fhB : FiniteHeightLattice B) where
+    open Lattice.FiniteHeightLattice fhB using () renaming
+        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
+        ; height to height₂
+        ; isLattice to isLattice₂
+        ; fixedHeight to fixedHeight₂
+        )
+
+    module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) where
+        import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM
+
+        FiniteHeightType = FVM.FiniteMap
+
+        ≈-dec = FVM.≈-dec ks ≈₂-dec
+
+        finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂

Lattice/Bundles/IterProd.agda

@@ -0,0 +1,38 @@
+open import Lattice
+
+module Lattice.Bundles.IterProd {a} (A B : Set a) where
+open import Data.Nat using (ℕ)
+
+module _ (lA : Lattice A) (lB : Lattice B) where
+    open Lattice.Lattice lA using () renaming
+        ( _≈_ to _≈₁_; _⊔_ to _⊔₁_; _⊓_ to _⊓₁_
+        ; isLattice to isLattice₁
+        )
+
+    open Lattice.Lattice lB using () renaming
+        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
+        ; isLattice to isLattice₂
+        )
+
+    module _ (k : ℕ) where
+        open import Lattice.IterProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_ isLattice₁ isLattice₂ using (lattice) public
+
+module _ (fhA : FiniteHeightLattice A) (fhB : FiniteHeightLattice B) where
+    open Lattice.FiniteHeightLattice fhA using () renaming
+        ( _≈_ to _≈₁_; _⊔_ to _⊔₁_; _⊓_ to _⊓₁_
+        ; height to height₁
+        ; isLattice to isLattice₁
+        ; fixedHeight to fixedHeight₁
+        )
+
+    open Lattice.FiniteHeightLattice fhB using () renaming
+        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
+        ; height to height₂
+        ; isLattice to isLattice₂
+        ; fixedHeight to fixedHeight₂
+        )
+
+    module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) (k : ℕ) where
+        import Lattice.IterProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_ isLattice₁ isLattice₂ as IP
+
+        finiteHeightLattice = IP.finiteHeightLattice k ≈₁-dec ≈₂-dec height₁ height₂ fixedHeight₁ fixedHeight₂

Lattice/FiniteMap.agda

@@ -27,6 +27,7 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
         ; ⊓-idemp to ⊓ᵐ-idemp
         ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
         ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
+        ; ≈-dec to ≈ᵐ-dec
         )
 open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
 open import Equivalence
@@ -38,6 +39,9 @@ module _ (ks : List A) where
     _≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b)
     _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
 
+    ≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_
+    ≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂)
+
     _⊔_ : 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)
 

Lattice/FiniteValueMap.agda

@@ -271,4 +271,4 @@ module IterProdIsomorphism where
             (to-preserves-≈ uks) (from-preserves-≈ {ks})
             (to-⊔-distr uks) (from-⊔-distr {ks})
             (from-to-inverseʳ uks) (from-to-inverseˡ uks)
-            using (isFiniteHeightLattice) public
+            using (isFiniteHeightLattice; finiteHeightLattice) public

Lattice/Map.agda

@@ -582,7 +582,7 @@ Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂
 ...   | no k∉ke₁ | yes k∈ke₂ = ⊥-elim (intersect-preserves-∉₁ {l₂ = proj₁ ⟦ e₂ ⟧} k∉ke₁ k∈ke₁e₂)
 ...   | no k∉ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ ⟦ e₁ ⟧} k∉ke₂ k∈ke₁e₂)
 
-module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
+module _ (≈₂-dec : IsDecidable _≈₂_) where
     private module _ where
         data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
             extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂

Main.agda

@@ -0,0 +1,69 @@
+module Main where
+
+open import IO
+open import Level using (0ℓ)
+open import Data.Nat.Show using (show)
+open import Data.List using (List; _∷_; []; foldr)
+open import Data.String using (String; _++_) renaming (_≟_ to _≟ˢ_)
+open import Data.Unit using (⊤; tt) renaming (_≟_ to _≟ᵘ_)
+open import Data.Product using (_,_; _×_; proj₁; proj₂)
+open import Data.List.Relation.Unary.All using (_∷_; [])
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl; trans)
+open import Relation.Nullary using (¬_)
+
+open import Utils using (Unique; push; empty)
+
+xyzw : List String
+xyzw = "x" ∷ "y" ∷ "z" ∷ "w" ∷ []
+
+xyzw-Unique : Unique xyzw
+xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ []) (push [] empty)))
+
+open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice; Monotonic)
+open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_  as AB using () renaming (≈-dec to ≈ᵘ-dec)
+open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
+open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
+
+fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt)
+
+FiniteHeightMap = FiniteHeightTypeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
+
+showAboveBelow : AB.AboveBelow → String
+showAboveBelow AB.⊤ = "⊤"
+showAboveBelow AB.⊥ = "⊥"
+showAboveBelow (AB.[_] tt) = "()"
+
+showMap : ∀ {ks : List String} → FiniteHeightMap ks → String
+showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}"
+
+fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
+
+open FiniteHeightLattice fhlⁱᵖ using (_≈_; _⊔_; _⊓_; ⊔-idemp; _≼_; ≈-⊔-cong; ≈-refl; ≈-trans; ≈-sym; ⊔-assoc; ⊔-comm; ⊔-Monotonicˡ)
+open import Relation.Binary.Reasoning.Base.Single _≈_ (λ {m} → ≈-refl {m}) (λ {m₁} {m₂} {m₃} → ≈-trans {m₁} {m₂} {m₃}) -- why am I having to eta-expand here?
+
+smallestMap = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
+largestMap = proj₂ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
+
+dumb : FiniteHeightMap xyzw
+dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl)
+
+dumbFunction : FiniteHeightMap xyzw → FiniteHeightMap xyzw
+dumbFunction = _⊔_ dumb
+
+dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction
+dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {m₂} m₁≼m₂
+
+
+open import Fixedpoint {0ℓ} {FiniteHeightMap xyzw} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
+
+-- 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
+
+main = run {0ℓ} (putStrLn (showMap aᶠ))