Commit bca6a1a9 authored by POTTIER Francois's avatar POTTIER Francois

Documented some naming conventions in --coq mode.

parent 17ca85e5
......@@ -3216,12 +3216,19 @@ The generated file contains several modules:
while establishing the soundness and completeness of the parser.
\end{itemize}
The type of the terminal symbols is an inductive type, with one constructor
for each terminal symbol. A~terminal symbol per se does not carry a the
semantic value. We also define the type \verb+token+ of tokens, that is,
dependent pairs of a terminal symbol and a semantic value of an appropriate
type for this symbol. We model the lexer as an object of type
\verb+Streams.Stream token+, that is, an infinite stream of tokens.
The type~\verb+terminal+ of the terminal symbols is an inductive type, with
one constructor for each terminal symbol. A terminal symbol named \verb+Foo+
in the \verb+.vy+ file is named \verb+Foo't+ in Coq. A~terminal symbol per se
does not carry a the semantic value.
We also define the type \verb+token+ of tokens, that is, dependent pairs of a
terminal symbol and a semantic value of an appropriate type for this symbol.
We model the lexer as an object of type \verb+Streams.Stream token+, that is,
an infinite stream of tokens.
The type~\verb+nonterminal+ of the non-terminal symbols is an inductive type,
with one constructor for each non-terminal symbol. A non-terminal symbol named
\verb+Bar+ in the \verb+.vy+ file is named \verb+Bar'nt+ in Coq.
The proof of termination of an LR(1) parser in the case of invalid input seems
far from obvious. We did not find such a proof in the literature. In an
......
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