DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Make main run the fixed point algorithm

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-01 23:42:10 -08:00
parent 0774946211
commit 6cb6281bc2
1 changed files with 47 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

55
Main.agda
View File

@ -1,11 +1,12 @@
module Main where module Main where
open import IO open import IO
open import Level open import Level using (0ℓ)
open import Data.Nat.Show using (show) open import Data.Nat.Show using (show)
open import Data.List using (List; _∷_; []) open import Data.List using (List; _∷_; []; foldr)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.String using (String; _++_) renaming (_≟_ to _≟ˢ_)
open import Data.Unit using (⊤; tt) 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 Data.List.Relation.Unary.All using (_∷_; [])
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl; trans) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl; trans)
open import Relation.Nullary using (¬_) open import Relation.Nullary using (¬_)
@ -18,13 +19,51 @@ xyzw = "x" ∷ "y" ∷ "z" ∷ "w" ∷ []
xyzw-Unique : Unique xyzw xyzw-Unique : Unique xyzw
xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ []) (push [] empty))) xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ []) (push [] empty)))
open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice) open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice; Monotonic)
open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_ as AB renaming (≈-dec to ≈ᵘ-dec) open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_ as AB using () renaming (≈-dec to ≈ᵘ-dec)
open AB.Plain renaming (finiteHeightLattice to finiteHeightLatticeᵘ) open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ 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) 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 fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
main = run {0ℓ} (putStrLn (show (FiniteHeightLattice.height fhlⁱᵖ))) 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ᶠ))