Re-export members of isLattice together with the record where needed

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

Analysis/Forward/Lattices.agda

@@ -10,7 +10,6 @@ module Analysis.Forward.Lattices
 
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
 open import Data.Product using (proj₁; proj₂; _,_)
-open import Data.Unit using (tt)
 open import Data.Sum using (inj₁; inj₂)
 open import Data.List using (List; _∷_; []; foldr)
 open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
@@ -38,7 +37,7 @@ instance
 -- with keys strings. Use a bundle to avoid explicitly specifying operators.
 -- It's helpful to export these via 'public' since consumers tend to
 -- use various variable lattice operations.
-module VariableValuesFiniteMap = Lattice.FiniteMap.WithKeys String L tt vars
+module VariableValuesFiniteMap = Lattice.FiniteMap String L vars
 open VariableValuesFiniteMap
     using ()
     renaming
@@ -55,23 +54,13 @@ open VariableValuesFiniteMap
         ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ
         ; ∈k-dec to ∈k-decᵛ
         ; all-equal-keys to all-equal-keysᵛ
-        )
+        ; Provenance-union to Provenance-unionᵛ
-    public
+        ; ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
-open IsLattice isLatticeᵛ
-    using ()
-    renaming
-        ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
         ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
         ; ⊔-idemp to ⊔ᵛ-idemp
         )
     public
-open Lattice.FiniteMap.IterProdIsomorphism String L _
+open VariableValuesFiniteMap.FixedHeight vars-Unique
-    using ()
-    renaming
-        ( Provenance-union to Provenance-unionᵐ
-        )
-    public
-open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight String L _ vars-Unique
     using ()
     renaming
         ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
@@ -83,7 +72,7 @@ open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight String L
 ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
 
 -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
-module StateVariablesFiniteMap = Lattice.FiniteMap.WithKeys State VariableValues tt states
+module StateVariablesFiniteMap = Lattice.FiniteMap State VariableValues states
 open StateVariablesFiniteMap
     using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂)
     renaming
@@ -96,20 +85,15 @@ open StateVariablesFiniteMap
         ; _≼_ to _≼ᵐ_
         ; ≈-Decidable to ≈ᵐ-Decidable
         ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
+        ; ≈-sym to ≈ᵐ-sym
         )
     public
-open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight State VariableValues _ states-Unique
+open StateVariablesFiniteMap.FixedHeight states-Unique
     using ()
     renaming
         ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
         )
     public
-open IsFiniteHeightLattice isFiniteHeightLatticeᵐ
-    using ()
-    renaming
-        ( ≈-sym to ≈ᵐ-sym
-        )
-    public
 
 -- We now have our (state -> (variables -> value)) map.
 -- Define a couple of helpers to retrieve values from it. Specifically,
@@ -197,7 +181,7 @@ module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where
     ⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {vs₁ vs₂ : VariableValues} → (⟦ vs₁ ⟧ᵛ ∨ ⟦ vs₂ ⟧ᵛ) ⇒ ⟦ vs₁ ⊔ᵛ vs₂ ⟧ᵛ
     ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁} {vs₂} ρ ⟦vs₁⟧ρ∨⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ
         with ((l₁ , l₂) , (refl , (k,l₁∈vs₁ , k,l₂∈vs₂)))
-             ← Provenance-unionᵐ vs₁ vs₂ k,l∈vs₁₂
+             ← Provenance-unionᵛ vs₁ vs₂ k,l∈vs₁₂
         with ⟦vs₁⟧ρ∨⟦vs₂⟧ρ
     ...   | inj₁ ⟦vs₁⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₁ (⟦vs₁⟧ρ k,l₁∈vs₁ k,v∈ρ))
     ...   | inj₂ ⟦vs₂⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₂ (⟦vs₂⟧ρ k,l₂∈vs₂ k,v∈ρ))

Analysis/Sign.agda

@@ -78,10 +78,9 @@ open AB.Plain 0ˢ using ()
         ; _≼_ to _≼ᵍ_
         ; _⊔_ to _⊔ᵍ_
         ; _⊓_ to _⊓ᵍ_
+        ; ≼-trans to ≼ᵍ-trans
         )
 
-open IsLattice isLatticeᵍ using () renaming (≼-trans to ≼ᵍ-trans)
-
 plus : SignLattice → SignLattice → SignLattice
 plus ⊥ᵍ _ = ⊥ᵍ
 plus _ ⊥ᵍ = ⊥ᵍ

Lattice/AboveBelow.agda

@@ -321,7 +321,7 @@ module Plain (x : A) where
             ; isLattice = isLattice
             }
 
-    open IsLattice isLattice using (_≼_; _≺_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_; _≺_; ≼-trans; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
     ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
     ⊥≺[x] x = (≈-refl , λ ())

Lattice/FiniteMap.agda

@@ -9,10 +9,10 @@ module Lattice.FiniteMap (A : Set) (B : Set)
     {_≈₂_ : B → B → Set}
     {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
     {{≡-Decidable-A : IsDecidable {_} {A} _≡_}}
-    {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (dummy : ⊤) where
+    {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (ks : List A) where
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
-open import Lattice.Map A B dummy as Map
+open import Lattice.Map A B _ as Map
     using
         ( Map
         ; ⊔-equal-keys
@@ -74,7 +74,7 @@ open import Showable using (Showable; show)
 open import Isomorphism using (IsInverseˡ; IsInverseʳ)
 open import Chain using (Height)
 
-module WithKeys (ks : List A) where
+private module WithKeys (ks : List A) where
     FiniteMap : Set
     FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)
 
@@ -131,7 +131,7 @@ module WithKeys (ks : List A) where
 
     []-∈ : ∀ {k : A} {v : B} {ks' : List A} (fm : FiniteMap) →
            k ∈ˡ ks' → (k , v) ∈ fm → v ∈ˡ (fm [ ks' ])
-    []-∈ {k} {v} {ks'} (m , _) k∈ks' k,v∈fm = []ᵐ-∈ m k,v∈fm k∈ks' 
+    []-∈ {k} {v} {ks'} (m , _) k∈ks' k,v∈fm = []ᵐ-∈ m k,v∈fm k∈ks'
 
     ≈-equiv : IsEquivalence FiniteMap _≈_
     ≈-equiv = record
@@ -143,6 +143,7 @@ module WithKeys (ks : List A) where
             λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} →
                 IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
         }
+    open IsEquivalence ≈-equiv public
 
     instance
         isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
@@ -183,7 +184,7 @@ module WithKeys (ks : List A) where
             ; isLattice = isLattice
             }
 
-    open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_; ⊔-idemp; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
     m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (fm₁ fm₂ : FiniteMap) {k : A} {v₁ v₂ : B} →
                         fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂
@@ -253,9 +254,35 @@ module WithKeys (ks : List A) where
     ...   | 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
+private
+    _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → WithKeys.FiniteMap ks₁ → WithKeys.FiniteMap ks₂ → Set
+    _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
 
-module IterProdIsomorphism where
+    _∈ᵐ_ : ∀ {ks : List A} → A × B → WithKeys.FiniteMap ks → Set
+    _∈ᵐ_ {ks} = WithKeys._∈_ ks
+
+FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : WithKeys.FiniteMap ks) → Set
+FromBothMaps k v fm₁ fm₂ =
+    Σ (B × B)
+      (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
+
+Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : WithKeys.FiniteMap ks) {k : A} {v : B} →
+                   (k , v) ∈ᵐ (WithKeys._⊔_ ks fm₁ fm₂) → FromBothMaps k v fm₁ fm₂
+Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
+    with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂
+...   | in₁ (single k,v∈m₁) k∉km₂
+        with k∈km₁ ← (WithKeys.forget k,v∈m₁)
+        rewrite trans ks₁≡ks (sym ks₂≡ks) =
+        ⊥-elim (k∉km₂ k∈km₁)
+...   | in₂ k∉km₁ (single k,v∈m₂)
+        with k∈km₂ ← (WithKeys.forget k,v∈m₂)
+        rewrite trans ks₁≡ks (sym ks₂≡ks) =
+        ⊥-elim (k∉km₁ k∈km₂)
+...   | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
+        ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
+
+private module IterProdIsomorphism where
+    open WithKeys
     open import Data.Unit using (tt)
     open import Lattice.Unit using ()
         renaming
@@ -267,7 +294,7 @@ module IterProdIsomorphism where
             ; ≈-equiv to ≈ᵘ-equiv
             ; fixedHeight to fixedHeightᵘ
             )
-    open import Lattice.IterProd B ⊤ dummy
+    open import Lattice.IterProd B ⊤ _
         as IP
         using (IterProd)
     open IsLattice lB using ()
@@ -296,20 +323,12 @@ module IterProdIsomorphism where
         in
             (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡ks)
 
+    _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set
+    _≈ⁱᵖ_ {n} = IP._≈_ {n}
 
-    private
+    _⊔ⁱᵖ_ : ∀ {ks : List A} →
-        _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → FiniteMap ks₁ → FiniteMap ks₂ → Set
+            IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
-        _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
+    _⊔ⁱᵖ_ {ks} = IP._⊔_ {length ks}
-
-        _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set
-        _≈ⁱᵖ_ {n} = IP._≈_ {n}
-
-        _⊔ⁱᵖ_ : ∀ {ks : List A} →
-                IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
-        _⊔ⁱᵖ_ {ks} = IP._⊔_ {length ks}
-
-        _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set
-        _∈ᵐ_ {ks} = _∈_ ks
 
     to-build : ∀ {b : B} {ks : List A} (uks : Unique ks) →
                let fm = to uks (IP.build b tt (length ks))
@@ -368,26 +387,6 @@ module IterProdIsomorphism where
                                 fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
                         in (v'' , (v'≈v'' , there k',v''∈fm'₁))
 
-    FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set
-    FromBothMaps k v fm₁ fm₂ =
-        Σ (B × B)
-          (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
-
-    Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} →
-                       (k , v) ∈ᵐ (_⊔_ ks fm₁ fm₂) → FromBothMaps k v fm₁ fm₂
-    Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
-        with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂
-    ...   | in₁ (single k,v∈m₁) k∉km₂
-            with k∈km₁ ← (forget k,v∈m₁)
-            rewrite trans ks₁≡ks (sym ks₂≡ks) =
-            ⊥-elim (k∉km₂ k∈km₁)
-    ...   | in₂ k∉km₁ (single k,v∈m₂)
-            with k∈km₂ ← (forget k,v∈m₂)
-            rewrite trans ks₁≡ks (sym ks₂≡ks) =
-            ⊥-elim (k∉km₁ k∈km₂)
-    ...   | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
-            ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
-
     private
         first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
                            Σ B (λ v → (k , v) ∈ᵐ fm)
@@ -613,7 +612,7 @@ module IterProdIsomorphism where
                         in
                             (v' , (v₁⊔v₂≈v' , there v'∈fm'))
 
-    module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) {{≈₂-Decidable : IsDecidable _≈₂_}} {h₂ : ℕ} {{fhB : FixedHeight₂ h₂}} where
+    module FixedHeight {ks : List A} {{≈₂-Decidable : IsDecidable _≈₂_}} {h₂ : ℕ} {{fhB : FixedHeight₂ h₂}} (uks : Unique ks) where
         import Isomorphism
         open Isomorphism.TransportFiniteHeight
             (IP.isFiniteHeightLattice {k = length ks} {{fhB = fixedHeightᵘ}}) (isLattice ks)
@@ -631,3 +630,6 @@ module IterProdIsomorphism where
         ⊥-contains-bottoms {k} {v} k,v∈⊥
             rewrite IP.⊥-built {length ks} {{fhB = fixedHeightᵘ}} =
             to-build uks k v k,v∈⊥
+
+open WithKeys ks public
+module FixedHeight = IterProdIsomorphism.FixedHeight

Lattice/Prod.agda

@@ -106,6 +106,8 @@ instance
         ; isLattice = isLattice
         }
 
+open IsLattice isLattice using (_≼_; _≺_; ≺-cong) public
+
 module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}} where
     open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
     open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
@@ -125,7 +127,6 @@ module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDeci
              {{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where
 
         open import Data.Nat.Properties
-        open IsLattice isLattice using (_≼_; _≺_; ≺-cong)
 
         module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
         module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice