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

1 files changed, 81 insertions, 34 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f35b1b10b6..4d6af242be 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -14,6 +14,7 @@ open Term
 open Environ
 open Type_errors
 open Rawterm
+open Inductive
 
 type ml_case_error =
   | MlCaseAbsurd
@@ -21,7 +22,7 @@ type ml_case_error =
 
 type pretype_error =
   (* Old Case *)
-  | MlCase of ml_case_error
+  | MlCase of ml_case_error * inductive_type * unsafe_judgment
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of int * constr
@@ -33,58 +34,104 @@ type pretype_error =
 
 exception PretypeError of env * pretype_error
 
-let raise_pretype_error (loc,ctx,te) =
-  Stdpp.raise_with_loc loc (PretypeError(ctx,te))
+(* Replacing defined evars for error messages *)
+let rec whd_evar sigma c =
+  match kind_of_term c with
+    | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
+	whd_evar sigma (Instantiate.existential_value sigma (ev,args))
+    | _ -> collapse_appl c
 
-let raise_located_type_error (loc,k,ctx,te) =
-  Stdpp.raise_with_loc loc (TypeError(k,ctx,te))
+let nf_evar sigma = Reduction.local_strong (whd_evar sigma)
+let j_nf_evar sigma j = 
+  { uj_val = nf_evar sigma j.uj_val;
+    uj_type = nf_evar sigma j.uj_type }
+let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
+let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
+let tj_nf_evar sigma {utj_val=v;utj_type=t} =
+  {utj_val=type_app (nf_evar sigma) v;utj_type=t}
 
-let error_cant_find_case_type_loc loc env expr =
-  raise_pretype_error (loc, env, CantFindCaseType expr)
 
-let error_ill_formed_branch_loc loc k env c i actty expty =
-  raise_located_type_error (loc, k, env, IllFormedBranch (c,i,actty,expty))
+let env_ise sigma env =
+  map_context (nf_evar sigma) env
 
-let error_actual_type_loc loc env c actty expty =
-  raise_located_type_error (loc, CCI, env, ActualType (c,actty,expty))
 
-let error_cant_apply_not_functional_loc loc env rator randl =
+let raise_pretype_error (loc,ctx,sigma,te) =
+  Stdpp.raise_with_loc loc (PretypeError(env_ise sigma ctx,te))
+
+let raise_located_type_error (loc,k,ctx,sigma,te) =
+  Stdpp.raise_with_loc loc (TypeError(k,env_ise sigma ctx,te))
+
+
+let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
+  raise_located_type_error
+    (loc, CCI, env, sigma,
+     ActualType (c,nf_evar sigma actty, nf_evar sigma expty))
+
+let error_cant_apply_not_functional_loc loc env sigma rator randl =
+  raise_located_type_error
+    (loc, CCI, env, sigma,
+    CantApplyNonFunctional (j_nf_evar sigma rator, jl_nf_evar sigma randl))
+
+let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
   raise_located_type_error
-    (loc,CCI,env, CantApplyNonFunctional (rator,randl))
+    (loc, CCI, env, sigma,
+     CantApplyBadType
+       ((n,nf_evar sigma c, nf_evar sigma t),
+        j_nf_evar sigma rator, jl_nf_evar sigma randl))
 
-let error_cant_apply_bad_type_loc loc env t rator randl =
-  raise_located_type_error (loc, CCI, env, CantApplyBadType (t,rator,randl))
+let error_cant_find_case_type_loc loc env sigma expr =
+  raise_pretype_error
+    (loc, env, sigma, CantFindCaseType (nf_evar sigma expr))
 
-let error_ill_formed_branch k env c i actty expty =
-  raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty)))
+let error_ill_formed_branch_loc loc k env sigma c i actty expty =
+  let simp t = Reduction.nf_betaiota (nf_evar sigma t) in
+  raise_located_type_error
+    (loc, k, env, sigma,
+     IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty))
 
-let error_number_branches_loc loc k env c ct expn =
-  raise_located_type_error (loc, k, env, NumberBranches (c,ct,expn))
+let error_number_branches_loc loc k env sigma cj expn =
+  raise_located_type_error
+    (loc, k, env, sigma,
+     NumberBranches (j_nf_evar sigma cj, expn))
 
-let error_case_not_inductive_loc loc k env c ct =
-  raise_located_type_error (loc, k, env, CaseNotInductive (c,ct))
+let error_case_not_inductive_loc loc k env sigma cj =
+  raise_located_type_error
+    (loc, k, env, sigma, CaseNotInductive (j_nf_evar sigma cj))
 
+let error_ill_typed_rec_body_loc loc k env sigma i na jl tys =
+  raise_located_type_error
+    (loc, k, env, sigma,
+     IllTypedRecBody (i,na,jv_nf_evar sigma jl,
+                      Array.map (nf_evar sigma) tys))
 
-(*s Implicit arguments synthesis errors *)
+(*s Implicit arguments synthesis errors. It is hard to find
+    a precise location. *)
 
-let error_occur_check env ev c =
-  raise (PretypeError (env, OccurCheck (ev,c)))
+let error_occur_check env sigma ev c =
+  let c = nf_evar sigma c in
+  raise (PretypeError (env_ise sigma env, OccurCheck (ev,c)))
 
-let error_not_clean env ev c =
-  raise (PretypeError (env, NotClean (ev,c)))
+let error_not_clean env sigma ev c =
+  let c = nf_evar sigma c in
+  raise (PretypeError (env_ise sigma env, NotClean (ev,c)))
 
 (*s Ml Case errors *)
 
-let error_ml_case_loc loc env mes =
-  raise_pretype_error (loc, env, MlCase mes)
+let error_ml_case_loc loc env sigma mes indt j =
+  raise_pretype_error
+    (loc, env, sigma, MlCase (mes, indt, j_nf_evar sigma j))
 
 (*s Pretyping errors *)
 
-let error_var_not_found_loc loc s =
-  raise_pretype_error (loc, Global.env() (*bidon*), VarNotFound s)
+let error_unexpected_type_loc loc env sigma actty expty =
+  raise_pretype_error
+    (loc, env, sigma,
+     UnexpectedType (nf_evar sigma actty, nf_evar sigma expty))
+
+let error_not_product_loc loc env sigma c =
+  raise_pretype_error (loc, env, sigma, NotProduct (nf_evar sigma c))
 
-let error_unexpected_type_loc loc env actty expty =
-  raise_pretype_error (loc, env, UnexpectedType (actty, expty))
+(*s Error in conversion from AST to rawterms *)
 
-let error_not_product_loc loc env c =
-  raise_pretype_error (loc, env, NotProduct c)
+let error_var_not_found_loc loc s =
+  raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s)