diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-07-07 04:56:24 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 01:48:30 +0200 |
commit | de038270f72214b169d056642eb7144a79e6f126 (patch) | |
tree | c1a5dc835f5042c79418fdbadc7b266a473b8c82 /toplevel | |
parent | 13fb26d615cdb03a4c4841c20b108deab2de60b3 (diff) |
Unify location handling of error functions.
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/classes.ml | 4 | ||||
-rw-r--r-- | toplevel/command.ml | 18 | ||||
-rw-r--r-- | toplevel/obligations.ml | 4 | ||||
-rw-r--r-- | toplevel/record.ml | 8 | ||||
-rw-r--r-- | toplevel/vernac.ml | 2 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 23 |
6 files changed, 29 insertions, 30 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index d6a6162f9..26cb7451a 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -66,8 +66,8 @@ let existing_instance glob g pri = match class_of_constr r with | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob (*FIXME*) (Flags.use_polymorphic_flag ()) c) - | None -> user_err_loc (loc_of_reference g, "declare_instance", - Pp.str "Constant does not build instances of a declared type class.") + | None -> user_err ~loc:(loc_of_reference g) "declare_instance" + (Pp.str "Constant does not build instances of a declared type class.") let mismatched_params env n m = mismatched_ctx_inst env Parameters n m let mismatched_props env n m = mismatched_ctx_inst env Properties n m diff --git a/toplevel/command.ml b/toplevel/command.ml index 097865648..b9a72fa33 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -57,8 +57,8 @@ let rec complete_conclusion a cs = function | CHole (loc, k, _, _) -> let (has_no_args,name,params) = a in if not has_no_args then - user_err_loc (loc,"", - strbrk"Cannot infer the non constant arguments of the conclusion of " + user_err ~loc "" + (strbrk"Cannot infer the non constant arguments of the conclusion of " ++ pr_id cs ++ str "."); let args = List.map (fun id -> CRef(Ident(loc,id),None)) params in CAppExpl (loc,(None,Ident(loc,name),None),List.rev args) @@ -330,7 +330,7 @@ let do_assumptions kind nl l = match l with | (Discharge, _, _) when Lib.sections_are_opened () -> let loc = fst id in let msg = Pp.str "Section variables cannot be polymorphic." in - user_err_loc (loc, "", msg) + user_err ~loc "" msg | _ -> () in do_assumptions_bound_univs coe kind nl id (Some pl) c @@ -342,7 +342,7 @@ let do_assumptions kind nl l = match l with let loc = fst id in let msg = Pp.str "Assumptions with bound universes can only be defined one at a time." in - user_err_loc (loc, "", msg) + user_err ~loc "" msg in (coe, (List.map map idl, c)) in @@ -438,7 +438,7 @@ let interp_ind_arity env evdref ind = let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in let pseudo_poly = check_anonymous_type c in let () = if not (Reduction.is_arity env t) then - user_err_loc (constr_loc ind.ind_arity, "", str "Not an arity") + user_err ~loc:(constr_loc ind.ind_arity) "" (str "Not an arity") in t, pseudo_poly, impls @@ -553,7 +553,7 @@ let check_named (loc, na) = match na with | Name _ -> () | Anonymous -> let msg = str "Parameters must be named." in - user_err_loc (loc, "", msg) + user_err ~loc "" msg let check_param = function @@ -954,9 +954,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = - user_err_loc (constr_loc r, - "Command.build_wellfounded", - Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.") + user_err ~loc:(constr_loc r) + "Command.build_wellfounded" + (Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.") in try let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 29d745732..38d4a62b4 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -34,7 +34,7 @@ let check_evars env evm = | Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_,_,false) -> () | _ -> - Pretype_errors.error_unsolvable_implicit loc env evm key None) + Pretype_errors.error_unsolvable_implicit ~loc env evm key None) (Evd.undefined_map evm) type oblinfo = @@ -985,7 +985,7 @@ and solve_obligation_by_tac prg obls i tac = let (e, _) = CErrors.push e in match e with | Refiner.FailError (_, s) -> - user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) + user_err ~loc:(fst obl.obl_location) "solve_obligation" (Lazy.force s) | e -> None (* FIXME really ? *) and solve_prg_obligations prg ?oblset tac = diff --git a/toplevel/record.ml b/toplevel/record.ml index 71d070776..6a64b0d66 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -102,7 +102,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = let error bk (loc, name) = match bk, name with | Default _, Anonymous -> - user_err_loc (loc, "record", str "Record parameters must be named") + user_err ~loc "record" (str "Record parameters must be named") | _ -> () in List.iter @@ -127,7 +127,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = sred, true | None -> s, false else s, false) - | _ -> user_err_loc (constr_loc t,"", str"Sort expected.")) + | _ -> user_err ~loc:(constr_loc t) "" (str"Sort expected.")) | None -> let uvarkind = Evd.univ_flexible_alg in mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true @@ -539,8 +539,8 @@ let declare_existing_class g = match g with | ConstRef x -> add_constant_class x | IndRef x -> add_inductive_class x - | _ -> user_err_loc (Loc.dummy_loc, "declare_existing_class", - Pp.str"Unsupported class type, only constants and inductives are allowed") + | _ -> user_err "declare_existing_class" + (Pp.str"Unsupported class type, only constants and inductives are allowed") open Vernacexpr diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f83ada466..00655497b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -70,7 +70,7 @@ let disable_drop = function | Drop -> CErrors.error "Drop is forbidden." | e -> e -let user_error loc s = CErrors.user_err_loc (loc,"_",str s) +let user_error loc s = CErrors.user_err ~loc "_" (str s) (* Opening and closing a channel. Open it twice when verbose: the first channel is used to read the commands, and the second one to print them. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f69c4fa18..3f784fd8a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -380,9 +380,9 @@ let err_unmapped_library loc ?from qid = | Some from -> str " and prefix " ++ pr_dirpath from ++ str "." in - user_err_loc - (loc,"locate_library", - strbrk "Cannot find a physical path bound to logical path matching suffix " ++ + user_err ~loc + "locate_library" + (strbrk "Cannot find a physical path bound to logical path matching suffix " ++ pr_dirpath dir ++ prefix) let err_notfound_library loc ?from qid = @@ -391,9 +391,8 @@ let err_notfound_library loc ?from qid = | Some from -> str " with prefix " ++ pr_dirpath from ++ str "." in - user_err_loc - (loc,"locate_library", - strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) + user_err ~loc "locate_library" + (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library r = let (loc,qid) = qualid_of_reference r in @@ -605,15 +604,15 @@ let vernac_combined_scheme lid l = let vernac_universe loc poly l = if poly && not (Lib.sections_are_opened ()) then - user_err_loc (loc, "vernac_universe", - str"Polymorphic universes can only be declared inside sections, " ++ + user_err ~loc "vernac_universe" + (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); do_universe poly l let vernac_constraint loc poly l = if poly && not (Lib.sections_are_opened ()) then - user_err_loc (loc, "vernac_constraint", - str"Polymorphic universe constraints can only be declared" + user_err ~loc "vernac_constraint" + (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); do_constraint poly l @@ -1575,8 +1574,8 @@ let global_module r = let (loc,qid) = qualid_of_reference r in try Nametab.full_name_module qid with Not_found -> - user_err_loc (loc, "global_module", - str "Module/section " ++ pr_qualid qid ++ str " not found.") + user_err ~loc "global_module" + (str "Module/section " ++ pr_qualid qid ++ str " not found.") let interp_search_restriction = function | SearchOutside l -> (List.map global_module l, true) |