aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evarconv.ml9
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/pretype_errors.ml6
-rw-r--r--pretyping/pretype_errors.mli7
-rw-r--r--pretyping/typing.ml5
-rw-r--r--pretyping/typing.mli2
-rw-r--r--pretyping/unification.ml11
-rw-r--r--toplevel/himsg.ml10
8 files changed, 30 insertions, 22 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c2ded73ad..be5eb5dbd 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -651,6 +651,8 @@ let set_solve_evars f = solve_evars := f
* proposition from Dan Grayson]
*)
+exception TypingFailed of evar_map
+
let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
try
let args = Array.to_list args in
@@ -702,10 +704,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
(* We instantiate the evars of which the value is forced by typing *)
let evd,rhs =
- try !solve_evars env_evar evd rhs
+ let evdref = ref evd in
+ try let c = !solve_evars env_evar evdref rhs in !evdref,c
with e when Pretype_errors.precatchable_exception e ->
(* Could not revert all subterms *)
- raise Exit in
+ raise (TypingFailed !evdref) in
let rec abstract_free_holes evd = function
| (id,idty,c,_,evsref,_,_)::l ->
@@ -736,7 +739,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
Evd.define evk rhs evd in
abstract_free_holes evd subst, true
- with Exit -> evd, false
+ with TypingFailed evd -> Evd.define evk rhs evd, false
let second_order_matching_with_args ts env evd ev l t =
(*
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index d3f8b451a..5a329f5f4 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -44,7 +44,7 @@ val check_conv_record : constr * types stack -> constr * types stack ->
(constr stack * types stack) * constr *
(int * constr)
-val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit
+val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit
val second_order_matching : transparent_state -> env -> evar_map ->
existential -> occurrences option list -> constr -> evar_map * bool
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index ec808de0f..f5870a8c0 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -39,7 +39,7 @@ type pretype_error =
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr * Id.t option
- | CannotFindWellTypedAbstraction of constr * constr list
+ | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
| WrongAbstractionType of Name.t * constr * types * types
| AbstractionOverMeta of Name.t * Name.t
| NonLinearUnification of Name.t * constr
@@ -162,8 +162,8 @@ let error_cannot_unify_local env sigma (m,n,sn) =
let error_cannot_coerce env sigma (m,n) =
raise (PretypeError (env, sigma,CannotUnify (m,n,None)))
-let error_cannot_find_well_typed_abstraction env sigma p l =
- raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l)))
+let error_cannot_find_well_typed_abstraction env sigma p l e =
+ raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l,e)))
let error_wrong_abstraction_type env sigma na a p l =
raise (PretypeError (env, sigma,WrongAbstractionType (na,a,p,l)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 36ae6c13f..ee7965131 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -13,6 +13,7 @@ open Sign
open Environ
open Glob_term
open Inductiveops
+open Type_errors
(** {6 The type of errors raised by the pretyper } *)
@@ -41,7 +42,7 @@ type pretype_error =
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr * Id.t option
- | CannotFindWellTypedAbstraction of constr * constr list
+ | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
| WrongAbstractionType of Name.t * constr * types * types
| AbstractionOverMeta of Name.t * Name.t
| NonLinearUnification of Name.t * constr
@@ -49,7 +50,7 @@ type pretype_error =
| VarNotFound of Id.t
| UnexpectedType of constr * constr
| NotProduct of constr
- | TypingError of Type_errors.type_error
+ | TypingError of type_error
exception PretypeError of env * Evd.evar_map * pretype_error
@@ -105,7 +106,7 @@ val error_cannot_unify : env -> Evd.evar_map -> ?reason:unification_error ->
val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
- constr -> constr list -> 'b
+ constr -> constr list -> (env * type_error) option -> 'b
val error_wrong_abstraction_type : env -> Evd.evar_map ->
Name.t -> constr -> types -> types -> 'b
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 5ae04488f..7cf7e5889 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -287,10 +287,9 @@ let e_type_of env evd c =
(* side-effect on evdref *)
!evdref, Termops.refresh_universes j.uj_type
-let solve_evars env evd c =
- let evdref = ref evd in
+let solve_evars env evdref c =
let c = (execute env evdref c).uj_val in
(* side-effect on evdref *)
- !evdref, nf_evar !evdref c
+ nf_evar !evdref c
let _ = Evarconv.set_solve_evars solve_evars
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 88dc895e6..084bdbc4f 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -30,7 +30,7 @@ val check : env -> evar_map -> constr -> types -> unit
val meta_type : evar_map -> metavariable -> types
(** Solve existential variables using typing *)
-val solve_evars : env -> evar_map -> constr -> evar_map * constr
+val solve_evars : env -> evar_map ref -> constr -> constr
(** Raise an error message if incorrect elimination for this inductive *)
(** (first constr is term to match, second is return predicate) *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4c0f12d3c..8b89bd438 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -69,8 +69,11 @@ let abstract_list_all env evd typ c l =
let p = abstract_scheme env c l_with_all_occs ctxt in
let typp =
try Typing.type_of env evd p
- with UserError _ | Type_errors.TypeError _ ->
- error_cannot_find_well_typed_abstraction env evd p l in
+ with
+ | UserError _ ->
+ error_cannot_find_well_typed_abstraction env evd p l None
+ | Type_errors.TypeError (env',x) ->
+ error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
(p,typp)
let set_occurrences_of_last_arg args =
@@ -83,8 +86,8 @@ let abstract_list_all_with_dependencies env evd typ c l =
let evd,b =
Evarconv.second_order_matching empty_transparent_state
env evd ev' argoccs c in
- if b then nf_evar evd (existential_value evd (destEvar ev))
- else error "Cannot find a well-typed abstraction."
+ let p = nf_evar evd (existential_value evd (destEvar ev)) in
+ if b then p else error_cannot_find_well_typed_abstraction env evd p l None
(**)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 848bf5232..14202a32a 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -219,7 +219,7 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
let pc,pct = pr_ljudge_env env c in
hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
in
- str "Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++
+ str "Illegal application: " ++ (* pe ++ *) fnl () ++
str "The term" ++ brk(1,1) ++ pr ++ spc () ++
str "of type" ++ brk(1,1) ++ prt ++ spc () ++
str "cannot be applied to the " ++ term_string1 ++ fnl () ++
@@ -489,12 +489,13 @@ let explain_cannot_unify_binding_type env m n =
str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "."
-let explain_cannot_find_well_typed_abstraction env p l =
+let explain_cannot_find_well_typed_abstraction env p l e =
str "Abstracting over the " ++
str (String.plural (List.length l) "term") ++ spc () ++
hov 0 (pr_enum (pr_lconstr_env env) l) ++ spc () ++
str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++
- str "which is ill-typed."
+ str "which is ill-typed." ++
+ (match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e)
let explain_wrong_abstraction_type env na abs expected result =
let ppname = match na with Anonymous -> mt() | Name id -> pr_id id ++ spc() in
@@ -565,8 +566,9 @@ let explain_pretype_error env sigma err =
| CannotGeneralize ty -> explain_refiner_cannot_generalize env ty
| NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id
| CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
- | CannotFindWellTypedAbstraction (p,l) ->
+ | CannotFindWellTypedAbstraction (p,l,e) ->
explain_cannot_find_well_typed_abstraction env p l
+ (Option.map (fun (env',e) -> explain_type_error env' sigma e) e)
| WrongAbstractionType (n,a,t,u) -> explain_wrong_abstraction_type env n a t u
| AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n
| NonLinearUnification (m,c) -> explain_non_linear_unification env m c
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 08:25:45 +0000