Commit f92028e0 authored by POTTIER Francois's avatar POTTIER Francois

Document the assumptions under which $symbolstartpos is optimized.

parent c1e559ff
...@@ -161,3 +161,6 @@ ...@@ -161,3 +161,6 @@
% URLs. % URLs.
\newcommand{\compcertgithub}{https://github.com/AbsInt/CompCert/tree/master} \newcommand{\compcertgithub}{https://github.com/AbsInt/CompCert/tree/master}
\newcommand{\compcertgithubfile}[1]{\href{\compcertgithub/#1}{\texttt{#1}}} \newcommand{\compcertgithubfile}[1]{\href{\compcertgithub/#1}{\texttt{#1}}}
% Position keywords.
\newcommand{\ksymbolstartpos}{\texttt{\$symbolstartpos}\xspace}
...@@ -1719,7 +1719,7 @@ the author of the lexical analyzer.) ...@@ -1719,7 +1719,7 @@ the author of the lexical analyzer.)
& start position of the symbol named \verb+$+\nt{i} or \nt{id} \\ & start position of the symbol named \verb+$+\nt{i} or \nt{id} \\
\verb+$endpos(+ \verb+$+\nt{i} \barre \nt{id} \verb+)+ \verb+$endpos(+ \verb+$+\nt{i} \barre \nt{id} \verb+)+
& end position of the symbol named \verb+$+\nt{i} or \nt{id} \\ & end position of the symbol named \verb+$+\nt{i} or \nt{id} \\
\verb+$symbolstartpos+ & start position of the leftmost symbol \nt{id} such that \ksymbolstartpos & start position of the leftmost symbol \nt{id} such that
\verb+$startpos(+\nt{id}\verb+) != $endpos(+\nt{id}\verb+)+; \\& \verb+$startpos(+\nt{id}\verb+) != $endpos(+\nt{id}\verb+)+; \\&
if there is no such symbol, \verb+$endpos+ \\[2mm] if there is no such symbol, \verb+$endpos+ \\[2mm]
\verb+$startofs+ \\ \verb+$startofs+ \\
...@@ -1739,7 +1739,7 @@ the author of the lexical analyzer.) ...@@ -1739,7 +1739,7 @@ the author of the lexical analyzer.)
\begin{tabular}{ll@{\hskip2cm}l} \begin{tabular}{ll@{\hskip2cm}l}
% Positions. % Positions.
\verb+symbol_start_pos()+ & \verb+symbol_start_pos()+ &
\verb+$symbolstartpos+ \\ \ksymbolstartpos \\
\verb+symbol_end_pos()+ & \verb+symbol_end_pos()+ &
\verb+$endpos+ \\ \verb+$endpos+ \\
\verb+rhs_start_pos i+ & \verb+rhs_start_pos i+ &
...@@ -1795,22 +1795,42 @@ modifier \verb+modifier?+. If this modifier turns out to be absent, then its ...@@ -1795,22 +1795,42 @@ modifier \verb+modifier?+. If this modifier turns out to be absent, then its
start position is (by definition) the end position of the most recently parsed start position is (by definition) the end position of the most recently parsed
symbol. This may not be what is desired: perhaps the user would prefer in this symbol. This may not be what is desired: perhaps the user would prefer in this
case to use the start position of the symbol \verb+variable+. This is achieved by case to use the start position of the symbol \verb+variable+. This is achieved by
using \verb+$symbolstartpos+ instead of \verb+$startpos+. By definition, using \ksymbolstartpos instead of \verb+$startpos+. By definition,
\verb+$symbolstartpos+ is the start position of the leftmost symbol whose \ksymbolstartpos is the start position of the leftmost symbol whose
start and end positions differ. In this example, the computation of start and end positions differ. In this example, the computation of
\verb+$symbolstartpos+ skips the absent \verb+modifier+, whose start and end \ksymbolstartpos skips the absent \verb+modifier+, whose start and end
positions coincide, and returns the start position of the symbol \verb+variable+ positions coincide, and returns the start position of the symbol \verb+variable+
(assuming this symbol has distinct start and end positions). (assuming this symbol has distinct start and end positions).
% On pourrait souligner que $symbolstartpos renvoie la $startpos du premier
% symbole non vide, et non pas la $symbolstartpos du premier symbole non vide.
% Donc ça peut rester un peu contre-intuitif, et ne pas correspondre
% exactement à ce que l'on attend. D'ailleurs, le calcul de $symbolstartpos
% est préservé par %inline (on obtient cela très facilement en éliminant
% $symbolstartpos avant l'inlining) mais ne correspond pas à ce que donnerait
% $symbolstartpos après un inlining manuel. Fondamentalement, cette notion de
% $symbolstartpos ne tourne pas très rond.
There is no keyword \verb+$symbolendpos+. Indeed, the problem There is no keyword \verb+$symbolendpos+. Indeed, the problem
with \verb+$startpos+ is due to the asymmetry in the definition with \verb+$startpos+ is due to the asymmetry in the definition
of \verb+$startpos+ and \verb+$endpos+ in the case of an empty right-hand of \verb+$startpos+ and \verb+$endpos+ in the case of an empty right-hand
side, and does not affect \verb+$endpos+. side, and does not affect \verb+$endpos+.
The positions computed by Menhir are exactly the same as computed \newcommand{\fineprint}{\footnote{%
by \verb+ocamlyacc+. More precisely, \fref{fig:pos:mapping} sums up how to The computation of \ksymbolstartpos
translate a call to the \texttt{Parsing} module, as used in an \ocamlyacc grammar, is optimized by \menhir under two assumptions about the lexer. First,
to a \menhir keyword. \menhir assumes that the lexer never produces a token whose start and end
positions are equal. Second, \menhir assumes that two positions produced
by the lexer are equal if and only if they are physically equal. If the
lexer violates either of these assumptions, the computation of
\ksymbolstartpos could produce a result that differs from
\texttt{Parsing.symbol\_start\_pos()}.
}}
The positions computed by Menhir are exactly the same as those computed by
\verb+ocamlyacc+\fineprint. More precisely, \fref{fig:pos:mapping} sums up how
to translate a call to the \texttt{Parsing} module, as used in an \ocamlyacc
grammar, to a \menhir keyword.
We note that \menhir's \verb+$startpos+ does not appear in the right-hand We note that \menhir's \verb+$startpos+ does not appear in the right-hand
column in \fref{fig:pos:mapping}. In other words, \menhir's \verb+$startpos+ column in \fref{fig:pos:mapping}. In other words, \menhir's \verb+$startpos+
......
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