Commit 48c2c888 authored by POTTIER Francois's avatar POTTIER Francois

Standard library: add `epsilon`, `rev`, `flatten`, `append`.

Add a link from the manual to `standard.mly` in the repository.
parent 7f47be85
......@@ -2,6 +2,9 @@
## 2018/10/05
* Standard library: add `epsilon`, `rev`, `flatten`, `append`.
Add a link from the manual to `standard.mly` in the repository.
* Update the manual to explain how to use `dune` and `menhir` together.
* Install `.cmxs` files for menhirLib and menhirSdk.
......
......@@ -159,15 +159,8 @@
* Produce well-chosen (predictable) names for anonymous rules?
* Add standard library support for specifying arithmetic-expression-levels?
Check connection with parsec (chainl1).
More generally, find inspiration in parsec combinators.
https://hackage.haskell.org/package/parsec-3.1.11/docs/Text-Parsec-Combinator.html
* Document left_flex_list and right_flex_list. Document WHEN they were added.
* standard library: define "%public %inline epsilon: {}", which allows using
"epsilon" as a marker for an empty right-hand side. Document WHEN added.
* Standard library: add more list forms (left-recursive lists,
flexible lists, etc.)
* Define [print_checkpoint].
Define a printer that shows the states in the stack.
......
......@@ -34,7 +34,7 @@
\newcommand{\dprec}{\kw{\%prec}\xspace}
\newcommand{\dequal}{\kw{=}\xspace}
\newcommand{\dquestion}{\kw{?}\xspace}
\newcommand{\dplus}{\kw{+}\xspace}
\newcommand{\dplus}{\raisebox{2pt}{\kw{\small +}}\xspace}
\newcommand{\dstar}{\kw{*}\xspace}
\newcommand{\dlpar}{\kw{(}\,\xspace}
\newcommand{\drpar}{\,\kw{)}\xspace}
......@@ -55,6 +55,7 @@
\newcommand{\repo}[2]{\href{https://gitlab.inria.fr/fpottier/menhir/blob/master/#1}{#2}}
\newcommand{\menhirlibconvert}{\repo{src/Convert.mli}{\texttt{MenhirLib.Convert}}\xspace}
\newcommand{\menhirlibincrementalengine}{\repo{src/IncrementalEngine.ml}{\texttt{MenhirLib.IncrementalEngine}}\xspace}
\newcommand{\standardmly}{\repo{src/standard.mly}{\texttt{standard.mly}}\xspace}
% Links to CompCert's repository.
......
......@@ -875,7 +875,7 @@ again in \sref{sec:library}.)
\nt{actual}\dstar & is syntactic sugar for & \nt{list}(\nt{actual})
\end{tabular}
\end{center}
\caption{Syntactic sugar for simulating regular expressions}
\caption{Syntactic sugar for simulating regular expressions, also known as EBNF}
\label{fig:sugar}
\end{figure}
%
......@@ -1039,10 +1039,12 @@ recognized.
\begin{tabular}{lp{51mm}l@{}l}
Name & Recognizes & Produces & Comment \\
\hline\\
\nt{epsilon} & $\epsilon$ & \basic{unit} & (inlined) \\
\\
\nt{endrule}(\nt{X}) & \nt{X} & $\alpha$, if \nt{X} : $\alpha$ & (inlined) \\
\nt{midrule}(\nt{X}) & \nt{X} & $\alpha$, if \nt{X} : $\alpha$ \\
\\
\nt{option}(\nt{X}) & $\epsilon$ \barre \nt{X} & $\alpha$ \basic{option}, if \nt{X} : $\alpha$ \\
\nt{option}(\nt{X}) & $\epsilon$ \barre \nt{X} & $\alpha$ \basic{option}, if \nt{X} : $\alpha$ & (also \nt{X}\dquestion) \\
\nt{ioption}(\nt{X}) & $\epsilon$ \barre \nt{X} & $\alpha$ \basic{option}, if \nt{X} : $\alpha$ & (inlined) \\
\nt{boption}(\nt{X}) & $\epsilon$ \barre \nt{X} & \basic{bool} \\
\nt{loption}(\nt{X}) & $\epsilon$ \barre \nt{X} & $\alpha$ \basic{list}, if \nt{X} : $\alpha$ \nt{list} \\
......@@ -1057,10 +1059,12 @@ Name & Recognizes & Produces & Comment \\
\\
\nt{list}(\nt{X})
& a possibly empty sequence of \nt{X}'s
& $\alpha$ \basic{list}, if \nt{X} : $\alpha$ \\
& $\alpha$ \basic{list}, if \nt{X} : $\alpha$
& (also \nt{X}\dstar) \\
\nt{nonempty\_list}(\nt{X})
& a nonempty sequence of \nt{X}'s
& $\alpha$ \basic{list}, if \nt{X} : $\alpha$ \\
& $\alpha$ \basic{list}, if \nt{X} : $\alpha$
& (also \nt{X}\dplus) \\
\nt{separated\_list}(\nt{sep}, \nt{X})
& a possibly empty sequence of \nt{X}'s separated with \nt{sep}'s
& $\alpha$ \basic{list}, if \nt{X} : $\alpha$ \\
......@@ -1068,9 +1072,26 @@ Name & Recognizes & Produces & Comment \\
& a nonempty sequence of \nt{X}'s \hspace{2mm} separated with \nt{sep}'s
& $\alpha$ \basic{list}, if \nt{X} : $\alpha$ \\
\\
\nt{rev}(\nt{X})
& \nt{X}
& $\alpha$ \basic{list}, if \nt{X} : $\alpha$ \basic{list}
& (inlined)
\\
\nt{flatten}(\nt{X})
& \nt{X}
& $\alpha$ \basic{list}, if \nt{X} : $\alpha$ \basic{list} \basic{list}
& (inlined)
\\
\nt{append}(\nt{X}, \nt{Y})
& \nt{X} \nt{Y}
& $\alpha$ \basic{list}, if \nt{X}, \nt{Y} : $\alpha$ \basic{list}
& (inlined)
\\
\end{tabular}
\end{center}
\caption{Summary of the standard library}
\caption{Summary of the standard library; see \standardmly for details}
\label{fig:standard}
\end{figure}
......@@ -1105,7 +1126,7 @@ causes \nt{plist}(\nt{X}) to recognize a list of \nt{X}'s, where the empty
list is represented by the empty string, and a non-empty list is delimited
with parentheses and comma-separated.
The standard library is stored in a file named \texttt{standard.mly}, which is
The standard library is stored in a file named \standardmly, which is
installed at the same time as \menhir. By default, \menhir attempts to find this
file in the directory where this file was installed. This can be overridden by
setting the environment variable
......
......@@ -146,6 +146,13 @@ x = X
(* ------------------------------------------------------------------------- *)
(* Sequences. *)
(* [epsilon] recognizes the empty word. It can be used instead of the
traditional /* empty */ comment. (20181005) *)
%public %inline epsilon:
/* empty */
{ () }
(* [pair(X, Y)] recognizes the sequence [X Y]. It produces a value of
type ['a * 'b] if [X] and [Y] produce values of type ['a] and ['b],
respectively. *)
......@@ -230,4 +237,28 @@ x = X
| x = X; separator; xs = separated_nonempty_list(separator, X)
{ x :: xs }
(* ------------------------------------------------------------------------- *)
(* List manipulation and transformation. *)
(* [rev(XS)] recognizes the same language as [XS], but reverses the resulting
OCaml list. (20181005) *)
%public %inline rev(XS):
xs = XS
{ List.rev xs }
(* [flatten(XSS)] recognizes the same language as [XSS], and flattens the
resulting OCaml list of lists. (20181005) *)
%public %inline flatten(XSS):
xss = XSS
{ List.flatten xss }
(* [append(XS, YS)] recognizes [XS YS], and appends (concatenates) the
resulting OCaml lists. (20181005) *)
%public %inline append(XS, YS):
xs = XS ys = YS
{ xs @ ys }
%%
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