leo/grammar/abnf-grammar.txt

; Leo Library
;
; Copyright (C) 2021 Aleo Systems Inc.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Format Note
; -----------

; The ABNF standard requires grammars to consist of lines terminated by CR LF
; (i.e. carriage return followed by line feed, DOS/Windows-style),
; as explained in the background on ABNF later in this file.
; This file's lines are therefore terminated by CR LF.
; To avoid losing this requirement across systems,
; this file is marked as 'text eol=crlf' in .gitattributes:
; this means that the file is textual, enabling visual diffs,
; but its lines will always be terminated by CR LF on any system.

; Note that this CR LF requirement only applies to the grammar files themselves.
; It does not apply to the lines of the languages described by the grammar.
; ABNF grammars may describe any kind of languages,
; with any kind of line terminators,
; or even without line terminators at all (e.g. for "binary" languages).

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Introduction
; ------------

; This file contains an ABNF (Augmented Backus-Naur Form) grammar of Leo.
; Background on ABNF is provided later in this file.

; This grammar provides an official definition of the syntax of Leo
; that is both human-readable and machine-readable.
; It will be part of an upcoming Leo language reference.
; It may also be used to generate parser tests at some point.

; We are also using this grammar
; as part of a mathematical formalization of the Leo language,
; which we are developing in the ACL2 theorem prover
; and which we plan to publish at some point.
; In particular, we have used a formally verified parser of ABNF grammars
; (at https://github.com/acl2/acl2/tree/master/books/kestrel/abnf;
; also see the paper at https://www.kestrel.edu/people/coglio/vstte18.pdf)
; to parse this grammar into a formal representation of the Leo concrete syntax
; and to validate that the grammar satisfies certain consistency properties.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Background on ABNF
; ------------------

; ABNF is an Internet standard:
; see RFC 5234 at https://www.rfc-editor.org/info/rfc5234
; and RFC 7405 at https://www.rfc-editor.org/info/rfc7405.
; It is used to specify the syntax of JSON, HTTP, and other standards.

; ABNF adds conveniences and makes slight modifications
; to Backus-Naur Form (BNF),
; without going beyond context-free grammars.

; Instead of BNF's angle-bracket notation for nonterminals,
; ABNF uses case-insensitive names consisting of letters, digits, and dashes,
; e.g. HTTP-message and IPv6address.
; ABNF includes an angle-bracket notation for prose descriptions,
; e.g. <host, see [RFC3986], Section 3.2.2>,
; usable as last resort in the definiens of a nonterminal.

; While BNF allows arbitrary terminals,
; ABNF uses only natural numbers as terminals,
; and denotes them via:
; (i) binary, decimal, or hexadecimal sequences,
; e.g. %b1.11.1010, %d1.3.10, and %x.1.3.A
; all denote the sequence of terminals '1 3 10';
; (ii) binary, decimal, or hexadecimal ranges,
; e.g. %x30-39 denotes any singleton sequence of terminals
; 'n' with 48 <= n <= 57 (an ASCII digit);
; (iii) case-sensitive ASCII strings,
; e.g. %s"Ab" denotes the sequence of terminals '65 98';
; and (iv) case-insensitive ASCII strings,
; e.g. %i"ab", or just "ab", denotes
; any sequence of terminals among
; '65 66',
; '65 98',
; '97 66', and
; '97 98'.
; ABNF terminals in suitable sets represent ASCII or Unicode characters.

; ABNF allows repetition prefixes n*m,
; where n and m are natural numbers in decimal notation;
; if absent,
; n defaults to 0, and
; m defaults to infinity.
; For example,
; 1*4HEXDIG denotes one to four HEXDIGs,
; *3DIGIT denotes up to three DIGITs, and
; 1*OCTET denotes one or more OCTETs.
; A single n prefix
; abbreviates n*n,
; e.g. 3DIGIT denotes three DIGITs.

; Instead of BNF's |, ABNF uses / to separate alternatives.
; Repetition prefixes have precedence over juxtapositions,
; which have precedence over /.
; Round brackets group things and override the aforementioned precedence rules,
; e.g. *(WSP / CRLF WSP) denotes sequences of terminals
; obtained by repeating, zero or more times,
; either (i) a WSP or (ii) a CRLF followed by a WSP.
; Square brackets also group things but make them optional,
; e.g. [":" port] is equivalent to 0*1(":" port).

; Instead of BNF's ::=, ABNF uses = to define nonterminals,
; and =/ to incrementally add alternatives
; to previously defined nonterminals.
; For example, the rule BIT = "0" / "1"
; is equivalent to BIT = "0" followed by BIT =/ "1".

; The syntax of ABNF itself is formally specified in ABNF
; (in Section 4 of the aforementioned RFC 5234,
; after the syntax and semantics of ABNF
; are informally specified in natural language
; (in Sections 1, 2, and 3 of the aforementioned RFC 5234).
; The syntax rules of ABNF prescribe the ASCII codes allowed for
; white space (spaces and horizontal tabs),
; line endings (carriage returns followed by line feeds),
; and comments (semicolons to line endings).

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Structure
; ---------

; This ABNF grammar consists of two (sub-)grammars:
; (i) a lexical grammar that describes how
; sequence of characters are parsed into tokens, and
; (ii) a syntactic grammar that described how
; tokens are parsed into expressions, statements, etc.
; The adjectives 'lexical' and 'syntactic' are
; the same ones used in the Java language reference,
; for instance;
; alternative terms may be used in other languages,
; but the separation into these two components is quite common
; (the situation is sometimes a bit more complex, with multiple passes,
; e.g. Unicode escape processing in Java).

; This separation enables
; concerns of white space, line endings, etc.
; to be handled by the lexical grammar,
; with the syntactic grammar focused on the more important structure.
; Handling both aspects in a single grammar may be unwieldy,
; so having two grammars provides more clarity and readability.

; ABNF is a context-free grammar notation, with no procedural interpretation.
; The two grammars conceptually define two subsequent processing phases,
; as detailed below.
; However, a parser implementation does not need to perform
; two strictly separate phases (in fact, it typically does not),
; so long as it produces the same final result.

; The grammar is accompanied by some extra-grammatical requirements,
; which are not conveniently expressible in a context-free grammar like ABNF.
; These requirements are needed to make the grammar unambiguous,
; i.e. to ensure that, for each sequence of terminals,
; there is exactly one parse tree for that sequence terminals
; that satisfies not only the grammar rules
; but also the extra-grammatical requirements.
; These requirements are expressed as comments in this file.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Operator Precedence
; -------------------

; We formulate the grammar rules for expressions
; in a way that describes the relative precedence of operators,
; as often done in language syntax specifications.

; For instance, consider the rules
;
;  multiplicative-expression =
;          exponential-expression
;        / multiplicative-expression "*" exponential-expression
;        / multiplicative-expression "/" exponential-expression
;
;  additive-expression =
;          multiplicative-expression
;        / additive-expression "+" multiplicative-expression
;        / additive-expression "-" multiplicative-expression
;
; These rules tell us
; that the additive operators '+' and '-' have lower precedence
; than the multiplicative operators '*' and '/',
; and that both the additive and multiplicative operators associate to the left.
; This may be best understood via the examples given below.

; According to the rules, the expression
;
;  x + y * z
;
; can only be parsed as
;
;    +
;   / \
;  x   *
;     / \
;    y   z
;
; and not as
;
;      *
;     / \
;    +   z
;   / \
;  x   y
;
; because a multiplicative expression cannot have an additive expression
; as first sub-expression, as it would in the second tree above.

; Also according to the rules, the expression
;
;  x + y + z
;
; can only be parsed as
;
;      +
;     / \
;    +   z
;   / \
;  x   y
;
; and not as
;
;    +
;   / \
;  x   +
;     / \
;    y   z
;
; because an additive expression cannot have an additive expression
; as second sub-expression, as it would in the second tree above.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Naming Convention
; -----------------

; This ABNF grammar uses nonterminal names
; that consist of complete English words, separated by dashes,
; and that describe the construct the way it is in English.
; For instance, we use the name 'conditional-statement'
; to describe conditional statements.

; At the same time, this grammar establishes
; a precise and official nomenclature for the Leo constructs,
; by way of the nonterminal names that define their syntax.
; For instance, the rule
;
;  group-literal = product-group-literal
;                / affine-group-literal
;
; tells us that there are two kinds of group literals,
; namely product group literals and affine group literals.
; This is more precise than describing them as
; integers (which are not really group elements per se),
; or points (they are all points, just differently specified),
; or being singletons vs. pairs (which is a bit generic).

; The only exception to the nomenclature-establishing role of the grammar
; is the fact that, as discussed above,
; we write the grammar rules in a way that determines
; the relative precedence and the associativity of expression operators,
; and therefore we have rules like
;
;  unary-expression = primary-expression
;                   / "!" unary-expression
;                   / "-" unary-expression
;
; In order to allow the recursion of the rule to stop,
; we need to regard, in the grammar, a primary expression as a unary expression
; (i.e. a primary expression is also a unary expression in the grammar;
; but note that the opposite is not true).
; However, this is just a grammatical artifact:
; ontologically, a primary expression is not really a unary expression,
; because a unary expression is one that consists of
; a unary operator and an operand sub-expression.
; These terminological exceptions should be easy to identify in the rules.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Lexical Grammar
; ---------------

; A Leo file is a finite sequence of Unicode characters,
; represented as Unicode code points,
; which are numbers in the range form 0 to 10FFFFh.
; These are captured by the ABNF rule 'character' below.

; The lexical grammar defines how, at least conceptually,
; the sequence of characters is turned into
; a sequence of tokens, comments, and whitespaces:
; these entities are all defined by the grammar rules below.

; As stated, the lexical grammar alone is ambiguous.
; For example, the sequence of characters '**' (i.e. two stars)
; could be equally parsed as two '*' symbol tokens or one '**' symbol token
; (see rule for 'symbol' below).
; As another example, the sequence or characters '<CR><LF>'
; (i.e. carriage return followed by line feed)
; could be equally parsed as two line terminators or one
; (see rule for 'newline').

; Thus, as often done in language syntax definitions,
; the lexical grammar is disambiguated by
; the extra-grammatical requirement that
; the longest possible sequence of characters is always parsed.
; This way, '**' must be parsed as one '**' symbol token,
; and '<CR><LF>' must be parsed as one line terminator.

; As mentioned above, a character is any Unicode code point.
; This grammar does not say how those are encoded in files (e.g. UTF-8):
; it starts with a decoded sequence of Unicode code points.
; Note that we allow any value,
; even though some values may not be used according to the Unicode standard.

character = %x0-10FFFF   ; any Unicode code point

; We give names to certain ASCII characters.

horizontal-tab = %x9

line-feed = %xA

carriage-return = %xD

space = %x20

double-quote = %x22

; We give names to complements of certain ASCII characters.
; These consist of all the Unicode characters except for one or two.

not-double-quote = %x0-22 / %x24-10FFFF   ; anything but "

not-star = %x0-29 / %x2B-10FFFF   ; anything but *

not-line-feed-or-carriage-return = %x0-9 / %xB-C / %xE-10FFFF
                                   ; anything but LF or CR

not-star-or-slash = %x0-29 / %x2B-2E / %x30-10FFFF   ; anything but * or /

; Lines in Leo may be terminated via
; a single carriage return,
; a line feed,
; or a carriage return immediately followed by a line feed.
; Note that the latter combination constitutes a single line terminator,
; according to the extra-grammatical requirement of the longest sequence,
; described above.

newline = line-feed / carriage-return / carriage-return line-feed

; Line terminators form whitespace, along with spaces and horizontal tabs.

whitespace = space / horizontal-tab / newline

; There are two kinds of comments in Leo, as in other languages.
; One is block comments of the form '/* ... */',
; and the other is end-of-line comments of the form '// ...'.
; The first kind start at '/*' and end at the first '*/',
; possibly spanning multiple (partial) lines;
; these do no nest.
; The second kind start at '//' and extend till the end of the line.
; The rules about comments given below are similar to
; the ones used in the Java language reference.

comment = block-comment / end-of-line-comment

block-comment = "/*" rest-of-block-comment

rest-of-block-comment = "*" rest-of-block-comment-after-star
                      / not-star rest-of-block-comment

rest-of-block-comment-after-star = "/"
                                 / "*" rest-of-block-comment-after-star
                                 / not-star-or-slash rest-of-block-comment

end-of-line-comment = "//" *not-line-feed-or-carriage-return newline

; Below are the keywords in the Leo language.
; They cannot be used as identifiers.

keyword = %s"address"
        / %s"as"
        / %s"bool"
        / %s"circuit"
        / %s"console"
        / %s"const"
        / %s"else"
        / %s"false"
        / %s"field"
        / %s"for"
        / %s"function"
        / %s"group"
        / %s"i8"
        / %s"i16"
        / %s"i32"
        / %s"i64"
        / %s"i128"
        / %s"if"
        / %s"import"
        / %s"in"
        / %s"input"
        / %s"let"
        / %s"mut"
        / %s"return"
        / %s"Self"
        / %s"self"
        / %s"static"
        / %s"string"
        / %s"true"
        / %s"u8"
        / %s"u16"
        / %s"u32"
        / %s"u64"
        / %s"u128"

; The following rules define (ASCII) digits
; and (uppercase and lowercase) letters.

digit = %x30-39   ; 0-9

uppercase-letter = %x41-5A   ; A-Z

lowercase-letter = %x61-7A   ; a-z

letter = uppercase-letter / lowercase-letter

; An identifier is a non-empty sequence of letters, digits, and underscores,
; starting with a letter.
; It must not be a keyword: this is an extra-grammatical constraint.

identifier = letter *( letter / digit / "_" )   ; but not a keyword

; A package name consists of one or more segments separated by single dashes,
; where each segment is a non-empty sequence of lowercase letters and digits.

package-name = 1*( lowercase-letter / digit )
               *( "-" 1*( lowercase-letter / digit ) )

; An address starts with 'aleo1'
; and continues with exactly 58 lowercase letters and digits.
; Thus an address always consists of 63 characters.

address = %s"aleo1" 58( lowercase-letter / digit )

; A formatted string is a sequence of characters, other than double quote,
; surrounded by double quotes.
; Within a formatted string, sub-strings '{}' are distinguished as containers
; (these are the ones that may be matched with values
; whose textual representation replaces the containers
; in the printed string).
; There is an implicit extra-grammatical requirements that
; the explicit 'formatted-string-container' instances include
; all the occurrences of '{}' in the parsed character sequence:
; that is, there may not be two contiguous 'not-double-quote' instances
; that are '{' and '}'.

formatted-string-container = "{}"

formatted-string = double-quote
                   *( not-double-quote / formatted-string-container )
                   double-quote

; Here is (part of this ABNF comment),
; an alternative way to specify formatted strings,
; which captures the extra-grammatical requirement above in the grammar,
; but is more complicated:
;
;  not-double-quote-or-open-brace = %x0-22 / %x24-7A / %x7C-10FFFF
;
;  not-double-quote-or-close-brace = %x0-22 / %x24-7C / %x7E-10FFFF
;
;  formatted-string-element = not-double-quote-or-open-brace
;                           / "{" not-double-quote-or-close-brace
;                           / formatted-string-container
;
;  formatted-string = double-quote *formatted-string-element double-quote
;
; It is not immediately clear which approach is better; there are tradeoffs.
; We may choose to adopt this one in future revisions of the grammar.

; Annotations have names, which are identifiers immediately preceded by '@'.

annotation-name = "@" identifier

; A natural (number) is a sequence of one or more digits.
; We allow leading zeros, e.g. '007'.

natural = 1*digit

; An integer (number) is either a natural or its negation.
; We allow leading zeros also in negative numbers, e.g. '-007'.

integer = [ "-" ] natural

; An untyped literal is just an integer.

untyped-literal = integer

; Unsigned literals are naturals followed by unsigned types.

unsigned-literal = natural ( %s"u8" / %s"u16" / %s"u32" / %s"u64" / %s"u128" )

; Signed literals are integers followed by signed types.

signed-literal = integer ( %s"i8" / %s"i16" / %s"i32" / %s"i64" / %s"i128" )

; Field literals are integers followed by the type of field elements.

field-literal = integer %s"field"

; There are two kinds of group literals.
; One is a single integer followed by the type of group elements,
; which denotes the scalar product of the generator point by the integer.
; The other kind is not a token because it allows some whitespace inside;
; therefore, it is defined in the syntactic grammar.

product-group-literal = integer %s"group"

; Boolean literals are the usual two.

boolean-literal = %s"true" / %s"false"

; An address literal is an address wrapped into an indication of address,
; to differentiate it from an identifier.

address-literal = %s"address" "(" address ")"

; The ones above are all the atomic literals
; (in the sense that they are tokens, without whitespace allowed in them),
; as defined by the following rule.

atomic-literal = untyped-literal
               / unsigned-literal
               / signed-literal
               / field-literal
               / product-group-literal
               / boolean-literal
               / address-literal

; After defining the (mostly) alphanumeric tokens above,
; it remains to define tokens for non-alphanumeric symbols such as "+" and "(".
; Different programming languages used different terminologies for these,
; e.g. operators, separators, punctuators, etc.
; Here we use 'symbol', for all of them.
; We also include a token consisting of
; a closing parenthesis immediately followed by 'group':
; as defined in the syntactic grammar,
; this is the final part of an affine group literal;
; even though it includes letters,
; it seems appropriate to still consider it a symbol,
; particularly since it starts with a proper symbol.

; We could give names to all of these symbols,
; via rules such as
;
;  equality-operator = "=="
;
; and defining 'symbol' in terms of those
;
;  symbol = ... / equality-operator / ...
;
; This may or may not make the grammar more readable,
; but it would help establish a terminology in the grammar,
; namely the exact names of some of these token.
; On the other hand, at least some of them are perhaps simple enough
; that they could be just described in terms of their symbols,
; e.g. 'double dot', 'question mark', etc.

symbol = "!" / "&&" / "||"
       / "==" / "!="
       / "<" / "<=" / ">" / ">="
       / "+" / "-" / "*" / "/" / "**"
       / "=" / "+=" / "-=" / "*=" / "/=" / "**="
       / "(" / ")"
       / "[" / "]"
       / "{" / "}"
       / "," / "." / ".." / "..." / ";" / ":" / "::" / "?"
       / "->" / "_"
       / %s")group"

; Everything defined above, other than comments and whitespace,
; is a token, as defined by the following rule.

token = keyword
      / identifier
      / atomic-literal
      / package-name
      / formatted-string
      / annotation-name
      / symbol

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Syntactic Grammar
; -----------------

; The processing defined by the lexical grammar above
; turns the initial sequence of characters
; into a sequence of tokens, comments, and whitespaces.
; The purpose of comments and whitespaces, from a syntactic point of view,
; is just to separate tokens:
; they are discarded, leaving a sequence of tokens.
; The syntactic grammar describes how to turn
; a sequence of tokens into concrete syntax trees.

; There are unsigned and signed integer types, for five sizes.

unsigned-type = %s"u8" / %s"u16" / %s"u32" / %s"u64" / %s"u128"

signed-type = %s"i8" / %s"i16" / %s"i32" / %s"i64" / %s"i128"

integer-type = unsigned-type / signed-type

; The integer types, along with the field and group types,
; for the arithmetic types, i.e. the ones that support arithmetic operations.

field-type = %s"field"

group-type = %s"group"

arithmetic-type = integer-type / field-type / group-type

; The arithmetic types, along with the boolean and address types,
; form the scalar types, i.e. the ones whose values do not contain (sub-)values.

boolean-type = %s"bool"

address-type = %s"address"

scalar-type =  boolean-type / arithmetic-type / address-type

; Circuit types are denoted by identifiers and the keyword 'Self'.
; The latter is only allowed inside a circuit definition,
; to denote the circuit being defined.

self-type = %s"Self"

circuit-type = identifier / self-type

; A tuple type consists of zero, two, or more component types.

tuple-type = "(" [ type 1*( "," type ) ] ")"

; An array type consists of an element type
; and an indication of dimensions.
; There is either a single dimension,
; or a tuple of one or more dimensions.

array-type = "[" type ";" array-dimensions "]"

array-dimensions = natural
                 / "(" natural *( "," natural ) ")"

; Circuit, tuple, and array types form the aggregate types,
; i.e. types whose values contain (sub-)values
; (with the corner-case exception of the empty tuple value).

aggregate-type = tuple-type / array-type / circuit-type

; Scalar and aggregate types form all the types.

type = scalar-type / aggregate-type

; The lexical grammar given earlier defines product group literals.
; The other kind of group literal is a pair of integer coordinates,
; which are reduced modulo the prime to identify a point,
; which must be on the elliptic curve.
; It is also allowed to omit one coordinate (not both),
; with an indication of how to fill in the missing coordinate
; (i.e. sign high, sign low, or inferred).
; This is an affine group literal,
; because it consists of affine point coordinates.

group-coordinate = integer / "+" / "-" / "_"

affine-group-literal = "(" group-coordinate "," group-coordinate %s")group"

; A literal is either an atomic one or an affine group literal.

literal = atomic-literal / affine-group-literal

; The following rule is not directly referenced in the rules for expressions
; (which reference 'literal' instead),
; but it is useful to establish terminology:
; a group literal is either a product group literal or an affine group literal.

group-literal = product-group-literal / affine-group-literal

; As often done in grammatical language syntax specifications,
; we define rules for different kinds of expressions,
; which also defines the relative precedence
; of operators and other expression constructs,
; and the (left or right) associativity of binary operators.

; The primary expressions are self-contained in a way,
; i.e. they have clear deliminations:
; Some consist of single tokens,
; while others have explicit endings.
; Primary expressions also include parenthesized expressions,
; i.e. any expression may be turned into a primary one
; by putting parentheses around it.

primary-expression = identifier
                   / %s"self"
                   / %s"input"
                   / literal
                   / "(" expression ")"
                   / tuple-expression
                   / array-expression
                   / circuit-expression

; Tuple expressions construct tuples.
; Each consists of zero, two, or more component expressions.

tuple-construction = "(" [ expression 1*( "," expression ) ] ")"

tuple-expression = tuple-construction

; Array expressions construct arrays.
; There are two kinds:
; one lists the element expressions (at least one),
; including spreads (via '...') which are arrays being spliced in;
; the other repeats (the value of) a single expression
; across one or more dimensions.

array-inline-construction = "["
                            array-inline-element
                            *( "," array-inline-element )
                            "]"

array-inline-element = expression / "..." expression

array-repeat-construction = "[" expression ";" array-dimensions "]"

array-construction = array-inline-construction / array-repeat-construction

array-expression = array-construction

; Circuit expressions construct circuit values.
; Each lists values for all the member variables (in any order);
; there must be at least one member variable.
; A single identifier abbreviates
; a pair consisting of the same identifier separated by colon;
; note that, in the expansion, the left one denotes a member name,
; while the right one denotes an expression (a variable),
; so they are syntactically identical but semantically different.

circuit-construction = circuit-type "{"
                       circuit-inline-element *( "," circuit-inline-element )
                       "}"

circuit-inline-element = identifier ":" expression / identifier

circuit-expression = circuit-construction

; After primary expressions, postfix expressions have highest precedence.
; They apply to primary expressions, and recursively to postfix expressions.

; There are postfix expressions to access parts of aggregate values.
; A tuple access selects a component by index (zero-based).
; There are two kinds of array accesses:
; one selects a single element by index (zero-based);
; the other selects a range via two indices,
; the first inclusive and the second exclusive --
; both are optional,
; the first defaulting to 0 and the second to the array length.
; A circuit access selects a member variable by name.

; Function calls are also postfix expressions.
; There are three kinds of function calls:
; top-level function calls,
; instance (i.e. non-static) member function calls, and
; static member function calls.
; What changes is the start, but they all end in an argument list.

function-arguments = "(" [ expression *( "," expression ) ] ")"

postfix-expression = primary-expression
                   / postfix-expression "." natural
                   / postfix-expression "." identifier
                   / identifier function-arguments
                   / postfix-expression "." identifier function-arguments
                   / circuit-type "::" identifier function-arguments
                   / postfix-expression "[" expression "]"
                   / postfix-expression "[" [expression] ".." [expression] "]"

; Unary operators have the highest operator precedence.
; They apply to postfix expressions,
; and recursively to unary expressions.

unary-expression = postfix-expression
                 / "!" unary-expression
                 / "-" unary-expression

; Next in the operator precedence is casting.

cast-expression = unary-expression
                / cast-expression %s"as" type

; Next in the operator precedence is exponentiation,
; following mathematical practice.
; The current rule below makes exponentiation left-associative,
; i.e. 'a ** b ** c' must be parsed as '(a ** b) ** c'.

exponential-expression = cast-expression
                       / exponential-expression "**" cast-expression

; Next in precedence come multiplication and division, both left-associative.

multiplicative-expression = exponential-expression
                          / multiplicative-expression "*" exponential-expression
                          / multiplicative-expression "/" exponential-expression

; Then there are addition and subtraction, both left-assocative.

additive-expression = multiplicative-expression
                    / additive-expression "+" multiplicative-expression
                    / additive-expression "-" multiplicative-expression

; Next in the precedence order are ordering relations.
; These are not associative, because they return boolean values.

ordering-expression = additive-expression
                    / additive-expression "<" additive-expression
                    / additive-expression ">" additive-expression
                    / additive-expression "<=" additive-expression
                    / additive-expression ">=" additive-expression

; Equalities return booleans but may also operate on booleans;
; the rule below makes them left-associative.

equality-expression = ordering-expression
                    / equality-expression "==" ordering-expression
                    / equality-expression "!=" ordering-expression

; Next come conjunctive expressions, left-associative.

conjunctive-expression = equality-expression
                       / conjunctive-expression "&&" equality-expression

; Next come disjunctive expressions, left-associative.

disjunctive-expression = conjunctive-expression
                       / disjunctive-expression "||" conjunctive-expression

; Finally we have conditional expressions.

conditional-expression = disjunctive-expression
                       / conditional-expression
                         "?" expression
                         ":" conditional-expression

; Those above are all the expressions.
; Recall that conditional expressions
; may be disjunctive expressions,
; which may be conjunctive expressions,
; and so on all the way to primary expressions.

expression = conditional-expression

; There are various kinds of statements, including blocks.
; Blocks are possibly empty sequences of statements surrounded by curly braces.

statement = expression-statement
          / return-statement
          / variable-definition-statement
          / conditional-statement
          / loop-statement
          / assignment-statement
          / console-statement
          / block

block = "{" *statement "}"

; An expression (that must return the empty tuple, as semantically required)
; can be turned into a statement by appending a semicolon.

expression-statement = expression ";"

; A return statement always takes an expression,
; and does not end with a semicolon.

return-statement = %s"return" expression

; There are two kinds of variable definition statements,
; which only differ in the starting keyword.
; The variables are either a single one or a tuple of two or more;
; in all cases, there is just one optional type
; and just one initializing expression.

variable-definition-statement = ( %s"let" / %s"const" )
                                identifier-or-identifiers
                                [ ":" type ] "=" expression ";"

identifier-or-identifiers = identifier
                          / "(" identifier 1*( "," identifier ) ")"

; A conditional statement always starts with a condition and a block
; (which together form a branch).
; It may stop there, or it may continue with an alternative block,
; or possibly with another conditional statement, forming a chain.
; Note that blocks are required in all branches, not merely statements.

branch = %s"if" expression block

conditional-statement = branch
                      / branch %s"else" block
                      / branch %s"else" conditional-statement

; A loop statement implicitly defines a loop variable
; that goes from a starting value (inclusive) to an ending value (exclusive).
; The body is a block.

loop-statement = %s"for" identifier %s"in" expression ".." expression block

; An assignment statement is straightforward.
; Based on the operator, the assignment may be simple (i.e. '=')
; or compound (i.e. combining assignment with an arithmetic operation).

assignment-operator = "=" / "+=" / "-=" / "*=" / "/=" / "**="

assignment-statement = expression assignment-operator expression ";"

; Console statements start with the 'console' keyword,
; followed by a console function call.
; The call may be an assertion or a print command.
; The former takes an expression (which must be boolean) as argument.
; The latter takes either no argument,
; or a formatted string followed by expressions,
; whose number must match the number of containers '{}' in the formatted string.
; Note that the console function names are identifiers, not keywords.
; There are three kinds of print commands.

console-statement = %s"console" "." console-call

console-call = assert-call
             / print-call

assert-call = %s"assert" "(" expression ")"

print-function = %s"debug" / %s"error" / %s"log"

print-arguments = "(" [ formatted-string *( "," expression ) ] ")"

print-call = print-function print-arguments

; An annotation consists of an annotation name (which starts with '@')
; with optional annotation arguments, which are identifiers.
; Note that no parentheses are used if there are no arguments.

annotation = annotation-name
             [ "(" identifier *( "," identifier ) ")" ]

; A function declaration defines a function.
; The output type is optional, defaulting to the empty tuple type.
; In general, a function input consists of an identifier and a type,
; with an optional 'const' modifier.
; Additionally, functions inside circuits
; may start with a 'mut self' or 'const self' or 'self' parameter.
; Furthermore, any function may end with an 'input' parameter.

function-declaration = *annotation %s"function" identifier
                       "(" [ function-parameters ] ")" [ "->" type ]
                       block

function-parameters = self-parameter [ "," input-parameter ]
                    / self-parameter "," function-inputs [ "," input-parameter ]
                    / function-inputs [ "," input-parameter ]
                    / input-parameter

self-parameter = [ %s"mut" / %s"const" ] %s"self"

function-inputs = function-input *( "," function-input )

function-input = [ %s"const" ] identifier ":" type

input-parameter = %s"input"

; A circuit member variable declaration consists of an identifier and a type.
; A circuit member function declaration consists of a function declaration.

member-declaration = member-variable-declaration
                   / member-function-declaration

member-variable-declaration = identifier ":" type

member-function-declaration = function-declaration

; A circuit declaration defines a circuit type,
; as consisting of member variables and functions.

circuit-declaration = *annotation %s"circuit" identifier
                      "{" member-declaration *( "," member-declaration ) "}"

; An import declaration consists of the 'import' keyword
; followed by a package path, which may be one of the following:
; a single wildcard;
; an identifier, optionally followed by a local renamer;
; a package name followed by a path, recursively;
; or a parenthesized list of package paths,
; which are "fan out" of the initial path.
; Note that we allow the last element of the parenthesized list
; to be followed by a comma, for convenience.

import-declaration = %s"import" package-path

package-path = "*"
             / identifier [ %s"as" identifier ]
             / package-name "." package-path
             / "(" package-path *( "," package-path ) [","] ")"

; Finally, we define a file as a sequence of zero or more declarations.

declaration = import-declaration
            / function-declaration
            / circuit-declaration

file = *declaration