From de038270f72214b169d056642eb7144a79e6f126 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 7 Jul 2016 04:56:24 +0200 Subject: 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. --- toplevel/command.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'toplevel/command.ml') diff --git a/toplevel/command.ml b/toplevel/command.ml index 097865648e..b9a72fa332 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 -- cgit v1.2.3 From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 01:58:04 +0200 Subject: Remove errorlabstrm in favor of user_err As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch. --- toplevel/command.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'toplevel/command.ml') diff --git a/toplevel/command.ml b/toplevel/command.ml index b9a72fa332..4d333c30d0 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1312,7 +1312,7 @@ let do_program_fixpoint local poly l = match n with | Some n -> mkIdentC (snd n) | None -> - errorlabstrm "do_program_fixpoint" + user_err "do_program_fixpoint" (str "Recursive argument required for well-founded fixpoints") in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn @@ -1326,7 +1326,7 @@ let do_program_fixpoint local poly l = do_program_recursive local poly fixkind fixl ntns | _, _ -> - errorlabstrm "do_program_fixpoint" + user_err "do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") let check_safe () = -- cgit v1.2.3 From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 02:35:47 +0200 Subject: Make the user_err header an optional parameter. Suggested by @ppedrot --- toplevel/command.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'toplevel/command.ml') diff --git a/toplevel/command.ml b/toplevel/command.ml index 4d333c30d0..c8e0d16372 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -57,7 +57,7 @@ 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 "" + 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 @@ -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 "" 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 "" 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 "" msg + user_err ~loc msg let check_param = function @@ -955,7 +955,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let relargty = let error () = user_err ~loc:(constr_loc r) - "Command.build_wellfounded" + ~hdr:"Command.build_wellfounded" (Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.") in try @@ -1312,7 +1312,7 @@ let do_program_fixpoint local poly l = match n with | Some n -> mkIdentC (snd n) | None -> - user_err "do_program_fixpoint" + user_err ~hdr:"do_program_fixpoint" (str "Recursive argument required for well-founded fixpoints") in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn @@ -1326,7 +1326,7 @@ let do_program_fixpoint local poly l = do_program_recursive local poly fixkind fixl ntns | _, _ -> - user_err "do_program_fixpoint" + user_err ~hdr:"do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") let check_safe () = -- cgit v1.2.3