package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Parser.MenhirInterpreterSource

include MenhirLib.IncrementalEngine.INCREMENTAL_ENGINE with type token = token
Sourcetype token = token
Sourcetype production

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.

Sourcetype 'a env

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.

Sourcetype 'a checkpoint = private
  1. | InputNeeded of 'a env
  2. | Shifting of 'a env * 'a env * bool
  3. | AboutToReduce of 'a env * production
  4. | HandlingError of 'a env
  5. | Accepted of 'a
  6. | Rejected

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.

Sourcetype strategy = [
  1. | `Legacy
  2. | `Simplified
]

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.

Sourceval resume : ?strategy:strategy -> 'a checkpoint -> 'a checkpoint

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.

Sourceval lexer_lexbuf_to_supplier : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> supplier

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

The functions offer and resume are sufficient to write a parser loop. One can imagine many variations (which is why we expose these functions in the first place!). Here, we expose a few variations of the main loop, ready for use.

Sourceval loop : ?strategy:strategy -> supplier -> 'a checkpoint -> 'a

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.

Sourceval loop_handle : ('a -> 'answer) -> ('a checkpoint -> 'answer) -> supplier -> 'a checkpoint -> 'answer

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.

Sourceval loop_handle_undo : ('a -> 'answer) -> ('a checkpoint -> '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.

Sourceval shifts : 'a checkpoint -> 'a env option

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.

Sourcetype 'a lr1state

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.

Sourceval number : _ lr1state -> int

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

Sourceval production_index : production -> int

production_index maps a production to its integer index.

Sourceval find_production : int -> production

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.

The parser's stack is (or, more precisely, can be viewed as) a stream of elements. The functions top and pop offer access to this stream.

Sourceval top : 'a env -> element option

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.

Sourceval pop_many : int -> 'a env -> 'a env option

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

Sourceval get : int -> 'a env -> element option

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

Sourceval current_state_number : 'a env -> int

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.

Sourceval equal : 'a env -> 'a env -> bool

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.

Sourceval env_has_default_reduction : 'a env -> bool

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.

Sourceval state_has_default_reduction : _ lr1state -> bool

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

Sourceval pop : 'a env -> 'a env option

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.

Sourceval force_reduction : production -> 'a env -> 'a env

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.

Sourceval input_needed : 'a env -> 'a checkpoint

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.

Sourcetype _ terminal =
  1. | T_error : unit terminal
  2. | T_WHILE : unit terminal
  3. | T_UNDERSCORE : unit terminal
  4. | T_UNALIGNED : unit terminal
  5. | T_T_W : Syntax.swsize terminal
  6. | T_T_INT_CAST : Syntax.sign terminal
  7. | T_T_INT : unit terminal
  8. | T_T_BOOL : unit terminal
  9. | T_TYPE : unit terminal
  10. | T_TRUE : unit terminal
  11. | T_TO : unit terminal
  12. | T_SWSIZE : Syntax.swsize terminal
  13. | T_SVSIZE : Syntax.svsize terminal
  14. | T_STRING : string terminal
  15. | T_STAR : unit terminal
  16. | T_STACK : unit terminal
  17. | T_SLASH : Syntax.sign option terminal
  18. | T_SHARP : unit terminal
  19. | T_SEMICOLON : unit terminal
  20. | T_RPAREN : unit terminal
  21. | T_ROR : unit terminal
  22. | T_ROL : unit terminal
  23. | T_RETURN : unit terminal
  24. | T_REQUIRE : unit terminal
  25. | T_REG : unit terminal
  26. | T_RBRACKET : unit terminal
  27. | T_RBRACE : unit terminal
  28. | T_RARROW : unit terminal
  29. | T_QUESTIONMARK : unit terminal
  30. | T_POINTER : unit terminal
  31. | T_PLUS : unit terminal
  32. | T_PIPEPIPE : unit terminal
  33. | T_PIPE : unit terminal
  34. | T_PERCENT : Syntax.sign option terminal
  35. | T_PARAM : unit terminal
  36. | T_NID : string terminal
  37. | T_NAMESPACE : unit terminal
  38. | T_MUTABLE : unit terminal
  39. | T_MINUS : unit terminal
  40. | T_LTLT : unit terminal
  41. | T_LT : Syntax.sign option terminal
  42. | T_LPAREN : unit terminal
  43. | T_LE : Syntax.sign option terminal
  44. | T_LBRACKET : unit terminal
  45. | T_LBRACE : unit terminal
  46. | T_INT : Syntax.int_representation terminal
  47. | T_INLINE : unit terminal
  48. | T_IF : unit terminal
  49. | T_HAT : unit terminal
  50. | T_GTGT : Syntax.sign option terminal
  51. | T_GT : Syntax.sign option terminal
  52. | T_GLOBAL : unit terminal
  53. | T_GE : Syntax.sign option terminal
  54. | T_FROM : unit terminal
  55. | T_FOR : unit terminal
  56. | T_FN : unit terminal
  57. | T_FALSE : unit terminal
  58. | T_EXPORT : unit terminal
  59. | T_EXEC : unit terminal
  60. | T_EQEQ : unit terminal
  61. | T_EQ : unit terminal
  62. | T_EOF : unit terminal
  63. | T_ELSE : unit terminal
  64. | T_DOWNTO : unit terminal
  65. | T_DOT : unit terminal
  66. | T_CONSTANT : unit terminal
  67. | T_COMMA : unit terminal
  68. | T_COLONCOLON : unit terminal
  69. | T_COLON : unit terminal
  70. | T_BANGEQ : unit terminal
  71. | T_BANG : unit terminal
  72. | T_ARRAYINIT : unit terminal
  73. | T_AMPAMP : unit terminal
  74. | T_AMP : unit terminal
  75. | T_ALIGNED : unit terminal
Sourcetype _ nonterminal =
  1. | N_writable : Syntax.writable nonterminal
  2. | N_var : Annotations.pident nonterminal
  3. | N_utype_array : Syntax.psizetype nonterminal
  4. | N_utype : Syntax.swsize nonterminal
  5. | N_top_annotation : Annotations.annotations nonterminal
  6. | N_top : Syntax.pitem nonterminal
  7. | N_swsize : Syntax.swsize nonterminal
  8. | N_svsize : Syntax.svsize nonterminal
  9. | N_struct_annot : Annotations.annotations nonterminal
  10. | N_storage : Syntax.pstorage nonterminal
  11. | N_stor_type : Syntax.pstotype nonterminal
  12. | N_simple_attribute : Annotations.simple_attribute nonterminal
  13. | N_separated_nonempty_list_option_COMMA__var_ : Annotations.pident list nonterminal
  14. | N_separated_nonempty_list_empty_var_ : Annotations.pident list nonterminal
  15. | N_separated_nonempty_list_COMMA_var_ : Annotations.pident list nonterminal
  16. | N_separated_nonempty_list_COMMA_range_ : (string * string) list nonterminal
  17. | N_separated_nonempty_list_COMMA_plvalue_ : Syntax.plvalue list nonterminal
  18. | N_separated_nonempty_list_COMMA_pexpr_ : Syntax.pexpr list nonterminal
  19. | N_separated_nonempty_list_COMMA_loc_decl__ : (Annotations.pident * Syntax.pexpr) Location.located list nonterminal
  20. | N_separated_nonempty_list_COMMA_annotation_ : Annotations.annotations nonterminal
  21. | N_separated_nonempty_list_COMMA_annot_stor_type_ : (Annotations.annotations * Syntax.pstotype) list nonterminal
  22. | N_separated_nonempty_list_COMMA_annot_pparamdecl_ : (Annotations.annotations * Syntax.paramdecls) list nonterminal
  23. | N_separated_nonempty_list_COLONCOLON_NID_ : string list nonterminal
  24. | N_range : (string * string) nonterminal
  25. | N_ptype_r : Syntax.ptype_r nonterminal
  26. | N_ptype : Syntax.ptype nonterminal
  27. | N_ptr : Syntax.ptr nonterminal
  28. | N_prim : Annotations.pident nonterminal
  29. | N_prequire1 : Syntax.prequire nonterminal
  30. | N_prequire : (Annotations.pident option * Syntax.prequire list) nonterminal
  31. | N_pparamdecl_empty_ : Syntax.paramdecls nonterminal
  32. | N_pparam : Syntax.pparam nonterminal
  33. | N_pointer : Syntax.writable option nonterminal
  34. | N_plvalues : Syntax.plvals nonterminal
  35. | N_plvalue_r : Syntax.plvalue_r nonterminal
  36. | N_plvalue : Syntax.plvalue nonterminal
  37. | N_pinstr_r : Syntax.pinstr_r nonterminal
  38. | N_pinstr : Syntax.pinstr nonterminal
  39. | N_pif : Syntax.pinstr_r nonterminal
  40. | N_pglobal : Syntax.pglobal nonterminal
  41. | N_pgexpr : Syntax.gpexpr nonterminal
  42. | N_pfundef : Syntax.pfundef nonterminal
  43. | N_pfunbody : Syntax.pfunbody nonterminal
  44. | N_pexpr_r : Syntax.pexpr_r nonterminal
  45. | N_pexpr : Syntax.pexpr nonterminal
  46. | N_pexec : Syntax.pexec nonterminal
  47. | N_peqop : Syntax.peqop nonterminal
  48. | N_pelseif : Syntax.pblock_r nonterminal
  49. | N_pelse : Syntax.pblock nonterminal
  50. | N_pblock_r : Syntax.pblock_r nonterminal
  51. | N_pblock : Syntax.pblock nonterminal
  52. | N_option_writable_ : Syntax.writable option nonterminal
  53. | N_option_unaligned_ : [ `Aligned | `Unaligned ] option nonterminal
  54. | N_option_prefix_RARROW_tuple_annot_stor_type___ : (Annotations.annotations * Syntax.pstotype) list option nonterminal
  55. | N_option_prefix_IF_pexpr__ : Syntax.pexpr option nonterminal
  56. | N_option_pointer_ : Syntax.writable option option nonterminal
  57. | N_option_pblock_ : Syntax.pblock option nonterminal
  58. | N_option_loc_castop1__ : Syntax.castop nonterminal
  59. | N_option_from_ : Annotations.pident option nonterminal
  60. | N_option_call_conv_ : Syntax.pcall_conv option nonterminal
  61. | N_option_attribute_ : Annotations.attribute option nonterminal
  62. | N_option_arr_access_len_ : Syntax.pexpr option nonterminal
  63. | N_option_access_type_ : (unit option * Syntax.swsize Location.located) option nonterminal
  64. | N_option___anonymous_1_ : Annotations.pident list option nonterminal
  65. | N_option_DOT_ : unit option nonterminal
  66. | N_option_COMMA_ : unit option nonterminal
  67. | N_option_COLON_ : unit option nonterminal
  68. | N_nonempty_list_prequire1_ : Syntax.prequire list nonterminal
  69. | N_module_ : Syntax.pprogram nonterminal
  70. | N_loption_separated_nonempty_list_COMMA_var__ : Annotations.pident list nonterminal
  71. | N_loption_separated_nonempty_list_COMMA_range__ : (string * string) list nonterminal
  72. | N_loption_separated_nonempty_list_COMMA_pexpr__ : Syntax.pexpr list nonterminal
  73. | N_loption_separated_nonempty_list_COMMA_annotation__ : Annotations.annotations nonterminal
  74. | N_loption_separated_nonempty_list_COMMA_annot_stor_type__ : (Annotations.annotations * Syntax.pstotype) list nonterminal
  75. | N_loption_separated_nonempty_list_COMMA_annot_pparamdecl__ : (Annotations.annotations * Syntax.paramdecls) list nonterminal
  76. | N_list_top_annotation_ : Annotations.annotations list nonterminal
  77. | N_list_pinstr_ : Syntax.pblock_r nonterminal
  78. | N_list_loc_top__ : Syntax.pprogram nonterminal
  79. | N_keyword : string nonterminal
  80. | N_int : Z.t nonterminal
  81. | N_implicites : Annotations.annotations Location.located nonterminal
  82. | N_from : Annotations.pident nonterminal
  83. | N_castop1 : Syntax.castop1 nonterminal
  84. | N_castop : Syntax.castop nonterminal
  85. | N_cast : Syntax.cast nonterminal
  86. | N_call_conv : Syntax.pcall_conv nonterminal
  87. | N_attribute : Annotations.simple_attribute Location.located nonterminal
  88. | N_arr_access_len : Syntax.pexpr nonterminal
  89. | N_arr_access_i : ((unit option * Syntax.swsize Location.located) option * Syntax.pexpr * Syntax.pexpr option * [ `Aligned | `Unaligned ] option) nonterminal
  90. | N_arr_access : (Warray_.arr_access * (Syntax.swsize Location.located option * Syntax.pexpr * Syntax.pexpr option * [ `Aligned | `Unaligned ] option)) nonterminal
  91. | N_annotations : Annotations.annotations nonterminal
  92. | N_annotationlabel : Syntax.prequire nonterminal
  93. | N_annotation : Annotations.annotation nonterminal
  94. | N_annot_stor_type : (Annotations.annotations * Syntax.pstotype) nonterminal
  95. | N_annot_pparamdecl : (Annotations.annotations * Syntax.paramdecls) nonterminal
include MenhirLib.IncrementalEngine.INSPECTION with type 'a lr1state := 'a lr1state with type production := production with type 'a terminal := 'a terminal with type 'a nonterminal := 'a nonterminal with type 'a env := 'a env
include MenhirLib.IncrementalEngine.SYMBOLS with type 'a terminal := 'a terminal with type 'a nonterminal := 'a nonterminal
Sourcetype 'a symbol =
  1. | T : 'a terminal -> 'a symbol
  2. | N : 'a nonterminal -> 'a symbol

The type 'a symbol represents a terminal or nonterminal symbol. It is the disjoint union of the types 'a terminal and 'a nonterminal.

Sourcetype xsymbol =
  1. | X : 'a symbol -> xsymbol

The type xsymbol is an existentially quantified version of the type 'a symbol. This type is useful in situations where 'a is not statically known.

Sourcetype item = production * int

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.

The following are total ordering functions.

Sourceval compare_terminals : _ terminal -> _ terminal -> int
Sourceval compare_nonterminals : _ nonterminal -> _ nonterminal -> int
Sourceval compare_symbols : xsymbol -> xsymbol -> int
Sourceval compare_productions : production -> production -> int
Sourceval compare_items : item -> item -> int
Sourceval incoming_symbol : 'a lr1state -> 'a symbol

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.

Sourceval items : _ lr1state -> item list

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.

Sourceval rhs : production -> xsymbol list

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

Sourceval nullable : _ nonterminal -> bool

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.

Sourceval first : _ nonterminal -> _ terminal -> bool

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.

Sourceval xfirst : xsymbol -> _ terminal -> bool

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

Sourceval foreach_terminal : (xsymbol -> 'a -> 'a) -> 'a -> 'a

foreach_terminal enumerates the terminal symbols, including error.

Sourceval foreach_terminal_but_error : (xsymbol -> 'a -> 'a) -> 'a -> 'a

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.