From 07749462115e32d247e0e26d628e0525acecd8b8 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 1 Mar 2024 23:27:49 -0800 Subject: [PATCH] Expose decidability from Map modules Signed-off-by: Danila Fedorin --- Lattice/Bundles/FiniteValueMap.agda | 4 ++++ Lattice/FiniteMap.agda | 4 ++++ Lattice/Map.agda | 2 +- 3 files changed, 9 insertions(+), 1 deletion(-) diff --git a/Lattice/Bundles/FiniteValueMap.agda b/Lattice/Bundles/FiniteValueMap.agda index 57f62c6..5eb8d0c 100644 --- a/Lattice/Bundles/FiniteValueMap.agda +++ b/Lattice/Bundles/FiniteValueMap.agda @@ -19,4 +19,8 @@ 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 + + ≈-dec = FVM.≈-dec ks ≈₂-dec + finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂ diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index 0a82eeb..5bbb5b5 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -27,6 +27,7 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map ; ⊓-idemp to ⊓ᵐ-idemp ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ + ; ≈-dec to ≈ᵐ-dec ) open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂) open import Equivalence @@ -38,6 +39,9 @@ module _ (ks : List A) where _≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b) _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂ + ≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_ + ≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂) + _⊔_ : FiniteMap → FiniteMap → FiniteMap _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊔ᵐ m₂ , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks) diff --git a/Lattice/Map.agda b/Lattice/Map.agda index 2017962..d821f64 100644 --- a/Lattice/Map.agda +++ b/Lattice/Map.agda @@ -582,7 +582,7 @@ Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂ ... | no k∉ke₁ | yes k∈ke₂ = ⊥-elim (intersect-preserves-∉₁ {l₂ = proj₁ ⟦ e₂ ⟧} k∉ke₁ k∈ke₁e₂) ... | no k∉ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ ⟦ e₁ ⟧} k∉ke₂ k∈ke₁e₂) -module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where +module _ (≈₂-dec : IsDecidable _≈₂_) where private module _ where data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂