Utilisation d'un type spécifique (elimination_sorts) pour caractériser les éliminations, pour éviter les collisions avec les univers

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

14 files changed, 85 insertions, 50 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index da393b235..549496d91 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -40,6 +40,18 @@ 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 
@@ -56,7 +68,7 @@ type one_inductive_body = {
   mind_user_arity : types option;
   mind_sort : sorts;
   mind_nrealargs : int;
-  mind_kelim : sorts list;
+  mind_kelim : elimination_sorts list;
   mind_listrec : (recarg list) array;
   mind_finite : bool;
   mind_nparams : int;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 18566a0c3..e9d83506e 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -44,6 +44,11 @@ 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 
@@ -65,7 +70,7 @@ type one_inductive_body = {
   mind_user_arity : types option;
   mind_sort : sorts;
   mind_nrealargs : int;
-  mind_kelim : sorts list;
+  mind_kelim : elimination_sorts list;
   mind_listrec : (recarg list) array;
   mind_finite : bool;
   mind_nparams : int;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 344ca87fb..662692eca 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -101,11 +101,12 @@ let mind_check_wellformed env mie =
 
 let allowed_sorts issmall isunit = function
   | Type _ -> 
-      [prop;spec;types]
+      [ElimOnProp;ElimOnSet;ElimOnType]
   | Prop Pos -> 
-      if issmall then [prop;spec;types] else [prop;spec]
+      if issmall then [ElimOnProp;ElimOnSet;ElimOnType]
+      else [ElimOnProp;ElimOnSet]
   | Prop Null -> 
-      if isunit then [prop;spec] else [prop]
+      if isunit then [ElimOnProp;ElimOnSet] else [ElimOnProp]
 
 type ill_formed_ind =
   | LocalNonPos of int
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index cb6d7b117..e42df6d9c 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 -> sorts list
+val mis_kelim : inductive_instance -> elimination_sorts 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.mli b/kernel/term.mli
index 4c7d23cc4..76daa96f0 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -152,7 +152,7 @@ val mkSet : constr
 val mkType : Univ.universe -> constr
 val prop : sorts
 val spec : sorts
-val types : sorts 
+(*val types : sorts *)
 val type_0 : sorts
 
 (* Construct an implicit (see implicit arguments in the RefMan).
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 10d0bb611..317cc199d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -301,31 +301,37 @@ let is_correct_arity env sigma kelim (c,pj) indf t =
           srec (a2,a2') (Constraint.union u univ)
       | IsProd (_,a1,a2), _ -> 
           let k = whd_betadeltaiota env sigma a2 in 
-          let ksort = (match kind_of_term k with IsSort s -> s 
-			 | _ -> raise (Arity None)) in
+          let ksort = match kind_of_term k with
+	    | IsSort s -> elimination_of_sort s 
+	    | _ -> raise (Arity None) in
 	  let ind = build_dependent_inductive indf in
           let univ =
             try conv env sigma a1 ind
             with NotConvertible -> raise (Arity None) in
-          if List.exists (base_sort_cmp CONV ksort) kelim then
+          if List.exists ((=) ksort) kelim then
 	    ((true,k), Constraint.union u univ)
           else 
 	    raise (Arity (Some(k,t',error_elim_expln env sigma k t')))
       | k, IsProd (_,_,_) ->
 	  raise (Arity None)
       | k, ki -> 
-	  let ksort = (match k with IsSort s -> s 
-                         | _ ->  raise (Arity None)) in
-          if List.exists (base_sort_cmp CONV ksort) kelim then 
+	  let ksort = match k with
+	    | IsSort s -> elimination_of_sort s
+            | _ ->  raise (Arity None) in
+          if List.exists ((=) ksort) kelim then 
 	    (false, pt'), u
           else 
 	    raise (Arity (Some(pt',t',error_elim_expln env sigma pt' t')))
   in 
   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
     let listarity =
-      (List.map (make_arity env true indf) kelim)
-      @(List.map (make_arity env false indf) kelim)
+      (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)
     in 
     let ind = mis_inductive (fst (dest_ind_family indf)) in
     error_elim_arity CCI env ind listarity c pj kinds
diff --git a/library/declare.ml b/library/declare.ml
index 6809b6e55..c07a8577f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -523,12 +523,13 @@ let instantiate_inductive_section_params t ind =
   else t
 (* Eliminations. *)
 
-let eliminations = [ (prop,"_ind") ; (spec,"_rec") ; (types,"_rect") ]
+let eliminations =
+  [ (ElimOnProp,"_ind") ; (ElimOnSet,"_rec") ; (ElimOnType,"_rect") ]
 
 let elimination_suffix = function
-  | Type _    -> "_rect"
-  | Prop Null -> "_ind"
-  | Prop Pos  -> "_rec"
+  | ElimOnProp -> "_ind"
+  | ElimOnSet  -> "_rec"
+  | ElimOnType -> "_rect"
 
 let make_elimination_ident id s = add_suffix id (elimination_suffix s)
   
@@ -551,7 +552,8 @@ let declare_one_elimination mispec =
   let kelim = mis_kelim mispec in
   List.iter
     (fun (sort,suff) -> 
-       if List.mem sort kelim then declare (mindstr^suff) (make_elim sort))
+       if List.mem sort kelim then
+	 declare (mindstr^suff) (make_elim (sort_of_elimination sort)))
     eliminations
 
 let declare_eliminations sp =
diff --git a/library/declare.mli b/library/declare.mli
index c623a0cce..e17be37e3 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -117,6 +117,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 : sorts -> string
-val make_elimination_ident : inductive_ident:identifier -> sorts -> identifier
-val lookup_eliminator : Environ.env -> inductive -> sorts -> constr
+val elimination_suffix : elimination_sorts -> string
+val make_elimination_ident :
+  inductive_ident:identifier -> elimination_sorts -> identifier
+val lookup_eliminator : Environ.env -> inductive -> elimination_sorts -> constr
diff --git a/library/indrec.ml b/library/indrec.ml
index 251656c60..f15ed4b53 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -40,10 +40,11 @@ let mis_make_case_com depopt env sigma mispec kind =
     | None -> mis_sort mispec <> (Prop Null)
     | Some d -> d
   in
-  if not (List.exists (base_sort_cmp CONV kind) (mis_kelim mispec)) then
+  if not (List.exists ((=) kind) (mis_kelim mispec)) then
     raise
       (InductiveError
-	 (NotAllowedCaseAnalysis (dep,kind,mis_inductive mispec)));
+	 (NotAllowedCaseAnalysis
+	    (dep,(sort_of_elimination kind),mis_inductive mispec)));
 
   let nbargsprod = mis_nrealargs mispec + 1 in
 
@@ -74,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 kind in
+  let typP = make_arity env' dep indf (sort_of_elimination kind) in
   it_mkLambda_or_LetIn_name env 
     (mkLambda_string "P" typP
        (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
@@ -371,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 kinds in
+	  let typP = make_arity env dep indf (sort_of_elimination kinds) in
 	  mkLambda_string "P" typP
 	    (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
       | [] -> 
@@ -432,11 +433,12 @@ let instanciate_indrec_scheme sort =
 
 let check_arities listdepkind = 
   List.iter 
-    (function (mispeci,dep,kinds) -> 
+    (function (mispeci,dep,kind) -> 
        let id = mis_typename mispeci  in
        let kelim = mis_kelim mispeci in
-       if not (List.exists (base_sort_cmp CONV kinds) kelim) then
-	 raise (InductiveError (BadInduction (dep, id, kinds))))
+       if not (List.exists ((=) kind) kelim) then
+	 raise
+	   (InductiveError (BadInduction (dep, id, sort_of_elimination kind))))
     listdepkind
 
 let build_mutual_indrec env sigma = function 
@@ -459,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 = mis_sort mispec in
-  let dep = kind <> Prop Null in
+  let kind = elimination_of_sort (mis_sort mispec) in
+  let dep = kind <> ElimOnProp in
   List.hd (mis_make_indrec env sigma [(mispec,dep,kind)] mispec)
 
 (**********************************************************************)
diff --git a/library/indrec.mli b/library/indrec.mli
index e50766348..e53b7d2a8 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 -> sorts -> constr
-val make_case_nodep : env -> 'a evar_map -> inductive -> sorts -> constr
-val make_case_gen : env -> 'a evar_map -> inductive -> sorts -> constr
+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
 
 (* This builds an elimination scheme associated (using the own arity
    of the inductive) *)
@@ -34,7 +34,8 @@ val instanciate_indrec_scheme : sorts -> int -> constr -> constr
 (* This builds complex [Scheme] *)
 
 val build_mutual_indrec : 
-  env -> 'a evar_map -> (inductive * bool * sorts) list -> constr list
+  env -> 'a evar_map -> (inductive * bool * elimination_sorts) list
+    -> constr list
 
 (* These are for old Case/Match typing *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c0584cd98..c2c21d9fd 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -57,7 +57,7 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
 	else error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
         let hdcncls = string_head hdcncl in 
-	let suffix = Declare.elimination_suffix (sort_of_goal gl) in
+	let suffix = Declare.elimination_suffix (elimination_sort_of_goal gl)in
         let elim =
 	  if lft2rgt then
             pf_global gl (id_of_string (hdcncls^suffix^"_r"))
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 234c9dcd1..6e3d33121 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -309,9 +309,13 @@ let elim_sign ity i =
   let recarg = mis_recarg (lookup_mind_specif ity (Global.env())) in
   analrec [] recarg.(i-1)
 
-let sort_of_goal gl = 
+let elimination_sort_of_goal gl = 
   match kind_of_term (hnf_type_of gl (pf_concl gl)) with 
-    | IsSort s -> s
+    | IsSort s ->
+	(match s with
+	   | Prop Null -> ElimOnProp
+	   | Prop Pos -> ElimOnSet
+	   | Type _ -> ElimOnType)
     | _        -> anomaly "goal should be a type"
 
 
@@ -374,7 +378,7 @@ let general_elim_then_using
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
   let (ind,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
-  let elim = lookup_eliminator (pf_env gl) ind (sort_of_goal gl) in
+  let elim = lookup_eliminator (pf_env gl) ind (elimination_sort_of_goal gl) in
   general_elim_then_using
     elim elim_sign tac predicate (indbindings,elimbindings) c gl
 
@@ -386,7 +390,7 @@ let case_then_using tac predicate (indbindings,elimbindings) c gl =
   (* finding the case combinator *)
   let (ity,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let sigma = project gl in 
-  let sort  = sort_of_goal gl  in
+  let sort  = elimination_sort_of_goal gl  in
   let elim  = Indrec.make_case_gen (pf_env gl) sigma ity sort in  
   general_elim_then_using 
     elim case_sign tac predicate (indbindings,elimbindings) c gl
@@ -395,7 +399,7 @@ let case_nodep_then_using tac predicate (indbindings,elimbindings) c gl =
   (* finding the case combinator *)
   let (ity,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let sigma = project gl in 
-  let sort  = sort_of_goal gl  in
+  let sort  = elimination_sort_of_goal gl  in
   let elim  = Indrec.make_case_nodep (pf_env gl) sigma ity sort in  
   general_elim_then_using 
     elim case_sign tac predicate (indbindings,elimbindings) c gl
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 9bc572c6a..54b66539b 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 sort_of_goal      : goal sigma -> sorts
+val elimination_sort_of_goal : goal sigma -> Declarations.elimination_sorts
 (*i val suff              : goal sigma -> constr -> string i*)
 
 val general_elim_then_using :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a7f2fb976..09879fe39 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1058,7 +1058,7 @@ let general_elim (c,lbindc) (elimc,lbindelimc) gl =
 let default_elim (c,lbindc)  gl = 
   let env = pf_env gl in
   let (ind,t) = reduce_to_quantified_ind env (project gl) (pf_type_of gl c) in
-  let s = sort_of_goal gl in
+  let s = elimination_sort_of_goal gl in
   let elimc =
     try lookup_eliminator env ind s 
     with Not_found -> 
@@ -1069,7 +1069,8 @@ 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 s ; 'sTR " is probably not allowed" >]
+           'sPC; print_sort (Declarations.sort_of_elimination s) ;
+	   'sTR " is probably not allowed" >]
   in  general_elim (c,lbindc) (elimc,[]) gl
 
 
@@ -1422,8 +1423,8 @@ let induction_from_context isrec style hyp0 gl =
   let (mind,typ0) = pf_reduce_to_quantified_ind gl tmptyp0 in
   let indvars = find_atomic_param_of_ind mind (snd (decompose_prod typ0)) in
   let elimc =
-    if isrec then lookup_eliminator env mind (sort_of_goal gl)
-    else Indrec.make_case_gen env (project gl) mind (sort_of_goal gl)
+    if isrec then lookup_eliminator env mind (elimination_sort_of_goal gl)
+    else Indrec.make_case_gen env (project gl) mind (elimination_sort_of_goal gl)
   in
   let elimt = pf_type_of gl elimc in
   let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in
@@ -1533,7 +1534,7 @@ let general_case_analysis (c,lbindc) gl =
   let env = pf_env gl in
   let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let sigma    = project gl in 
-  let sort     = sort_of_goal gl in
+  let sort     = elimination_sort_of_goal gl in
   let elim     = Indrec.make_case_gen env sigma mind sort in 
   general_elim (c,lbindc) (elim,[]) gl
     
@@ -1585,7 +1586,7 @@ let elim_scheme_type elim t gl =
 
 let elim_type t gl =
   let (ind,t) = pf_reduce_to_atomic_ind gl t in
-  let elimc = lookup_eliminator (pf_env gl) ind (sort_of_goal gl) in
+  let elimc = lookup_eliminator (pf_env gl) ind (elimination_sort_of_goal gl) in
   elim_scheme_type elimc t gl
 
 let dyn_elim_type = function
@@ -1596,7 +1597,7 @@ let dyn_elim_type = function
 let case_type t gl =
   let (ind,t) = pf_reduce_to_atomic_ind gl t in
   let env = pf_env gl in
-  let elimc = Indrec.make_case_gen env (project gl) ind (sort_of_goal gl) in 
+  let elimc = Indrec.make_case_gen env (project gl) ind (elimination_sort_of_goal gl) in 
   elim_scheme_type elimc t gl
 
 let dyn_case_type = function