invariant.mli 4.83 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 General Public License version 2, as described in the    *)
(*  file LICENSE.                                                             *)
(*                                                                            *)
(******************************************************************************)

POTTIER Francois's avatar
POTTIER Francois committed
14
(* This module discovers and publishes information about the automaton.
15 16 17 18 19 20 21 22 23

   It determines the shape of the stack when a state is about to be
   entered, when a production is about to be reduced, and when a goto
   transition is about to be taken.

   It also determines which states should be represented (that is,
   need to physically exist on the stack at runtime) and which symbols
   need to keep track of (start or end) positions.

24
   It also determines which automaton states could have to deal with an
POTTIER Francois's avatar
POTTIER Francois committed
25 26 27 28 29
   [error] token.

   The information computed in this module is used in the code back-end,
   in the Coq back-end, and in the automated production of .messages files.
   It is not used in the table back-end. *)
30 31 32 33 34 35 36 37 38 39 40 41

open Grammar

(* ------------------------------------------------------------------------- *)
(* A representation of stack shapes. *)

(* A word is a representation of a stack or stack suffix. *)

type word

(* [fold] folds over a word. At each cell, [f] is applied to the
   accumulator, to a Boolean flag that tells whether the cell holds a
42
   state, to the set of possible states of the cell, and to the symbol
43 44 45 46 47 48 49 50 51 52
   associated with the cell. The stack is visited from bottom to top. *)

val fold: ('a -> bool -> Symbol.t -> Lr1.NodeSet.t -> 'a) -> 'a -> word -> 'a

(* [fold_top f accu s] is analogous to [fold], but only folds over the
   top stack cell, if there is one, so that [f] is either not invoked
   at all or invoked just once. *)

val fold_top: (bool -> Symbol.t -> 'a) -> 'a -> word -> 'a

53 54
(* [print w] produces a string representation of the word [w]. Only the
   symbols are shown. One space is printed in front of each symbol. *)
55 56 57

val print: word -> string

58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
(* ------------------------------------------------------------------------- *)
(* Information about the stack. *)

(* [stack s] is the structure of the stack at state [s]. *)

val stack: Lr1.node -> word

(* [prodstack prod] is the structure of the stack when production
   [prod] is about to be reduced. This function should not be called
   if production [prod] is never reduced. *)

val prodstack: Production.index -> word

(* [gotostack nt] is the structure of the stack when a shift
   transition over nonterminal [nt] is about to be taken. It
   consists of just one cell. *)

val gotostack: Nonterminal.t -> word

(* [rewind s] explains how to rewind the stack when dealing with an
   error in state [s]. It produces an instruction to either die
   (because no state on the stack can handle errors) or pop a suffix
   of the stack. In the latter case, one reaches a state that is
   either represented (its identity is physically stored in the
   bottommost cell that is popped) or unrepresented (its identity is
   statically known). *)

type instruction =
  | Die
  | DownTo of word * state

and state =
  | Represented
  | UnRepresented of Lr1.node

val rewind: Lr1.node -> instruction

(* ------------------------------------------------------------------------- *)
(* Information about which states and positions need to physically
   exist on the stack. *)

(* [represented s] tells whether state [s] must have an explicit
   representation, that is, whether it is pushed onto the stack. *)

val represented: Lr1.node -> bool

(* [startp symbol] and [endp symbol] tell whether start or end
   positions must be recorded for symbol [symbol]. *)

val startp: Symbol.t -> bool
val endp: Symbol.t -> bool

(* ------------------------------------------------------------------------- *)
(* Information about error handling. *)

(* [errorpeeker s] tells whether state [s] can potentially peek at an
114 115
   error. This is the case if, in state [s], an error token may be on
   the stream. *)
116 117 118 119 120 121 122 123 124 125

val errorpeeker: Lr1.node -> bool

(* ------------------------------------------------------------------------- *)
(* Miscellaneous. *)

(* [universal symbol] tells whether every represented state has an
   outgoing transition along [symbol]. *)

val universal: Symbol.t -> bool