aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/pretype_errors.ml19
-rw-r--r--pretyping/pretype_errors.mli11
-rw-r--r--pretyping/typeclasses_errors.ml20
-rw-r--r--pretyping/typeclasses_errors.mli10
-rw-r--r--pretyping/unification.ml2
-rw-r--r--proofs/logic.ml7
-rw-r--r--tactics/class_tactics.ml4
-rw-r--r--tactics/rewrite.ml23
-rw-r--r--toplevel/himsg.ml112
9 files changed, 100 insertions, 108 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 934e7bdbb..cad0beabf 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -51,6 +51,8 @@ type pretype_error =
| NotProduct of constr
| TypingError of type_error
| CannotUnifyOccurrences of subterm_unification_error
+ | UnsatisfiableConstraints of
+ (existential_key * Evar_kinds.t) option * Evar.Set.t option
exception PretypeError of env * Evd.evar_map * pretype_error
@@ -150,3 +152,20 @@ let error_not_product_loc loc env sigma c =
let error_var_not_found_loc loc s =
raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s)
+
+(*s Typeclass errors *)
+
+let unsatisfiable_constraints env evd ev comp =
+ match ev with
+ | None ->
+ let err = UnsatisfiableConstraints (None, comp) in
+ raise (PretypeError (env,evd,err))
+ | Some ev ->
+ let loc, kind = Evd.evar_source ev evd in
+ let err = UnsatisfiableConstraints (Some (ev, kind), comp) in
+ Loc.raise loc (PretypeError (env,evd,err))
+
+let unsatisfiable_exception exn =
+ match exn with
+ | PretypeError (_, _, UnsatisfiableConstraints _) -> true
+ | _ -> false
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index e816463e7..cc1443162 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -52,6 +52,9 @@ type pretype_error =
| NotProduct of constr
| TypingError of type_error
| CannotUnifyOccurrences of subterm_unification_error
+ | UnsatisfiableConstraints of
+ (existential_key * Evar_kinds.t) option * Evar.Set.t option
+ (** unresolvable evar, connex component *)
exception PretypeError of env * Evd.evar_map * pretype_error
@@ -134,3 +137,11 @@ val error_not_product_loc :
(** {6 Error in conversion from AST to glob_constr } *)
val error_var_not_found_loc : Loc.t -> Id.t -> 'b
+
+(** {6 Typeclass errors } *)
+
+val unsatisfiable_constraints : env -> Evd.evar_map -> Evd.evar option ->
+ Evar.Set.t option -> 'a
+
+val unsatisfiable_exception : exn -> bool
+
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index b16f000d4..816f03321 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -21,9 +21,6 @@ type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
| UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *)
- | NoInstance of Id.t Loc.located * constr list
- | UnsatisfiableConstraints of
- evar_map * (existential_key * Evar_kinds.t) option * Evar.Set.t option
| MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
exception TypeClassError of env * typeclass_error
@@ -34,21 +31,4 @@ let not_a_class env c = typeclass_error env (NotAClass c)
let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
-let no_instance env id args = typeclass_error env (NoInstance (id, args))
-
-let unsatisfiable_constraints env evd ev comp =
- match ev with
- | None ->
- let err = UnsatisfiableConstraints (evd, None, comp) in
- raise (TypeClassError (env, err))
- | Some ev ->
- let loc, kind = Evd.evar_source ev evd in
- let err = UnsatisfiableConstraints (evd, Some (ev, kind), comp) in
- Loc.raise loc (TypeClassError (env, err))
-
let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
-
-let unsatisfiable_exception exn =
- match exn with
- | TypeClassError (_, UnsatisfiableConstraints _) -> true
- | _ -> false
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index b3cfb37fa..c2a295bbc 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -20,10 +20,6 @@ type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
| UnboundMethod of global_reference * Id.t located (** Class name, method *)
- | NoInstance of Id.t located * constr list
- | UnsatisfiableConstraints of
- evar_map * (existential_key * Evar_kinds.t) option * Evar.Set.t option
- (** evar map, unresolvable evar, connex component *)
| MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
exception TypeClassError of env * typeclass_error
@@ -32,11 +28,5 @@ val not_a_class : env -> constr -> 'a
val unbound_method : env -> global_reference -> Id.t located -> 'a
-val no_instance : env -> Id.t located -> constr list -> 'a
-
-val unsatisfiable_constraints : env -> evar_map -> evar option ->
- Evar.Set.t option -> 'a
-
val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
-val unsatisfiable_exception : exn -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ed01c6b7b..5f7e2916b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1337,7 +1337,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
if closed0 cl && not (isEvar cl)
then
(try w_typed_unify env evd CONV flags op cl,cl
- with ex when Typeclasses_errors.unsatisfiable_exception ex ->
+ with ex when Pretype_errors.unsatisfiable_exception ex ->
bestexn := Some ex; error "Unsat")
else error "Bound 1"
with ex when precatchable_exception ex ->
diff --git a/proofs/logic.ml b/proofs/logic.ml
index dc8f31859..a7538193b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -54,7 +54,8 @@ let is_unification_error = function
| NoOccurrenceFound _ | CannotUnifyBindingType _
| ActualTypeNotCoercible _ | UnifOccurCheck _
| CannotFindWellTypedAbstraction _ | WrongAbstractionType _
-| UnsolvableImplicit _| AbstractionOverMeta _ -> true
+| UnsolvableImplicit _| AbstractionOverMeta _
+| UnsatisfiableConstraints _ -> true
| _ -> false
let catchable_exception = function
@@ -64,9 +65,7 @@ let catchable_exception = function
(* reduction errors *)
| Tacred.ReductionTacticError _ -> true
(* unification and typing errors *)
- | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e
- | Typeclasses_errors.TypeClassError
- (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
+ | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e
| _ -> false
let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id))
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7c9aa59b6..9cf5aec04 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -602,8 +602,8 @@ let error_unresolvable env comp evd =
else (found, accu)
in
let (_, ev) = Evd.fold_undefined fold evd (true, None) in
- Typeclasses_errors.unsatisfiable_constraints
- (Evarutil.nf_env_evar evd env) evd ev comp
+ Pretype_errors.unsatisfiable_constraints
+ (Evarutil.nf_env_evar evd env) evd ev comp
(** Check if an evar is concerned by the current resolution attempt,
(and in particular is in the current component), and also update
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 5d4a7509a..efcde3d1b 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -21,6 +21,7 @@ open Tacticals
open Tacmach
open Tactics
open Clenv
+open Pretype_errors
open Typeclasses
open Typeclasses_errors
open Classes
@@ -1449,10 +1450,11 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) [] sigma concl is_hyp in
treat res
with
- | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
+ | Pretype_errors.PretypeError (env, sigma,
+ (Pretype_errors.UnsatisfiableConstraints _ as e)) ->
Refiner.tclFAIL 0
(str"Unable to satisfy the rewriting constraints."
- ++ fnl () ++ Himsg.explain_typeclass_error env e)
+ ++ fnl () ++ Himsg.explain_pretype_error env sigma e)
in tac gl
@@ -1535,9 +1537,9 @@ let cl_rewrite_clause_newtac ?abs strat clause =
cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
in treat (res, is_hyp)
with
- | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
+ | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
- ++ fnl () ++ Himsg.explain_typeclass_error env e))
+ ++ fnl () ++ Himsg.explain_pretype_error env evd e))
end
let newtactic_init_setoid () =
@@ -1905,13 +1907,12 @@ let unification_rewrite l2r c1 c2 cl car rel but env =
~flags:{ rewrite_unif_flags with Unification.resolve_evars = true } env
cl.evd ((if l2r then c1 else c2),but)
with
- | ex when Pretype_errors.precatchable_exception ex ||
- Typeclasses_errors.unsatisfiable_exception ex ->
- (* ~flags:(true,true) to make Ring work (since it really
- exploits conversion) *)
- Unification.w_unify_to_subterm
- ~flags:{ rewrite2_unif_flags with Unification.resolve_evars = true }
- env cl.evd ((if l2r then c1 else c2),but)
+ | ex when Pretype_errors.precatchable_exception ex ->
+ (* ~flags:(true,true) to make Ring work (since it really
+ exploits conversion) *)
+ Unification.w_unify_to_subterm
+ ~flags:{ rewrite2_unif_flags with Unification.resolve_evars = true }
+ env cl.evd ((if l2r then c1 else c2),but)
in
let cl' = {cl with evd = evd'} in
let cl' = Clenvtac.clenv_pose_dependent_evars true cl' in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ae8e1f532..e3a303aed 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -660,6 +660,57 @@ let explain_cannot_unify_occurrences env sigma nested (cl2,pos2,t2) (cl1,pos1,t1
pr_lconstr_env env t1 ++ strbrk " at position " ++
pr_position (cl1,pos1) ++ ppreason ++ str "."
+let pr_constraints printenv env evd evars cstrs =
+ let (ev, evi) = Evar.Map.choose evars in
+ if Evar.Map.for_all (fun ev' evi' ->
+ eq_named_context_val evi.evar_hyps evi'.evar_hyps) evars
+ then
+ let l = Evar.Map.bindings evars in
+ let pe =
+ if printenv then
+ pr_ne_context_of (str "In environment:") (mt ())
+ (reset_with_named_context evi.evar_hyps env) ++ fnl ()
+ else mt ()
+ in
+ let evs =
+ prlist_with_sep (fun () -> fnl ())
+ (fun (ev, evi) -> str(string_of_existential ev) ++
+ str " : " ++ pr_lconstr evi.evar_concl) l
+ in
+ pe ++ evs ++ fnl() ++ h 0 (pr_evar_constraints cstrs)
+ else
+ let filter evk _ = Evar.Map.mem evk evars in
+ pr_evar_map_filter ~with_univs:false filter evd
+
+let explain_unsatisfiable_constraints env evd constr comp =
+ let (_, constraints) = Evd.extract_all_conv_pbs evd in
+ let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined evd) in
+ (** Only keep evars that are subject to resolution and members of the given
+ component. *)
+ let is_kept evk evi = match comp with
+ | None -> Typeclasses.is_resolvable evi
+ | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp
+ in
+ let undef =
+ let m = Evar.Map.filter is_kept undef in
+ if Evar.Map.is_empty m then undef
+ else m
+ in
+ match constr with
+ | None ->
+ str "Unable to satisfy the following constraints:" ++ fnl () ++
+ pr_constraints true env evd undef constraints
+ | Some (ev, k) ->
+ let cstr =
+ let remaining = Evar.Map.remove ev undef in
+ if not (Evar.Map.is_empty remaining) then
+ str "With the following constraints:" ++ fnl () ++
+ pr_constraints false env evd remaining constraints
+ else mt ()
+ in
+ let info = Evar.Map.find ev undef in
+ explain_typeclass_resolution env info k ++ fnl () ++ cstr
+
let explain_pretype_error env sigma err =
let env = Evarutil.env_nf_betaiotaevar sigma env in
let env = make_all_name_different env in
@@ -693,7 +744,7 @@ let explain_pretype_error env sigma err =
| NonLinearUnification (m,c) -> explain_non_linear_unification env m c
| TypingError t -> explain_type_error env sigma t
| CannotUnifyOccurrences (b,c1,c2,e) -> explain_cannot_unify_occurrences env sigma b c1 c2 e
-
+ | UnsatisfiableConstraints (c,comp) -> explain_unsatisfiable_constraints env sigma c comp
(* Module errors *)
open Modops
@@ -850,62 +901,6 @@ let pr_constr_exprs exprs =
(fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr d ++ pps)
exprs (mt ()))
-let explain_no_instance env (_,id) l =
- str "No instance found for class " ++ Nameops.pr_id id ++ spc () ++
- str "applied to arguments" ++ spc () ++
- pr_sequence (pr_lconstr_env env) l
-
-let pr_constraints printenv env evd evars cstrs =
- let (ev, evi) = Evar.Map.choose evars in
- if Evar.Map.for_all (fun ev' evi' ->
- eq_named_context_val evi.evar_hyps evi'.evar_hyps) evars
- then
- let l = Evar.Map.bindings evars in
- let pe =
- if printenv then
- pr_ne_context_of (str "In environment:") (mt ())
- (reset_with_named_context evi.evar_hyps env) ++ fnl ()
- else mt ()
- in
- let evs =
- prlist_with_sep (fun () -> fnl ())
- (fun (ev, evi) -> str(string_of_existential ev) ++
- str " : " ++ pr_lconstr evi.evar_concl) l
- in
- pe ++ evs ++ fnl() ++ h 0 (pr_evar_constraints cstrs)
- else
- let filter evk _ = Evar.Map.mem evk evars in
- pr_evar_map_filter ~with_univs:false filter evd
-
-let explain_unsatisfiable_constraints env evd constr comp =
- let (_, constraints) = Evd.extract_all_conv_pbs evd in
- let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined evd) in
- (** Only keep evars that are subject to resolution and members of the given
- component. *)
- let is_kept evk evi = match comp with
- | None -> Typeclasses.is_resolvable evi
- | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp
- in
- let undef =
- let m = Evar.Map.filter is_kept undef in
- if Evar.Map.is_empty m then undef
- else m
- in
- match constr with
- | None ->
- str "Unable to satisfy the following constraints:" ++ fnl () ++
- pr_constraints true env evd undef constraints
- | Some (ev, k) ->
- let cstr =
- let remaining = Evar.Map.remove ev undef in
- if not (Evar.Map.is_empty remaining) then
- str "With the following constraints:" ++ fnl () ++
- pr_constraints false env evd remaining constraints
- else mt ()
- in
- let info = Evar.Map.find ev undef in
- explain_typeclass_resolution env info k ++ fnl () ++ cstr
-
let explain_mismatched_contexts env c i j =
str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env j) ++
@@ -915,9 +910,6 @@ let explain_mismatched_contexts env c i j =
let explain_typeclass_error env = function
| NotAClass c -> explain_not_a_class env c
| UnboundMethod (cid, id) -> explain_unbound_method env cid id
- | NoInstance (id, l) -> explain_no_instance env id l
- | UnsatisfiableConstraints (evd, c, comp) ->
- explain_unsatisfiable_constraints env evd c comp
| MismatchedContextInstance (c,i,j) -> explain_mismatched_contexts env c i j
(* Refiner errors *)