add metalang99 testsuite (preprocessor stress testing)

4 files changed, 582 insertions, 0 deletions

diff --git a/test/external/metalang99/spec/.gitignore b/test/external/metalang99/spec/.gitignore
new file mode 100644
index 0000000..859f705
--- /dev/null
+++ b/test/external/metalang99/spec/.gitignore
@@ -0,0 +1,276 @@
+## Core latex/pdflatex auxiliary files:
+*.aux
+*.lof
+*.log
+*.lot
+*.fls
+*.out
+*.toc
+*.fmt
+*.fot
+*.cb
+*.cb2
+.*.lb
+
+## Intermediate documents:
+*.dvi
+*.xdv
+*-converted-to.*
+# these rules might exclude image files for figures etc.
+# *.ps
+# *.eps
+# *.pdf
+
+## Generated if empty string is given at "Please type another file name for output:"
+.pdf
+
+## Bibliography auxiliary files (bibtex/biblatex/biber):
+*.bbl
+*.bcf
+*.blg
+*-blx.aux
+*-blx.bib
+*.run.xml
+
+## Build tool auxiliary files:
+*.fdb_latexmk
+*.synctex
+*.synctex(busy)
+*.synctex.gz
+*.synctex.gz(busy)
+*.pdfsync
+
+## Build tool directories for auxiliary files
+# latexrun
+latex.out/
+
+## Auxiliary and intermediate files from other packages:
+# algorithms
+*.alg
+*.loa
+
+# achemso
+acs-*.bib
+
+# amsthm
+*.thm
+
+# beamer
+*.nav
+*.pre
+*.snm
+*.vrb
+
+# changes
+*.soc
+
+# comment
+*.cut
+
+# cprotect
+*.cpt
+
+# elsarticle (documentclass of Elsevier journals)
+*.spl
+
+# endnotes
+*.ent
+
+# fixme
+*.lox
+
+# feynmf/feynmp
+*.mf
+*.mp
+*.t[1-9]
+*.t[1-9][0-9]
+*.tfm
+
+#(r)(e)ledmac/(r)(e)ledpar
+*.end
+*.?end
+*.[1-9]
+*.[1-9][0-9]
+*.[1-9][0-9][0-9]
+*.[1-9]R
+*.[1-9][0-9]R
+*.[1-9][0-9][0-9]R
+*.eledsec[1-9]
+*.eledsec[1-9]R
+*.eledsec[1-9][0-9]
+*.eledsec[1-9][0-9]R
+*.eledsec[1-9][0-9][0-9]
+*.eledsec[1-9][0-9][0-9]R
+
+# glossaries
+*.acn
+*.acr
+*.glg
+*.glo
+*.gls
+*.glsdefs
+*.lzo
+*.lzs
+
+# uncomment this for glossaries-extra (will ignore makeindex's style files!)
+# *.ist
+
+# gnuplottex
+*-gnuplottex-*
+
+# gregoriotex
+*.gaux
+*.gtex
+
+# htlatex
+*.4ct
+*.4tc
+*.idv
+*.lg
+*.trc
+*.xref
+
+# hyperref
+*.brf
+
+# knitr
+*-concordance.tex
+# TODO Comment the next line if you want to keep your tikz graphics files
+*.tikz
+*-tikzDictionary
+
+# listings
+*.lol
+
+# luatexja-ruby
+*.ltjruby
+
+# makeidx
+*.idx
+*.ilg
+*.ind
+
+# minitoc
+*.maf
+*.mlf
+*.mlt
+*.mtc[0-9]*
+*.slf[0-9]*
+*.slt[0-9]*
+*.stc[0-9]*
+
+# minted
+_minted*
+*.pyg
+
+# morewrites
+*.mw
+
+# nomencl
+*.nlg
+*.nlo
+*.nls
+
+# pax
+*.pax
+
+# pdfpcnotes
+*.pdfpc
+
+# sagetex
+*.sagetex.sage
+*.sagetex.py
+*.sagetex.scmd
+
+# scrwfile
+*.wrt
+
+# sympy
+*.sout
+*.sympy
+sympy-plots-for-*.tex/
+
+# pdfcomment
+*.upa
+*.upb
+
+# pythontex
+*.pytxcode
+pythontex-files-*/
+
+# tcolorbox
+*.listing
+
+# thmtools
+*.loe
+
+# TikZ & PGF
+*.dpth
+*.md5
+*.auxlock
+
+# todonotes
+*.tdo
+
+# vhistory
+*.hst
+*.ver
+
+# easy-todo
+*.lod
+
+# xcolor
+*.xcp
+
+# xmpincl
+*.xmpi
+
+# xindy
+*.xdy
+
+# xypic precompiled matrices and outlines
+*.xyc
+*.xyd
+
+# endfloat
+*.ttt
+*.fff
+
+# Latexian
+TSWLatexianTemp*
+
+## Editors:
+# WinEdt
+*.bak
+*.sav
+
+# Texpad
+.texpadtmp
+
+# LyX
+*.lyx~
+
+# Kile
+*.backup
+
+# gummi
+.*.swp
+
+# KBibTeX
+*~[0-9]*
+
+# TeXnicCenter
+*.tps
+
+# auto folder when using emacs and auctex
+./auto/*
+*.el
+
+# expex forward references with \gathertags
+*-tags.tex
+
+# standalone packages
+*.sta
+
+# Makeindex log files
+*.lpz
diff --git a/test/external/metalang99/spec/references.bib b/test/external/metalang99/spec/references.bib
new file mode 100644
index 0000000..adcb68a
--- /dev/null
+++ b/test/external/metalang99/spec/references.bib
@@ -0,0 +1,17 @@
+@online{Metalang99,
+    author = "hirrolot",
+    title = "Full-blown preprocessor metaprogramming",
+    url = "https://github.com/hirrolot/metalang99",
+}
+
+@online{ApplicativeEvaluationStrategy,
+    author = "Wikipedia",
+    title = "Applicative order",
+    url = "https://en.wikipedia.org/wiki/Evaluation_strategy#Applicative_order",
+}
+
+@online{Bluepainting,
+    author = "",
+    title = "C99 draft, section 6.10.3.4, paragraph 2 -- Rescanning and further replacement",
+    url = "http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf",
+}
diff --git a/test/external/metalang99/spec/spec.pdf b/test/external/metalang99/spec/spec.pdf
new file mode 100644
index 0000000..de1a062
--- /dev/null
+++ b/test/external/metalang99/spec/spec.pdf
diff --git a/test/external/metalang99/spec/spec.tex b/test/external/metalang99/spec/spec.tex
new file mode 100644
index 0000000..99fb7e4
--- /dev/null
+++ b/test/external/metalang99/spec/spec.tex
@@ -0,0 +1,289 @@
+\documentclass[12pt]{article}
+
+\usepackage{hyperref}
+\usepackage{float}
+\usepackage{bussproofs}
+\usepackage{minted}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage[standard,thmmarks]{ntheorem}
+\usepackage{biblatex}
+\usepackage{csquotes}
+\usepackage{mathtools}
+\usepackage{tabularx}
+\usepackage[english]{babel}
+
+\theoremstyle{break}
+\newtheorem{notation}{Notation}
+
+\addbibresource{references.bib}
+
+\floatstyle{boxed}
+\restylefloat{figure}
+\allowdisplaybreaks
+
+\begin{document}
+
+\title{Metalang99 Specification (v1.13.5)}
+\date{\today}
+\author{\texttt{hirrolot} \\ e-mail: \href{mailto:hirrolot@gmail.com}{hirrolot@gmail.com}}
+\maketitle
+
+\begin{abstract}
+This paper formally describes the syntax and semantics of metaprograms written in Metalang99,
+a metalanguage aimed at full-blown C99 preprocessor metaprogramming. For the motivation and
+a user-friendly overview, please see the official repository \cite{Metalang99}.
+\end{abstract}
+
+\tableofcontents
+
+\newpage
+
+\section{EBNF Grammar}
+
+\begin{figure}[H]
+    \caption{Grammar rules}
+
+\begin{minted}{bnf}
+<eval> ::= "ML99_EVAL(" <term-seq> ")" ;
+
+<term-seq> ::= <term> { "," <term> }* ;
+
+<term> ::=
+      "ML99_call(" <op> "," <term-seq> ")"
+    | "ML99_callUneval(" <ident> "," <pp-token-list> ")"
+    | "ML99_abort(" <term-seq> ")"
+    | "ML99_fatal(" <ident> "," <pp-token-list> ")"
+    | "v(" <pp-token-list> ")" ;
+
+<op> ::= <ident> | <term> ;
+\end{minted}
+
+\end{figure}
+
+Notes:
+
+\begin{itemize}
+    \item \texttt{<pp-token-list>} stands for a list of preprocessor tokens (e.g., \texttt{a 123, hello!}).
+    \item The grammar above describes metaprograms already expanded by the preprocessor,
+    except for \texttt{ML99\_EVAL}, \texttt{ML99\_call}, \texttt{ML99\_callUneval}, \\
+    \texttt{ML99\_abort}, \texttt{ML99\_fatal}, and \texttt{v}.
+    \item \texttt{ML99\_call} accepts \texttt{op} either as an identifier or as a term that
+    reduces to an identifier.
+    \item \texttt{ML99\_callUneval} accepts an operation strictly as an identifier.
+\end{itemize}
+
+The \texttt{ML99\_call} syntax hurts IDE support (no parameters documentation highlighting) and is also
+less natural. The workaround is to define a wrapper around an implementation macro like this:
+
+\begin{minted}{c}
+/// The documentation string.
+#define FOO(a, b, c) ML99_call(FOO, a, b, c)
+#define FOO_IMPL(a, b, c) // The implementation.
+\end{minted}
+
+Then \texttt{FOO} can be conveniently called as \texttt{FOO(v(1), v(2), v(3))}.
+
+\section{Notations}
+
+\begin{notation}[Sequence]
+    \begin{itemize}
+        \item $\overline{x} \coloneqq x_1 \ldots x_n$. Examples:
+        \begin{itemize}
+            \item Metalang99 terms: \texttt{v(abc), ML99\_call(FOO, v(123)), v(u 8 9)}
+            \item Preprocessor tokens: \texttt{abc 13 "hello" + -}
+        \end{itemize}
+        \item $()$ denotes the empty sequence.
+        \item Appending to a sequence:
+        \begin{itemize}
+            \item Appending an element: $S \ y \coloneqq x_1 \ldots x_n \ y$, where $S = x_1 \ldots x_n$
+            \item Appending a sequence: $S_1 \ S_2 \coloneqq x_1 \ldots x_n \ y_1 \ldots y_m$, where $S_1 = x_1 \ldots x_n$
+            and $S_2 = y_1 \ldots y_m$
+        \end{itemize}
+    \end{itemize}
+\end{notation}
+
+\begin{notation}[Reduction step]
+    $\to$ denotes a single step of reduction (computation, evaluation).
+\end{notation}
+
+\begin{notation}[Metavariables]
+    \ \\
+    \begin{tabular}{|c|c|}
+        \hline
+        \texttt{tok} & preprocessor token \\
+        \texttt{ident} & preprocessor identifier \\
+        \texttt{t} & Metalang99 term \\
+        \texttt{a} & Metalang99 term used as an argument \\
+        \hline
+    \end{tabular}
+\end{notation}
+
+\section{Reduction Semantics}
+
+We define a reduction semantics for Metalang99 \ref{ReductionSemantics}. The abstract
+machine executes configurations of the form $\langle K; F; A; C \rangle$:
+
+\begin{itemize}
+    \item $K$ is a continuation of the form $\langle K; F; A; C \rangle$, where
+    $C$ includes the $?$ sign denoting a result passed into the continuation.
+    For example, let $K$ be $\langle K'; (1, 2, 3); v(x), \ ? \rangle$,
+    then $K(v(y))$ is $\langle K'; (1, 2, 3); v(x), v(y) \rangle$. A special
+    continuation $halt$ terminates the abstract machine and substitutes itself
+    with a provided result. For example, when the abstract machine encounters
+    $halt(1 + 2)$, it will just stop and paste $1 + 2$.
+
+    \item $F$ is a left folder of the form $(acc, \overline{tok}) \to acc$. It is used
+    to flexibly append a newly evaluated term to an accumulator without extra reduction
+    steps. There are the only two folders:
+    \begin{itemize}
+        \item $fspace(acc, \overline{tok}) \coloneqq acc \ \overline{tok}$
+        \item $fcomma(acc, \overline{tok}) \coloneqq if (acc \ is \ ()) \ then \ \overline{tok} \ else \ acc \ "," \ \overline{tok}$
+    \end{itemize}
+
+    \item $A$ (accumulator) is a sequence of already computed results.
+
+    \item $C$ (control) is a sequence of terms upon which the abstract
+    machine is operating right now.
+\end{itemize}
+
+\begin{figure}
+    \caption{Reduction Semantics}
+
+    \begin{align*}
+        (v): & \ \langle K; F; A; \texttt{v}(\overline{tok}), \overline{t} \rangle \to
+            \langle K; F; F(A, \overline{tok}); \overline{t} \rangle \\
+        (op): & \ \langle K; F; A; \texttt{ML99\_call}(t, \overline{a}), \overline{t'} \rangle \to \langle \\
+            & \ \ \ \ \langle K; F; A; \texttt{ML99\_call}(?), \overline{t'} \rangle; \\
+            & \ \ \ \ fcomma; \\
+            & \ \ \ \ (); \\
+            & \ \ \ \ t, \overline{a} \rangle \\
+        (args): & \ \langle K; F; A; \texttt{ML99\_call}(ident, \overline{a}), \overline{t} \rangle \to \langle \\
+            & \ \ \ \ \langle \langle K; F; F(A, ?); \overline{t} \rangle; fspace; (); ident\texttt{\_IMPL}(?) \rangle; \\
+            & \ \ \ \ fcomma; \\
+            & \ \ \ \ (); \\
+            & \ \ \ \ \overline{a} \rangle \\
+        (callUneval): & \ \langle K; F; A; \texttt{ML99\_callUneval}(ident, \overline{tok}), \overline{t} \rangle \to \langle \\
+            & \ \ \ \ \langle K; F; F(A, ?); \overline{t} \rangle; \\
+            & \ \ \ \ fspace; \\
+            & \ \ \ \ (); \\
+            & \ \ \ \ ident\texttt{\_IMPL}(\overline{tok}) \rangle \\
+        (abort): & \ \langle K; F; A; \texttt{ML99\_abort}(\overline{t}), \overline{t'} \rangle \to \langle halt; fspace; (); \overline{t} \rangle \\
+        (fatal): & \ \langle K; F; A; \texttt{ML99\_fatal}(ident, \overline{tok}), \overline{t} \rangle \to halt(\ldots) \\
+        (end): & \ \langle K; F; A; () \rangle \to K(A) \\
+        (start): & \ \texttt{ML99\_call}(\overline{t}) \to \langle halt; fspace; (); \overline{t} \rangle
+    \end{align*}
+    \label{ReductionSemantics}
+\end{figure}
+
+Notes:
+
+\begin{itemize}
+    \item Metalang99 follows applicative evaluation strategy \cite{ApplicativeEvaluationStrategy}.
+
+    \item $(args)$ Metalang99 generates a usual C-style macro invocation with
+    fully evaluated arguments, which will be then expanded by the preprocessor, resulting
+    in yet another concrete sequence of Metalang99 terms to be evaluated by the computational
+    rules.
+    \item $(args)$ Metalang99 appends \texttt{\_IMPL} to every macro identifier called using
+    \texttt{ML99\_call} -- it makes easier to follow the convention that all implementations
+    of metafunctions must have the postfix \texttt{\_IMPL}.
+    \item $(callUneval)$ \texttt{ML99\_callUneval} is used when an operation and all
+    arguments are already evaluated. It is semantically the same as \\ \texttt{ML99\_call(ident, v(...))}
+    but performs one less reduction steps to benefit in performance.
+    \item $(fatal)$ The ellipsis means that an implementation is free to provide
+    diagnostics in any format.
+    \item $(fatal)$ interprets its variadic arguments without preprocessor expansion -- i.e.,
+    they are pasted as-is. This is intended because otherwise identifiers located in an
+    error message may stand for other macros that will be unintentionally expanded.
+    \item The number of reduction steps is finite and may vary from version to version. If
+    the limit is exceeded, Metalang99 will not be able to perform reduction of a given
+    metaprogram anymore.
+\end{itemize}
+
+\subsection{Examples}
+
+Take the following code:
+
+\begin{minted}{c}
+#define X_IMPL(op)        ML99_call(op, v(123))
+#define CALL_X_IMPL(_123) ML99_call(X, v(ID))
+#define ID_IMPL(x)        v(x)
+\end{minted}
+
+See how \texttt{ML99\_call(X, v(CALL\_X))} is evaluated:
+
+\begin{example}[Evaluation of terms]
+\begin{align*}
+    \texttt{ML99\_EVAL}(\texttt{ML99\_call}(X, \texttt{v}(\texttt{CALL\_X}))) & \ \underrightarrow{(start)} \\
+    \langle halt; fspace; (); \texttt{ML99\_call}(X, \texttt{v}(\texttt{CALL\_X})) \rangle & \ \underrightarrow{(args)} \\
+    \langle \langle halt; fspace; (); \texttt{X}(?) \rangle; fcomma; (); \texttt{v}(\texttt{CALL\_X}) \rangle & \ \underrightarrow{(v)} \\
+    \langle \langle halt; fspace; (); \texttt{X}(?) \rangle; fcomma; \texttt{CALL\_X}; () \rangle & \ \underrightarrow{(end)} \\
+    \langle halt; fspace; (); \texttt{ML99\_call}(\texttt{CALL\_X}, \texttt{v}(123)) \rangle & \ \underrightarrow{(args)} \\
+    \langle \langle halt; fspace; (); \texttt{CALL\_X}(?) \rangle; fcomma; (); \texttt{v}(123) \rangle & \ \underrightarrow{(v)} \\
+    \langle \langle halt; fspace; (); \texttt{CALL\_X}(?) \rangle; fcomma; 123; () \rangle & \ \underrightarrow{(end)} \\
+    \langle halt; fspace; (); \texttt{ML99\_call}(X, \texttt{v}(\texttt{ID})) \rangle & \ \underrightarrow{(args)} \\
+    \langle \langle halt; fspace; (); \texttt{X}(?) \rangle; fcomma; (); \texttt{v}(\texttt{ID}) \rangle & \ \underrightarrow{(v)} \\
+    \langle \langle halt; fspace; (); \texttt{X}(?) \rangle; fcomma; \texttt{ID}; \rangle & \ \underrightarrow{(end)} \\
+    \langle halt; fspace; (); \texttt{ML99\_call}(\texttt{ID}, \texttt{v}(123)) \rangle & \ \underrightarrow{(args)} \\
+    \langle \langle halt; fspace; (); \texttt{ID}(?) \rangle; fcomma; (); \texttt{v}(123) \rangle & \ \underrightarrow{(v)} \\
+    \langle \langle halt; fspace; (); \texttt{ID}(?) \rangle; fcomma; 123; () \rangle & \ \underrightarrow{(end)} \\
+    \langle halt; fspace; (); \texttt{v}(123) \rangle & \ \underrightarrow{(v)} \\
+    \langle halt; fspace; 123; () \rangle & \ \underrightarrow{(end)} \\
+    halt(123) &
+\end{align*}
+\end{example}
+
+The analogous version written in ordinary C looks like this:
+
+\begin{minted}{c}
+#define X(op)        op(123)
+#define CALL_X(_123) X(ID)
+#define ID(x)        x
+\end{minted}
+
+However, unlike the Metalang99 version above, \texttt{X(CALL\_X)} gets blocked \cite{Bluepainting} due to the
+second call to \texttt{X}. The trick is that Metalang99 performs evaluation step-by-step,
+unlike the preprocessor:
+
+\begin{itemize}
+    \item The Metalang99 version: \texttt{X(CALL\_X)} expands to \texttt{ML99\_call(\\ CALL\_X, v(123))}.
+    This expansion does not contain \texttt{X}, and therefore \texttt{X} is \textbf{not}
+    blocked by the preprocessor.
+
+    \item The ordinary version: \texttt{X(CALL\_X)} expands to \texttt{X(ID)}. This expansion
+    does contains \texttt{X}, and therefore \texttt{X} is blocked by the preprocessor.
+\end{itemize}
+
+\section{Properties}
+
+\subsection{Progress}
+
+\begin{proposition}[Progress]
+Either $\langle K; F; A; \overline{t} \rangle \to \langle K; F; A; \overline{t'} \rangle$ or \\
+$\langle K; F; A; \overline{t} \rangle \to halt(\overline{x})$.
+\end{proposition}
+
+\begin{proof}
+By inspection of \ref{ReductionSemantics}.
+\end{proof}
+
+\section{Caveats}
+
+\begin{itemize}
+\item Consider this scenario:
+    \begin{itemize}
+        \item You call \texttt{FOO(1, 2, 3)}
+        \item It gets expanded by the preprocessor (not by Metalang99)
+        \item Its expansion contains \texttt{FOO}
+    \end{itemize}
+Then \texttt{FOO} gets blocked \cite{Bluepainting} by the preprocessor, i.e. Metalang99 cannot handle ordinary
+macro recursion; you must use \texttt{ML99\_call} to be sure that recursive calls
+will behave as expected. I therefore recommend to use only primitive C-style macros, e.g.
+for performance reasons or because of you cannot express them in terms of Metalang99.
+\end{itemize}
+
+\emergencystretch=1em
+\printbibliography
+
+\end{document}