New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))

 "Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for
 "Module M (...). Include M1. Include M2. Include M3... End M."

 Moreover M2,M3,etc can be functors as long as they find what they need in what
 comes before them (see new command "Include Self").
 The only real constraint is that M1,M2,M3,... should not have common elements
 (for the moment (?)).

 Same behavior for signature : Module Type M := M1 <+ M2 <+ M3.

 Note that this <+ is _not_ a primitive construct of the module language,
 for instance it cannot be used in signature (Module M <: M1 <+ M2 is
 illegal for the moment).

 Some example of use in Decidable2 and NZAxioms

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 75 insertions, 136 deletions

diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 7cae4358b..111f45ca7 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -22,135 +22,98 @@ End BareEquality.
 
 (** * Specification of the equality by the Type Classe [Equivalence] *)
 
-Module Type Equality_fun (Import E:BareEquality).
+Module Type IsEq (Import E:BareEquality).
   Instance eq_equiv : Equivalence eq.
   Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv).
   Hint Resolve (@Equivalence_Transitive _ _ eq_equiv).
   Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv).
-End Equality_fun.
+End IsEq.
 
 (** * Earlier specification of equality by three separate lemmas. *)
 
-Module Type EqualityOrig_fun(Import E:BareEquality).
+Module Type IsEqOrig (Import E:BareEquality).
   Axiom eq_refl : forall x : t, eq x x.
   Axiom eq_sym : forall x y : t, eq x y -> eq y x.
   Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
   Hint Immediate eq_sym.
   Hint Resolve eq_refl eq_trans.
-End EqualityOrig_fun.
+End IsEqOrig.
 
 (** * Types with decidable equality *)
 
-Module Type Decidable_fun (Import E:BareEquality).
+Module Type HasEqDec (Import E:BareEquality).
   Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
-End Decidable_fun.
+End HasEqDec.
 
 (** * Boolean Equality *)
 
 (** Having [eq_dec] is the same as having a boolean equality plus
     a correctness proof. *)
 
-Module Type BoolEq_fun (Import E:BareEquality).
+Module Type HasEqBool (Import E:BareEquality).
   Parameter Inline eqb : t -> t -> bool.
   Parameter eqb_eq : forall x y, eqb x y = true <-> eq x y.
-End BoolEq_fun.
+End HasEqBool.
 
 (** From these basic blocks, we can build many combinations
     of static standalone module types. *)
 
-Module Type EqualityType.
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-End EqualityType.
-
-Module Type EqualityTypeOrig.
-  Include Type BareEquality.
-  Include Self Type EqualityOrig_fun.
-End EqualityTypeOrig.
-
-Module Type EqualityTypeBoth. (* <: EqualityType <: EqualityTypeOrig *)
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-  Include Self Type EqualityOrig_fun.
-End EqualityTypeBoth.
-
-Module Type DecidableType. (* <: EqualityType *)
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-  Include Self Type Decidable_fun.
-End DecidableType.
-
-Module Type DecidableTypeOrig. (* <: EqualityTypeOrig *)
-  Include Type BareEquality.
-  Include Self Type EqualityOrig_fun.
-  Include Self Type Decidable_fun.
-End DecidableTypeOrig.
-
-Module Type DecidableTypeBoth. (* <: DecidableType <: DecidableTypeOrig *)
-  Include Type EqualityTypeBoth.
-  Include Self Type Decidable_fun.
-End DecidableTypeBoth.
-
-Module Type BooleanEqualityType. (* <: EqualityType *)
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-  Include Self Type BoolEq_fun.
-End BooleanEqualityType.
-
-Module Type BooleanDecidableType. (* <: DecidableType <: BooleanEqualityType *)
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-  Include Self Type Decidable_fun.
-  Include Self Type BoolEq_fun.
-End BooleanDecidableType.
-
-Module Type DecidableTypeFull. (* <: all previous interfaces *)
-  Include Type BareEquality.
-  Include Self Type Equality_fun.
-  Include Self Type EqualityOrig_fun.
-  Include Self Type Decidable_fun.
-  Include Self Type BoolEq_fun.
-End DecidableTypeFull.
+Module Type EqualityType := BareEquality <+ IsEq.
+
+Module Type EqualityTypeOrig := BareEquality <+ IsEqOrig.
+
+Module Type EqualityTypeBoth (* <: EqualityType <: EqualityTypeOrig *)
+ := BareEquality <+ IsEq <+ IsEqOrig.
+
+Module Type DecidableType (* <: EqualityType *)
+ := BareEquality <+ IsEq <+ HasEqDec.
+
+Module Type DecidableTypeOrig (* <: EqualityTypeOrig *)
+ := BareEquality <+ IsEqOrig <+ HasEqDec.
+
+Module Type DecidableTypeBoth (* <: DecidableType <: DecidableTypeOrig *)
+ := EqualityTypeBoth <+ HasEqDec.
+
+Module Type BooleanEqualityType (* <: EqualityType *)
+ := BareEquality <+ IsEq <+ HasEqBool.
+
+Module Type BooleanDecidableType (* <: DecidableType <: BooleanEqualityType *)
+ := BareEquality <+ IsEq <+ HasEqDec <+ HasEqBool.
+
+Module Type DecidableTypeFull (* <: all previous interfaces *)
+ := BareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
 
 
 (** * Compatibility wrapper from/to the old version of
       [EqualityType] and [DecidableType] *)
 
-Module Backport_ET_fun (E:BareEquality)(F:Equality_fun E) <: EqualityOrig_fun E.
+Module BackportEq (E:BareEquality)(F:IsEq E) <: IsEqOrig E.
  Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
  Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
  Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
-End Backport_ET_fun.
+End BackportEq.
 
-Module Update_ET_fun (E:BareEquality)(F:EqualityOrig_fun E) <: Equality_fun E.
+Module UpdateEq (E:BareEquality)(F:IsEqOrig E) <: IsEq E.
  Instance eq_equiv : Equivalence E.eq.
  Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed.
-End Update_ET_fun.
+End UpdateEq.
 
-Module Backport_ET (E:EqualityType) <: EqualityTypeBoth.
- Include E.
- Include Backport_ET_fun E E.
-End Backport_ET.
+Module Backport_ET (E:EqualityType) <: EqualityTypeBoth
+ := E <+ BackportEq E E.
 
-Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth.
- Include E.
- Include Update_ET_fun E E.
-End Update_ET.
+Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth
+ := E <+ UpdateEq E E.
 
-Module Backport_DT (E:DecidableType) <: DecidableTypeBoth.
- Include E.
- Include Backport_ET_fun E E.
-End Backport_DT.
+Module Backport_DT (E:DecidableType) <: DecidableTypeBoth
+ := E <+ BackportEq E E.
 
-Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth.
- Include E.
- Include Update_ET_fun E E.
-End Update_DT.
+Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth
+ := E <+ UpdateEq E E.
 
 
 (** * Having [eq_dec] is equivalent to having [eqb] and its spec. *)
 
-Module Dec2Bool_fun (E:BareEquality)(F:Decidable_fun E) <: BoolEq_fun E.
+Module HasEqDec2Bool (E:BareEquality)(F:HasEqDec E) <: HasEqBool E.
  Definition eqb x y := if F.eq_dec x y then true else false.
  Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y.
  Proof.
@@ -158,9 +121,9 @@ Module Dec2Bool_fun (E:BareEquality)(F:Decidable_fun E) <: BoolEq_fun E.
   auto with *.
   split. discriminate. intro EQ; elim NEQ; auto.
  Qed.
-End Dec2Bool_fun.
+End HasEqDec2Bool.
 
-Module Bool2Dec_fun (E:BareEquality)(F:BoolEq_fun E) <: Decidable_fun E.
+Module HasEqBool2Dec (E:BareEquality)(F:HasEqBool E) <: HasEqDec E.
  Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}.
  Proof.
   intros x y. assert (H:=F.eqb_eq x y).
@@ -168,17 +131,13 @@ Module Bool2Dec_fun (E:BareEquality)(F:BoolEq_fun E) <: Decidable_fun E.
   apply -> H; auto.
   intro EQ. apply H in EQ. discriminate.
  Defined.
-End Bool2Dec_fun.
+End HasEqBool2Dec.
 
-Module Dec2Bool (E:DecidableType) <: BooleanDecidableType.
- Include E.
- Include Dec2Bool_fun E E.
-End Dec2Bool.
+Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
+ := E <+ HasEqDec2Bool E E.
 
-Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType.
- Include E.
- Include Bool2Dec_fun E E.
-End Bool2Dec.
+Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
+ := E <+ HasEqBool2Dec E E.
 
 
 
@@ -192,46 +151,30 @@ Module Type UsualBareEquality. (* <: BareEquality *)
  Definition eq := @eq t.
 End UsualBareEquality.
 
-Module UsualEquality_fun (E:UsualBareEquality) <: Equality_fun E.
+Module UsualIsEq (E:UsualBareEquality) <: IsEq E.
  Program Instance eq_equiv : Equivalence E.eq.
-End UsualEquality_fun.
+End UsualIsEq.
 
-Module UsualEqualityOrig_fun (E:UsualBareEquality) <: EqualityOrig_fun E.
+Module UsualIsEqOrig (E:UsualBareEquality) <: IsEqOrig E.
  Definition eq_refl := @eq_refl E.t.
  Definition eq_sym := @eq_sym E.t.
  Definition eq_trans := @eq_trans E.t.
-End UsualEqualityOrig_fun.
-
-Module Type UsualEqualityType. (* <: EqualityType *)
- Include Type UsualBareEquality.
- Include Self Type Equality_fun.
-End UsualEqualityType.
-
-Module Type UsualDecidableType. (* <: DecidableType *)
- Include Type UsualBareEquality.
- Include Self Type Equality_fun.
- Include Self Type Decidable_fun.
-End UsualDecidableType.
-
-Module Type UsualDecidableTypeBoth. (* <: DecidableTypeBoth *)
- Include Type UsualBareEquality.
- Include Self Type Equality_fun.
- Include Self Type EqualityOrig_fun.
- Include Self Type Decidable_fun.
-End UsualDecidableTypeBoth.
-
-Module Type UsualBoolEq.
- Include Type UsualBareEquality.
- Include Self Type BoolEq_fun.
-End UsualBoolEq.
-
-Module Type UsualDecidableTypeFull. (* <: DecidableTypeFull *)
- Include Type UsualBareEquality.
- Include Self Type Equality_fun.
- Include Self Type EqualityOrig_fun.
- Include Self Type Decidable_fun.
- Include Self Type BoolEq_fun.
-End UsualDecidableTypeFull.
+End UsualIsEqOrig.
+
+Module Type UsualEqualityType (* <: EqualityType *)
+ := UsualBareEquality <+ IsEq.
+
+Module Type UsualDecidableType (* <: DecidableType *)
+ := UsualBareEquality <+ IsEq <+ HasEqDec.
+
+Module Type UsualDecidableTypeBoth (* <: DecidableTypeBoth *)
+ := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec.
+
+Module Type UsualBoolEq := UsualBareEquality <+ HasEqBool.
+
+Module Type UsualDecidableTypeFull (* <: DecidableTypeFull *)
+ := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
+
 
 (** a [UsualDecidableType] is in particular an [DecidableType]. *)
 
@@ -247,14 +190,10 @@ End MiniDecidableType.
 Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth.
  Include M.
  Definition eq := @eq M.t.
- Include Self UsualEquality_fun.
- Include Self UsualEqualityOrig_fun.
+ Include Self UsualIsEq.
+ Include Self UsualIsEqOrig.
 End Make_UDT.
 
-Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull.
- Include M. (* t, eq, eqb, eqb_eq *)
- Include UsualEquality_fun M.
- Include UsualEqualityOrig_fun M.
- Include Bool2Dec_fun M M.
-End Make_UDTF.
+Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull
+ := M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec.