Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles des sortes (InProp, InSet, InType)

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

7 files changed, 37 insertions, 34 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 549496d918..28f26a3afc 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -40,18 +40,6 @@ type local_entry =
 
 (* Inductive entries *)
 
-type elimination_sorts = ElimOnProp | ElimOnSet | ElimOnType
-
-let sort_of_elimination = function 
-  | ElimOnProp -> prop
-  | ElimOnSet -> spec
-  | ElimOnType -> Type (Univ.new_univ ())
-
-let elimination_of_sort = function
-  | Prop Null -> ElimOnProp
-  | Prop Pos -> ElimOnSet
-  | Type _ -> ElimOnType
-
 type recarg = 
   | Param of int 
   | Norec 
@@ -68,7 +56,7 @@ type one_inductive_body = {
   mind_user_arity : types option;
   mind_sort : sorts;
   mind_nrealargs : int;
-  mind_kelim : elimination_sorts list;
+  mind_kelim : sorts_family list;
   mind_listrec : (recarg list) array;
   mind_finite : bool;
   mind_nparams : int;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index e9d83506ec..ff002230ff 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -44,11 +44,6 @@ type local_entry =
 
 (*s Inductive types (internal representation). *)
 
-type elimination_sorts = ElimOnProp | ElimOnSet | ElimOnType
-
-val elimination_of_sort : sorts -> elimination_sorts
-val sort_of_elimination : elimination_sorts -> sorts
-
 type recarg = 
   | Param of int 
   | Norec 
@@ -70,7 +65,7 @@ type one_inductive_body = {
   mind_user_arity : types option;
   mind_sort : sorts;
   mind_nrealargs : int;
-  mind_kelim : elimination_sorts list;
+  mind_kelim : sorts_family list;
   mind_listrec : (recarg list) array;
   mind_finite : bool;
   mind_nparams : int;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 662692ecaa..c28055ae6b 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -101,12 +101,12 @@ let mind_check_wellformed env mie =
 
 let allowed_sorts issmall isunit = function
   | Type _ -> 
-      [ElimOnProp;ElimOnSet;ElimOnType]
+      [InProp;InSet;InType]
   | Prop Pos -> 
-      if issmall then [ElimOnProp;ElimOnSet;ElimOnType]
-      else [ElimOnProp;ElimOnSet]
+      if issmall then [InProp;InSet;InType]
+      else [InProp;InSet]
   | Prop Null -> 
-      if isunit then [ElimOnProp;ElimOnSet] else [ElimOnProp]
+      if isunit then [InProp;InSet] else [InProp]
 
 type ill_formed_ind =
   | LocalNonPos of int
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index e42df6d9c5..c8f49ed611 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -41,7 +41,7 @@ val mis_ntypes : inductive_instance -> int
 val mis_nconstr : inductive_instance -> int
 val mis_nparams : inductive_instance -> int
 val mis_nrealargs : inductive_instance -> int
-val mis_kelim : inductive_instance -> elimination_sorts list
+val mis_kelim : inductive_instance -> sorts_family list
 val mis_recargs : inductive_instance -> (recarg list) array array
 val mis_recarg : inductive_instance -> (recarg list) array
 val mis_typename : inductive_instance -> identifier
diff --git a/kernel/term.ml b/kernel/term.ml
index 1637fcafba..8b276c0683 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -45,6 +45,18 @@ let print_sort = function
 (*  | Type _ -> [< 'sTR "Type" >] *)
   | Type u -> [< 'sTR "Type("; pr_uni u; 'sTR ")" >]
 
+type sorts_family = InProp | InSet | InType
+
+let new_sort_in_family = function 
+  | InProp -> mk_Prop
+  | InSet -> mk_Set
+  | InType -> Type (Univ.new_univ ())
+
+let family_of_sort = function
+  | Prop Null -> InProp
+  | Prop Pos -> InSet
+  | Type _ -> InType
+
 (********************************************************************)
 (* type of global reference *)
 
@@ -1057,8 +1069,8 @@ let mkProp   = mkSort mk_Prop
 let mkSet    = mkSort mk_Set
 let mkType u = mkSort (Type u)
 
-let prop = Prop Null
-and spec = Prop Pos
+let prop = mk_Prop
+and spec = mk_Set
 and types = Type implicit_univ (* For eliminations *)
 and type_0 = Type prop_univ
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 76daa96f0a..ca0bae8385 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -27,6 +27,14 @@ val mk_Prop : sorts
 
 val print_sort : sorts -> std_ppcmds
 
+(*s The sorts family of CCI. *)
+
+type sorts_family = InProp | InSet | InType
+
+val family_of_sort : sorts -> sorts_family
+val new_sort_in_family : sorts_family -> sorts
+
+(*s Useful types *)
 
 type existential_key = int
 
@@ -38,7 +46,7 @@ type case_printing =
 (* the integer is the number of real args, needed for reduction *)
 type case_info = int * case_printing
 
-(* Concrete type for making pattern-matching. *)
+(*s Concrete type for making pattern-matching. *)
 module Polymorph :
 sig
 (* [constr array] is an instance matching definitional [named_context] in
@@ -58,7 +66,7 @@ type ('constr, 'types) cofixpoint =
    de Bruijn indices. *)
 end 
 
-(********************************************************************)
+(*s*******************************************************************)
 (* type of global reference *)
 
 type global_reference =
@@ -67,7 +75,7 @@ type global_reference =
   | IndRef of inductive_path
   | ConstructRef of constructor_path
 
-(********************************************************************)
+(*s*******************************************************************)
 (* The type of constructions *)
 
 type constr
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 317cc199d6..3e8de823a6 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -302,7 +302,7 @@ let is_correct_arity env sigma kelim (c,pj) indf t =
       | IsProd (_,a1,a2), _ -> 
           let k = whd_betadeltaiota env sigma a2 in 
           let ksort = match kind_of_term k with
-	    | IsSort s -> elimination_of_sort s 
+	    | IsSort s -> family_of_sort s 
 	    | _ -> raise (Arity None) in
 	  let ind = build_dependent_inductive indf in
           let univ =
@@ -316,7 +316,7 @@ let is_correct_arity env sigma kelim (c,pj) indf t =
 	  raise (Arity None)
       | k, ki -> 
 	  let ksort = match k with
-	    | IsSort s -> elimination_of_sort s
+	    | IsSort s -> family_of_sort s
             | _ ->  raise (Arity None) in
           if List.exists ((=) ksort) kelim then 
 	    (false, pt'), u
@@ -326,9 +326,9 @@ let is_correct_arity env sigma kelim (c,pj) indf t =
   try srec (pj.uj_type,t) Constraint.empty
   with Arity kinds ->
     let create_sort = function 
-      | ElimOnProp -> prop
-      | ElimOnSet -> spec
-      | ElimOnType -> Type (Univ.new_univ ()) in
+      | InProp -> prop
+      | InSet -> spec
+      | InType -> Type (Univ.new_univ ()) in
     let listarity =
       (List.map (fun s -> make_arity env true indf (create_sort s)) kelim)
       @(List.map (fun s -> make_arity env false indf (create_sort s)) kelim)