Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

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.