amelioration des messages d'erreurs vis a vis des evars

ajout automatique des chemins vers les sources au moment du Drop


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

9 files changed, 66 insertions, 118 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 2ad841d03..0a023fb9c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -110,7 +110,7 @@ let modify_opers replfun absfun (constl,indl,cstrl) =
 let expmod_constr oldenv modlist c =
   let sigma = Evd.empty in
   let simpfun = 
-    if modlist = ([],[],[]) then fun x -> x else nf_betaiota oldenv sigma in
+    if modlist = ([],[],[]) then fun x -> x else nf_betaiota in
   let expfun cst = 
     try 
       constant_value oldenv cst
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e67aff002..344ca87fb 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -165,7 +165,7 @@ let abstract_mind_lc env ntyps npars lc =
       list_tabulate
 	(function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps 
     in 
-    Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lc
+    Array.map (compose nf_beta (substl make_abs)) lc
 
 let listrec_mconstr env ntypes hyps nparams i indlc =
   let nhyps = List.length hyps in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 312ee83d2..5b602bfdc 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -81,9 +81,9 @@ let rec strong_prodspine redfun c =
 let clos_norm_flags flgs env sigma t =
   norm_val (create_clos_infos flgs env sigma) (inject t)
 
-let nf_beta env = clos_norm_flags beta env
-let nf_betaiota env = clos_norm_flags betaiota env
-let nf_betadeltaiota env =  clos_norm_flags betadeltaiota env
+let nf_beta = clos_norm_flags beta empty_env Evd.empty
+let nf_betaiota = clos_norm_flags betaiota empty_env Evd.empty
+let nf_betadeltaiota env sigma =  clos_norm_flags betadeltaiota env sigma
 
 (* lazy weak head reduction functions *)
 let whd_flags flgs env sigma t =
@@ -1088,43 +1088,3 @@ let is_info_type env sigma t =
   (s = Prop Pos) ||
   (s <> Prop Null && 
    try info_arity env sigma t.utj_val with IsType -> true)
-
-(* Expanding existential variables (pretyping.ml) *)
-(* 1- whd_ise fails if an existential is undefined *)
-
-exception Uninstantiated_evar of int
-
-let rec whd_ise sigma c =
-  match kind_of_term c with
-    | IsEvar (ev,args) when Evd.in_dom sigma ev ->
-	if Evd.is_defined sigma ev then
-          whd_ise sigma (existential_value sigma (ev,args))
-	else raise (Uninstantiated_evar ev)
-  | _ -> c
-
-
-(* 2- undefined existentials are left unchanged *)
-let rec whd_ise1 sigma c =
-  match kind_of_term c with
-    | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
-	whd_ise1 sigma (existential_value sigma (ev,args))
-    | _ -> collapse_appl c
-
-let nf_ise1 sigma = local_strong (whd_ise1 sigma)
-
-(* A form of [whd_ise1] with type "reduction_function" *)
-let whd_evar env = whd_ise1
-
-(* Expand evars, possibly in the head of an application *)
-let whd_castappevar_stack sigma c = 
-  let rec whrec (c, l as s) =
-    match kind_of_term c with
-      | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> 
-	  whrec (existential_value sigma (ev,args), l)
-      | IsCast (c,_) -> whrec (c, l)
-      | IsApp (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
-      | _ -> s
-  in 
-  whrec (c, [])
-
-let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index ae0640aef..a32f36a6a 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -58,8 +58,8 @@ val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a
 
 val clos_norm_flags : Closure.flags -> 'a reduction_function
 (* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) 
-val nf_beta : 'a reduction_function
-val nf_betaiota : 'a reduction_function
+val nf_beta : local_reduction_function
+val nf_betaiota : local_reduction_function
 val nf_betadeltaiota : 'a reduction_function
 
 (* Lazy strategy, weak head reduction *)
@@ -101,7 +101,6 @@ val whd_betadeltaeta : 'a reduction_function
 val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
 val whd_betadeltaiotaeta_state : 'a state_reduction_function
 val whd_betadeltaiotaeta : 'a reduction_function
-val whd_evar : 'a reduction_function
 
 val beta_applist : constr * constr list -> constr
 
@@ -192,16 +191,6 @@ val whd_meta : (int * constr) list -> constr -> constr
 val plain_instance : (int * constr) list -> constr -> constr
 val instance : (int * constr) list -> constr -> constr
 
-(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *)
-(* *[whd_ise1]* is synonymous of *[whd_evar empty_env]* and *[nf_ise1]* of *)
-(* *[strong whd_evar empty_env]*: they leave uninstantiated evar as it *)
-
-val whd_ise1 : 'a evar_map -> constr -> constr
-val nf_ise1 : 'a evar_map -> constr -> constr
-exception Uninstantiated_evar of int
-val whd_ise : 'a evar_map -> constr -> constr
-val whd_castappevar : 'a evar_map -> constr -> constr
-
 (*s Obsolete Reduction Functions *)
 
 (*i
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7df425894..d2887cce8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -90,7 +90,7 @@ let rec execute env cstr cu =
           (cast_rel env Evd.empty cj tj)
 
     | IsRel n -> 
-	(relative env Evd.empty n, cu)
+	(relative env n, cu)
 
     | IsVar id -> 
 	(make_judge cstr (lookup_named_type id env), cu)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 320a30369..05b6e2675 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -13,6 +13,7 @@ open Names
 open Term
 open Sign
 open Environ
+open Reduction
 
 (* Type errors. *)
 
@@ -39,10 +40,10 @@ type type_error =
   | NotAType of unsafe_judgment
   | BadAssumption of constr
   | ReferenceVariables of identifier
-  | ElimArity of inductive * constr list * constr * constr * constr
+  | ElimArity of inductive * constr list * constr * unsafe_judgment
       * (constr * constr * string) option
-  | CaseNotInductive of constr * constr
-  | NumberBranches of constr * constr * int
+  | CaseNotInductive of unsafe_judgment
+  | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * types) * unsafe_judgment
   | ActualType of constr * constr * constr
@@ -55,11 +56,11 @@ type type_error =
 
 exception TypeError of path_kind * env * type_error
 
-let env_ise sigma env =
-  map_context (Reduction.nf_ise1 sigma) env
+let nfj {uj_val=c;uj_type=ct} =
+  {uj_val=c;uj_type=nf_betaiota ct}
 
-let error_unbound_rel k env sigma n =
-  raise (TypeError (k, env_ise sigma env, UnboundRel n))
+let error_unbound_rel k env n =
+  raise (TypeError (k, env, UnboundRel n))
 
 let error_not_type k env c =
   raise (TypeError (k, env, NotAType c))
@@ -70,20 +71,21 @@ let error_assumption k env c =
 let error_reference_variables k env id =
   raise (TypeError (k, env, ReferenceVariables id))
 
-let error_elim_arity k env ind aritylst c p pt okinds = 
-  raise (TypeError (k, env, ElimArity (ind,aritylst,c,p,pt,okinds)))
+let error_elim_arity k env ind aritylst c pj okinds = 
+  raise (TypeError (k, env, ElimArity (ind,aritylst,c,pj,okinds)))
 
-let error_case_not_inductive k env c ct = 
-  raise (TypeError (k, env, CaseNotInductive (c,ct)))
+let error_case_not_inductive k env j = 
+  raise (TypeError (k, env, CaseNotInductive j))
 
-let error_number_branches k env c ct expn =
-  raise (TypeError (k, env, NumberBranches (c,ct,expn)))
+let error_number_branches k env cj expn =
+  raise (TypeError (k, env, NumberBranches (nfj cj,expn)))
 
 let error_ill_formed_branch k env c i actty expty =
-  raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty)))
+  raise (TypeError (k, env,
+    IllFormedBranch (c,i,nf_betaiota actty, nf_betaiota expty)))
 
-let error_generalization k env sigma nvar c =
-  raise (TypeError (k, env_ise sigma env, Generalization (nvar,c)))
+let error_generalization k env nvar c =
+  raise (TypeError (k, env, Generalization (nvar,c)))
 
 let error_actual_type k env c actty expty =
   raise (TypeError (k, env, ActualType (c,actty,expty)))
@@ -91,8 +93,8 @@ let error_actual_type k env c actty expty =
 let error_cant_apply_not_functional k env rator randl =
   raise (TypeError (k, env, CantApplyNonFunctional (rator,randl)))
 
-let error_cant_apply_bad_type k env sigma t rator randl =
-  raise(TypeError (k, env_ise sigma env, CantApplyBadType (t,rator,randl)))
+let error_cant_apply_bad_type k env t rator randl =
+  raise(TypeError (k, env, CantApplyBadType (t,rator,randl)))
 
 let error_ill_formed_rec_body k env why lna i vdefs =
   raise (TypeError (k, env, IllFormedRecBody (why,lna,i,vdefs)))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 277e5ca4e..11729171b 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -43,10 +43,10 @@ type type_error =
   | NotAType of unsafe_judgment
   | BadAssumption of constr
   | ReferenceVariables of identifier
-  | ElimArity of inductive * constr list * constr * constr * constr
+  | ElimArity of inductive * constr list * constr * unsafe_judgment
       * (constr * constr * string) option
-  | CaseNotInductive of constr * constr
-  | NumberBranches of constr * constr * int
+  | CaseNotInductive of unsafe_judgment
+  | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * types) * unsafe_judgment
   | ActualType of constr * constr * constr
@@ -59,44 +59,44 @@ type type_error =
 
 exception TypeError of path_kind * env * type_error
 
-val error_unbound_rel : path_kind -> env -> 'a Evd.evar_map -> int -> 'b
+val error_unbound_rel : path_kind -> env -> int -> 'a
 
-val error_not_type : path_kind -> env -> unsafe_judgment -> 'b
+val error_not_type : path_kind -> env -> unsafe_judgment -> 'a
 
-val error_assumption : path_kind -> env -> constr -> 'b
+val error_assumption : path_kind -> env -> constr -> 'a
  
-val error_reference_variables : path_kind -> env -> identifier -> 'b
+val error_reference_variables : path_kind -> env -> identifier -> 'a
 
 val error_elim_arity : 
   path_kind -> env -> inductive -> constr list -> constr 
-    -> constr -> constr -> (constr * constr * string) option -> 'b
+    -> unsafe_judgment -> (constr * constr * string) option -> 'a
 
 val error_case_not_inductive : 
-  path_kind -> env -> constr -> constr -> 'b
+  path_kind -> env -> unsafe_judgment -> 'a
 
 val error_number_branches : 
-  path_kind -> env -> constr -> constr -> int -> 'b
+  path_kind -> env -> unsafe_judgment -> int -> 'a
 
 val error_ill_formed_branch :
-  path_kind -> env -> constr -> int -> constr -> constr -> 'b
+  path_kind -> env -> constr -> int -> constr -> constr -> 'a
 
 val error_generalization :
-  path_kind -> env -> 'a Evd.evar_map -> name * types -> unsafe_judgment -> 'b
+  path_kind -> env -> name * types -> unsafe_judgment -> 'a
 
 val error_actual_type :
-  path_kind -> env -> constr -> constr -> constr -> 'b
+  path_kind -> env -> constr -> constr -> constr -> 'a
 
 val error_cant_apply_not_functional : 
-  path_kind -> env -> unsafe_judgment -> unsafe_judgment list -> 'b
+  path_kind -> env -> unsafe_judgment -> unsafe_judgment list -> 'a
 
 val error_cant_apply_bad_type : 
-  path_kind -> env -> 'a Evd.evar_map -> int * constr * constr -> 
-      unsafe_judgment -> unsafe_judgment list -> 'b
+  path_kind -> env -> int * constr * constr -> 
+      unsafe_judgment -> unsafe_judgment list -> 'a
 
 val error_ill_formed_rec_body :
-  path_kind -> env -> guard_error -> name array -> int -> constr array -> 'b
+  path_kind -> env -> guard_error -> name array -> int -> constr array -> 'a
 
 val error_ill_typed_rec_body  :
   path_kind -> env -> int -> name array -> unsafe_judgment array 
-    -> types array -> 'b
+    -> types array -> 'a
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 37106b200..ecbd59636 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -84,13 +84,13 @@ let type_of_sort c =
 
 (* Type of a de Bruijn index. *)
 	  
-let relative env sigma n = 
+let relative env n = 
   try
     let (_,typ) = lookup_rel_type n env in
     { uj_val  = mkRel n;
       uj_type = type_app (lift n) typ }
   with Not_found -> 
-    error_unbound_rel CCI env sigma n
+    error_unbound_rel CCI env n
 
 (*
 let relativekey = Profile.declare_profile "relative";;
@@ -206,7 +206,7 @@ let apply_rel_list env sigma nocheck argjl funj =
 		   let cst' = Constraint.union cst c in
 		   apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
 		 with NotConvertible -> 
-		   error_cant_apply_bad_type CCI env sigma
+		   error_cant_apply_bad_type CCI env
 		     (n,c1,body_of_type hj.uj_type)
 		     funj argjl)
 
@@ -289,7 +289,7 @@ let error_elim_expln env sigma kp ki =
 
 exception Arity of (constr * constr * string) option
 
-let is_correct_arity env sigma kelim (c,p) indf (pt,t) = 
+let is_correct_arity env sigma kelim (c,pj) indf t = 
   let rec srec (pt,t) u =
     let pt' = whd_betadeltaiota env sigma pt in
     let t' = whd_betadeltaiota env sigma t in
@@ -321,22 +321,22 @@ let is_correct_arity env sigma kelim (c,p) indf (pt,t) =
           else 
 	    raise (Arity (Some(pt',t',error_elim_expln env sigma pt' t')))
   in 
-  try srec (pt,t) Constraint.empty
+  try srec (pj.uj_type,t) Constraint.empty
   with Arity kinds ->
     let listarity =
       (List.map (make_arity env true indf) kelim)
       @(List.map (make_arity env false indf) kelim)
     in 
     let ind = mis_inductive (fst (dest_ind_family indf)) in
-    error_elim_arity CCI env ind listarity c p pt kinds
+    error_elim_arity CCI env ind listarity c pj kinds
 
 
-let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP =
+let find_case_dep_nparams env sigma (c,pj) (IndFamily (mis,_) as indf) =
   let kelim = mis_kelim mis in
   let arsign,s = get_arity indf in
   let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
   let ((dep,_),univ) =
-    is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in
+    is_correct_arity env sigma kelim (c,pj) indf glob_t in
   (dep,univ)
 
 (* type_case_branches type un <p>Case c of ... end 
@@ -346,8 +346,9 @@ let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP =
    attendus dans les branches du Case; lr est le type attendu du resultat
  *)
 
-let type_case_branches env sigma (IndType (indf,realargs)) pt p c =
-  let (dep,univ) = find_case_dep_nparams env sigma (c,p) indf pt in
+let type_case_branches env sigma (IndType (indf,realargs)) pj c =
+  let p = pj.uj_val in
+  let (dep,univ) = find_case_dep_nparams env sigma (c,pj) indf in
   let constructs = get_constructors indf in
   let lc = Array.map (build_branch_type env dep p) constructs in
   if dep then
@@ -355,17 +356,16 @@ let type_case_branches env sigma (IndType (indf,realargs)) pt p c =
   else 
     (lc, beta_applist (p,realargs), univ)
 
-let check_branches_message env sigma (c,ct) (explft,lft) = 
+let check_branches_message env sigma cj (explft,lft) = 
   let expn = Array.length explft and n = Array.length lft in
-  if n<>expn then error_number_branches CCI env c ct expn;
+  if n<>expn then error_number_branches CCI env cj expn;
   let univ = ref Constraint.empty in
   (for i = 0 to n-1 do
     try
       univ := Constraint.union !univ
         (conv_leq env sigma lft.(i) (explft.(i)))
     with NotConvertible ->
-      error_ill_formed_branch CCI env c i (nf_betaiota env sigma lft.(i))
-	(nf_betaiota env sigma explft.(i))
+      error_ill_formed_branch CCI env cj.uj_val i lft.(i) explft.(i)
   done;
   !univ)
 
@@ -373,14 +373,11 @@ let judge_of_case env sigma ci pj cj lfj =
   let lft = Array.map (fun j -> body_of_type j.uj_type) lfj in
   let indspec =
     try find_rectype env sigma (body_of_type cj.uj_type)
-    with Induc ->
-      error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in
+    with Induc -> error_case_not_inductive CCI env cj in
   let (bty,rslty,univ) =
-    type_case_branches env sigma indspec
-      (body_of_type pj.uj_type) pj.uj_val cj.uj_val in
+    type_case_branches env sigma indspec pj cj.uj_val in
   let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in
-  let univ' = check_branches_message env sigma
-    (cj.uj_val,body_of_type cj.uj_type) (bty,lft) in
+  let univ' = check_branches_message env sigma cj (bty,lft) in
   ({ uj_val  = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
      uj_type = rslty },
   Constraint.union univ univ')
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 3008c87cb..e4464fd89 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -39,7 +39,7 @@ val judge_of_prop_contents : contents -> unsafe_judgment
 val judge_of_type : universe -> unsafe_judgment * constraints
 
 (*s Type of atomic terms. *)
-val relative : env -> 'a evar_map -> int -> unsafe_judgment
+val relative : env -> int -> unsafe_judgment
 
 val type_of_constant : env -> 'a evar_map -> constant -> types
 
@@ -85,11 +85,11 @@ val judge_of_case : env -> 'a evar_map -> case_info
     -> unsafe_judgment array -> unsafe_judgment * constraints
 
 val find_case_dep_nparams :
-  env -> 'a evar_map -> constr * constr -> inductive_family -> constr
+  env -> 'a evar_map -> constr * unsafe_judgment -> inductive_family
     -> bool * constraints
 
 val type_case_branches :
-  env -> 'a evar_map -> Inductive.inductive_type -> constr -> types
+  env -> 'a evar_map -> Inductive.inductive_type -> unsafe_judgment
     -> constr -> types array * types * constraints
 
 (*s Type of fixpoints and guard condition. *)