The abstract syntax is the tree form of the grammar of Definition 1.2.1, with one inductive type or structure per class of nonterminals. It has no parentheses and no precedence, because the tree fixes the structure. The table below gives the alternatives of every constructor of Syntax.lean, in the order of the file, with the constructor in the right column.

The type Ty has the basic types int, bool and void, class types, pointer types, the types of the library such as std::vector<int>, function types, and \mathsf{nullptr\_t}, the internal type of nullptr.

The type UnOp has ! and unary -, and the type BinOp has the arithmetic, the comparison and the logical operators.

The type Expr has literals and variables, operators and the conditional, and three calls, of a named function, of a method and of a function value. It has the two forms of new, this, field access through . and ->, dereference and indexing, and the lambda.

The last two constructors, locOf and intrinsic, are forms no program writes, and the function Typing.annotate of the type checker inserts both. The form locOf e is the location of e as a value, on the return of a member that returns a reference. The form intrinsic L u args is a use u of the entity L of the library.

The type Cmd has the block, if, while, for and return, the declarations with a type, with a reference and with auto, the assignment, the expression statement and delete.

A Param may be by reference. A Fun has a return type, a name, parameters and a body. A Vis is public or private.

A member is a Field, a Method, a Ctor or a Dtor. A method also records whether it is virtual, whether it overrides and whether it returns a reference, and a destructor records whether it is virtual. A ClassDecl has a qualified name, an optional base, fields and methods with their visibility, at most one constructor and at most one destructor.

A Decl is a class, a function, a class template, or a class template or a function of the library declared without a body. A Program is a list of declarations.

\begin{array}{lcll} \textit{Ty} & ::= & \mathtt{int} \mid \mathtt{bool} \mid \mathtt{void} & \textsf{Ty.int, bool, void} \\ & \mid & C \mid \textit{Ty}\mathtt{*} & \textsf{cls, ptr} \\ & \mid & \mathtt{std{:}{:}}L\langle\textit{Ty}_1, \ldots, \textit{Ty}_k\rangle \mid \textit{Ty}(\textit{Ty}_1, \ldots, \textit{Ty}_k) & \textsf{lib, fn} \\ & \mid & \mathsf{nullptr\_t} & \textsf{nullT} \\ \textit{UnOp} & ::= & \mathtt{!} \mid \mathtt{-} & \textsf{UnOp.not, neg} \\ \textit{BinOp} & ::= & \mathtt{+} \mid \mathtt{-} \mid \mathtt{*} \mid \mathtt{/} \mid \mathtt{\%} & \textsf{BinOp.add} \ldots \textsf{mod} \\ & \mid & \mathtt{==} \mid \mathtt{!=} \mid \mathtt{<} \mid \mathtt{<=} \mid \mathtt{>} \mid \mathtt{>=} & \textsf{eq} \ldots \textsf{ge} \\ & \mid & \mathtt{\&\&} \mid \mathtt{||} & \textsf{and, or} \\ \textit{Param} & ::= & \textit{Ty}\ x \mid \textit{Ty}\mathtt{\&}\ x & \textsf{Param} \\ \textit{Expr} & ::= & n \mid b & \textsf{Expr.intLit, boolLit} \\ & \mid & \mathtt{nullptr} \mid x & \textsf{nullptr, var} \\ & \mid & \textit{UnOp}\, \textit{Expr} \mid \textit{Expr}_1 \textit{BinOp} \textit{Expr}_2 & \textsf{unop, binop} \\ & \mid & \textit{Expr}_1\ \mathtt{?}\ \textit{Expr}_2\ \mathtt{:}\ \textit{Expr}_3 & \textsf{cond} \\ & \mid & f(\textit{Expr}_1, \ldots, \textit{Expr}_k) & \textsf{call} \\ & \mid & \mathtt{new}\ C(\textit{Expr}_1, \ldots, \textit{Expr}_k) & \textsf{newObj} \\ & \mid & \mathtt{new}\ \mathtt{std{:}{:}}L\langle\textit{Ty}_1, \ldots, \textit{Ty}_k\rangle & \textsf{newLib} \\ & & \qquad (\textit{Expr}_1, \ldots, \textit{Expr}_n) & \\ & \mid & \mathtt{this} & \textsf{this} \\ & \mid & \textit{Expr}.m(\textit{Expr}_1, \ldots, \textit{Expr}_k) & \textsf{methodCall} \\ & & \qquad \mid \textit{Expr}\texttt{->}m(\textit{Expr}_1, \ldots, \textit{Expr}_k) & \\ & \mid & \textit{Expr}.f \mid \textit{Expr}\texttt{->}f & \textsf{field, arrow} \\ & \mid & \mathtt{*}\textit{Expr} \mid \textit{Expr}_1[\textit{Expr}_2] & \textsf{deref, index} \\ & \mid & \mathtt{[=]}(\textit{Param}_1, \ldots, \textit{Param}_k)\ \texttt{->}\ \textit{Ty} & \textsf{lambda} \\ & & \qquad \{\, \textit{Cmd}_1 \ldots \textit{Cmd}_n \,\} & \\ & \mid & \textit{Expr}(\textit{Expr}_1, \ldots, \textit{Expr}_k) & \textsf{callFn} \\ & \mid & \mathsf{locOf}\ \textit{Expr} & \textsf{locOf} \\ & \mid & L.u(\textit{Expr}_1, \ldots, \textit{Expr}_k) & \textsf{intrinsic} \\ \textit{Cmd} & ::= & \{\, \textit{Cmd}_1 \ldots \textit{Cmd}_n \,\} & \textsf{Cmd.block} \\ & \mid & \mathtt{if}\ (\textit{Expr})\ \{\, \textit{Cmd}_1 \ldots \textit{Cmd}_n \,\} & \textsf{ite} \\ & & \qquad \mathtt{else}\ \{\, \textit{Cmd}'_1 \ldots \textit{Cmd}'_m \,\} & \\ & \mid & \mathtt{while}\ (\textit{Expr})\ \{\, \textit{Cmd}_1 \ldots \textit{Cmd}_n \,\} & \textsf{while} \\ & \mid & \mathtt{for}\ (\textit{Cmd}_0;\ \textit{Expr};\ \textit{Cmd}_s) & \textsf{for} \\ & & \qquad \{\, \textit{Cmd}_1 \ldots \textit{Cmd}_n \,\} & \\ & \mid & \mathtt{return} \mid \mathtt{return}\ \textit{Expr} & \textsf{ret} \\ & \mid & \textit{Ty}\ x = \textit{Expr} \mid \textit{Ty}\mathtt{\&}\ x = \textit{Expr} & \textsf{decl, declRef} \\ & \mid & \mathtt{auto}\ x = \textit{Expr} & \textsf{declAuto} \\ & \mid & \textit{Expr}_1 = \textit{Expr}_2 & \textsf{assign} \\ & \mid & \textit{Expr}; & \textsf{exprStmt} \\ & \mid & \mathtt{delete}\ \textit{Expr} & \textsf{delete} \\ \textit{Fun} & ::= & \textit{Ty}\ f(\textit{Param}_1, \ldots, \textit{Param}_k) & \textsf{Fun} \\ & & \qquad \{\, \textit{Cmd}_1 \ldots \textit{Cmd}_n \,\} & \\ \textit{Vis} & ::= & \mathtt{public} \mid \mathtt{private} & \textsf{Vis.pub, priv} \\ \textit{Member} & ::= & \textit{Ty}\ f; & \textsf{Field} \\ & \mid & \textit{Ty}\ m(\textit{Param}_1, \ldots, \textit{Param}_k) & \textsf{Method} \\ & & \qquad \{\, \textit{Cmd}_1 \ldots \textit{Cmd}_n \,\} & \\ & \mid & C(\textit{Param}_1, \ldots, \textit{Param}_k)\ \{\, \textit{Cmd}_1 \ldots \textit{Cmd}_n \,\} & \textsf{Ctor} \\ & \mid & \mathtt{\sim}C()\ \{\, \textit{Cmd}_1 \ldots \textit{Cmd}_n \,\} & \textsf{Dtor} \\ \textit{ClassDecl} & ::= & \mathtt{class}\ C\ (\mathtt{:}\ \mathtt{public}\ B)^{?} & \textsf{ClassDecl} \\ & & \qquad \{\, \textit{Member}_1 \ldots \textit{Member}_n \,\} & \\ \textit{Decl} & ::= & \textit{ClassDecl} \mid \textit{Fun} & \textsf{Decl.cls, fn} \\ & \mid & \mathtt{template}\ \langle\mathtt{typename}\ T\rangle\ \textit{ClassDecl} & \textsf{tmpl} \\ & \mid & \mathtt{template}\ \langle\mathtt{typename}\ T_1, \ldots, \mathtt{typename}\ T_k\rangle & \textsf{libTmpl} \\ & & \qquad \mathtt{class}\ L; & \\ & \mid & \textit{Ty}\ f(\textit{Param}_1, \ldots, \textit{Param}_k); & \textsf{libFn} \\ \textit{Program} & ::= & \textit{Decl}_1 \ldots \textit{Decl}_n & \textsf{Program} \end{array}

The symbols on the left are the nonterminals of this grammar, each named after the type of Syntax.lean it describes. The nonterminal Member stands for the four structures Field, Method, Ctor and Dtor.

The rules of the typing and of the evaluation abbreviate them, τ for a Ty, e for an Expr, c for a Cmd and p for a Param, and a subscript tells two occurrences apart.

Inside the productions, n stands for an integer literal and b for a boolean one, x for a variable, f for a field or a function, m for a method and u for an intrinsic, all of them written as a VarId, and C for a class, B for a base, T for a template parameter and L for a library class, all of them written as a TypeId.

The right column names, for each alternative, the constructor of the inductive type of Syntax.lean that the alternative builds, Expr.intLit for a literal and Cmd.block for a block. The type is written out on the first line of a category and only the constructor afterwards.

A constructor here is a case of an inductive definition of Lean, and not the member of a class that new runs, which this table calls Ctor.

Every field and every method carries a Vis, which the parser takes from the section that holds it. The constructor and the destructor are public and carry no visibility.

A parser has the type P α, a state monad over PState that gives an α or fails with a message. The state holds the tokens, the position of the next one, the prefix of the enclosing namespaces and, for each token, whether it comes from a header.

One parser function per expression nonterminal, from Expr down to Primary, named after it. Each level of the grammar is one level of precedence, and the repetition of an operator and its operand builds a left associative tree.

The function postfixExpr reads Chain, After and ChainNoCall inline. It covers the call of a named function, the call of a function value, indexing, field access through . and ->, and the method call in its two forms. The nonterminal After separates a method call from a field access.

The function unaryExpr adds the dereference, and primary covers literals, nullptr, this, variables, parenthesised expressions and the two forms of new. Lambdas are parsed as argument expressions, by argExpr, in the three positions the grammar gives them.

One parser function per command nonterminal and per type nonterminal, named after it. The function statement chooses the production by the first token, and a token that opens a type, by isTypeStart, opens a declaration. The function exprStatement reads an expression and then decides between assignment and expression statement by the presence of =.

A Type is a basic type or a class type, optionally followed by *. A class type is a name, qualified by namespaces or not, with template arguments or without. An unqualified name is read in the enclosing namespace. The case of the last component of a qualified name says which type it is, an uppercase one names a class of the program and a lowercase one a class of the library, whose names are lowercase, so Geometry::Shape is the first and std::vector<int> the second.

A template argument is a type, and a function type Type(Type, …) as well. A local declaration with a type may be a reference, and its initialiser may be a lambda.

A program is a sequence of declarations up to eof. Each one is a class, a class template, a namespace, a function, or a class template or a function of the library declared without a body.

The functions carry the names of their nonterminals, with three exceptions. The function classDecl reads Class, operatorName reads Op and P.name reads Name. The function classRest reads Section inline, and member reads MemberRest.

A class carries its fields, its methods, its constructor and its destructor, under the visibility of the section that holds them. A namespace is flattened at parse time, and every class it declares carries the prefix of the enclosing namespaces, as N::C.

The function runParser runs the lexer and a parser on a string and requires the whole input to be consumed. The function parseUnit parses the output of Preproc, runs the automaton on each line alone and the pass qualifiers on all the tokens, and marks the tokens of the lines that come from a header.