From ca99e181848659da5d4e01c583a091323ff7ab00 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 9 Mar 2024 13:59:22 -0800 Subject: [PATCH] Tweak exports from finite value bundle to avoid (some) redundant arguments Signed-off-by: Danila Fedorin --- Lattice/Bundles/FiniteValueMap.agda | 6 ++++-- Main.agda | 10 +++++----- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/Lattice/Bundles/FiniteValueMap.agda b/Lattice/Bundles/FiniteValueMap.agda index 5eb8d0c..e67163b 100644 --- a/Lattice/Bundles/FiniteValueMap.agda +++ b/Lattice/Bundles/FiniteValueMap.agda @@ -19,8 +19,10 @@ module _ (fhB : FiniteHeightLattice B) where module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) where import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM - FiniteHeightType = FVM.FiniteMap + FiniteHeightType = FVM.FiniteMap ks + + finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂ + open FiniteHeightLattice finiteHeightLattice public ≈-dec = FVM.≈-dec ks ≈₂-dec - finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂ diff --git a/Main.agda b/Main.agda index 99ae755..205968a 100644 --- a/Main.agda +++ b/Main.agda @@ -22,7 +22,7 @@ xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ ( 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) +open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ using () renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec) fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt) @@ -33,7 +33,7 @@ showAboveBelow AB.⊤ = "⊤" showAboveBelow AB.⊥ = "⊥" showAboveBelow (AB.[_] tt) = "()" -showMap : ∀ {ks : List String} → FiniteHeightMap ks → String +showMap : FiniteHeightMap → String showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}" fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec @@ -44,16 +44,16 @@ open import Relation.Binary.Reasoning.Base.Single _≈_ (λ {m} → ≈-refl {m} smallestMap = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ))) largestMap = proj₂ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ))) -dumb : FiniteHeightMap xyzw +dumb : FiniteHeightMap dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl) -dumbFunction : FiniteHeightMap xyzw → FiniteHeightMap xyzw +dumbFunction : FiniteHeightMap → FiniteHeightMap 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₂) +open import Fixedpoint {0ℓ} {FiniteHeightMap} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂) main = run {0ℓ} (putStrLn (showMap aᶠ))