Analysis/Forward/Lattices.agda

@@ -10,6 +10,7 @@ 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 _∈ˡ_)
@@ -37,7 +38,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 String L vars
+module VariableValuesFiniteMap = Lattice.FiniteMap.WithKeys String L tt vars
 open VariableValuesFiniteMap
     using ()
     renaming
@@ -54,13 +55,23 @@ 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ᵛ
-        ; ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
+        )
+    public
+open IsLattice isLatticeᵛ
+    using ()
+    renaming
+        ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
         ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
         ; ⊔-idemp to ⊔ᵛ-idemp
         )
     public
-open VariableValuesFiniteMap.FixedHeight vars-Unique
+open Lattice.FiniteMap.IterProdIsomorphism String L _
+    using ()
+    renaming
+        ( Provenance-union to Provenance-unionᵐ
+        )
+    public
+open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight String L _ vars-Unique
     using ()
     renaming
         ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
@@ -72,7 +83,7 @@ open VariableValuesFiniteMap.FixedHeight vars-Unique
 ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
 
 -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
-module StateVariablesFiniteMap = Lattice.FiniteMap State VariableValues states
+module StateVariablesFiniteMap = Lattice.FiniteMap.WithKeys State VariableValues tt states
 open StateVariablesFiniteMap
     using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂)
     renaming
@@ -85,15 +96,20 @@ open StateVariablesFiniteMap
         ; _≼_ to _≼ᵐ_
         ; ≈-Decidable to ≈ᵐ-Decidable
         ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
-        ; ≈-sym to ≈ᵐ-sym
         )
     public
-open StateVariablesFiniteMap.FixedHeight states-Unique
+open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight State VariableValues _ 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,
@@ -181,7 +197,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,9 +78,10 @@ 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 (_≼_; _≺_; ≼-trans; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_; _≺_; ⊔-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 _≈₂_ _⊔₂_ _⊓₂_}} (ks : List A) where
+    {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (dummy : ⊤) where
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
-open import Lattice.Map A B _ as Map
+open import Lattice.Map A B dummy 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)
 
-private module WithKeys (ks : List A) where
+module WithKeys (ks : List A) where
     FiniteMap : Set
     FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)
 
@@ -131,7 +131,7 @@ private 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,7 +143,6 @@ private module WithKeys (ks : List A) where
             λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} →
                 IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
         }
-    open IsEquivalence ≈-equiv public
 
     instance
         isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
@@ -184,7 +183,7 @@ private module WithKeys (ks : List A) where
             ; isLattice = isLattice
             }
 
-    open IsLattice isLattice using (_≼_; ⊔-idemp; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_; ⊔-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₂
@@ -254,35 +253,9 @@ private 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₁))
 
-private
-    _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → WithKeys.FiniteMap ks₁ → WithKeys.FiniteMap ks₂ → Set
-    _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
+open WithKeys public
 
-    _∈ᵐ_ : ∀ {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
+module IterProdIsomorphism where
     open import Data.Unit using (tt)
     open import Lattice.Unit using ()
         renaming
@@ -294,7 +267,7 @@ private module IterProdIsomorphism where
             ; ≈-equiv to ≈ᵘ-equiv
             ; fixedHeight to fixedHeightᵘ
             )
-    open import Lattice.IterProd B ⊤ _
+    open import Lattice.IterProd B ⊤ dummy
         as IP
         using (IterProd)
     open IsLattice lB using ()
@@ -323,12 +296,20 @@ private module IterProdIsomorphism where
         in
             (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡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}
+    private
+        _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → FiniteMap ks₁ → FiniteMap ks₂ → Set
+        _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
+
+        _≈ⁱᵖ_ : ∀ {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))
@@ -387,6 +368,26 @@ private 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)
@@ -612,7 +613,7 @@ private module IterProdIsomorphism where
                         in
                             (v' , (v₁⊔v₂≈v' , there v'∈fm'))
 
-    module FixedHeight {ks : List A} {{≈₂-Decidable : IsDecidable _≈₂_}} {h₂ : ℕ} {{fhB : FixedHeight₂ h₂}} (uks : Unique ks) where
+    module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) {{≈₂-Decidable : IsDecidable _≈₂_}} {h₂ : ℕ} {{fhB : FixedHeight₂ h₂}} where
         import Isomorphism
         open Isomorphism.TransportFiniteHeight
             (IP.isFiniteHeightLattice {k = length ks} {{fhB = fixedHeightᵘ}}) (isLattice ks)
@@ -630,6 +631,3 @@ private 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,8 +106,6 @@ 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)
@@ -127,6 +125,7 @@ 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