- Reforme de la gestion des args recursifs (via arbres reguliers)

- coqtop -byte -opt bouclait!


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

7 files changed, 60 insertions, 53 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 41d6941a9..ca13c1c16 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -76,7 +76,7 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr =
     match args, recargs with 
       | (name,None,c as d)::rea,(ra::reca) -> 
 	  let d =
- 	    match ra with 
+ 	    match dest_recarg ra with 
 	      | Mrec k when k=j ->
 		  let t = mkExistential isevars env in
 		  mkArrow t
@@ -99,7 +99,7 @@ let branch_scheme env isevars isrec indf =
   if isrec then
     array_map2
       (rec_branch_scheme env isevars ind)
-      mip.mind_listrec cstrs
+      (dest_subterms mip.mind_recargs) cstrs
   else 
     Array.map (norec_branch_scheme env isevars) cstrs
 
@@ -117,8 +117,10 @@ let concl_n env sigma =
 let count_rec_arg j = 
   let rec crec i = function 
     | [] -> i 
-    | (Mrec k::l) -> crec (if k=j then (i+1) else i) l
-    | (_::l) -> crec i l
+    | ra::l ->
+        (match dest_recarg ra with
+            Mrec k -> crec (if k=j then (i+1) else i) l
+          | _ -> crec i l)
   in 
   crec 0
 
@@ -142,7 +144,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) =
   let pred =
     let (ind,params) = dest_ind_family indf in
     let (mib,mip) = Inductive.lookup_mind_specif env ind in
-    let recargs = mip.mind_listrec in
+    let recargs = dest_subterms mip.mind_recargs in
     if Array.length recargs = 0 then raise (NotInferable MlCaseAbsurd);
     let recargi = recargs.(i) in
     let j = snd ind in (* index of inductive *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6d12257b3..8e5e35930 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -15,6 +15,7 @@ open Names
 open Term
 open Declarations
 open Inductive
+open Inductiveops
 open Environ
 open Sign
 open Declare
@@ -34,17 +35,9 @@ let encode_inductive ref =
         errorlabstrm "indsp_of_id"
           (pr_global_env (Global.env()) ref ++
 	     str" is not an inductive type") in
-  let (mib,mip) = Global.lookup_inductive indsp in
-  let constr_lengths = Array.map List.length mip.mind_listrec in
+  let constr_lengths = mis_constr_nargs indsp in
   (indsp,constr_lengths)
 
-let constr_nargs indsp =
-  let (mib,mip) = Global.lookup_inductive indsp in
-  let nparams = mip.mind_nparams in
-  Array.map
-    (fun t -> List.length (fst (decompose_prod_assum t)) - nparams)
-    mip.mind_nf_lc
-
 (* Parameterization of the translation from constr to ast      *)
 
 (* Tables for Cases printing under a "if" form, a "let" form,  *)
@@ -110,10 +103,10 @@ module PrintingLet = Goptions.MakeIdentTable(PrintingCasesLet)
 
 let force_let ci =
   let indsp = ci.ci_ind in
-  let lc = constr_nargs indsp in PrintingLet.active (indsp,lc)
+  let lc = mis_constr_nargs indsp in PrintingLet.active (indsp,lc)
 let force_if ci =
   let indsp = ci.ci_ind in
-  let lc = constr_nargs indsp in PrintingIf.active (indsp,lc)
+  let lc = mis_constr_nargs indsp in PrintingIf.active (indsp,lc)
 
 (* Options for printing or not wildcard and synthetisable types *)
 
@@ -235,7 +228,7 @@ let rec detype tenv avoid env t =
 	let indsp = annot.ci_ind in
         let considl = annot.ci_pp_info.cnames in
         let k = annot.ci_pp_info.ind_nargs in
-	let consnargsl = constr_nargs indsp in
+	let consnargsl = mis_constr_nargs indsp in
 	let pred = 
 	  if synth_type & computable p k & considl <> [||] then
 	    None
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index cb51cecaf..ef9db0c44 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -42,7 +42,6 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 
 let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
   let lnamespar = mip.mind_params_ctxt in
-  let nparams = mip.mind_nparams in
   let dep = match depopt with 
     | None -> mip.mind_sort <> (Prop Null)
     | Some d -> d
@@ -133,12 +132,14 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
       | Prod (n,t,c_0) ->
           let (optionpos,rest) = 
 	    match recargs with 
-	      | [] -> None,[] 
-	      | Mrec j :: rest when is_rec -> (depPvect.(j),rest)
-	      | Imbr _ :: rest  -> 
-		  Options.if_verbose warning "Ignoring recursive call"; 
-		  (None,rest) 
-              | _ :: rest -> (None, rest)
+	      | [] -> None,[]
+              | ra::rest ->
+                  (match dest_recarg ra with 
+	            | Mrec j when is_rec -> (depPvect.(j),rest)
+	            | Imbr _  -> 
+		        Options.if_verbose warning "Ignoring recursive call"; 
+		        (None,rest) 
+                    | _ -> (None, rest))
 	  in 
           (match optionpos with 
 	     | None -> 
@@ -201,8 +202,7 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
   let rec process_constr env i f = function
     | (n,None,t as d)::cprest, recarg::rest -> 
         let optionpos = 
-	  match recarg with 
-            | Param i -> None
+	  match dest_recarg recarg with 
             | Norec   -> None
             | Imbr _  -> None
             | Mrec i  -> fvect.(i)
@@ -246,10 +246,9 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
             (Array.set depPvec (snd indi) (Some(dep,mkRel k));
              assign (k-1) rest)
     in 
-    assign nrec listdepkind  
-  in 
+    assign nrec listdepkind in 
   let recargsvec =
-    Array.map (fun mip -> mip.mind_listrec) mib.mind_packets in
+    Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
   let make_one_rec p =
     let makefix nbconstruct =
       let rec mrec i ln ltyp ldef = function
@@ -277,7 +276,8 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 	    let branches = 
 	      array_map3
 		(make_rec_branch_arg env sigma (nparams,depPvec,nar+1))
-                vecfi constrs recargsvec.(tyi) in
+                vecfi constrs
+                (dest_subterms recargsvec.(tyi)) in
 	    let j = (match depPvec.(tyi) with 
 		       | Some (_,c) when isRel c -> destRel c 
 		       | _ -> assert false) in
@@ -322,7 +322,7 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 	    if j = nconstr then 
 	      make_branch env (i+j) rest 
 	    else 
-	      let recarg = recargsvec.(tyi).(j) in
+	      let recarg = (dest_subterms recargsvec.(tyi)).(j) in
 	      let vargs = extended_rel_list (nrec+i+j) lnamespar in
 	      let indf = (indi, vargs) in
 	      let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
@@ -348,7 +348,8 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
     let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
     let env' = push_rel_context lnamespar env in
     if mis_is_recursive_subset
-      (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind) mipi
+      (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
+      mipi.mind_recargs
     then 
       it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamespar
     else 
@@ -461,19 +462,19 @@ let type_rec_branches recursive env sigma indt pj c =
   let IndType (indf,realargs) = indt in
   let p = pj.uj_val in
   let (ind,params) = dest_ind_family indf in
-  let tyi = snd ind in
   let (mib,mip) = lookup_mind_specif env ind in
-  let is_rec = recursive && mis_is_recursive_subset [tyi] mip in
+  let recargs = mip.mind_recargs in
+  let tyi = snd ind in
+  let is_rec = recursive && mis_is_recursive_subset [tyi] recargs in
   let dep = is_dependent_elimination env pj.uj_type indf in 
   let init_depPvec i = if i = tyi then Some(dep,p) else None in
   let depPvec = Array.init mib.mind_ntypes init_depPvec in
   let vargs = Array.of_list params in
   let constructors = get_constructors env indf in
-  let recargs = mip.mind_listrec in
   let lft =
     array_map2
       (type_rec_branch recursive dep env sigma (params,depPvec,0) tyi)
-      constructors recargs in
+      constructors (dest_subterms recargs) in
   (lft,
    if dep then Reduction.beta_appvect p (Array.of_list (realargs@[c])) 
    else Reduction.beta_appvect p (Array.of_list realargs))
@@ -516,7 +517,8 @@ let declare_one_elimination ind =
 (* in case the inductive has a type elimination, generates only one induction scheme, 
    the other ones share the same code with the apropriate type *)
    if List.mem InType kelim then
-    let cte = declare (mindstr^type_suff) (make_elim (new_sort_in_family InType)) None
+    let cte =
+      declare (mindstr^type_suff) (make_elim (new_sort_in_family InType)) None
     in let c = mkConst cte and t = constant_type (Global.env ()) cte
     in List.iter  
 	 (fun (sort,suff) -> 
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index e28331848..14b9cd5e1 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -46,7 +46,7 @@ val type_rec_branches : bool -> env -> evar_map -> inductive_type
 val make_rec_branch_arg : 
   env -> evar_map ->
     int * ('b * constr) option array * int ->
-    constr -> constructor_summary -> recarg list -> constr
+    constr -> constructor_summary -> wf_paths list -> constr
 
 (* *)
 val declare_eliminations : mutual_inductive -> unit
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index cb1e7d3ee..3a51ae0a0 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -48,19 +48,20 @@ let mkAppliedInd (IndType ((ind,params), realargs)) =
   applist (mkInd ind,params@realargs)
 
 
-let mis_is_recursive_subset listind mip = 
+let mis_is_recursive_subset listind rarg = 
   let rec one_is_rec rvec = 
     List.exists
-      (function
-	 | Mrec i       -> List.mem i listind 
-         | Imbr(_,lvec) -> one_is_rec lvec
-         | Norec        -> false
-         | Param _      -> false) rvec
+      (fun ra ->
+        match dest_recarg ra with
+	  | Mrec i -> List.mem i listind 
+          | Imbr _ -> array_exists one_is_rec (dest_subterms ra)
+          | Norec  -> false) rvec
   in 
-  array_exists one_is_rec mip.mind_listrec
+  array_exists one_is_rec (dest_subterms rarg)
 
-let mis_is_recursive (mib,mip) =
-  mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1)) mip
+let mis_is_recursive (ind,mib,mip) =
+  mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1))
+    mip.mind_recargs
 
 let mis_nf_constructor_type (ind,mib,mip) j =
   let specif = mip.mind_nf_lc
@@ -70,6 +71,13 @@ let mis_nf_constructor_type (ind,mib,mip) j =
   if j > nconstr then error "Not enough constructors in the type";
   substl (list_tabulate make_Ik ntypes) specif.(j-1)
 
+(* Arity of constructors excluding parameters and local defs *)
+let mis_constr_nargs indsp =
+  let (mib,mip) = Global.lookup_inductive indsp in
+  let recargs = dest_subterms mip.mind_recargs in
+  Array.map List.length recargs
+
+
 (* Annotation for cases *)
 let make_case_info env ind style pats_source =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b807c2d7f..a76395dd8 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -33,10 +33,12 @@ val substnl_ind_type :
   constr list -> int -> inductive_type -> inductive_type
 
 val mkAppliedInd : inductive_type -> constr
-val mis_is_recursive_subset : int list -> one_inductive_body -> bool
-val mis_is_recursive : mutual_inductive_body * one_inductive_body -> bool
+val mis_is_recursive_subset : int list -> wf_paths -> bool
+val mis_is_recursive :
+  inductive * mutual_inductive_body * one_inductive_body -> bool
 val mis_nf_constructor_type :
   inductive * mutual_inductive_body * one_inductive_body -> int -> constr
+val mis_constr_nargs : inductive -> int array
 
 type constructor_summary = {
   cs_cstr : constructor;
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 11ddc43cd..8e9e0278e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -46,15 +46,15 @@ let transform_rec loc env sigma (pj,c,lf) indt =
   let (indf,realargs) = dest_ind_type indt in
   let (ind,params) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
+  let recargs = mip.mind_recargs in
   let mI = mkInd ind in
-  let recargs = mip.mind_listrec in
-  let tyi = snd ind in
   let ci = make_default_case_info env ind in
   let nconstr = Array.length mip.mind_consnames in
   if Array.length lf <> nconstr then 
     (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in
      error_number_branches_loc loc env sigma cj nconstr);
-  if mis_is_recursive_subset [tyi] mip then
+  let tyi = snd ind in
+  if mis_is_recursive_subset [tyi] recargs then
     let dep =
       is_dependent_elimination env (nf_evar sigma pj.uj_type) indf in 
     let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
@@ -71,7 +71,7 @@ let transform_rec loc env sigma (pj,c,lf) indt =
              (Indrec.make_rec_branch_arg env sigma
                 (nparams,depFvec,nar+1)
                 f t reca))
-        (Array.map (lift (nar+2)) lf) constrs recargs 
+        (Array.map (lift (nar+2)) lf) constrs (dest_subterms recargs) 
     in 
     let deffix = 
       it_mkLambda_or_LetIn_name env