Use named modules to avoid having to pass redundant parameters

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

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)
+    open FixedHeightFiniteMap String SignLattice _≟ˢ_ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
-
+        renaming
-
+            ( finiteHeightLattice to finiteHeightLatticeᵛ
-    VariableSigns = FiniteHeightTypeᵛ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
+            ; FiniteMap to VariableSigns
-    finiteHeightLatticeᵛ = finiteHeightLatticeᵛ-if-B-finite finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
+            ; _≈_ to _≈ᵛ_
-    ≈ᵛ-dec = ≈ᵛ-dec-if-≈ᵍ-dec finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
+            ; ≈-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ᵐ)
+    open FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
-
+        renaming
-    StateVariables = FiniteHeightTypeᵐ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
+            ( finiteHeightLattice to finiteHeightLatticeᵐ
-    finiteHeightLatticeᵐ = finiteHeightLatticeᵐ-if-B-finite finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
+            ; FiniteMap to StateVariables
+            )

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.FiniteMap
-        import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM
+    module FM = Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂
+    open FM.WithKeys ks public
 
-        FiniteHeightType = FVM.FiniteMap ks
+    import Lattice.FiniteValueMap
-
+    module FVM = Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂
-        finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂
+    open FVM.IterProdIsomorphism.WithUniqueKeysAndFixedHeight uks ≈₂-dec height₂ fixedHeight₂ public
-        open FiniteHeightLattice finiteHeightLattice public
-
-        ≈-dec = FVM.≈-dec ks ≈₂-dec
 
+    ≈-dec = ≈₂-dec⇒≈-dec ≈₂-dec

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 : IsDecidable _≈₂_ → IsDecidable _≈_
-    ≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂)
+    ≈₂-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

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)

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
+fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt)
-showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}"
 
-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ℓ} {FiniteMap} {8} {_≈_} {_⊔_} {_⊓_} ≈-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ᶠ))