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

17 files changed, 69 insertions, 62 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)
diff --git a/library/declare.ml b/library/declare.ml
index 9b6466f47f..d2e451dd9e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -554,12 +554,12 @@ let instantiate_inductive_section_params t ind =
 (* Eliminations. *)
 
 let eliminations =
-  [ (ElimOnProp,"_ind") ; (ElimOnSet,"_rec") ; (ElimOnType,"_rect") ]
+  [ (InProp,"_ind") ; (InSet,"_rec") ; (InType,"_rect") ]
 
 let elimination_suffix = function
-  | ElimOnProp -> "_ind"
-  | ElimOnSet  -> "_rec"
-  | ElimOnType -> "_rect"
+  | InProp -> "_ind"
+  | InSet  -> "_rec"
+  | InType -> "_rect"
 
 let make_elimination_ident id s = add_suffix id (elimination_suffix s)
   
@@ -583,7 +583,7 @@ let declare_one_elimination mispec =
   List.iter
     (fun (sort,suff) -> 
        if List.mem sort kelim then
-	 declare (mindstr^suff) (make_elim (sort_of_elimination sort)))
+	 declare (mindstr^suff) (make_elim (new_sort_in_family sort)))
     eliminations
 
 let declare_eliminations sp =
diff --git a/library/declare.mli b/library/declare.mli
index b347456ce5..4d7043eae7 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -119,7 +119,7 @@ val path_of_inductive_path : inductive_path -> mutual_inductive_path
 val path_of_constructor_path : constructor_path -> mutual_inductive_path
 
 (* Look up function for the default elimination constant *)
-val elimination_suffix : elimination_sorts -> string
+val elimination_suffix : sorts_family -> string
 val make_elimination_ident :
-  inductive_ident:identifier -> elimination_sorts -> identifier
-val lookup_eliminator : Environ.env -> inductive -> elimination_sorts -> constr
+  inductive_ident:identifier -> sorts_family -> identifier
+val lookup_eliminator : Environ.env -> inductive -> sorts_family -> constr
diff --git a/library/indrec.ml b/library/indrec.ml
index f15ed4b53f..96a188da79 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -44,7 +44,7 @@ let mis_make_case_com depopt env sigma mispec kind =
     raise
       (InductiveError
 	 (NotAllowedCaseAnalysis
-	    (dep,(sort_of_elimination kind),mis_inductive mispec)));
+	    (dep,(new_sort_in_family kind),mis_inductive mispec)));
 
   let nbargsprod = mis_nrealargs mispec + 1 in
 
@@ -75,7 +75,7 @@ let mis_make_case_com depopt env sigma mispec kind =
       mkLambda_string "f" t
 	(add_branch (push_rel (Anonymous, None, t) env) (k+1))
   in
-  let typP = make_arity env' dep indf (sort_of_elimination kind) in
+  let typP = make_arity env' dep indf (new_sort_in_family kind) in
   it_mkLambda_or_LetIn_name env 
     (mkLambda_string "P" typP
        (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
@@ -372,7 +372,7 @@ let mis_make_indrec env sigma listdepkind mispec =
     let rec put_arity env i = function 
       | (mispeci,dep,kinds)::rest -> 
 	  let indf = make_ind_family (mispeci,extended_rel_list i lnamespar) in
-	  let typP = make_arity env dep indf (sort_of_elimination kinds) in
+	  let typP = make_arity env dep indf (new_sort_in_family kinds) in
 	  mkLambda_string "P" typP
 	    (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
       | [] -> 
@@ -438,7 +438,7 @@ let check_arities listdepkind =
        let kelim = mis_kelim mispeci in
        if not (List.exists ((=) kind) kelim) then
 	 raise
-	   (InductiveError (BadInduction (dep, id, sort_of_elimination kind))))
+	   (InductiveError (BadInduction (dep, id, new_sort_in_family kind))))
     listdepkind
 
 let build_mutual_indrec env sigma = function 
@@ -461,8 +461,8 @@ let build_mutual_indrec env sigma = function
   | _ -> anomaly "build_indrec expects a non empty list of inductive types"
 
 let build_indrec env sigma mispec =
-  let kind = elimination_of_sort (mis_sort mispec) in
-  let dep = kind <> ElimOnProp in
+  let kind = family_of_sort (mis_sort mispec) in
+  let dep = kind <> InProp in
   List.hd (mis_make_indrec env sigma [(mispec,dep,kind)] mispec)
 
 (**********************************************************************)
diff --git a/library/indrec.mli b/library/indrec.mli
index e53b7d2a8c..aa3a0b6f1f 100644
--- a/library/indrec.mli
+++ b/library/indrec.mli
@@ -21,9 +21,9 @@ open Evd
 
 (* These functions build elimination predicate for Case tactic *)
 
-val make_case_dep : env -> 'a evar_map -> inductive -> elimination_sorts -> constr
-val make_case_nodep : env -> 'a evar_map -> inductive -> elimination_sorts -> constr
-val make_case_gen : env -> 'a evar_map -> inductive -> elimination_sorts -> constr
+val make_case_dep : env -> 'a evar_map -> inductive -> sorts_family -> constr
+val make_case_nodep : env -> 'a evar_map -> inductive -> sorts_family -> constr
+val make_case_gen : env -> 'a evar_map -> inductive -> sorts_family -> constr
 
 (* This builds an elimination scheme associated (using the own arity
    of the inductive) *)
@@ -34,7 +34,7 @@ val instanciate_indrec_scheme : sorts -> int -> constr -> constr
 (* This builds complex [Scheme] *)
 
 val build_mutual_indrec : 
-  env -> 'a evar_map -> (inductive * bool * elimination_sorts) list
+  env -> 'a evar_map -> (inductive * bool * sorts_family) list
     -> constr list
 
 (* These are for old Case/Match typing *)
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 3017a6aee8..9b537f70e8 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -706,9 +706,9 @@ let interp_sort = function
   | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
 
 let interp_elimination_sort = function
-  | Node(loc,"PROP", []) -> Declarations.ElimOnProp
-  | Node(loc,"SET", [])  -> Declarations.ElimOnSet
-  | Node(loc,"TYPE", _) -> Declarations.ElimOnType
+  | Node(loc,"PROP", []) -> InProp
+  | Node(loc,"SET", [])  -> InSet
+  | Node(loc,"TYPE", _) -> InType
   | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
 
 let judgment_of_rawconstr sigma env c =
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 4503f09a6a..1941439c75 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -26,7 +26,7 @@ val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr
 val interp_type          : 'a evar_map -> env -> Coqast.t -> types
 val interp_sort          : Coqast.t -> sorts
 
-val interp_elimination_sort : Coqast.t -> Declarations.elimination_sorts
+val interp_elimination_sort : Coqast.t -> sorts_family
 
 val interp_openconstr    :
   'a evar_map -> env -> Coqast.t -> (existential * constr) list * constr
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0fb8d73740..89c4c84061 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -851,16 +851,20 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
       (true,pred) (* true = dependent -- par défaut *)
     else
+(*
       let s = get_sort_of env (evars_of isevars) typs.(0) in
       let predpred = it_mkLambda_or_LetIn (mkSort s) sign in
       let caseinfo = make_default_case_info mis in
       let brs = array_map2 abstract_conclusion typs cstrs in
       let predbody = mkMutCase (caseinfo, (nf_betaiota predpred), mkRel 1, brs) in
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
+*)
       (* "TODO4-2" *)
       error ("Unable to infer a Cases predicate\n"^
-"Either there is a type incompatiblity or the problem involves dependencies");
+"Either there is a type incompatiblity or the problem involves dependencies")
+(*
       (true,pred)
+*)
 
 (* Propagation of user-provided predicate through compilation steps *)
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6e3d331218..168cd94e1c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -313,9 +313,9 @@ let elimination_sort_of_goal gl =
   match kind_of_term (hnf_type_of gl (pf_concl gl)) with 
     | IsSort s ->
 	(match s with
-	   | Prop Null -> ElimOnProp
-	   | Prop Pos -> ElimOnSet
-	   | Type _ -> ElimOnType)
+	   | Prop Null -> InProp
+	   | Prop Pos -> InSet
+	   | Type _ -> InType)
     | _        -> anomaly "goal should be a type"
 
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 54b66539b8..2451a89794 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -119,7 +119,7 @@ type branch_assumptions = {
   recargs   : identifier list; (* the RECURSIVE constructor arguments *)
   indargs   : identifier list} (* the inductive arguments *)
 
-val elimination_sort_of_goal : goal sigma -> Declarations.elimination_sorts
+val elimination_sort_of_goal : goal sigma -> sorts_family
 (*i val suff              : goal sigma -> constr -> string i*)
 
 val general_elim_then_using :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f168cb5cb0..18cb8ee509 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1067,7 +1067,7 @@ let default_elim (c,lbindc)  gl =
            pr_id id; 'sPC;
 	   'sTR "The elimination of the inductive definition :";
            pr_id base; 'sPC; 'sTR "on sort "; 
-           'sPC; print_sort (Declarations.sort_of_elimination s) ;
+           'sPC; print_sort (new_sort_in_family s) ;
 	   'sTR " is probably not allowed" >]
   in  general_elim (c,lbindc) (elimc,[]) gl