diff options
-rw-r--r-- | pretyping/pretype_errors.ml | 19 | ||||
-rw-r--r-- | pretyping/pretype_errors.mli | 11 | ||||
-rw-r--r-- | pretyping/typeclasses_errors.ml | 20 | ||||
-rw-r--r-- | pretyping/typeclasses_errors.mli | 10 | ||||
-rw-r--r-- | pretyping/unification.ml | 2 | ||||
-rw-r--r-- | proofs/logic.ml | 7 | ||||
-rw-r--r-- | tactics/class_tactics.ml | 4 | ||||
-rw-r--r-- | tactics/rewrite.ml | 23 | ||||
-rw-r--r-- | toplevel/himsg.ml | 112 |
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 *) |