diff options
Diffstat (limited to 'theories/FSets/FMapInterface.v')
| -rw-r--r-- | theories/FSets/FMapInterface.v | 233 |
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. |