From 1b8c88b1a28678bed8ee17f676f661c044009feb Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 10 Feb 2024 16:35:21 -0800 Subject: [PATCH] Expose only a 'public' "keys" function from Map Signed-off-by: Danila Fedorin --- Lattice/Map.agda | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/Lattice/Map.agda b/Lattice/Map.agda index 88e82aa..d6731aa 100644 --- a/Lattice/Map.agda +++ b/Lattice/Map.agda @@ -28,8 +28,9 @@ open IsLattice lB using () renaming ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂ ) -keys : List (A × B) → List A -keys = map proj₁ +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 [] @@ -57,6 +58,7 @@ All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs private module _ where open MemProp using (_∈_) + open ImplKeys unique-not-in : ∀ {k : A} {v : B} {l : List (A × B)} → ¬ (All (λ k' → ¬ k ≡ k') (keys l) × (k , v) ∈ l) @@ -108,6 +110,7 @@ private module ImplRelation where private module ImplInsert (f : B → B → B) where open import Data.List using (map) open MemProp using (_∈_) + open ImplKeys private _∈k_ : A → List (A × B) → Set a @@ -448,13 +451,16 @@ private module ImplInsert (f : B → B → B) where Map : Set (a ⊔ℓ b) -Map = Σ (List (A × B)) (λ l → Unique (keys l)) +Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l)) + +keys : Map → List A +keys (kvs , _) = ImplKeys.keys kvs _∈_ : (A × B) → Map → Set (a ⊔ℓ b) _∈_ p (kvs , _) = MemProp._∈_ p kvs _∈k_ : A → Map → Set a -_∈k_ k (kvs , _) = MemProp._∈_ k (keys kvs) +_∈k_ k m = MemProp._∈_ k (keys m) Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v' Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m