DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Expose only a 'public' "keys" function from Map

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-10 16:35:21 -08:00
parent a55c786a51
commit 1b8c88b1a2
1 changed files with 10 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
Lattice/Map.agda
View File

@ -28,8 +28,9 @@ open IsLattice lB using () renaming
; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂ ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
) )
keys : List (A × B) → List A module ImplKeys where
keys = map proj₁ keys : List (A × B) → List A
keys = map proj₁
data Unique {c} {C : Set c} : List C → Set c where data Unique {c} {C : Set c} : List C → Set c where
empty : Unique [] empty : Unique []
@ -57,6 +58,7 @@ All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
private module _ where private module _ where
open MemProp using (_∈_) open MemProp using (_∈_)
open ImplKeys
unique-not-in : ∀ {k : A} {v : B} {l : List (A × B)} → unique-not-in : ∀ {k : A} {v : B} {l : List (A × B)} →
¬ (All (λ k' → ¬ k ≡ k') (keys l) × (k , v) ∈ l) ¬ (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 private module ImplInsert (f : B → B → B) where
open import Data.List using (map) open import Data.List using (map)
open MemProp using (_∈_) open MemProp using (_∈_)
open ImplKeys
private private
_∈k_ : A → List (A × B) → Set a _∈k_ : A → List (A × B) → Set a
@ -448,13 +451,16 @@ private module ImplInsert (f : B → B → B) where
Map : Set (a ⊔ℓ b) 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) _∈_ : (A × B) → Map → Set (a ⊔ℓ b)
_∈_ p (kvs , _) = MemProp._∈_ p kvs _∈_ p (kvs , _) = MemProp._∈_ p kvs
_∈k_ : A → Map → Set a _∈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 : ∀ {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 Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m