Correction du bug #1273 (problème avec les paramètres non récursivement uniformes dans le cas de types mutuellement inductifs)

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

1 files changed, 74 insertions, 73 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index f3e3b6d2c5..abd49ee4b7 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -275,19 +275,18 @@ let mis_make_indrec env sigma listdepkind mib =
     Array.create mib.mind_ntypes (None : (bool * constr) option) in 
   let _ = 
     let rec 
-      assign k = function 
-	| [] -> ()
-        | (indi,mibi,mipi,dep,_)::rest -> 
-            (Array.set depPvec (snd indi) (Some(dep,mkRel k));
-             assign (k-1) rest)
+	assign k = function 
+	  | [] -> ()
+          | (indi,mibi,mipi,dep,_)::rest -> 
+              (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_recargs) mib.mind_packets in
- (* recarg information for non recursive parameters *)
+  (* recarg information for non recursive parameters *)
   let rec recargparn l n = 
-    if n = 0 then l else recargparn (mk_norec::l) (n-1) 
-  in
+    if n = 0 then l else recargparn (mk_norec::l) (n-1) in
   let recargpar = recargparn [] (nparams-nparrec) in
   let make_one_rec p =
     let makefix nbconstruct =
@@ -296,97 +295,97 @@ let mis_make_indrec env sigma listdepkind mib =
 	    let tyi = snd indi in
 	    let nctyi =
               Array.length mipi.mind_consnames in (* nb constructeurs du type*)
-
+	      
             (* arity in the context of the fixpoint, i.e.
-                P1..P_nrec f1..f_nbconstruct *)
+               P1..P_nrec f1..f_nbconstruct *)
 	    let args = extended_rel_list (nrec+nbconstruct) lnamesparrec in
 	    let indf = make_ind_family(indi,args) in
-
+	      
 	    let arsign,_ = get_arity env indf in
 	    let depind = build_dependent_inductive env indf in
 	    let deparsign = (Anonymous,None,depind)::arsign in
-	    
+	      
 	    let nonrecpar = rel_context_length lnonparrec in
 	    let larsign = rel_context_length deparsign in
 	    let ndepar = larsign - nonrecpar in
 	    let dect = larsign+nrec+nbconstruct in
-
-              (* constructors in context of the Cases expr, i.e.
-         P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
+	      
+            (* constructors in context of the Cases expr, i.e.
+               P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
 	    let args' = extended_rel_list (dect+nrec) lnamesparrec in
 	    let args'' = extended_rel_list ndepar lnonparrec in
             let indf' = make_ind_family(indi,args'@args'') in
-
+	      
 	    let branches = 
 	      let constrs = get_constructors env indf' in
 	      let fi = rel_vect (dect-i-nctyi) nctyi in
 	      let vecfi = Array.map 
-			    (fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
-			    fi 
+		(fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
+		fi 
 	      in
-	      array_map3
-		(make_rec_branch_arg env sigma 
-		   (nparrec,depPvec,larsign))
-                vecfi constrs (dest_subterms recargsvec.(tyi)) 
+		array_map3
+		  (make_rec_branch_arg env sigma 
+		      (nparrec,depPvec,larsign))
+                  vecfi constrs (dest_subterms recargsvec.(tyi)) 
 	    in
-
+	      
 	    let j = (match depPvec.(tyi) with 
-		       | Some (_,c) when isRel c -> destRel c 
-		       | _ -> assert false) 
+	      | Some (_,c) when isRel c -> destRel c 
+	      | _ -> assert false) 
 	    in
-
-	      (* Predicate in the context of the case *)
-
+	      
+	    (* Predicate in the context of the case *)
+	      
 	    let depind' = build_dependent_inductive env indf' in
 	    let arsign',_ = get_arity env indf' in
 	    let deparsign' = (Anonymous,None,depind')::arsign' in
-
+	      
 	    let pargs =
 	      let nrpar = extended_rel_list (2*ndepar) lnonparrec 
 	      and nrar = if dep then extended_rel_list 0 deparsign'
-	      else extended_rel_list 1 arsign'
+		else extended_rel_list 1 arsign'
 	      in nrpar@nrar
-
+		
 	    in
 
-		(* body of i-th component of the mutual fixpoint *)
+	    (* body of i-th component of the mutual fixpoint *)
 	    let deftyi = 
 	      let ci = make_default_case_info env RegularStyle indi in
 	      let concl = applist (mkRel (dect+j+ndepar),pargs) in 
 	      let pred =
 		it_mkLambda_or_LetIn_name env 
 		  ((if dep then mkLambda_name env else mkLambda)
-		   (Anonymous,depind',concl))
+		      (Anonymous,depind',concl))
 		  arsign'
 	      in
-	      it_mkLambda_or_LetIn_name env
-		(mkCase (ci, pred, 
-		             mkRel 1,
-			     branches))
-		(lift_rel_context nrec deparsign)
+		it_mkLambda_or_LetIn_name env
+		  (mkCase (ci, pred, 
+		          mkRel 1,
+			  branches))
+		  (lift_rel_context nrec deparsign)
 	    in
-
+	      
 	    (* type of i-th component of the mutual fixpoint *)
-
+	      
 	    let typtyi =
-	    let concl = 
-	      let pargs = if dep then extended_rel_vect 0 deparsign
-	      else extended_rel_vect 1 arsign
-	      in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
-	    in it_mkProd_or_LetIn_name env
+	      let concl = 
+		let pargs = if dep then extended_rel_vect 0 deparsign
+		  else extended_rel_vect 1 arsign
+		in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
+	      in it_mkProd_or_LetIn_name env
 		concl
 		deparsign
 	    in
-	    mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp) 
-                 (deftyi::ldef) rest
+	      mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp) 
+                (deftyi::ldef) rest
         | [] -> 
 	    let fixn = Array.of_list (List.rev ln) in
             let fixtyi = Array.of_list (List.rev ltyp) in
             let fixdef = Array.of_list (List.rev ldef) in 
             let names = Array.create nrec (Name(id_of_string "F")) in
-	    mkFix ((fixn,p),(names,fixtyi,fixdef))
+	      mkFix ((fixn,p),(names,fixtyi,fixdef))
       in 
-	      mrec 0 [] [] [] 
+	mrec 0 [] [] [] 
     in 
     let rec make_branch env i = function 
       | (indi,mibi,mipi,dep,_)::rest ->
@@ -404,44 +403,46 @@ let mis_make_indrec env sigma listdepkind mib =
 		type_rec_branch
                   true dep env sigma (vargs,depPvec,i+j) tyi cs recarg
 	      in 
-	      mkLambda_string "f" p_0
-		(onerec (push_rel (Anonymous,None,p_0) env) (j+1))
+		mkLambda_string "f" p_0
+		  (onerec (push_rel (Anonymous,None,p_0) env) (j+1))
 	  in onerec env 0
       | [] -> 
 	  makefix i listdepkind
-    in 
+    in
     let rec put_arity env i = function 
       | (indi,_,_,dep,kinds)::rest -> 
 	  let indf = make_ind_family (indi,extended_rel_list i lnamesparrec) 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)
+	    mkLambda_string "P" typP
+	      (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
       | [] -> 
 	  make_branch env 0 listdepkind 
-    in 
-
-      (* Body on make_one_rec *)
+    in
+      
+    (* Body on make_one_rec *)
     let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
-
-    if mis_is_recursive_subset
-      (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
-      mipi.mind_recargs
-    then 
-    let env' = push_rel_context lnamesparrec env in
-      it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) 
-	lnamesparrec
-    else 
-      mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind 
+      
+      if (mis_is_recursive_subset
+	(List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
+	mipi.mind_recargs) 
+	(* mis_is_recursive_subset do not care about mutually recursive calls so: *)
+	|| (nparams-nparrec > 0)
+      then 
+	let env' = push_rel_context lnamesparrec env in
+	  it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) 
+	    lnamesparrec
+      else 
+	mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind 
   in 
-      (* Body of mis_make_indrec *)
-  list_tabulate make_one_rec nrec
+    (* Body of mis_make_indrec *)
+    list_tabulate make_one_rec nrec
 
 (**********************************************************************)
 (* This builds elimination predicate for Case tactic *)
 
 let make_case_com depopt env sigma ity kind =
   let (mib,mip) = lookup_mind_specif env ity in 
-  mis_make_case_com depopt env sigma ity (mib,mip) kind
+    mis_make_case_com depopt env sigma ity (mib,mip) kind
 
 let make_case_dep env   = make_case_com (Some true) env
 let make_case_nodep env = make_case_com (Some false) env 
@@ -460,7 +461,7 @@ let change_sort_arity sort =
     | Sort _ -> mkSort sort
     | _ -> assert false
   in 
-  drec 
+    drec 
 
 (* [npar] is the number of expected arguments (then excluding letin's) *)
 let instantiate_indrec_scheme sort =
@@ -536,7 +537,7 @@ let build_indrec env sigma ind =
   let (mib,mip) = lookup_mind_specif env ind in
   let kind = inductive_sort_family mip in
   let dep = kind <> InProp in
-  List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
+    List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
 
 (**********************************************************************)
 (* To handle old Case/Match syntax in Pretyping                       *)