Commit b44fd3ae authored by POTTIER Francois's avatar POTTIER Francois

Proof-reading.

parent 5247c2f5
...@@ -1958,15 +1958,15 @@ a \texttt{.mly} file. There are however several restrictions: ...@@ -1958,15 +1958,15 @@ a \texttt{.mly} file. There are however several restrictions:
The generated file contains several modules: The generated file contains several modules:
\begin{itemize} \begin{itemize}
\item Module \verb+Gram+ contains the types of terminals and \item The module \verb+Gram+ defines the terminal and
non-terminals, the grammar description, and semantic actions. non-terminal symbols, the grammar, and the semantic actions.
\item Module \verb+Aut+ contains description of the automaton \item The module \verb+Aut+ contains the automaton
generated by \menhir, with a certificate that will be checked in generated by \menhir, together with a certificate that is checked by Coq
order to prove the soundness and completeness of the parser. while establishing the soundness and completeness of the parser.
\end{itemize} \end{itemize}
The type of terminals is a big inductive type, with a constructor for The type of the terminal symbols is an inductive type, with one constructor for
each terminal, but it does not contains the semantic values: we also each terminal symbol. but it does not contains the semantic values: we also
define the type \verb+token+, which is a dependant pair of a terminal define the type \verb+token+, which is a dependant pair of a terminal
and a semantic value of the corresponding type. Thus, we model the and a semantic value of the corresponding type. Thus, we model the
lexer by an object of type \verb+Stream.Stream token+. lexer by an object of type \verb+Stream.Stream token+.
......
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