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
af3bd6e2
Commit
af3bd6e2
authored
Nov 19, 2020
by
POTTIER Francois
Browse files
Remove the redundancy between StackSymbols and Invariant.
parent
dd17fa7b
Pipeline
#187980
passed with stages
in 1 minute and 14 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
2 additions
and
41 deletions
+2
-41
src/invariant.ml
src/invariant.ml
+2
-41
No files found.
src/invariant.ml
View file @
af3bd6e2
...
...
@@ -17,47 +17,8 @@
open
Grammar
module
C
=
Conflict
(* artificial dependency; ensures that [Conflict] runs first *)
(* ------------------------------------------------------------------------ *)
(* Compute a lower bound on the height of the stack at every state. At the
same time, 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
stack_symbols
=
StackSymbols
.
stack_symbols
let
stack_height
(
node
:
Lr1
.
node
)
:
int
=
Array
.
length
(
stack_symbols
node
)
...
...
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