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
M
menhir
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
12
Issues
12
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
POTTIER Francois
menhir
Commits
3ffb877e
Commit
3ffb877e
authored
Nov 11, 2015
by
POTTIER Francois
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Comment, explaining the constraints that must be imposed by [Invariant].
The old comment was wrong, I think.
parent
6c6982b4
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
35 additions
and
26 deletions
+35
-26
src/invariant.ml
src/invariant.ml
+35
-26
No files found.
src/invariant.ml
View file @
3ffb877e
...
...
@@ -596,32 +596,41 @@ let rewind node : instruction =
rewind
w
(* ------------------------------------------------------------------------ *)
(* We now determine which positions must be kept track of. For
simplicity, we do this on a per symbol basis. That is, for each
symbol, either we never keep track of position information, or we
always do. In fact, we do distinguish start and end positions.
This leads to computing two sets of symbols -- those that keep
track of their start position and those that keep track of their
end position.
A symbol on the right-hand side of a production must keep track of
its (start or end) position if that position is explicitly
requested by a semantic action.
Furthermore, if the left-hand symbol of a production must keep
track of its start (resp. end) position, then the first
(resp. last) symbol of its right-hand side (if there is one) must
do so as well. That is, unless the right-hand side is empty. *)
(* 2015/11/04. When an epsilon production is reduced, the top stack cell is
consulted for its end position. This implies that this cell must exist and
must store an end position! Thus, we have the following constraint: if some
state whose incoming symbol is [sym] can reduce an epsilon production, then
[sym] must keep track of its end position. (Furthermore, if some initial
state can reduce an epsilon production, then the sentinel cell at the bottom
of the stack must contain a position. This does not concern us here.)
Similarly, if some state whose incoming symbol is [sym] uses [$endpos($0)],
then [sym] must keep track of its end position. *)
(* We now determine which positions must be kept track of. For simplicity, we
do this on a per-symbol basis. That is, for each symbol, either we never
keep track of position information, or we always do. In fact, we do
distinguish start and end positions. This leads to computing two sets of
symbols -- those that keep track of their start position and those that
keep track of their end position.
A symbol on the right-hand side of a production must keep track of its
(start or end) position if that position is explicitly requested by a
semantic action.
Furthermore, if the left-hand symbol of a production must keep track of its
start (resp. end) position, then the first (resp. last) symbol of its
right-hand side (if there is one) must do so as well. That is, unless the
right-hand side is empty. *)
(* 2015/11/04. When an epsilon production [prod] is reduced, the top stack cell
may be consulted for its end position. This implies that this cell must exist
and must store an end position! Now, when does this happen?
1- This happens if the left-hand symbol of the production, [nt prod], keeps
track of its start or end position.
2- This happens if the semantic action explicitly mentions the keyword
[$endpos($0)].
Now, if this happens, what should we do?
a- If this happens in a state [s] whose incoming symbol is [sym], then [sym]
must keep track of its end position.
b- If this happens in an initial state, where the stack may be empty, then
the sentinel cell at the bottom of the stack must contain an end position.
Point (b) doesn't concern us here, but point (a) does. We must implement the
constraint (1) \/ (2) -> (a). *)
open
Keyword
...
...
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