BNF Grammar

In the Sail language documentation, the term BNF Grammar designates the formal Backus-Naur Form grammar that specifies the concrete surface syntax of Sail. The grammar is presented as a sequence of productions (::=) covering lexical rules, type-level constructs, expression-level constructs, patterns, and the top-level definitions that constitute a Sail specification.

Lexical and Identifier Productions

The grammar defines identifiers and operators as follows:

<id> ::= ID
       | operator OPERATOR
       | operator -
       | operator |
       | operator ^
       | operator *

<op_no_caret> ::= OPERATOR
                | -
                | |
                | *
                | in

<op> ::= OPERATOR
       | -
       | |
       | ^
       | *
       | in

<exp_op> ::= OPERATOR
           | -
           | |
           | @
           | ::
           | ^
           | *

<pat_op> ::= @
           | ::
           | ^

Types, Kinds, Quantifiers, and Effects

The type-level productions describe type variables, type arguments, prefix/postfix operators, infix types, atomic types, type lists, kinds, type quantifiers, effects, effect sets, and type schemas.

<typ_var> ::= TYPE_VARIABLE

<tyarg> ::= ( <typ_list> )

<prefix_typ_op> ::= epsilon
                  | 2^
                  | -
                  | *

<postfix_typ> ::= <atomic_typ>

<typ_no_caret> ::= <prefix_typ_op> <postfix_typ> (<op_no_caret> <prefix_typ_op> <postfix_typ>)*

<typ> ::= if <infix_typ> then <infix_typ> else <typ>
        | <infix_typ>

<infix_typ> ::= <prefix_typ_op> <postfix_typ> (<op> <prefix_typ_op> <postfix_typ>)*

<atomic_typ> ::= <id>
               | _
               | <typ_var>
               | <lit>
               | dec
               | inc
               | <id> <tyarg>
               | register ( <typ> )
               | ( <typ> )
               | ( <typ> , <typ_list> )
               | { NUMBER (, NUMBER)* }
               | { <kopt> . <typ> }
               | { <kopt> , <typ> . <typ> }

<typ_list> ::= <typ> [,]
             | <typ> , <typ_list>

<kind> ::= Int
         | Type
         | Order
         | Bool

<kopt> ::= ( constant <typ_var> : <kind> )
         | ( <typ_var> : <kind> )
         | <typ_var>

<quantifier> ::= <kopt> , <typ>
             | <kopt>

<effect> ::= <id>

<effect_set> ::= { <effect> (, <effect>)* }
               | pure

<typschm> ::= <typ> -> <typ>
            | forall <quantifier> . <typ> -> <typ>
            | <typ> <-> <typ>
            | forall <quantifier> . <typ> <-> <typ>

Patterns and Literals

The pattern grammar includes atomic patterns, single and sequenced patterns, field patterns, and the literal forms.

<pat1> ::= <atomic_pat> (<pat_op> <atomic_pat>)*

<pat> ::= <pat1>
        | <attribute> <pat>
        | <pat1> as <typ>

<pat_list> ::= <pat> [,]
             | <pat> , <pat_list>

<atomic_pat> ::= _
               | <lit>
               | <id>
               | <typ_var>
               | <id> ()
               | <id> [ NUMBER ]
               | <id> [ NUMBER .. NUMBER ]
               | <id> ( <pat_list> )
               | <atomic_pat> : <typ_no_caret>
               | ( <pat> )
               | ( <pat> , <pat_list> )
               | [ <pat_list> ]
               | [| |]
               | [| <pat_list> |]
               | struct { <fpat> (, <fpat>)* }

<fpat> ::= <id> = <pat>
         | <id>
         | _

<lit> ::= true
        | false
        | ()
        | NUMBER
        | undefined
        | bitzero
        | bitone
        | BINARY_LITERAL
        | HEXADECIMAL_LITERAL
        | STRING_LITERAL

Expressions, Cases, and Blocks

The expression grammar covers atomic expressions, prefix/infix operators, full expressions, case clauses, blocks, let bindings, vector updates, attribute annotations, and function clause forms.

<exp> ::= <exp0>
        | <attribute> <exp>
        | <exp0> = <exp>
        | let <letbind> in <exp>
        | var <atomic_exp> = <exp> in <exp>
        | { <block> }
        | return <exp>
        | throw <exp>
        | if <exp> then <exp> else <exp>
        | if <exp> then <exp>
        | match <exp> { <case_list> }
        | try <exp> catch { <case_list> }
        | foreach ( <id> ID <atomic_exp> ID <atomic_exp> by <atomic_exp> in <typ> ) <exp>
        | foreach ( <id> ID <atomic_exp> ID <atomic_exp> by <atomic_exp> ) <exp>
        | foreach ( <id> ID <atomic_exp> ID <atomic_exp> ) <exp>
        | repeat [termination_measure { <exp> }] <exp> until <exp>
        | while [termination_measure { <exp> }] <exp> do <exp>

<prefix_op> ::= epsilon
              | 2^
              | -
              | *

<exp0> ::= <prefix_op> <atomic_exp> (<exp_op> <prefix_op> <atomic_exp>)*

<case> ::= <pat> => <exp>
         | <pat> if <exp> => <exp>

<case_list> ::= <case>
              | <case> ,
              | <case> , <case_list>

<block> ::= <exp> [;]
          | let <letbind> [;]
          | let <letbind> ; <block>
          | var <atomic_exp> = <exp> [;]
          | var <atomic_exp> = <exp> ; <block>
          | <exp> ; <block>

<letbind> ::= <pat> = <exp>

<atomic_exp> ::= <atomic_exp> : <atomic_typ>
               | <lit>
               | <id> -> <id> ()
               | <id> -> <id> ( <exp_list> )
               | <atomic_exp> . <id> ()
               | <atomic_exp> . <id> ( <exp_list> )
               | <atomic_exp> . <id>
               | <id>
               | <typ_var>
               | ref <id>
               | <id> ()
               | <id> ( <exp_list> )
               | sizeof ( <typ> )
               | constraint ( <typ> )
               | <atomic_exp> [ <exp> ]
               | <atomic_exp> [ <exp> .. <exp> ]
               | <atomic_exp> [ <exp> , <exp> ]
               | struct { <fexp_exp_list> }
               | { <exp> with <fexp_exp_list> }
               | [ ]
               | [ <exp_list> ]
               | [ <exp> with <vector_update_list> ]
               | [| |]
               | [| <exp_list> |]
               | ( <exp> )
               | ( <exp> , <exp_list> )

<fexp_exp> ::= <atomic_exp> = <exp>
             | <id>

<fexp_exp_list> ::= <fexp_exp>
                  | <fexp_exp> ,
                  | <fexp_exp> , <fexp_exp_list>

<exp_list> ::= <exp> [,]
             | <exp> , <exp_list>

<vector_update> ::= <atomic_exp> = <exp>
                  | <atomic_exp> .. <atomic_exp> = <exp>
                  | <id>

<vector_update_list> ::= <vector_update> [,]
                       | <vector_update> , <vector_update_list>

<attribute_data_key_value> ::= ID = <attribute_data>
                             | STRING_LITERAL = <attribute_data>

<attribute_data> ::= { [<attribute_data_key_value> (, <attribute_data_key_value>)*] }
                   | NUMBER
                   | STRING_LITERAL
                   | ID
                   | true
                   | false
                   | [ [<attribute_data> (, <attribute_data>)*] ]

<attribute> ::= $[ATTRIBUTE] ]
              | $[ATTRIBUTE] <attribute_data> ]

Function Clauses, Register Definitions, and Index Ranges

<funcl_annotation> ::= Private
                     | <attribute>

<funcl_patexp> ::= <pat> = <exp>
                 | ( <pat> if <exp> ) = <exp>

<funcl_patexp_typ> ::= <pat> = <exp>
                     | <pat> -> <typ> = <exp>
                     | forall <quantifier> . <pat> -> <typ> = <exp>
                     | ( <pat> if <exp> ) = <exp>
                     | ( <pat> if <exp> ) -> <typ> = <exp>
                     | forall <quantifier> . ( <pat> if <exp> ) -> <typ> = <exp>

<funcl> ::= <funcl_annotation> <id> <funcl_patexp>
          | <id> <funcl_patexp>

<funcls> ::= <funcl_annotation> <id> <funcl_patexp_typ>
           | <id> <funcl_patexp_typ>
           | <funcl_annotation> <id> <funcl_patexp> and <funcl> (and <funcl>)*
           | <id> <funcl_patexp> and <funcl> (and <funcl>)*

<funcl_typ> ::= forall <quantifier> . <typ>
              | <typ>

<paren_index_range> ::= ( <paren_index_range> @ <paren_index_range> (@ <paren_index_range>)* )
                      | <atomic_index_range>

<atomic_index_range> ::= <typ>
                       | <typ> .. <typ>
                       | ( <typ> .. <typ> )

<r_id_def> ::= <id> : <paren_index_range> (@ <paren_index_range>)*

<r_def_body> ::= <r_id_def>
               | <r_id_def> ,
               | <r_id_def> , <r_def_body>

Type, Struct, Enum, Union, and Bitfield Definitions

<param_kopt> ::= <typ_var> : <kind>
               | <typ_var>

<typaram> ::= ( <param_kopt> (, <param_kopt>)* ) , <typ>
            | ( <param_kopt> (, <param_kopt>)* )

<type_def> ::= type <id> <typaram> = <typ>
             | type <id> = <typ>
             | type <id> <typaram> -> <kind> = <typ>
             | type <id> : <kind> = <typ>
             | type <id> : <kind>
             | struct <id> = { <struct_fields> }
             | struct <id> <typaram> = { <struct_fields> }
             | enum <id> = <id> (| <id>)*
             | enum <id> = { <enum_comma> }
             | enum <id> with <enum_functions> = { <enum_comma> }
             | union <id> = { <type_unions> }
             | union <id> <typaram> = { <type_unions> }
             | bitfield <id> : <typ> = { <r_def_body> }

<enum_functions> ::= <id> -> <typ> , <enum_functions>
                   | <id> -> <typ> ,
                   | <id> -> <typ>

<enum_comma> ::= <id> [,]
         | <id> => <exp> [,]
         | <id> , <enum_comma>
         | <id> => <exp> , <enum_comma>

<struct_field> ::= <id> : <typ>

<struct_fields> ::= <struct_field>
                  | <struct_field> ,
                  | <struct_field> , <struct_fields>

<type_union> ::= Private <type_union>
               | <attribute> <type_union>
               | <id> : <typ>
               | <id> : { <struct_fields> }

<type_unions> ::= <type_union>
                | <type_union> ,
                | <type_union> , <type_unions>

Function Definitions, Patterns, and Mappings

<rec_measure> ::= { <pat> => <exp> }

<fun_def> ::= function [<rec_measure>] <funcls>

<mpat> ::= <atomic_mpat> (<pat_op> <atomic_mpat>)*
         | <atomic_mpat> as <id>

<atomic_mpat> ::= <lit>
                | <id>
                | <id> [ NUMBER ]
                | <id> [ NUMBER .. NUMBER ]
                | <id> ()
                | <id> ( <mpat> (, <mpat>)* )
                | ( <mpat> )
                | ( <mpat> , <mpat> (, <mpat>)* )
                | [ <mpat> (, <mpat>)* ]
                | [| |]
                | [| <mpat> (, <mpat>)* |]
                | <atomic_mpat> : <typ_no_caret>
                | struct { <fmpat> (, <fmpat>)* }

<fmpat> ::= <id> = <mpat>
          | <id>

<mpexp> ::= <mpat>
          | <mpat> if <exp>

<mapcl> ::= <attribute> <mapcl>
          | <mpexp> <-> <mpexp>
          | <mpexp> => <exp>
          | forwards <case>
          | backwards <case>

<mapcl_list> ::= <mapcl> [,]
               | <mapcl> , <mapcl_list>

<map_def> ::= mapping <id> = { <mapcl_list> }
            | mapping <id> : <typschm> = { <mapcl_list> }

Let, Extern, Value Specification, Register, and Default Definitions

<let_def> ::= let <letbind>

<pure_opt> ::= impure
             | pure

<extern_binding> ::= <id> : STRING_LITERAL
                   | _ : STRING_LITERAL

<externs> ::= epsilon
            | = STRING_LITERAL
            | = { <extern_binding> (, <extern_binding>)* }
            | = <pure_opt> STRING_LITERAL
            | = <pure_opt> { <extern_binding> (, <extern_binding>)* }

<val_spec_def> ::= val STRING_LITERAL : <typschm>
                 | val <id> <externs> : <typschm>

<register_def> ::= register <id> : <typ>
                 | register <id> : <typ> = <exp>

<default_def> ::= default <kind> inc
                | default <kind> dec

Scattered Definitions, Loop Measures, Instantiations, Overloads, and Top-Level Definitions

<scattered_def> ::= scattered enum <id>
                  | scattered union <id> <typaram>
                  | scattered union <id>
                  | scattered function <id>
                  | scattered mapping <id>
                  | scattered mapping <id> : <funcl_typ>
                  | enum clause <id> = <id>
                  | function clause <funcl>
                  | union clause <id> = <type_union>
                  | mapping clause <id> = <mapcl>
                  | end <id>

<loop_measure> ::= until <exp>
                 | repeat <exp>
                 | while <exp>

<subst> ::= <typ_var> = <typ>
          | <id> = <id>

<instantiation_def> ::= instantiation <id>
                      | instantiation <id> with <subst> (, <subst>)*

<overload_def> ::= overload <id> = { <id> (, <id>)* }
                 | overload <id> = <id> (| <id>)*

<def_aux> ::= <fun_def>
            | <map_def>
            | FIXITY_DEF
            | <val_spec_def>
            | <instantiation_def>
            | <type_def>
            | <let_def>
            | <register_def>
            | <overload_def>
            | <scattered_def>
            | <default_def>
            | constraint <typ>
            | $LINE_DIRECTIVE
            | termination_measure <id> <pat> = <exp>
            | termination_measure <id> <loop_measure> (, <loop_measure>)*

<def> ::= Private <def>
        | <attribute> <def>
        | <def_aux>

Role Within Sail

The BNF grammar is the authoritative reference for the surface syntax that the Sail toolchain accepts as input. It enumerates every production that downstream tools, including the [Sail ISA Specification Language], must parse and elaborates into semantics, type-checking, and code generation pipelines. Specific sub-grammars within this BNF correspond to identifiable concepts of the language, including [Type Variable], [Type Quantifier], [Kind Annotation], [Pattern Matching], [Expression Language], [Function Definition], [Mapping Definition], [Struct Type], [Enum Type], [Union Type], [Bitfield Type], [Register Type], [Overload Definition], [Scattered Definition], [Termination Measure], [Let Binding], [Attribute Annotation], [Value Specification], [Extern Binding], [Effect System], [Bitvector Literal], and [Vector Type].

Related Concepts Outside Sail

The use of a BNF grammar to pin down the syntax of a language is a standard formal-languages technique. In the broader literature, BNF grammars are also used to define the surface syntax of other declarative and executable languages, for example the BSL (boldsea Semantic Language) executable-ontology language. In addition, supplying a BNF grammar as part of the prompt context for large language models has been shown to substantially improve syntactic and structural validity when those models generate code in domain-specific languages.