From 26b9ad1d0423f8dc1dbd4d90557469db6a5eaa03 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 18 Sep 2017 19:00:09 +0200 Subject: Fixing two anomalies in corner cases of the syntax of notation formats. --- vernac/metasyntax.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac/metasyntax.ml') diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c424b1d50..3126b1b14 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -129,12 +129,12 @@ let parse_format ((loc, str) : lstring) = and parse_quoted n i = if i < len then match str.[i] with (* Parse " // " *) - | '/' when i <= len && str.[i+1] == '/' -> - (* We forget the useless n spaces... *) + | '/' when i+1 < len && str.[i+1] == '/' -> + (* We discard the useless n spaces... *) push_token (UnpCut PpFnl) (parse_token 1 (close_quotation (i+2))) (* Parse " .. / .. " *) - | '/' when i <= len -> + | '/' when i+1 < len -> let p = spaces 0 (i+1) in push_token (UnpCut (PpBrk (n,p))) (parse_token 1 (close_quotation (i+p+1))) -- cgit v1.2.3 From 46a17141e6a19fff9dfeb1ef18cbba054e34e3c3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 18 Sep 2017 18:14:25 +0200 Subject: Reporting locations in error messages about notation formats. --- interp/ppextend.ml | 2 +- interp/ppextend.mli | 2 +- lib/loc.ml | 2 + lib/loc.mli | 5 ++ printing/ppconstr.ml | 2 +- vernac/metasyntax.ml | 168 +++++++++++++++++++++++++++------------------------ 6 files changed, 98 insertions(+), 83 deletions(-) (limited to 'vernac/metasyntax.ml') diff --git a/interp/ppextend.ml b/interp/ppextend.ml index 3ebc9b71d..ce19dd8a9 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -36,5 +36,5 @@ type unparsing = | UnpListMetaVar of int * parenRelation * unparsing list | UnpBinderListMetaVar of int * bool * unparsing list | UnpTerminal of string - | UnpBox of ppbox * unparsing list + | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut diff --git a/interp/ppextend.mli b/interp/ppextend.mli index 6ff5a4272..7b62a2074 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -29,5 +29,5 @@ type unparsing = | UnpListMetaVar of int * parenRelation * unparsing list | UnpBinderListMetaVar of int * bool * unparsing list | UnpTerminal of string - | UnpBox of ppbox * unparsing list + | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut diff --git a/lib/loc.ml b/lib/loc.ml index 06da13d44..4a935a9d9 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -62,6 +62,8 @@ let merge_opt l1 l2 = match l1, l2 with let unloc loc = (loc.bp, loc.ep) +let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp } + (** Located type *) type 'a located = t option * 'a diff --git a/lib/loc.mli b/lib/loc.mli index d4061e044..fde490cc8 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -40,6 +40,11 @@ val merge : t -> t -> t val merge_opt : t option -> t option -> t option (** Merge locations, usually generating the largest possible span *) +val shift_loc : int -> int -> t -> t +(** [shift_loc loc n p] shifts the beginning of location by [n] and + the end by [p]; it is assumed that the shifts do not change the + lines at which the location starts and ends *) + (** {5 Located exceptions} *) val add_loc : Exninfo.info -> t -> Exninfo.info diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 37204c213..102c6ef6d 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -117,7 +117,7 @@ let tag_var = tag Tag.variable let pp1 = str s in return unp pp1 pp2 | UnpBox (b,sub) as unp :: l -> - let pp1 = ppcmd_of_box b (aux sub) in + let pp1 = ppcmd_of_box b (aux (List.map snd sub)) in let pp2 = aux l in return unp pp1 pp2 | UnpCut cut as unp :: l -> diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 3126b1b14..3b5490e31 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -99,18 +99,24 @@ let pr_grammar = function let parse_format ((loc, str) : lstring) = let len = String.length str in - let push_token a = function - | cur::l -> (a::cur)::l - | [] -> [[a]] in - let push_white n l = - if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in - let close_box i b = function - | a::(_::_ as l) -> push_token (UnpBox (b,a)) l - | _ -> user_err Pp.(str "Non terminated box in format.") in - let close_quotation i = - if i < len && str.[i] == '\'' && (Int.equal (i+1) len || str.[i+1] == ' ') - then i+1 - else user_err Pp.(str "Incorrectly terminated quoted expression.") in + (* TODO: update the line of the location when the string contains newlines *) + let make_loc i j = Option.map (Loc.shift_loc (i+1) (j-len)) loc in + let push_token loc a = function + | (i,cur)::l -> (i,(loc,a)::cur)::l + | [] -> assert false in + let push_white i n l = + if Int.equal n 0 then l else push_token (make_loc i (i+n)) (UnpTerminal (String.make n ' ')) l in + let close_box start stop b = function + | (_,a)::(_::_ as l) -> push_token (make_loc start stop) (UnpBox (b,a)) l + | [a] -> user_err ?loc:(make_loc start stop) Pp.(str "Non terminated box in format.") + | [] -> assert false in + let close_quotation start i = + if i < len && str.[i] == '\'' then + if (Int.equal (i+1) len || str.[i+1] == ' ') + then i+1 + else user_err ?loc:(make_loc (i+1) (i+1)) Pp.(str "Space expected after quoted expression.") + else + user_err ?loc:(make_loc start (i-1)) Pp.(str "Beginning of quoted expression expected to be ended by a quote.") in let rec spaces n i = if i < len && str.[i] == ' ' then spaces (n+1) (i+1) else n in @@ -118,81 +124,78 @@ let parse_format ((loc, str) : lstring) = if i < len && str.[i] != ' ' then if str.[i] == '\'' && quoted && (i+1 >= len || str.[i+1] == ' ') - then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n + then if Int.equal n 0 then user_err ?loc:(make_loc (i-1) i) Pp.(str "Empty quoted token.") else n else nonspaces quoted (n+1) (i+1) else - if quoted then user_err Pp.(str "Spaces are not allowed in (quoted) symbols.") + if quoted then user_err ?loc:(make_loc i i) Pp.(str "Spaces are not allowed in (quoted) symbols.") else n in let rec parse_non_format i = let n = nonspaces false 0 i in - push_token (UnpTerminal (String.sub str i n)) (parse_token 1 (i+n)) + push_token (make_loc i (i+n-1)) (UnpTerminal (String.sub str i n)) (parse_token 1 (i+n)) and parse_quoted n i = if i < len then match str.[i] with (* Parse " // " *) | '/' when i+1 < len && str.[i+1] == '/' -> (* We discard the useless n spaces... *) - push_token (UnpCut PpFnl) - (parse_token 1 (close_quotation (i+2))) + push_token (make_loc (i-n) (i+1)) (UnpCut PpFnl) + (parse_token 1 (close_quotation i (i+2))) (* Parse " .. / .. " *) | '/' when i+1 < len -> let p = spaces 0 (i+1) in - push_token (UnpCut (PpBrk (n,p))) - (parse_token 1 (close_quotation (i+p+1))) + push_token (make_loc (i-n) (i+p)) (UnpCut (PpBrk (n,p))) + (parse_token 1 (close_quotation i (i+p+1))) | c -> (* The spaces are real spaces *) - push_white n (match c with + push_white i n (match c with | '[' -> - if i <= len then match str.[i+1] with + if i+1 < len then match str.[i+1] with (* Parse " [h .. ", *) | 'h' when i+1 <= len && str.[i+2] == 'v' -> - (parse_box (fun n -> PpHVB n) (i+3)) + (parse_box i (fun n -> PpHVB n) (i+3)) (* Parse " [v .. ", *) | 'v' -> - parse_box (fun n -> PpVB n) (i+2) + parse_box i (fun n -> PpVB n) (i+2) (* Parse " [ .. ", *) | ' ' | '\'' -> - parse_box (fun n -> PpHOVB n) (i+1) - | _ -> user_err Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.") - else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.") + parse_box i (fun n -> PpHOVB n) (i+1) + | _ -> user_err ?loc:(make_loc i i) Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.") + else user_err ?loc:(make_loc i i) Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.") (* Parse "]" *) | ']' -> - ([] :: parse_token 1 (close_quotation (i+1))) + ((i,[]) :: parse_token 1 (close_quotation i (i+1))) (* Parse a non formatting token *) | c -> let n = nonspaces true 0 i in - push_token (UnpTerminal (String.sub str (i-1) (n+2))) - (parse_token 1 (close_quotation (i+n)))) + push_token (make_loc i (i+n-1)) (UnpTerminal (String.sub str (i-1) (n+2))) + (parse_token 1 (close_quotation i (i+n)))) else if Int.equal n 0 then [] - else user_err Pp.(str "Ending spaces non part of a format annotation.") - and parse_box box i = + else user_err ?loc:(make_loc (len-n) len) Pp.(str "Ending spaces non part of a format annotation.") + and parse_box start box i = let n = spaces 0 i in - close_box i (box n) (parse_token 1 (close_quotation (i+n))) + close_box start (i+n-1) (box n) (parse_token 1 (close_quotation i (i+n))) and parse_token k i = let n = spaces 0 i in let i = i+n in if i < len then match str.[i] with (* Parse a ' *) | '\'' when i+1 >= len || str.[i+1] == ' ' -> - push_white (n-k) (push_token (UnpTerminal "'") (parse_token 1 (i+1))) + push_white (i-n) (n-k) (push_token (make_loc i (i+1)) (UnpTerminal "'") (parse_token 1 (i+1))) (* Parse the beginning of a quoted expression *) | '\'' -> parse_quoted (n-k) (i+1) (* Otherwise *) | _ -> - push_white (n-k) (parse_non_format i) - else push_white n [[]] + push_white (i-n) (n-k) (parse_non_format i) + else push_white (i-n) n [(len,[])] in - try - if not (String.is_empty str) then match parse_token 0 0 with - | [l] -> l - | _ -> user_err Pp.(str "Box closed without being opened in format.") - else - [] - with reraise -> - let (e, info) = CErrors.push reraise in - let info = Option.cata (Loc.add_loc info) info loc in - iraise (e, info) + if not (String.is_empty str) then + match parse_token 0 0 with + | [_,l] -> l + | (i,_)::_ -> user_err ?loc:(make_loc i i) Pp.(str "Box closed without being opened.") + | [] -> assert false + else + [] (***********************) (* Analyzing notations *) @@ -383,11 +386,11 @@ let is_next_terminal = function Terminal _ :: _ -> true | _ -> false let is_next_break = function Break _ :: _ -> true | _ -> false -let add_break n l = UnpCut (PpBrk(n,0)) :: l +let add_break n l = (None,UnpCut (PpBrk(n,0))) :: l let add_break_if_none n = function - | ((UnpCut (PpBrk _) :: _) | []) as l -> l - | l -> UnpCut (PpBrk(n,0)) :: l + | (((_,UnpCut (PpBrk _)) :: _) | []) as l -> l + | l -> (None,UnpCut (PpBrk(n,0))) :: l let check_open_binder isopen sl m = let pr_token = function @@ -413,30 +416,30 @@ let make_hunks etyps symbols from = let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in let u = UnpMetaVar (i,prec) in if is_next_non_terminal prods then - u :: add_break_if_none 1 (make prods) + (None,u) :: add_break_if_none 1 (make prods) else - u :: make_with_space prods + (None,u) :: make_with_space prods | Terminal s :: prods when List.exists is_non_terminal prods -> if (is_comma s || is_operator s) then (* Always a breakable space after comma or separator *) - UnpTerminal s :: add_break_if_none 1 (make prods) + (None,UnpTerminal s) :: add_break_if_none 1 (make prods) else if is_right_bracket s && is_next_terminal prods then (* Always no space after right bracked, but possibly a break *) - UnpTerminal s :: add_break_if_none 0 (make prods) + (None,UnpTerminal s) :: add_break_if_none 0 (make prods) else if is_left_bracket s && is_next_non_terminal prods then - UnpTerminal s :: make prods + (None,UnpTerminal s) :: make prods else if not (is_next_break prods) then (* Add rigid space, no break, unless user asked for something *) - UnpTerminal (s^" ") :: make prods + (None,UnpTerminal (s^" ")) :: make prods else (* Rely on user spaces *) - UnpTerminal s :: make prods + (None,UnpTerminal s) :: make prods | Terminal s :: prods -> (* Separate but do not cut a trailing sequence of terminal *) (match prods with - | Terminal _ :: _ -> UnpTerminal (s^" ") :: make prods - | _ -> UnpTerminal s :: make prods) + | Terminal _ :: _ -> (None,UnpTerminal (s^" ")) :: make prods + | _ -> (None,UnpTerminal s) :: make prods) | Break n :: prods -> add_break n (make prods) @@ -451,12 +454,12 @@ let make_hunks etyps symbols from = (* We add NonTerminal for simulation but remove it afterwards *) else snd (List.sep_last (make (sl@[NonTerminal m]))) in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,sl') + | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl') | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,sl') + UnpBinderListMetaVar (i,isopen,List.map snd sl') | _ -> assert false in - hunk :: make_with_space prods + (None,hunk) :: make_with_space prods | [] -> [] @@ -465,7 +468,7 @@ let make_hunks etyps symbols from = | Terminal s' :: prods'-> if is_operator s' then (* A rigid space before operator and a breakable after *) - UnpTerminal (" "^s') :: add_break_if_none 1 (make prods') + (None,UnpTerminal (" "^s')) :: add_break_if_none 1 (make prods') else if is_comma s' then (* No space whatsoever before comma *) make prods @@ -486,58 +489,63 @@ let make_hunks etyps symbols from = (* Build default printing rules from explicit format *) -let error_format () = user_err Pp.(str "The format does not match the notation.") +let error_format ?loc () = user_err ?loc Pp.(str "The format does not match the notation.") let rec split_format_at_ldots hd = function - | UnpTerminal s :: fmt when String.equal s (Id.to_string ldots_var) -> List.rev hd, fmt + | (loc,UnpTerminal s) :: fmt when String.equal s (Id.to_string ldots_var) -> loc, List.rev hd, fmt | u :: fmt -> check_no_ldots_in_box u; split_format_at_ldots (u::hd) fmt | [] -> raise Exit and check_no_ldots_in_box = function - | UnpBox (_,fmt) -> + | (_,UnpBox (_,fmt)) -> (try - let _ = split_format_at_ldots [] fmt in - user_err Pp.(str ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.")) + let loc,_,_ = split_format_at_ldots [] fmt in + user_err ?loc Pp.(str ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.")) with Exit -> ()) | _ -> () +let error_not_same ?loc () = + user_err ?loc Pp.(str "The format is not the same on the right- and left-hand sides of the special token \"..\".") + let skip_var_in_recursive_format = function - | UnpTerminal _ :: sl (* skip first var *) -> + | (_,UnpTerminal s) :: sl (* skip first var *) when not (List.for_all (fun c -> c = " ") (String.explode s)) -> (* To do, though not so important: check that the names match the names in the notation *) sl - | _ -> error_format () + | (loc,_) :: _ -> error_not_same ?loc () + | [] -> assert false let read_recursive_format sl fmt = let get_head fmt = let sl = skip_var_in_recursive_format fmt in - try split_format_at_ldots [] sl with Exit -> error_format () in + try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in let rec get_tail = function - | a :: sepfmt, b :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *) + | (loc,a) :: sepfmt, (_,b) :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *) | [], tail -> skip_var_in_recursive_format tail - | _ -> user_err Pp.(str "The format is not the same on the right and left hand side of the special token \"..\".") in - let slfmt, fmt = get_head fmt in + | (loc,_) :: _, ([] | (_,UnpTerminal _) :: _)-> error_not_same ?loc () + | _, (loc,_)::_ -> error_not_same ?loc () in + let loc, slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) let hunks_of_format (from,(vars,typs)) symfmt = let rec aux = function - | symbs, (UnpTerminal s' as u) :: fmt + | symbs, (_,(UnpTerminal s' as u)) :: fmt when String.equal s' (String.make (String.length s') ' ') -> let symbs, l = aux (symbs,fmt) in symbs, u :: l - | Terminal s :: symbs, (UnpTerminal s') :: fmt + | Terminal s :: symbs, (_,UnpTerminal s') :: fmt when String.equal s (String.drop_simple_quotes s') -> let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l - | NonTerminal s :: symbs, UnpTerminal s' :: fmt when Id.equal s (Id.of_string s') -> + | NonTerminal s :: symbs, (_,UnpTerminal s') :: fmt when Id.equal s (Id.of_string s') -> let i = index_id s vars in let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in let symbs, l = aux (symbs,fmt) in symbs, UnpMetaVar (i,prec) :: l - | symbs, UnpBox (a,b) :: fmt -> + | symbs, (_,UnpBox (a,b)) :: fmt -> let symbs', b' = aux (symbs,b) in let symbs', l = aux (symbs',fmt) in - symbs', UnpBox (a,b') :: l - | symbs, (UnpCut _ as u) :: fmt -> + symbs', UnpBox (a,List.map (fun x -> (None,x)) b') :: l + | symbs, (_,(UnpCut _ as u)) :: fmt -> let symbs, l = aux (symbs,fmt) in symbs, u :: l | SProdList (m,sl) :: symbs, fmt -> let i = index_id m vars in @@ -545,7 +553,7 @@ let hunks_of_format (from,(vars,typs)) symfmt = let _,prec = precedence_of_entry_type from typ in let slfmt,fmt = read_recursive_format sl fmt in let sl, slfmt = aux (sl,slfmt) in - if not (List.is_empty sl) then error_format (); + if not (List.is_empty sl) then error_format ?loc:(fst (List.last fmt)) (); let symbs, l = aux (symbs,fmt) in let hunk = match typ with | ETConstr _ -> UnpListMetaVar (i,prec,slfmt) @@ -555,7 +563,7 @@ let hunks_of_format (from,(vars,typs)) symfmt = | _ -> assert false in symbs, hunk :: l | symbs, [] -> symbs, [] - | _, _ -> error_format () + | _, fmt -> error_format ?loc:(fst (List.hd fmt)) () in match aux symfmt with | [], l -> l -- cgit v1.2.3