Implement map intersection

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice.agda

@@ -74,7 +74,7 @@ module IsEquivalenceInstances where
         (_≈₂_ : B → B → Set b)
         (eB : IsEquivalence B _≈₂_) where
 
-        open import Map A B ≡-dec-A using (Map; lift; subset; insert)
+        open import Map A B ≡-dec-A using (Map; lift; subset)
         open import Data.List using (_∷_; []) -- TODO: re-export these with nicer names from map
 
         open IsEquivalence eB renaming

Map.agda

@@ -277,6 +277,58 @@ private module ImplInsert (f : B → B → B) where
             ...    | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v₁∈xs₁))
             ...    | no  k≢k' = k≢k'
 
+    update : A → B → List (A × B) → List (A × B)
+    update k v [] = []
+    update k v ((k' , v') ∷ xs) with ≡-dec-A k k'
+    ...                            | yes _ = (k' , f v v') ∷ xs
+    ...                            | no _ = (k' , v') ∷ update k v xs
+
+    restrict : List (A × B) → List (A × B) → List (A × B)
+    restrict l [] = []
+    restrict l ((k' , v') ∷ xs) with ∈k-dec k' l
+    ...                           | yes _ = (k' , v') ∷ restrict l xs
+    ...                           | no _ = restrict l xs
+
+    intersect : List (A × B) → List (A × B) → List (A × B)
+    intersect l₁ l₂ = restrict l₁ (foldr update l₂ l₁)
+
+    update-keys : ∀ {k : A} {v : B} {l : List (A × B)} →
+                  keys l ≡ keys (update k v l)
+    update-keys {l = []} = refl
+    update-keys {k} {v} {l = (k' , v') ∷ xs}
+        with ≡-dec-A k k'
+    ...   | yes _ = refl
+    ...   | no _ rewrite update-keys {k} {v} {xs} = refl
+
+    update-preserves-Unique : ∀ {k : A} {v : B} {l : List (A × B)} →
+                              Unique (keys l) → Unique (keys (update k v l ))
+    update-preserves-Unique {k} {v} {l} u rewrite update-keys {k} {v} {l} = u
+
+    updates-preserve-Unique : ∀ {l₁ l₂ : List (A × B)} →
+                              Unique (keys l₂) → Unique (keys (foldr update l₂ l₁))
+    updates-preserve-Unique {[]} u = u
+    updates-preserve-Unique {(k , v) ∷ xs} u = update-preserves-Unique (updates-preserve-Unique {xs} u)
+
+    restrict-preserves-k≢ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
+                            All (λ k' → ¬ k ≡ k') (keys l₂) → All (λ k' → ¬ k ≡ k') (keys (restrict l₁ l₂))
+    restrict-preserves-k≢ {k} {l₁} {[]} k≢l₂ = k≢l₂
+    restrict-preserves-k≢ {k} {l₁} {(k' , v') ∷ xs} (k≢k' ∷ k≢xs)
+        with ∈k-dec k' l₁
+    ...   | yes _ = k≢k' ∷ restrict-preserves-k≢ k≢xs
+    ...   | no _ = restrict-preserves-k≢ k≢xs
+
+    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₁} {(k , v) ∷ xs} (push k≢xs uxs)
+        with ∈k-dec k l₁
+    ...   | yes _ = push (restrict-preserves-k≢ k≢xs) (restrict-preserves-Unique uxs)
+    ...   | no _ = restrict-preserves-Unique uxs
+
+    intersect-preserves-Unique : ∀ {l₁ l₂ : List (A × B)} →
+                                 Unique (keys l₂) → Unique (keys (intersect l₁ l₂))
+    intersect-preserves-Unique {l₁} u = restrict-preserves-Unique (updates-preserve-Unique {l₁} u)
+
 
 Map : Set (a ⊔ b)
 Map = Σ (List (A × B)) (λ l → Unique (keys l))
@@ -298,14 +350,15 @@ module _ (f : B → B → B) where
     open ImplInsert f renaming
         ( insert to insert-impl
         ; union to union-impl
+        ; intersect to intersect-impl
         )
 
-    insert : A → B → Map → Map
-    insert k v (kvs , uks) = (insert-impl k v kvs , insert-preserves-Unique uks)
-
     union : Map → Map → Map
     union (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
 
+    intersect : Map → Map → Map
+    intersect (kvs₁ , _) (kvs₂ , uks₂) = (intersect-impl kvs₁ kvs₂ , intersect-preserves-Unique {kvs₁} {kvs₂} uks₂)
+
     ⟦_⟧ : Expr -> Map
     ⟦ ` m ⟧ = m
     ⟦ e₁ ∪ e₂ ⟧ = union ⟦ e₁ ⟧ ⟦ e₂ ⟧