Extension du case_info : ajout du nombre de vrais args de chaque constr pour la iota-réduction et d'autres informations pour l'affichage dans l'argument du cases

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

3 files changed, 32 insertions, 31 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 00dd44445a..844e364316 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -115,8 +115,6 @@ type rhs =
       rhs_lift   : int;
       it         : rawconstr }
 
-type pattern_source = DefaultPat of int | RegularPat
-
 type equation =
     { dependencies : constr lifted list;
       patterns     : pattern list; 
@@ -222,9 +220,9 @@ let liftn_ind_data n depth md =
     nrealargs = md.nrealargs;
     nconstr = md.nconstr;
     params = List.map (liftn n depth) md.params;
-    realargs = List.map (liftn n depth) md.realargs;
-    make_arity = md.make_arity;
-    make_constrs = md.make_constrs }
+    realargs = List.map (liftn n depth) md.realargs }
+
+let lift_ind_data n = liftn_ind_data n 1
 
 let liftn_tomatch_type n depth = function
   | IsInd ind_data -> IsInd (liftn_ind_data n depth ind_data)
@@ -245,9 +243,7 @@ let substn_many_ind_data cv depth md =
     nrealargs = md.nrealargs;
     nconstr = md.nconstr;
     params = List.map (substn_many cv depth) md.params;
-    realargs = List.map (substn_many cv depth) md.realargs;
-    make_arity = md.make_arity;
-    make_constrs = md.make_constrs }
+    realargs = List.map (substn_many cv depth) md.realargs }
 
 let substn_many_tomatch v depth = function
   | IsInd ind_data -> IsInd (substn_many_ind_data v depth ind_data)
@@ -501,7 +497,7 @@ let infer_predicate env isevars typs cstrs ind_data =
   let (cclargs,_,typn) = eqns.(ind_data.nconstr -1) in
   if array_for_all (fun (_,_,typ) -> the_conv_x env isevars typn typ) eqns
   then
-    let (sign,_) = ind_data.make_arity ind_data.mind ind_data.params in
+    let (sign,_) = get_arity env !isevars ind_data in
     let pred = lam_it (lift (List.length sign) typn) sign in
     (false,pred) (* true = dependent -- par défaut *)
   else
@@ -559,10 +555,10 @@ let rec extract_predicate = function
   | PrLetIn ((args,None),pred) -> substl args (extract_predicate pred)
   | PrCcl ccl -> ccl
 
-let abstract_predicate ind_data = function
+let abstract_predicate env sigma ind_data = function
   | PrProd _ | PrCcl _ -> anomaly "abstract_predicate: must be some LetIn"
   | PrLetIn ((_,copt),pred) ->
-      let asign,_ = ind_data.make_arity ind_data.mind ind_data.params in
+      let asign,_ = get_arity env sigma ind_data in
       let sign =
 	List.map (fun (na,t) -> (named_hd (Global.env()) t na,t)) asign in
       let dep = copt<> None in
@@ -590,7 +586,7 @@ let specialize_predicate_match tomatchs cs = function
 let find_predicate env isevars p typs cstrs current ind_data =
   let (dep,pred) =
     match p with
-      | Some p -> abstract_predicate ind_data p
+      | Some p -> abstract_predicate env !isevars ind_data p
       | None -> infer_predicate env isevars typs cstrs ind_data in
   let typ = applist (pred, ind_data.realargs) in
   if dep then (pred, applist (typ, [current]), dummy_sort)
@@ -721,7 +717,7 @@ and match_current pb (n,tm) =
 	check_all_variables typ pb.mat;
 	compile (shift_problem pb)
     | IsInd ind_data ->
-	let cstrs = ind_data.make_constrs ind_data.mind ind_data.params in
+	let cstrs = get_constructors pb.env !(pb.isevars) ind_data in
 	let eqns,defaults = group_equations ind_data.mind cstrs pb.mat in
 	if array_for_all ((=) []) eqns
 	then compile (shift_problem pb)
@@ -736,8 +732,9 @@ and match_current pb (n,tm) =
 	  let (pred,typ,s) =
 	    find_predicate pb.env pb.isevars 
 	      pb.pred brtyps cstrs current ind_data in
-	  { uj_val = mkMutCaseA (ci_of_mind (mkMutInd ind_data.mind (*,tags*)))
-		       (*eta_reduce_if_rel*) pred current brvals;
+	  let ci = make_case_info
+		     (lookup_mind_specif ind_data.mind pb.env) None tags in
+	  { uj_val = mkMutCaseA ci (*eta_reduce_if_rel*) pred current brvals;
 	    uj_type = typ;
 	    uj_kind = s }
 
@@ -858,11 +855,11 @@ let coerce_to_indtype typing_fun isevars env matx tomatchl =
 (***********************************************************************)
 (* preparing the elimination predicate if any                          *)
 
-let build_expected_arity isdep tomatchl sort =
+let build_expected_arity env sigma isdep tomatchl sort =
   let cook n = function
     | _,IsInd ind_data ->
-	(build_dependent_inductive ind_data,
-	 fst (ind_data.make_arity ind_data.mind ind_data.params))
+	let is = lift_ind_data n ind_data in
+	(build_dependent_inductive is, fst (get_arity env sigma is))
     | _,NotInd _ -> anomaly "Should have been catched in case_dependent"
   in
   let rec buildrec n = function
@@ -870,7 +867,7 @@ let build_expected_arity isdep tomatchl sort =
     | tm::ltm ->
 	let (ty1,aritysign) = cook n tm in
 	let rec follow n = function
-	  | (na,ty2)::sign -> DOP2(Prod,lift n ty2,DLAM(na,follow (n+1) sign))
+	  | (na,ty2)::sign -> DOP2(Prod,ty2,DLAM(na,follow (n+1) sign))
 	  | _ ->
 	      if isdep then DOP2(Prod,ty1,DLAM(Anonymous,buildrec (n+1) ltm))
 	      else buildrec n ltm
@@ -930,9 +927,9 @@ let case_dependent env sigma loc predj tomatchs =
   let ndepv = List.map nb_dep_ity tomatchs in
   let sum = List.fold_right (fun i j -> i+j)  ndepv 0 in
   let depsum = sum + List.length tomatchs in
-  if n = sum then (false,build_expected_arity true tomatchs sort)
+  if n = sum then (false,build_expected_arity env sigma false tomatchs sort)
   else if n = depsum
-  then (true,build_expected_arity true tomatchs sort)
+  then (true,build_expected_arity env sigma true tomatchs sort)
   else error_wrong_predicate_arity_loc loc CCI env etapred sum depsum
 
 let prepare_predicate typing_fun isevars env tomatchs = function
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 02742b64c1..3af306fe43 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -83,7 +83,7 @@ let transform_rec loc env sigma cl (ct,pt) =
     error_number_branches_loc loc CCI env c ct expn;
   if is_recursive [mispec.mis_tyi] recargs then
     let (dep,_) = find_case_dep_nparams env sigma (c,p) appmind pt in 
-    let ntypes = mis_nconstr mispec 
+    let ntypes = mis_ntypes mispec (* was mis_nconstr !?! *)
     and tyi = mispec.mis_tyi 
     and nparams = mis_nparams mispec in
     let depFvec = Array.create ntypes (None : (bool * constr) option) in 
@@ -96,6 +96,7 @@ let transform_rec loc env sigma cl (ct,pt) =
       hnf_prod_appvect env sigma "make_branch" (mis_arity mispec) vargs in
     let lnames,_ = splay_prod env sigma realar in 
     let nar = List.length lnames in
+    let ci = make_default_case_info mispec in
     let branches = 
       array_map3
 	(fun f t reca -> 
@@ -110,8 +111,7 @@ let transform_rec loc env sigma cl (ct,pt) =
 	(lambda_create env
 	   (appvect (mI,Array.append (Array.map (lift (nar+1)) vargs)
                        (rel_vect 0 nar)),
-            mkMutCaseA (ci_of_mind mI) 
-              (lift (nar+2) p) (Rel 1) branches))
+            mkMutCaseA ci (lift (nar+2) p) (Rel 1) branches))
         (lift_context 1 lnames) 
     in
     if noccurn 1 deffix then 
@@ -136,8 +136,11 @@ let transform_rec loc env sigma cl (ct,pt) =
 		       DLAMV(Name(id_of_string "F"),[|deffix|])|])
       in 
       applist (fix,realargs@[c])
-  else 
-    mkMutCaseA (ci_of_mind mI) p c lf
+  else
+    let lnames,_ = splay_prod env sigma (mis_arity mispec) in 
+    let nar = List.length lnames in
+    let ci = make_default_case_info mispec in
+    mkMutCaseA ci p c lf
 
 (***********************************************************************)
 let ctxt_of_ids ids =
@@ -411,7 +414,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
   let evalct = nf_ise1 !isevars cj.uj_type
   and evalPt = nf_ise1 !isevars pj.uj_type in
 
-  let (mind,bty,rsty) =
+  let (_,bty,rsty) =
     Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in
   if Array.length bty <> Array.length lf then
     wrong_number_of_cases_message loc env isevars (cj.uj_val,evalct)
@@ -428,7 +431,8 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
       then 
 	let rEC = Array.append [|pj.uj_val; cj.uj_val|] lfv in
 	transform_rec loc env !isevars rEC (evalct,evalPt)
-      else let ci = ci_of_mind mind in
+      else
+	let ci = make_default_case_info (lookup_mind_specif mind env) in
 	mkMutCaseA ci pj.uj_val cj.uj_val (Array.map (fun j-> j.uj_val) lfj) in
 
        {uj_val = v;
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index b84e1f0bef..51f7e66e30 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -53,14 +53,14 @@ let rec type_of env cstr=
     | IsMutConstruct cstr -> 
         let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ
     | IsMutCase (_,p,c,lf) ->
-        let {realargs=args;make_arity=make_arity;params=params;mind=mind} =
+        let ind_data =
           try try_mutind_of env sigma (type_of env c)
           with Induc -> anomaly "type_of: Bad inductive" in
-	let (aritysign,_) = make_arity mind params in
+	let (aritysign,_) = get_arity env sigma ind_data in
 	let (psign,_) = splay_prod env sigma (type_of env p) in
         let al =
 	  if List.length psign > List.length aritysign
-	  then args@[c] else args in
+	  then ind_data.realargs@[c] else ind_data.realargs in
         whd_betadeltaiota env sigma (applist (p,al))
     | IsLambda (name,c1,c2) ->
         let var = make_typed c1 (sort_of env c1) in