A value of type production is (an index for) a production. The start productions (which do not exist in an .mly file, but are constructed by Menhir internally) are not part of this type.

A value of type 'a env represents a configuration of the automaton: current state, stack, lookahead token, etc. The parameter 'a is the type of the semantic value that will eventually be produced if the parser succeeds.

In normal operation, the parser works with checkpoints: see the functions offer and resume. However, it is also possible to work directly with environments (see the functions pop, force_reduction, and feed) and to reconstruct a checkpoint out of an environment (see input_needed). This is considered advanced functionality; its purpose is to allow error recovery strategies to be programmed by the user.

The type 'a checkpoint represents an intermediate or 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 'a is the type of the semantic value that will eventually be produced if the parser succeeds.

Accepted and Rejected are final checkpoints. Accepted carries a semantic value.

InputNeeded is an intermediate checkpoint. It means that the parser wishes to read one token before continuing.

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 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 accept.)

AboutToReduce is an intermediate checkpoint. It means that the parser is about to perform a reduction step. It exposes the parser's current state as well as the production that is about to be reduced.

HandlingError is an intermediate checkpoint. It means that the parser has detected an error and is currently handling it, in several steps.

offer allows the user to resume the parser after it has suspended itself with a checkpoint of the form InputNeeded env. offer expects the old checkpoint as well as a new token and produces a new checkpoint. It does not raise any exception.

The optional argument strategy influences the manner in which resume deals with checkpoints of the form HandlingError _. Its default value is `Legacy. It can be briefly described as follows:

• If the error token is used only to report errors (that is, if the error token appears only at the end of a production, whose semantic action raises an exception) then the simplified strategy should be preferred. (This includes the case where the error token does not appear at all in the grammar.)

• If the error token is used to recover after an error, or if perfect backward compatibility is required, the legacy strategy should be selected.

More details on strategies appear in the file Engine.ml.

resume allows the user to resume the parser after it has suspended itself with a checkpoint of the form Shifting _, AboutToReduce _, or HandlingError _. resume expects the old checkpoint and produces a new checkpoint. It does not raise any exception.

A token supplier is a function of no arguments which delivers a new token (together with its start and end positions) every time it is called.

A pair of a lexer and a lexing buffer can be turned into a supplier.

loop supplier checkpoint begins parsing from checkpoint, reading tokens from supplier. It continues parsing until it reaches a checkpoint of the form Accepted v or Rejected. In the former case, it returns v. In the latter case, it raises the exception Error. The optional argument strategy, whose default value is Legacy, is passed to resume and influences the error-handling strategy.

loop_handle succeed fail supplier checkpoint begins parsing from checkpoint, reading tokens from supplier. It continues parsing until it reaches a checkpoint of the form Accepted v or HandlingError env (or Rejected, but that should not happen, as HandlingError _ will be observed first). In the former case, it calls succeed v. In the latter case, it calls fail with this checkpoint. It cannot raise Error.

This means that Menhir's error-handling procedure does not get a chance to run. For this reason, there is no strategy parameter. Instead, the user can implement her own error handling code, in the fail continuation.

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.

shifts checkpoint assumes that checkpoint has been obtained by submitting a token to the parser. It runs the parser from checkpoint, through an arbitrary number of reductions, until the parser either accepts this token (i.e., shifts) or rejects it (i.e., signals an error). If the parser decides to shift, then Some env is returned, where env is the parser's state just before shifting. Otherwise, None is returned.

It is desirable that the semantic actions be side-effect free, or that their side-effects be harmless (replayable).

The function acceptable allows testing, after an error has been detected, which tokens would have been accepted at this point. It is implemented using shifts. Its argument should be an InputNeeded checkpoint.

For completeness, one must undo any spurious reductions before carrying out this test -- that is, one must apply acceptable to the FIRST checkpoint that is passed by loop_handle_undo to its failure continuation.

This test causes some semantic actions to be run! The semantic actions should be side-effect free, or their side-effects should be harmless.

The position pos is used as the start and end positions of the hypothetical token, and may be picked up by the semantic actions. We suggest using the position where the error was detected.

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.

The states of the LR(1) automaton are numbered (from 0 and up).

production_index maps a production to its integer index.

find_production maps a production index to a production. Its argument must be a valid index; use with care.

An element is a pair of a non-initial state s and a semantic value v associated with the incoming symbol of this state. The idea is, the value v was pushed onto the stack just before the state s was entered. Thus, for some type 'a, the state s has type 'a lr1state and the value v has type 'a. In other words, the type element is an existential type.

top env returns the parser's top stack element. The state contained in this stack element is the current state of the automaton. If the stack is empty, None is returned. In that case, the current state of the automaton must be an initial state.

pop_many i env pops i cells off the automaton's stack. This is done via i successive invocations of pop. Thus, pop_many 1 is pop. The index i must be nonnegative. The time complexity is O(i).

get i env returns the parser's i-th stack element. The index i is 0-based: thus, get 0 is top. If i is greater than or equal to the number of elements in the stack, None is returned. The time complexity is O(i).

current_state_number env is (the integer number of) the automaton's current state. This works even if the automaton's stack is empty, in which case the current state is an initial state. This number can be passed as an argument to a message function generated by menhir --compile-errors.

equal env1 env2 tells whether the parser configurations env1 and env2 are equal in the sense that the automaton's current state is the same in env1 and env2 and the stack is *physically* the same in env1 and env2. If equal env1 env2 is true, then the sequence of the stack elements, as observed via pop and top, must be the same in env1 and env2. Also, if equal env1 env2 holds, then the checkpoints input_needed env1 and input_needed env2 must be equivalent. The function equal has time complexity O(1).

positions env returns the start and end positions of the current lookahead token. In an initial state, a pair of twice the initial position is returned.

When applied to an environment taken from a checkpoint of the form AboutToReduce (env, prod), the function env_has_default_reduction tells whether the reduction that is about to take place is a default reduction.

state_has_default_reduction s tells whether the state s has a default reduction. This includes the case where s is an accepting state.

pop env returns a new environment, where the parser's top stack cell has been popped off. (If the stack is empty, None is returned.) This amounts to pretending that the (terminal or nonterminal) symbol that corresponds to this stack cell has not been read.

force_reduction prod env should be called only if in the state env the parser is capable of reducing the production prod. If this condition is satisfied, then this production is reduced, which means that its semantic action is executed (this can have side effects!) and the automaton makes a goto (nonterminal) transition. If this condition is not satisfied, Invalid_argument _ is raised.

input_needed env returns InputNeeded env. That is, out of an env that might have been obtained via a series of calls to the functions pop, force_reduction, feed, etc., it produces a checkpoint, which can be used to resume normal parsing, by supplying this checkpoint as an argument to offer.

This function should be used with some care. It could "mess up the lookahead" in the sense that it allows parsing to resume in an arbitrary state s with an arbitrary lookahead symbol t, even though Menhir's reachability analysis (menhir --list-errors) might well think that it is impossible to reach this particular configuration. If one is using Menhir's new error reporting facility, this could cause the parser to reach an error state for which no error message has been prepared.

An LR(0) item is a pair of a production prod and a valid index i into this production. That is, if the length of rhs prod is n, then i is comprised between 0 and n, inclusive.

incoming_symbol s is the incoming symbol of the state s, that is, the symbol that the parser must recognize before (has recognized when) it enters the state s. This function gives access to the semantic value v stored in a stack element Element (s, v, _, _). Indeed, by case analysis on the symbol incoming_symbol s, one discovers the type 'a of the value v.

items s is the set of the LR(0) items in the LR(0) core of the LR(1) state s. This set is not epsilon-closed. This set is presented as a list, in an arbitrary order.

lhs prod is the left-hand side of the production prod. This is always a non-terminal symbol.

rhs prod is the right-hand side of the production prod. This is a (possibly empty) sequence of (terminal or nonterminal) symbols.

nullable nt tells whether the non-terminal symbol nt is nullable. That is, it is true if and only if this symbol produces the empty word epsilon.

first nt t tells whether the FIRST set of the nonterminal symbol nt contains the terminal symbol t. That is, it is true if and only if nt produces a word that begins with t.

xfirst is analogous to first, but expects a first argument of type xsymbol instead of _ terminal.

foreach_terminal enumerates the terminal symbols, including error.

foreach_terminal_but_error enumerates the terminal symbols, excluding error.

feed symbol startp semv endp env causes the parser to consume the (terminal or nonterminal) symbol symbol, accompanied with the semantic value semv and with the start and end positions startp and endp. Thus, the automaton makes a transition, and reaches a new state. The stack grows by one cell. This operation is permitted only if the current state (as determined by env) has an outgoing transition labeled with symbol. Otherwise, Invalid_argument _ is raised.