Les params d'inductif deviennent en même temps propre à chaque inductif d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing

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

2 files changed, 61 insertions, 31 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index caa6d05d67..41085d3508 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -155,13 +155,21 @@ let build_mutual lparams lnamearconstrs finite =
 	 (Environ.push_rel_assum (Name id,p) env, (Name id,p)::params))
       (env0,[]) lparams
   in
+  (* Pour permettre à terme les let-in dans les params *)
+  let params' =
+    List.map (fun (na,p) ->
+		let id = match na with
+		  | Name id -> id
+		  | Anonymous -> anomaly "Unnamed inductive variable"
+		in (id, LocalAssum p)) params
+  in
   let (ind_env,arityl) =
     List.fold_left
       (fun (env,arl) (recname,arityc,_) ->
          let arity = interp_type sigma env_params arityc in
 	 let fullarity = prod_it arity params in
 	 let env' = Environ.push_rel_assum (Name recname,fullarity) env in
-	 (env', (fullarity::arl)))
+	 (env', (arity::arl)))
       (env0,[]) lnamearconstrs
   in
   let ind_env_params = Environ.push_rels_assum params ind_env in
@@ -169,17 +177,16 @@ let build_mutual lparams lnamearconstrs finite =
     List.map2
       (fun ar (name,_,lname_constr) ->
 	 let constrnames, bodies = List.split lname_constr in
-         let constrs =
-	   List.map
-	     (fun c -> prod_it (interp_constr sigma ind_env_params c) params)
-	     bodies
-	 in (name, ar, constrnames, constrs))
+         let constrs = List.map (interp_constr sigma ind_env_params) bodies in
+	 { mind_entry_nparams = nparams;
+	   mind_entry_params = params';
+	   mind_entry_typename = name;
+	   mind_entry_arity = ar;
+	   mind_entry_consnames = constrnames;
+	   mind_entry_lc = constrs })
       (List.rev arityl) lnamearconstrs
   in
-  let mie = { 
-    mind_entry_nparams = nparams;
-    mind_entry_finite = finite;
-    mind_entry_inds = mispecvec }
+  let mie = { mind_entry_finite = finite; mind_entry_inds = mispecvec }
   in
   let sp = declare_mind mie in
   if is_verbose() then pPNL(minductive_message lrecnames);
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 25b1383c35..b90f7e4935 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -43,21 +43,21 @@ let abstract_inductive ids_to_abs hyps inds =
       list_tabulate (fun k -> applist(mkRel (k+2),[mkRel 1])) ntyp in
     let inds' =
       List.map
-      	(function (tname,arity,cnames,lc) -> 
+      	(function (np,tname,arity,cnames,lc) -> 
 	   let arity' = mkNamedProd id t arity in
 	   let lc' =
 	     List.map (fun b -> mkNamedProd id t (substl new_refs b)) lc
 	   in
-           (tname,arity',cnames,lc'))
+           (np,tname,arity',cnames,lc'))
       	inds
     in 
     (inds',ABSTRACT) in
   let abstract_one_def id c inds =
     List.map
-      (function (tname,arity,cnames,lc) -> 
+      (function (np,tname,arity,cnames,lc) -> 
 	 let arity' = replace_vars [id, c] arity in
 	 let lc' = List.map (replace_vars [id, c]) lc in
-         (tname,arity',cnames,lc'))
+         (np,tname,arity',cnames,lc'))
       inds in
   let abstract_once ((hyps,inds,modl) as sofar) id =
     match hyps with
@@ -73,7 +73,24 @@ let abstract_inductive ids_to_abs hyps inds =
     List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
   let inds'' =
     List.map 
-      (fun (a,b,c,d) -> (a,body_of_type b,c,List.map body_of_type d))
+      (fun (nparams,a,arity,c,lc) ->
+	 let nparams' = nparams + (List.length revmodl) in
+	 let params, short_arity = decompose_prod_n_assum nparams' arity in
+	 let shortlc =
+	   List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in
+	 let params' =
+	   List.map 
+	     (function
+		| (Name id,None,p) -> id, LocalAssum p
+		| (Name id,Some p,_) -> id, LocalDef p
+		| (Anonymous,_,_) -> anomaly"Unnamed inductive local variable")
+	     params in
+	 { mind_entry_nparams = nparams';
+	   mind_entry_params = params';
+	   mind_entry_typename = a;
+	   mind_entry_arity = short_arity;
+	   mind_entry_consnames = c;
+	   mind_entry_lc = shortlc })
       inds' in
   (inds'', List.rev revmodl)
 
@@ -83,11 +100,14 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
   let inds = 
     array_map_to_list
       (fun mip ->
-	 (mip.mind_typename,
-	  expmod_type oldenv modlist (mind_user_arity mip),
+	 let nparams = mip.mind_nparams in
+	 let arity = expmod_type oldenv modlist (mind_user_arity mip) in
+	 let lc = Array.map (expmod_type oldenv modlist) (mind_user_lc mip) in
+	 (nparams,
+	  mip.mind_typename,
+	  arity,
 	  Array.to_list mip.mind_consnames,
-	  Array.to_list
-	    (Array.map (expmod_type oldenv modlist) (mind_user_lc mip))))
+	  Array.to_list lc))
       mib.mind_packets
   in
   let hyps' = map_named_context (expmod_constr oldenv modlist) mib.mind_hyps in
@@ -103,8 +123,7 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
   in
   let indmodifs,cstrmodifs =
     List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in 
-  ({ mind_entry_nparams = mib.mind_nparams + (List.length modl);
-     mind_entry_finite = finite;
+  ({ mind_entry_finite = finite;
      mind_entry_inds = inds' },
    indmodifs,
    List.flatten cstrmodifs)
@@ -116,13 +135,16 @@ let constant_message id =
 
 let inductive_message inds =
   if Options.is_verbose() then 
-    pPNL (hOV 0 
-	    (match inds with
-	       | [] -> assert false
-	       | [(i,_,_,_)] -> [< pr_id i; 'sTR " is discharged." >]
-	       | l -> [< prlist_with_sep pr_coma 
-			   (fun (id,_,_,_) -> pr_id id) l;
-			 'sPC; 'sTR "are discharged.">]))
+    pPNL
+      (hOV 0 
+	 (match inds with
+	    | [] -> assert false
+	    | [ind] ->
+		[< pr_id ind.mind_entry_typename; 'sTR " is discharged." >]
+	    | l ->
+		[< prlist_with_sep pr_coma 
+		     (fun ind -> pr_id ind.mind_entry_typename) l;
+		   'sPC; 'sTR "are discharged.">]))
 
 (* Discharge operations for the various objects of the environment. *)
 
@@ -213,7 +235,7 @@ let process_object oldenv dir sec_sp
 	let mib = Environ.lookup_mind sp oldenv in
 	let strobj =
 	  { s_CONST = info.s_CONST;
-	    s_PARAM = mib.mind_nparams;
+	    s_PARAM = (mind_nth_type_packet mib 0).mind_nparams;
 	    s_PROJ = List.map (option_app (recalc_sp dir)) info.s_PROJ } in
 	((Struc ((newsp,i),strobj))::ops, ids_to_discard, work_alist)
 
@@ -254,7 +276,8 @@ let process_operation = function
 let push_inductive_names ccitab sp mie =
   let _,ccitab =
     List.fold_left
-      (fun (n,ccitab) (id,_,cnames,_) ->
+      (fun (n,ccitab) ind ->
+	 let id = ind.mind_entry_typename in
 	 let indsp = (sp,n) in
 	 let _,ccitab =
 	   List.fold_left
@@ -263,7 +286,7 @@ let push_inductive_names ccitab sp mie =
 		 Stringmap.add (string_of_id x) (ConstructRef (indsp,p)) 
 		   ccitab))
 	     (1,Stringmap.add (string_of_id id) (IndRef indsp) ccitab)
-	     cnames in
+	     ind.mind_entry_consnames in
 	 (n+1,ccitab))
       (0,ccitab)
       mie.mind_entry_inds