Commit 75c50174 authored by POTTIER Francois's avatar POTTIER Francois

The incremental API is now based on a private type 'a result.

The type env no longer needs to be parameterized. This makes the API safe (and simpler). There a slight runtime cost (e.g., from 4.6s to 4.7 seconds).
parent 63e0bd9b
2014/12/29:
Incompatible change of the incremental API.
The API now exposes reduction events.
The type 'a result is now private.
The type env is no longer parameterized.
[handle] is renamed to [resume].
[offer] and [resume] now expect a result, not an environment.
2014/12/22:
Documented the Coq back-end (designed and implemented by Jacques-Henri Jourdan).
......
* Update documentation of incremental API.
* Try speeding up the table back-end by internally allowing a
non-interruptible mode.
* Introduce a submodule Incremental for the incremental entry
points. Move also the types terminal, nonterminal, symbol
to a sub-module, to avoid any name clashes.
......@@ -24,8 +29,9 @@
Then, one could remove Makefile.shared and ocamldep.wrapper.
* Suite des patchs de Frédéric Bour.
Exposer aussi les réductions (Gabriel).
Ça peut servir à revenir en arrière après une erreur, car l'erreur
* Meilleurs messages d'erreur de syntaxe.
Revenir en arrière après une erreur, car l'erreur
n'est détectée qu'après quelques réductions. Une fois que l'on est
revenu, on peut examiner les items de l'état courant et donner des
positions de début d'item qui devraient être intéressantes.
......
......@@ -84,7 +84,10 @@ let rec loop linebuf (result : int I.result) =
let token = Lexer.token linebuf in
let startp = linebuf.Lexing.lex_start_p
and endp = linebuf.Lexing.lex_curr_p in
let result = I.offer env (token, startp, endp) in
let result = I.offer result (token, startp, endp) in
loop linebuf result
| I.AboutToReduce _ ->
let result = I.resume result in
loop linebuf result
| I.HandlingError env ->
(* The parser has suspended itself because of a syntax error. Stop. *)
......
......@@ -19,11 +19,16 @@ module type INCREMENTAL_ENGINE = sig
(* [InputNeeded] is an intermediate result. It means that the parser wishes
to read one token before continuing. *)
(* [HandlingError] is also an intermediate result. It means that the parser
has detected an error and is currently handling it, in several steps. It
does not need more input at this point. The parser suspends itself at
this point only in order to give the user an opportunity to handle this
error in a different manner, if desired. *)
(* [AboutToReduce] is an intermediate result. It means that the parser is
about to perform a reduction step. It does not need more input at this
point. The parser suspends itself at this point only in order to give the
user an opportunity to observe this reduction step. *)
(* [HandlingError] is an intermediate result. It means that the parser has
detected an error and is currently handling it, in several steps. It does
not need more input at this point. The parser suspends itself at this
point only in order to give the user an opportunity to handle this error
in a different manner, if desired. *)
(* The type [('a, 'pc) env] is shared by [InputNeeded] and [HandlingError].
As above, the parameter ['a] is the type of the final semantic value.
......@@ -31,37 +36,34 @@ module type INCREMENTAL_ENGINE = sig
or [handling_error], as appropriate. This prevents the user from
calling [offer] when she should call [handle], or vice-versa. *)
type input_needed
type about_to_reduce
type handling_error
type ('a, 'pc) env
type env
type production
type 'a result =
| InputNeeded of ('a, input_needed) env
| AboutToReduce of ('a, about_to_reduce) env * production
| HandlingError of ('a, handling_error) env
type 'a result = private
| InputNeeded of env
| AboutToReduce of env * production
| HandlingError of env
| Accepted of 'a
| Rejected
(* [offer] allows the user to resume the parser after it has suspended
itself with a result of the form [InputNeeded env]. [offer] expects [env]
as well as a new token and produces a new result. It does not raise any
exception. *)
itself with a result of the form [InputNeeded env]. [offer] expects the
old result as well as a new token and produces a new result. It does not
raise any exception. *)
val offer:
('a, input_needed) env ->
'a result ->
token * Lexing.position * Lexing.position ->
'a result
(* [handle] allows the user to resume the parser after it has suspended
itself with a result of the form [HandlingError env]. [handle] expects
[env] and produces a new result. It does not raise any exception. *)
(* [resume] allows the user to resume the parser after it has suspended
itself with a result of the form [AboutToReduce (env, prod)] or
[HandlingError env]. [resume] expects the old result and produces a new
result. It does not raise any exception. *)
val handle:
('a, handling_error) env ->
val resume:
'a result ->
'a result
(* The abstract type ['a lr1state] describes the non-initial states of the
......@@ -90,6 +92,6 @@ module type INCREMENTAL_ENGINE = sig
(* We offer a read-only view of the parser's state as a stream of elements. *)
val view: (_, _) env -> element stream
val view: env -> element stream
end
......@@ -13,11 +13,7 @@ module Make (T : TABLE) = struct
include T
type input_needed
type about_to_reduce
type handling_error
type ('a, 'pc) env =
type env =
(state, semantic_value, token) EngineTypes.env
(* --------------------------------------------------------------------------- *)
......@@ -25,10 +21,15 @@ module Make (T : TABLE) = struct
(* The type [result] represents an intermediate or final result of the
parser. See [EngineTypes]. *)
(* The type [result] is presented to the user as a private type (see
[IncrementalEngine]). This prevents the user from manufacturing results
(i.e., continuations) that do not make sense. (Such continuations could
potentially violate the LR invariant and lead to crashes.) *)
type 'a result =
| InputNeeded of ('a, input_needed) env
| AboutToReduce of ('a, about_to_reduce) env * production
| HandlingError of ('a, handling_error) env
| InputNeeded of env
| AboutToReduce of env * production
| HandlingError of env
| Accepted of 'a
| Rejected
......@@ -187,7 +188,8 @@ module Make (T : TABLE) = struct
and announce_reduce env (prod : production) =
AboutToReduce (env, prod)
(* The function [reduce] takes care of reductions. *)
(* The function [reduce] takes care of reductions. It is invoked by
[resume] after an [AboutToReduce] event has been produced. *)
(* Here, the lookahead token CAN be [error]. *)
......@@ -361,59 +363,46 @@ module Make (T : TABLE) = struct
run env true
(* [offer env triple] is invoked by the user in response to a result of the
form [InputNeeded env]. [offer] is just a synonym for [discard]. *)
(* [handle env] is invoked by the user in response to a result of the form
[HandlingError env]. [handle] is just a synonym for [error]. *)
(* [reduce env prod] is invoked by the user in response to a result of the
form [AboutToReduce (env, prod)]. *)
(* [offer result triple] is invoked by the user in response to a result
of the form [InputNeeded env]. It checks that [result] is indeed of
this form, and invokes [discard]. *)
(* In reality, [offer], [handle] and [reduce] accept an environment of type
[('a, 'pc) env], where ['a] and ['pc] are unconstrained, since they are
phantom type parameters. They produce a result of type [semantic_value
result] -- where the choice of the type [semantic_value] is forced by the
fact that this is the parameter of the exception [Accept]. *)
(* [resume result] is invoked by the user in response to a result of the
form [AboutToReduce (env, prod)] or [HandlingError env]. It checks
that [result] is indeed of this form, and invokes [reduce] or [error],
as appropriate. *)
(* We change these types in two ways. *)
(* In reality, [offer] and [resume] accept an argument of type
[semantic_value result] and produce a result of the same type. The choice
of [semantic_value] is forced by the fact that this is the parameter of
the exception [Accept]. *)
(* First, we restrict ['pc] to be [input_needed] in the case of [offer],
[handling_error] in the case of [handle], and [about_to_reduce] in the
case of [reduce]. This is safe, and prevents the user from providing
[offer] with an environment that comes from a [HandlingError] result,
etc. This is important: it guarantees that the LR invariant holds. *)
(* We change this as follows. *)
(* Second, we change the result type of [offer], [handle] and [reduce] from
(* We change the argument and result type of [offer] and [resume] from
[semantic_value result] to ['a result]. This is safe, in this case,
because we give the user access to values of type [(t, _) env] only if
[t] is indeed the type of the eventual semantic value for this run. (More
because we give the user access to values of type [t result] only if [t]
is indeed the type of the eventual semantic value for this run. (More
precisely, by examining the signatures [INCREMENTAL_ENGINE] and
[INCREMENTAL_ENGINE_START], one finds that the user can build a value of
type [('a, _) env] or ['a result] only if ['a] is [semantic_value]. The
table back-end goes further than this and produces versions of [start]
composed with a suitable cast, which give the user access to a value of
type [t result] where [t] is the type of the start symbol.) *)
(* The unsafe type cast is performed in two steps, due to the strange
interaction between type annotations and the relaxed value restriction.
If the two steps are merged, the type annotation is pushed inwards and
prevents generalization! This is a standard workaround, says Jacques. *)
let offer =
Obj.magic discard
let offer : 'a . ('a, input_needed) env -> token * Lexing.position * Lexing.position -> 'a result =
offer
let handle =
Obj.magic error
let handle : 'a . ('a, handling_error) env -> 'a result =
handle
let reduce =
Obj.magic reduce
let reduce : 'a. ('a, about_to_reduce) env -> production -> 'a result =
reduce
type ['a result] only if ['a] is [semantic_value]. The table back-end
goes further than this and produces versions of [start] composed with a
suitable cast, which give the user access to a value of type [t result]
where [t] is the type of the start symbol.) *)
let offer : 'a . 'a result -> token * Lexing.position * Lexing.position -> 'a result = function
| InputNeeded env ->
Obj.magic discard env
| _ ->
raise (Invalid_argument "offer expects InputNeeded")
let resume : 'a . 'a result -> 'a result = function
| HandlingError env ->
Obj.magic error env
| AboutToReduce (env, prod) ->
Obj.magic reduce env prod
| _ ->
raise (Invalid_argument "resume expects HandlingError | AboutToReduce")
(* --------------------------------------------------------------------------- *)
(* --------------------------------------------------------------------------- *)
......@@ -450,21 +439,18 @@ module Make (T : TABLE) = struct
let rec loop : 'a . reader -> 'a result -> 'a =
fun read result ->
match result with
| InputNeeded env ->
| InputNeeded _ ->
(* The parser needs a token. Request one from the lexer,
and offer it to the parser, which will produce a new
result. Then, repeat. *)
let triple = read() in
let result = offer env triple in
let result = offer result triple in
loop read result
| AboutToReduce (env, prod) ->
| AboutToReduce _
| HandlingError _ ->
(* The parser has suspended itself, but does not need
new input. Just resume the parser. Then, repeat. *)
let result = reduce env prod in
loop read result
| HandlingError env ->
(* Same scheme as above. *)
let result = handle env in
let result = resume result in
loop read result
| Accepted v ->
(* The parser has succeeded and produced a semantic value.
......
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