Values¶

The grammar productions in this section define lexical syntax, hence no white space is allowed.

Integers¶

All integers can be written in either decimal or hexadecimal notation. In both cases, digits can optionally be separated by underscores.

𝚜 𝚒 𝚐 𝚗 : : = 𝜖 \Rightarrow + 1 | ‘ + ’ \Rightarrow + 1 | ‘ - ’ \Rightarrow - 1 𝚍 𝚒 𝚐 𝚒 𝚝 : : = ‘ 𝟶 ’ \Rightarrow 0 | \dots | ‘ 𝟿 ’ \Rightarrow 9 𝚑 𝚎 𝚡 𝚍 𝚒 𝚐 𝚒 𝚝 : : = 𝑑 : 𝚍 𝚒 𝚐 𝚒 𝚝 \Rightarrow 𝑑 | ‘ 𝙰 ’ \Rightarrow 10 | \dots | ‘ 𝙵 ’ \Rightarrow 15 | ‘ 𝚊 ’ \Rightarrow 10 | \dots | ‘ 𝚏 ’ \Rightarrow 15 𝚗 𝚞 𝚖 : : = 𝑑 : 𝚍 𝚒 𝚐 𝚒 𝚝 \Rightarrow 𝑑 | 𝑛 : 𝚗 𝚞 𝚖 ‘_’ ? 𝑑 : 𝚍 𝚒 𝚐 𝚒 𝚝 \Rightarrow 10 𝑛 + 𝑑 𝚑 𝚎 𝚡 𝚗 𝚞 𝚖 : : = ℎ : 𝚑 𝚎 𝚡 𝚍 𝚒 𝚐 𝚒 𝚝 \Rightarrow ℎ | 𝑛 : 𝚑 𝚎 𝚡 𝚗 𝚞 𝚖 ‘_’ ? ℎ : 𝚑 𝚎 𝚡 𝚍 𝚒 𝚐 𝚒 𝚝 \Rightarrow 16 𝑛 + ℎ

The allowed syntax for integer literals depends on size and signedness. Moreover, their value must lie within the range of the respective type.

𝚞 𝑁 : : = 𝑛 : 𝚗 𝚞 𝚖 \Rightarrow 𝑛 i f 𝑛 < 2 𝑁 | ‘ 𝟶 𝚡 ’ 𝑛 : 𝚑 𝚎 𝚡 𝚗 𝚞 𝚖 \Rightarrow 𝑛 i f 𝑛 < 2 𝑁 𝚜 𝑁 : : = 𝑠 : 𝚜 𝚒 𝚐 𝚗 𝑛 : 𝚞 𝑁 \Rightarrow 𝑠 \cdot 𝑛 i f - 2 𝑁 - 1 \leq 𝑠 \cdot 𝑛 < 2 𝑁 - 1

Uninterpreted integers can be written as either signed or unsigned, and are normalized to unsigned in the abstract syntax.

𝚒 𝑁 : : = 𝑛 : 𝚞 𝑁 \Rightarrow 𝑛 | 𝑖 : 𝚜 𝑁 \Rightarrow s i g n e d - 1 𝑁 (𝑖)

Floating-Point¶

Floating-point values can be represented in either decimal or hexadecimal notation.

𝚏 𝚛 𝚊 𝚌 : : = 𝑑 : 𝚍 𝚒 𝚐 𝚒 𝚝 \Rightarrow 𝑑 / 10 | 𝑑 : 𝚍 𝚒 𝚐 𝚒 𝚝 ‘_’ ? 𝑝 : 𝚏 𝚛 𝚊 𝚌 \Rightarrow (𝑑 + 𝑝 / 10) / 10 𝚑 𝚎 𝚡 𝚏 𝚛 𝚊 𝚌 : : = ℎ : 𝚑 𝚎 𝚡 𝚍 𝚒 𝚐 𝚒 𝚝 \Rightarrow ℎ / 16 | ℎ : 𝚑 𝚎 𝚡 𝚍 𝚒 𝚐 𝚒 𝚝 ‘_’ ? 𝑝 : 𝚑 𝚎 𝚡 𝚏 𝚛 𝚊 𝚌 \Rightarrow (ℎ + 𝑝 / 16) / 16 𝚖 𝚊 𝚗 𝚝 : : = 𝑝 : 𝚗 𝚞 𝚖 ‘ . ’ ? \Rightarrow 𝑝 | 𝑝 : 𝚗 𝚞 𝚖 ‘ . ’ 𝑞 : 𝚏 𝚛 𝚊 𝚌 \Rightarrow 𝑝 + 𝑞 𝚑 𝚎 𝚡 𝚖 𝚊 𝚗 𝚝 : : = 𝑝 : 𝚑 𝚎 𝚡 𝚗 𝚞 𝚖 ‘ . ’ ? \Rightarrow 𝑝 | 𝑝 : 𝚑 𝚎 𝚡 𝚗 𝚞 𝚖 ‘ . ’ 𝑞 : 𝚑 𝚎 𝚡 𝚏 𝚛 𝚊 𝚌 \Rightarrow 𝑝 + 𝑞 𝚏 𝚕 𝚘 𝚊 𝚝 : : = 𝑝 : 𝚖 𝚊 𝚗 𝚝 (‘ 𝙴 ’ | ‘ 𝚎 ’) 𝑠 : 𝚜 𝚒 𝚐 𝚗 𝑒 : 𝚗 𝚞 𝚖 \Rightarrow 𝑝 \cdot 10 𝑠 \cdot 𝑒 𝚑 𝚎 𝚡 𝚏 𝚕 𝚘 𝚊 𝚝 : : = ‘ 𝟶 𝚡 ’ 𝑝 : 𝚑 𝚎 𝚡 𝚖 𝚊 𝚗 𝚝 (‘ 𝙿 ’ | ‘ 𝚙 ’) 𝑠 : 𝚜 𝚒 𝚐 𝚗 𝑒 : 𝚗 𝚞 𝚖 \Rightarrow 𝑝 \cdot 2 𝑠 \cdot 𝑒

The value of a literal must not lie outside the representable range of the corresponding IEEE 754 type (that is, a numeric value must not overflow to $\pm \infty$ ), but it may be rounded to the nearest representable value.

Note

Rounding can be prevented by using hexadecimal notation with no more significant bits than supported by the required type.

Floating-point values may also be written as constants for infinity or canonical NaN (not a number). Furthermore, arbitrary NaN values may be expressed by providing an explicit payload value.

𝚏 𝑁 : : = (+ 1) : 𝚜 𝚒 𝚐 𝚗 𝑞 : 𝚏 𝑁 𝚖 𝚊 𝚐 \Rightarrow + 𝑞 | (- 1) : 𝚜 𝚒 𝚐 𝚗 𝑞 : 𝚏 𝑁 𝚖 𝚊 𝚐 \Rightarrow - 𝑞 𝚏 𝑁 𝚖 𝚊 𝚐 : : = 𝑞 : 𝚏 𝚕 𝚘 𝚊 𝚝 \Rightarrow f l o a t 𝑁 (𝑞) i f f l o a t 𝑁 (𝑞) \neq \infty | 𝑞 : 𝚑 𝚎 𝚡 𝚏 𝚕 𝚘 𝚊 𝚝 \Rightarrow f l o a t 𝑁 (𝑞) i f f l o a t 𝑁 (𝑞) \neq \infty | ‘ 𝚒 𝚗 𝚏 ’ \Rightarrow \infty | ‘ 𝚗 𝚊 𝚗 ’ \Rightarrow 𝗇 𝖺 𝗇 (c a n o n 𝑁) | ‘ 𝚗 𝚊 𝚗 : 𝟶 𝚡 ’ 𝑛 : 𝚑 𝚎 𝚡 𝚗 𝚞 𝚖 \Rightarrow 𝗇 𝖺 𝗇 (𝑛) i f 1 \leq 𝑛 < 2 s i g n i f (𝑁)

Strings¶

Strings denote sequences of bytes that can represent both textual and binary data. They are enclosed in quotation marks and may contain any character other than ASCII control characters, quotation marks ( $‘'' ’$ ), or backslash ( $‘\’$ ), except when expressed with an escape sequence.

𝚜𝚝𝚛𝚒𝚗𝚐::=‘′⁢′’  (𝑏∗:𝚜𝚝𝚛𝚒𝚗𝚐𝚎𝚕𝚎𝚖)∗  ‘′⁢′’⇒⨁𝑏∗∗if |⨁𝑏∗∗|<232𝚜𝚝𝚛𝚒𝚗𝚐𝚎𝚕𝚎𝚖::=𝑐:𝚜𝚝𝚛𝚒𝚗𝚐𝚌𝚑𝚊𝚛⇒utf⁢8⁢(𝑐)|‘\’  ℎ1:𝚑𝚎𝚡𝚍𝚒𝚐𝚒𝚝  ℎ2:𝚑𝚎𝚡𝚍𝚒𝚐𝚒𝚝⇒16ℎ1+ℎ2

Each character in a string literal represents the byte sequence corresponding to its UTF-8 Unicode (Section 2.5) encoding, except for hexadecimal escape sequences $‘\𝚑𝚑’$ , which represent raw bytes of the respective value.

𝚜𝚝𝚛𝚒𝚗𝚐𝚌𝚑𝚊𝚛::=𝑐:𝚌𝚑𝚊𝚛⇒𝑐if 𝑐≥U+20∧𝑐≠U+7⁢F∧𝑐≠‘′⁢′’∧𝑐≠‘\’|‘\𝚝’⇒U+09|‘\𝚗’⇒U+0⁢A|‘\𝚛’⇒U+0⁢D|‘\′⁢′’⇒U+22|‘\′’⇒U+27|‘\\’⇒U+5⁢C|‘\𝚞{’  𝑛:𝚑𝚎𝚡𝚗𝚞𝚖  ‘}’⇒𝑛if 𝑛<𝟶⁢𝚡𝙳⁢𝟾𝟶𝟶∨𝟶⁢𝚡𝙴⁢𝟾𝟶𝟶≤𝑛<𝟶⁢𝚡⁢𝟷𝟷𝟶𝟶𝟶𝟶

Names¶

Names are strings denoting a literal character sequence. A name string must form a valid UTF-8 encoding as defined by Unicode (Section 2.5) and is interpreted as a string of Unicode scalar values.

𝚗 𝚊 𝚖 𝚎 : : = 𝑏 * : 𝚜 𝚝 𝚛 𝚒 𝚗 𝚐 \Rightarrow 𝑐 * i f 𝑏 * = u t f 8 (𝑐 *)

Note

Presuming the source text is itself encoded correctly, strings that do not contain any uses of hexadecimal byte escapes are always valid names.

Identifiers¶

Indices can be given in both numeric and symbolic form. Symbolic identifiers that stand in lieu of indices start with $‘ $ ’$ , followed by eiter a sequence of printable ASCII characters that does not contain a space, quotation mark, comma, semicolon, or bracket, or by a quoted name.

𝚒𝚍::=‘$’  𝑐∗:𝚒𝚍𝚌𝚑𝚊𝚛+⇒𝑐∗|‘$’  𝑐∗:𝚗𝚊𝚖𝚎⇒𝑐∗if |𝑐∗|>0𝚒𝚍𝚌𝚑𝚊𝚛::=‘𝟶’  |  …  |  ‘𝟿’|‘𝙰’  |  …  |  ‘𝚉’|‘𝚊’  |  …  |  ‘𝚣’|‘!’  |  ‘#’  |  ‘$’  |  ‘%’  |  ‘&’  |  ‘′’  |  ‘∗’  |  ‘+’  |  ‘-’  |  ‘.’  |  ‘/’|‘:’  |  ‘<’  |  ‘=’  |  ‘>’  |  ‘?’  |  ‘@’  |  ‘\’  |  ‘ˆ  ’  |  ‘_’  |  ‘`  ’  |  ‘|’  |  ‘˜  ’

Note

The value of an identifier character is the Unicode codepoint denoting it.

Conventions¶

The expansion rules of some abbreviations require insertion of a fresh identifier. That may be any syntactically valid identifier that does not already occur in the given source text.