Preproc is the preprocessor of Core C++, a language of its own that runs before the lexer of Definition 1.1.3. It reads a file as a sequence of lines and never lexes or parses Core C++, so the two languages share no surface. Every Preproc program is also a valid input of the preprocessor of g++.

The terminals of its grammar are whole lines. \textit{Text} stands for any text line, and \textit{NL} ends a directive line.

\begin{array}{lcl} \textit{File} & ::= & \textit{Group} \\ \textit{Group} & ::= & \big(\ \textit{Line}\ \mid\ \textit{Cond}\ \big)^{*} \\ \textit{Line} & ::= & \texttt{\#include}\ \texttt{<}\ \textit{Header}\ \texttt{>}\ \textit{NL}\ \mid\ \texttt{\#define}\ \textit{FlagId}\ \textit{NL}\ \mid\ \textit{Text} \\ \textit{Cond} & ::= & \textit{Test}\ \textit{FlagId}\ \textit{NL}\ \textit{Group}\ \big(\ \texttt{\#else}\ \textit{NL}\ \textit{Group}\ \big)^{?}\ \texttt{\#endif}\ \textit{NL} \\ \textit{Test} & ::= & \texttt{\#ifdef}\ \mid\ \texttt{\#ifndef} \end{array}

Preproc supports conditional compilation on flags, the inclusion of a subset of the standard library and of the STL, and the function assert of <cassert>. A flag has no value and never reaches the code. The design is preproc/ccpp-preproc.md.

Every line satisfies five rules, including the lines of a branch that is not selected and the lines of every header. The C++ preprocessor splices lines and removes comments before it recognises directives (N4659 §5.2, phases 2 to 4), and the rules keep the line structure the same for both.

• A directive line is exactly one of the forms of the grammar.

• A text line does not start with # or with the digraph %:, possibly after blanks, since C++ reads %: as # (N4659 §5.5, Table 1).

• No line contains a backslash, /*, a single quote or a double quote.

• A flag has the prefix CCPP_, a nonempty rest of letters, digits and _, and no __, which C++ reserves (N4659 §5.10).

• No word of a text line starts with CCPP_, so a flag never occurs in the code. A word is a maximal run of letters, digits and _.

The flag environment \varphi is a finite set of flags, initially the flags given as -D CCPP_X=. The judgement \varphi \vdash G \Rightarrow t, \varphi' gives the output lines t of a group and the environment after it. H(h) is the contents of the Core C++ header h.

\dfrac{}{\varphi \vdash \texttt{\#define}\ F \Rightarrow \varepsilon, \varphi \cup \{F\}}\;\textsf{(P-Define)}

\dfrac{\varphi \vdash H(h) \Rightarrow t, \varphi'}{\varphi \vdash \texttt{\#include}\ \texttt{<}h\texttt{>} \Rightarrow t, \varphi'}\;\textsf{(P-Include)}

\dfrac{F \in \varphi \qquad \varphi \vdash G_1 \Rightarrow t, \varphi'}{\varphi \vdash \texttt{\#ifdef}\ F\ G_1\ \texttt{\#else}\ G_2\ \texttt{\#endif} \Rightarrow t, \varphi'}\;\textsf{(P-IfdefT)}

\dfrac{F \notin \varphi \qquad \varphi \vdash G_2 \Rightarrow t, \varphi'}{\varphi \vdash \texttt{\#ifdef}\ F\ G_1\ \texttt{\#else}\ G_2\ \texttt{\#endif} \Rightarrow t, \varphi'}\;\textsf{(P-IfdefF)}

The directive #ifndef swaps the premises F \in \varphi and F \notin \varphi, and a missing #else stands for an empty G_2. A text line gives itself. An #include gives the output of the header, and Preproc marks those lines as lines of a header. Every other directive line and every line of a branch that is not selected gives an empty line, so a source file without #include keeps its line numbers.

The functions run, runItem and Item.size are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.

The headers of Core C++ are Core C++ code for the Core C++ compiler, in preproc/include, and g++ uses its own headers. Each is a Preproc file whose guard makes it idempotent, as a C++ header is (N4659 §20.5.2.2, paragraph 2).

The headers <vector> and <functional> declare the class templates std::vector and std::function, and <cassert> declares the function assert. Chapter Definition 8.1.1 gives their semantics.

An #include inside a function body puts declarations inside a block, which the grammar of Definition 1.2.1 rejects. Inclusion fails beyond a depth of 64, which bounds a cycle of headers without a guard.