Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
POTTIER Francois
menhir
Commits
d42a810e
Commit
d42a810e
authored
Nov 19, 2020
by
POTTIER Francois
Browse files
Turn StackSymbols into a functor.
parent
af3bd6e2
Changes
4
Hide whitespace changes
Inline
Side-by-side
src/StackSymbols.ml
View file @
d42a810e
...
...
@@ -12,7 +12,6 @@
(******************************************************************************)
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. *)
...
...
@@ -33,40 +32,44 @@ module C = Conflict (* artificial dependency; ensures that [Conflict] runs first
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"
(* Printing. *)
let
buffer
=
Buffer
.
create
1024
let
print_stack_symbols
node
=
stack_symbols
node
|>
Array
.
iter
(
fun
symbol
->
Printf
.
bprintf
buffer
" %s"
(
Symbol
.
print
symbol
)
);
let
s
=
Buffer
.
contents
buffer
in
Buffer
.
clear
buffer
;
s
module
Run
()
=
struct
(* Compute and tabulate this information at the level of the LR(0)
automaton. *)
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
)
(* 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"
(* Printing. *)
let
buffer
=
Buffer
.
create
1024
let
print_stack_symbols
node
=
stack_symbols
node
|>
Array
.
iter
(
fun
symbol
->
Printf
.
bprintf
buffer
" %s"
(
Symbol
.
print
symbol
)
);
let
s
=
Buffer
.
contents
buffer
in
Buffer
.
clear
buffer
;
s
end
src/StackSymbols.mli
View file @
d42a810e
...
...
@@ -16,14 +16,18 @@
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. *)
module
Run
()
:
sig
val
stack_symbols
:
Lr1
.
node
->
Symbol
.
t
array
(* [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. *)
(* [print_stack_symbols s] is a printed representation of the known
prefix of the stack at state [s]. Every symbol is preceded with
a space. *)
val
stack_symbols
:
Lr1
.
node
->
Symbol
.
t
array
val
print_stack_symbols
:
Lr1
.
node
->
string
(* [print_stack_symbols s] is a printed representation of the known
prefix of the stack at state [s]. Every symbol is preceded with
a space. *)
val
print_stack_symbols
:
Lr1
.
node
->
string
end
src/interpret.ml
View file @
d42a810e
...
...
@@ -240,6 +240,12 @@ let interpret_error_aux log poss ((_, terminals) as sentence) fail succeed =
let
default_message
=
"<YOUR SYNTAX ERROR MESSAGE HERE>
\n
"
(* This is needed in the following function. If [print_messages_auto] is never
called, then we end up needlessly performing this analysis. Fortunately, it
is extremely cheap. *)
module
SS
=
StackSymbols
.
Run
()
(* [print_messages_auto] displays just the sentence and the auto-generated
comments. [otarget] may be [None], in which case the auto-generated comment
is just a warning that this sentence does not end in an error. *)
...
...
@@ -268,7 +274,7 @@ let print_messages_auto (nt, sentence, otarget) : unit =
"## The known suffix of the stack is as follows:
\n
\
##%s
\n
\
##
\n
"
(
S
tackSymbols
.
print_stack_symbols
s'
)
(
S
S
.
print_stack_symbols
s'
)
;
if
spurious
<>
[]
then
begin
Printf
.
printf
...
...
src/invariant.ml
View file @
d42a810e
...
...
@@ -18,7 +18,8 @@ open Grammar
module
C
=
Conflict
(* artificial dependency; ensures that [Conflict] runs first *)
let
stack_symbols
=
StackSymbols
.
stack_symbols
let
module
SS
=
StackSymbols
.
Run
()
in
SS
.
stack_symbols
let
stack_height
(
node
:
Lr1
.
node
)
:
int
=
Array
.
length
(
stack_symbols
node
)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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