r[notation]

Notation

Grammar

The following notations are used by the Lexer and Syntax grammar snippets:

Notation	Examples	Meaning
CAPITAL	KW_IF, INTEGER_LITERAL	A token produced by the lexer
ItalicCamelCase	LetStatement, Item	A syntactical production
string	x, while, *	The exact character(s)
x?	pub?	An optional item
x*	OuterAttribute*	0 or more of x
x+	MacroMatch+	1 or more of x
xa..b	HEX_DIGIT1..6	a to b repetitions of x
Rule1 Rule2	fn Name Parameters	Sequence of rules in order
|	u8 | u16, Block | Item	Either one or another
[ ]	[b B]	Any of the characters listed
[ - ]	[a-z]	Any of the characters in the range
~[ ]	~[b B]	Any characters, except those listed
~string	~\n, ~*/	Any characters, except this sequence
( )	(, Parameter)?	Groups items
U+xxxx	U+0060	A single unicode character
<text>	<any ASCII char except CR>	An English description of what should be matched
Rule suffix	IDENTIFIER_OR_KEYWORD except crate	A modification to the previous rule

Sequences have a higher precedence than | alternation.

String table productions

Some rules in the grammar — notably unary operators, binary operators, and keywords — are given in a simplified form: as a listing of printable strings. These cases form a subset of the rules regarding the token rule, and are assumed to be the result of a lexical-analysis phase feeding the parser, driven by a DFA, operating over the disjunction of all such string table entries.

When such a string in monospace font occurs inside the grammar, it is an implicit reference to a single member of such a string table production. See tokens for more information.

Grammar visualizations

Below each grammar block is a button to toggle the display of a syntax diagram. A square element is a non-terminal rule, and a rounded rectangle is a terminal.

Common productions

The following are common definitions used in the grammar.

r[input.syntax]

@root CHAR -> <a Unicode scalar value>

NUL -> U+0000

TAB -> U+0009

LF -> U+000A

CR -> U+000D

r[notation.tools]

Common tools in examples

In code examples throughout this book, we use certain tools and patterns which we document below.

r[notation.tools.prove]

prove!

macro_rules! prove { /* .. */ }

Given a set of antecedent type system predicates, assert that a set of consequent predicates are (=>) or are not (?=>) proven by rustc.

The macro accepts a set of parameters in a for<..> binder. These parameters are put into scope for the antecedent and consequent. When using the => rule, the macro asserts that rustc can prove the consequent given the antecedent. When using the ?=> rule, the macro asserts that rustc does not prove the consequent give the antecedent.

For example, if we say prove! { for<'a, 'b, 'c> { 'a: 'b, 'b: 'c } => { 'a: 'c } }, read that as, “for all lifetimes 'a, 'b, 'c, assert that 'a: 'b and 'b: 'c implies 'a: 'c”.

Similarly, if we say prove! { for<T> { T: ?Sized } ?=> { T: Sized } }, we mean “for all types T, assert that if the Sized bound on T is relaxed then we do not prove T: Sized”.

When asserting what is proven by rustc, lifetimes are taken into account. However, when asserting what is not proven by rustc, lifetime bounds are ignored and treated as it they always hold, so asserting lifetime relationships in the consequent with the ?=> rule will produce misleading results (this book never does that).

Syntax

@root ProveBody ->
    ( `for<` ProveParams? `>` )? `{` ProveAntecedents? `}`
    ( `=>` | `?=>` ) `{` ProveConsequents? `}`

ProveParams -> (
        ProveLtParams ( `,` ProveTyParams )?
      | ProveTyParams
    ) `,`?

ProveLtParams -> Lifetime ( `,` Lifetime )*

ProveTyParams -> IDENTIFIER ( `,` IDENTIFIER )*

ProveAntecedents -> WhereClauseItem ( `,` WhereClauseItem )*  `,`?

ProveConsequents -> WhereClauseItem ( `,` WhereClauseItem )*  `,`?

Examples

{{#rustdoc_include notation/prove.rs:-1 }}
// Assert that rustc proves that `U: From<T>` implies `T: Into<U>`.
prove! { for<T, U> { U: From<T> } => { T: Into<U> } }
//~^               ~~~~~~~~~~~~~~    ~~~~~~~~~~~~~~ Consequent.
//~|                 Antecedent.
prove! { {} => { u32: Into<u64> } }
//~^     ~~ It's OK for the antecedent to be empty.
prove! { for<'a, 'b, 'c> { 'a: 'b, 'b: 'c } => { 'a: 'c } }
//~^                     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
//~|                           Transitive property.
prove! { for<T> { T: ?Sized } ?=> { T: Sized } }
//~^                          ~~~
//~| Asserts that rustc does not make this implication.

{{#rustdoc_include notation/prove.rs:-1 }}
// This is an error as it does not logically hold.
prove! { for<'a, 'b> {} => { 'a: 'b } } //~ ERROR

{{#rustdoc_include notation/prove.rs:-1 }}
// This is an error as the `?=>` rule treats lifetime bounds as
// always holding.
prove! { for<'a, 'b> {} ?=> { 'a: 'b } } //~ ERROR