diff options
Diffstat (limited to 'test/external/metalang99/spec')
| -rw-r--r-- | test/external/metalang99/spec/.gitignore | 276 | ||||
| -rw-r--r-- | test/external/metalang99/spec/references.bib | 17 | ||||
| -rw-r--r-- | test/external/metalang99/spec/spec.pdf | bin | 0 -> 201160 bytes | |||
| -rw-r--r-- | test/external/metalang99/spec/spec.tex | 289 |
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 Binary files differnew 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} |