Commit db212c57 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Saved and published documentation for release 20201122.

parent c1d511b8
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -58,13 +58,13 @@ font-size: 1rem;
}
</style>
<title>Menhir Reference Manual
(version 20200624)
(version 20201122)
</title>
</head>
<body >
<!--HEVEA command line is: hevea -fix manual.tex -->
<!--CUT STYLE article--><!--CUT DEF section 1 --><table class="title"><tr><td style="padding:1ex"><h1 class="titlemain">Menhir Reference Manual<br>
(version 20200624)</h1><h3 class="titlerest">François Pottier and Yann Régis-Gianas<br>
(version 20201122)</h1><h3 class="titlerest">François Pottier and Yann Régis-Gianas<br>
INRIA<br>
<span style="font-family:monospace">{Francois.Pottier, Yann.Regis-Gianas}@inria.fr</span></h3></td></tr>
</table><!--TOC section id="sec1" Contents-->
......@@ -227,8 +227,15 @@ disables the generation of the proof of completeness of the parser
possible only if the grammar has no conflict (not even a benign one, in the
sense of §<a href="#sec%3Aconflicts%3Abenign">6.1</a>). This can be desirable also because, for
a complex grammar, completeness may require a heavy certificate and its
validation by Coq may take time.</p><p><span style="font-family:monospace">--depend</span>.  See §<a href="#sec%3Abuild">14</a>.</p><p><span style="font-family:monospace">--dump</span>.  This switch causes a description of the automaton
to be written to the file <span style="font-style:italic">basename</span><span style="font-family:monospace">.automaton</span>.</p><p><span style="font-family:monospace">--echo-errors</span> <span style="font-style:italic">filename</span>.  This switch causes Menhir to
validation by Coq may take time.</p><p><span style="font-family:monospace">--depend</span>.  See §<a href="#sec%3Abuild">14</a>.</p><p><span style="font-family:monospace">--dump</span>.  This switch causes a description of the automaton to be
written to the file <span style="font-style:italic">basename</span><span style="font-family:monospace">.automaton</span>. This description is written after
benign conflicts have been resolved, before severe conflicts are resolved
<a href="#sec%3Aconflicts">6</a>), and before extra reductions are introduced
<a href="#sec%3Aonerrorreduce">4.1.8</a>).</p><p><span style="font-family:monospace">--dump-resolved</span>.  This command line switch causes a description of
the automaton to be written to the file <span style="font-style:italic">basename</span><span style="font-family:monospace">.automaton.resolved</span>. This
description is written after all conflicts have been resolved
<a href="#sec%3Aconflicts">6</a>) and after extra reductions have been introduced
<a href="#sec%3Aonerrorreduce">4.1.8</a>).</p><p><span style="font-family:monospace">--echo-errors</span> <span style="font-style:italic">filename</span>.  This switch causes Menhir to
read the <span style="font-family:monospace">.messages</span> file <span style="font-style:italic">filename</span> and to produce on the standard output
channel just the input sentences. (That is, all messages, blank lines, and
comments are filtered out.) For more information, see §<a href="#sec%3Aerrors%3Anew">11</a>.</p><p><span style="font-family:monospace">--explain</span>.  This switch causes conflict explanations to be
......@@ -1393,7 +1400,7 @@ token, it makes sense for it to <em>shift</em> that token.</p>
<div class="caption"><table style="border-spacing:6px;border-collapse:separate;" class="cellpading0"><tr><td style="vertical-align:top;text-align:left;" >Figure 8: A textual version of the tree in Figure <a href="#fig%3Areducing%3Atree">7</a></td></tr>
</table></div>
<a id="fig:reducing:text"></a>
<div class="center"><hr style="width:80%;height:2"></div></blockquote><p>In our example, the proof that shifting is possible is the derivation tree
<div class="center"><hr style="width:80%;height:2"></div></blockquote><p>In our example, the proof that reducing is possible is the derivation tree
shown in Figures <a href="#fig%3Areducing%3Atree">7</a> and <a href="#fig%3Areducing%3Atext">8</a>. Again,
the sentential form found at the fringe of the tree begins with the conflict
string, followed with the conflict token.</p><p>Again, in Figure <a href="#fig%3Areducing%3Atext">8</a>, the end of the conflict string is
......@@ -1935,7 +1942,7 @@ follows:
with type token = token
</pre><p>
The signature <code>INCREMENTAL_ENGINE</code>, defined in the module
<a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/src/IncrementalEngine.ml"><span style="font-family:monospace">MenhirLib.IncrementalEngine</span></a>, contains many types and functions,
<a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/lib/IncrementalEngine.ml"><span style="font-family:monospace">MenhirLib.IncrementalEngine</span></a>, contains many types and functions,
which are described in the rest of this section
<a href="#sec%3Aincremental%3Adriving">9.2.2</a>) and in the following sections
<a href="#sec%3Aincremental%3Ainspecting">9.2.3</a>, §<a href="#sec%3Aincremental%3Aupdating">9.2.4</a>).</p><p>Please keep in mind that, from the outside, these types and functions should be referred
......@@ -2866,9 +2873,9 @@ joining multiple <span style="font-family:monospace">.mly</span> files, if neces
</li><li class="li-itemize">performing OCaml type inference, if the <span style="font-family:monospace">--infer</span> switch is used;
</li><li class="li-itemize">inlining away nonterminal symbols that are decorated with <span style="font-family:sans-serif"><span style="font-weight:bold">%inline</span></span>.
</li></ul><p>The library <span style="font-family:monospace">MenhirSdk</span> offers an API for reading a <span style="font-family:monospace">.cmly</span> file.
The functor <a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/src/cmly_read.mli"><span style="font-family:monospace">MenhirSdk.Cmly_read.Read</span></a>
The functor <a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/sdk/cmly_read.mli"><span style="font-family:monospace">MenhirSdk.Cmly_read.Read</span></a>
reads such a file and produces a module whose signature is
<a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/src/cmly_api.ml"><span style="font-family:monospace">MenhirSdk.Cmly_api.GRAMMAR</span></a>.
<a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/sdk/cmly_api.ml"><span style="font-family:monospace">MenhirSdk.Cmly_api.GRAMMAR</span></a>.
This API is not explained in this document; for details,
the reader is expected to follow the above links.</p>
<!--TOC subsection id="sec81" Attributes-->
......@@ -2986,7 +2993,7 @@ invokes the OCaml compiler, under the form <code>ocamlc -i</code>, so as to
type-check this file and infer the types of the semantic actions. Menhir then
reads this information and produces real <span style="font-family:monospace">.ml</span> and <span style="font-family:monospace">.mli</span> files.</p><p><span style="font-family:monospace">--ocamlc</span> <span style="font-style:italic">command</span>.  This switch controls how <span style="font-family:monospace">ocamlc</span> is invoked.
It allows setting both the name of the executable and the command line options
that are passed to it.</p><p>One difficulty with the this approach is that the OCaml compiler usually
that are passed to it.</p><p>One difficulty with this approach is that the OCaml compiler usually
needs to consult a few <span style="font-family:monospace">.cm[iox]</span> files. Indeed, if the <span style="font-family:monospace">.mly</span> file
contains a reference to an external OCaml module, say <span style="font-family:monospace">A</span>, then the
OCaml compiler typically needs to read one or more files named
......@@ -3106,7 +3113,7 @@ scientific) benchmark suggests that the parsers produced by <span style="font-fa
<span style="font-family:monospace">menhir</span> are between 2 and 5 times faster. This benchmark excludes the
time spent in the lexer and in the semantic actions.</p><p><br>
<span style="font-weight:bold">How do I write </span><span style="font-weight:bold"><span style="font-family:monospace">Makefile</span></span><span style="font-weight:bold"> rules for Menhir?</span>
This can a bit tricky. If you must do this, see §<a href="#sec%3Abuild">14</a>.
This can be a bit tricky. If you must do this, see §<a href="#sec%3Abuild">14</a>.
It is recommended instead to use a build system
with built-in support for Menhir, such as <a href="#dune"><span style="font-family:monospace">dune</span></a> (preferred)
or <span style="font-family:monospace">ocamlbuild</span>.</p><p><br>
......@@ -3158,6 +3165,19 @@ For more details, see
https://dune.readthedocs.io/en/stable/dune-files.html#menhir"><span style="font-family:monospace">dune</span>’s documentation</a>.
To deal with <span style="font-family:monospace">.messages</span> files (§<a href="#sec%3Aerrors%3Anew">11</a>),
please use and adapt the rules found in the file <a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/src/stage2/dune"><span style="font-family:monospace">src/stage2/dune</span></a>.</p><p><br>
<span style="font-weight:bold">My </span><span style="font-weight:bold"><span style="font-family:monospace">.mly</span></span><span style="font-weight:bold"> file begins with a module alias declaration </span><span style="font-weight:bold"><span style="font-family:monospace">module F
= Foo</span></span><span style="font-weight:bold">. Because of this, the </span><span style="font-weight:bold"><span style="font-family:monospace">.mli</span></span><span style="font-weight:bold"> file generated by Menhir contains
references to </span><span style="font-weight:bold"><span style="font-family:monospace">F</span></span><span style="font-weight:bold"> instead of </span><span style="font-weight:bold"><span style="font-family:monospace">Foo</span></span><span style="font-weight:bold">. This does not make sense!</span>
Beginning with Menhir 20200525, Menhir prefers to use the types inferred by
the OCaml compiler over the types provided by the user in <span style="font-family:sans-serif"><span style="font-weight:bold">%type</span></span> declarations. (This may sound strange, but these types can differ in some
situations that involve polymorphic variants. Using the inferred type is
required for type soundness.)
In the presence of a module alias declaration such as <span style="font-family:monospace">module F =
Foo</span>, OCaml can infer types that begin with <span style="font-family:monospace">F.</span> instead of
<span style="font-family:monospace">Foo.</span>, and Menhir currently does not detect that <span style="font-family:monospace">F</span> is a local
name.
The suggested fix is to avoid placing module alias declarations in <span style="font-family:monospace">.mly</span> files.
</p><p><br>
<span style="font-weight:bold">Menhir reports </span><span style="font-weight:bold"><em>more</em></span><span style="font-weight:bold"> shift/reduce conflicts than
</span><span style="font-weight:bold"><span style="font-family:monospace">ocamlyacc</span></span><span style="font-weight:bold">! How come?</span> <span style="font-family:monospace">ocamlyacc</span> sometimes merges two states
of the automaton that Menhir considers distinct. This happens
......@@ -3171,8 +3191,8 @@ buffers?</span> Like <span style="font-family:monospace">ocamlyacc</span>, Menhi
possible to convert them, after the fact, to a simpler, revised API. In the
revised API, there are no lexing buffers, and a lexer is just a function from
unit to tokens. Converters are provided by the library module
<a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/src/Convert.mli"><span style="font-family:monospace">MenhirLib.Convert</span></a>. This can be useful, for instance, for users of
<span style="font-family:monospace">ulex</span>, the Unicode lexer generator. Also, please note that Menhir’s
<a href="https://gitlab.inria.fr/fpottier/menhir/blob/master/lib/Convert.mli"><span style="font-family:monospace">MenhirLib.Convert</span></a>. This can be useful, for instance, for users of
<span style="font-family:monospace">sedlex</span>, the Unicode-friendly lexer generator. Also, please note that Menhir’s
incremental API (§<a href="#sec%3Aincremental">9.2</a>) does not mention the type
<code>Lexing.lexbuf</code>. In this API, the parser expects to be supplied with
triples of a token and start/end positions of type <code>Lexing.position</code>.</p><p><br>
......
No preview for this file type
www/doc/manual001.png

4.33 KB | W: | H:

www/doc/manual001.png

4.21 KB | W: | H:

www/doc/manual001.png
www/doc/manual001.png
www/doc/manual001.png
www/doc/manual001.png
  • 2-up
  • Swipe
  • Onion skin
www/doc/manual002.png

4.14 KB | W: | H:

www/doc/manual002.png

4.03 KB | W: | H:

www/doc/manual002.png
www/doc/manual002.png
www/doc/manual002.png
www/doc/manual002.png
  • 2-up
  • Swipe
  • Onion skin
www/doc/manual003.png

5.14 KB | W: | H:

www/doc/manual003.png

5.02 KB | W: | H:

www/doc/manual003.png
www/doc/manual003.png
www/doc/manual003.png
www/doc/manual003.png
  • 2-up
  • Swipe
  • Onion skin
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