Commit 39dd2d39 by POTTIER Francois

Added [loop_handle_undo].

parent 1ed5b5f1
......@@ -122,6 +122,7 @@
* Suite des patchs de Frédéric Bour.
API d'inspection complète.
Documenter loop_handle_undo.
Exposer le nombre d'états (pour la mémoisation).
Idem pour les productions.
Fonctions d'affichage pour les types terminal, nonterminal, etc.?
......
......@@ -167,53 +167,29 @@ module Make
) []
)
(* The following is a custom version of the loop found in [Engine]. It
drives the parser in the usual way, but records the last [InputNeeded]
checkpoint. If a syntax error is detected, it goes back to this
checkpoint and analyzes it in order to produce a meaningful
diagnostic. *)
(* We drive the parser in the usual way, but records the last [InputNeeded]
checkpoint. If a syntax error is detected, we go back to this checkpoint
and analyze it in order to produce a meaningful diagnostic. *)
exception Error of (Lexing.position * Lexing.position) * explanation list
(* TEMPORARY why loop-style? we should offer a simplified incremental API *)
type 'a checkpoint = {
inputneeded: 'a I.checkpoint;
current: 'a I.checkpoint
}
let rec loop (read : supplier) ({ inputneeded; current } : 'a checkpoint) : 'a =
match current with
| InputNeeded _ ->
(* Update the last recorded [InputNeeded] checkpoint. *)
let inputneeded = current in
let triple = read() in
let current = offer current triple in
loop read { inputneeded; current }
| Shifting _
| AboutToReduce _ ->
let current = resume current in
loop read { inputneeded; current }
| HandlingError env ->
(* The parser signals a syntax error. Note the position of the
problematic token, which is useful. Then, go back to the
checkpoint and investigate. *)
let (startp, _) as positions = positions env in
raise (Error (positions, investigate startp inputneeded))
| Accepted v ->
v
| Rejected ->
(* The parser rejects this input. This cannot happen, because
we stop as soon as the parser reports [HandlingError]. *)
assert false
let entry (start : 'a I.checkpoint) lexer lexbuf =
(* The parser cannot accept or reject before it asks for the very first
character of input. (Indeed, we statically reject a symbol that
generates the empty language or the singleton language {epsilon}.)
So, [start] must be [InputNeeded _]. *)
assert (match start with InputNeeded _ -> true | _ -> false);
loop (lexer_lexbuf_to_supplier lexer lexbuf) { inputneeded = start; current = start }
let fail (inputneeded : 'a I.checkpoint) (checkpoint : 'a I.checkpoint) =
(* The parser signals a syntax error. Note the position of the
problematic token, which is useful. Then, go back to the
last [InputNeeded] checkpoint and investigate. *)
match checkpoint with
| HandlingError env ->
let (startp, _) as positions = positions env in
raise (Error (positions, investigate startp inputneeded))
| _ ->
assert false
in
I.loop_handle_undo
(fun v -> v)
fail
(lexer_lexbuf_to_supplier lexer lexbuf)
start
(* TEMPORARY could also publish a list of the terminal symbols that
do not cause an error *)
......
......@@ -107,6 +107,24 @@ module type INCREMENTAL_ENGINE = sig
('a checkpoint -> 'answer) ->
supplier -> 'a checkpoint -> 'answer
(* [loop_handle_undo] is analogous to [loop_handle], except it passes a pair
of checkpoints to the failure continuation.
The first (and oldest) checkpoint is the last [InputNeeded] checkpoint that
was encountered before the error was detected. The second (and newest)
checkpoint is where the error was detected, as in [loop_handle]. Going back
to the first checkpoint can be thought of as undoing any reductions that
were performed after seeing the problematic token. (These reductions must
be default reductions or spurious reductions.)
[loop_handle_undo] must initially be applied to an [InputNeeded] checkpoint.
The parser's initial checkpoints satisfy this constraint. *)
val loop_handle_undo:
('a -> 'answer) ->
('a checkpoint -> 'a checkpoint -> 'answer) ->
supplier -> 'a checkpoint -> 'answer
(* The abstract type ['a lr1state] describes the non-initial states of the
LR(1) automaton. The index ['a] represents the type of the semantic value
associated with this state's incoming symbol. *)
......
......@@ -515,16 +515,11 @@ module Make (T : TABLE) = struct
let rec loop_handle succeed fail read checkpoint =
match checkpoint with
| InputNeeded _ ->
(* The parser needs a token. Request one from the lexer,
and offer it to the parser, which will produce a new
checkpoint. Then, repeat. *)
let triple = read() in
let checkpoint = offer checkpoint triple in
loop_handle succeed fail read checkpoint
| Shifting _
| AboutToReduce _ ->
(* The parser has suspended itself, but does not need
new input. Just resume the parser. Then, repeat. *)
let checkpoint = resume checkpoint in
loop_handle succeed fail read checkpoint
| HandlingError _
......@@ -532,10 +527,54 @@ module Make (T : TABLE) = struct
(* The parser has detected an error. Invoke the failure continuation. *)
fail checkpoint
| Accepted v ->
(* The parser has succeeded and produced a semantic value.
Return this semantic value to the user. *)
(* The parser has succeeded and produced a semantic value. Invoke the
success continuation. *)
succeed v
(* --------------------------------------------------------------------------- *)
(* [loop_handle_undo] is analogous to [loop_handle], except it passes a pair
of checkpoints to the failure continuation.
The first (and oldest) checkpoint is the last [InputNeeded] checkpoint that
was encountered before the error was detected. The second (and newest)
checkpoint is where the error was detected, as in [loop_handle]. Going back
to the first checkpoint can be thought of as undoing any reductions that
were performed after seeing the problematic token. (These reductions must
be default reductions or spurious reductions.) *)
let rec loop_handle_undo succeed fail read (inputneeded, checkpoint) =
match checkpoint with
| InputNeeded _ ->
(* Update the last recorded [InputNeeded] checkpoint. *)
let inputneeded = checkpoint in
let triple = read() in
let checkpoint = offer checkpoint triple in
loop_handle_undo succeed fail read (inputneeded, checkpoint)
| Shifting _
| AboutToReduce _ ->
let checkpoint = resume checkpoint in
loop_handle_undo succeed fail read (inputneeded, checkpoint)
| HandlingError _
| Rejected ->
fail inputneeded checkpoint
| Accepted v ->
succeed v
(* For simplicity, we publish a version of [loop_handle_undo] that takes a
single checkpoint as an argument, instead of a pair of checkpoints. We
check that the argument is [InputNeeded _], and duplicate it. *)
(* The parser cannot accept or reject before it asks for the very first
character of input. (Indeed, we statically reject a symbol that
generates the empty language or the singleton language {epsilon}.)
So, the [start] checkpoint must match [InputNeeded _]. Hence, it is
permitted to call [loop_handle_undo] with a [start] checkpoint. *)
let loop_handle_undo succeed fail read checkpoint =
assert (match checkpoint with InputNeeded _ -> true | _ -> false);
loop_handle_undo succeed fail read (checkpoint, checkpoint)
(* --------------------------------------------------------------------------- *)
(* The type ['a lr1state] describes the (non-initial) states of the LR(1)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment