Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
POTTIER Francois
menhir
Commits
26b2a3dc
Commit
26b2a3dc
authored
Feb 02, 2020
by
POTTIER Francois
Committed by
POTTIER Francois
Feb 10, 2020
Browse files
Reformulate LALR as an instance of Fix.DataFlow.
parent
f27dddeb
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
48 additions
and
121 deletions
+48
121
src/LALR.ml
src/LALR.ml
+48
121
No files found.
src/LALR.ml
View file @
26b2a3dc
...
...
@@ 23,151 +23,78 @@ type lr1state =
Lr0
.
lr1state
module
Run
()
=
struct
let
()
=
()
(*  *)
(* Since the LALR automaton has exactly the same states as the LR(0)
automaton, up to lookahead information, we can use the same state
numbers. *)
(* The LALR automaton has exactly the same states as the LR(0) automaton, up
to lookahead information. Therefore, we can use the same state numbers.
Thus, the states and the transitions of the LALR automaton are the same as
those of the LR(0) automaton! *)
type
node
=
int
let
n
=
Lr0
.
n
(* This means that we have almost nothing to do: in fact, the only thing that
we have to do is compute a mapping of LR(0) nodes to LR(1) states. *)
(* Each node is associated with a state. This state can change during
construction as nodes are merged. *)
(* This computation can be viewed as a fixed point computation. In fact, it is
a special kind of fixed point computation: it can be viewed as a forward
data flow analysis where the graph is the LR(0) automaton and a property is
an LR(1) state. *)
let
states
:
lr1state
option
array
=
Array
.
make
n
None
(*  *)
(* Output debugging information if [followconstruction] is enabled. *)
let
print_state
(
state
:
lr1state
)
=
Lr0
.
print_closure
""
state
let
print_ostate
(
ostate
:
lr1state
option
)
=
match
ostate
with

None
>
"<none>"

Some
state
>
print_state
state
let
follow_transition
(
source
:
node
)
(
symbol
:
Symbol
.
t
)
(
target
:
node
)
(
state
:
lr1state
)
=
if
Settings
.
follow
then
Printf
.
fprintf
stderr
"Examining transition out of state %d along symbol %s to state %d.
\n
\
Proposed target state:
\n
%s"
source
(
Symbol
.
print
symbol
)
target
(
print_state
state
)
let
follow_state
(
msg
:
string
)
(
node
:
node
)
(
print
:
bool
)
=
if
Settings
.
follow
then
Printf
.
fprintf
stderr
"%s: %d.
\n
%s
\n
"
msg
node
(
if
print
then
print_ostate
states
.
(
node
)
else
""
)
(*  *)
type
node
=
int
(* A stack of pending nodes, whose outgoing transitions must be reexamined. *)
(* A property is an LR(1) state. The function [join] is used to merge the
contributions of multiple predecessor states. The function [leq] is used to
detect stabilization. *)
(* Invariant: if a node is in the stack, then [states.(node)] is not [None]. *)
module
P
=
struct
type
property
=
lr1state
let
leq
=
Lr0
.
subsume
let
join
=
Lr0
.
union
end
let
stack
:
node
Stack
.
t
=
Stack
.
create
()
(* The graph. *)
(* The Boolean array [dirty] keeps track of which nodes are in the stack and
allows us to avoid pushing a node onto the stack when it is already in the
stack. *)
module
G
=
struct
let
dirty
:
bool
array
=
Array
.
make
n
false
type
variable
=
node
type
property
=
P
.
property
let
schedule
node
=
if
not
dirty
.
(
node
)
then
begin
dirty
.
(
node
)
<
true
;
Stack
.
push
node
stack
end
(* The root nodes are the entry nodes of the LR(0) automaton. The properties
associated with these nodes are given by the function [Lr0.start]. *)
(*  *)
let
foreach_root
f
=
ProductionMap
.
iter
(
fun
_prod
node
>
f
node
(
Lr0
.
start
node
)
)
Lr0
.
entry
(* [examine] examines a node that has just been taken out of the stack. Its
outgoing transitions are inspected. If a successor node is newly discovered
or updated, then it is scheduled or rescheduled for examination. *)
let
rec
examine
node
=
(* Fetch the LR(1) state currently associated with this node. *)
let
state
:
lr1state
=
Option
.
force
states
.
(
node
)
in
(* Inspect the node's outgoing transitions. *)
SymbolMap
.
iter
(
fun
symbol
(
successor_node
:
node
)
>
let
successor_state
:
lr1state
=
Lr0
.
transition
symbol
state
in
follow_transition
node
symbol
successor_node
successor_state
;
inspect
successor_node
successor_state
)
(
Lr0
.
outgoing_edges
node
)
(* [inspect node state] ensures that the state currently associated with
[node] is at least [state]. If this requires an update of [states.(node)],
then [node] is (re)scheduled for examination. *)
and
inspect
node
state
=
match
states
.
(
node
)
with

None
>
(* [node] is newly discovered. *)
follow_state
"Target state is newly discovered"
node
true
;
states
.
(
node
)
<
Some
state
;
schedule
node

Some
current
>
(* [node] has been discovered earlier. *)
if
Lr0
.
subsume
state
current
then
begin
(* It is unaffected. *)
follow_state
"Target state is unaffected"
node
false
end
else
begin
(* It is affected and must itself be scheduled. *)
states
.
(
node
)
<
Some
(
Lr0
.
union
state
current
);
follow_state
"Growing existing state"
node
true
;
schedule
node
end
(*  *)
(* The edges are the edges of the LR(0) automaton, and the manner in which
each edge contributes to the computation of a property is given by the
function [Lr0.transition]. *)
(* The actual construction process. *)
let
foreach_successor
node
state
f
=
SymbolMap
.
iter
(
fun
symbol
(
successor_node
:
node
)
>
let
successor_state
:
lr1state
=
Lr0
.
transition
symbol
state
in
f
successor_node
successor_state
)
(
Lr0
.
outgoing_edges
node
)
(* Populate the stack with the entry nodes. *)
end
let
()
=
ProductionMap
.
iter
(
fun
_prod
node
>
states
.
(
node
)
<
Some
(
Lr0
.
start
node
);
schedule
node
)
Lr0
.
entry
(* Run the data flow computation. *)
(* As long as the stack is nonempty, examine the nodes in it. *)
let
()
=
try
while
true
do
let
node
=
Stack
.
pop
stack
in
dirty
.
(
node
)
<
false
;
examine
node
done
with
Stack
.
Empty
>
()
module
F
=
Fix
.
DataFlow
.
ForIntSegment
(
Lr0
)(
P
)(
G
)
(* [solution : variable > property option]. *)
(* Because every node is reachable, this function never returns [None]. *)
(*  *)
(* Expose the mapping of nodes to LR(1) states. *)
let
n
=
Lr0
.
n
let
states
:
lr1state
array
=
Array
.
map
Option
.
force
states
Array
.
init
n
(
fun
node
>
Option
.
force
(
F
.
solution
node
))
let
state
:
node
>
lr1state
=
Array
.
get
states
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment