Commit 496e9a8d authored by POTTIER Francois's avatar POTTIER Francois

In --coq mode, qualify references to MenhirLib modules.

New options --coq-lib-path and --coq-lib-no-path control this behavior.
parent be8cd23c
# Changes
## 2018/05/30
* In `--coq` mode, Menhir now produces references to `MenhirLib.Grammar`
instead of just `Grammar`, and similarly for all modules in Menhir's support
library.
* New command line option `--coq-lib-no-path` to suppress the above behavior
and retain the previous (now-deprecated) behavior, that is, produce
unqualified references the modules in Menhir's support library.
* New command line option `--coq-lib-path <path>` to indicate under what name
(or path) the support library has been installed. Its default value is
`MenhirLib`.
## 2018/05/23
* New commands `--infer-write-query`, `--infer-read-reply`, and
......
......@@ -160,6 +160,8 @@
\newcommand{\ostdlib}{\oo{stdlib}}
\newcommand{\oversion}{\oo{version}}
\newcommand{\ocoq}{\oo{coq}}
\newcommand{\ocoqlibpath}{\oo{coq-lib-path}}
\newcommand{\ocoqlibnopath}{\oo{coq-lib-no-path}}
\newcommand{\ocoqnocomplete}{\oo{coq-no-complete}}
\newcommand{\ocoqnoactions}{\oo{coq-no-actions}}
\newcommand{\olisterrors}{\oo{list-errors}}
......
......@@ -130,6 +130,15 @@ irredundant. For more information, see \sref{sec:errors:new}.
\docswitch{\ocoq} This switch causes \menhir to produce Coq code. See \sref{sec:coq}.
\docswitch{\ocoqlibpath \nt{path}} This switch allows specifying under what name (or path) the Coq support library
MenhirLib is known to Coq. When \menhir runs in \ocoq mode, the generated
parser contains references to several modules in this library. This path is
used to qualify these references. Its default value is \texttt{MenhirLib}.
\docswitch{\ocoqlibnopath} This switch indicates that references to the Coq library MenhirLib
should \emph{not} be qualified. This was the default behavior of \menhir prior to 2018/05/30.
This switch is provided for compatibility, but normally should not be used.
\docswitch{\ocoqnoactions} (Used in conjunction with \ocoq.) This switch
causes the semantic actions present in the \vy file to be ignored and
replaced with \verb+tt+, the unique inhabitant of Coq's \verb+unit+ type. This
......@@ -3518,11 +3527,19 @@ named \verb+Parser.unambiguous+.
% correspond bien à la fin du Stream.
The parsers produced by \menhir's Coq back-end must be linked with a Coq
library, which can be found in the CompCert tree~\cite{compcert,compcert-github}, in the
\compcertgithubfile{cparser/validator}
subdirectory. CompCert can be used as
library. This library can be installed via the command \verb+opam install coq-menhirlib+.%
%
\footnote{This assumes that you have installed \texttt{opam}, the OCaml package manager,
and that you have run the command \texttt{opam repo add coq-released
https://coq.inria.fr/opam/released}.}
%
The Coq sources of this library can be found at
\url{https://gitlab.inria.fr/fpottier/coq-menhirlib}.
The CompCert verified compiler~\cite{compcert,compcert-github} can be used as
an example if one wishes to use \menhir to generate a formally verified parser
as part of some other project.
as part of some other project. See in particular the directory
\compcertgithubfile{cparser}.
% fp: ce pourrait être bien de documenter les directives nécessaires pour
% extraire du code efficace. D'après Xavier ce morceau de extraction.v
......
......@@ -451,8 +451,15 @@ module Run (T: sig end) = struct
write_items f;
fprintf f "End Aut.\n\n"
let from_menhirlib f =
match Settings.coq_lib_path with
| None ->
()
| Some path ->
fprintf f "From %s " path
let write_theorems f =
fprintf f "Require Import Main.\n\n";
from_menhirlib f; fprintf f "Require Import Main.\n\n";
fprintf f "Module Parser := Main.Make Aut.\n";
......@@ -503,13 +510,13 @@ module Run (T: sig end) = struct
List.iter (fun s -> fprintf f "%s\n\n" s.Stretch.stretch_content)
Front.grammar.UnparameterizedSyntax.preludes;
fprintf f "Require Import List.\n";
fprintf f "Require Import Int31.\n";
fprintf f "Require Import Syntax.\n";
fprintf f "Require Import Tuples.\n";
fprintf f "Require Import Alphabet.\n";
fprintf f "Require Grammar.\n";
fprintf f "Require Automaton.\n\n";
fprintf f "From Coq.Lists Require Import List.\n";
fprintf f "From Coq.Numbers.Cyclic.Int31 Require Import Int31.\n";
fprintf f "From Coq.Program Require Import Syntax.\n";
from_menhirlib f; fprintf f "Require Import Tuples.\n";
from_menhirlib f; fprintf f "Require Import Alphabet.\n";
from_menhirlib f; fprintf f "Require Grammar.\n";
from_menhirlib f; fprintf f "Require Automaton.\n\n";
fprintf f "Unset Elimination Schemes.\n\n";
write_grammar f;
write_automaton f;
......
......@@ -287,6 +287,9 @@ let set_echo_errors filename =
let cmly =
ref false
let coq_lib_path =
ref (Some "MenhirLib")
let options = Arg.align [
"--base", Arg.Set_string base, "<basename> Specifies a base name for the output file(s)";
"--canonical", Arg.Unit (fun () -> construction_mode := ModeCanonical), " Construct a canonical Knuth LR(1) automaton";
......@@ -295,8 +298,10 @@ let options = Arg.align [
"--compare-errors", Arg.String add_compare_errors, "<filename> (used twice) Compare two .messages files";
"--compile-errors", Arg.String set_compile_errors, "<filename> Compile a .messages file to OCaml code";
"--coq", Arg.Set coq, " Generate a formally verified parser, in Coq";
"--coq-no-complete", Arg.Set coq_no_complete, " Do not generate a proof of completeness";
"--coq-lib-path", Arg.String (fun path -> coq_lib_path := Some path), "<path> How to qualify references to MenhirLib";
"--coq-lib-no-path", Arg.Unit (fun () -> coq_lib_path := None), " Do *not* qualify references to MenhirLib";
"--coq-no-actions", Arg.Set coq_no_actions, " Ignore semantic actions in the Coq output";
"--coq-no-complete", Arg.Set coq_no_complete, " Do not generate a proof of completeness";
"--depend", Arg.Unit enable_depend, " Invoke ocamldep and display dependencies";
"--dump", Arg.Set dump, " Write an .automaton file";
"--echo-errors", Arg.String set_echo_errors, "<filename> Echo the sentences in a .messages file";
......@@ -579,6 +584,9 @@ let echo_errors =
let cmly =
!cmly
let coq_lib_path =
!coq_lib_path
let infer =
!infer
......
......@@ -231,3 +231,9 @@ val echo_errors: string option
binary-format description of the grammar and automaton. *)
val cmly: bool
(* This name is used in --coq mode. It appears in the generated Coq file,
and indicates under what name (or path) the Coq library MenhirLib is
known. Its default value is [Some "MenhirLib"]. *)
val coq_lib_path: string option
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