From 1b1b80465c08ae44a77814f3116296cf9a85d79c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 9 Mar 2024 21:46:15 -0800 Subject: [PATCH] Use named modules to avoid having to pass redundant parameters Signed-off-by: Danila Fedorin --- Analysis/Sign.agda | 25 +++++++++++++++---------- Lattice/Bundles/FiniteValueMap.agda | 20 +++++++++++--------- Lattice/FiniteMap.agda | 8 +++++--- Lattice/FiniteValueMap.agda | 2 +- Main.agda | 22 ++++++++++------------ 5 files changed, 42 insertions(+), 35 deletions(-) diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index 1ca4aaa..e259b4e 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -6,6 +6,9 @@ open import Relation.Nullary using (¬_; Dec; yes; no) open import Language open import Lattice +import Lattice.Bundles.FiniteValueMap + +private module FixedHeightFiniteMap = Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice data Sign : Set where + : Sign @@ -36,15 +39,17 @@ module _ (prog : Program) where finiteHeightLatticeᵍ = finiteHeightLatticeᵍ-if-inhabited 0ˢ -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators. - open import Lattice.Bundles.FiniteValueMap String SignLattice _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵛ-if-B-finite; FiniteHeightType to FiniteHeightTypeᵛ; _≈_ to _≈ᵛ_; ≈-dec to ≈ᵛ-dec-if-≈ᵍ-dec) - - - VariableSigns = FiniteHeightTypeᵛ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec - finiteHeightLatticeᵛ = finiteHeightLatticeᵛ-if-B-finite finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec - ≈ᵛ-dec = ≈ᵛ-dec-if-≈ᵍ-dec finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec + open FixedHeightFiniteMap String SignLattice _≟ˢ_ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec + renaming + ( finiteHeightLattice to finiteHeightLatticeᵛ + ; FiniteMap to VariableSigns + ; _≈_ to _≈ᵛ_ + ; ≈-dec to ≈ᵛ-dec + ) -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in. - open import Lattice.Bundles.FiniteValueMap State VariableSigns _≟_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ-if-B-finite; FiniteHeightType to FiniteHeightTypeᵐ) - - StateVariables = FiniteHeightTypeᵐ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec - finiteHeightLatticeᵐ = finiteHeightLatticeᵐ-if-B-finite finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec + open FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec + renaming + ( finiteHeightLattice to finiteHeightLatticeᵐ + ; FiniteMap to StateVariables + ) diff --git a/Lattice/Bundles/FiniteValueMap.agda b/Lattice/Bundles/FiniteValueMap.agda index e67163b..26506de 100644 --- a/Lattice/Bundles/FiniteValueMap.agda +++ b/Lattice/Bundles/FiniteValueMap.agda @@ -8,7 +8,10 @@ open import Data.List using (List) open import Data.Nat using (ℕ) open import Utils using (Unique) -module _ (fhB : FiniteHeightLattice B) where +module FromFiniteHeightLattice (fhB : FiniteHeightLattice B) + {ks : List A} (uks : Unique ks) + (≈₂-dec : Decidable (FiniteHeightLattice._≈_ fhB)) where + open Lattice.FiniteHeightLattice fhB using () renaming ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_ ; height to height₂ @@ -16,13 +19,12 @@ module _ (fhB : FiniteHeightLattice B) where ; fixedHeight to fixedHeight₂ ) - module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) where - import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM + import Lattice.FiniteMap + module FM = Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ + open FM.WithKeys ks public - FiniteHeightType = FVM.FiniteMap ks - - finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂ - open FiniteHeightLattice finiteHeightLattice public - - ≈-dec = FVM.≈-dec ks ≈₂-dec + import Lattice.FiniteValueMap + module FVM = Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ + open FVM.IterProdIsomorphism.WithUniqueKeysAndFixedHeight uks ≈₂-dec height₂ fixedHeight₂ public + ≈-dec = ≈₂-dec⇒≈-dec ≈₂-dec diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index 774fb74..d8c3b3e 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -45,15 +45,15 @@ open import Relation.Nullary using (¬_; Dec; yes; no) open import Utils using (Pairwise; _∷_; []) open import Data.Empty using (⊥-elim) -module _ (ks : List A) where +module WithKeys (ks : List A) where FiniteMap : Set (a ⊔ℓ b) FiniteMap = Σ Map (λ m → Map.keys m ≡ ks) _≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b) _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂ - ≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_ - ≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂) + ≈₂-dec⇒≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_ + ≈₂-dec⇒≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂) _⊔_ : FiniteMap → FiniteMap → FiniteMap _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = @@ -174,3 +174,5 @@ module _ (ks : List A) where ... | no k∉km₁ | no k∉km₂ = m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ ks'' m₁≼m₂ ... | yes k∈km₁ | no k∉km₂ = ⊥-elim (∈k-exclusive fm₁ fm₂ (k∈km₁ , k∉km₂)) ... | no k∉km₁ | yes k∈km₂ = ⊥-elim (∈k-exclusive fm₂ fm₁ (k∈km₂ , k∉km₁)) + +open WithKeys public diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index d046bbc..287654d 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -399,7 +399,7 @@ module IterProdIsomorphism where in (v' , (v₁⊔v₂≈v' , there v'∈fm')) - module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where + module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where import Isomorphism open Isomorphism.TransportFiniteHeight (IP.isFiniteHeightLattice (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ) (isLattice ks) diff --git a/Main.agda b/Main.agda index 205968a..ce7fe61 100644 --- a/Main.agda +++ b/Main.agda @@ -20,23 +20,22 @@ 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 _≟ˢ_ using () 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 : FiniteHeightMap → String -showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}" +fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt) -fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec +import Lattice.Bundles.FiniteValueMap +open Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice String AB.AboveBelow _≟ˢ_ fhlᵘ xyzw-Unique ≈ᵘ-dec using (FiniteMap; ≈-dec) renaming (finiteHeightLattice to fhlⁱᵖ) + +showMap : FiniteMap → String +showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}" 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? @@ -44,16 +43,15 @@ 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 +dumb : FiniteMap dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl) -dumbFunction : FiniteHeightMap → FiniteHeightMap +dumbFunction : FiniteMap → FiniteMap dumbFunction = _⊔_ dumb dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {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₂) +open import Fixedpoint {0ℓ} {FiniteMap} {8} {_≈_} {_⊔_} {_⊓_} ≈-dec (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂) main = run {0ℓ} (putStrLn (showMap aᶠ))