IncrementalEngine.ml 20.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(******************************************************************************)
(*                                                                            *)
(*                                   Menhir                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*              Yann Régis-Gianas, PPS, Université Paris Diderot              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU Library General Public License version 2, with a         *)
(*  special exception on linking, as described in the file LICENSE.           *)
(*                                                                            *)
(******************************************************************************)

14 15
type position = Lexing.position

16 17
open General

18 19 20 21 22 23 24 25 26
(* This signature describes the incremental LR engine. *)

(* In this mode, the user controls the lexer, and the parser suspends
   itself when it needs to read a new token. *)

module type INCREMENTAL_ENGINE = sig

  type token

27 28 29 30 31 32
  (* 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. *)

  type production

33 34
  (* The type ['a checkpoint] represents an intermediate or final state of the
     parser. An intermediate checkpoint is a suspension: it records the parser's
35 36 37 38
     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. *)

39
  (* [Accepted] and [Rejected] are final checkpoints. [Accepted] carries a
40 41
     semantic value. *)

42
  (* [InputNeeded] is an intermediate checkpoint. It means that the parser wishes
43 44
     to read one token before continuing. *)

45
  (* [Shifting] is an intermediate checkpoint. It means that the parser is taking
46 47 48 49 50
     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.) *)

51
  (* [AboutToReduce] is an intermediate checkpoint. It means that the parser is
52 53
     about to perform a reduction step. It exposes the parser's current
     state as well as the production that is about to be reduced. *)
54

55
  (* [HandlingError] is an intermediate checkpoint. It means that the parser has
56
     detected an error and is currently handling it, in several steps. *)
57

58 59 60 61 62 63 64 65 66 67 68 69 70
  (* 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. *)

  type 'a env
71

72
  type 'a checkpoint = private
73 74 75 76
    | InputNeeded of 'a env
    | Shifting of 'a env * 'a env * bool
    | AboutToReduce of 'a env * production
    | HandlingError of 'a env
77 78 79 80
    | Accepted of 'a
    | Rejected

  (* [offer] allows the user to resume the parser after it has suspended
81 82 83
     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. *)
84 85

  val offer:
86
    'a checkpoint ->
87
    token * position * position ->
88
    'a checkpoint
89

90
  (* [resume] allows the user to resume the parser after it has suspended
91
     itself with a checkpoint of the form [AboutToReduce (env, prod)] or
92 93 94 95 96
     [HandlingError env]. [resume] expects the old checkpoint 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 [ErrorHandling _]. Its default value
97
     is [`Legacy]. It can be briefly described as follows:
98 99 100 101 102 103 104 105 106 107 108 109 110 111

     - 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 these strategies appear in the file [Engine.ml]. *)

  type strategy =
112
    [ `Legacy | `Simplified ]
113

114
  val resume:
115
    ?strategy:strategy ->
116 117
    'a checkpoint ->
    'a checkpoint
118

119 120 121 122
  (* 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. *)

  type supplier =
123
    unit -> token * position * position
124

125 126
  (* A pair of a lexer and a lexing buffer can be easily turned into a
     supplier. *)
127 128 129 130 131 132 133 134 135 136 137 138 139 140

  val lexer_lexbuf_to_supplier:
    (Lexing.lexbuf -> token) ->
    Lexing.lexbuf ->
    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. *)

  (* [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
141 142 143
     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. *)
144

145
  val loop: ?strategy:strategy -> supplier -> 'a checkpoint -> 'a
146 147 148 149 150

  (* [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
POTTIER Francois's avatar
POTTIER Francois committed
151 152
     observed first). In the former case, it calls [succeed v]. In the latter
     case, it calls [fail] with this checkpoint. It cannot raise [Error].
153

154 155 156 157
     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. *)
158 159 160 161 162

  val loop_handle:
    ('a -> 'answer) ->
    ('a checkpoint -> 'answer) ->
    supplier -> 'a checkpoint -> 'answer
163

POTTIER Francois's avatar
POTTIER Francois committed
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
  (* [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

182 183 184 185 186 187 188
  (* [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. *)
POTTIER Francois's avatar
POTTIER Francois committed
189 190 191 192

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

193
  val shifts: 'a checkpoint -> 'a env option
POTTIER Francois's avatar
POTTIER Francois committed
194

195 196
  (* The function [acceptable] allows testing, after an error has been
     detected, which tokens would have been accepted at this point. It is
POTTIER Francois's avatar
POTTIER Francois committed
197 198
     implemented using [shifts]. Its argument should be an [InputNeeded]
     checkpoint. *)
POTTIER Francois's avatar
POTTIER Francois committed
199 200 201 202 203 204 205 206 207 208 209 210

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

211
  val acceptable: 'a checkpoint -> token -> position -> bool
POTTIER Francois's avatar
POTTIER Francois committed
212

213 214 215 216 217 218
  (* 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. *)

  type 'a lr1state

219 220 221 222
  (* The states of the LR(1) automaton are numbered (from 0 and up). *)

  val number: _ lr1state -> int

223 224 225 226 227 228 229
  (* Productions are numbered. *)

  (* [find_production i] requires the index [i] to be valid. Use with care. *)

  val production_index: production -> int
  val find_production: int -> production

230 231 232
  (* 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,
233
     for some type ['a], the state [s] has type ['a lr1state] and the value [v]
234 235 236
     has type ['a]. In other words, the type [element] is an existential type. *)

  type element =
237
    | Element: 'a lr1state * 'a * position * position -> element
238 239

  (* The parser's stack is (or, more precisely, can be viewed as) a stream of
POTTIER Francois's avatar
POTTIER Francois committed
240
     elements. The type [stream] is defined by the module [General]. *)
241

242 243 244
  (* As of 2017/03/31, the types [stream] and [stack] and the function [stack]
     are DEPRECATED. They might be removed in the future. An alternative way
     of inspecting the stack is via the functions [top] and [pop]. *)
245 246

  type stack = (* DEPRECATED *)
247 248
    element stream

249 250 251 252
  (* This is the parser's stack, a stream of elements. This stream is empty if
     the parser is in an initial state; otherwise, it is non-empty.  The LR(1)
     automaton's current state is the one found in the top element of the
     stack. *)
253

254 255
  val stack: 'a env -> stack (* DEPRECATED *)

POTTIER Francois's avatar
POTTIER Francois committed
256 257 258 259
  (* [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. *)
260 261

  val top: 'a env -> element option
262

POTTIER Francois's avatar
POTTIER Francois committed
263 264
  (* [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
265 266
     index [i] must be nonnegative. The time complexity is O(i). *)

267
  val pop_many: int -> 'a env -> 'a env option
268

POTTIER Francois's avatar
POTTIER Francois committed
269
  (* [get i env] returns the parser's [i]-th stack element. The index [i] is
270 271 272 273 274 275
     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). *)

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

276 277 278 279
  (* [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
280 281 282
     --compile-errors]. *)

  val current_state_number: 'a env -> int
POTTIER Francois's avatar
POTTIER Francois committed
283

284
  (* [equal env1 env2] tells whether the parser configurations [env1] and
285 286
     [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
POTTIER Francois's avatar
POTTIER Francois committed
287 288 289 290 291
     [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). *)
292 293 294

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

295 296 297
  (* These are the start and end positions of the current lookahead token. If
     invoked in an initial state, this function returns a pair of twice the
     initial position. *)
298

299
  val positions: 'a env -> position * position
300

301 302 303 304
  (* 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. *)
305

306
  val env_has_default_reduction: 'a env -> bool
307

308 309 310 311 312
  (* [state_has_default_reduction s] tells whether the state [s] has a default
     reduction. This includes the case where [s] is an accepting state. *)

  val state_has_default_reduction: _ lr1state -> bool

313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
  (* [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. *)

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

  (* [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. *)

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

  (* [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. *)

  val input_needed: 'a env -> 'a checkpoint

345
end
346

347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371
(* This signature is a fragment of the inspection API that is made available
   to the user when [--inspection] is used. This fragment contains type
   definitions for symbols. *)

module type SYMBOLS = sig

  (* The type ['a terminal] represents a terminal symbol. The type ['a
     nonterminal] represents a nonterminal symbol. In both cases, the index
     ['a] represents the type of the semantic values associated with this
     symbol. The concrete definitions of these types are generated. *)

  type 'a terminal
  type 'a nonterminal

  (* The type ['a symbol] represents a terminal or nonterminal symbol. It is
     the disjoint union of the types ['a terminal] and ['a nonterminal]. *)

  type 'a symbol =
    | T : 'a terminal -> 'a symbol
    | N : 'a nonterminal -> 'a symbol

  (* The type [xsymbol] is an existentially quantified version of the type
     ['a symbol]. This type is useful in situations where the index ['a]
     is not statically known. *)

POTTIER Francois's avatar
POTTIER Francois committed
372
  type xsymbol =
373 374 375 376
    | X : 'a symbol -> xsymbol

end

377 378
(* This signature describes the inspection API that is made available to the
   user when [--inspection] is used. *)
379 380 381

module type INSPECTION = sig

382 383 384 385
  (* The types of symbols are described above. *)

  include SYMBOLS

386 387
  (* The type ['a lr1state] is meant to be the same as in [INCREMENTAL_ENGINE]. *)

388
  type 'a lr1state
389

390 391 392 393
  (* The type [production] is meant to be the same as in [INCREMENTAL_ENGINE].
     It represents a production of the grammar. A production can be examined
     via the functions [lhs] and [rhs] below. *)

394 395
  type production

396 397 398 399
  (* 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. *)

400
  type item =
401 402
      production * int

403 404 405 406 407 408 409 410
  (* Ordering functions. *)

  val compare_terminals: _ terminal -> _ terminal -> int
  val compare_nonterminals: _ nonterminal -> _ nonterminal -> int
  val compare_symbols: xsymbol -> xsymbol -> int
  val compare_productions: production -> production -> int
  val compare_items: item -> item -> int

411 412 413 414 415 416
  (* [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]. *)
417

POTTIER Francois's avatar
POTTIER Francois committed
418
  val incoming_symbol: 'a lr1state -> 'a symbol
419

POTTIER Francois's avatar
POTTIER Francois committed
420 421 422 423 424 425
  (* [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. *)

  val items: _ lr1state -> item list

426 427 428
  (* [lhs prod] is the left-hand side of the production [prod]. This is
     always a non-terminal symbol. *)

429 430
  val lhs: production -> xsymbol

431 432 433
  (* [rhs prod] is the right-hand side of the production [prod]. This is
     a (possibly empty) sequence of (terminal or nonterminal) symbols. *)

434 435
  val rhs: production -> xsymbol list

436 437 438 439
  (* [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]. *)

440
  val nullable: _ nonterminal -> bool
441

442 443 444 445
  (* [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]. *)

446 447 448 449 450 451
  val first: _ nonterminal -> _ terminal -> bool

  (* [xfirst] is analogous to [first], but expects a first argument of type
     [xsymbol] instead of [_ terminal]. *)

  val xfirst: xsymbol -> _ terminal -> bool
452

453 454 455 456 457 458 459
  (* [foreach_terminal] enumerates the terminal symbols, including [error].
     [foreach_terminal_but_error] enumerates the terminal symbols, excluding
     [error]. *)

  val foreach_terminal:           (xsymbol -> 'a -> 'a) -> 'a -> 'a
  val foreach_terminal_but_error: (xsymbol -> 'a -> 'a) -> 'a -> 'a

460 461
  (* The type [env] is meant to be the same as in [INCREMENTAL_ENGINE]. *)

462
  type 'a env
463

POTTIER Francois's avatar
POTTIER Francois committed
464
  (* [feed symbol startp semv endp env] causes the parser to consume the
465
     (terminal or nonterminal) symbol [symbol], accompanied with the semantic
POTTIER Francois's avatar
POTTIER Francois committed
466 467 468 469 470
     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. *)
471

472
  val feed: 'a symbol -> position -> 'a -> position -> 'b env -> 'b env
473

474 475
end

476 477 478 479 480 481 482 483 484
(* This signature combines the incremental API and the inspection API. *)

module type EVERYTHING = sig

  include INCREMENTAL_ENGINE

  include INSPECTION
    with type 'a lr1state := 'a lr1state
    with type production := production
485
    with type 'a env := 'a env
486 487

end