summaryrefslogtreecommitdiff
path: root/theories/FSets/FMapInterface.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/FSets/FMapInterface.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/FSets/FMapInterface.v')
-rw-r--r--theories/FSets/FMapInterface.v233
1 files changed, 156 insertions, 77 deletions
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index dde74a0a..1e475887 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -6,42 +6,72 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapInterface.v 8671 2006-03-29 08:31:28Z letouzey $ *)
+(* $Id: FMapInterface.v 10616 2008-03-04 17:33:35Z letouzey $ *)
(** * Finite map library *)
-(** This file proposes an interface for finite maps *)
+(** This file proposes interfaces for finite maps *)
-(* begin hide *)
+Require Export Bool DecidableType OrderedType.
Set Implicit Arguments.
Unset Strict Implicit.
-Require Import FSetInterface.
-(* end hide *)
-
-(** When compared with Ocaml Map, this signature has been split in two:
- - The first part [S] contains the usual operators (add, find, ...)
- It only requires a ordered key type, the data type can be arbitrary.
- The only function that asks more is [equal], whose first argument should
- be an equality on data.
- - Then, [Sord] extends [S] with a complete comparison function. For
- that, the data type should have a decidable total ordering.
+
+(** When compared with Ocaml Map, this signature has been split in
+ several parts :
+
+ - The first parts [WSfun] and [WS] propose signatures for weak
+ maps, which are maps with no ordering on the key type nor the
+ data type. [WSfun] and [WS] are almost identical, apart from the
+ fact that [WSfun] is expressed in a functorial way whereas [WS]
+ is self-contained. For obtaining an instance of such signatures,
+ a decidable equality on keys in enough (see for example
+ [FMapWeakList]). These signatures contain the usual operators
+ (add, find, ...). The only function that asks for more is
+ [equal], whose first argument should be a comparison on data.
+
+ - Then comes [Sfun] and [S], that extend [WSfun] and [WS] to the
+ case where the key type is ordered. The main novelty is that
+ [elements] is required to produce sorted lists.
+
+ - Finally, [Sord] extends [S] with a complete comparison function. For
+ that, the data type should have a decidable total ordering as well.
+
+ If unsure, what you're looking for is probably [S]: apart from [Sord],
+ all other signatures are subsets of [S].
+
+ Some additional differences with Ocaml:
+
+ - no [iter] function, useless since Coq is purely functional
+ - [option] types are used instead of [Not_found] exceptions
+ - more functions are provided: [elements] and [cardinal] and [map2]
+
*)
-Module Type S.
+Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
- Declare Module E : OrderedType.
+(** ** Weak signature for maps
+
+ No requirements for an ordering on keys nor elements, only decidability
+ of equality on keys. First, a functorial signature: *)
+
+Module Type WSfun (E : EqualityType).
+
+ (** The module E of base objects is meant to be a [DecidableType]
+ (and used to be so). But requiring only an [EqualityType] here
+ allows subtyping between weak and ordered maps. *)
Definition key := E.t.
- Parameter t : Set -> Set. (** the abstract type of maps *)
+ Parameter t : Type -> Type.
+ (** the abstract type of maps *)
Section Types.
- Variable elt:Set.
+ Variable elt:Type.
Parameter empty : t elt.
- (** The empty map. *)
+ (** The empty map. *)
Parameter is_empty : t elt -> bool.
(** Test whether a map is empty or not. *)
@@ -53,8 +83,7 @@ Module Type S.
Parameter find : key -> t elt -> option elt.
(** [find x m] returns the current binding of [x] in [m],
- or raises [Not_found] if no such binding exists.
- NB: in Coq, the exception mechanism becomes a option type. *)
+ or [None] if no such binding exists. *)
Parameter remove : key -> t elt -> t elt.
(** [remove x m] returns a map containing the same bindings as [m],
@@ -64,45 +93,36 @@ Module Type S.
(** [mem x m] returns [true] if [m] contains a binding for [x],
and [false] otherwise. *)
- (** Coq comment: [iter] is useless in a purely functional world *)
- (** val iter : (key -> 'a -> unit) -> 'a t -> unit *)
- (** iter f m applies f to all bindings in map m. f receives the key as
- first argument, and the associated value as second argument.
- The bindings are passed to f in increasing order with respect to the
- ordering over the type of the keys. Only current bindings are
- presented to f: bindings hidden by more recent bindings are not
- passed to f. *)
-
- Variable elt' : Set.
- Variable elt'': Set.
+ Variable elt' elt'' : Type.
Parameter map : (elt -> elt') -> t elt -> t elt'.
(** [map f m] returns a map with same domain as [m], where the associated
value a of all bindings of [m] has been replaced by the result of the
- application of [f] to [a]. The bindings are passed to [f] in
- increasing order with respect to the ordering over the type of the
- keys. *)
+ application of [f] to [a]. Since Coq is purely functional, the order
+ in which the bindings are passed to [f] is irrelevant. *)
Parameter mapi : (key -> elt -> elt') -> t elt -> t elt'.
- (** Same as [S.map], but the function receives as arguments both the
+ (** Same as [map], but the function receives as arguments both the
key and the associated value for each binding of the map. *)
- Parameter map2 : (option elt -> option elt' -> option elt'') -> t elt -> t elt' -> t elt''.
- (** Not present in Ocaml.
- [map f m m'] creates a new map whose bindings belong to the ones of either
- [m] or [m']. The presence and value for a key [k] is determined by [f e e']
- where [e] and [e'] are the (optional) bindings of [k] in [m] and [m']. *)
+ Parameter map2 :
+ (option elt -> option elt' -> option elt'') -> t elt -> t elt' -> t elt''.
+ (** [map2 f m m'] creates a new map whose bindings belong to the ones
+ of either [m] or [m']. The presence and value for a key [k] is
+ determined by [f e e'] where [e] and [e'] are the (optional) bindings
+ of [k] in [m] and [m']. *)
Parameter elements : t elt -> list (key*elt).
- (** Not present in Ocaml.
- [elements m] returns an assoc list corresponding to the bindings of [m].
- Elements of this list are sorted with respect to their first components.
- Useful to specify [fold] ... *)
+ (** [elements m] returns an assoc list corresponding to the bindings
+ of [m], in any order. *)
- Parameter fold : forall A: Set, (key -> elt -> A -> A) -> t elt -> A -> A.
+ Parameter cardinal : t elt -> nat.
+ (** [cardinal m] returns the number of bindings in [m]. *)
+
+ Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A.
(** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)],
where [k1] ... [kN] are the keys of all bindings in [m]
- (in increasing order), and [d1] ... [dN] are the associated data. *)
+ (in any order), and [d1] ... [dN] are the associated data. *)
Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool.
(** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are equal,
@@ -127,8 +147,6 @@ Module Type S.
Definition eq_key_elt (p p':key*elt) :=
E.eq (fst p) (fst p') /\ (snd p) = (snd p').
- Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
-
(** Specification of [MapsTo] *)
Parameter MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m.
@@ -162,61 +180,123 @@ Module Type S.
MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
Parameter elements_2 :
InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
- Parameter elements_3 : sort lt_key (elements m).
+ (** When compared with ordered maps, here comes the only
+ property that is really weaker: *)
+ Parameter elements_3w : NoDupA eq_key (elements m).
+
+ (** Specification of [cardinal] *)
+ Parameter cardinal_1 : cardinal m = length (elements m).
(** Specification of [fold] *)
Parameter fold_1 :
- forall (A : Set) (i : A) (f : key -> elt -> A -> A),
+ forall (A : Type) (i : A) (f : key -> elt -> A -> A),
fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
+
+ (** Equality of maps *)
- Definition Equal cmp m m' :=
+ (** Caveat: there are at least three distinct equality predicates on maps.
+ - The simpliest (and maybe most natural) way is to consider keys up to
+ their equivalence [E.eq], but elements up to Leibniz equality, in
+ the spirit of [eq_key_elt] above. This leads to predicate [Equal].
+ - Unfortunately, this [Equal] predicate can't be used to describe
+ the [equal] function, since this function (for compatibility with
+ ocaml) expects a boolean comparison [cmp] that may identify more
+ elements than Leibniz. So logical specification of [equal] is done
+ via another predicate [Equivb]
+ - This predicate [Equivb] is quite ad-hoc with its boolean [cmp],
+ it can be generalized in a [Equiv] expecting a more general
+ (possibly non-decidable) equality predicate on elements *)
+
+ Definition Equal m m' := forall y, find y m = find y m'.
+ Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
(forall k, In k m <-> In k m') /\
- (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).
+ (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
+ Definition Equivb (cmp: elt->elt->bool) := Equiv (Cmp cmp).
- Variable cmp : elt -> elt -> bool.
+ (** Specification of [equal] *)
- (** Specification of [equal] *)
- Parameter equal_1 : Equal cmp m m' -> equal cmp m m' = true.
- Parameter equal_2 : equal cmp m m' = true -> Equal cmp m m'.
+ Variable cmp : elt -> elt -> bool.
- End Spec.
- End Types.
+ Parameter equal_1 : Equivb cmp m m' -> equal cmp m m' = true.
+ Parameter equal_2 : equal cmp m m' = true -> Equivb cmp m m'.
+
+ End Spec.
+ End Types.
(** Specification of [map] *)
- Parameter map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
+ Parameter map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
MapsTo x e m -> MapsTo x (f e) (map f m).
- Parameter map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'),
+ Parameter map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'),
In x (map f m) -> In x m.
(** Specification of [mapi] *)
- Parameter mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)
+ Parameter mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
(f:key->elt->elt'), MapsTo x e m ->
exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
- Parameter mapi_2 : forall (elt elt':Set)(m: t elt)(x:key)
+ Parameter mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
(f:key->elt->elt'), In x (mapi f m) -> In x m.
(** Specification of [map2] *)
- Parameter map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt')
+ Parameter map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
(x:key)(f:option elt->option elt'->option elt''),
In x m \/ In x m' ->
find x (map2 f m m') = f (find x m) (find x m').
- Parameter map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt')
+ Parameter map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
(x:key)(f:option elt->option elt'->option elt''),
In x (map2 f m m') -> In x m \/ In x m'.
- (* begin hide *)
- Hint Immediate MapsTo_1 mem_2 is_empty_2.
-
- Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 add_3 remove_1
- remove_2 remove_3 find_1 find_2 fold_1 map_1 map_2 mapi_1 mapi_2.
- (* end hide *)
+ Hint Immediate MapsTo_1 mem_2 is_empty_2
+ map_2 mapi_2 add_3 remove_3 find_2
+ : map.
+ Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
+ remove_2 find_1 fold_1 map_1 mapi_1 mapi_2
+ : map.
+End WSfun.
+
+
+(** ** Static signature for Weak Maps
+
+ Similar to [WSfun] but expressed in a self-contained way. *)
+
+Module Type WS.
+ Declare Module E : EqualityType.
+ Include Type WSfun E.
+End WS.
+
+
+
+(** ** Maps on ordered keys, functorial signature *)
+
+Module Type Sfun (E : OrderedType).
+ Include Type WSfun E.
+ Section elt.
+ Variable elt:Type.
+ Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
+ (* Additional specification of [elements] *)
+ Parameter elements_3 : forall m, sort lt_key (elements m).
+ (** Remark: since [fold] is specified via [elements], this stronger
+ specification of [elements] has an indirect impact on [fold],
+ which can now be proved to receive elements in increasing order. *)
+ End elt.
+End Sfun.
+
+
+
+(** ** Maps on ordered keys, self-contained signature *)
+
+Module Type S.
+ Declare Module E : OrderedType.
+ Include Type Sfun E.
End S.
+
+(** ** Maps with ordering both on keys and datas *)
+
Module Type Sord.
-
+
Declare Module Data : OrderedType.
Declare Module MapS : S.
Import MapS.
@@ -234,12 +314,11 @@ Module Type Sord.
Definition cmp e e' := match Data.compare e e' with EQ _ => true | _ => false end.
- Parameter eq_1 : forall m m', Equal cmp m m' -> eq m m'.
- Parameter eq_2 : forall m m', eq m m' -> Equal cmp m m'.
+ Parameter eq_1 : forall m m', Equivb cmp m m' -> eq m m'.
+ Parameter eq_2 : forall m m', eq m m' -> Equivb cmp m m'.
Parameter compare : forall m1 m2, Compare lt eq m1 m2.
- (** Total ordering between maps. The first argument (in Coq: Data.compare)
- is a total ordering used to compare data associated with equal keys
- in the two maps. *)
+ (** Total ordering between maps. [Data.compare] is a total ordering
+ used to compare data associated with equal keys in the two maps. *)
-End Sord. \ No newline at end of file
+End Sord.