From a9e7f3c88b0dddec15a709d0a8b4e4a143913aea Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 4 Sep 2012 11:06:21 +0200
Subject: [PATCH] Make the types of the finite map operational type classes
explicit, and make some more specific.
---
theories/base.v | 51 +++++++++++++++++++++++----------------------
theories/fin_maps.v | 14 ++++++-------
theories/nmap.v | 2 +-
theories/pmap.v | 2 +-
4 files changed, 35 insertions(+), 34 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index 4a19399..7ce783d 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -161,10 +161,11 @@ Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope.
Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : C_scope.
(** ** Operations on maps *)
-(** In this file we will only define operational type classes for the
-operations on maps. In the file [fin_maps] we will axiomatize finite maps.
+(** In this section we define operational type classes for the operations
+on maps. In the file [fin_maps] we will axiomatize finite maps.
The function lookup [m !! k] should yield the element at key [k] in [m]. *)
-Class Lookup K M := lookup: ∀ {A}, K → M A → option A.
+Class Lookup (K : Type) (M : Type → Type) :=
+ lookup: ∀ {A}, K → M A → option A.
Instance: Params (@lookup) 4.
Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
@@ -174,43 +175,43 @@ Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
(** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *)
-Class Insert K M :=
+Class Insert (K : Type) (M : Type → Type) :=
insert: ∀ {A}, K → A → M A → M A.
Instance: Params (@insert) 4.
Notation "<[ k := a ]>" := (insert k a)
(at level 5, right associativity, format "<[ k := a ]>") : C_scope.
-(** The function delete [delete k m] should deletes the value at key [k] in
-[m]. *)
-Class Delete K M :=
- delete: K → M → M.
-Instance: Params (@delete) 3.
+(** The function delete [delete k m] should delete the value at key [k] in
+[m]. If the key [k] is not a member of [m], the original map should be
+returned. *)
+Class Delete (K : Type) (M : Type → Type) :=
+ delete: ∀ {A}, K → M A → M A.
+Instance: Params (@delete) 4.
(** The function [alter f k m] should update the value at key [k] using the
-function [f], which is called with the original value at key [k]. When [k] is
-not a member of [m], the original map should be returned. *)
-Class Alter K M :=
+function [f], which is called with the original value. *)
+Class Alter (K : Type) (M : Type → Type) :=
alter: ∀ {A}, (A → A) → K → M A → M A.
Instance: Params (@alter) 4.
(** The function [alter f k m] should update the value at key [k] using the
-function [f], which is called with the original value at key [k] or [None] if
-[k] is not a member of [m]. The value at [k] should be deleted if [f] yields
-[None]. *)
-Class PartialAlter K M :=
+function [f], which is called with the original value at key [k] or [None]
+if [k] is not a member of [m]. The value at [k] should be deleted if [f]
+yields [None]. *)
+Class PartialAlter (K : Type) (M : Type → Type) :=
partial_alter: ∀ {A}, (option A → option A) → K → M A → M A.
Instance: Params (@partial_alter) 4.
(** The function [dom C m] should yield the domain of [m]. That is a finite
collection of type [C] that contains the keys that are a member of [m]. *)
-Class Dom K M :=
- dom: ∀ C `{Empty C} `{Union C} `{Singleton K C}, M → C.
-Instance: Params (@dom) 7.
+Class Dom (K : Type) (M : Type → Type) :=
+ dom: ∀ {A} C `{Empty C} `{Union C} `{Singleton K C}, M A → C.
+Instance: Params (@dom) 8.
(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)]
provided that [k] is a member of either [m1] or [m2].*)
-Class Merge M :=
+Class Merge (M : Type → Type) :=
merge: ∀ {A}, (option A → option A → option A) → M A → M A → M A.
Instance: Params (@merge) 3.
@@ -218,22 +219,22 @@ Instance: Params (@merge) 3.
Definition insert_list `{Insert K M} {A} (l : list (K * A)) (m : M A) : M A :=
fold_right (λ p, <[ fst p := snd p ]>) m l.
Instance: Params (@insert_list) 4.
-Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
+Definition delete_list `{Delete K M} {A} (l : list K) (m : M A) : M A :=
fold_right delete m l.
-Instance: Params (@delete_list) 3.
+Instance: Params (@delete_list) 4.
(** The function [union_with f m1 m2] should yield the union of [m1] and [m2]
using the function [f] to combine values of members that are in both [m1] and
[m2]. *)
-Class UnionWith M :=
+Class UnionWith (M : Type → Type) :=
union_with: ∀ {A}, (A → A → A) → M A → M A → M A.
Instance: Params (@union_with) 3.
(** Similarly for the intersection and difference. *)
-Class IntersectionWith M :=
+Class IntersectionWith (M : Type → Type) :=
intersection_with: ∀ {A}, (A → A → A) → M A → M A → M A.
Instance: Params (@intersection_with) 3.
-Class DifferenceWith M :=
+Class DifferenceWith (M : Type → Type) :=
difference_with: ∀ {A}, (A → A → option A) → M A → M A → M A.
Instance: Params (@difference_with) 3.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index f023e46..d2d0113 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -8,11 +8,11 @@ Require Export prelude.
(** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of
-course limits the class of finite map implementations, but since we are mainly
-interested in finite maps with numbers or paths as indexes, we do not consider
-this a serious limitation. The main application of finite maps is to implement
-the memory, where extensionality of Leibniz equality becomes very important for
-a convenient use in assertions of our axiomatic semantics. *)
+course limits the space of finite map implementations, but since we are mainly
+interested in finite maps with numbers as indexes, we do not consider this to
+be a serious limitation. The main application of finite maps is to implement
+the memory, where extensionality of Leibniz equality is very important for a
+convenient use in the assertions of our axiomatic semantics. *)
(** Finiteness is axiomatized by requiring each map to have a finite domain.
Since we may have multiple implementations of finite sets, the [dom] function is
parametrized by an implementation of finite sets over the map's key type. *)
@@ -20,7 +20,7 @@ parametrized by an implementation of finite sets over the map's key type. *)
which enables us to give a generic implementation of [union_with],
[intersection_with], and [difference_with]. *)
Class FinMap K M `{∀ A, Empty (M A)} `{Lookup K M} `{FMap M}
- `{PartialAlter K M} `{∀ A, Dom K (M A)} `{Merge M} := {
+ `{PartialAlter K M} `{Dom K M} `{Merge M} := {
finmap_eq {A} (m1 m2 : M A) :
(∀ i, m1 !! i = m2 !! i) → m1 = m2;
lookup_empty {A} i :
@@ -46,7 +46,7 @@ Instance finmap_alter `{PartialAlter K M} : Alter K M := λ A f,
partial_alter (fmap f).
Instance finmap_insert `{PartialAlter K M} : Insert K M := λ A k x,
partial_alter (λ _, Some x) k.
-Instance finmap_delete `{PartialAlter K M} {A} : Delete K (M A) :=
+Instance finmap_delete `{PartialAlter K M} : Delete K M := λ A,
partial_alter (λ _, None).
Instance finmap_singleton `{PartialAlter K M} {A}
`{Empty (M A)} : Singleton (K * A) (M A) := λ p, <[fst p:=snd p]>∅.
diff --git a/theories/nmap.v b/theories/nmap.v
index 8e6fe72..1ee586e 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -27,7 +27,7 @@ Global Instance Npartial_alter: PartialAlter N Nmap := λ A f i t,
| N0, Build_Nmap o t => Build_Nmap (f o) t
| Npos p, Build_Nmap o t => Build_Nmap o (partial_alter f p t)
end.
-Global Instance Ndom {A} : Dom N (Nmap A) := λ A _ _ _ t,
+Global Instance Ndom: Dom N Nmap := λ C _ _ _ _ t,
match t with
| Build_Nmap o t => option_case (λ _, {[ 0 ]}) ∅ o ∪ (Pdom_raw Npos (`t))
end.
diff --git a/theories/pmap.v b/theories/pmap.v
index d760798..b8a35bb 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -281,7 +281,7 @@ Section dom.
Qed.
End dom.
-Global Instance Pdom {A} : Dom positive (Pmap A) := λ C _ _ _ t,
+Global Instance Pdom : Dom positive Pmap := λ C _ _ _ _ t,
Pdom_raw id (`t).
Fixpoint Pmerge_aux `(f : option A → option B) (t : Pmap_raw A) : Pmap_raw B :=
--
GitLab