Core C++

1.2. Grammar🔗

Definition1.2.1
Group: Syntax, tokens and the parser. (13)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

The grammar of Core C++, in EBNF. The superscript X^{*} repeats X zero or more times, and the superscript X^{?} makes X optional. Large parentheses group, the bar separates alternatives, and terminals are in typewriter font. The grammar has no left recursive production, and it is left factored.

\begin{array}{lcl} \textit{Program} & ::= & \textit{Declaration}^{*} \\ \textit{Declaration} & ::= & \texttt{namespace}\ \textit{Name}\ \texttt{\{}\ \textit{Declaration}^{*}\ \texttt{\}} \\ & \mid & \texttt{template}\ \texttt{<}\ \texttt{typename}\ \textit{TypeId}\ \big(\ \texttt{,}\ \texttt{typename}\ \textit{TypeId}\ \big)^{*}\ \texttt{>} \\ & & \qquad \texttt{class}\ \big(\ \textit{TypeId}\ \textit{ClassRest}\ \mid\ \textit{VarId}\ \texttt{;}\ \big) \\ & \mid & \textit{Class} \\ & \mid & \textit{Function} \\ \textit{Name} & ::= & \textit{TypeId}\ \mid\ \textit{VarId} \\ \textit{Class} & ::= & \texttt{class}\ \textit{TypeId}\ \textit{ClassRest} \\ \textit{ClassRest} & ::= & \big(\ \texttt{:}\ \texttt{public}\ \textit{ClassType}\ \big)^{?}\ \texttt{\{}\ \textit{Member}^{*}\ \textit{Section}^{*}\ \texttt{\}}\ \texttt{;} \\ \textit{Section} & ::= & \big(\ \texttt{public}\ \mid\ \texttt{private}\ \big)\ \texttt{:}\ \textit{Member}^{*} \\ \textit{Member} & ::= & \texttt{virtual}\ \big(\ \textit{Type}\ \texttt{\&}^{?}\ \textit{MemberRest}\ \mid\ \texttt{\textasciitilde}\ \textit{TypeId}\ \texttt{(}\ \texttt{)}\ \textit{Block}\ \big) \\ & \mid & \texttt{\textasciitilde}\ \textit{TypeId}\ \texttt{(}\ \texttt{)}\ \textit{Block} \\ & \mid & \big(\ \textit{BasicType}\ \mid\ \textit{NsId}\ \texttt{::}\ \textit{QualTail}\ \texttt{*}^{?}\ \big)\ \texttt{\&}^{?}\ \textit{MemberRest} \\ & \mid & \textit{TypeId}\ \big(\ \textit{Params}\ \textit{Block} \\ & & \qquad \mid\ \textit{TemplateArgs}^{?}\ \texttt{*}^{?}\ \texttt{\&}^{?}\ \textit{MemberRest}\ \big) \\ \textit{MemberRest} & ::= & \textit{VarId}\ \big(\ \texttt{;}\ \mid\ \textit{Params}\ \texttt{override}^{?}\ \textit{Block}\ \big) \\ & \mid & \texttt{operator}\ \textit{Op}\ \textit{Params}\ \textit{Block} \\ \textit{Op} & ::= & \texttt{+}\ \mid\ \texttt{-}\ \mid\ \texttt{*}\ \mid\ \texttt{/}\ \mid\ \texttt{\%}\ \mid\ \texttt{==}\ \mid\ \texttt{!=}\ \mid\ \texttt{<}\ \mid\ \texttt{<=}\ \mid\ \texttt{>}\ \mid\ \texttt{>=}\ \mid\ \texttt{[}\ \texttt{]} \\ \textit{Function} & ::= & \textit{Type}\ \textit{VarId}\ \textit{Params}\ \big(\ \textit{Block}\ \mid\ \texttt{;}\ \big) \\ \textit{Params} & ::= & \texttt{(}\ \big(\ \textit{Param}\ \big(\ \texttt{,}\ \textit{Param}\ \big)^{*}\ \big)^{?}\ \texttt{)} \\ \textit{Param} & ::= & \textit{Type}\ \texttt{\&}^{?}\ \textit{VarId} \\ \textit{Type} & ::= & \textit{BasicType}\ \mid\ \textit{ClassType}\ \texttt{*}^{?} \\ \textit{TemplateArg} & ::= & \textit{Type}\ \big(\ \texttt{(}\ \big(\ \textit{Type}\ \big(\ \texttt{,}\ \textit{Type}\ \big)^{*}\ \big)^{?}\ \texttt{)}\ \big)^{?} \\ \textit{BasicType} & ::= & \texttt{int}\ \mid\ \texttt{bool}\ \mid\ \texttt{void} \\ \textit{ClassType} & ::= & \textit{NsId}\ \texttt{::}\ \textit{QualTail}\ \mid\ \textit{TypeId}\ \textit{TemplateArgs}^{?} \\ \textit{QualTail} & ::= & \textit{NsId}\ \texttt{::}\ \textit{QualTail}\ \mid\ \textit{Name}\ \textit{TemplateArgs}^{?} \\ \textit{TemplateArgs} & ::= & \texttt{<}\ \textit{TemplateArg}\ \big(\ \texttt{,}\ \textit{TemplateArg}\ \big)^{*}\ \texttt{>} \\ \textit{Block} & ::= & \texttt{\{}\ \textit{Statement}^{*}\ \texttt{\}} \\ \textit{Statement} & ::= & \textit{Block} \\ & \mid & \texttt{if}\ \texttt{(}\ \textit{Expr}\ \texttt{)}\ \textit{Block}\ \big(\ \texttt{else}\ \textit{Block}\ \big)^{?} \\ & \mid & \texttt{while}\ \texttt{(}\ \textit{Expr}\ \texttt{)}\ \textit{Block} \\ & \mid & \texttt{for}\ \texttt{(}\ \textit{ForInit}\ \texttt{;}\ \textit{Expr}\ \texttt{;}\ \textit{ExprStatement}\ \texttt{)}\ \textit{Block} \\ & \mid & \texttt{return}\ \textit{ArgExpr}^{?}\ \texttt{;} \\ & \mid & \texttt{delete}\ \textit{Expr}\ \texttt{;} \\ & \mid & \textit{LocalDecl}\ \texttt{;} \\ & \mid & \textit{ExprStatement}\ \texttt{;} \\ \textit{LocalDecl} & ::= & \texttt{auto}\ \textit{VarId}\ \texttt{=}\ \textit{Expr} \\ & \mid & \textit{Type}\ \texttt{\&}^{?}\ \textit{VarId}\ \texttt{=}\ \textit{ArgExpr} \\ \textit{ForInit} & ::= & \textit{LocalDecl}\ \mid\ \textit{ExprStatement} \\ \textit{ExprStatement} & ::= & \textit{Expr}\ \big(\ \texttt{=}\ \textit{Expr}\ \big)^{?} \\ \textit{Expr} & ::= & \textit{OrExpr}\ \big(\ \texttt{?}\ \textit{Expr}\ \texttt{:}\ \textit{Expr}\ \big)^{?} \\ \textit{OrExpr} & ::= & \textit{AndExpr}\ \big(\ \texttt{||}\ \textit{AndExpr}\ \big)^{*} \\ \textit{AndExpr} & ::= & \textit{EqExpr}\ \big(\ \texttt{\&\&}\ \textit{EqExpr}\ \big)^{*} \\ \textit{EqExpr} & ::= & \textit{RelExpr}\ \big(\ \big(\ \texttt{==}\ \mid\ \texttt{!=}\ \big)\ \textit{RelExpr}\ \big)^{*} \\ \textit{RelExpr} & ::= & \textit{AddExpr}\ \big(\ \big(\ \texttt{<}\ \mid\ \texttt{<=}\ \mid\ \texttt{>}\ \mid\ \texttt{>=}\ \big)\ \textit{AddExpr}\ \big)^{*} \\ \textit{AddExpr} & ::= & \textit{MulExpr}\ \big(\ \big(\ \texttt{+}\ \mid\ \texttt{-}\ \big)\ \textit{MulExpr}\ \big)^{*} \\ \textit{MulExpr} & ::= & \textit{UnaryExpr}\ \big(\ \big(\ \texttt{*}\ \mid\ \texttt{/}\ \mid\ \texttt{\%}\ \big)\ \textit{UnaryExpr}\ \big)^{*} \\ \textit{UnaryExpr} & ::= & \big(\ \texttt{!}\ \mid\ \texttt{-}\ \mid\ \texttt{*}\ \big)\ \textit{UnaryExpr}\ \mid\ \textit{PostfixExpr} \\ \textit{PostfixExpr} & ::= & \textit{Primary}\ \textit{Chain} \\ \textit{Chain} & ::= & \big(\ \texttt{[}\ \textit{Expr}\ \texttt{]}\ \textit{Chain}\ \mid\ \texttt{.}\ \textit{VarId}\ \textit{After} \\ & & \qquad \mid\ \texttt{->}\ \textit{VarId}\ \textit{After}\ \mid\ \textit{Args}\ \textit{Chain}\ \big)^{?} \\ \textit{After} & ::= & \textit{Args}\ \textit{Chain}\ \mid\ \textit{ChainNoCall} \\ \textit{ChainNoCall} & ::= & \big(\ \texttt{[}\ \textit{Expr}\ \texttt{]}\ \textit{Chain}\ \mid\ \texttt{.}\ \textit{VarId}\ \textit{After} \\ & & \qquad \mid\ \texttt{->}\ \textit{VarId}\ \textit{After}\ \big)^{?} \\ \textit{Primary} & ::= & \textit{IntLit}\ \mid\ \texttt{true}\ \mid\ \texttt{false}\ \mid\ \texttt{nullptr}\ \mid\ \texttt{this}\ \mid\ \textit{VarId} \\ & \mid & \texttt{(}\ \textit{Expr}\ \texttt{)} \\ & \mid & \texttt{new}\ \textit{ClassType}\ \textit{Args} \\ \textit{Args} & ::= & \texttt{(}\ \big(\ \textit{ArgExpr}\ \big(\ \texttt{,}\ \textit{ArgExpr}\ \big)^{*}\ \big)^{?}\ \texttt{)} \\ \textit{ArgExpr} & ::= & \textit{Lambda}\ \mid\ \textit{Expr} \\ \textit{Lambda} & ::= & \texttt{[=]}\ \textit{Params}\ \texttt{->}\ \textit{Type}\ \textit{Block} \end{array}

A statement is a command or an expression followed by ;. Assignment is a command, and ExprStatement joins the two forms that start with an expression to keep the grammar LL(1).

In the abstract syntax the commands form the type Cmd, and the expression statement is the command exprStmt, which evaluates and discards the value. The left side of an assignment must denote a location, a check made by the type checker.

A lambda expression is an ArgExpr and not a Primary, so it occurs only as argument, as initialiser of a declaration with a type and as return expression.

The parser rejects forms that the grammar derives and the subset excludes.

A class template with a body has one type parameter, and an instantiation of a class template of the program has one template argument. A class of the library always takes template arguments, and a base class is a class of the program.

A lambda parameter is by value, and a field is not a reference. A namespace holds only classes, templates and namespaces.

Only a header of Core C++ opens the namespace std, declares a function without a body or declares a class template without a body, since C++ leaves a program that adds declarations to std undefined (N4659 §20.5.4.2.1, paragraph 1). Preproc marks the lines that come from a header, and the parser reads the marks. The type checker then rejects a class template without a body that no intrinsic implements.

The parser also checks the names of the constructor and the destructor against their class. A class has at most one of each, both are public, and a field is never virtual. The public destructor is a restriction of the subset, since C++ accepts a private destructor that no code outside the class calls.

Lean code for Definition1.2.1●3 definitions
  • inductive(6 constructors)defined in CoreCpp/GrammarTerm.lean
    complete
    inductive CoreCpp.Grammar.Term : Type
    inductive CoreCpp.Grammar.Term : Type
    A terminal of the grammar, a token class. Reserved words and symbols stand
for themselves, identifiers and literals for their class.

    Constructors

    CoreCpp.Grammar.Term.kw (s : String) : CoreCpp.Grammar.Term
    CoreCpp.Grammar.Term.sym (s : String) : CoreCpp.Grammar.Term
    CoreCpp.Grammar.Term.typeId : CoreCpp.Grammar.Term
    CoreCpp.Grammar.Term.varId : CoreCpp.Grammar.Term
    CoreCpp.Grammar.Term.nsId : CoreCpp.Grammar.Term
    CoreCpp.Grammar.Term.intLit : CoreCpp.Grammar.Term
  • defdefined in CoreCpp/GrammarRules.lean
    complete
    def CoreCpp.Grammar.rules : List (LL1.Rule CoreCpp.Grammar.Term)
    def CoreCpp.Grammar.rules :
  List (LL1.Rule CoreCpp.Grammar.Term)
    The rules of the grammar of Core C++, generated from `grammar/core-cpp.ebnf`.
  • defdefined in CoreCpp/Grammar.lean
    complete
    def CoreCpp.Grammar.grammar : LL1.Grammar CoreCpp.Grammar.Term
    def CoreCpp.Grammar.grammar :
  LL1.Grammar CoreCpp.Grammar.Term
    The grammar in BNF.
Theorem1.2.2
Group: Syntax, tokens and the parser. (13)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

The grammar is LL(1).

Lean code for Theorem1.2.2●7 declarations
  • theoremdefined in CoreCpp/Grammar.lean
    complete
    theorem CoreCpp.Grammar.isLL1_grammar : CoreCpp.Grammar.grammar.isLL1 = true
    theorem CoreCpp.Grammar.isLL1_grammar :
  CoreCpp.Grammar.grammar.isLL1 = true
    The grammar of Core C++ is LL(1). The table has no entry with two
productions. The proof evaluates `Grammar.isLL1` with `native_decide`, which
trusts the compiled evaluation.
  • defdefined in CoreCpp/Grammar.lean
    complete
    def CoreCpp.Grammar.table : LL1.Table CoreCpp.Grammar.Term
    def CoreCpp.Grammar.table :
  LL1.Table CoreCpp.Grammar.Term
    The predictive parsing table of the grammar.
  • defdefined in CoreCpp/Grammar.lean
    complete
    def CoreCpp.Grammar.derive (src : String) : Except String (List Nat)
    def CoreCpp.Grammar.derive (src : String) :
  Except String (List Nat)
    The leftmost derivation of a program by the predictive parser, from the
tokens of the lexer without the end token.
  • defdefined in LL1/Parser.lean
    complete
    def LL1.translate {T : Type} (start : String) (rules : List (LL1.Rule T)) :
  LL1.Grammar T
    def LL1.translate {T : Type} (start : String)
  (rules : List (LL1.Rule T)) :
  LL1.Grammar T
    The BNF grammar of a list of EBNF rules. A top level alternative gives one
production per alternative, without an auxiliary nonterminal.
  • defdefined in LL1/Parser.lean
    complete
    def LL1.Grammar.isLL1 {T : Type} [DecidableEq T] (g : LL1.Grammar T) : Bool
    def LL1.Grammar.isLL1 {T : Type}
  [DecidableEq T] (g : LL1.Grammar T) :
  Bool
    The grammar is LL(1) when its table has no conflict. Equivalently, any two
productions of a nonterminal have disjoint `predict` sets. The set of `A → α`
is FIRST(α), together with FOLLOW(A) when α is nullable.
  • defdefined in LL1/Parser.lean
    complete
    def LL1.Grammar.table {T : Type} [DecidableEq T] (g : LL1.Grammar T) :
  LL1.Table T
    def LL1.Grammar.table {T : Type}
  [DecidableEq T] (g : LL1.Grammar T) :
  LL1.Table T
  • defdefined in LL1/Parser.lean
    complete
    def LL1.Grammar.parse.{u_1} {T : Type} [DecidableEq T] {α : Type u_1}
  [Hashable T] (g : LL1.Grammar T) (tb : LL1.Table T) (cls : α → T)
  (input : List α) : Except String (List Nat)
    def LL1.Grammar.parse.{u_1} {T : Type}
  [DecidableEq T] {α : Type u_1}
  [Hashable T] (g : LL1.Grammar T)
  (tb : LL1.Table T) (cls : α → T)
  (input : List α) :
  Except String (List Nat)
    The nonrecursive predictive parser. The stack starts with the start symbol.
A terminal on top must match the next token, and the parser pops it and
consumes the token. For a nonterminal `A` on top, the table gives a production
for `A` and the lookahead, the first one when the entry holds several. The
parser replaces `A` by the right side of that production and outputs its
index. The parser accepts when stack and input end together, and its output
is the leftmost derivation. It runs within a fuel bound and fails with
`parser fuel exhausted` when the bound runs out. Deeply nested nullable
nonterminals can exhaust it on a valid input.
Proof for Theorem 1.2.2
uses 0

The proof is a computation. The theorem CoreCpp.Grammar.isLL1_grammar builds the predictive parsing table of the grammar of Definition 1.2.1 and checks that no entry holds two productions.

The grammar comes from the file grammar/core-cpp.ebnf, rule by rule over token classes. The generator lake exe ebnf2lean writes the file as the module CoreCpp/GrammarRules.lean, and the theorem is about the rules of that module.

The library LL1 of the package ll1-lean translates them from EBNF to BNF. It then computes the nullable nonterminals, FIRST and FOLLOW as least fixed points, and fills the table.

Three left factorings and one restriction of the language explain the result.

In Member, a TypeId opens both a constructor and the type of a field or method. The next token decides, ( for a constructor and any other token for a type.

In ExprStatement, an assignment and an expression statement share the prefix Expr, and the token = decides.

In Declaration, a class template with a body and a class template of the library without one share the prefix up to class. The case of the name decides, a TypeId for the first and a VarId for the second.

In Statement, the FIRST sets of LocalDecl and ExprStatement are disjoint. A local declaration starts with auto, int, bool, void, a TypeId or an NsId. An expression starts with a VarId, an IntLit, true, false, nullptr, this, new, (, !, - or *, and never with a TypeId or an NsId.

The restriction shapes Chain. After a . or a ->, an argument list opens the arguments of a method, so e.f(a) and e->f(a) are method calls and never the call of a function held in a field. The nonterminal After says exactly that, since a field access continues through ChainNoCall, which no argument list may follow directly.

Without the restriction the two readings would both derive e->f(a) and no lookahead would separate them.

A function held in a field is called by binding it first, as in std::function<int(int)> h = b->handler; h(3);, and calling it in place is a type error that names the field.

The same table drives the nonrecursive predictive parser LL1.Grammar.parse, which CoreCpp.Grammar.derive runs on the tokens of a program.