Delayed the evar normalization in error messages to the last minute

before the message is delivered to the user. Should avoid useless
computation in heavily backtracking tactics (auto, try, ...).

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

3 files changed, 57 insertions, 75 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index eb07addb0..cd2ed76c1 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -38,8 +38,9 @@ type pretype_error =
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
   | NotProduct of constr
+  | TypingError of type_error
 
-exception PretypeError of env * pretype_error
+exception PretypeError of env * Evd.evar_map * pretype_error
 
 let precatchable_exception = function
   | Util.UserError _ | TypeError _ | PretypeError _
@@ -55,13 +56,13 @@ let j_nf_betaiotaevar sigma j =
   { uj_val = nf_evar sigma j.uj_val;
     uj_type = Reductionops.nf_betaiota sigma j.uj_type }
 let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
-let jl_nf_betaiotaevar sigma jl =
-  List.map (j_nf_betaiotaevar sigma) jl
+let jv_nf_betaiotaevar sigma jl =
+  Array.map (j_nf_betaiotaevar 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=nf_evar sigma v;utj_type=t}
 
-let env_ise sigma env =
+let env_nf_evar sigma env =
   let sign = named_context_val env in
   let ctxt = rel_context env in
   let env0 = reset_with_named_context sign env in
@@ -97,110 +98,90 @@ let contract2 env a b = match contract env [a;b] with
 let contract3 env a b c = match contract env [a;b;c] with
   | env, [a;b;c] -> env,a,b,c | _ -> assert false
 
-let raise_pretype_error (loc,ctx,sigma,te) =
-  Loc.raise loc (PretypeError(env_ise sigma ctx,te))
+let raise_pretype_error (loc,env,sigma,te) =
+  Loc.raise loc (PretypeError(env,sigma,te))
 
-let raise_located_type_error (loc,ctx,sigma,te) =
-  Loc.raise loc (TypeError(env_ise sigma ctx,te))
+let raise_located_type_error (loc,env,sigma,te) =
+  Loc.raise loc (PretypeError(env,sigma,TypingError te))
 
 
 let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
   let env, c, actty, expty = contract3 env c actty expty in
-  let j = j_nf_evar sigma {uj_val=c;uj_type=actty} in
-  raise_located_type_error
-    (loc, env, sigma, ActualType (j, nf_evar sigma expty))
+  let j = {uj_val=c;uj_type=actty} in
+  raise_located_type_error (loc, env, sigma, ActualType (j, expty))
 
 let error_cant_apply_not_functional_loc loc env sigma rator randl =
-  let ja = Array.of_list (jl_nf_evar sigma randl) in
   raise_located_type_error
-    (loc, env, sigma,
-    CantApplyNonFunctional (j_nf_evar sigma rator, ja))
+    (loc, env, sigma, CantApplyNonFunctional (rator, Array.of_list randl))
 
 let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
-  let ja = Array.of_list (jl_nf_betaiotaevar sigma randl) in
   raise_located_type_error
     (loc, env, sigma,
-     CantApplyBadType
-       ((n,nf_evar sigma c, Reductionops.nf_betaiota sigma t),
-        j_nf_evar sigma rator, ja))
+       CantApplyBadType ((n,c,t), rator, Array.of_list randl))
 
 let error_ill_formed_branch_loc loc env sigma c i actty expty =
-  let simp t = Reduction.nf_betaiota (nf_evar sigma t) in
   raise_located_type_error
-    (loc, env, sigma,
-     IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty))
+    (loc, env, sigma, IllFormedBranch (c, i, actty, expty))
 
 let error_number_branches_loc loc env sigma cj expn =
-  raise_located_type_error
-    (loc, env, sigma,
-     NumberBranches (j_nf_evar sigma cj, expn))
+  raise_located_type_error (loc, env, sigma, NumberBranches (cj, expn))
 
 let error_case_not_inductive_loc loc env sigma cj =
-  raise_located_type_error
-    (loc, env, sigma, CaseNotInductive (j_nf_evar sigma cj))
+  raise_located_type_error (loc, env, sigma, CaseNotInductive cj)
 
 let error_ill_typed_rec_body_loc loc env sigma i na jl tys =
   raise_located_type_error
-    (loc, env, sigma,
-     IllTypedRecBody (i,na,jv_nf_evar sigma jl,
-                      Array.map (nf_evar sigma) tys))
+    (loc, env, sigma, IllTypedRecBody (i, na, jl, tys))
 
 let error_not_a_type_loc loc env sigma j =
-  raise_located_type_error (loc, env, sigma, NotAType (j_nf_evar sigma j))
+  raise_located_type_error (loc, env, sigma, NotAType j)
 
 (*s Implicit arguments synthesis errors. It is hard to find
     a precise location. *)
 
 let error_occur_check env sigma ev c =
-  let c = nf_evar sigma c in
-  raise (PretypeError (env_ise sigma env, OccurCheck (ev,c)))
+  raise (PretypeError (env, sigma, OccurCheck (ev,c)))
 
 let error_not_clean env sigma ev c (loc,k) =
-  let c = nf_evar sigma c in
-  Loc.raise loc
-    (PretypeError (env_ise sigma env,  NotClean (ev,c,k)))
+  Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k)))
 
 let error_unsolvable_implicit loc env sigma evi e explain =
   Loc.raise loc
-    (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain)))
+    (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain)))
 
 let error_cannot_unify env sigma (m,n) =
-  let m = nf_evar sigma m and n = nf_evar sigma n in
-  raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+  raise (PretypeError (env, sigma,CannotUnify (m,n)))
 
 let error_cannot_unify_local env sigma (m,n,sn) =
-  raise (PretypeError (env_ise sigma env,CannotUnifyLocal (m,n,sn)))
+  raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn)))
 
 let error_cannot_coerce env sigma (m,n) =
-  raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+  raise (PretypeError (env, sigma,CannotUnify (m,n)))
 
 let error_cannot_find_well_typed_abstraction env sigma p l =
-  raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l)))
+  raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l)))
 
 let error_abstraction_over_meta env sigma hdmeta metaarg =
   let m = Evd.meta_name sigma hdmeta and n = Evd.meta_name sigma metaarg in
-  raise (PretypeError (env_ise sigma env,AbstractionOverMeta (m,n)))
+  raise (PretypeError (env, sigma,AbstractionOverMeta (m,n)))
 
 let error_non_linear_unification env sigma hdmeta t =
   let m = Evd.meta_name sigma hdmeta in
-  raise (PretypeError (env_ise sigma env,NonLinearUnification (m,t)))
+  raise (PretypeError (env, sigma,NonLinearUnification (m,t)))
 
 (*s Ml Case errors *)
 
 let error_cant_find_case_type_loc loc env sigma expr =
-  raise_pretype_error
-    (loc, env, sigma, CantFindCaseType (nf_evar sigma expr))
+  raise_pretype_error (loc, env, sigma, CantFindCaseType expr)
 
 (*s Pretyping errors *)
 
 let error_unexpected_type_loc loc env sigma actty expty =
   let env, actty, expty = contract2 env actty expty in
-  raise_pretype_error
-    (loc, env, sigma,
-     UnexpectedType (nf_evar sigma actty, nf_evar sigma expty))
+  raise_pretype_error (loc, env, sigma, UnexpectedType (actty, expty))
 
 let error_not_product_loc loc env sigma c =
-  raise_pretype_error (loc, env, sigma, NotProduct (nf_evar sigma c))
+  raise_pretype_error (loc, env, sigma, NotProduct c)
 
 (*s Error in conversion from AST to rawterms *)
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index d81adb6b0..cdf6b523c 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -37,47 +37,48 @@ type pretype_error =
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
   | NotProduct of constr
+  | TypingError of Type_errors.type_error
 
-exception PretypeError of env * pretype_error
+exception PretypeError of env * Evd.evar_map * pretype_error
 
 val precatchable_exception : exn -> bool
 
 (** Presenting terms without solved evars *)
-val nf_evar :  Evd.evar_map -> constr -> constr
-val j_nf_evar :  Evd.evar_map -> unsafe_judgment -> unsafe_judgment
-val jl_nf_evar :
-   Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_evar :
-   Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_evar :
-   Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+val nf_evar : Evd.evar_map -> constr -> constr
+val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
+val jl_nf_evar : Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
+val env_nf_evar : Evd.evar_map -> env -> env
+val jv_nf_betaiotaevar :
+  Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
 
 (** Raising errors *)
 val error_actual_type_loc :
-  loc -> env ->  Evd.evar_map -> unsafe_judgment -> constr -> 'b
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_cant_apply_bad_type_loc :
-  loc -> env ->  Evd.evar_map -> int * constr * constr ->
+  loc -> env -> Evd.evar_map -> int * constr * constr ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_case_not_inductive_loc :
-  loc -> env ->  Evd.evar_map -> unsafe_judgment -> 'b
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_ill_formed_branch_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       constr -> int -> constr -> constr -> 'b
 
 val error_number_branches_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       unsafe_judgment -> int -> 'b
 
 val error_ill_typed_rec_body_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       int -> name array -> unsafe_judgment array -> types array -> 'b
 
 val error_not_a_type_loc :
@@ -87,7 +88,7 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 
 (** {6 Implicit arguments synthesis errors } *)
 
-val error_occur_check : env ->  Evd.evar_map -> existential_key -> constr -> 'b
+val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_not_clean :
   env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b
@@ -112,15 +113,15 @@ val error_non_linear_unification : env -> Evd.evar_map ->
 (** {6 Ml Case errors } *)
 
 val error_cant_find_case_type_loc :
-  loc -> env ->  Evd.evar_map -> constr -> 'b
+  loc -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Pretyping errors } *)
 
 val error_unexpected_type_loc :
-  loc -> env ->  Evd.evar_map -> constr -> constr -> 'b
+  loc -> env -> Evd.evar_map -> constr -> constr -> 'b
 
 val error_not_product_loc :
-  loc -> env ->  Evd.evar_map -> constr -> 'b
+  loc -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Error in conversion from AST to rawterms } *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 38cf59bc0..6c17567c3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -844,7 +844,7 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
   in
   try matchrec cl
   with ex when precatchable_exception ex ->
-    raise (PretypeError (env,NoOccurrenceFound (op, None)))
+    raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
 
 (* Tries to find all instances of term [cl] in term [op].
    Unifies [cl] to every subterm of [op] and return all the matches.
@@ -906,7 +906,7 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
   in
   let res = matchrec cl [] in
   if res = [] then
-    raise (PretypeError (env,NoOccurrenceFound (op, None)))
+    raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
   else
     res
 
@@ -922,7 +922,7 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
           try
 	    (* This is up to delta for subterms w/o metas ... *)
 	    w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd
-	  with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
+	  with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op)
         in
 	  if not allow_K && (* ensure we found a different instance *)
 	    List.exists (fun op -> eq_constr op cl) l
@@ -932,7 +932,7 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
 	(evd,op::l)
       else
 	(* This is not up to delta ... *)
-	raise (PretypeError (env,NoOccurrenceFound (op, None))))
+	raise (PretypeError (env,evd,NoOccurrenceFound (op, None))))
     oplist
     (evd,[])
 
@@ -996,13 +996,13 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
 	    with ex when precatchable_exception ex ->
 	      try
 		w_unify2 env flags allow_K cv_pb ty1 ty2 evd
-	      with PretypeError (env,NoOccurrenceFound _) as e -> raise e)
+	      with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e)
 
       (* Second order case *)
       | (Meta _, true, _, _ | _, _, Meta _, true) ->
 	  (try
 	      w_unify2 env flags allow_K cv_pb ty1 ty2 evd
-	    with PretypeError (env,NoOccurrenceFound _) as e -> raise e
+	    with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e
 	      | ex when precatchable_exception ex ->
 		  try
 		    w_typed_unify env cv_pb flags ty1 ty2 evd