Commit a08a0df2 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

New module StackSymbols. This isolates the cheap part of Invariant.

parent 1587005b
(******************************************************************************)
(* *)
(* 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. *)
(* *)
(******************************************************************************)
open Grammar
module C = Conflict (* artificial dependency; ensures that [Conflict] runs first *)
(* We compute a lower bound on the height of the stack at every state, and at
the same time, we compute which symbols are held in this stack prefix. *)
(* In order to compute a lower bound on the height of the stack at a state
[s], we examine the LR(0) items that compose [s]. For each item, if the
bullet is at position [pos], then we can be assured that the height of the
stack is at least [pos]. Thus, we compute the maximum of [pos] over all
items (of which there is at least one). *)
(* The set of items that we use is not closed, but this does not matter; the
items that would be added by the closure would not add any information
regarding the height of the stack, since the bullet is at position 0 in
these items. *)
(* Instead of computing just the stack height, we compute, in the same manner,
which symbols are on the stack at a state [s]. This is an array of symbols
whose length is the height of the stack at [s]. By convention, the top of
the stack is the end of the array. *)
(* We first compute and tabulate this information at the level of the LR(0)
automaton. *)
(* This analysis is extremely fast: on an automaton with over 100,000 states,
it takes under 0.01 second. *)
let stack_symbols : Lr0.node -> Symbol.t array =
let dummy =
Array.make 0 (Symbol.T Terminal.sharp)
in
Misc.tabulate Lr0.n (fun node ->
Item.Set.fold (fun item accu ->
let _prod, _nt, rhs, pos, _length = Item.def item in
if pos > Array.length accu then Array.sub rhs 0 pos else accu
) (Lr0.items node) dummy
)
(* Then, it is easy to extend it to the LR(1) automaton. *)
let stack_symbols (node : Lr1.node) : Symbol.t array =
stack_symbols (Lr0.core (Lr1.state node))
let () =
Time.tick "Computing stack symbols"
(******************************************************************************)
(* *)
(* 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. *)
(* *)
(******************************************************************************)
(* This module computes the known prefix of the stack, a sequence of symbols,
in each of the automaton's states. *)
open Grammar
(* [stack_symbols s] is the known prefix of the stack at state [s]. It
is represented as an array of symbols. By convention, the top of
the stack is the end of the array. *)
val stack_symbols: Lr1.node -> Symbol.t array
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment