From d7183387598dac01136c3eb1b0e5441b8181f716 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 10 Feb 2024 16:51:43 -0800 Subject: [PATCH] Clean up 'Map' to hide implementation details, extract code Signed-off-by: Danila Fedorin --- Lattice/Map.agda | 104 +++++++++++++++++++---------------------------- Utils.agda | 32 +++++++++++++++ 2 files changed, 73 insertions(+), 63 deletions(-) create mode 100644 Utils.agda diff --git a/Lattice/Map.agda b/Lattice/Map.agda index d6731aa..2f74dc0 100644 --- a/Lattice/Map.agda +++ b/Lattice/Map.agda @@ -19,6 +19,7 @@ open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-ex open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂) open import Data.Empty using (⊥; ⊥-elim) open import Equivalence +open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any) open IsLattice lB using () renaming ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans @@ -28,34 +29,10 @@ open IsLattice lB using () renaming ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂ ) -module ImplKeys where +private module ImplKeys where keys : List (A × B) → List A keys = map proj₁ -data Unique {c} {C : Set c} : List C → Set c where - empty : Unique [] - push : ∀ {x : C} {xs : List C} - → All (λ x' → ¬ x ≡ x') xs - → Unique xs - → Unique (x ∷ xs) - -Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} → - ¬ MemProp._∈_ x xs → Unique xs → Unique (xs ++ (x ∷ [])) -Unique-append {c} {C} {x} {[]} _ _ = push [] empty -Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') = - push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs') - where - x'≢x : ¬ x' ≡ x - x'≢x x'≡x = x∉xs (here (sym x'≡x)) - - help : {l : List C} → All (λ x'' → ¬ x' ≡ x'') l → All (λ x'' → ¬ x' ≡ x'') (l ++ (x ∷ [])) - help {[]} _ = x'≢x ∷ [] - help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es - -All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l -All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px -All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs - private module _ where open MemProp using (_∈_) open ImplKeys @@ -559,45 +536,46 @@ 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₂) -data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where - extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂ - mismatch : (k : A) (v₁ v₂ : B) → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → ¬ v₁ ≈₂ v₂ → SubsetInfo m₁ m₂ - fine : m₁ ⊆ m₂ → SubsetInfo m₁ m₂ - -SubsetInfo-to-dec : ∀ {m₁ m₂ : Map} → SubsetInfo m₁ m₂ → Dec (m₁ ⊆ m₂) -SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) = - let (v , k,v∈m₁) = locate k∈km₁ - in no (λ m₁⊆m₂ → - let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁ - in k∉km₂ (∈-cong proj₁ k,v'∈m₂)) -SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) = - no (λ m₁⊆m₂ → - let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁ - in v₁̷≈v₂ (subst (λ v'' → v₁ ≈₂ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst... -SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂ - module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where - compute-SubsetInfo : ∀ m₁ m₂ → SubsetInfo m₁ m₂ - compute-SubsetInfo ([] , _) m₂ = fine (λ k v ()) - compute-SubsetInfo m₁@((k , v) ∷ xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂) - with compute-SubsetInfo (xs₁ , uxs₁) m₂ - ... | extra k' k'∈kxs₁ k'∉km₂ = extra k' (there k'∈kxs₁) k'∉km₂ - ... | mismatch k' v₁ v₂ k',v₁∈xs₁ k',v₂∈m₂ v₁̷≈v₂ = - mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂ - ... | fine xs₁⊆m₂ with ∈k-dec k l₂ - ... | no k∉km₂ = extra k (here refl) k∉km₂ - ... | yes k∈km₂ with locate k∈km₂ - ... | (v' , k,v'∈m₂) with ≈₂-dec v v' - ... | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v' - ... | yes v≈v' = fine m₁⊆m₂ - where - m₁⊆m₂ : m₁ ⊆ m₂ - m₁⊆m₂ k' v'' (here k,v≡k',v'') - rewrite cong proj₁ k,v≡k',v'' - rewrite cong proj₂ k,v≡k',v'' = - (v' , (v≈v' , k,v'∈m₂)) - m₁⊆m₂ k' v'' (there k,v≡k',v'') = - xs₁⊆m₂ k' v'' k,v≡k',v'' + private module _ where + data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where + extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂ + mismatch : (k : A) (v₁ v₂ : B) → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → ¬ v₁ ≈₂ v₂ → SubsetInfo m₁ m₂ + fine : m₁ ⊆ m₂ → SubsetInfo m₁ m₂ + + SubsetInfo-to-dec : ∀ {m₁ m₂ : Map} → SubsetInfo m₁ m₂ → Dec (m₁ ⊆ m₂) + SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) = + let (v , k,v∈m₁) = locate k∈km₁ + in no (λ m₁⊆m₂ → + let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁ + in k∉km₂ (∈-cong proj₁ k,v'∈m₂)) + SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) = + no (λ m₁⊆m₂ → + let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁ + in v₁̷≈v₂ (subst (λ v'' → v₁ ≈₂ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst... + SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂ + + compute-SubsetInfo : ∀ m₁ m₂ → SubsetInfo m₁ m₂ + compute-SubsetInfo ([] , _) m₂ = fine (λ k v ()) + compute-SubsetInfo m₁@((k , v) ∷ xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂) + with compute-SubsetInfo (xs₁ , uxs₁) m₂ + ... | extra k' k'∈kxs₁ k'∉km₂ = extra k' (there k'∈kxs₁) k'∉km₂ + ... | mismatch k' v₁ v₂ k',v₁∈xs₁ k',v₂∈m₂ v₁̷≈v₂ = + mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂ + ... | fine xs₁⊆m₂ with ∈k-dec k l₂ + ... | no k∉km₂ = extra k (here refl) k∉km₂ + ... | yes k∈km₂ with locate k∈km₂ + ... | (v' , k,v'∈m₂) with ≈₂-dec v v' + ... | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v' + ... | yes v≈v' = fine m₁⊆m₂ + where + m₁⊆m₂ : m₁ ⊆ m₂ + m₁⊆m₂ k' v'' (here k,v≡k',v'') + rewrite cong proj₁ k,v≡k',v'' + rewrite cong proj₂ k,v≡k',v'' = + (v' , (v≈v' , k,v'∈m₂)) + m₁⊆m₂ k' v'' (there k,v≡k',v'') = + xs₁⊆m₂ k' v'' k,v≡k',v'' ⊆-dec : ∀ m₁ m₂ → Dec (m₁ ⊆ m₂) ⊆-dec m₁ m₂ = SubsetInfo-to-dec (compute-SubsetInfo m₁ m₂) diff --git a/Utils.agda b/Utils.agda new file mode 100644 index 0000000..804c40e --- /dev/null +++ b/Utils.agda @@ -0,0 +1,32 @@ +module Utils where + +open import Data.List using (List; []; _∷_; _++_) +open import Data.List.Membership.Propositional using (_∈_) +open import Data.List.Relation.Unary.All using (All; []; _∷_) +open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map +open import Relation.Binary.PropositionalEquality using (_≡_; sym) +open import Relation.Nullary using (¬_) + +data Unique {c} {C : Set c} : List C → Set c where + empty : Unique [] + push : ∀ {x : C} {xs : List C} + → All (λ x' → ¬ x ≡ x') xs + → Unique xs + → Unique (x ∷ xs) + +Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} → + ¬ x ∈ xs → Unique xs → Unique (xs ++ (x ∷ [])) +Unique-append {c} {C} {x} {[]} _ _ = push [] empty +Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') = + push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs') + where + x'≢x : ¬ x' ≡ x + x'≢x x'≡x = x∉xs (here (sym x'≡x)) + + help : {l : List C} → All (λ x'' → ¬ x' ≡ x'') l → All (λ x'' → ¬ x' ≡ x'') (l ++ (x ∷ [])) + help {[]} _ = x'≢x ∷ [] + help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es + +All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l +All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px +All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs