diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-17 15:31:54 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-17 15:31:54 +0000 |
commit | 211030a7a870bdf3bc36b0923379e2d1bf6c729a (patch) | |
tree | 9953a1d775fe3161d43ca32e7073d10ae10349e1 /theories/FSets/FSetFacts.v | |
parent | 275151328893782671c1c6949c93b65f6d65fefa (diff) |
FSet/OrderedType now includes an eq_dec, and hence become an extension of DecidableType
After lots of hesitations, OrderedType now requires this "eq_dec" field, which
is redundant (can be deduced from "compare"), but allows the subtyping relation
DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly
extensions of weak sets. Of course this change introduces a last-minute
incompatibility, but:
- There is a clear gain in term of functionnality / simplicity.
- FSets 8.2 already needs some adaptations when compared with 8.1, so it's
the right time to push such incompatible changes.
- Transition shouldn't be too hard: the old OrderedType still exists under
the name MiniOrderedType, and functor MOT_to_OT allows to convert from
one to the other.
Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType
(resp. OrderedType), an eq_dec on sets is now required in these interfaces
and in the implementations. In pratice, it is really easy to build from
equal and equal_1 and equal_2.
Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun,
while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M).
Idem with WDecide, WProperties and WEqProperties.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11693 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FSetFacts.v')
-rw-r--r-- | theories/FSets/FSetFacts.v | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 6afb8fcb7..8c692bd07 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -21,11 +21,9 @@ Require Export FSetInterface. Set Implicit Arguments. Unset Strict Implicit. -(** First, a functor for Weak Sets. Since the signature [WS] includes - an EqualityType and not a stronger DecidableType, this functor - should take two arguments in order to compensate this. *) +(** First, a functor for Weak Sets in functorial version. *) -Module WFacts (Import E : DecidableType)(Import M : WSfun E). +Module WFacts_fun (Import E : DecidableType)(Import M : WSfun E). Notation eq_dec := E.eq_dec. Definition eqb x y := if eq_dec x y then true else false. @@ -491,15 +489,14 @@ Qed. Add Morphism cardinal ; cardinal_m. *) -End WFacts. +End WFacts_fun. +(** Now comes variants for self-contained weak sets and for full sets. + For these variants, only one argument is necessary. Thanks to + the subtyping [WS<=S], the [Facts] functor which is meant to be + used on modules [(M:S)] can simply be an alias of [WFacts]. *) -(** Now comes a special version dedicated to full sets. For this - one, only one argument [(M:S)] is necessary. *) +Module WFacts (M:WS) := WFacts_fun M.E M. +Module Facts := WFacts. -Module Facts (Import M:S). - Module D:=OT_as_DT M.E. - Include WFacts D M. - -End Facts. |