More tweaks to naming and style

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-07-30 13:46:52 -07:00
parent 26db4cc86c
commit eaee73236f

View File

@ -23,7 +23,7 @@ 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 []
push : forall {x : C} {xs : List C} push : {x : C} {xs : List C}
All (λ x' ¬ x x') xs All (λ x' ¬ x x') xs
Unique xs Unique xs
Unique (x xs) Unique (x xs)
@ -169,18 +169,18 @@ private module ImplInsert (f : B → B → B) where
let (v , k,v∈l) = locate k∈kl let (v , k,v∈l) = locate k∈kl
in ∈-cong proj₁ (insert-preserves-∈ k≢k' k,v∈l) in ∈-cong proj₁ (insert-preserves-∈ k≢k' k,v∈l)
insert-preserves-∉ : {k k' : A} {v' : B} {l : List (A × B)} insert-preserves-∉k : {k k' : A} {v' : B} {l : List (A × B)}
¬ k k' ¬ k ∈k l ¬ k ∈k insert k' v' l ¬ k k' ¬ k ∈k l ¬ k ∈k insert k' v' l
insert-preserves-∉ {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k' insert-preserves-∉k {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k'
insert-preserves-∉ {l = []} k≢k' k∉kl (there ()) insert-preserves-∉k {l = []} k≢k' k∉kl (there ())
insert-preserves-∉ {k} {k'} {v'} {(k'' , v'') xs} k≢k' k∉kl k∈kil insert-preserves-∉k {k} {k'} {v'} {(k'' , v'') xs} k≢k' k∉kl k∈kil
with ≡-dec-A k k'' with ≡-dec-A k k''
... | yes k≡k'' = k∉kl (here k≡k'') ... | yes k≡k'' = k∉kl (here k≡k'')
... | no k≢k'' with ≡-dec-A k' k'' | k∈kil ... | no k≢k'' with ≡-dec-A k' k'' | k∈kil
... | yes k'≡k'' | here k≡k'' = k≢k'' k≡k'' ... | yes k'≡k'' | here k≡k'' = k≢k'' k≡k''
... | yes k'≡k'' | there k∈kxs = k∉kl (there k∈kxs) ... | yes k'≡k'' | there k∈kxs = k∉kl (there k∈kxs)
... | no k'≢k'' | here k≡k'' = k∉kl (here k≡k'') ... | no k'≢k'' | here k≡k'' = k∉kl (here k≡k'')
... | no k'≢k'' | there k∈kxs = insert-preserves-∉ k≢k' ... | no k'≢k'' | there k∈kxs = insert-preserves-∉k k≢k'
(λ k∈kxs k∉kl (there k∈kxs)) k∈kxs (λ k∈kxs k∉kl (there k∈kxs)) k∈kxs
merge-preserves-∉ : {k : A} {l₁ l₂ : List (A × B)} merge-preserves-∉ : {k : A} {l₁ l₂ : List (A × B)}
@ -189,13 +189,13 @@ private module ImplInsert (f : B → B → B) where
merge-preserves-∉ {k} {(k' , v') xs₁} k∉kl₁ k∉kl₂ merge-preserves-∉ {k} {(k' , v') xs₁} k∉kl₁ k∉kl₂
with ≡-dec-A k k' with ≡-dec-A k k'
... | yes k≡k' = absurd (k∉kl₁ (here k≡k')) ... | yes k≡k' = absurd (k∉kl₁ (here k≡k'))
... | no k≢k' = insert-preserves-∉ k≢k' (merge-preserves-∉ (λ k∈kxs₁ k∉kl₁ (there k∈kxs₁)) k∉kl₂) ... | no k≢k' = insert-preserves-∉k k≢k' (merge-preserves-∉ (λ k∈kxs₁ k∉kl₁ (there k∈kxs₁)) k∉kl₂)
merge-preserves-keys : {k : A} {v : B} {l₁ l₂ : List (A × B)} merge-preserves- : {k : A} {v : B} {l₁ l₂ : List (A × B)}
¬ k ∈k l₁ (k , v) l₂ (k , v) merge l₁ l₂ ¬ k ∈k l₁ (k , v) l₂ (k , v) merge l₁ l₂
merge-preserves-keys {l₁ = []} _ k,v∈l₂ = k,v∈l₂ merge-preserves- {l₁ = []} _ k,v∈l₂ = k,v∈l₂
merge-preserves-keys {l₁ = (k' , v') xs₁} k∉kl₁ k,v∈l₂ = merge-preserves- {l₁ = (k' , v') xs₁} k∉kl₁ k,v∈l₂ =
let recursion = merge-preserves-keys (λ k∈xs₁ k∉kl₁ (there k∈xs₁)) k,v∈l₂ let recursion = merge-preserves- (λ k∈xs₁ k∉kl₁ (there k∈xs₁)) k,v∈l₂
in insert-preserves-∈ (λ k≡k' k∉kl₁ (here k≡k')) recursion in insert-preserves-∈ (λ k≡k' k∉kl₁ (here k≡k')) recursion
insert-fresh : {k : A} {v : B} {l : List (A × B)} insert-fresh : {k : A} {v : B} {l : List (A × B)}
@ -206,18 +206,18 @@ private module ImplInsert (f : B → B → B) where
... | yes k≡k' = absurd (k∉kl (here k≡k')) ... | yes k≡k' = absurd (k∉kl (here k≡k'))
... | no _ = there (insert-fresh (λ k∈kxs k∉kl (there k∈kxs))) ... | no _ = there (insert-fresh (λ k∈kxs k∉kl (there k∈kxs)))
merge-preserves-keys : {k : A} {v : B} {l₁ l₂ : List (A × B)} merge-preserves- : {k : A} {v : B} {l₁ l₂ : List (A × B)}
Unique (keys l₁) (k , v) l₁ ¬ k ∈k l₂ (k , v) merge l₁ l₂ Unique (keys l₁) (k , v) l₁ ¬ k ∈k l₂ (k , v) merge l₁ l₂
merge-preserves-keys {k} {v} {(k' , v') xs₁} (push k'≢xs₁ uxs₁) (there k,v∈xs₁) k∉kl₂ = merge-preserves- {k} {v} {(k' , v') xs₁} (push k'≢xs₁ uxs₁) (there k,v∈xs₁) k∉kl₂ =
insert-preserves-∈ k≢k' k,v∈mxs₁l insert-preserves-∈ k≢k' k,v∈mxs₁l
where where
k,v∈mxs₁l = merge-preserves-keys uxs₁ k,v∈xs₁ k∉kl₂ k,v∈mxs₁l = merge-preserves- uxs₁ k,v∈xs₁ k∉kl₂
k≢k' : ¬ k k' k≢k' : ¬ k k'
k≢k' with ≡-dec-A k k' k≢k' with ≡-dec-A k k'
... | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁)) ... | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁))
... | no k≢k' = k≢k' ... | no k≢k' = k≢k'
merge-preserves-keys {l₁ = (k' , v') xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂ merge-preserves- {l₁ = (k' , v') xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂
rewrite cong proj₁ k,v≡k',v' rewrite cong proj₂ k,v≡k',v' = rewrite cong proj₁ k,v≡k',v' rewrite cong proj₂ k,v≡k',v' =
insert-fresh (merge-preserves-∉ (All¬-¬Any k'≢xs₁) k∉kl₂) insert-fresh (merge-preserves-∉ (All¬-¬Any k'≢xs₁) k∉kl₂)
@ -233,12 +233,12 @@ private module ImplInsert (f : B → B → B) where
... | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs (∈-cong proj₁ k,v'∈xs)) ... | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs (∈-cong proj₁ k,v'∈xs))
... | no k≢k' = there (insert-combines uxs k,v'∈xs) ... | no k≢k' = there (insert-combines uxs k,v'∈xs)
merge-combines : forall {k : A} {v₁ v₂ : B} {l₁ l₂ : List (A × B)} merge-combines : {k : A} {v₁ v₂ : B} {l₁ l₂ : List (A × B)}
Unique (keys l₁) Unique (keys l₂) Unique (keys l₁) Unique (keys l₂)
(k , v₁) l₁ (k , v₂) l₂ (k , f v₁ v₂) merge l₁ l₂ (k , v₁) l₁ (k , v₂) l₂ (k , f v₁ v₂) merge l₁ l₂
merge-combines {l₁ = (k' , v) xs₁} {l₂} (push k'≢xs₁ uxs₁) ul₂ (here k,v₁≡k',v) k,v₂∈l₂ merge-combines {l₁ = (k' , v) xs₁} {l₂} (push k'≢xs₁ uxs₁) ul₂ (here k,v₁≡k',v) k,v₂∈l₂
rewrite cong proj₁ (sym (k,v₁≡k',v)) rewrite cong proj₂ (sym (k,v₁≡k',v)) = rewrite cong proj₁ (sym (k,v₁≡k',v)) rewrite cong proj₂ (sym (k,v₁≡k',v)) =
insert-combines (merge-preserves-Unique xs₁ l₂ ul₂) (merge-preserves-keys (All¬-¬Any k'≢xs₁) k,v₂∈l₂) insert-combines (merge-preserves-Unique xs₁ l₂ ul₂) (merge-preserves- (All¬-¬Any k'≢xs₁) k,v₂∈l₂)
merge-combines {k} {l₁ = (k' , v) xs₁} (push k'≢xs₁ uxs₁) ul₂ (there k,v₁∈xs₁) k,v₂∈l₂ = merge-combines {k} {l₁ = (k' , v) xs₁} (push k'≢xs₁ uxs₁) ul₂ (there k,v₁∈xs₁) k,v₂∈l₂ =
insert-preserves-∈ k≢k' (merge-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂) insert-preserves-∈ k≢k' (merge-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂)
where where
@ -295,12 +295,12 @@ module _ (f : B → B → B) where
let let
(v₁ , k,v₁∈l₁) = locate k∈kl₁ (v₁ , k,v₁∈l₁) = locate k∈kl₁
in in
(in v₁ k,v₁∈l₁ k∉kl₂ , merge-preserves-keys u₁ k,v₁∈l₁ k∉kl₂) (in v₁ k,v₁∈l₁ k∉kl₂ , merge-preserves- u₁ k,v₁∈l₁ k∉kl₂)
... | no k∉kl₁ | yes k∈kl₂ = ... | no k∉kl₁ | yes k∈kl₂ =
let let
(v₂ , k,v₂∈l₂) = locate k∈kl₂ (v₂ , k,v₂∈l₂) = locate k∈kl₂
in in
(in v₂ k∉kl₁ k,v₂∈l₂ , merge-preserves-keys k∉kl₁ k,v₂∈l₂) (in v₂ k∉kl₁ k,v₂∈l₂ , merge-preserves- k∉kl₁ k,v₂∈l₂)
... | no k∉kl₁ | no k∉kl₂ = absurd (merge-preserves-∉ k∉kl₁ k∉kl₂ k∈km₁m₂) ... | no k∉kl₁ | no k∉kl₂ = absurd (merge-preserves-∉ k∉kl₁ k∉kl₂ k∈km₁m₂)
module _ (_≈_ : B B Set b) where module _ (_≈_ : B B Set b) where
@ -314,7 +314,7 @@ module _ (_≈_ : B → B → Set b) where
module _ (f : B B B) where module _ (f : B B B) where
module _ (f-comm : (b₁ b₂ : B) f b₁ b₂ f b₂ b₁) where module _ (f-comm : (b₁ b₂ : B) f b₁ b₂ f b₂ b₁) where
merge-comm : forall (m₁ m₂ : Map) lift (_≡_) (merge f m₁ m₂) (merge f m₂ m₁) merge-comm : (m₁ m₂ : Map) lift (_≡_) (merge f m₁ m₂) (merge f m₂ m₁)
merge-comm m₁ m₂ = (merge-comm-subset m₁ m₂ , merge-comm-subset m₂ m₁) merge-comm m₁ m₂ = (merge-comm-subset m₁ m₂ , merge-comm-subset m₂ m₁)
where where
merge-comm-subset : (m₁ m₂ : Map) subset (_≡_) (merge f m₁ m₂) (merge f m₂ m₁) merge-comm-subset : (m₁ m₂ : Map) subset (_≡_) (merge f m₁ m₂) (merge f m₂ m₁)