Minor cleanup of Map module
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
850984ec15
commit
c9ab1152c4
18
Map.agda
18
Map.agda
|
@ -29,9 +29,6 @@ data Unique {c} {C : Set c} : List C → Set c where
|
||||||
→ Unique xs
|
→ Unique xs
|
||||||
→ Unique (x ∷ xs)
|
→ Unique (x ∷ xs)
|
||||||
|
|
||||||
Map : Set (a ⊔ b)
|
|
||||||
Map = Σ (List (A × B)) (λ l → Unique (keys l))
|
|
||||||
|
|
||||||
Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} → ¬ MemProp._∈_ x xs → Unique xs → Unique (xs ++ (x ∷ []))
|
Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} → ¬ MemProp._∈_ x xs → Unique xs → Unique (xs ++ (x ∷ []))
|
||||||
Unique-append {c} {C} {x} {[]} _ _ = push [] empty
|
Unique-append {c} {C} {x} {[]} _ _ = push [] empty
|
||||||
Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') = push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs')
|
Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') = push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs')
|
||||||
|
@ -43,24 +40,27 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') = push (help x'
|
||||||
help {[]} _ = x'≢x ∷ []
|
help {[]} _ = x'≢x ∷ []
|
||||||
help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
|
help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
|
||||||
|
|
||||||
_∈_ : (A × B) → List (A × B) → Set (a ⊔ b)
|
Map : Set (a ⊔ b)
|
||||||
_∈_ p m = MemProp._∈_ p m
|
Map = Σ (List (A × B)) (λ l → Unique (keys l))
|
||||||
|
|
||||||
foldr : ∀ {c} {C : Set c} → (A → B → C → C) -> C -> List (A × B) -> C
|
_∈_ : (A × B) → Map → Set (a ⊔ b)
|
||||||
foldr f b [] = b
|
_∈_ p (kvs , _) = MemProp._∈_ p kvs
|
||||||
foldr f b ((k , v) ∷ xs) = f k v (foldr f b xs)
|
|
||||||
|
|
||||||
absurd : ∀ {a} {A : Set a} → ⊥ → A
|
absurd : ∀ {a} {A : Set a} → ⊥ → A
|
||||||
absurd ()
|
absurd ()
|
||||||
|
|
||||||
private module ImplRelation (_≈_ : B → B → Set b) where
|
private module ImplRelation (_≈_ : B → B → Set b) where
|
||||||
subset : List (A × B) → List (A × B) → Set (a ⊔ b)
|
subset : List (A × B) → List (A × B) → Set (a ⊔ b)
|
||||||
subset m₁ m₂ = ∀ (k : A) (v : B) → (k , v) ∈ m₁ → Σ B (λ v' → v ≈ v' × ((k , v') ∈ m₂))
|
subset m₁ m₂ = ∀ (k : A) (v : B) → MemProp._∈_ (k , v) m₁ → Σ B (λ v' → v ≈ v' × (MemProp._∈_ (k , v') m₂))
|
||||||
|
|
||||||
private module ImplInsert (f : B → B → B) where
|
private module ImplInsert (f : B → B → B) where
|
||||||
_∈k_ : A → List (A × B) → Set a
|
_∈k_ : A → List (A × B) → Set a
|
||||||
_∈k_ k m = MemProp._∈_ k (keys m)
|
_∈k_ k m = MemProp._∈_ k (keys m)
|
||||||
|
|
||||||
|
foldr : ∀ {c} {C : Set c} → (A → B → C → C) -> C -> List (A × B) -> C
|
||||||
|
foldr f b [] = b
|
||||||
|
foldr f b ((k , v) ∷ xs) = f k v (foldr f b xs)
|
||||||
|
|
||||||
insert : A → B → List (A × B) → List (A × B)
|
insert : A → B → List (A × B) → List (A × B)
|
||||||
insert k v [] = (k , v) ∷ []
|
insert k v [] = (k , v) ∷ []
|
||||||
insert k v (x@(k' , v') ∷ xs) with ≡-dec-A k k'
|
insert k v (x@(k' , v') ∷ xs) with ≡-dec-A k k'
|
||||||
|
|
Loading…
Reference in New Issue
Block a user