Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 37 insertions, 30 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 9f8c06da..636f8622 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductiveops.ml 11436 2008-10-07 13:56:55Z barras $ *)
+(* $Id$ *)
 
 open Util
 open Names
 open Univ
 open Term
 open Termops
+open Namegen
 open Sign
 open Declarations
 open Environ
@@ -71,16 +72,15 @@ let substnl_ind_type l n = map_inductive_type (substnl l n)
 let mkAppliedInd (IndType ((ind,params), realargs)) =
   applist (mkInd ind,params@realargs)
 
-
-(* Does not consider imbricated or mutually recursive types *) 
-let mis_is_recursive_subset listind rarg = 
-  let rec one_is_rec rvec = 
+(* Does not consider imbricated or mutually recursive types *)
+let mis_is_recursive_subset listind rarg =
+  let rec one_is_rec rvec =
     List.exists
       (fun ra ->
         match dest_recarg ra with
-	  | Mrec i -> List.mem i listind 
+	  | Mrec i -> List.mem i listind
           | _ -> false) rvec
-  in 
+  in
   array_exists one_is_rec (dest_subterms rarg)
 
 let mis_is_recursive (ind,mib,mip) =
@@ -91,7 +91,7 @@ let mis_nf_constructor_type (ind,mib,mip) j =
   let specif = mip.mind_nf_lc
   and ntypes = mib.mind_ntypes
   and nconstr = Array.length mip.mind_consnames in
-  let make_Ik k = mkInd ((fst ind),ntypes-k-1) in 
+  let make_Ik k = mkInd ((fst ind),ntypes-k-1) in
   if j > nconstr then error "Not enough constructors in the type.";
   substl (list_tabulate make_Ik ntypes) specif.(j-1)
 
@@ -102,15 +102,15 @@ let mis_constr_nargs indsp =
   let recargs = dest_subterms mip.mind_recargs in
   Array.map List.length recargs
 
-let mis_constr_nargs_env env (kn,i) = 
+let mis_constr_nargs_env env (kn,i) =
   let mib = Environ.lookup_mind kn env in
-  let mip = mib.mind_packets.(i) in 
+  let mip = mib.mind_packets.(i) in
   let recargs = dest_subterms mip.mind_recargs in
   Array.map List.length recargs
 
 let mis_constructor_nargs_env env ((kn,i),j) =
   let mib = Environ.lookup_mind kn env in
-  let mip = mib.mind_packets.(i) in 
+  let mip = mib.mind_packets.(i) in
   recarg_length mip.mind_recargs j + mib.mind_nparams
 
 let constructor_nrealargs env (ind,j) =
@@ -125,11 +125,15 @@ let get_full_arity_sign env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_arity_ctxt
 
+let nconstructors ind =
+  let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+  Array.length mip.mind_consnames
+
 (* Length of arity (w/o local defs) *)
 
 let inductive_nargs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  mib.mind_nparams, mip.mind_nrealargs
+  (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt)
 
 let allowed_sorts env (kn,i as ind) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -138,7 +142,7 @@ let allowed_sorts env (kn,i as ind) =
 (* Annotation for cases *)
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let print_info = { ind_nargs = mip.mind_nrealargs; style = style } in
+  let print_info = { ind_nargs = mip.mind_nrealargs_ctxt; style = style } in
   { ci_ind     = ind;
     ci_npar    = mib.mind_nparams;
     ci_cstr_nargs = mip.mind_consnrealdecls;
@@ -172,7 +176,7 @@ let instantiate_params t args sign =
 	(match kind_of_term t with
 	   | Prod(_,_,t) -> inst (a::s) t (ctxt,args)
 	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
-    | ((_,(Some b),_)::ctxt,args) -> 
+    | ((_,(Some b),_)::ctxt,args) ->
 	(match kind_of_term t with
 	   | LetIn(_,_,_,t) -> inst ((substl s b)::s) t (ctxt,args)
 	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
@@ -249,7 +253,7 @@ let build_dependent_constructor cs =
 let build_dependent_inductive env ((ind, params) as indf) =
   let arsign,_ = get_arity env indf in
   let nrealargs = List.length arsign in
-  applist 
+  applist
     (mkInd ind,
      (List.map (lift nrealargs) params)@(extended_rel_list 0 arsign))
 
@@ -322,7 +326,7 @@ let find_coinductive env sigma c =
 (* find appropriate names for pattern variables. Useful in the Case
    and Inversion (case_then_using et case_nodep_then_using) tactics. *)
 
-let is_predicate_explicitly_dep env pred arsign = 
+let is_predicate_explicitly_dep env pred arsign =
   let rec srec env pval arsign =
     let pv' = whd_betadeltaiota env Evd.empty pval in
     match kind_of_term pv', arsign with
@@ -330,7 +334,7 @@ let is_predicate_explicitly_dep env pred arsign =
 	  srec (push_rel_assum (na,t) env) b arsign
       | Lambda (na,_,_), _ ->
 
-       (* The following code has impact on the introduction names
+       (* The following code has an impact on the introduction names
 	  given by the tactics "case" and "inversion": when the
 	  elimination is not dependent, "case" uses Anonymous for
 	  inductive types in Prop and names created by mkProd_name for
@@ -370,18 +374,21 @@ let set_pattern_names env ind brv =
   let arities =
     Array.map
       (fun c ->
-        rel_context_length (fst (decompose_prod_assum c)) -
+        rel_context_length ((prod_assum c)) -
         mib.mind_nparams)
       mip.mind_nf_lc in
   array_map2 (set_names env) arities brv
 
-
-let type_case_branches_with_names env indspec pj c =
+let type_case_branches_with_names env indspec p c =
   let (ind,args) = indspec in
-  let (lbrty,conclty,_) = Inductive.type_case_branches env indspec pj c in
-  let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let params = list_firstn mib.mind_nparams args in
-  if is_elim_predicate_explicitly_dependent env pj.uj_val (ind,params) then
+  let (mib,mip as specif) = Inductive.lookup_mind_specif env ind in
+  let nparams = mib.mind_nparams in
+  let (params,realargs) = list_chop nparams args in
+  let lbrty = Inductive.build_branches_type ind specif params p in
+  (* Build case type *)
+  let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
+  (* Adjust names *)
+  if is_elim_predicate_explicitly_dependent env p (ind,params) then
     (set_pattern_names env ind lbrty, conclty)
   else (lbrty, conclty)
 
@@ -399,7 +406,7 @@ let arity_of_case_predicate env (ind,params) dep k =
 (* Check if u (sort of a parameter) appears in the sort of the
    inductive (is). This is done by trying to enforce u > u' >= is
    in the empty univ graph. If an inconsistency appears, then
-   is depends on u. *)  
+   is depends on u. *)
 let is_constrained is u =
   try
     let u' = fresh_local_univ() in
@@ -450,7 +457,7 @@ let type_of_inductive_knowing_conclusion env mip conclty =
 (* A function which checks that a term well typed verifies both
    syntactic conditions *)
 
-let control_only_guard env c = 
+let control_only_guard env c =
   let check_fix_cofix e c = match kind_of_term c with
     | CoFix (_,(_,_,_) as cofix) ->
 	Inductive.check_cofix e cofix
@@ -458,12 +465,12 @@ let control_only_guard env c =
 	Inductive.check_fix e fix
     | _ -> ()
   in
-  let rec iter env c = 
-    check_fix_cofix env c; 
+  let rec iter env c =
+    check_fix_cofix env c;
     iter_constr_with_full_binders push_rel iter env c
   in
   iter env c
 
-let subst_inductive subst (kn,i as ind) = 
-  let kn' = Mod_subst.subst_kn subst kn in
+let subst_inductive subst (kn,i as ind) =
+  let kn' = Mod_subst.subst_ind subst kn in
   if kn == kn' then ind else (kn',i)