debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes

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

6 files changed, 54 insertions, 10 deletions

diff --git a/kernel/generic.ml b/kernel/generic.ml
index 6b38b72ff6..0484a801d5 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -337,7 +337,17 @@ let global_varsl l constr =
 let global_vars constr = global_varsl [] constr
 
 let global_vars_set constr = 
-  List.fold_left (fun s x -> Idset.add x s) Idset.empty (global_vars constr)
+  let rec filtrec acc = function
+    | VAR id             -> Idset.add id acc
+    | DOP1(oper,c)       -> filtrec acc c
+    | DOP2(oper,c1,c2)   -> filtrec (filtrec acc c1) c2
+    | DOPN(oper,cl)      -> Array.fold_left filtrec acc cl
+    | DOPL(oper,cl)      -> List.fold_left filtrec acc cl
+    | DLAM(_,c)          -> filtrec acc c
+    | DLAMV(_,v)         -> Array.fold_left filtrec acc v
+    | _                  -> acc
+  in 
+  filtrec Idset.empty constr
 
 (* alpha equality for generic terms : checks first if M and M' are equal,
    otherwise checks equality forgetting the name annotation of DLAM and DLAMV*)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a34c98832f..da9604699c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 open Util
+open Names
 open Generic
 open Term
 open Inductive
@@ -9,6 +10,7 @@ open Sign
 open Environ
 open Instantiate
 open Reduction
+open Typeops
 
 (* In the following, each time an [evar_map] is required, then [Evd.empty]
    is given, since inductive types are typed in an environment without 
@@ -49,7 +51,7 @@ type ill_formed_ind =
 exception IllFormedInd of ill_formed_ind
 
 let explain_ind_err ntyp lna nbpar c err = 
-  let (lpar,c') = decompose_prod_n nbpar c in
+  let (lpar,c') = mind_extract_params nbpar c in
   let env = (List.map fst lpar)@lna in
   match err with
     | NonPos kt -> 
@@ -94,7 +96,7 @@ let abstract_mind_lc env ntyps npars lc =
     in 
     Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lC
 
-let decomp_par n c = snd (decompose_prod_n n c)
+let decomp_par n c = snd (mind_extract_params n c)
       
 let listrec_mconstr env ntypes nparams i indlc =
   (* check the inductive types occur positively in C *)
@@ -267,10 +269,17 @@ let cci_inductive env env_ar kind nparams finite inds cst =
       mind_listrec = recargs;
       mind_finite = finite }
   in
+  let ids = 
+    List.fold_left 
+      (fun acc (_,ar,_,_,_,lc) -> 
+	 Idset.union (global_vars_set ar.body) 
+	   (Idset.union (global_vars_set lc) acc))
+      Idset.empty inds
+  in
   let packets = Array.of_list (list_map_i one_packet 1 inds) in
   { mind_kind = kind;
     mind_ntypes = ntypes;
-    mind_hyps = var_context env;
+    mind_hyps = keep_hyps (var_context env) ids;
     mind_packets = packets;
     mind_constraints = cst;
     mind_singl = None;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 433a2c1d95..5ab2886a97 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -121,7 +121,8 @@ let mind_check_names mie =
    declaration, and checks that they are all present (and all the same)
    for all the given types. *)
 
-let mind_extract_params = decompose_prod_n
+let mind_extract_params n c = 
+  let (l,c') = decompose_prod_n n c in (List.rev l,c')
   
 let extract nparams c =
   try mind_extract_params nparams c 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8f1ad37874..efa860fa2c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -280,11 +280,14 @@ let add_constant sp ce env =
 	  with NotConvertible -> 
 	    error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
   in
+  let ids = 
+    Idset.union (global_vars_set ce.const_entry_body) (global_vars_set ty.body)
+  in
   let cb = { 
     const_kind = kind_of_path sp;
     const_body = Some ce.const_entry_body;
     const_type = ty;
-    const_hyps = var_context env;
+    const_hyps = keep_hyps (var_context env) ids;
     const_constraints = Constraint.union cst cst';
     const_opaque = false } 
   in
@@ -293,11 +296,12 @@ let add_constant sp ce env =
 let add_parameter sp t env =
   let (jt,cst) = safe_machine env t in
   let env' = add_constraints cst env in
+  let ids = global_vars_set jt.uj_val in
   let cb = {
     const_kind = kind_of_path sp;
     const_body = None;
     const_type = assumption_of_judgment env' Evd.empty jt;
-    const_hyps = var_context env;
+    const_hyps = keep_hyps (var_context env) ids;
     const_constraints = cst;
     const_opaque = false } 
   in
@@ -333,7 +337,7 @@ let enforce_type_constructor env univ j cst =
     | _ -> error "Type of Constructor not well-formed"
 
 let type_one_constructor env_ar nparams ar c =
-  let (params,dc) = decompose_prod_n nparams c in
+  let (params,dc) = mind_extract_params nparams c in
   let env_par = push_rels params env_ar in
   let (jc,cst) = safe_machine env_par dc in
   let cst' = match sort_of_arity env_ar ar with
@@ -356,8 +360,10 @@ let logic_arity env c =
 let is_unit env_par nparams ar spec =
   match decomp_all_DLAMV_name spec with
     | (_,[|c|]) ->
-	(let (_,a) = decompose_prod_n nparams ar in logic_arity env_par ar) &&
-	(let (_,c') = decompose_prod_n nparams c in logic_constr env_par c')
+	(let (_,a) = mind_extract_params nparams ar in 
+	 logic_arity env_par ar) &&
+	(let (_,c') = mind_extract_params nparams c in 
+	 logic_constr env_par c')
     | _ -> false
 
 let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) =
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 255e8d7aa5..46dd750781 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -954,3 +954,19 @@ let control_only_guard env sigma =
     | DLAMV(_,v)    -> Array.iter control_rec v
   in 
   control_rec 
+
+(* [keep_hyps sign ids] keeps the part of the signature [sign] which 
+   contains the variables of the set [ids], and recursively the variables 
+   contained in the types of the needed variables. *)
+
+let keep_hyps sign needed =
+  rev_sign
+    (fst (it_sign 
+	    (fun ((hyps,globs) as sofar) id a ->
+               if Idset.mem id globs then
+                 (add_sign (id,a) hyps, 
+		  Idset.union (global_vars_set a.body) globs)
+               else 
+		 sofar) 
+	    (nil_sign,needed) sign))
+    
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 8a2974f6c8..9542dba9f8 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -90,3 +90,5 @@ val find_case_dep_nparams :
 val type_inst_construct : env -> 'a evar_map -> int -> constr -> constr 
 
 val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
+
+val keep_hyps : var_context -> Idset.t -> var_context