From 311ed751862744f4e466c7604a0f7fba5f9a3275 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 9 Mar 2024 13:57:02 -0800 Subject: [PATCH] Expose more helpers from 'Map' Signed-off-by: Danila Fedorin --- Lattice/Map.agda | 52 ++++++++++++++++++++++++++++++------------------ 1 file changed, 33 insertions(+), 19 deletions(-) diff --git a/Lattice/Map.agda b/Lattice/Map.agda index f5c8c33..405a7d3 100644 --- a/Lattice/Map.agda +++ b/Lattice/Map.agda @@ -19,7 +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; All-x∈xs) +open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs) open IsLattice lB using () renaming ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans @@ -34,6 +34,21 @@ private module ImplKeys where keys : List (A × B) → List A keys = map proj₁ +-- See note on `forget` for why this is defined in global scope even though +-- it operates on lists. +∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ˡ (ImplKeys.keys l)) +∈k-dec k [] = no (λ ()) +∈k-dec k ((k' , v) ∷ xs) + with (≡-dec-A k k') +... | yes k≡k' = yes (here k≡k') +... | no k≢k' with (∈k-dec k xs) +... | yes k∈kxs = yes (there k∈kxs) +... | no k∉kxs = no witness + where + witness : ¬ k ∈ˡ (ImplKeys.keys ((k' , v) ∷ xs)) + witness (here k≡k') = k≢k' k≡k' + witness (there k∈kxs) = k∉kxs k∈kxs + private module _ where open MemProp using (_∈_) open ImplKeys @@ -65,19 +80,6 @@ private module _ where ... | yes k∈xs = yes (there k∈xs) ... | no k∉xs = no (λ { (here k≡x) → k≢x k≡x; (there k∈xs) → k∉xs k∈xs }) - ∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ keys l) - ∈k-dec k [] = no (λ ()) - ∈k-dec k ((k' , v) ∷ xs) - with (≡-dec-A k k') - ... | yes k≡k' = yes (here k≡k') - ... | no k≢k' with (∈k-dec k xs) - ... | yes k∈kxs = yes (there k∈kxs) - ... | no k∉kxs = no witness - where - witness : ¬ k ∈ keys ((k' , v) ∷ xs) - witness (here k≡k') = k≢k' k≡k' - witness (there k∈kxs) = k∉kxs k∈kxs - ∈-cong : ∀ {c d} {C : Set c} {D : Set d} {c : C} {l : List C} → (f : C → D) → c ∈ l → f c ∈ map f l ∈-cong f (here c≡c') = here (cong f c≡c') @@ -340,7 +342,7 @@ private module ImplInsert (f : B → B → B) where restrict-preserves-Unique : ∀ {l₁ l₂ : List (A × B)} → Unique (keys l₂) → Unique (keys (restrict l₁ l₂)) - restrict-preserves-Unique {l₁} {[]} _ = empty + restrict-preserves-Unique {l₁} {[]} _ = Utils.empty restrict-preserves-Unique {l₁} {(k , v) ∷ xs} (push k≢xs uxs) with ∈k-dec k l₁ ... | yes _ = push (restrict-preserves-k≢ k≢xs) (restrict-preserves-Unique uxs) @@ -476,6 +478,9 @@ private module ImplInsert (f : B → B → B) where Map : Set (a ⊔ℓ b) Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l)) +empty : Map +empty = ([] , Utils.empty) + keys : Map → List A keys (kvs , _) = ImplKeys.keys kvs @@ -488,8 +493,9 @@ _∈k_ k m = MemProp._∈_ k (keys m) locate : ∀ {k : A} {m : Map} → k ∈k m → Σ B (λ v → (k , v) ∈ m) locate k∈km = locate-impl k∈km --- defined this way because ∈ for maps uses projection, so the full map can't be guessed. --- On the other hand, list can be guessed. +-- `forget` and `∈k-dec` are defined this way because ∈ for maps uses +-- projection, so the full map can't be guessed. On the other hand, list can +-- be guessed. forget : ∀ {k : A} {v : B} {l : List (A × B)} → (k , v) ∈ˡ l → k ∈ˡ (ImplKeys.keys l) forget = ∈-cong proj₁ @@ -529,9 +535,12 @@ data Expr : Set (a ⊔ℓ b) where _∪_ : Expr → Expr → Expr _∩_ : Expr → Expr → Expr -open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys) renaming (insert to insert-impl; union to union-impl) +open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys; insert-preserves-Unique) renaming (insert to insert-impl; union to union-impl) open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl) +insert : A → B → Map → Map +insert k v (l , uks) = (insert-impl k v l , insert-preserves-Unique uks) + _⊔_ : Map → Map → Map _⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂) @@ -878,6 +887,8 @@ isLattice = record ; absorb-⊓-⊔ = absorb-⊓-⊔ } +open IsLattice isLattice using (_≼_) public + lattice : Lattice Map lattice = record { _≈_ = _≈_ @@ -958,6 +969,10 @@ _updating_via_ (kvs , uks) ks f = , subst Unique (transform-keys-≡ kvs ks f) uks ) +updating-via-keys-≡ : ∀ (m : Map) (ks : List A) (f : A → B) → + keys m ≡ keys (m updating ks via f) +updating-via-keys-≡ (l , _) = transform-keys-≡ l + updating-via-∉k-forward : ∀ (m : Map) (ks : List A) (f : A → B) {k : A} → ¬ k ∈k m → ¬ k ∈k (m updating ks via f) updating-via-∉k-forward m = transform-∉k-forward @@ -995,7 +1010,6 @@ updating-via-k∉ks-backward m = transform-k∉ks-backward module _ {l} {L : Set l} {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where - open IsLattice isLattice using (_≼_) open IsLattice lL using () renaming (_≼_ to _≼ˡ_) module _ (f : L → Map) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)