Commit e137a86d authored by POTTIER Francois's avatar POTTIER Francois

Renamed the type ['a result] to ['a checkpoint].

parent b0b81007
2015/10/16:
Incompatible change of the incremental API: renamed the type ['a result]
to ['a checkpoint]. This is a better name anyway, and should help avoid
confusion with the type ['a result] introduced in OCaml 4.03.
2015/10/12: 2015/10/12:
Avoid using $(shell pwd) in Makefile, for better Windows compatibility. Avoid using $(shell pwd) in Makefile, for better Windows compatibility.
......
...@@ -4,26 +4,26 @@ module I = ...@@ -4,26 +4,26 @@ module I =
Parser.MenhirInterpreter Parser.MenhirInterpreter
(* The loop which drives the parser. At each iteration, we analyze a (* The loop which drives the parser. At each iteration, we analyze a
result produced by the parser, and act in an appropriate manner. *) checkpoint produced by the parser, and act in an appropriate manner. *)
(* [lexbuf] is the lexing buffer. [result] is the last result produced (* [lexbuf] is the lexing buffer. [checkpoint] is the last checkpoint produced
by the parser. *) by the parser. *)
let rec loop lexbuf (result : int I.result) = let rec loop lexbuf (checkpoint : int I.checkpoint) =
match result with match checkpoint with
| I.InputNeeded env -> | I.InputNeeded env ->
(* The parser needs a token. Request one from the lexer, (* The parser needs a token. Request one from the lexer,
and offer it to the parser, which will produce a new and offer it to the parser, which will produce a new
result. Then, repeat. *) checkpoint. Then, repeat. *)
let token = Lexer.token lexbuf in let token = Lexer.token lexbuf in
let startp = lexbuf.Lexing.lex_start_p let startp = lexbuf.Lexing.lex_start_p
and endp = lexbuf.Lexing.lex_curr_p in and endp = lexbuf.Lexing.lex_curr_p in
let result = I.offer result (token, startp, endp) in let checkpoint = I.offer checkpoint (token, startp, endp) in
loop lexbuf result loop lexbuf checkpoint
| I.Shifting _ | I.Shifting _
| I.AboutToReduce _ -> | I.AboutToReduce _ ->
let result = I.resume result in let checkpoint = I.resume checkpoint in
loop lexbuf result loop lexbuf checkpoint
| I.HandlingError env -> | I.HandlingError env ->
(* The parser has suspended itself because of a syntax error. Stop. *) (* The parser has suspended itself because of a syntax error. Stop. *)
Printf.fprintf stderr Printf.fprintf stderr
......
...@@ -1941,7 +1941,7 @@ the name of the start symbol.) The generated file \texttt{parser.mli} contains ...@@ -1941,7 +1941,7 @@ the name of the start symbol.) The generated file \texttt{parser.mli} contains
the following declaration: the following declaration:
\begin{verbatim} \begin{verbatim}
module Incremental : sig module Incremental : sig
val main: unit -> thing MenhirInterpreter.result val main: unit -> thing MenhirInterpreter.checkpoint
end end
\end{verbatim} \end{verbatim}
We emphasize that the function \verb+Incremental.main+ does not parse We emphasize that the function \verb+Incremental.main+ does not parse
...@@ -1959,9 +1959,9 @@ follows: ...@@ -1959,9 +1959,9 @@ follows:
The signature \verb+INCREMENTAL_ENGINE+, defined in the module The signature \verb+INCREMENTAL_ENGINE+, defined in the module
\menhirlibincrementalengine, contains the following elements. \menhirlibincrementalengine, contains the following elements.
Please keep in mind that, from the outside, these elements should be referred Please keep in mind that, from the outside, these elements should be referred
to with an appropriate prefix: e.g., the type \verb+result+ should be referred to with an appropriate prefix: e.g., the type \verb+checkpoint+ should be referred
to as \verb+MenhirInterpreter.result+, or to as \verb+MenhirInterpreter.checkpoint+, or
\verb+Parser.MenhirInterpreter.result+, depending on which modules the user \verb+Parser.MenhirInterpreter.checkpoint+, depending on which modules the user
chooses to open. chooses to open.
%% type token %% type token
...@@ -1987,10 +1987,10 @@ data structure: it can be stored and used multiple times, if desired. ...@@ -1987,10 +1987,10 @@ data structure: it can be stored and used multiple times, if desired.
The abstract type \verb+production+ represents a production of the grammar. The abstract type \verb+production+ represents a production of the grammar.
%% type 'a result %% type 'a checkpoint
\begin{verbatim} \begin{verbatim}
type 'a result = private type 'a checkpoint = private
| InputNeeded of env | InputNeeded of env
| Shifting of env * env * bool | Shifting of env * env * bool
| AboutToReduce of env * production | AboutToReduce of env * production
...@@ -1999,29 +1999,29 @@ The abstract type \verb+production+ represents a production of the grammar. ...@@ -1999,29 +1999,29 @@ The abstract type \verb+production+ represents a production of the grammar.
| Rejected | Rejected
\end{verbatim} \end{verbatim}
The type \verb+'a result+ represents an intermediate or The type \verb+'a checkpoint+ represents an intermediate or
final result of the parser. An intermediate result is a suspension: it records final state of the parser. An intermediate checkpoint is a suspension: it records
the parser's current state, and allows parsing to be resumed. The parameter the parser's current state, and allows parsing to be resumed. The parameter
\verb+'a+ is the type of the semantic value that will eventually be produced \verb+'a+ is the type of the semantic value that will eventually be produced
if the parser succeeds. if the parser succeeds.
\verb+Accepted+ and \verb+Rejected+ are final results. \verb+Accepted+ carries \verb+Accepted+ and \verb+Rejected+ are final checkpoints. \verb+Accepted+ carries
a semantic value. a semantic value.
\verb+InputNeeded+ is an intermediate result. It means that the parser wishes \verb+InputNeeded+ is an intermediate checkpoint. It means that the parser wishes
to read one token before continuing. to read one token before continuing.
\verb+Shifting+ is an intermediate result. It means that the parser is taking \verb+Shifting+ is an intermediate checkpoint. It means that the parser is taking
a shift transition. It exposes the state of the parser before and after the a shift transition. It exposes the state of the parser before and after the
transition. The Boolean parameter tells whether the parser intends to request transition. The Boolean parameter tells whether the parser intends to request
a new token after this transition. (It always does, except when it is about to a new token after this transition. (It always does, except when it is about to
accept.) accept.)
\verb+AboutToReduce+ is an intermediate result: it means that the parser is \verb+AboutToReduce+ is an intermediate checkpoint: it means that the parser is
about to perform a reduction step. \verb+HandlingError+ is also an about to perform a reduction step. \verb+HandlingError+ is also an
intermediate result: it means that the parser has detected an error and is intermediate checkpoint: it means that the parser has detected an error and is
about to handle it. (Error handling is typically performed in several steps, about to handle it. (Error handling is typically performed in several steps,
so the next result is likely to be \verb+HandlingError+ again.) In these two so the next checkpoint is likely to be \verb+HandlingError+ again.) In these two
cases, the parser does not need more input. The parser suspends itself at this cases, the parser does not need more input. The parser suspends itself at this
point only in order to give the user an opportunity to observe the parser's point only in order to give the user an opportunity to observe the parser's
transitions and possibly handle errors in a different manner, if desired. transitions and possibly handle errors in a different manner, if desired.
...@@ -2030,16 +2030,16 @@ transitions and possibly handle errors in a different manner, if desired. ...@@ -2030,16 +2030,16 @@ transitions and possibly handle errors in a different manner, if desired.
\begin{verbatim} \begin{verbatim}
val offer: val offer:
'a result -> 'a checkpoint ->
token * Lexing.position * Lexing.position -> token * Lexing.position * Lexing.position ->
'a result 'a checkpoint
\end{verbatim} \end{verbatim}
The function \verb+offer+ allows the user to resume the parser after the The function \verb+offer+ allows the user to resume the parser after the
parser has suspended itself with a result of the form \verb+InputNeeded env+. parser has suspended itself with a checkpoint of the form \verb+InputNeeded env+.
This function expects the previous result \verb+result+ as well as a new token This function expects the previous checkpoint \verb+checkpoint+ as well as a new token
(together with the start and end positions of this token). It produces a new (together with the start and end positions of this token). It produces a new
result, which again can be an intermediate result or a final result. It does checkpoint, which again can be an intermediate checkpoint or a final checkpoint. It does
not raise any exception. (The exception \texttt{Error} is used only in the not raise any exception. (The exception \texttt{Error} is used only in the
monolithic API.) monolithic API.)
...@@ -2047,20 +2047,20 @@ monolithic API.) ...@@ -2047,20 +2047,20 @@ monolithic API.)
\begin{verbatim} \begin{verbatim}
val resume: val resume:
'a result -> 'a checkpoint ->
'a result 'a checkpoint
\end{verbatim} \end{verbatim}
The function \verb+resume+ allows the user to resume the parser after the The function \verb+resume+ allows the user to resume the parser after the
parser has suspended itself with a result of the form parser has suspended itself with a checkpoint of the form
\verb+AboutToReduce (env, prod)+ or \verb+HandlingError env+. \verb+AboutToReduce (env, prod)+ or \verb+HandlingError env+.
This function expects just the previous result \verb+result+. It produces a new This function expects just the previous checkpoint \verb+checkpoint+. It produces a new
result. It does not raise any exception. checkpoint. It does not raise any exception.
The incremental API subsumes the monolithic API. Indeed, \verb+main+ can be The incremental API subsumes the monolithic API. Indeed, \verb+main+ can be
(and is in fact) implemented by first using (and is in fact) implemented by first using
\verb+Incremental.main+, then calling \verb+offer+ and \verb+Incremental.main+, then calling \verb+offer+ and
\verb+resume+ in a loop, until a final result is obtained. \verb+resume+ in a loop, until a final checkpoint is obtained.
Although the type \verb+env+ is opaque, a parser state can be inspected via a Although the type \verb+env+ is opaque, a parser state can be inspected via a
few accessor functions, which we are about to describe. Before we do so, we few accessor functions, which we are about to describe. Before we do so, we
......
...@@ -99,7 +99,7 @@ module Make ...@@ -99,7 +99,7 @@ module Make
| _ :: _, lazy Nil -> | _ :: _, lazy Nil ->
assert false assert false
(* [investigate t result] assumes that [result] has been obtained by (* [investigate t checkpoint] assumes that [checkpoint] has been obtained by
offering the terminal symbol [t] to the parser. It runs the parser, offering the terminal symbol [t] to the parser. It runs the parser,
through an arbitrary number of reductions, until the parser either through an arbitrary number of reductions, until the parser either
accepts this token (i.e., shifts) or rejects it (i.e., signals an accepts this token (i.e., shifts) or rejects it (i.e., signals an
...@@ -109,8 +109,8 @@ module Make ...@@ -109,8 +109,8 @@ module Make
(* It is desirable that the semantic actions be side-effect free, or (* It is desirable that the semantic actions be side-effect free, or
that their side-effects be harmless (replayable). *) that their side-effects be harmless (replayable). *)
let rec investigate (t : _ terminal) (result : _ result) explanations = let rec investigate (t : _ terminal) (checkpoint : _ checkpoint) explanations =
match result with match checkpoint with
| Shifting (env, _, _) -> | Shifting (env, _, _) ->
(* The parser is about to shift, which means it is willing to (* The parser is about to shift, which means it is willing to
consume the terminal symbol [t]. In the state before the consume the terminal symbol [t]. In the state before the
...@@ -132,7 +132,7 @@ module Make ...@@ -132,7 +132,7 @@ module Make
(* TEMPORARY [env] may be an initial state! violating [item_current]'s precondition *) (* TEMPORARY [env] may be an initial state! violating [item_current]'s precondition *)
| AboutToReduce _ -> | AboutToReduce _ ->
(* The parser wishes to reduce. Just follow. *) (* The parser wishes to reduce. Just follow. *)
investigate t (resume result) explanations investigate t (resume checkpoint) explanations
| HandlingError _ -> | HandlingError _ ->
(* The parser fails, which means the terminal symbol [t] does (* The parser fails, which means the terminal symbol [t] does
not make sense at this point. Thus, no new explanations of not make sense at this point. Thus, no new explanations of
...@@ -146,7 +146,7 @@ module Make ...@@ -146,7 +146,7 @@ module Make
it can request another token or terminate. *) it can request another token or terminate. *)
assert false assert false
(* [investigate pos result] assumes that [result] is of the form (* [investigate pos checkpoint] assumes that [checkpoint] is of the form
[InputNeeded _]. For every terminal symbol [t], it investigates [InputNeeded _]. For every terminal symbol [t], it investigates
how the parser reacts when fed the symbol [t], and returns a list how the parser reacts when fed the symbol [t], and returns a list
of explanations. The position [pos] is where a syntax error was of explanations. The position [pos] is where a syntax error was
...@@ -154,7 +154,7 @@ module Make ...@@ -154,7 +154,7 @@ module Make
important because the position of the dummy token may end up in important because the position of the dummy token may end up in
the explanations that we produce. *) the explanations that we produce. *)
let investigate pos (result : _ result) : explanation list = let investigate pos (checkpoint : _ checkpoint) : explanation list =
weed compare_explanations ( weed compare_explanations (
foreach_terminal_but_error (fun symbol explanations -> foreach_terminal_but_error (fun symbol explanations ->
match symbol with match symbol with
...@@ -163,7 +163,7 @@ module Make ...@@ -163,7 +163,7 @@ module Make
(* Build a dummy token for the terminal symbol [t]. *) (* Build a dummy token for the terminal symbol [t]. *)
let token = (terminal2token t, pos, pos) in let token = (terminal2token t, pos, pos) in
(* Submit it to the parser. Accumulate explanations. *) (* Submit it to the parser. Accumulate explanations. *)
investigate t (offer result token) explanations investigate t (offer checkpoint token) explanations
) [] ) []
) )
...@@ -180,38 +180,38 @@ module Make ...@@ -180,38 +180,38 @@ module Make
token, startp, endp token, startp, endp
(* The following is a custom version of the loop found in [Engine]. It (* The following is a custom version of the loop found in [Engine]. It
drives the parser in the usual way, but keeps a checkpoint, which is the drives the parser in the usual way, but records the last [InputNeeded]
last [InputNeeded] result. If a syntax error is detected, it goes back to checkpoint. If a syntax error is detected, it goes back to this
this state and analyzes it in order to produce a meaningful checkpoint and analyzes it in order to produce a meaningful
diagnostic. *) diagnostic. *)
exception Error of (Lexing.position * Lexing.position) * explanation list exception Error of (Lexing.position * Lexing.position) * explanation list
(* TEMPORARY why loop-style? we should offer a simplified incremental API *) (* TEMPORARY why loop-style? we should offer a simplified incremental API *)
type 'a result = { type 'a checkpoint = {
checkpoint: 'a I.result; inputneeded: 'a I.checkpoint;
current: 'a I.result current: 'a I.checkpoint
} }
let rec loop (read : reader) ({ checkpoint; current } : 'a result) : 'a = let rec loop (read : reader) ({ inputneeded; current } : 'a checkpoint) : 'a =
match current with match current with
| InputNeeded _ -> | InputNeeded _ ->
(* Update the checkpoint. *) (* Update the last recorded [InputNeeded] checkpoint. *)
let checkpoint = current in let inputneeded = current in
let triple = read() in let triple = read() in
let current = offer current triple in let current = offer current triple in
loop read { checkpoint; current } loop read { inputneeded; current }
| Shifting _ | Shifting _
| AboutToReduce _ -> | AboutToReduce _ ->
let current = resume current in let current = resume current in
loop read { checkpoint; current } loop read { inputneeded; current }
| HandlingError env -> | HandlingError env ->
(* The parser signals a syntax error. Note the position of the (* The parser signals a syntax error. Note the position of the
problematic token, which is useful. Then, go back to the problematic token, which is useful. Then, go back to the
checkpoint and investigate. *) checkpoint and investigate. *)
let (startp, _) as positions = positions env in let (startp, _) as positions = positions env in
raise (Error (positions, investigate startp checkpoint)) raise (Error (positions, investigate startp inputneeded))
| Accepted v -> | Accepted v ->
v v
| Rejected -> | Rejected ->
...@@ -219,13 +219,13 @@ module Make ...@@ -219,13 +219,13 @@ module Make
we stop as soon as the parser reports [HandlingError]. *) we stop as soon as the parser reports [HandlingError]. *)
assert false assert false
let entry (start : 'a I.result) lexer lexbuf = let entry (start : 'a I.checkpoint) lexer lexbuf =
(* The parser cannot accept or reject before it asks for the very first (* The parser cannot accept or reject before it asks for the very first
character of input. (Indeed, we statically reject a symbol that character of input. (Indeed, we statically reject a symbol that
generates the empty language or the singleton language {epsilon}.) generates the empty language or the singleton language {epsilon}.)
So, [start] must be [InputNeeded _]. *) So, [start] must be [InputNeeded _]. *)
assert (match start with InputNeeded _ -> true | _ -> false); assert (match start with InputNeeded _ -> true | _ -> false);
loop (wrap lexer lexbuf) { checkpoint = start; current = start } loop (wrap lexer lexbuf) { inputneeded = start; current = start }
(* TEMPORARY could also publish a list of the terminal symbols that (* TEMPORARY could also publish a list of the terminal symbols that
do not cause an error *) do not cause an error *)
......
...@@ -75,6 +75,6 @@ module Make ...@@ -75,6 +75,6 @@ module Make
type reader = type reader =
unit -> token * Lexing.position * Lexing.position unit -> token * Lexing.position * Lexing.position
val entry: 'a I.result -> (Lexing.lexbuf -> token) -> Lexing.lexbuf -> 'a val entry: 'a I.checkpoint -> (Lexing.lexbuf -> token) -> Lexing.lexbuf -> 'a
end end
...@@ -9,36 +9,36 @@ module type INCREMENTAL_ENGINE = sig ...@@ -9,36 +9,36 @@ module type INCREMENTAL_ENGINE = sig
type token type token
(* The type ['a result] represents an intermediate or final result of the (* The type ['a checkpoint] represents an intermediate or final state of the
parser. An intermediate result is a suspension: it records the parser's parser. An intermediate checkpoint is a suspension: it records the parser's
current state, and allows parsing to be resumed. The parameter ['a] is current state, and allows parsing to be resumed. The parameter ['a] is
the type of the semantic value that will eventually be produced if the the type of the semantic value that will eventually be produced if the
parser succeeds. *) parser succeeds. *)
(* [Accepted] and [Rejected] are final results. [Accepted] carries a (* [Accepted] and [Rejected] are final checkpoints. [Accepted] carries a
semantic value. *) semantic value. *)
(* [InputNeeded] is an intermediate result. It means that the parser wishes (* [InputNeeded] is an intermediate checkpoint. It means that the parser wishes
to read one token before continuing. *) to read one token before continuing. *)
(* [Shifting] is an intermediate result. It means that the parser is taking (* [Shifting] is an intermediate checkpoint. It means that the parser is taking
a shift transition. It exposes the state of the parser before and after a shift transition. It exposes the state of the parser before and after
the transition. The Boolean parameter tells whether the parser intends to the transition. The Boolean parameter tells whether the parser intends to
request a new token after this transition. (It always does, except when request a new token after this transition. (It always does, except when
it is about to accept.) *) it is about to accept.) *)
(* [AboutToReduce] is an intermediate result. It means that the parser is (* [AboutToReduce] is an intermediate checkpoint. It means that the parser is
about to perform a reduction step. It exposes the parser's current about to perform a reduction step. It exposes the parser's current
state as well as the production that is about to be reduced. *) state as well as the production that is about to be reduced. *)
(* [HandlingError] is an intermediate result. It means that the parser has (* [HandlingError] is an intermediate checkpoint. It means that the parser has
detected an error and is currently handling it, in several steps. *) detected an error and is currently handling it, in several steps. *)
type env type env
type production type production
type 'a result = private type 'a checkpoint = private
| InputNeeded of env | InputNeeded of env
| Shifting of env * env * bool | Shifting of env * env * bool
| AboutToReduce of env * production | AboutToReduce of env * production
...@@ -47,23 +47,23 @@ module type INCREMENTAL_ENGINE = sig ...@@ -47,23 +47,23 @@ module type INCREMENTAL_ENGINE = sig
| Rejected | Rejected
(* [offer] allows the user to resume the parser after it has suspended (* [offer] allows the user to resume the parser after it has suspended
itself with a result of the form [InputNeeded env]. [offer] expects the itself with a checkpoint of the form [InputNeeded env]. [offer] expects the
old result as well as a new token and produces a new result. It does not old checkpoint as well as a new token and produces a new checkpoint. It does not
raise any exception. *) raise any exception. *)
val offer: val offer:
'a result -> 'a checkpoint ->
token * Lexing.position * Lexing.position -> token * Lexing.position * Lexing.position ->
'a result 'a checkpoint
(* [resume] allows the user to resume the parser after it has suspended (* [resume] allows the user to resume the parser after it has suspended
itself with a result of the form [AboutToReduce (env, prod)] or itself with a checkpoint of the form [AboutToReduce (env, prod)] or
[HandlingError env]. [resume] expects the old result and produces a new [HandlingError env]. [resume] expects the old checkpoint and produces a new
result. It does not raise any exception. *) checkpoint. It does not raise any exception. *)
val resume: val resume:
'a result -> 'a checkpoint ->
'a result 'a checkpoint
(* The abstract type ['a lr1state] describes the non-initial states of the (* 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 LR(1) automaton. The index ['a] represents the type of the semantic value
......
...@@ -28,15 +28,15 @@ module Make (T : TABLE) = struct ...@@ -28,15 +28,15 @@ module Make (T : TABLE) = struct
(* --------------------------------------------------------------------------- *) (* --------------------------------------------------------------------------- *)
(* The type [result] represents an intermediate or final result of the (* The type [checkpoint] represents an intermediate or final result of the
parser. See [EngineTypes]. *) parser. See [EngineTypes]. *)
(* The type [result] is presented to the user as a private type (see (* The type [checkpoint] is presented to the user as a private type (see
[IncrementalEngine]). This prevents the user from manufacturing results [IncrementalEngine]). This prevents the user from manufacturing checkpoints
(i.e., continuations) that do not make sense. (Such continuations could (i.e., continuations) that do not make sense. (Such continuations could
potentially violate the LR invariant and lead to crashes.) *) potentially violate the LR invariant and lead to crashes.) *)
type 'a result = type 'a checkpoint =
| InputNeeded of env | InputNeeded of env
| Shifting of env * env * bool | Shifting of env * env * bool
| AboutToReduce of env * production | AboutToReduce of env * production
...@@ -72,11 +72,11 @@ module Make (T : TABLE) = struct ...@@ -72,11 +72,11 @@ module Make (T : TABLE) = struct
a terminal symbol and [s] does not have a default reduction on [#]. *) a terminal symbol and [s] does not have a default reduction on [#]. *)
(* The following recursive group of functions are tail recursive, produce a (* The following recursive group of functions are tail recursive, produce a
result of type [semantic_value result], and cannot raise an exception. A checkpoint of type [semantic_value checkpoint], and cannot raise an
semantic action can raise [Error], but this exception is immediately exception. A semantic action can raise [Error], but this exception is
caught within [reduce]. *) immediately caught within [reduce]. *)
let rec run env please_discard : semantic_value result = let rec run env please_discard : semantic_value checkpoint =
(* Log the fact that we just entered this state. *) (* Log the fact that we just entered this state. *)
...@@ -96,7 +96,7 @@ module Make (T : TABLE) = struct ...@@ -96,7 +96,7 @@ module Make (T : TABLE) = struct
(* [discard env triple] stores [triple] into [env], overwriting the previous (* [discard env triple] stores [triple] into [env], overwriting the previous
token. It is invoked by [offer], which itself is invoked by the user in token. It is invoked by [offer], which itself is invoked by the user in
response to an [InputNeeded] result. *) response to an [InputNeeded] checkpoint. *)
and discard env triple = and discard env triple =
if log then begin if log then begin
...@@ -200,7 +200,7 @@ module Make (T : TABLE) = struct ...@@ -200,7 +200,7 @@ module Make (T : TABLE) = struct
(* --------------------------------------------------------------------------- *) (* --------------------------------------------------------------------------- *)
(* The function [announce_reduce] stops the parser and returns a result (* The function [announce_reduce] stops the parser and returns a checkpoint
which allows the parser to be resumed by calling [reduce]. *) which allows the parser to be resumed by calling [reduce]. *)
(* Only ordinary productions are exposed to the user. Start productions (* Only ordinary productions are exposed to the user. Start productions
...@@ -355,7 +355,7 @@ module Make (T : TABLE) = struct ...@@ -355,7 +355,7 @@ module Make (T : TABLE) = struct
(* [start s] begins the parsing process. *) (* [start s] begins the parsing process. *)
let start (s : state) : semantic_value result = let start (s : state) : semantic_value checkpoint =
(* Build an empty stack. This is a dummy cell, which is its own (* Build an empty stack. This is a dummy cell, which is its own
successor. Its fields other than [next] contain dummy values. successor. Its fields other than [next] contain dummy values.
...@@ -396,40 +396,43 @@ module Make (T : TABLE) = struct ...@@ -396,40 +396,43 @@ module Make (T : TABLE) = struct
run env true run env true
(* [offer result triple] is invoked by the user in response to a result (* [offer checkpoint triple] is invoked by the user in response to a
of the form [InputNeeded env]. It checks that [result] is indeed of checkpoint of the form [InputNeeded env]. It checks that [checkpoint] is
this form, and invokes [discard]. *) indeed of this form, and invokes [discard]. *)
(* [resume result] is invoked by the user in response to a result of the (* [resume checkpoint] is invoked by the user in response to a checkpoint of
form [AboutToReduce (env, prod)] or [HandlingError env]. It checks the form [AboutToReduce (env, prod)] or [HandlingError env]. It checks
that [result] is indeed of this form, and invokes [reduce] or [error], that [checkpoint] is indeed of this form, and invokes [reduce] or
as appropriate. *) [error], as appropriate. *)
(* In reality, [offer] and [resume] accept an argument of type (* In reality, [offer] and [resume] accept an argument of type
[semantic_value result] and produce a result of the same type. The choice [semantic_value checkpoint] and produce a checkpoint of the same type.
of [semantic_value] is forced by the fact that this is the parameter of The choice of [semantic_value] is forced by the fact that this is the
the result [Accepted]. *) parameter of the checkpoint [Accepted]. *)
(* We change this as follows. *) (* We change this as follows. *)
(* We change the argument and result type of [offer] and [resume] 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, [semantic_value checkpoint] to ['a checkpoint]. This is safe, in this
because we give the user access to values of type [t result] only if [t] case, because we give the user access to values of type [t checkpoint]
is indeed the type of the eventual semantic value for this run. (More only if [t] is indeed the type of the eventual semantic value for this