Commit 410b65b5 authored by POTTIER Francois's avatar POTTIER Francois Committed by POTTIER Francois
Browse files

Rename [LR1construction] to [LALR], and simplify it, as it now implements LALR mode only.

parent eca2b451
......@@ -11,26 +11,11 @@
(* *)
(******************************************************************************)
(* This module constructs an LR(1) automaton for the grammar described by the
(* This module constructs an LALR automaton for the grammar described by the
module [Grammar]. *)
(* Depending on Menhir's settings, one of four methods is used:
- Canonical mode: no merging of states at all.
- Inclusion only: a new state can be merged into a larger existing state.
The reverse is forbidden, though: a smaller existing state will not be
grown if a new larger state must be created. This mode is undocumented
and may be removed in the future.
- Normal mode: a version of Pager's weak compatibility criterion is used to
determine which states can be merged. Merging is performed on the fly,
during construction. A proposed new state can be merged with an existing
state, which is then grown.
- LALR mode: two states are merged as soon as they have the same LR(0) core.
*)
(* In LALR mode, two LR(1) states are merged as soon as they have the same
LR(0) core. *)
open Grammar
......@@ -92,25 +77,7 @@ let follow_state (msg : string) (node : node) (print : bool) =
(* The following two mutually recursive functions are invoked when the state
associated with an existing node grows. The node's descendants are examined
and grown until a fixpoint is reached.
This work is performed in an eager manner: we do not attempt to build any
new transitions until all existing nodes have been suitably grown. Indeed,
building new transitions requires making merging decisions, and such
decisions cannot be made on a sound basis unless all existing nodes have
been suitably grown. Otherwise, one could run into a dead end where two
successive, incompatible merging decisions are made, because the
consequences of the first decision (growing descendant nodes) were not made
explicit before the second decision was taken. This was a bug in versions
of Menhir ante 20070520.
Although I wrote this code independently, I later found out that it seems
quite similar to the code in Karl Schimpf's Ph.D. thesis (1981), page 35.
It is necessary that all existing transitions be explicit before the [grow]
functions are called. In other words, if it has been decided that there
will be a transition from [node1] to [node2], then [node1.transitions] must
be updated before [grow] is invoked. *)
and grown until a fixpoint is reached. *)
(* [grow node state] grows the existing node [node], if necessary, so that its
associated state subsumes [state]. If this represents an actual (strict)
......@@ -119,46 +86,7 @@ let follow_state (msg : string) (node : node) (print : bool) =
let rec grow node state =
if Lr0.subsume state node.state then
follow_state "Target state is unaffected" node false
else begin
(* In versions of Menhir prior to June 2008, I wrote this:
If I know what I am doing, then the new state that is being
merged into the existing state should be compatible, in
Pager's sense, with the existing node. In other words,
compatibility should be preserved through transitions.
and the code contained this assertion:
assert (Lr0.compatible state node.state);
assert (Lr0.eos_compatible state node.state);
However, this was wrong. See, for instance, the sample grammars
cocci.mly and boris-mini.mly. The problem is particularly clearly
apparent in boris-mini.mly, where it only involves inclusion of
states -- the definition of Pager's weak compatibility does not
enter the picture. Here is, roughly, what is going on.
Assume we have built some state A, which, along some symbol S,
has a transition to itself. This means, in fact, that computing
the successor of A along S yields a *subset* of A, that is,
succ(A, S) <= A.
Then, we wish to build a new state A', which turns out to be a
superset of A, so we decide to grow A. (The fact that A is a
subset of A' implies that A and A' are Pager-compatible.) As
per the code below, we immediately update the state A in place,
to become A'. Then, we inspect the transition along symbol S.
We find that the state succ(A', S) must be merged into A'.
In this situation, the assertions above require succ(A', S)
to be compatible with A'. However, this is not necessarily
the case. By monotonicity of succ, we do have succ(A, S) <=
succ(A', S). But nothing says that succ(A', S) and A' are related
with respect to inclusion, or even Pager-compatible. The
grammar in boris-mini.mly shows that they are not.
*)
else begin
(* Grow [node]. *)
......@@ -195,12 +123,12 @@ and grow_successors node =
let queue : node Queue.t =
Queue.create()
(* A mapping of LR(0) node numbers to lists of nodes. This allows us to
efficiently find all existing nodes that are core-compatible with a
newly found state. *)
(* A mapping of LR(0) node numbers to at most one node. This allows us to
efficiently find the unique node (if it exists) that is core-compatible
with a newly found state. *)
let map : node list array =
Array.make Lr0.n []
let map : node option array =
Array.make Lr0.n None
(* A counter that allows assigning raw numbers to nodes. *)
......@@ -236,7 +164,8 @@ let create (state : lr1state) : node =
let k = Lr0.core state in
assert (k < Lr0.n);
map.(k) <- node :: map.(k);
assert (map.(k) = None);
map.(k) <- Some node;
(* Enqueue this node for further examination. *)
......@@ -253,127 +182,34 @@ let create (state : lr1state) : node =
(* -------------------------------------------------------------------------- *)
(* Materializing a transition turns its target state into a (fresh or
existing) node. There are three scenarios: the proposed new state can be
subsumed by an existing state, compatible with an existing state, or
neither. *)
exception Subsumed of node
exception Compatible of node
existing) node. There are two scenarios: the proposed new state may
or may not be subsumed by an existing state. *)
let materialize (source : node) (symbol : Symbol.t) (target : lr1state) : unit =
try
(* Debugging output. *)
follow_transition false source symbol target;
(* Find all existing core-compatible states. *)
let k = Lr0.core target in
assert (k < Lr0.n);
let similar = map.(k) in
(* Check whether we need to create a new node or can reuse an existing
state. *)
(* 20120525: the manner in which this check is performed depends on
[Settings.construction_mode]. There are now three modes. *)
(* 20150204: there are now four modes. *)
begin match Settings.construction_mode with
| Settings.ModeCanonical ->
(* In a canonical automaton, two states can be merged only if they
are identical. *)
List.iter (fun node ->
if Lr0.subsume target node.state &&
Lr0.subsume node.state target then
raise (Subsumed node)
) similar
| Settings.ModeInclusionOnly
| Settings.ModePager ->
(* A more aggressive approach is to take subsumption into account:
if the new candidate state is a subset of an existing state,
then no new node needs to be created. Furthermore, the existing
state does not need to be enlarged. *)
(* 20110124: require error compatibility in addition to subsumption. *)
List.iter (fun node ->
if Lr0.subsume target node.state &&
Lr0.error_compatible target node.state then
raise (Subsumed node)
) similar
| Settings.ModeLALR ->
()
end;
begin match Settings.construction_mode with
| Settings.ModeCanonical
| Settings.ModeInclusionOnly ->
()
| Settings.ModePager ->
(* One can be even more aggressive and check whether the existing state is
compatible, in Pager's sense, with the new state. If so, there is no
need to create a new state: just merge the new state into the existing
one. The result is a state that may be larger than each of the two
states that have been merged. *)
(* 20110124: require error compatibility in addition to the existing
compatibility criteria. *)
List.iter (fun node ->
if Lr0.compatible target node.state &&
Lr0.eos_compatible target node.state &&
Lr0.error_compatible target node.state then
raise (Compatible node)
) similar
| Settings.ModeLALR ->
(* In LALR mode, as soon as there is one similar state -- i.e. one
state that shares the same LR(0) core -- we merge the new state
into the existing one. *)
List.iter (fun node ->
raise (Compatible node)
) similar
end;
(* The above checks have failed. Create a new node. Two states that are in
the subsumption relation are also compatible. This implies that the
newly created node does not subsume any existing states. *)
source.transitions <- SymbolMap.add symbol (create target) source.transitions
with
(* Debugging output. *)
| Subsumed node ->
follow_transition false source symbol target;
(* Join an existing target node. *)
(* Find all existing core-compatible states. *)
follow_state "Joining existing state" node false;
source.transitions <- SymbolMap.add symbol node source.transitions
let k = Lr0.core target in
assert (k < Lr0.n);
| Compatible node ->
(* Check whether we must create a new node or reuse an existing one. *)
(* Join and grow an existing target node. It seems important that the
new transition is created before [grow_successors] is invoked, so
that all transition decisions made so far are explicit. *)
(* In LALR mode, as soon as there is one similar state -- i.e. one state
that shares the same LR(0) core -- we merge the new state into the
existing one. *)
node.state <- Lr0.union target node.state;
follow_state "Joining and growing existing state" node true;
match map.(k) with
| None ->
(* There is no similar state. Create a new node. *)
source.transitions <- SymbolMap.add symbol (create target) source.transitions
| Some node ->
(* There is an existing node. Join it and grow it if necessary. *)
source.transitions <- SymbolMap.add symbol node source.transitions;
grow_successors node
grow node target
(* -------------------------------------------------------------------------- *)
......@@ -382,7 +218,7 @@ let materialize (source : node) (symbol : Symbol.t) (target : lr1state) : unit =
(* Populate the queue with the start nodes and store them in an array. *)
let entry : node ProductionMap.t =
ProductionMap.map (fun (k : Lr0.node) ->
ProductionMap.map (fun k ->
create (Lr0.start k)
) Lr0.entry
......
......@@ -11,7 +11,7 @@
(* *)
(******************************************************************************)
(* This module constructs an LR(1) automaton for the grammar described by the
(* This module constructs an LALR automaton for the grammar described by the
module [Grammar]. *)
(* In this construction, precedence declarations are not taken into account.
......
......@@ -14,7 +14,8 @@
open Grammar
open LR1Sigs
(* This module first constructs an LR(1) automaton by using [Lr1construction].
(* This module first constructs an LR(1) automaton by using an appropriate
construction method (LALR, Pager, canonical).
Then, this automaton is further transformed (in place), in three steps:
- Silent conflict resolution (without warnings),
......@@ -57,7 +58,7 @@ let algo : (module ALGORITHM) =
| ModePager ->
(module LR1Pager : ALGORITHM)
| ModeLALR ->
(module Lr1construction : ALGORITHM)
(module LALR : ALGORITHM)
)
module Algorithm =
......
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