|
|
|
|
@ -488,7 +488,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
|
|
|
|
|
|
|
|
|
|
forget : ∀ {k : A} {v : B} {m : Map} → (k , v) ∈ m → k ∈k m
|
|
|
|
|
-- 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₁
|
|
|
|
|
|
|
|
|
|
Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
|
|
|
|
|
@ -592,9 +594,9 @@ 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₂)
|
|
|
|
|
|
|
|
|
|
Expr-Provenance-≡ : ∀ (k : A) (v : B) (e : Expr) → (k , v) ∈ ⟦ e ⟧ → Provenance k v e
|
|
|
|
|
Expr-Provenance-≡ k v e k,v∈e
|
|
|
|
|
with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget {m = ⟦ e ⟧} k,v∈e)
|
|
|
|
|
Expr-Provenance-≡ : ∀ {k : A} {v : B} (e : Expr) → (k , v) ∈ ⟦ e ⟧ → Provenance k v e
|
|
|
|
|
Expr-Provenance-≡ {k} {v} e k,v∈e
|
|
|
|
|
with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget k,v∈e)
|
|
|
|
|
rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p
|
|
|
|
|
|
|
|
|
|
module _ (≈₂-dec : IsDecidable _≈₂_) where
|
|
|
|
|
@ -609,7 +611,7 @@ module _ (≈₂-dec : IsDecidable _≈₂_) where
|
|
|
|
|
let (v , k,v∈m₁) = locate-impl 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₂))
|
|
|
|
|
in k∉km₂ (forget 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₁
|
|
|
|
|
@ -665,19 +667,16 @@ private module I⊓ = ImplInsert _⊓₂_
|
|
|
|
|
|
|
|
|
|
⊔-⊆ : ∀ (m₁ m₂ m₃ m₄ : Map) → m₁ ≈ m₂ → m₃ ≈ m₄ → (m₁ ⊔ m₃) ⊆ (m₂ ⊔ m₄)
|
|
|
|
|
⊔-⊆ m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
|
|
|
|
|
with Expr-Provenance k ((` m₁) ∪ (` m₃)) (∈-cong proj₁ k,v∈m₁m₃)
|
|
|
|
|
... | (_ , (bothᵘ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) , v₁v₃∈m₁m₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₁v₃∈m₁m₃ =
|
|
|
|
|
with Expr-Provenance-≡ ((` m₁) ∪ (` m₃)) k,v∈m₁m₃
|
|
|
|
|
... | bothᵘ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) =
|
|
|
|
|
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
|
|
|
|
|
(v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
|
|
|
|
|
in (v₂ ⊔₂ v₄ , (≈₂-⊔₂-cong v₁≈v₂ v₃≈v₄ , I⊔.union-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
|
|
|
|
|
... | (_ , (in₁ (single {v₁} v₁∈m₁) k∉km₃ , v₁∈m₁m₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₁∈m₁m₃ =
|
|
|
|
|
... | in₁ (single {v₁} v₁∈m₁) k∉km₃ =
|
|
|
|
|
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
|
|
|
|
|
k∉km₄ = ≈-∉-cong {m₃} {m₄} m₃≈m₄ k∉km₃
|
|
|
|
|
in (v₂ , (v₁≈v₂ , I⊔.union-preserves-∈₁ (proj₂ m₂) k,v₂∈m₂ k∉km₄))
|
|
|
|
|
... | (_ , (in₂ k∉km₁ (single {v₃} v₃∈m₃) , v₃∈m₁m₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₃∈m₁m₃ =
|
|
|
|
|
... | in₂ k∉km₁ (single {v₃} v₃∈m₃) =
|
|
|
|
|
let (v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
|
|
|
|
|
k∉km₂ = ≈-∉-cong {m₁} {m₂} m₁≈m₂ k∉km₁
|
|
|
|
|
in (v₄ , (v₃≈v₄ , I⊔.union-preserves-∈₂ k∉km₂ k,v₄∈m₄))
|
|
|
|
|
@ -690,9 +689,8 @@ private module I⊓ = ImplInsert _⊓₂_
|
|
|
|
|
where
|
|
|
|
|
⊓-⊆ : ∀ (m₁ m₂ m₃ m₄ : Map) → m₁ ≈ m₂ → m₃ ≈ m₄ → (m₁ ⊓ m₃) ⊆ (m₂ ⊓ m₄)
|
|
|
|
|
⊓-⊆ m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
|
|
|
|
|
with Expr-Provenance k ((` m₁) ∩ (` m₃)) (∈-cong proj₁ k,v∈m₁m₃)
|
|
|
|
|
... | (_ , (bothⁱ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) , v₁v₃∈m₁m₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊓ m₃} k,v∈m₁m₃ v₁v₃∈m₁m₃ =
|
|
|
|
|
with Expr-Provenance-≡ ((` m₁) ∩ (` m₃)) k,v∈m₁m₃
|
|
|
|
|
... | bothⁱ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) =
|
|
|
|
|
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
|
|
|
|
|
(v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
|
|
|
|
|
in (v₂ ⊓₂ v₄ , (≈₂-⊓₂-cong v₁≈v₂ v₃≈v₄ , I⊓.intersect-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
|
|
|
|
|
@ -702,13 +700,12 @@ private module I⊓ = ImplInsert _⊓₂_
|
|
|
|
|
where
|
|
|
|
|
mm-m-⊆ : (m ⊔ m) ⊆ m
|
|
|
|
|
mm-m-⊆ k v k,v∈mm
|
|
|
|
|
with Expr-Provenance k ((` m) ∪ (` m)) (∈-cong proj₁ k,v∈mm)
|
|
|
|
|
... | (_ , (bothᵘ (single {v'} v'∈m) (single {v''} v''∈m) , v'v''∈mm))
|
|
|
|
|
rewrite Map-functional {m = m} v'∈m v''∈m
|
|
|
|
|
rewrite Map-functional {m = m ⊔ m} k,v∈mm v'v''∈mm =
|
|
|
|
|
with Expr-Provenance-≡ ((` m) ∪ (` m)) k,v∈mm
|
|
|
|
|
... | bothᵘ (single {v'} v'∈m) (single {v''} v''∈m)
|
|
|
|
|
rewrite Map-functional {m = m} v'∈m v''∈m =
|
|
|
|
|
(v'' , (⊔₂-idemp v'' , v''∈m))
|
|
|
|
|
... | (_ , (in₁ (single {v'} v'∈m) k∉km , _)) = ⊥-elim (k∉km (∈-cong proj₁ v'∈m))
|
|
|
|
|
... | (_ , (in₂ k∉km (single {v''} v''∈m) , _)) = ⊥-elim (k∉km (∈-cong proj₁ v''∈m))
|
|
|
|
|
... | in₁ (single {v'} v'∈m) k∉km = ⊥-elim (k∉km (∈-cong proj₁ v'∈m))
|
|
|
|
|
... | in₂ k∉km (single {v''} v''∈m) = ⊥-elim (k∉km (∈-cong proj₁ v''∈m))
|
|
|
|
|
|
|
|
|
|
m-mm-⊆ : m ⊆ (m ⊔ m)
|
|
|
|
|
m-mm-⊆ k v k,v∈m = (v ⊔₂ v , (≈₂-sym (⊔₂-idemp v) , I⊔.union-combines u u k,v∈m k,v∈m))
|
|
|
|
|
@ -718,15 +715,12 @@ private module I⊓ = ImplInsert _⊓₂_
|
|
|
|
|
where
|
|
|
|
|
⊔-comm-⊆ : ∀ (m₁ m₂ : Map) → (m₁ ⊔ m₂) ⊆ (m₂ ⊔ m₁)
|
|
|
|
|
⊔-comm-⊆ m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
|
|
|
|
|
with Expr-Provenance k ((` m₁) ∪ (` m₂)) (∈-cong proj₁ k,v∈m₁m₂)
|
|
|
|
|
... | (_ , (bothᵘ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) , v₁v₂∈m₁m₂))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
|
|
|
|
|
with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈m₁m₂
|
|
|
|
|
... | bothᵘ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) =
|
|
|
|
|
(v₂ ⊔₂ v₁ , (⊔₂-comm v₁ v₂ , I⊔.union-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
|
|
|
|
|
... | (_ , (in₁ {v₁} (single v₁∈m₁) k∉km₂ , v₁∈m₁m₂))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₁∈m₁m₂ =
|
|
|
|
|
... | in₁ {v₁} (single v₁∈m₁) k∉km₂ =
|
|
|
|
|
(v₁ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉km₂ v₁∈m₁))
|
|
|
|
|
... | (_ , (in₂ {v₂} k∉km₁ (single v₂∈m₂) , v₂∈m₁m₂))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
|
|
|
|
|
... | in₂ {v₂} k∉km₁ (single v₂∈m₂) =
|
|
|
|
|
(v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ u₂ v₂∈m₂ k∉km₁))
|
|
|
|
|
|
|
|
|
|
⊔-assoc : ∀ (m₁ m₂ m₃ : Map) → ((m₁ ⊔ m₂) ⊔ m₃) ≈ (m₁ ⊔ (m₂ ⊔ m₃))
|
|
|
|
|
@ -734,54 +728,40 @@ private module I⊓ = ImplInsert _⊓₂_
|
|
|
|
|
where
|
|
|
|
|
⊔-assoc₁ : ((m₁ ⊔ m₂) ⊔ m₃) ⊆ (m₁ ⊔ (m₂ ⊔ m₃))
|
|
|
|
|
⊔-assoc₁ k v k,v∈m₁₂m₃
|
|
|
|
|
with Expr-Provenance k (((` m₁) ∪ (` m₂)) ∪ (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
|
|
|
|
|
... | (_ , (in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) , v₃∈m₁₂m₃))
|
|
|
|
|
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₃∈m₁₂m₃ =
|
|
|
|
|
with Expr-Provenance-≡ (((` m₁) ∪ (` m₂)) ∪ (` m₃)) k,v∈m₁₂m₃
|
|
|
|
|
... | in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) =
|
|
|
|
|
let (k∉ke₁ , k∉ke₂) = I⊔.∉-union-∉-either {l₁ = l₁} {l₂ = l₂} k∉ke₁₂
|
|
|
|
|
in (v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
|
|
|
|
|
... | (_ , (in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ , v₂∈m₁₂m₃))
|
|
|
|
|
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₂∈m₁₂m₃ =
|
|
|
|
|
... | in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ =
|
|
|
|
|
(v₂ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
|
|
|
|
|
... | (_ , (bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₂v₃∈m₁₂m₃))
|
|
|
|
|
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₂v₃∈m₁₂m₃ =
|
|
|
|
|
... | bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
|
|
|
|
|
(v₂ ⊔₂ v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
|
|
|
|
|
... | (_ , (in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ , v₁∈m₁₂m₃))
|
|
|
|
|
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁∈m₁₂m₃ =
|
|
|
|
|
... | in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ =
|
|
|
|
|
(v₁ , (≈₂-refl , I⊔.union-preserves-∈₁ u₁ v₁∈e₁ (I⊔.union-preserves-∉ k∉ke₂ k∉ke₃)))
|
|
|
|
|
... | (_ , (bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) , v₁v₃∈m₁₂m₃))
|
|
|
|
|
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₃∈m₁₂m₃ =
|
|
|
|
|
... | bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) =
|
|
|
|
|
(v₁ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
|
|
|
|
|
... | (_ , (in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃), v₁v₂∈m₁₂m₃)
|
|
|
|
|
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₂∈m₁₂m₃ =
|
|
|
|
|
... | in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃ =
|
|
|
|
|
(v₁ ⊔₂ v₂ , (≈₂-refl , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
|
|
|
|
|
... | (_ , (bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
|
|
|
|
|
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
|
|
|
|
|
... | bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
|
|
|
|
|
(v₁ ⊔₂ (v₂ ⊔₂ v₃) , (⊔₂-assoc v₁ v₂ v₃ , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
|
|
|
|
|
|
|
|
|
|
⊔-assoc₂ : (m₁ ⊔ (m₂ ⊔ m₃)) ⊆ ((m₁ ⊔ m₂) ⊔ m₃)
|
|
|
|
|
⊔-assoc₂ k v k,v∈m₁m₂₃
|
|
|
|
|
with Expr-Provenance k ((` m₁) ∪ ((` m₂) ∪ (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
|
|
|
|
|
... | (_ , (in₂ k∉ke₁ (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) , v₃∈m₁m₂₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₃∈m₁m₂₃ =
|
|
|
|
|
with Expr-Provenance-≡ ((` m₁) ∪ ((` m₂) ∪ (` m₃))) k,v∈m₁m₂₃
|
|
|
|
|
... | in₂ k∉ke₁ (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) =
|
|
|
|
|
(v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ (I⊔.union-preserves-∉ k∉ke₁ k∉ke₂) v₃∈e₃))
|
|
|
|
|
... | (_ , (in₂ k∉ke₁ (in₁ (single {v₂} v₂∈e₂) k∉ke₃) , v₂∈m₁m₂₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₂∈m₁m₂₃ =
|
|
|
|
|
... | in₂ k∉ke₁ (in₁ (single {v₂} v₂∈e₂) k∉ke₃) =
|
|
|
|
|
(v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-preserves-∈₂ k∉ke₁ v₂∈e₂) k∉ke₃))
|
|
|
|
|
... | (_ , (in₂ k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₂v₃∈m₁m₂₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₂v₃∈m₁m₂₃ =
|
|
|
|
|
... | in₂ k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
|
|
|
|
|
(v₂ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-preserves-∈₂ k∉ke₁ v₂∈e₂) v₃∈e₃))
|
|
|
|
|
... | (_ , (in₁ (single {v₁} v₁∈e₁) k∉ke₂₃ , v₁∈m₁m₂₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁∈m₁m₂₃ =
|
|
|
|
|
... | in₁ (single {v₁} v₁∈e₁) k∉ke₂₃ =
|
|
|
|
|
let (k∉ke₂ , k∉ke₃) = I⊔.∉-union-∉-either {l₁ = l₂} {l₂ = l₃} k∉ke₂₃
|
|
|
|
|
in (v₁ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-preserves-∈₁ u₁ v₁∈e₁ k∉ke₂) k∉ke₃))
|
|
|
|
|
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) , v₁v₃∈m₁m₂₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₃∈m₁m₂₃ =
|
|
|
|
|
... | bothᵘ (single {v₁} v₁∈e₁) (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) =
|
|
|
|
|
(v₁ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-preserves-∈₁ u₁ v₁∈e₁ k∉ke₂) v₃∈e₃))
|
|
|
|
|
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₁ (single {v₂} v₂∈e₂) k∉ke₃) , v₁v₂∈m₁m₂₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₂∈m₁m₂₃ =
|
|
|
|
|
... | bothᵘ (single {v₁} v₁∈e₁) (in₁ (single {v₂} v₂∈e₂) k∉ke₃) =
|
|
|
|
|
(v₁ ⊔₂ v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-combines u₁ u₂ v₁∈e₁ v₂∈e₂) k∉ke₃))
|
|
|
|
|
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
|
|
|
|
|
... | bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
|
|
|
|
|
((v₁ ⊔₂ v₂) ⊔₂ v₃ , (≈₂-sym (⊔₂-assoc v₁ v₂ v₃) , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-combines u₁ u₂ v₁∈e₁ v₂∈e₂) v₃∈e₃))
|
|
|
|
|
|
|
|
|
|
⊓-idemp : ∀ (m : Map) → (m ⊓ m) ≈ m
|
|
|
|
|
@ -789,10 +769,9 @@ private module I⊓ = ImplInsert _⊓₂_
|
|
|
|
|
where
|
|
|
|
|
mm-m-⊆ : (m ⊓ m) ⊆ m
|
|
|
|
|
mm-m-⊆ k v k,v∈mm
|
|
|
|
|
with Expr-Provenance k ((` m) ∩ (` m)) (∈-cong proj₁ k,v∈mm)
|
|
|
|
|
... | (_ , (bothⁱ (single {v'} v'∈m) (single {v''} v''∈m) , v'v''∈mm))
|
|
|
|
|
rewrite Map-functional {m = m} v'∈m v''∈m
|
|
|
|
|
rewrite Map-functional {m = m ⊓ m} k,v∈mm v'v''∈mm =
|
|
|
|
|
with Expr-Provenance-≡ ((` m) ∩ (` m)) k,v∈mm
|
|
|
|
|
... | bothⁱ (single {v'} v'∈m) (single {v''} v''∈m)
|
|
|
|
|
rewrite Map-functional {m = m} v'∈m v''∈m =
|
|
|
|
|
(v'' , (⊓₂-idemp v'' , v''∈m))
|
|
|
|
|
|
|
|
|
|
m-mm-⊆ : m ⊆ (m ⊓ m)
|
|
|
|
|
@ -803,9 +782,8 @@ private module I⊓ = ImplInsert _⊓₂_
|
|
|
|
|
where
|
|
|
|
|
⊓-comm-⊆ : ∀ (m₁ m₂ : Map) → (m₁ ⊓ m₂) ⊆ (m₂ ⊓ m₁)
|
|
|
|
|
⊓-comm-⊆ m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
|
|
|
|
|
with Expr-Provenance k ((` m₁) ∩ (` m₂)) (∈-cong proj₁ k,v∈m₁m₂)
|
|
|
|
|
... | (_ , (bothⁱ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) , v₁v₂∈m₁m₂))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊓ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
|
|
|
|
|
with Expr-Provenance-≡ ((` m₁) ∩ (` m₂)) k,v∈m₁m₂
|
|
|
|
|
... | bothⁱ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) =
|
|
|
|
|
(v₂ ⊓₂ v₁ , (⊓₂-comm v₁ v₂ , I⊓.intersect-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
|
|
|
|
|
|
|
|
|
|
⊓-assoc : ∀ (m₁ m₂ m₃ : Map) → ((m₁ ⊓ m₂) ⊓ m₃) ≈ (m₁ ⊓ (m₂ ⊓ m₃))
|
|
|
|
|
@ -813,16 +791,14 @@ private module I⊓ = ImplInsert _⊓₂_
|
|
|
|
|
where
|
|
|
|
|
⊓-assoc₁ : ((m₁ ⊓ m₂) ⊓ m₃) ⊆ (m₁ ⊓ (m₂ ⊓ m₃))
|
|
|
|
|
⊓-assoc₁ k v k,v∈m₁₂m₃
|
|
|
|
|
with Expr-Provenance k (((` m₁) ∩ (` m₂)) ∩ (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
|
|
|
|
|
... | (_ , (bothⁱ (bothⁱ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
|
|
|
|
|
rewrite Map-functional {m = (m₁ ⊓ m₂) ⊓ m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
|
|
|
|
|
with Expr-Provenance-≡ (((` m₁) ∩ (` m₂)) ∩ (` m₃)) k,v∈m₁₂m₃
|
|
|
|
|
... | bothⁱ (bothⁱ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
|
|
|
|
|
(v₁ ⊓₂ (v₂ ⊓₂ v₃) , (⊓₂-assoc v₁ v₂ v₃ , I⊓.intersect-combines u₁ (I⊓.intersect-preserves-Unique {l₂} {l₃} u₃) v₁∈e₁ (I⊓.intersect-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
|
|
|
|
|
|
|
|
|
|
⊓-assoc₂ : (m₁ ⊓ (m₂ ⊓ m₃)) ⊆ ((m₁ ⊓ m₂) ⊓ m₃)
|
|
|
|
|
⊓-assoc₂ k v k,v∈m₁m₂₃
|
|
|
|
|
with Expr-Provenance k ((` m₁) ∩ ((` m₂) ∩ (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
|
|
|
|
|
... | (_ , (bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊓ (m₂ ⊓ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
|
|
|
|
|
with Expr-Provenance-≡ ((` m₁) ∩ ((` m₂) ∩ (` m₃))) k,v∈m₁m₂₃
|
|
|
|
|
... | bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
|
|
|
|
|
((v₁ ⊓₂ v₂) ⊓₂ v₃ , (≈₂-sym (⊓₂-assoc v₁ v₂ v₃) , I⊓.intersect-combines (I⊓.intersect-preserves-Unique {l₁} {l₂} u₂) u₃ (I⊓.intersect-combines u₁ u₂ v₁∈e₁ v₂∈e₂) v₃∈e₃))
|
|
|
|
|
|
|
|
|
|
absorb-⊓-⊔ : ∀ (m₁ m₂ : Map) → (m₁ ⊓ (m₁ ⊔ m₂)) ≈ m₁
|
|
|
|
|
@ -830,20 +806,18 @@ absorb-⊓-⊔ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊓-⊔¹ , absor
|
|
|
|
|
where
|
|
|
|
|
absorb-⊓-⊔¹ : (m₁ ⊓ (m₁ ⊔ m₂)) ⊆ m₁
|
|
|
|
|
absorb-⊓-⊔¹ k v k,v∈m₁m₁₂
|
|
|
|
|
with Expr-Provenance k ((` m₁) ∩ ((` m₁) ∪ (` m₂))) (∈-cong proj₁ k,v∈m₁m₁₂)
|
|
|
|
|
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
|
|
|
|
|
(bothᵘ (single {v₁'} k,v₁'∈m₁)
|
|
|
|
|
(single {v₂} v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
|
|
|
|
|
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊓ (m₁ ⊔ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
|
|
|
|
|
with Expr-Provenance-≡ ((` m₁) ∩ ((` m₁) ∪ (` m₂))) k,v∈m₁m₁₂
|
|
|
|
|
... | bothⁱ (single {v₁} k,v₁∈m₁)
|
|
|
|
|
(bothᵘ (single {v₁'} k,v₁'∈m₁)
|
|
|
|
|
(single {v₂} v₂∈m₂))
|
|
|
|
|
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
|
|
|
|
|
(v₁' , (absorb-⊓₂-⊔₂ v₁' v₂ , k,v₁'∈m₁))
|
|
|
|
|
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
|
|
|
|
|
(in₁ (single {v₁'} k,v₁'∈m₁) _) , v₁v₁'∈m₁m₁₂))
|
|
|
|
|
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊓ (m₁ ⊔ m₂)} k,v∈m₁m₁₂ v₁v₁'∈m₁m₁₂ =
|
|
|
|
|
... | bothⁱ (single {v₁} k,v₁∈m₁)
|
|
|
|
|
(in₁ (single {v₁'} k,v₁'∈m₁) _)
|
|
|
|
|
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
|
|
|
|
|
(v₁' , (⊓₂-idemp v₁' , k,v₁'∈m₁))
|
|
|
|
|
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
|
|
|
|
|
(in₂ k∉m₁ _ ) , _)) = ⊥-elim (k∉m₁ (∈-cong proj₁ k,v₁∈m₁))
|
|
|
|
|
... | bothⁱ (single {v₁} k,v₁∈m₁)
|
|
|
|
|
(in₂ k∉m₁ _ ) = ⊥-elim (k∉m₁ (∈-cong proj₁ k,v₁∈m₁))
|
|
|
|
|
|
|
|
|
|
absorb-⊓-⊔² : m₁ ⊆ (m₁ ⊓ (m₁ ⊔ m₂))
|
|
|
|
|
absorb-⊓-⊔² k v k,v∈m₁
|
|
|
|
|
@ -858,18 +832,16 @@ absorb-⊔-⊓ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊔-⊓¹ , absor
|
|
|
|
|
where
|
|
|
|
|
absorb-⊔-⊓¹ : (m₁ ⊔ (m₁ ⊓ m₂)) ⊆ m₁
|
|
|
|
|
absorb-⊔-⊓¹ k v k,v∈m₁m₁₂
|
|
|
|
|
with Expr-Provenance k ((` m₁) ∪ ((` m₁) ∩ (` m₂))) (∈-cong proj₁ k,v∈m₁m₁₂)
|
|
|
|
|
... | (_ , (bothᵘ (single {v₁} k,v₁∈m₁)
|
|
|
|
|
(bothⁱ (single {v₁'} k,v₁'∈m₁)
|
|
|
|
|
(single {v₂} k,v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
|
|
|
|
|
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ (m₁ ⊓ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
|
|
|
|
|
with Expr-Provenance-≡ ((` m₁) ∪ ((` m₁) ∩ (` m₂))) k,v∈m₁m₁₂
|
|
|
|
|
... | bothᵘ (single {v₁} k,v₁∈m₁)
|
|
|
|
|
(bothⁱ (single {v₁'} k,v₁'∈m₁)
|
|
|
|
|
(single {v₂} k,v₂∈m₂))
|
|
|
|
|
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
|
|
|
|
|
(v₁' , (absorb-⊔₂-⊓₂ v₁' v₂ , k,v₁'∈m₁))
|
|
|
|
|
... | (_ , (in₁ (single {v₁} k,v₁∈m₁) k∉km₁₂ , k,v₁∈m₁m₁₂))
|
|
|
|
|
rewrite Map-functional {m = m₁ ⊔ (m₁ ⊓ m₂)} k,v∈m₁m₁₂ k,v₁∈m₁m₁₂ =
|
|
|
|
|
... | in₁ (single {v₁} k,v₁∈m₁) k∉km₁₂ =
|
|
|
|
|
(v₁ , (≈₂-refl , k,v₁∈m₁))
|
|
|
|
|
... | (_ , (in₂ k∉km₁ (bothⁱ (single {v₁'} k,v₁'∈m₁)
|
|
|
|
|
(single {v₂} k,v₂∈m₂)) , _)) =
|
|
|
|
|
... | in₂ k∉km₁ (bothⁱ (single {v₁'} k,v₁'∈m₁)
|
|
|
|
|
(single {v₂} k,v₂∈m₂)) =
|
|
|
|
|
⊥-elim (k∉km₁ (∈-cong proj₁ k,v₁'∈m₁))
|
|
|
|
|
|
|
|
|
|
absorb-⊔-⊓² : m₁ ⊆ (m₁ ⊔ (m₁ ⊓ m₂))
|
|
|
|
|
@ -1009,7 +981,7 @@ updating-via-k∈ks-forward m {ks} f k∈ks k∈km rewrite transform-keys-≡ (p
|
|
|
|
|
updating-via-k∈ks-≡ : ∀ (m : Map) {ks : List A} (f : A → B) {k : A} {v : B} →
|
|
|
|
|
k ∈ˡ ks → (k , v) ∈ (m updating ks via f)→ v ≡ f k
|
|
|
|
|
updating-via-k∈ks-≡ m {ks} f k∈ks k,v∈um
|
|
|
|
|
with updating-via-k∈ks m f k∈ks (forget {m = (m updating ks via f)} k,v∈um)
|
|
|
|
|
with updating-via-k∈ks m f k∈ks (forget k,v∈um)
|
|
|
|
|
... | k,fk∈um = Map-functional {m = (m updating ks via f)} k,v∈um k,fk∈um
|
|
|
|
|
|
|
|
|
|
updating-via-k∉ks-forward : ∀ (m : Map) {ks : List A} (f : A → B) {k : A} {v : B} →
|
|
|
|
|
@ -1044,14 +1016,14 @@ module _ {l} {L : Set l}
|
|
|
|
|
|
|
|
|
|
f'l₁f'l₂⊆f'l₂ : ((f' l₁) ⊔ (f' l₂)) ⊆ f' l₂
|
|
|
|
|
f'l₁f'l₂⊆f'l₂ k v k,v∈f'l₁f'l₂
|
|
|
|
|
with Expr-Provenance-≡ k v ((` (f' l₁)) ∪ (` (f' l₂))) k,v∈f'l₁f'l₂
|
|
|
|
|
with Expr-Provenance-≡ ((` (f' l₁)) ∪ (` (f' l₂))) k,v∈f'l₁f'l₂
|
|
|
|
|
... | in₁ (single k,v∈f'l₁) k∉kf'l₂ =
|
|
|
|
|
let
|
|
|
|
|
k∈kfl₁ = updating-via-∈k-backward (f l₁) ks (updater l₁) (forget {m = f' l₁} k,v∈f'l₁)
|
|
|
|
|
k∈kfl₁ = updating-via-∈k-backward (f l₁) ks (updater l₁) (forget k,v∈f'l₁)
|
|
|
|
|
k∈kfl₁fl₂ = union-preserves-∈k₁ {l₁ = proj₁ (f l₁)} {l₂ = proj₁ (f l₂)} k∈kfl₁
|
|
|
|
|
(v' , k,v'∈fl₁l₂) = locate {m = (f l₁ ⊔ f l₂)} k∈kfl₁fl₂
|
|
|
|
|
(v'' , (v'≈v'' , k,v''∈fl₂)) = fl₁fl₂⊆fl₂ k v' k,v'∈fl₁l₂
|
|
|
|
|
k∈kf'l₂ = updating-via-∈k-forward (f l₂) ks (updater l₂) (forget {m = f l₂} k,v''∈fl₂)
|
|
|
|
|
k∈kf'l₂ = updating-via-∈k-forward (f l₂) ks (updater l₂) (forget k,v''∈fl₂)
|
|
|
|
|
in
|
|
|
|
|
⊥-elim (k∉kf'l₂ k∈kf'l₂)
|
|
|
|
|
... | in₂ k∉kf'l₁ (single k,v'∈f'l₂) =
|
|
|
|
|
@ -1074,10 +1046,10 @@ module _ {l} {L : Set l}
|
|
|
|
|
|
|
|
|
|
f'l₂⊆f'l₁f'l₂ : f' l₂ ⊆ ((f' l₁) ⊔ (f' l₂))
|
|
|
|
|
f'l₂⊆f'l₁f'l₂ k v k,v∈f'l₂
|
|
|
|
|
with k∈kfl₂ ← updating-via-∈k-backward (f l₂) ks (updater l₂) (forget {m = f' l₂} k,v∈f'l₂)
|
|
|
|
|
with k∈kfl₂ ← updating-via-∈k-backward (f l₂) ks (updater l₂) (forget k,v∈f'l₂)
|
|
|
|
|
with (v' , k,v'∈fl₂) ← locate {m = f l₂} k∈kfl₂
|
|
|
|
|
with (v'' , (v'≈v'' , k,v''∈fl₁fl₂)) ← fl₂⊆fl₁fl₂ k v' k,v'∈fl₂
|
|
|
|
|
with Expr-Provenance-≡ k v'' ((` (f l₁)) ∪ (` (f l₂))) k,v''∈fl₁fl₂
|
|
|
|
|
with Expr-Provenance-≡ ((` (f l₁)) ∪ (` (f l₂))) k,v''∈fl₁fl₂
|
|
|
|
|
... | in₁ (single k,v''∈fl₁) k∉kfl₂ = ⊥-elim (k∉kfl₂ k∈kfl₂)
|
|
|
|
|
... | in₂ k∉kfl₁ (single k,v''∈fl₂) =
|
|
|
|
|
let
|
|
|
|
|
@ -1088,8 +1060,8 @@ module _ {l} {L : Set l}
|
|
|
|
|
with k∈-dec k ks
|
|
|
|
|
... | yes k∈ks with refl ← updating-via-k∈ks-≡ (f l₂) (updater l₂) k∈ks k,v∈f'l₂ =
|
|
|
|
|
let
|
|
|
|
|
k,uv₁∈f'l₁ = updating-via-k∈ks-forward (f l₁) (updater l₁) k∈ks (forget {m = f l₁} k,v₁∈fl₁)
|
|
|
|
|
k,uv₂∈f'l₂ = updating-via-k∈ks-forward (f l₂) (updater l₂) k∈ks (forget {m = f l₂} k,v₂∈fl₂)
|
|
|
|
|
k,uv₁∈f'l₁ = updating-via-k∈ks-forward (f l₁) (updater l₁) k∈ks (forget k,v₁∈fl₁)
|
|
|
|
|
k,uv₂∈f'l₂ = updating-via-k∈ks-forward (f l₂) (updater l₂) k∈ks (forget k,v₂∈fl₂)
|
|
|
|
|
k,uv₁uv₂∈f'l₁f'l₂ = ⊔-combines {m₁ = f' l₁} {m₂ = f' l₂} k,uv₁∈f'l₁ k,uv₂∈f'l₂
|
|
|
|
|
in
|
|
|
|
|
(updater l₁ k ⊔₂ updater l₂ k , (IsLattice.≈-sym lB (g-Monotonicʳ k l₁≼l₂) , k,uv₁uv₂∈f'l₁f'l₂))
|
|
|
|
|
|
Danila Fedorin