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. --- interp/notation_ops.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'interp/notation_ops.ml') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f3e0682bd7..7ab6ebb265 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -233,8 +233,8 @@ let split_at_recursive_part c = let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1) let check_is_hole id = function GHole _ -> () | t -> - user_err_loc (loc_of_glob_constr t,"", - strbrk "In recursive notation with binders, " ++ pr_id id ++ + user_err ~loc:(loc_of_glob_constr t) "" + (strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' @@ -283,8 +283,8 @@ let compare_recursive_parts found f f' (iterator,subc) = let loc1 = loc_of_glob_constr iterator in let loc2 = loc_of_glob_constr (Option.get !terminator) in (* Here, we would need a loc made of several parts ... *) - user_err_loc (subtract_loc loc1 loc2,"", - str "Both ends of the recursive pattern are the same.") + user_err ~loc:(subtract_loc loc1 loc2) "" + (str "Both ends of the recursive pattern are the same.") | Some (x,y,Some lassoc) -> let newfound,x,y,lassoc = if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || @@ -324,8 +324,8 @@ let notation_constr_and_vars_of_glob_constr a = | GApp (_,GVar (loc,f),[c]) when Id.equal f ldots_var -> (* Fall on the second part of the recursive pattern w/o having found the first part *) - user_err_loc (loc,"", - str "Cannot find where the recursive pattern starts.") + user_err ~loc "" + (str "Cannot find where the recursive pattern starts.") | c -> aux' c and aux' = function -- 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. --- interp/notation_ops.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp/notation_ops.ml') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7ab6ebb265..d565f01ba1 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -377,7 +377,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = let vars = Id.Map.filter filter nenv.ninterp_var_type in let check_recvar x = if Id.List.mem x found then - errorlabstrm "" (pr_id x ++ + user_err "" (pr_id x ++ strbrk " should only be used in the recursive part of a pattern.") in let check (x, y) = check_recvar x; check_recvar y in let () = List.iter check foundrec in @@ -396,7 +396,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then - errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++ + user_err "" (strbrk "in the right-hand side, " ++ pr_id x ++ str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in let check_type x typ = -- 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 --- interp/notation_ops.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'interp/notation_ops.ml') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index d565f01ba1..048cd5769b 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -233,7 +233,7 @@ let split_at_recursive_part c = let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1) let check_is_hole id = function GHole _ -> () | t -> - user_err ~loc:(loc_of_glob_constr t) "" + user_err ~loc:(loc_of_glob_constr t) (strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") @@ -283,7 +283,7 @@ let compare_recursive_parts found f f' (iterator,subc) = let loc1 = loc_of_glob_constr iterator in let loc2 = loc_of_glob_constr (Option.get !terminator) in (* Here, we would need a loc made of several parts ... *) - user_err ~loc:(subtract_loc loc1 loc2) "" + user_err ~loc:(subtract_loc loc1 loc2) (str "Both ends of the recursive pattern are the same.") | Some (x,y,Some lassoc) -> let newfound,x,y,lassoc = @@ -324,7 +324,7 @@ let notation_constr_and_vars_of_glob_constr a = | GApp (_,GVar (loc,f),[c]) when Id.equal f ldots_var -> (* Fall on the second part of the recursive pattern w/o having found the first part *) - user_err ~loc "" + user_err ~loc (str "Cannot find where the recursive pattern starts.") | c -> aux' c @@ -377,7 +377,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = let vars = Id.Map.filter filter nenv.ninterp_var_type in let check_recvar x = if Id.List.mem x found then - user_err "" (pr_id x ++ + user_err (pr_id x ++ strbrk " should only be used in the recursive part of a pattern.") in let check (x, y) = check_recvar x; check_recvar y in let () = List.iter check foundrec in @@ -396,7 +396,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then - user_err "" (strbrk "in the right-hand side, " ++ pr_id x ++ + user_err (strbrk "in the right-hand side, " ++ pr_id x ++ str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in let check_type x typ = -- cgit v1.2.3