diff options
| -rw-r--r-- | configure.ml | 4 | ||||
| -rw-r--r-- | lib/loc.ml | 5 | ||||
| -rw-r--r-- | lib/loc.mli | 17 | ||||
| -rw-r--r-- | parsing/cLexer.ml4 | 311 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 3 | ||||
| -rw-r--r-- | parsing/compat.ml4 | 108 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 48 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 35 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 6 |
9 files changed, 299 insertions, 238 deletions
diff --git a/configure.ml b/configure.ml index 2e7bf1854..a1c243d65 100644 --- a/configure.ml +++ b/configure.ml @@ -550,9 +550,9 @@ let check_camlp5_version camlp5o = let version_line, _ = run ~err:StdOut camlp5o ["-v"] in let version = List.nth (string_split ' ' version_line) 2 in match string_split '.' version with - | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) -> + | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) -> printf "You have Camlp5 %s. Good!\n" version; version - | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n" + | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" let check_caml_version_for_camlp4 () = if caml_version_nums = [4;1;0] && !Prefs.debug && not !Prefs.force_caml_version then diff --git a/lib/loc.ml b/lib/loc.ml index afdab928c..0f9864a9a 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -8,7 +8,6 @@ (* Locations management *) - type t = { fname : string; (** filename *) line_nb : int; (** start line number *) @@ -19,7 +18,7 @@ type t = { ep : int; (** end position *) } -let create fname line_nb bol_pos (bp, ep) = { +let create fname line_nb bol_pos bp ep = { fname = fname; line_nb = line_nb; bol_pos = bol_pos; line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; } @@ -54,8 +53,6 @@ let merge loc1 loc2 = let unloc loc = (loc.bp, loc.ep) -let represent loc = (loc.fname, loc.line_nb, loc.bol_pos, loc.bp, loc.ep) - let dummy_loc = ghost let join_loc = merge diff --git a/lib/loc.mli b/lib/loc.mli index f39cd2670..c08e097a8 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -8,7 +8,15 @@ (** {5 Basic types} *) -type t +type t = { + fname : string; (** filename *) + line_nb : int; (** start line number *) + bol_pos : int; (** position of the beginning of start line *) + line_nb_last : int; (** end line number *) + bol_pos_last : int; (** position of the beginning of end line *) + bp : int; (** start position *) + ep : int; (** end position *) +} type 'a located = t * 'a (** Embed a location in a type *) @@ -17,9 +25,9 @@ type 'a located = t * 'a (** This is inherited from CAMPL4/5. *) -val create : string -> int -> int -> (int * int) -> t +val create : string -> int -> int -> int -> int -> t (** Create a location from a filename, a line number, a position of the - beginning of the line and a pair of start and end position *) + beginning of the line, a start and end position *) val unloc : t -> int * int (** Return the start and end position of a location *) @@ -35,9 +43,6 @@ val is_ghost : t -> bool val merge : t -> t -> t -val represent : t -> (string * int * int * int * int) -(** Return the arguments given in [create] *) - (** {5 Located exceptions} *) val add_loc : Exninfo.info -> t -> Exninfo.info diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 9a7aeaf0c..b04c7633a 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -9,6 +9,7 @@ open Pp open Util open Tok +open Compat (* Dictionaries: trees annotated with string options, each node being a map from chars to dictionaries (the subtrees). A trie, in other words. *) @@ -110,7 +111,12 @@ module Error = struct end open Error -let err loc str = Loc.raise (Loc.make_loc loc) (Error.E str) +let current_file = ref "" + +let set_current_file ~fname = + current_file := fname + +let err loc str = Loc.raise (Compat.to_coqloc loc) (Error.E str) let bad_token str = raise (Error.E (Bad_token str)) @@ -121,64 +127,68 @@ type token_kind = | AsciiChar | EmptyStream -let error_unsupported_unicode_character n unicode cs = +let error_unsupported_unicode_character loc n unicode cs = let bp = Stream.count cs in - err (bp,bp+n) (UnsupportedUnicode unicode) + let loc = set_loc_pos loc bp (bp+n) in + err loc (UnsupportedUnicode unicode) -let error_utf8 cs = +let error_utf8 loc cs = let bp = Stream.count cs in Stream.junk cs; (* consume the char to avoid read it and fail again *) - err (bp, bp+1) Illegal_character + let loc = set_loc_pos loc bp (bp+1) in + err loc Illegal_character -let utf8_char_size cs = function +let utf8_char_size loc cs = function (* Utf8 leading byte *) | '\x00'..'\x7F' -> 1 | '\xC0'..'\xDF' -> 2 | '\xE0'..'\xEF' -> 3 | '\xF0'..'\xF7' -> 4 - | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs + | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 loc cs let njunk n = Util.repeat n Stream.junk -let check_utf8_trailing_byte cs c = - if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 cs +let check_utf8_trailing_byte loc cs c = + if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 loc cs (* Recognize utf8 blocks (of length less than 4 bytes) *) (* but don't certify full utf8 compliance (e.g. no emptyness check) *) -let lookup_utf8_tail c cs = +let lookup_utf8_tail loc c cs = let c1 = Char.code c in - if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 cs + if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 loc cs else let n, unicode = if Int.equal (c1 land 0x20) 0 then match Stream.npeek 2 cs with | [_;c2] -> - check_utf8_trailing_byte cs c2; + check_utf8_trailing_byte loc cs c2; 2, (c1 land 0x1F) lsl 6 + (Char.code c2 land 0x3F) - | _ -> error_utf8 cs + | _ -> error_utf8 loc cs else if Int.equal (c1 land 0x10) 0 then match Stream.npeek 3 cs with | [_;c2;c3] -> - check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3; + check_utf8_trailing_byte loc cs c2; + check_utf8_trailing_byte loc cs c3; 3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 + (Char.code c3 land 0x3F) - | _ -> error_utf8 cs + | _ -> error_utf8 loc cs else match Stream.npeek 4 cs with | [_;c2;c3;c4] -> - check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3; - check_utf8_trailing_byte cs c4; + check_utf8_trailing_byte loc cs c2; + check_utf8_trailing_byte loc cs c3; + check_utf8_trailing_byte loc cs c4; 4, (c1 land 0x07) lsl 18 + (Char.code c2 land 0x3F) lsl 12 + (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F) - | _ -> error_utf8 cs + | _ -> error_utf8 loc cs in try Unicode.classify unicode, n with Unicode.Unsupported -> - njunk n cs; error_unsupported_unicode_character n unicode cs + njunk n cs; error_unsupported_unicode_character loc n unicode cs -let lookup_utf8 cs = +let lookup_utf8 loc cs = match Stream.peek cs with | Some ('\x00'..'\x7F') -> AsciiChar - | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs) + | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail loc c cs) | None -> EmptyStream let unlocated f x = f x @@ -189,7 +199,7 @@ let check_keyword str = let rec loop_symb = parser | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str | [< s >] -> - match unlocated lookup_utf8 s with + match unlocated lookup_utf8 Compat.CompatLoc.ghost s with | Utf8Token (_,n) -> njunk n s; loop_symb s | AsciiChar -> Stream.junk s; loop_symb s | EmptyStream -> () @@ -210,7 +220,7 @@ let check_ident str = | [< ' ('0'..'9' | ''') when intail; s >] -> loop_id true s | [< s >] -> - match unlocated lookup_utf8 s with + match unlocated lookup_utf8 Compat.CompatLoc.ghost s with | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s | Utf8Token (Unicode.IdentPart, n) when intail -> njunk n s; @@ -263,13 +273,13 @@ let get_buff len = String.sub !buff 0 len (* The classical lexer: idents, numbers, quoted strings, comments *) -let rec ident_tail len = parser +let rec ident_tail loc len = parser | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] -> - ident_tail (store len c) s + ident_tail loc (store len c) s | [< s >] -> - match lookup_utf8 s with + match lookup_utf8 loc s with | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) -> - ident_tail (nstore n len s) s + ident_tail loc (nstore n len s) s | _ -> len let check_no_char s = @@ -287,40 +297,43 @@ let is_gt3 = function | c::_ when c == '1' || c == '2' || c == '3' -> false | _ -> true -let check_gt3 l loc len = +let check_gt3 loc l len = if not (l == ['0']) && (is_teen l || is_gt3 l) then (false, len) else err loc (IncorrectIndex l) -let check_n n l loc len = +let check_n loc n l len = if List.hd l == n && not (is_teen l) then (false, len) else err loc (IncorrectIndex l) -let rec number_or_index bp l len = parser - | [< ' ('0'..'9' as c); s >] -> number_or_index bp (c::l) (store len c) s +let rec number_or_index loc bp l len = parser + | [< ' ('0'..'9' as c); s >] -> number_or_index loc bp (c::l) (store len c) s | [< s >] ep -> + let loc = set_loc_pos loc bp ep in match Stream.npeek 2 s with - | ['s';'t'] when check_no_char s -> njunk 2 s; check_n '1' l (bp,ep) len - | ['n';'d'] when check_no_char s -> njunk 2 s; check_n '2' l (bp,ep) len - | ['r';'d'] when check_no_char s -> njunk 2 s; check_n '3' l (bp,ep) len - | ['t';'h'] when check_no_char s -> njunk 2 s; check_gt3 l (bp,ep) len + | ['s';'t'] when check_no_char s -> njunk 2 s; check_n loc '1' l len + | ['n';'d'] when check_no_char s -> njunk 2 s; check_n loc '2' l len + | ['r';'d'] when check_no_char s -> njunk 2 s; check_n loc '3' l len + | ['t';'h'] when check_no_char s -> njunk 2 s; check_gt3 loc l len | _ -> true, len -let rec string in_comments bp len = parser +(* If the string being lexed is in a comment, [comm_level] is Some i with i the + current level of comments nesting. Otherwise, [comm_level] is None. *) +let rec string loc ~comm_level bp len = parser | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> - if esc then string in_comments bp (store len '"') s else len + if esc then string loc ~comm_level bp (store len '"') s else (loc, len) | [< ''('; s >] -> (parser | [< ''*'; s >] -> - string - (Option.map succ in_comments) + string loc + (Option.map succ comm_level) bp (store (store len '(') '*') s | [< >] -> - string in_comments bp (store len '(') s) s + string loc comm_level bp (store len '(') s) s | [< ''*'; s >] -> (parser | [< '')'; s >] -> - let () = match in_comments with + let () = match comm_level with | Some 0 -> Feedback.msg_warning (strbrk @@ -329,12 +342,23 @@ let rec string in_comments bp len = parser non-terminated string of the comment.") | _ -> () in - let in_comments = Option.map pred in_comments in - string in_comments bp (store (store len '*') ')') s + let comm_level = Option.map pred comm_level in + string loc comm_level bp (store (store len '*') ')') s | [< >] -> - string in_comments bp (store len '*') s) s - | [< 'c; s >] -> string in_comments bp (store len c) s - | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string + string loc comm_level bp (store len '*') s) s + | [< ''\n' as c; s >] ep -> + (* If we are parsing a comment, the string if not part of a token so we + update the first line of the location. Otherwise, we update the last + line. *) + let loc = + if Option.has_some comm_level then bump_loc_line loc ep + else bump_loc_line_last loc ep + in + string loc comm_level bp (store len c) s + | [< 'c; s >] -> string loc comm_level bp (store len c) s + | [< _ = Stream.empty >] ep -> + let loc = set_loc_pos loc bp ep in + err loc Unterminated_string (* Hook for exporting comment into xml theory files *) let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () @@ -400,98 +424,109 @@ let comment_stop ep = between_com := false (* Does not unescape!!! *) -let rec comm_string bp = parser - | [< ''"' >] -> push_string "\"" - | [< ''\\'; _ = +let rec comm_string loc bp = parser + | [< ''"' >] ep -> push_string "\""; loc + | [< ''\\'; loc = (parser [< ' ('"' | '\\' as c) >] -> let () = match c with | '"' -> real_push_char c | _ -> () in - real_push_char c - | [< >] -> real_push_char '\\'); s >] - -> comm_string bp s - | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string - | [< 'c; s >] -> real_push_char c; comm_string bp s - -let rec comment bp = parser bp2 + real_push_char c; loc + | [< >] -> real_push_char '\\'; loc); s >] + -> comm_string loc bp s + | [< _ = Stream.empty >] ep -> + let loc = set_loc_pos loc bp ep in + err loc Unterminated_string + | [< ''\n' as c; s >] ep -> real_push_char c; comm_string (bump_loc_line loc ep) bp s + | [< 'c; s >] -> real_push_char c; comm_string loc bp s + +let rec comment loc bp = parser bp2 | [< ''('; - _ = (parser - | [< ''*'; s >] -> push_string "(*"; comment bp s - | [< >] -> push_string "(" ); - s >] -> comment bp s + loc = (parser + | [< ''*'; s >] -> push_string "(*"; comment loc bp s + | [< >] -> push_string "("; loc ); + s >] -> comment loc bp s | [< ''*'; - _ = parser - | [< '')' >] -> push_string "*)"; - | [< s >] -> real_push_char '*'; comment bp s >] -> () + loc = parser + | [< '')' >] -> push_string "*)"; loc + | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc | [< ''"'; s >] -> - if Flags.do_beautify() then (push_string"\"";comm_string bp2 s) - else ignore (string (Some 0) bp2 0 s); - comment bp s - | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment - | [< 'z; s >] -> real_push_char z; comment bp s + let loc = + (* In beautify mode, the lexing differs between strings in comments and + regular strings (e.g. escaping). It seems wrong. *) + if Flags.do_beautify() then (push_string"\""; comm_string loc bp2 s) + else fst (string loc ~comm_level:(Some 0) bp2 0 s) + in + comment loc bp s + | [< _ = Stream.empty >] ep -> + let loc = set_loc_pos loc bp ep in + err loc Unterminated_comment + | [< ''\n' as z; s >] ep -> real_push_char z; comment (bump_loc_line loc ep) bp s + | [< 'z; s >] -> real_push_char z; comment loc bp s (* Parse a special token, using the [token_tree] *) (* Peek as much utf-8 lexemes as possible *) (* and retain the longest valid special token obtained *) -let rec progress_further last nj tt cs = - try progress_from_byte last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj) +let rec progress_further loc last nj tt cs = + try progress_from_byte loc last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj) with Failure _ -> last -and update_longest_valid_token last nj tt cs = +and update_longest_valid_token loc last nj tt cs = match tt.node with | Some _ as last' -> stream_njunk nj cs; - progress_further last' 0 tt cs + progress_further loc last' 0 tt cs | None -> - progress_further last nj tt cs + progress_further loc last nj tt cs (* nj is the number of char peeked since last valid token *) (* n the number of char in utf8 block *) -and progress_utf8 last nj n c tt cs = +and progress_utf8 loc last nj n c tt cs = try let tt = CharMap.find c tt.branch in if Int.equal n 1 then - update_longest_valid_token last (nj+n) tt cs + update_longest_valid_token loc last (nj+n) tt cs else match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with | l when Int.equal (List.length l) (n - 1) -> - List.iter (check_utf8_trailing_byte cs) l; + List.iter (check_utf8_trailing_byte loc cs) l; let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in - update_longest_valid_token last (nj+n) tt cs + update_longest_valid_token loc last (nj+n) tt cs | _ -> - error_utf8 cs + error_utf8 loc cs with Not_found -> last -and progress_from_byte last nj tt cs c = - progress_utf8 last nj (utf8_char_size cs c) c tt cs +and progress_from_byte loc last nj tt cs c = + progress_utf8 loc last nj (utf8_char_size loc cs c) c tt cs -let find_keyword id s = +let find_keyword loc id s = let tt = ttree_find !token_tree id in - match progress_further tt.node 0 tt s with + match progress_further loc tt.node 0 tt s with | None -> raise Not_found | Some c -> KEYWORD c -let process_sequence bp c cs = +let process_sequence loc bp c cs = let rec aux n cs = match Stream.peek cs with | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs - | _ -> BULLET (String.make n c), (bp, Stream.count cs) + | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs) in aux 1 cs (* Must be a special token *) -let process_chars bp c cs = - let t = progress_from_byte None (-1) !token_tree cs c in +let process_chars loc bp c cs = + let t = progress_from_byte loc None (-1) !token_tree cs c in let ep = Stream.count cs in match t with - | Some t -> (KEYWORD t, (bp, ep)) + | Some t -> (KEYWORD t, set_loc_pos loc bp ep) | None -> - let ep' = bp + utf8_char_size cs c in + let ep' = bp + utf8_char_size loc cs c in njunk (ep' - ep) cs; - err (bp, ep') Undefined_token + let loc = set_loc_pos loc bp ep' in + err loc Undefined_token let token_of_special c s = match c with | '.' -> FIELD s @@ -499,27 +534,27 @@ let token_of_special c s = match c with (* Parse what follows a dot / a dollar *) -let parse_after_special c bp = +let parse_after_special loc c bp = parser - | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail (store 0 d) >] -> + | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail loc (store 0 d) >] -> token_of_special c (get_buff len) | [< s >] -> - match lookup_utf8 s with + match lookup_utf8 loc s with | Utf8Token (Unicode.Letter, n) -> - token_of_special c (get_buff (ident_tail (nstore n 0 s) s)) - | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp c s) + token_of_special c (get_buff (ident_tail loc (nstore n 0 s) s)) + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp c s) (* Parse what follows a question mark *) -let parse_after_qmark bp s = +let parse_after_qmark loc bp s = match Stream.peek s with | Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK | None -> KEYWORD "?" | _ -> - match lookup_utf8 s with + match lookup_utf8 loc s with | Utf8Token (Unicode.Letter, _) -> LEFTQMARK | AsciiChar | Utf8Token _ | EmptyStream -> - fst (process_chars bp '?' s) + fst (process_chars loc bp '?' s) let blank_or_eof cs = match Stream.peek cs with @@ -529,69 +564,72 @@ let blank_or_eof cs = (* Parse a token in a char stream *) -let rec next_token = parser bp - | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> - comm_loc bp; push_char c; next_token s - | [< ''.' as c; t = parse_after_special c bp; s >] ep -> +let rec next_token loc = parser bp + | [< ''\n' as c; s >] ep -> + comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s + | [< '' ' | '\t' | '\r' as c; s >] -> + comm_loc bp; push_char c; next_token loc s + | [< ''.' as c; t = parse_after_special loc c bp; s >] ep -> comment_stop bp; (* We enforce that "." should either be part of a larger keyword, for instance ".(", or followed by a blank or eof. *) let () = match t with | KEYWORD ("." | "...") -> - if not (blank_or_eof s) then err (bp,ep+1) Undefined_token; - between_com := true; + if not (blank_or_eof s) then + err (set_loc_pos loc bp (ep+1)) Undefined_token; + between_com := true; | _ -> () in - (t, (bp,ep)) + (t, set_loc_pos loc bp ep) | [< ' ('-'|'+'|'*' as c); s >] -> let t,new_between_com = - if !between_com then process_sequence bp c s,true - else process_chars bp c s,false + if !between_com then process_sequence loc bp c s, true + else process_chars loc bp c s,false in comment_stop bp; between_com := new_between_com; t | [< ''?'; s >] ep -> - let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp)) + let t = parse_after_qmark loc bp s in + comment_stop bp; (t, set_loc_pos loc ep bp) | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); - len = ident_tail (store 0 c); s >] ep -> + len = ident_tail loc (store 0 c); s >] ep -> let id = get_buff len in comment_stop bp; - (try find_keyword id s with Not_found -> IDENT id), (bp, ep) - | [< ' ('0'..'9' as c); (b,len) = number_or_index bp [c] (store 0 c) >] ep -> + (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep + | [< ' ('0'..'9' as c); (b,len) = number_or_index loc bp [c] (store 0 c) >] ep -> comment_stop bp; - (if b then INT (get_buff len) else INDEX (get_buff len)), (bp, ep) - | [< ''\"'; len = string None bp 0 >] ep -> + (if b then INT (get_buff len) else INDEX (get_buff len)), set_loc_pos loc bp ep + | [< ''\"'; (loc,len) = string loc None bp 0 >] ep -> comment_stop bp; - (STRING (get_buff len), (bp, ep)) + (STRING (get_buff len), set_loc_pos loc bp ep) | [< ' ('(' as c); t = parser | [< ''*'; s >] -> comm_loc bp; push_string "(*"; - comment bp s; - next_token s - | [< t = process_chars bp c >] -> comment_stop bp; t >] -> + let loc = comment loc bp s in next_token loc s + | [< t = process_chars loc bp c >] -> comment_stop bp; t >] -> t | [< s >] -> - match lookup_utf8 s with + match lookup_utf8 loc s with | Utf8Token (Unicode.Letter, n) -> - let len = ident_tail (nstore n 0 s) s in + let len = ident_tail loc (nstore n 0 s) s in let id = get_buff len in let ep = Stream.count s in comment_stop bp; - (try find_keyword id s with Not_found -> IDENT id), (bp, ep) + (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) -> - let t = process_chars bp (Stream.next s) s in + let t = process_chars loc bp (Stream.next s) s in let new_between_com = match t with (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in comment_stop bp; between_com := new_between_com; t | EmptyStream -> - comment_stop bp; (EOI, (bp, bp + 1)) + comment_stop bp; (EOI, set_loc_pos loc bp (bp+1)) (* (* Debug: uncomment this for tracing tokens seen by coq...*) -let next_token s = - let (t,(bp,ep)) = next_token s in Printf.eprintf "[%s]\n%!" (Tok.to_string t); - (t,(bp,ep)) -*) +let next_token loc s = + let (t,loc as r) = next_token loc s in + Printf.eprintf "(line %i, %i-%i)[%s]\n%!" (Ploc.line_nb loc) (Ploc.first_pos loc) (Ploc.last_pos loc) (Tok.to_string t); + r *) (* Location table system for creating tables associating a token count to its location in a char stream (the source) *) @@ -640,11 +678,13 @@ let token_text = function let func cs = let loct = loct_create () in + let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in let ts = Stream.from (fun i -> - let (tok, loc) = next_token cs in - loct_add loct i (Compat.make_loc loc); Some tok) + let (tok, loc) = next_token !cur_loc cs in + cur_loc := Compat.after loc; + loct_add loct i loc; Some tok) in current_location_table := loct; (ts, loct_func loct) @@ -680,16 +720,19 @@ module Token = struct end end -let mk () _init_loc(*FIXME*) cs = +let mk () = let loct = loct_create () in - let rec self = + let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in + current_location_table := loct; + let rec self init_loc (* FIXME *) = parser i - [< (tok, loc) = next_token; s >] -> - let loc = Compat.make_loc loc in - loct_add loct i loc; - [< '(tok, loc); self s >] + [< (tok, loc) = next_token !cur_loc; s >] -> + cur_loc := Compat.set_loc_file loc !current_file; + loct_add loct i loc; + [< '(tok, loc); self init_loc s >] | [< >] -> [< >] - in current_location_table := loct; self cs + in + self END diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 24b0ec847..d99ba3557 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -17,6 +17,9 @@ type location_table val location_table : unit -> location_table val restore_location_table : location_table -> unit +(** [set_current_file fname] sets the filename in locations emitted by the lexer *) +val set_current_file : fname:string -> unit + val check_ident : string -> unit val is_ident : string -> bool val check_keyword : string -> unit diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 2b67693d2..9eb07990e 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -20,17 +20,49 @@ end exception Exc_located = Ploc.Exc -IFDEF CAMLP5_6_00 THEN -let ploc_file_name = Ploc.file_name -ELSE -let ploc_file_name _ = "" -END - let to_coqloc loc = - Loc.create (ploc_file_name loc) (Ploc.line_nb loc) - (Ploc.bol_pos loc) (Ploc.first_pos loc, Ploc.last_pos loc) + { Loc.fname = Ploc.file_name loc; + Loc.line_nb = Ploc.line_nb loc; + Loc.bol_pos = Ploc.bol_pos loc; + Loc.bp = Ploc.first_pos loc; + Loc.ep = Ploc.last_pos loc; + Loc.line_nb_last = Ploc.line_nb_last loc; + Loc.bol_pos_last = Ploc.bol_pos_last loc; } + +let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc fname line_nb bol_pos (bp, ep) "" + +(* Update a loc without allocating an intermediate pair *) +let set_loc_pos loc bp ep = + let open Ploc in sub loc (bp - first_pos loc) (ep - bp) + +(* Increase line number by 1 and update position of beginning of line *) +let bump_loc_line loc bol_pos = + Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos + (Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc) + +(* Same as [bump_loc_line], but for the last line in location *) +(* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop, + so we have to resort to a hack merging two locations. *) +(* Warning: [bump_loc_line_last] changes the end position. You may need to call + [set_loc_pos] to fix it. *) +let bump_loc_line_last loc bol_pos = + let loc' = + Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos + (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc) + in + Ploc.encl loc loc' + +let set_loc_file loc fname = + Ploc.make_loc fname (Ploc.line_nb loc) (Ploc.bol_pos loc) + (Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc) -let make_loc = Ploc.make_unlined +(* For some reason, the [Ploc.after] function of Camlp5 does not update line + numbers, so we define our own function that does it. *) +let after loc = + let line_nb = Ploc.line_nb_last loc in + let bol_pos = Ploc.bol_pos_last loc in + Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos + (Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc) ELSE @@ -39,11 +71,41 @@ module CompatLoc = Camlp4.PreCast.Loc exception Exc_located = CompatLoc.Exc_located let to_coqloc loc = - Loc.create (CompatLoc.file_name loc) (CompatLoc.start_line loc) - (CompatLoc.start_bol loc) (CompatLoc.start_off loc, CompatLoc.stop_off loc) - -let make_loc (start, stop) = - CompatLoc.of_tuple ("", 0, 0, start, 0, 0, stop, false) + { Loc.fname = CompatLoc.file_name loc; + Loc.line_nb = CompatLoc.start_line loc; + Loc.bol_pos = CompatLoc.start_bol loc; + Loc.bp = CompatLoc.start_off loc; + Loc.ep = CompatLoc.stop_off loc; + Loc.line_nb_last = CompatLoc.stop_line loc; + Loc.bol_pos_last = CompatLoc.stop_bol loc; } + +let make_loc fname line_nb bol_pos start stop = + CompatLoc.of_tuple (fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false) + +let set_loc_pos loc bp ep = + let open CompatLoc in + of_tuple (file_name loc, start_line loc, start_bol loc, bp, + stop_line loc, stop_bol loc, ep, is_ghost loc) + +let bump_loc_line loc bol_pos = + let open CompatLoc in + of_tuple (file_name loc, start_line loc + 1, bol_pos, start_off loc, + start_line loc + 1, bol_pos, stop_off loc, is_ghost loc) + +let bump_loc_line_last loc bol_pos = + let open CompatLoc in + of_tuple (file_name loc, start_line loc, start_bol loc, start_off loc, + stop_line loc + 1, bol_pos, stop_off loc, is_ghost loc) + +let set_loc_file loc fname = + let open CompatLoc in + of_tuple (fname, start_line loc, start_bol loc, start_off loc, + stop_line loc, stop_bol loc, stop_off loc, is_ghost loc) + +let after loc = + let open CompatLoc in + of_tuple (file_name loc, stop_line loc, stop_bol loc, stop_off loc, + stop_line loc, stop_bol loc, stop_off loc, is_ghost loc) END @@ -131,11 +193,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in Loc.raise loc e -IFDEF CAMLP5_6_02_1 THEN let entry_print ft x = Entry.print ft x -ELSE - let entry_print _ x = Entry.print x -END let srules' = Gramext.srules let parse_tokens_after_filter = Entry.parse_token end @@ -216,13 +274,13 @@ ELSE | tok -> Gramext.Stoken (Tok.equal tok, G.Token.to_string tok) END -IFDEF CAMLP5_6_00 THEN - let slist0sep (x, y) = Gramext.Slist0sep (x, y, false) - let slist1sep (x, y) = Gramext.Slist1sep (x, y, false) -ELSE - let slist0sep (x, y) = Gramext.Slist0sep (x, y) - let slist1sep (x, y) = Gramext.Slist1sep (x, y) -END + IFDEF CAMLP5 THEN + let slist0sep (x, y) = Gramext.Slist0sep (x, y, false) + let slist1sep (x, y) = Gramext.Slist1sep (x, y, false) + ELSE + let slist0sep (x, y) = Gramext.Slist0sep (x, y) + let slist1sep (x, y) = Gramext.Slist1sep (x, y) + END let snterml (x, y) = Gramext.Snterml (x, y) let snterm x = Gramext.Snterm x diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 1fe30217d..00e0219f1 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -152,38 +152,21 @@ let print_highlight_location ib loc = (* Functions to report located errors in a file. *) -let print_location_in_file {outer=s;inner=fname} loc = - let errstrm = str"Error while reading " ++ str s in +let print_location_in_file loc = + let fname = loc.Loc.fname in + let errstrm = str"Error while reading " ++ str fname in if Loc.is_ghost loc then hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl () else - let errstrm = - if String.equal s fname then mt() else errstrm ++ str":" ++ fnl() + let errstrm = mt () + (* if String.equal outer_fname fname then mt() else errstrm ++ str":" ++ fnl() *) in - let (bp,ep) = Loc.unloc loc in - let line_of_pos lin bol cnt = - try - let ic = open_in fname in - let rec line_of_pos lin bol cnt = - if cnt < bp then - if input_char ic == '\n' - then line_of_pos (lin + 1) (cnt +1) (cnt+1) - else line_of_pos lin bol (cnt+1) - else (lin, bol) - in - let rc = line_of_pos lin bol cnt in - close_in ic; - rc - with Sys_error _ -> 0, 0 in - try - let (line, bol) = line_of_pos 1 0 0 in - hov 0 (* No line break so as to follow emacs error message format *) - (errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++ - str", line " ++ int line ++ str", characters " ++ - Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++ - fnl () - with e when Errors.noncritical e -> - hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl () + let open Loc in + hov 0 (* No line break so as to follow emacs error message format *) + (errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++ + str", line " ++ int loc.line_nb ++ str", characters " ++ + Cerrors.print_loc (Loc.make_loc (loc.bp-loc.bol_pos,loc.ep-loc.bol_pos))) ++ str":" ++ + fnl () let valid_buffer_loc ib loc = not (Loc.is_ghost loc) && @@ -264,12 +247,13 @@ let locate_exn = function let print_toplevel_error (e, info) = let loc = Option.default Loc.ghost (Loc.get_loc info) in - let locmsg = match Vernac.get_exn_files info with - | Some files -> print_location_in_file files loc - | None -> + let fname = loc.Loc.fname in + let locmsg = + if String.equal fname "" then if locate_exn e && valid_buffer_loc top_buffer loc then - print_highlight_location top_buffer loc + print_highlight_location top_buffer loc else mt () + else print_location_in_file loc in locmsg ++ Errors.iprint (e, info) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9c3b170b9..ac9293d5f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -65,26 +65,6 @@ let _ = Goptions.optread = (fun () -> !atomic_load); Goptions.optwrite = ((:=) atomic_load) } -(* In case of error, register the file being currently Load'ed and the - inner file in which the error has been encountered. Any intermediate files - between the two are discarded. *) - -type location_files = { outer : string; inner : string } - -let files_of_exn : location_files Exninfo.t = Exninfo.make () - -let get_exn_files e = Exninfo.get e files_of_exn - -let add_exn_files e f = Exninfo.add e files_of_exn f - -let enrich_with_file f (e, info) = - let inner = match get_exn_files info with None -> f | Some x -> x.inner in - (e, add_exn_files info { outer = f; inner }) - -let raise_with_file f e = iraise (enrich_with_file f e) - -let cur_file = ref None - let disable_drop = function | Drop -> Errors.error "Drop is forbidden." | e -> e @@ -100,6 +80,7 @@ let open_file_twice_if verbosely longfname = let in_chan = open_utf8_file_in longfname in let verb_ch = if verbosely then Some (open_utf8_file_in longfname) else None in + CLexer.set_current_file longfname; let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in (in_chan, longfname, (po, verb_ch)) @@ -244,7 +225,6 @@ and read_vernac_file verbosely s = user_error loc "Navigation commands forbidden in files" in let (in_chan, fname, input) = open_file_twice_if verbosely s in - cur_file := Some fname; try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) @@ -258,10 +238,10 @@ and read_vernac_file verbosely s = close_input in_chan input; (* we must close the file first *) match e with | End_of_input -> - cur_file := None; if do_beautify () then pr_new_syntax (Loc.make_loc (max_int,max_int)) None - | _ -> raise_with_file fname (disable_drop e, info) + | reraise -> + iraise (disable_drop e, info) (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit] It executes one vernacular command. By default the command is @@ -290,7 +270,7 @@ let load_vernac verb file = with any -> let (e, info) = Errors.push any in if !Flags.beautify_file then close_out !chan_beautify; - raise_with_file file (disable_drop e, info) + iraise (disable_drop e, info) let ensure_ext ext f = if Filename.check_suffix f ext then f @@ -389,8 +369,5 @@ let compile v f = compile v f; CoqworkmgrApi.giveback 1 -let () = Hook.set Stm.process_error_hook (fun e -> - match !cur_file with - | None -> Cerrors.process_vernac_interp_error e - | Some f -> enrich_with_file f (Cerrors.process_vernac_interp_error e) -) +let () = Hook.set Stm.process_error_hook + Cerrors.process_vernac_interp_error diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 008d7a31a..7bfddd947 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -38,9 +38,3 @@ val load_vernac : bool -> string -> unit val compile : bool -> string -> unit val is_navigation_vernac : Vernacexpr.vernac_expr -> bool - -(** Has an exception been annotated with some file locations ? *) - -type location_files = { outer : string; inner : string } - -val get_exn_files : Exninfo.info -> location_files option |