Changement de subst_meta

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

6 files changed, 86 insertions, 9 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index b444baa8d..620f31eaa 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -45,7 +45,7 @@ let mis_finite mis = mis.mis_mip.mind_finite
 
 let mis_typed_nf_lc mis =
   let sign = mis.mis_mib.mind_hyps in
-  let args = Array.to_list mis.mis_args in
+(*  let args = Array.to_list mis.mis_args in *)
   Array.map (fun t -> (* Instantiate.instantiate_type sign*) t (*args*))
     mis.mis_mip.mind_nf_lc
 
@@ -53,7 +53,13 @@ let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis)
 
 let mis_user_lc mis = 
   let sign = mis.mis_mib.mind_hyps in
+(*i
+  let at = mind_user_lc mis.mis_mip in 
+  if Array.length mis.mis_args = 0 then at
+  else 
   let args = Array.to_list mis.mis_args in
+  Array.map (fun t -> Instantiate.instantiate_constr sign t args) at
+i*)
   Array.map (fun t -> (*Instantiate.instantiate_type sign*) t (*args*))
     (mind_user_lc mis.mis_mip)
 
@@ -61,6 +67,17 @@ let mis_user_lc mis =
    types of constructors of an inductive definition 
    correctly instanciated *)
 
+let mis_type_mconstructs mispec =
+  let specif = Array.map body_of_type (mis_user_lc mispec)
+  and ntypes = mis_ntypes mispec
+  and nconstr = mis_nconstr mispec in
+  let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) 
+  and make_Ck k = mkMutConstruct
+		    (((mispec.mis_sp,mispec.mis_tyi),k+1),
+		       mispec.mis_args) in
+  (Array.init nconstr make_Ck, 
+   Array.map (substl (list_tabulate make_Ik ntypes)) specif)
+
 let mis_nf_constructor_type i mispec =
   let specif = mis_nf_lc mispec
   and ntypes = mis_ntypes mispec
@@ -79,12 +96,15 @@ let mis_constructor_type i mispec =
 
 let mis_arity mis =
   let hyps = mis.mis_mib.mind_hyps 
-  and largs = Array.to_list mis.mis_args in
-  Instantiate.instantiate_type hyps (mind_user_arity mis.mis_mip) largs
+  in let ar = mind_user_arity mis.mis_mip
+  in if Array.length mis.mis_args = 0 then ar
+    else let largs = Array.to_list mis.mis_args in
+      Instantiate.instantiate_type hyps ar largs
 
 let mis_nf_arity mis =
   let hyps = mis.mis_mib.mind_hyps 
-  and largs = Array.to_list mis.mis_args in
+  in if Array.length mis.mis_args = 0 then mis.mis_mip.mind_nf_arity
+    else let largs = Array.to_list mis.mis_args in
   Instantiate.instantiate_type hyps mis.mis_mip.mind_nf_arity largs
 
 let mis_params_ctxt mis = mis.mis_mip.mind_params_ctxt
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 1414196f3..9b083293a 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -13,6 +13,7 @@ open Environ
 
 val instantiate_constr : 
   section_context -> constr -> constr list -> constr
+
 val instantiate_type : 
   section_context -> types -> constr list -> types
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 43a671536..18e3d2c32 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -840,6 +840,13 @@ let fconv cv_pb env sigma t1 t2 =
 let conv env = fconv CONV env
 let conv_leq env = fconv CONV_LEQ env 
 
+let convleqkey = Profile.declare_profile "conv_leq";;
+let conv_leq env sigma t1 t2 = Profile.profile4 convleqkey conv_leq env sigma t1 t2;;
+
+
+let convkey = Profile.declare_profile "conv";;
+let conv env sigma t1 t2 = Profile.profile4 convleqkey conv env sigma t1 t2;;
+
 let conv_forall2 f env sigma v1 v2 =
   array_fold_left2 
     (fun c x y -> let c' = f env sigma x y in Constraint.union c c')
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 72e9bfd1a..f98ee5bdd 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -75,7 +75,7 @@ let rec execute mf env cstr =
         let (larjv,vdefv,cst) = execute_fix mf env lar lfi vdef in
 	let larv = Array.map body_of_type larjv in
         let fix = (vni,(larv,lfi,vdefv)) in
-        check_fix env Evd.empty fix;
+        if not mf.fix then check_fix env Evd.empty fix;
 	(make_judge (mkFix fix) larjv.(i), cst)
 	  
     | IsCoFix (i,(lar,lfi,vdef)) ->
diff --git a/kernel/term.ml b/kernel/term.ml
index f942fe178..d75bea008 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -940,6 +940,11 @@ let substn_many lamv n =
   in 
   substrec n
 
+(*
+let substkey = Profile.declare_profile "substn_many";;
+let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;;
+*)
+
 let substnl laml k =
   substn_many (Array.map make_substituend (Array.of_list laml)) k
 let substl laml =
@@ -973,6 +978,11 @@ let replace_vars var_alist =
   in 
   if var_alist = [] then (function x -> x) else substrec 0
 
+(*
+let repvarkey = Profile.declare_profile "replace_vars";;
+let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;;
+*)
+
 (* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
 let subst_var str = replace_vars [(str, mkRel 1)]
 
@@ -1561,7 +1571,7 @@ let subst_term_eta = subst_term_gen eta_eq_constr
 (* Et puis meta doit fusionner avec Evar *)
 let rec subst_meta bl c = 
   match kind_of_term c with
-    | IsMeta i -> List.assoc i bl
+    | IsMeta i -> (try List.assoc i bl with Not_found -> c)
     | _ -> map_constr (subst_meta bl) c
 
 (* Substitute only a list of locations locs, the empty list is
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index fa3db0b86..da0266752 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -26,6 +26,10 @@ let assumption_of_judgment env sigma j =
     | IsSort s -> j.uj_val
     | _ -> error_assumption CCI env j.uj_val
 
+let aojkey = Profile.declare_profile "assumption_of_judgment";;
+let assumption_of_judgment env sigma j
+  = Profile.profile3 aojkey assumption_of_judgment env sigma j;;
+
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env sigma j =
   match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with
@@ -42,6 +46,9 @@ let relative env sigma n =
   with Not_found -> 
     error_unbound_rel CCI env sigma n
 
+let relativekey = Profile.declare_profile "relative";;
+let relative env sigma n = Profile.profile3 relativekey relative env sigma n;;
+
 (* Management of context of variables. *)
 
 (* Checks if a context of variable is included in another one. *)
@@ -76,12 +83,20 @@ let check_hyps id env sigma hyps =
 
 let type_of_constant = Instantiate.constant_type
 
+let tockey = Profile.declare_profile "type_of_constant";;
+let type_of_constant env sigma c 
+  = Profile.profile3 tockey type_of_constant env sigma c;;
+
 (* Inductive types. *)
 
 let type_of_inductive env sigma i =
   (* TODO: check args *)
   mis_arity (lookup_mind_specif i env)
 
+let toikey = Profile.declare_profile "type_of_inductive";;
+let type_of_inductive env sigma i
+  = Profile.profile3 toikey type_of_inductive env sigma i;;
+
 (* Constructors. *)
 
 let type_of_constructor env sigma cstr =
@@ -89,6 +104,11 @@ let type_of_constructor env sigma cstr =
     (index_of_constructor cstr) 
     (lookup_mind_specif (inductive_of_constructor cstr) env)
 
+let tockey = Profile.declare_profile "type_of_constructor";;
+let type_of_constructor env sigma cstr
+  = Profile.profile3 tockey type_of_constructor env sigma cstr;;
+
+
 let type_of_existential env sigma ev =
   Instantiate.existential_type sigma ev
 
@@ -198,6 +218,10 @@ let type_of_case env sigma ci pj cj lfj =
   { uj_val  = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
     uj_type = rslty }
 
+let tocasekey = Profile.declare_profile "type_of_case";;
+let type_of_case env sigma ci pj cj lfj
+  = Profile.profile6 tocasekey type_of_case env sigma ci pj cj lfj;;
+
 (* Prop and Set *)
 
 let judge_of_prop =
@@ -313,6 +337,9 @@ let apply_rel_list env sigma nocheck argjl funj =
   in 
   apply_rec 1 (body_of_type funj.uj_type) Constraint.empty argjl
 
+let applykey = Profile.declare_profile "apply_rel_list";;
+let apply_rel_list env sigma nocheck argjl funj
+  = Profile.profile5 applykey apply_rel_list env sigma nocheck argjl funj;;
 
 (* Fixpoints. *)
 
@@ -507,7 +534,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
      (* n gives the index of the recursive variable *)
      (noccur_with_meta (n+k+1) nfi t) or 
      (* no recursive call in the term *)
-     (let f,l = whd_betadeltaiota_stack env sigma t in
+     (let f,l = whd_betaiota_stack t in
       match kind_of_term f with
 	| IsRel p -> 
 	    if n+k+1 <= p & p < n+k+nfi+1 then
@@ -590,12 +617,16 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	       (n+1) (map_lift_fst lst) b) &&
             (List.for_all (check_rec_call env n lst) l)
 
-	| IsLetIn (x,a,b,c) -> 
+	| IsLetIn (x,a,b,c) as cst -> 
+	    (try 
 	    (check_rec_call env n lst a) &&
 	    (check_rec_call env n lst b) &&
             (check_rec_call (push_rel_def (x,a, b) env)
 	       (n+1) (map_lift_fst lst) c) &&
             (List.for_all (check_rec_call env n lst) l)
+	    with (FixGuardError NotEnoughArgumentsForFixCall) as e
+		-> check_rec_call env n lst (whd_betadeltaiota env sigma t)
+            )
 
 	| IsMutInd (_,la) -> 
 	     (array_for_all (check_rec_call env n lst) la) &&
@@ -605,9 +636,14 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	     (array_for_all (check_rec_call env n lst) la) &&
              (List.for_all (check_rec_call env n lst) l)
 
-	| IsConst (_,la) -> 
+	| IsConst (sp,la) as c -> 
+            (try 
 	    (array_for_all (check_rec_call env n lst) la) &&
             (List.for_all (check_rec_call env n lst) l)
+	     with (FixGuardError _ ) as e
+		 -> if evaluable_constant env sp then 
+		   check_rec_call env n lst (whd_betadeltaiota env sigma t)
+		    else raise e)
 
 	| IsApp (f,la) -> 
 	    (check_rec_call env n lst f) &&
@@ -673,6 +709,9 @@ let check_fix env sigma ((nvect,bodynum),(types,names,bodies as recdef)) =
       error_ill_formed_rec_body	CCI env err (List.rev names) i bodies
   done 
 
+let cfkey = Profile.declare_profile "check_fix";;
+let check_fix env sigma fix = Profile.profile3 cfkey check_fix env sigma fix;;
+
 (* Co-fixpoints. *)
 
 exception CoFixGuardError of guard_error