From 1432dfa6690bc4d7fc19d4cb4764cf457b148fcb Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 4 Jan 2025 22:28:47 -0800 Subject: [PATCH] Clean up FiniteMap module structure a bit Signed-off-by: Danila Fedorin --- Analysis/Forward/Lattices.agda | 17 +++-------- Lattice/FiniteMap.agda | 53 ++++++++++++++++++---------------- 2 files changed, 32 insertions(+), 38 deletions(-) diff --git a/Analysis/Forward/Lattices.agda b/Analysis/Forward/Lattices.agda index 4bbf80b..3df50bf 100644 --- a/Analysis/Forward/Lattices.agda +++ b/Analysis/Forward/Lattices.agda @@ -54,6 +54,7 @@ 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 open IsLattice isLatticeᵛ @@ -64,12 +65,6 @@ open IsLattice isLatticeᵛ ; ⊔-idemp to ⊔ᵛ-idemp ) public -open Lattice.FiniteMap.IterProdIsomorphism String L vars - using () - renaming - ( Provenance-union to Provenance-unionᵐ - ) - public open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight String L vars vars-Unique using () renaming @@ -95,20 +90,16 @@ 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 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, @@ -196,7 +187,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∈ρ)) diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index 66bb5f6..821c617 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -143,6 +143,7 @@ private module WithKeys (ks : List A) where λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} → IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃} } + open IsEquivalence ≈-equiv public instance isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_ @@ -253,6 +254,33 @@ 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₂)) + + _∈ᵐ_ : ∀ {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₂))) + module IterProdIsomorphism where open WithKeys open import Data.Unit using (tt) @@ -297,9 +325,6 @@ module IterProdIsomorphism where 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} @@ -307,8 +332,6 @@ module IterProdIsomorphism where 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)) @@ -367,26 +390,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)