From eaee73236fa27fde9187f65b9c8bc96e23d468dc Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 30 Jul 2023 13:46:52 -0700 Subject: [PATCH] More tweaks to naming and style Signed-off-by: Danila Fedorin --- Map.agda | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/Map.agda b/Map.agda index af0e3cd..a13707b 100644 --- a/Map.agda +++ b/Map.agda @@ -23,7 +23,7 @@ keys = map proj₁ data Unique {c} {C : Set c} : List C → Set c where empty : Unique [] - push : forall {x : C} {xs : List C} + push : ∀ {x : C} {xs : List C} → All (λ x' → ¬ x ≡ x') xs → Unique xs → Unique (x ∷ xs) @@ -169,18 +169,18 @@ private module ImplInsert (f : B → B → B) where let (v , k,v∈l) = locate k∈kl 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 - insert-preserves-∉ {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k' - insert-preserves-∉ {l = []} k≢k' k∉kl (there ()) - insert-preserves-∉ {k} {k'} {v'} {(k'' , v'') ∷ xs} k≢k' k∉kl k∈kil + insert-preserves-∉k {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k' + insert-preserves-∉k {l = []} k≢k' k∉kl (there ()) + insert-preserves-∉k {k} {k'} {v'} {(k'' , v'') ∷ xs} k≢k' k∉kl k∈kil with ≡-dec-A k k'' ... | yes k≡k'' = k∉kl (here k≡k'') ... | no k≢k'' with ≡-dec-A k' k'' | k∈kil ... | yes k'≡k'' | here k≡k'' = k≢k'' k≡k'' ... | 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'' | 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 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₂ with ≡-dec-A 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₂ - merge-preserves-keys₁ {l₁ = []} _ k,v∈l₂ = k,v∈l₂ - merge-preserves-keys₁ {l₁ = (k' , v') ∷ xs₁} k∉kl₁ k,v∈l₂ = - let recursion = merge-preserves-keys₁ (λ k∈xs₁ → k∉kl₁ (there k∈xs₁)) k,v∈l₂ + merge-preserves-∈₁ {l₁ = []} _ k,v∈l₂ = k,v∈l₂ + merge-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} k∉kl₁ 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 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')) ... | 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₂ - 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 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' with ≡-dec-A k k' ... | yes k≡k' rewrite k≡k' = absurd (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁)) ... | 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' = 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)) ... | 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₂) → (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₂ 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₂ = insert-preserves-∈ k≢k' (merge-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂) where @@ -295,12 +295,12 @@ module _ (f : B → B → B) where let (v₁ , k,v₁∈l₁) = locate k∈kl₁ 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₂ = let (v₂ , k,v₂∈l₂) = locate k∈kl₂ 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₂) module _ (_≈_ : B → B → Set b) where @@ -314,7 +314,7 @@ module _ (_≈_ : B → B → Set b) where module _ (f : B → 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₁) where merge-comm-subset : ∀ (m₁ m₂ : Map) → subset (_≡_) (merge f m₁ m₂) (merge f m₂ m₁)