Revision ca7ff3f7
Added by Lélio Brun 7 months ago
| src/parsers/parse.ml | ||
|---|---|---|
| 9 | 9 |
(* *) |
| 10 | 10 |
(********************************************************************) |
| 11 | 11 |
open Utils.Format |
| 12 |
|
|
| 13 | 12 |
module I = Parser_lustre_table.MenhirInterpreter |
| 14 | 13 |
module Inc = Parser_lustre_table.Incremental |
| 15 | 14 |
module E = MenhirLib.ErrorReports |
| ... | ... | |
| 17 | 16 |
|
| 18 | 17 |
exception Error |
| 19 | 18 |
|
| 20 |
type start_symbol = |
|
| 21 |
| Header |
|
| 22 |
| Program |
|
| 19 |
type start_symbol = Header | Program |
|
| 23 | 20 |
|
| 24 |
(* [env checkpoint] extracts a parser environment out of a checkpoint, |
|
| 25 |
which must be of the form [HandlingError env]. *)
|
|
| 21 |
(* [env checkpoint] extracts a parser environment out of a checkpoint, which
|
|
| 22 |
must be of the form [HandlingError env]. *) |
|
| 26 | 23 |
let env checkpoint = |
| 27 |
match checkpoint with |
|
| 28 |
| I.HandlingError env -> env |
|
| 29 |
| _ -> assert false |
|
| 24 |
match checkpoint with I.HandlingError env -> env | _ -> assert false |
|
| 30 | 25 |
|
| 31 | 26 |
(* [state checkpoint] extracts the number of the current state out of a |
| 32 | 27 |
checkpoint. *) |
| ... | ... | |
| 35 | 30 |
| Some (I.Element (s, _, _, _)) -> |
| 36 | 31 |
I.number s |
| 37 | 32 |
| None -> |
| 38 |
(* Hmm... The parser is in its initial state. The incremental API |
|
| 39 |
currently lacks a way of finding out the number of the initial
|
|
| 40 |
state. It is usually 0, so we return 0. This is unsatisfactory
|
|
| 41 |
and should be fixed in the future. *)
|
|
| 42 |
0
|
|
| 33 |
(* Hmm... The parser is in its initial state. The incremental API currently
|
|
| 34 |
lacks a way of finding out the number of the initial state. It is usually
|
|
| 35 |
0, so we return 0. This is unsatisfactory and should be fixed in the
|
|
| 36 |
future. *) |
|
| 37 |
0 |
|
| 43 | 38 |
|
| 44 |
(* [show text (pos1, pos2)] displays a range of the input text [text] |
|
| 45 |
delimited by the positions [pos1] and [pos2]. *)
|
|
| 39 |
(* [show text (pos1, pos2)] displays a range of the input text [text] delimited
|
|
| 40 |
by the positions [pos1] and [pos2]. *) |
|
| 46 | 41 |
let show text positions = |
| 47 |
E.extract text positions |
|
| 48 |
|> E.sanitize |
|
| 49 |
|> E.compress |
|
| 50 |
|> E.shorten 20 (* max width 43 *) |
|
| 42 |
E.extract text positions |> E.sanitize |> E.compress |> E.shorten 20 |
|
| 43 |
(* max width 43 *) |
|
| 51 | 44 |
|
| 52 | 45 |
(* (\* [get text checkpoint i] extracts and shows the range of the input text that |
| 53 | 46 |
* corresponds to the [i]-th stack cell. The top stack cell is numbered zero. *\) |
| ... | ... | |
| 63 | 56 |
* "???" *) |
| 64 | 57 |
|
| 65 | 58 |
module type LEXER = sig |
| 66 |
val token: Lexing.lexbuf -> Parser_lustre.token |
|
| 59 |
val token : Lexing.lexbuf -> Parser_lustre.token |
|
| 60 |
|
|
| 67 | 61 |
type error |
| 62 |
|
|
| 68 | 63 |
exception Error of Location.t * error |
| 69 |
val pp_error: formatter -> error -> unit |
|
| 64 |
|
|
| 65 |
val pp_error : formatter -> error -> unit |
|
| 70 | 66 |
end |
| 71 | 67 |
|
| 72 | 68 |
let reparse (module Lexer : LEXER) ?orig_loc filename start src = |
| 73 | 69 |
(* Allocate and initialize a lexing buffer. *) |
| 74 | 70 |
let lexbuf = L.init filename (Lexing.from_string src) in |
| 75 |
(* Wrap the lexer and lexbuf together into a supplier, that is, a |
|
| 76 |
function of type [unit -> token * position * position]. *)
|
|
| 71 |
(* Wrap the lexer and lexbuf together into a supplier, that is, a function of
|
|
| 72 |
type [unit -> token * position * position]. *) |
|
| 77 | 73 |
let supplier = I.lexer_lexbuf_to_supplier Lexer.token lexbuf in |
| 78 |
(* Equip the supplier with a two-place buffer that records the positions |
|
| 79 |
of the last two tokens. This is useful when a syntax error occurs, as
|
|
| 80 |
these are the token just before and just after the error. *)
|
|
| 74 |
(* Equip the supplier with a two-place buffer that records the positions of
|
|
| 75 |
the last two tokens. This is useful when a syntax error occurs, as these
|
|
| 76 |
are the token just before and just after the error. *) |
|
| 81 | 77 |
let buffer, supplier = E.wrap_supplier supplier in |
| 82 | 78 |
(* Fetch the parser's initial checkpoint. *) |
| 83 | 79 |
let checkpoint = start lexbuf.lex_curr_p in |
| 84 | 80 |
(* [succeed v] is invoked when the parser has succeeded and produced a |
| 85 | 81 |
semantic value [v]. In our setting, this cannot happen, since the |
| 86 |
table-based parser is invoked only when we know that there is a |
|
| 87 |
syntax error in the input file. *)
|
|
| 82 |
table-based parser is invoked only when we know that there is a syntax
|
|
| 83 |
error in the input file. *) |
|
| 88 | 84 |
let succeed _v = assert false in |
| 89 | 85 |
(* [fail checkpoint] is invoked when parser has encountered a syntax error. *) |
| 90 | 86 |
let fail (checkpoint : _ I.checkpoint) = |
| 91 | 87 |
(* Indicate where in the input file the error occurred. *) |
| 92 | 88 |
let loc = E.last buffer in |
| 93 |
let loc = match orig_loc with Some loc' -> Location.shift loc' loc | _ -> loc in |
|
| 89 |
let loc = |
|
| 90 |
match orig_loc with Some loc' -> Location.shift loc' loc | _ -> loc |
|
| 91 |
in |
|
| 94 | 92 |
(* Show the tokens just before and just after the error. *) |
| 95 | 93 |
let indication = E.show (show src) buffer in |
| 96 | 94 |
(* Fetch an error message from the database. *) |
| ... | ... | |
| 98 | 96 |
(* Expand away the $i keywords that might appear in the message. *) |
| 99 | 97 |
(* let message = E.expand (get src checkpoint) message in *) |
| 100 | 98 |
(* Show these three components. *) |
| 101 |
eprintf "@[<v>%aSyntax error %s.@,%s@]@." |
|
| 102 |
Location.pp_loc loc indication message;
|
|
| 99 |
eprintf "@[<v>%aSyntax error %s.@,%s@]@." Location.pp_loc loc indication
|
|
| 100 |
message; |
|
| 103 | 101 |
raise Error |
| 104 | 102 |
in |
| 105 | 103 |
(* Run the parser. *) |
| 106 |
(* We do not handle [Lexer.Error] because we know that we will not |
|
| 107 |
encounter a lexical error during this second parsing run. *)
|
|
| 104 |
(* We do not handle [Lexer.Error] because we know that we will not encounter a
|
|
| 105 |
lexical error during this second parsing run. *) |
|
| 108 | 106 |
I.loop_handle succeed fail supplier checkpoint |
| 109 | 107 |
|
| 110 |
let parse (module Lexer : LEXER) ?orig_loc filename src lexbuf start_mono start_incr = |
|
| 108 |
let parse (module Lexer : LEXER) ?orig_loc filename src lexbuf start_mono |
|
| 109 |
start_incr = |
|
| 111 | 110 |
let lexbuf = L.init filename lexbuf in |
| 112 |
try |
|
| 113 |
start_mono Lexer.token lexbuf |
|
| 114 |
with |
|
| 111 |
try start_mono Lexer.token lexbuf with |
|
| 115 | 112 |
| Lexer.Error (loc, err) -> |
| 116 |
let loc = match orig_loc with Some loc' -> Location.shift loc' loc | _ -> loc in |
|
| 117 |
eprintf "@[<v>%aSyntax error.@,%a@]@." |
|
| 118 |
Location.pp_loc loc Lexer.pp_error err; |
|
| 113 |
let loc = |
|
| 114 |
match orig_loc with Some loc' -> Location.shift loc' loc | _ -> loc |
|
| 115 |
in |
|
| 116 |
eprintf "@[<v>%aSyntax error.@,%a@]@." Location.pp_loc loc Lexer.pp_error |
|
| 117 |
err; |
|
| 119 | 118 |
raise Error |
| 120 | 119 |
| Parser_lustre.Error -> |
| 121 | 120 |
reparse (module Lexer) ?orig_loc filename start_incr src |
| 122 | 121 |
|
| 123 | 122 |
let parse_filename (module Lexer : LEXER) filename start = |
| 124 |
let start_mono, start_incr = match start with |
|
| 125 |
| Header -> Parser_lustre.header, Inc.header |
|
| 126 |
| Program -> Parser_lustre.prog, Inc.prog |
|
| 123 |
let start_mono, start_incr = |
|
| 124 |
match start with |
|
| 125 |
| Header -> |
|
| 126 |
Parser_lustre.header, Inc.header |
|
| 127 |
| Program -> |
|
| 128 |
Parser_lustre.prog, Inc.prog |
|
| 127 | 129 |
in |
| 128 | 130 |
let src, lexbuf = L.read filename in |
| 129 | 131 |
Location.set_input filename; |
Also available in: Unified diff
reformatting