parametres inductifs

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

3 files changed, 49 insertions, 22 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 67a0f850cc..218d7f8228 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -353,7 +353,8 @@ let array_min nmr a = if nmr = 0 then 0 else
 (* The recursive function that checks positivity and builds the list
    of recursive arguments *)
 let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
-  let nparams = rel_context_length hyps in
+  let lparams = rel_context_length hyps in
+  let nmr = rel_context_nhyps hyps in
   (* check the inductive types occur positively in [c] *)
   let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = 
     let x,largs = decompose_app (whd_betadeltaiota env c) in
@@ -453,31 +454,32 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
      Array.map
       (fun c ->
         let c = body_of_type c in
-        let sign, rawc = mind_extract_params nparams c in
+        let sign, rawc = mind_extract_params lparams c in
         try
-	  check_constructors ienv true nparams rawc
+	  check_constructors ienv true nmr rawc
         with IllFormedInd err -> 
-	  explain_ind_err (ntypes-i) env nparams c err)
+	  explain_ind_err (ntypes-i) env lparams c err)
       indlc
   in
   let irecargs = Array.map snd irecargs_nmr
-  and nmr' = array_min nparams irecargs_nmr
+  and nmr' = array_min nmr irecargs_nmr
   in (nmr', mk_paths (Mrec i) irecargs)
 
 let check_positivity env_ar params inds =
   let ntypes = Array.length inds in
   let lra_ind =
     List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in
-  let nparams = rel_context_length params in
+  let lparams = rel_context_length params in
+  let nmr = rel_context_nhyps params in
   let check_one i (_,_,_,_,_,lc) =
     let ra_env =
-      list_tabulate (fun _ -> (Norec,mk_norec)) nparams @ lra_ind in
-    let ienv = (env_ar, 1+nparams, ntypes, ra_env) in
+      list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
+    let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
     check_positivity_one ienv params i lc 
   in
   let irecargs_nmr = Array.mapi check_one inds in 
   let irecargs = Array.map snd irecargs_nmr
-  and nmr' = array_min nparams irecargs_nmr
+  and nmr' = array_min nmr irecargs_nmr
   in (nmr',Rtree.mk_rec irecargs)
 
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 235c82b1a8..b5d825e843 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -152,11 +152,16 @@ let get_arity mib mip params =
   let arity = mip.mind_nf_arity in
   destArity (full_inductive_instantiate mib params arity)
 
+let rel_list n m = 
+  let rec reln l p = 
+    if p>m then l else reln (mkRel(n+p)::l) (p+1)
+  in 
+  reln [] 1
+
 let build_dependent_inductive ind mib mip params =
-  let arsign,_ = get_arity mib mip params in
   let nrealargs = mip.mind_nrealargs in
   applist 
-    (mkInd ind, (List.map (lift nrealargs) params)@(local_rels arsign))
+    (mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
 
 
 (* This exception is local *)
@@ -166,6 +171,7 @@ let is_correct_arity env c pj ind mib mip params =
   let kelim = mip.mind_kelim in
   let arsign,s = get_arity mib mip params in
   let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in
+  let nrealargs = mip.mind_nrealargs in
   let rec srec env pt t u =
     let pt' = whd_betadeltaiota env pt in
     let t' = whd_betadeltaiota env t in
@@ -180,7 +186,9 @@ let is_correct_arity env c pj ind mib mip params =
           let ksort = match kind_of_term k with
             | Sort s -> family_of_sort s 
 	    | _ -> raise (LocalArity None) in
-	  let dep_ind = build_dependent_inductive ind mib mip params in
+
+	  let dep_ind = build_dependent_inductive ind mib mip params
+	  in 
           let univ =
             try conv env a1 dep_ind
             with NotConvertible -> raise (LocalArity None) in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index ea21efcc40..8cd3dc2c4a 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -26,6 +26,7 @@ open Type_errors
 open Indtypes (* pour les erreurs *)
 open Safe_typing
 open Nametab
+open Sign
 
 let make_prod_dep dep env = if dep then prod_name env else mkProd
 let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
@@ -244,12 +245,24 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
   in
   process_constr env 0 f (List.rev cstr.cs_args, recargs)
 
+
+(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k 
+   variables *)
+let context_chop k ctx = 
+  let rec chop_aux acc = function
+    | (0, l2) -> (List.rev acc, l2)
+    | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
+    | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
+    | (_, []) -> failwith "context_chop"
+  in chop_aux [] (k,ctx)
+
+
 (* Main function *)
 let mis_make_indrec env sigma listdepkind mib =
   let nparams = mib.mind_nparams in
   let nparrec = mib. mind_nparams_rec in
   let lnonparrec,lnamesparrec = 
-    list_chop (nparams-nparrec) mib.mind_params_ctxt in
+    context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let nrec = List.length listdepkind in
   let depPvec =
     Array.create mib.mind_ntypes (None : (bool * constr) option) in 
@@ -286,10 +299,10 @@ let mis_make_indrec env sigma listdepkind mib =
 	    let depind = build_dependent_inductive env indf in
 	    let deparsign = (Anonymous,None,depind)::arsign in
 	    
-	    let nonrecpar = nparams-nparrec in
-	    let nar = mipi.mind_nrealargs in
-	    let ndepar = nar + 1 in
-	    let dect = nonrecpar+ndepar+nrec+nbconstruct 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 *)
@@ -301,12 +314,12 @@ let mis_make_indrec env sigma listdepkind mib =
 	      let constrs = get_constructors env indf' in
 	      let fi = rel_vect (dect-i-nctyi) nctyi in
 	      let vecfi = Array.map 
-			    (fun f -> appvect (f,rel_vect ndepar nonrecpar))
+			    (fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
 			    fi 
 	      in
 	      array_map3
 		(make_rec_branch_arg env sigma 
-		   (nparrec,depPvec,ndepar+nonrecpar))
+		   (nparrec,depPvec,larsign))
                 vecfi constrs (dest_subterms recargsvec.(tyi)) 
 	    in
 
@@ -329,7 +342,7 @@ let mis_make_indrec env sigma listdepkind mib =
 
 	    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 
@@ -357,7 +370,7 @@ let mis_make_indrec env sigma listdepkind mib =
 		concl
 		deparsign
 	    in
-	    mrec (i+nctyi) (nar+nonrecpar::ln) (typtyi::ltyp) 
+	    mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp) 
                  (deftyi::ldef) rest
         | [] -> 
 	    let fixn = Array.of_list (List.rev ln) in
@@ -366,7 +379,7 @@ let mis_make_indrec env sigma listdepkind mib =
             let names = Array.create nrec (Name(id_of_string "F")) in
 	    mkFix ((fixn,p),(names,fixtyi,fixdef))
       in 
-      mrec 0 [] [] [] 
+	      mrec 0 [] [] [] 
     in 
     let rec make_branch env i = function 
       | (indi,mibi,mipi,dep,_)::rest ->
@@ -399,6 +412,8 @@ let mis_make_indrec env sigma listdepkind mib =
       | [] -> 
 	  make_branch env 0 listdepkind 
     in 
+
+      (* Body on make_one_rec *)
     let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
 
     if mis_is_recursive_subset
@@ -411,6 +426,7 @@ let mis_make_indrec env sigma listdepkind mib =
     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
 
 (**********************************************************************)
@@ -433,6 +449,7 @@ let change_sort_arity sort =
   let rec drec a = match kind_of_term a with
     | Cast (c,t) -> drec c 
     | Prod (n,t,c) -> mkProd (n, t, drec c)
+    | LetIn (n,b,t,c) -> mkLetIn (n,b, t, drec c)
     | Sort _ -> mkSort sort
     | _ -> assert false
   in