verus.pest

//! A Verus grammar
//!
//! Explicitly ignores regions of the code that are outside the `verus!` macro.

// Useful documentation on Rust's grammar can be found in the Rust Reference manual, e.g.,
//   https://doc.rust-lang.org/reference/expressions.html

// Legend:
//
//    //!                - documentation comment, for the full grammar
//    ///                - documentation comment
//    //                 - comment
//    foo = { ... }      - regular rule
//    baz = @{ ... }     - atomic
//    bar = _{ ... }     - silent
//    qux = ${ ... }     - compound-atomic
//    #tag = ...         - tags
//    plugh = !{ ... }   - non-atomic
//    "abc"              - exact string
//    ^"abc"             - case insensitive
//    'a'..'z'           - character range
//    ANY                - any character
//    foo ~ bar          - sequence
//    baz | qux          - ordered choice
//    foo*               - zero or more
//    bar+               - one or more
//    baz?               - optional
//    qux{n}             - exactly n
//    qux{m, n}          - between m and n (inclusive)
//    &foo               - positive predicate
//    !bar               - negative predicate

//***********************//
// General common things //
//***********************//

/// Allowed whitespace between any tokens in the grammar; completely ignored when the parsing is
/// done (except in cases such as strings or comments)
WHITESPACE = _{
  " " | "\t" | NEWLINE
}

/// Multiple-newlines that can be collapsed into a single double-newline
///
/// Only supported on a subset of syntactic locations; anywhere else,
/// double-newlines are collapsed as if they were just normal whitespace.
MULTI_NEWLINE = @{
    (" " | "\t")* ~ NEWLINE ~ ((" " | "\t")* ~ NEWLINE)+ ~ (" " | "\t")*
}

/// Comment syntax; NOT ignored in the syntax tree that is parsed. Allowed to
/// exist between any tokens (except atomic tokens, of course).
COMMENT = @{
    // Outer docstring
    ("//!" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
    // Multiline comment
  | multiline_comment
    // Singleline comment
    //
    // NOTE: Inner docstrings `/// ...` are _explicitly_ disallowed from being
    // called a comment, and are handled separately via
    // `inner_docstring_comment`
  | (!"///" ~ "//" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
}

inner_docstring_comment = @{
    ("///" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
}

multiline_comment = @{
    "/*" ~ (multiline_comment | (!"*/" ~ ANY))* ~ "*/"
}

/// The entirety of a Verus source file
file = {
    SOI ~
    (non_verus ~ verus_macro_use)* ~
    non_verus? ~
    EOI
}

/// Region of code that doesn't contain any Verus macro use whatsoever.
///
/// Notice that we explicitly also first check for `macro_rules` (which is
/// marked non-atomic to break out of the atomic `non_verus`); this is because
/// someone might define a macro-rules macro _outside_ the verus! macro, but use
/// a verus! inside of the macro body itself, to generate Verus code; if that
/// happens, then we need to make sure that we aren't accidentally starting
/// parsing in the middle of the macro_rules macro body itself. Similarly, strings.
non_verus = @{
  (!("verus" ~ WHITESPACE* ~ "!" ~ WHITESPACE* ~ "{") ~ (macro_rules | string | raw_string | byte_string | raw_byte_string | COMMENT | ANY))*
}

/// An actual use of the `verus! { ... }` macro
verus_macro_use = ${
    "verus" ~ WHITESPACE* ~ "!" ~ WHITESPACE* ~ "{" ~ (WHITESPACE | COMMENT)* ~ verus_macro_body ~ (WHITESPACE | COMMENT)* ~ "}" ~ WHITESPACE* ~ ("//" ~ WHITESPACE* ~ "verus" ~ WHITESPACE* ~ "!")?
}

/// Anything inside the `verus! { ... }` macro
verus_macro_body = !{
    item*
}

/// A valid identifier, currently only supports ASCII-based identifiers, but
/// this probably should be extended in the future to correctly handle all
/// allowed identifiers.
identifier_string = @{
    (ASCII_ALPHA | "_") ~
    (ASCII_ALPHANUMERIC | "_")*
}

identifier = @{
    "r#" ~ identifier_string
  | !(keyword ~ !(ASCII_ALPHA | "_" | ASCII_ALPHANUMERIC)) ~ identifier_string
}

hex_number = @{
    "0x" ~ (ASCII_HEX_DIGIT | "_")+
}

decimal_number = @{
    ASCII_DIGIT ~ ("_" | ASCII_DIGIT)*
}

octal_number = @{
    "0o" ~ (ASCII_OCT_DIGIT | "_")+
}

binary_number = @{
    "0b" ~ ("0" | "1" | "_")+
}

int_number = @{
    (
        hex_number
      | octal_number
      | binary_number
      | decimal_number
    ) ~
    (
        "usize" | "u8" | "u16" | "u32" | "u64" | "u128"
      | "isize" | "i8" | "i16" | "i32" | "i64" | "i128"
      | "int"
      | "nat"
      | "real"
    )?
}

float_decimal = @{
    ASCII_DIGIT+ ~
    !".." ~ "." ~
    (ASCII_DIGIT | "_")* ~
    ("f32" | "f64" | "real")?
}

float_exp = @{
    (ASCII_DIGIT | "_")+ ~
    ("e" | "E") ~
    ("+" | "-")? ~
    "_"* ~
    ASCII_DIGIT ~   // Must have at least one digit
    (ASCII_DIGIT | "_")* ~
    ("f32" | "f64" | "real")?    
}

float_number = @{
    float_decimal | float_exp
}

lifetime_ident = @{
    "'" ~ ("_" | identifier | static_str)
}

/// A valid string, accounting for escaped quotes too.
string = @{
    "\"" ~ ("\\\"" | !"\"" ~ ANY)* ~ "\""
}

raw_string = @{
    "r" ~ PUSH("#"*) ~ "\""    // push the number signs onto the stack
    ~ raw_string_interior
    ~ "\"" ~ POP               // match a quotation mark and the number signs
}
raw_string_interior = {
    (
        !("\"" ~ PEEK)    // unless the next character is a quotation mark
                          // followed by the correct amount of number signs,
        ~ ANY             // consume one character
    )*
}

byte_string = @{
    "b" ~ string
}

raw_byte_string = @{
    "b" ~ raw_string
}

char = @{
    "'" ~ (
        ("\\u{" ~ ASCII_HEX_DIGIT+ ~ "}")
      | ("\\x" ~ ('0'..'7') ~ ASCII_HEX_DIGIT) // match rustfmt, only accepts the range [\x00-\x7f]
      | ("\\" ~ ANY)
      | (!"'" ~ ANY)
    ) ~
    "'"
}

byte = @{
    "b" ~ char
}

//***********************************************************//
// Fixed strings we want to preserve in the formatted output //
//***********************************************************//
amp_str = { "&" }
at_str = { "@" }
bang_str = { "!" }
colon_str = { ":" }
colons_str = { "::" }
comma_str = { "," }
dash_str = { "-" }
dollar_str = { "$" }
dot_str = { "." }
dot_dot_str = { ".." }
dot_dot_eq_str = { "..=" }
ellipses_str = { "..." }
eq_str = { "=" }
eq_eq_str = { "==" }
fatarrow_str = { "=>" }
langle_str = { "<" }
lbrace_str = { "{" }
lbracket_str = { "[" }
lparen_str = { "(" }
pipe_str = { "|" }
plus_str = { "+" }
pound_str = { "#" }
question_str = { "?" }
rangle_str = { ">" }
rarrow_str = { "->" }
rbrace_str = { "}" }
rbracket_str = { "]" }
rbracket_space_str = { "]" }
rparen_str = { ")" }
semi_str = { ";" }
star_str = { "*" }
tilde_str = { "~" }
triple_and = { "&&&" }
triple_or = { "|||" }
underscore_str = { "_" }
any_str = ${ "any" ~ !("_" | ASCII_ALPHANUMERIC) }
assert_space_str = ${ "assert" ~ !("_" | ASCII_ALPHANUMERIC) }
assert_str = ${ "assert" ~ !("_" | ASCII_ALPHANUMERIC) }
assume_str = ${ "assume" ~ !("_" | ASCII_ALPHANUMERIC) }
assume_specification_str = ${ "assume_specification" ~ !("_" | ASCII_ALPHANUMERIC) }
async_str = ${ "async" ~ !("_" | ASCII_ALPHANUMERIC) }
as_str = ${ "as" ~ !("_" | ASCII_ALPHANUMERIC) }
auto_str = ${ "auto" ~ !("_" | ASCII_ALPHANUMERIC) }
await_str = ${ "await" ~ !("_" | ASCII_ALPHANUMERIC) }
axiom_str = ${ "axiom" ~ !("_" | ASCII_ALPHANUMERIC) }
box_str = ${ "box" ~ !("_" | ASCII_ALPHANUMERIC) }
break_str = ${ "break" ~ !("_" | ASCII_ALPHANUMERIC) }
broadcast_str = ${ "broadcast" ~ !("_" | ASCII_ALPHANUMERIC) }
by_str = ${ "by" ~ !("_" | ASCII_ALPHANUMERIC) }
by_str_inline = ${ "by" ~ !("_" | ASCII_ALPHANUMERIC) }
calc_str = ${ "calc" ~ !("_" | ASCII_ALPHANUMERIC) }
checked_str = ${ "checked" ~ !("_" | ASCII_ALPHANUMERIC) }
choose_str = ${ "choose" ~ !("_" | ASCII_ALPHANUMERIC) }
closed_str = ${ "closed" ~ !("_" | ASCII_ALPHANUMERIC) }
const_str = ${ "const" ~ !("_" | ASCII_ALPHANUMERIC) }
const_nospace_str = ${ "const" ~ !("_" | ASCII_ALPHANUMERIC) }
continue_str = ${ "continue" ~ !("_" | ASCII_ALPHANUMERIC) }
crate_str = ${ "crate" ~ !("_" | ASCII_ALPHANUMERIC) }
decreases_str = ${ "decreases" ~ !("_" | ASCII_ALPHANUMERIC) }
default_ensures_str = ${ "default_ensures" ~ !("_" | ASCII_ALPHANUMERIC) }
default_str = ${ "default" ~ !("_" | ASCII_ALPHANUMERIC) }
do_str = ${ "do" ~ !("_" | ASCII_ALPHANUMERIC) }
dyn_str = ${ "dyn" ~ !("_" | ASCII_ALPHANUMERIC) }
else_str = ${ "else" ~ !("_" | ASCII_ALPHANUMERIC) }
ensures_str = ${ "ensures" ~ !("_" | ASCII_ALPHANUMERIC) }
returns_str = ${ "returns" ~ !("_" | ASCII_ALPHANUMERIC) }
enum_str = ${ "enum" ~ !("_" | ASCII_ALPHANUMERIC) }
exec_str = ${ "exec" ~ !("_" | ASCII_ALPHANUMERIC) }
exists_str = ${ "exists" ~ !("_" | ASCII_ALPHANUMERIC) }
extern_str = ${ "extern" ~ !("_" | ASCII_ALPHANUMERIC) }
f32_str = ${ "f32" ~ !("_" | ASCII_ALPHANUMERIC) }
f64_str = ${ "f64" ~ !("_" | ASCII_ALPHANUMERIC) }
false_str = ${ "false" ~ !("_" | ASCII_ALPHANUMERIC) }
FnMut_str = ${ "FnMut" ~ !("_" | ASCII_ALPHANUMERIC) }
FnOnce_str = ${ "FnOnce" ~ !("_" | ASCII_ALPHANUMERIC) }
FnSpec_str = ${ "FnSpec" ~ !("_" | ASCII_ALPHANUMERIC) }
Fn_str = ${ "Fn" ~ !("_" | ASCII_ALPHANUMERIC) }
final_str = ${ "final" ~ !("_" | ASCII_ALPHANUMERIC) }
fn_str = ${ "fn" ~ !("_" | ASCII_ALPHANUMERIC) }
forall_str = ${ "forall" ~ !("_" | ASCII_ALPHANUMERIC) }
for_str = ${ "for" ~ !("_" | ASCII_ALPHANUMERIC) }
ghost_str = ${ "ghost" ~ !("_" | ASCII_ALPHANUMERIC) }
global_str = ${ "global" ~ !("_" | ASCII_ALPHANUMERIC) }
group_str = ${ "group" ~ !("_" | ASCII_ALPHANUMERIC) }
has_str = ${ "has" ~ !("_" | ASCII_ALPHANUMERIC) }
i128_str = ${ "i128" ~ !("_" | ASCII_ALPHANUMERIC) }
i16_str = ${ "i16" ~ !("_" | ASCII_ALPHANUMERIC) }
i32_str = ${ "i32" ~ !("_" | ASCII_ALPHANUMERIC) }
i64_str = ${ "i64" ~ !("_" | ASCII_ALPHANUMERIC) }
i8_str = ${ "i8" ~ !("_" | ASCII_ALPHANUMERIC) }
if_str = ${ "if" ~ !("_" | ASCII_ALPHANUMERIC) }
implies_str = ${ "implies" ~ !("_" | ASCII_ALPHANUMERIC) }
impl_str = ${ "impl" ~ !("_" | ASCII_ALPHANUMERIC) }
int_str = ${ "int" ~ !("_" | ASCII_ALPHANUMERIC) }
invariant_ensures_str = ${ "invariant_ensures" ~ !("_" | ASCII_ALPHANUMERIC) }
invariant_except_break_str = ${ "invariant_except_break" ~ !("_" | ASCII_ALPHANUMERIC) }
invariant_str = ${ "invariant" ~ !("_" | ASCII_ALPHANUMERIC) }
in_str = ${ "in" ~ !("_" | ASCII_ALPHANUMERIC) }
isize_str = ${ "isize" ~ !("_" | ASCII_ALPHANUMERIC) }
is_str = ${ "is" ~ !("_" | ASCII_ALPHANUMERIC) }
layout_str = ${ "layout" ~ !("_" | ASCII_ALPHANUMERIC) }
let_str = ${ "let" ~ !("_" | ASCII_ALPHANUMERIC) }
loop_str = ${ "loop" ~ !("_" | ASCII_ALPHANUMERIC) }
macro_rules_str = ${ "macro_rules" ~ !("_" | ASCII_ALPHANUMERIC) }
macro_str = ${ "macro" ~ !("_" | ASCII_ALPHANUMERIC) }
matches_str = ${ "matches" ~ !("_" | ASCII_ALPHANUMERIC) }
match_str = ${ "match" ~ !("_" | ASCII_ALPHANUMERIC) }
mod_str = ${ "mod" ~ !("_" | ASCII_ALPHANUMERIC) }
move_str = ${ "move" ~ !("_" | ASCII_ALPHANUMERIC) }
mut_str = ${ "mut" ~ !("_" | ASCII_ALPHANUMERIC) }
nat_str = ${ "nat" ~ !("_" | ASCII_ALPHANUMERIC) }
none_str = ${ "none" ~ !("_" | ASCII_ALPHANUMERIC) }
no_unwind_str = ${ "no_unwind" ~ !("_" | ASCII_ALPHANUMERIC) }
no_unwind_when_str = ${ "when" ~ !("_" | ASCII_ALPHANUMERIC) }
opens_invariants_str = ${ "opens_invariants" ~ !("_" | ASCII_ALPHANUMERIC) }
open_str = ${ "open" ~ !("_" | ASCII_ALPHANUMERIC) }
proof_fn_str = ${ "proof_fn" ~ !("_" | ASCII_ALPHANUMERIC) }
proof_space_str = ${ "proof" ~ !("_" | ASCII_ALPHANUMERIC) }
proof_str = ${ "proof" ~ !("_" | ASCII_ALPHANUMERIC) }
pub_str = ${ "pub" ~ !("_" | ASCII_ALPHANUMERIC) }
raw_str = ${ "raw" ~ !("_" | ASCII_ALPHANUMERIC) }
recommends_str = ${ "recommends" ~ !("_" | ASCII_ALPHANUMERIC) }
ref_str = ${ "ref" ~ !("_" | ASCII_ALPHANUMERIC) }
requires_str = ${ "requires" ~ !("_" | ASCII_ALPHANUMERIC) }
return_str = ${ "return" ~ !("_" | ASCII_ALPHANUMERIC) }
r_str = ${ "r" ~ !("_" | ASCII_ALPHANUMERIC) }
Self_str = ${ "Self" ~ !("_" | ASCII_ALPHANUMERIC) }
self_str = ${ "self" ~ !("_" | ASCII_ALPHANUMERIC) }
seq_str = ${ "seq" ~ !("_" | ASCII_ALPHANUMERIC) }
sizeof_str = ${ "size_of" ~ !("_" | ASCII_ALPHANUMERIC) }
spec_fn_str = ${ "spec_fn" ~ !("_" | ASCII_ALPHANUMERIC) }
spec_str = ${ "spec" ~ !("_" | ASCII_ALPHANUMERIC) }
static_str = ${ "static" ~ !("_" | ASCII_ALPHANUMERIC) }
struct_str = ${ "struct" ~ !("_" | ASCII_ALPHANUMERIC) }
super_str = ${ "super" ~ !("_" | ASCII_ALPHANUMERIC) }
tracked_str = ${ "tracked" ~ !("_" | ASCII_ALPHANUMERIC) }
trait_str = ${ "trait" ~ !("_" | ASCII_ALPHANUMERIC) }
trigger_str = ${ "trigger" ~ !("_" | ASCII_ALPHANUMERIC) }
true_str = ${ "true" ~ !("_" | ASCII_ALPHANUMERIC) }
try_str = ${ "try" ~ !("_" | ASCII_ALPHANUMERIC) }
type_str = ${ "type" ~ !("_" | ASCII_ALPHANUMERIC) }
u128_str = ${ "u128" ~ !("_" | ASCII_ALPHANUMERIC) }
u16_str = ${ "u16" ~ !("_" | ASCII_ALPHANUMERIC) }
u32_str = ${ "u32" ~ !("_" | ASCII_ALPHANUMERIC) }
u64_str = ${ "u64" ~ !("_" | ASCII_ALPHANUMERIC) }
u8_str = ${ "u8" ~ !("_" | ASCII_ALPHANUMERIC) }
uninterp_str = ${ "uninterp" ~ !("_" | ASCII_ALPHANUMERIC) }
union_str = ${ "union" ~ !("_" | ASCII_ALPHANUMERIC) }
unsafe_str = ${ "unsafe" ~ !("_" | ASCII_ALPHANUMERIC) }
use_str = ${ "use" ~ !("_" | ASCII_ALPHANUMERIC) }
usize_str = ${ "usize" ~ !("_" | ASCII_ALPHANUMERIC) }
via_str = ${ "via" ~ !("_" | ASCII_ALPHANUMERIC) }
when_str = ${ "when" ~ !("_" | ASCII_ALPHANUMERIC) }
where_str = ${ "where" ~ !("_" | ASCII_ALPHANUMERIC) }
while_str = ${ "while" ~ !("_" | ASCII_ALPHANUMERIC) }
yeet_str = ${ "yeet" ~ !("_" | ASCII_ALPHANUMERIC) }
yield_str = ${ "yield" ~ !("_" | ASCII_ALPHANUMERIC) }

verusfmt_skip_attribute = {
    "#" ~ "[" ~ "verusfmt" ~ "::" ~ "skip"  ~ "]"
}

// See https://doc.rust-lang.org/reference/keywords.html
keyword = {
    // Strict
      as_str
    | break_str
    | const_str
    | continue_str
    | crate_str
    | else_str
    | enum_str
    | extern_str
    | false_str
    | fn_str
    | for_str
    | if_str
    | impl_str
    | in_str
    | let_str
    | loop_str
    | match_str
    | mod_str
    | move_str
    | mut_str
    | pub_str
    | ref_str
    | return_str
    | self_str
    | Self_str
    | static_str
    | struct_str
    | super_str
    | trait_str
    | true_str
    | type_str
    | unsafe_str
    | use_str
    | where_str
    | while_str
    | async_str
    | await_str
    | dyn_str
    
    // Reserved    
    | "abstract"
    | "become"
    | box_str
    | do_str
    | final_str
    | macro_str
    | "override"
    | "priv"
    | "typeof"
    | "unsized"
    | "virtual"
    | yield_str
    | try_str  
}

//*************************//
// Names, Paths and Macros //
//*************************//

name = { identifier | self_str }

// name_ref is used below in path_segments, which Rust says cannot
// contain numbers: https://doc.rust-lang.org/beta/reference/paths.html#paths-in-expressions
//name_ref = { identifier | int_number | self_str | super_str | crate_str | Self_str }
name_ref = { identifier | self_str | super_str | crate_str | Self_str }

lifetime = { lifetime_ident }
lifetime_no_space = { lifetime }  // A lifetime that shouldn't be followed by a space

path = { (path_segment ~ colons_str)* ~ path_segment }

// A version of path without supporting `a<x>`, to allow for proper parsing of
// clauses such as
//
//   requires foo < 3, foo > 0,
//
// See https://github.com/jaybosamiya/verusfmt/issues/19 for more details on
// what prompted this change.
path_no_generics = { (path_segment_no_generics ~ colons_str)* ~ path_segment_no_generics }

path_segment = {
    colons_str? ~ name_ref ~ generic_arg_list?
  | colons_str? ~ name_ref ~ param_list ~ ret_type?
  | colons_str? ~ name_ref
  | langle_str ~ path_segment_type ~ (as_str ~ path_segment_type)? ~ rangle_str
}

path_segment_no_generics = {
    colons_str? ~ name_ref ~ generic_arg_list_with_colons?
  | colons_str? ~ name_ref ~ param_list ~ ret_type?
  | colons_str? ~ name_ref
  | langle_str ~ path_segment_type ~ (as_str ~ path_segment_type)? ~ rangle_str
}

path_segment_type = {
    type
}

generic_args = {
    generic_arg ~ ("," ~ generic_arg)* ~ ","?
}

generic_arg_list = {
    colons_str? ~ langle_str ~ generic_args? ~ rangle_str
}

generic_arg_list_with_colons = {
    colons_str ~ langle_str ~ generic_args? ~ rangle_str
}

generic_arg = {
    generic_args_binding
  | type_arg
  | assoc_type_arg
  | lifetime_arg
  | const_arg
}

type_arg = {
    type
}

assoc_type_arg = {
    name_ref ~
    (generic_arg_list | param_list ~ ret_type?)? ~
    (colon_str ~ type_bound_list | (eq_str ~ type | const_arg))?
}

lifetime_arg = {
    lifetime_no_space
}

const_arg = {
    // Currently stable Rust only support literals as const args inside generic
    // args. In general, it could be arbitrary expressions, but that causes
    // headaches for parsing (in particular, we need to parse an `expr` that
    // does _not_ have a `>` sign in it, but our `expr` parsing greedily eats
    // any `>` that exists within it. Thus, for now, we simply restrict to
    // literals.
    literal
}

generic_args_binding = {
    identifier ~ eq_str ~ type
}

calc_macro_reln = {
    // We _could_ be more precise here but might as well just allow more things
    "(" ~ calc_macro_reln ~ ")"
  | bin_expr_ops_normal
}

calc_macro_body = {
    "{" ~
    calc_macro_reln ~
    (expr ~ semi_str ~ calc_macro_reln? ~ block_expr?)* ~
    "}"
}

calc_macro_call = {
    attr* ~ calc_str ~ bang_str ~
    calc_macro_body
}

seq_macro_call = {
    attr* ~ seq_str ~ bang_str ~
    lbracket_str ~ comma_delimited_exprs? ~ rbracket_str
}

// TODO: Special handling for the state_machine! macros?
macro_call = {
    calc_macro_call
  | seq_macro_call
  | attr* ~ path ~ bang_str ~ delim_token_tree
}

// NOTE: By convention, stmt-like or item-like macros (e.g., calc!{}) tend to
// use curly braces; this is only a convention though, and _technically_ one
// could use parens or square brackets for the same. However, we use this to
// disambiguate unknown macros when used in statement lists _without_
// semi-colons; if it is intended as an expr, the user better be using parens.
//
// Another alternative is to use `!(expr ~ "}") ~ macro_call` rather than
// `macro_call_stmt`, but as of now, I believe this to be a better choice; we
// can switch to the alternative if we find situations where it might be better
// suited.
macro_call_stmt = {
    calc_macro_call
  | attr* ~ path ~ bang_str ~ !"=" ~ lbrace_str ~ token_tree* ~ rbrace_str
}

// See https://doc.rust-lang.org/beta/reference/tokens.html#punctuation
punctuation = {
    bin_expr_ops
  | bang_str
  | triple_and 
  | triple_or
  | at_str
  | underscore_str
  | dot_str 
  | dot_dot_str
  | ellipses_str
  | dot_dot_eq_str
  | comma_str
  | semi_str
  | colon_str
  | colons_str
  | rarrow_str
  | fatarrow_str
  | pound_str
  | dollar_str
  | question_str
  | tilde_str
}

// See https://doc.rust-lang.org/beta/reference/tokens.html
token = {
    identifier
  | literal
  | lifetime_ident
  | keyword 
  | punctuation
}

delim_token_tree = {
      lparen_str ~ token_tree* ~ rparen_str
    | lbracket_str ~ token_tree* ~ rbracket_str
    | lbrace_str ~ token_tree* ~ rbrace_str
}

token_tree = {
    token | delim_token_tree
}

macro_items = {
    item*
}

macro_stmts = {
    stmt* ~ expr?
}

// Detected inside the formatter as a comma that should be followed by a space
spaced_comma_str = { comma_str }

global_sizeof = {
    sizeof_str ~ type ~ eq_eq_str ~ expr
}

spaced_is_str = { is_str }

global_layout = {
    layout_str ~ type ~ spaced_is_str ~ identifier ~ eq_eq_str ~ literal
    ~ (spaced_comma_str ~ identifier ~ eq_eq_str ~ literal)?
}

global_inner = _{
    global_sizeof
  | global_layout
}

global = {
    attr* ~
    global_str ~ global_inner ~ semi_str
}

//*************************//
//          Items          //
//*************************//

item_no_macro_call = _{
    const
  | enum
  | extern_block
  | extern_crate
  | assume_specification
  | fn
  | global
  | impl
  | macro_rules
  | macro_def
  | module
  | static
  | struct
  | trait
  | trait_alias
  | type_alias
  | union
  | use
  | broadcast_group
  | broadcast_uses
}

verusfmt_skipped_item = {
    item
}

item = {
    (attr* ~ verusfmt_skip_attribute ~ attr* ~ verusfmt_skipped_item)
  | item_no_macro_call
  | macro_call ~ semi_str?
}

/// Explicitly non-atomic rule (notice the '!'): this is so that it can be used
/// inside atomic rules, and still have the correct whitespace/comment behavior;
/// the atomic rule it is used for is `non_verus`.
macro_rules = !{
    attr* ~ visibility? ~
    macro_rules_str ~ bang_str ~ name ~
    token_tree
}

macro_def = {
    attr* ~ visibility? ~
    macro_str ~ name ~ token_tree? ~
    token_tree
}

module = {
    attr* ~ visibility? ~
    mod_str ~ name ~
    (item_list | semi_str)
}

item_list = {
    "{" ~ attr* ~ item* ~ "}"
}

extern_crate = {
    attr* ~ visibility? ~
    extern_str ~ crate_str ~ name_ref ~ rename? ~ semi_str
}

rename = {
    as_str ~ (name | underscore_str)
}

use = {
    attr* ~ visibility? ~
    use_str ~ use_tree ~ semi_str
}

use_tree = {
    (path? ~ colons_str)? ~ (star_str | use_tree_list)
  | path ~ rename?
}

use_tree_list = {
    "{" ~ (use_tree ~ ("," ~ use_tree)* ~ ","?)? ~ "}"
}

fn_qualifier = {
    (requires_clause | recommends_clause | ensures_clause | default_ensures_clause | returns_clause | decreases_clause | opens_invariants_clause | unwind_clause)*
}

fn_terminator = {
    fn_block_expr 
  | semi_str
}

fn = {
    attr* ~ visibility? ~ publish? ~
    default_str? ~ const_str? ~ async_str? ~ unsafe_str? ~ abi? ~ broadcast_str? ~ fn_mode? ~
    fn_str ~ name ~ generic_param_list? ~ param_list ~ ret_type? ~
    prover? ~ where_clause? ~
    fn_qualifier ~
    fn_terminator
}

assume_specification = {
    attr* ~
    visibility? ~
    assume_specification_str ~
    generic_param_list? ~
    lbracket_str ~ assume_specification_for ~ rbracket_str ~
    param_list? ~
    ret_type? ~
    where_clause? ~
    fn_qualifier ~
    semi_str
}

assume_specification_for = {
    path
}

abi = {
    extern_str ~ string?
}

param_list = {
    | "(" ~ ")"
    | "(" ~ self_param ~ ","? ~ ")"
    | "(" ~  (self_param ~ ",")? ~ param ~ ("," ~ param)* ~ ","? ~ ")"    
}

closure_param_list = {
    "|" ~ (param ~ ("," ~ param)* ~ ","?)? ~ "|"
}

self_param = {
    attr* ~ tracked_str? ~ (
        (amp_str ~ lifetime?)? ~ mut_str? ~ self_str
      | mut_str? ~ self_str ~ colon_str ~ type
    )
}

param = {
    attr* ~ (
        tracked_str? ~ pat_no_top_alt ~ (colon_str ~ type)?
        | type
        | ellipses_str
    )
}

ret_type = {
    rarrow_str ~ (lparen_str ~ tracked_str? ~ pat_no_top_alt ~ colon_str ~ type ~ rparen_str | tracked_str? ~ type)
}

type_alias = {
    attr* ~ visibility? ~
    default_str? ~
    type_str ~ name ~ generic_param_list? ~ (colon_str ~ type_bound_list)? ~ where_clause? ~
    (eq_str ~ type)? ~ semi_str
}

struct = {
    attr* ~ visibility? ~ data_mode? ~
    struct_str ~ name ~ generic_param_list? ~ (
        where_clause? ~ (record_field_list | semi_str)
      | tuple_field_list ~ where_clause? ~ semi_str
    )
}

// Each record must have its own line
record_field_list = {
    "{" ~ (record_field ~ ("," ~ record_field)* ~ ","?)? ~ "}"
}

// Records may be condensed onto a single line if sufficiently short
condensable_record_field_list = {
    "{" ~ (record_field ~ ("," ~ record_field)* ~ ","?)? ~ "}"
}

record_field = {
    attr* ~ visibility? ~ data_mode? ~
    name ~ colon_str ~ type
}

tuple_field_list = {
    "(" ~ (tuple_field ~ ("," ~ tuple_field)* ~ ","?)? ~ ")"
}

tuple_field = {
    attr* ~ visibility? ~
    data_mode? ~
    type
}

field_list = {
    condensable_record_field_list
  | tuple_field_list
}

enum = {
    attr* ~ visibility? ~ data_mode? ~
    enum_str ~ name ~ generic_param_list? ~ where_clause? ~
    variant_list
}

variant_list = {
    "{" ~ (variant ~ ("," ~ variant)* ~ ","?)? ~ "}"
}

variant = {
    attr* ~ visibility? ~
    name ~ field_list? ~ (eq_str ~ expr)?
}

union = {
    attr* ~ visibility? ~
    union_str ~ name ~ generic_param_list? ~ where_clause? ~
    record_field_list
}

const = {
    attr* ~ visibility? ~ publish? ~ fn_mode? ~
    default_str? ~
    const_str ~ (name | underscore_str) ~ colon_str ~ type ~
    ((eq_str ~ expr? ~ semi_str?)  // Semi should not be included for const fn
    | (ensures_clause ~ fn_block_expr)
    | semi_str)  // For trait associated const declarations without a default value
}

static = {
    attr* ~ visibility? ~ fn_mode? ~
    static_str ~ mut_str? ~ name ~ colon_str ~ type ~
    (((eq_str ~ expr)? ~ semi_str) | (ensures_clause ~ fn_block_expr))
}

trait = {
    attr* ~ visibility? ~
    const_str? ~ unsafe_str? ~ auto_str? ~
    trait_str ~ name ~ generic_param_list? ~
    (colon_str ~ type_bound_list)? ~ where_clause? ~ assoc_item_list
}

trait_alias = {
    attr* ~ visibility? ~
    trait_str ~ name ~ generic_param_list? ~ eq_str ~ type_bound_list? ~ where_clause? ~ semi_str
}

assoc_items = {
    assoc_item*
}

assoc_item_list = {
    "{" ~ attr* ~ assoc_items ~ "}"
}

verusfmt_skipped_assoc_item = {
    assoc_item
}

assoc_item = {
    (attr* ~ verusfmt_skip_attribute ~ attr* ~ verusfmt_skipped_assoc_item)
  | const
  | fn
  | macro_call
  | type_alias
  | broadcast_group
}

impl = {
    attr* ~ visibility? ~
    default_str? ~ unsafe_str? ~ const_str? ~
    impl_str ~ spaced_generic_param_list? ~ (const_str? ~ bang_str? ~ type ~ for_str)? ~ type ~ where_clause? ~
    assoc_item_list
}

extern_block = {
    attr* ~ unsafe_str? ~ abi ~ extern_item_list
}

extern_item_list = {
    "{" ~ attr* ~ extern_item* ~ "}"
}

extern_item = {
    fn
  | macro_call
  | static
  | type_alias
}

generic_param_list = {
    "<" ~ (generic_param ~ ("," ~ generic_param)* ~ ","?)? ~ ">"
}

// A generic_param_list that should be followed by a space
spaced_generic_param_list = {
    generic_param_list
}

generic_param = {
    const_param
  | lifetime_param
  | type_param
}

type_param = {
    attr* ~ name ~ (colon_str ~ type_bound_list)? ~
    (eq_str ~ type)?
}

const_param = {
    attr* ~ const_str ~ name ~ colon_str ~ type ~
    (eq_str ~ expr)?
}

lifetime_param = {
    attr* ~ lifetime_no_space ~ (colon_str ~ type_bound_list)?
}

where_clause = {
    where_str ~ where_preds?
}

where_preds = {
    where_pred ~ ("," ~ where_pred)* ~ ","?
}

where_pred = {
    (for_str ~ generic_param_list)? ~ (lifetime_no_space | type) ~ colon_str ~ type_bound_list?
}

visibility = {
    pub_str ~ (lparen_str ~ (in_str)? ~ path ~ rparen_str)?
}

attr_core = {
    trigger_attribute
    | "#" ~ bang_str? ~ "[" ~ !"verusfmt" ~ meta ~ "]"
}
// Two aliases for attr_core, so that we can print them differently
attr = !{
    attr_core
    // Inner docstrings are essentially syntax sugar for `#[doc(...)]` and thus
    // are usable wherever attributes are usable. This way, docstring comments
    // can be used anywhere attributes can.
  | inner_docstring_comment
}

attr_inner = {
    attr_core
}

meta = {
    path ~ (eq_str ~ expr | token_tree)?
}

broadcast_use_list = {
    ("{" ~ path ~ ("," ~ path)* ~ ","? ~ "}")
  | (path ~ ("," ~ path)* ~ ","?)
}

broadcast_uses = {
    // We explicitly eat up the extra WHITESPACEs here
    // to prevent it from messing with the MULTI_NEWLINE
    // handling, which would otherwise cause extra newlines
    // to show up.
    broadcast_use+ ~ WHITESPACE*
}

broadcast_use = {
    broadcast_str ~ use_str ~ broadcast_use_list ~ semi_str
}

broadcast_group_identifier = {
    identifier
}

broadcast_group_member = {
    attr* ~ path
}

broadcast_group_list = {
    "{" ~ (broadcast_group_member ~ ("," ~ broadcast_group_member)* ~ ","?)? ~ "}"
}

broadcast_group = {
    attr* ~ visibility? ~ broadcast_str ~ group_str ~ broadcast_group_identifier ~ broadcast_group_list
}

//****************************//
// Statements and Expressions //
//****************************//

verusfmt_skipped_stmt = {
    stmt
}

stmt = !{
    (attr* ~ verusfmt_skip_attribute ~ attr* ~ verusfmt_skipped_stmt)
  | semi_str
  | proof_block
  | let_stmt
  | assignment_stmt
  // We can't use `expr_with_block ~ semi_str?` here, and instead need to do it
  // as the two separate ordered alternatives (`ewb ~ semi_str | ewb`) to
  // prevent munching of multi-newlines that happens otherwise
  | expr_with_block ~ semi_str
  | expr_with_block
  | expr ~ semi_str
  | item_no_macro_call
  | macro_call_stmt
}

let_stmt = {
    attr* ~ let_str ~ ghost_str? ~ tracked_str? ~ mut_str? ~ pat ~ (colon_str ~ type)? ~
    (eq_str ~ expr ~
    let_else?)? ~
    semi_str
}

let_else = {
    else_str ~ block_expr
}

assignment_stmt = {
    star_str* ~ path ~ assignment_ops ~ expr ~ semi_str
}

verusfmt_skipped_expr = {
    expr
}

verusfmt_skipped_expr_no_struct = {
    expr_no_struct
}

// This split of `expr` and `expr_inner` is to simply break the left-recursion
// that would happen otherwise.
expr = !{
    (attr* ~ verusfmt_skip_attribute ~ attr* ~ verusfmt_skipped_expr)
  | expr_inner ~
    expr_outer*
}

expr_no_struct = {
    (attr* ~ verusfmt_skip_attribute ~ attr* ~ verusfmt_skipped_expr_no_struct)
  | expr_inner_no_struct ~
    expr_outer_no_struct*
}

// In certain places, like the conditional for an if_expr,
// we have to prohibit struct_expr, since there is otherwise
// an ambiguity between struct_expr and pattern_expr.  E.g.,
//     let x = if b { 5 } else { 10 };
//     let u = MyStruct { x: 2, y: 3 };
expr_inner_no_struct = _{
    array_expr
  | assert_expr
  | assume_expr
  | final_expr
  | assert_forall_expr
  | bulleted_expr
  | bulleted_expr_inner
  | block_expr
  | box_expr
  | break_expr
  | prefix_expr_no_struct
  | closure_expr
  | quantifier_expr_no_struct
  | continue_expr
  | for_expr
  | if_expr
  | literal
  | loop_expr
  | macro_call
  | match_expr
  | paren_expr
  | ref_expr
  | return_expr
  | tuple_expr
  | while_expr
  | yield_expr
  | yeet_expr
  | let_expr_no_struct
  | path_expr_no_generics   // Needs to be late in this list, or it matches against keywords like "while"
  | underscore_expr // Needs to follow path_expr, so we don't parse "_x" as "_" followed by an unexpected "x"
}

expr_as = {
    as_str ~ type
}

has_or_nothas = {
    bang_str? ~ has_str
}

expr_has = {
    has_or_nothas ~ expr
}

is_or_notis = {
    bang_str? ~ is_str
}

expr_is = {
    is_or_notis ~ type
}

expr_matches = {
    matches_str ~ pat
}

// Separate rule for `->` (rarrow_str) because rarrow_str is normally used for
// functions, and that introduces spaces before and after.
arrow_expr_str = {
    rarrow_str
}

expr_outer = _{
    // await_expr
    dot_str ~ await_str
    // call_expr
    | arg_list
    // cast_expr
    | expr_as
    // collection test
    | expr_has
    // datatype test
    | expr_is
    // tuple index
    | dot_str ~ int_number
    // try_expr
    | question_str
    // view_expr
    | at_str
    // index_expr
    | lbracket_str ~ expr ~ rbracket_str
    // method_call_expr
    | dot_str ~ name_ref ~ generic_arg_list? ~ arg_list
    // field_expr
    | dot_str ~ name_ref
    // arrow_expr
    | arrow_expr_str ~ (int_number | name_ref)
    // matches_expr
    | expr_matches
    // bin_expr
    | bin_expr_ops ~ expr
    // range_expr
    | (dot_dot_str | dot_dot_eq_str) ~ expr?
}

expr_outer_no_struct = _{
    // await_expr
    dot_str ~ await_str
    // call_expr
    | arg_list
    // cast_expr
    | expr_as
    // collection test
    | expr_has
    // datatype test
    | expr_is
    // tuple index
    | dot_str ~ int_number
    // try_expr
    | question_str
    // view_expr
    | at_str
    // index_expr
    | lbracket_str ~ expr_no_struct ~ rbracket_str
    // method_call_expr
    | dot_str ~ name_ref ~ generic_arg_list? ~ arg_list
    // field_expr
    | dot_str ~ name_ref
    // arrow_expr
    | arrow_expr_str ~ (int_number | name_ref)
    // matches_expr
    | expr_matches
    // bin_expr
    | bin_expr_ops ~ expr_no_struct
    // range_expr
    | (dot_dot_str | dot_dot_eq_str) ~ expr_no_struct?
}

expr_inner = {
    if_expr  // Must precede struct_expr or struct_expr thinks `if {}` is a struct
  | struct_expr // Must precede expr_inner_no_struct or `my_struct { }` will be `my_struct`: path_expr
  | quantifier_expr
  | prefix_expr
  | expr_inner_no_struct
  | path_expr
}

expr_with_block = {
    block_expr
  | loop_expr
  | if_expr
  | while_expr
  | for_expr
  | match_expr
  | assert_by_block_expr
  | assert_forall_expr
}

bulleted_expr = {
    "{" ~ bulleted_expr_inner ~ "}"
}

bulleted_expr_inner = {
    (triple_and ~ expr)+
  | (triple_or ~ expr)+
}

macro_expr = {
    macro_call
}

literal = {
    attr* ~ (     
        float_number
      | int_number
      | string
      | raw_string
      | byte_string
      | raw_byte_string
      | true_str
      | false_str
      | char
      | byte
    )
}

path_expr = {
    attr* ~ path
}

path_expr_no_generics = {
    attr* ~ path_no_generics
}

stmt_list = ${
    "{" ~ (WHITESPACE | COMMENT)* ~
    (attr ~ (WHITESPACE | COMMENT)*)* ~
    (stmt ~ (MULTI_NEWLINE | WHITESPACE | COMMENT)*)* ~
    expr? ~ (WHITESPACE | COMMENT)* ~
    "}"
}

ref_expr = {
    attr* ~ amp_str ~ (raw_str | mut_str | const_str)? ~ expr
}

proof_block = {
    attr* ~ label? ~ proof_space_str ~ stmt_list
}

block_expr = {
    proof_block
    | attr* ~ label? ~ (try_str | unsafe_str | async_str | const_str)? ~ stmt_list
}

fn_block_expr = ${
    "{" ~ (WHITESPACE | COMMENT)* ~
    (attr ~ (WHITESPACE | COMMENT)*)* ~
    (stmt ~ (MULTI_NEWLINE | WHITESPACE | COMMENT)*)* ~
    expr? ~ (WHITESPACE | COMMENT)* ~
    "}"
  | "{" ~ (WHITESPACE | COMMENT)* ~ bulleted_expr_inner ~ (WHITESPACE | COMMENT)* ~ "}"
}

prefix_expr = {
    attr* ~ (dash_str | bang_str | star_str) ~ expr
}

prefix_expr_no_struct = {
    attr* ~ (dash_str | bang_str | star_str) ~ expr_no_struct
}

assignment_ops = {
    "=" | "+=" | "/=" | "*=" | "%=" | ">>=" | "<<=" | "-=" | "|=" | "&=" | "^="
}

bin_expr_ops_normal = {
    | (!"|||" ~ ("||" | (!"|=" ~ "|")))
    | (!"&&&" ~ ("&&" | (!"&=" ~ "&")))
    | "<==>"
    | "===" | "=~=" | "=~~="
    | "==>" | "<=="
    | "!=="
    | "<<" | ">>"  // Need to precede "<" and ">"
    | "==" | "!=" | "<=" | ">=" | "<" | ">"
    | assignment_ops
    | "+" | "*" | "-" | "/" | "%" | (!"^=" ~ "^")
}

bin_expr_ops = {
    bin_expr_ops_normal
}

paren_expr_inner = {
    "(" ~ expr ~ ")"
}

paren_expr = {
    attr* ~ paren_expr_inner
}

array_expr_inner = {
    "[" ~ attr* ~ (
        expr ~ semi_str ~ expr
      | comma_delimited_exprs?
    ) ~ "]"
}

array_expr = {
    attr* ~ array_expr_inner
}

tuple_comma_delimited_exprs = {
    comma_delimited_exprs
}

tuple_expr_inner = {
    "(" ~ attr* ~ tuple_comma_delimited_exprs? ~ ")"
}

tuple_expr = {
    attr* ~ tuple_expr_inner
}

struct_expr = {
    path ~ record_expr_field_list
}

struct_update_base = {
    ".." ~ expr
}

record_expr_field_list = {
    "{" ~
    attr* ~
    (record_expr_field ~ ("," ~ record_expr_field)* ~ ","?)? ~
    struct_update_base? ~
    "}"
}

record_expr_field = {
    attr* ~ (name ~ colon_str)? ~ expr
}

arg_list = {
    "(" ~ comma_delimited_exprs? ~ ")"
}

proof_fn_characteristics = {
    "[" ~
    path_segment ~ ("," ~ path_segment)* ~ ","? ~
    "]"
}

proof_fn_with_characteristics_spaced = {
    proof_fn_str ~ proof_fn_characteristics?
}

closure_expr = {
    attr* ~ (!forall_str ~ for_str ~ generic_param_list)? ~
    const_str? ~ static_str? ~ async_str? ~ move_str? ~
    proof_fn_with_characteristics_spaced? ~
    closure_param_list ~ ret_type? ~ requires_clause? ~ ensures_clause? ~
    attr_inner* ~
    expr
}

quantifier_expr = {
    attr* ~
    (forall_str | exists_str | choose_str) ~
    closure_param_list ~ ret_type? ~
    attr_inner* ~
    expr
}

quantifier_expr_no_struct = {
    attr* ~
    (forall_str | exists_str | choose_str) ~
    closure_param_list ~ ret_type? ~
    attr_inner* ~
    expr_no_struct
}

condition = {
    bang_str ~ condition
  | expr_no_struct
}

if_expr = {
    attr* ~ if_str ~ condition ~ fn_block_expr ~
    (else_str ~ (if_expr | fn_block_expr))?
}

loop_clause = {
    invariant_except_break_clause
  | invariant_clause
  | invariant_ensures_clause
  | ensures_clause
  | decreases_clause
}

loop_expr = {
    attr* ~ label? ~ loop_str ~ loop_clause* ~ fn_block_expr
}

for_expr = {
    attr* ~ label? ~ for_str ~ pat ~ in_str ~ expr_no_struct ~
    (colon_str ~ expr_no_struct)?
    ~ loop_clause* ~
    fn_block_expr
}

while_expr = {
    attr* ~ label? ~ while_str ~ condition ~
    loop_clause* ~
    fn_block_expr
}

label = {
    lifetime_no_space ~ colon_str
}

break_expr = {
    attr* ~ break_str ~ lifetime? ~ expr?
}

continue_expr = {
    attr* ~ continue_str ~ lifetime?
}

match_expr = {
    attr* ~ match_str ~ expr ~ match_arm_list
}

match_arm_list = {
    "{" ~
    attr* ~
    match_arm* ~
    "}"
}

match_arm_lhs = {
    attr* ~ pat ~ match_guard?
}

match_arm = {
    match_arm_lhs ~ "=>" ~ ((expr_with_block ~ ","?) | (expr ~ ((!"}" ~ ",") | ","?)))
}

match_guard = {
    if_str ~ expr
}

return_expr = {
    attr* ~ return_str ~ expr?
}

yield_expr = {
    attr* ~ yield_str ~ expr?
}

yeet_expr = {
    attr* ~ do_str ~ yeet_str ~ expr?
}

let_expr_no_struct = {
    attr* ~ let_str ~ pat ~ eq_str ~ expr_no_struct
}

underscore_expr = {
    attr* ~ "_"
}

box_expr = {
    attr* ~ box_str ~ expr
}

//*************************//
//          Types          //
//*************************//

type = {
    array_type
  | dyn_trait_type
  | fn_ptr_type
  | proof_fn_type
  | fn_trait_type
  | for_type
  | impl_trait_type
  | infer_type
  | macro_type
  | never_type
  | paren_type
  | path_type
  | ptr_type
  | ref_type
  | slice_type
  | tuple_type
}

paren_type = {
    "(" ~ type ~ ")"
}

never_type = {
    bang_str
}

macro_type = {
    macro_call
}

path_type = {
    path
}

tuple_type = {
    "(" ~ (type ~ ("," ~ type)* ~ ","?)? ~ ")"
}

ptr_type = {
    star_str ~ (const_str | mut_str) ~ type
}

ref_type = {
    "&" ~ lifetime? ~ mut_str? ~ type
}

array_type = {
    "[" ~ type ~ semi_str ~ expr ~ "]"
}

slice_type = {
    "[" ~ type ~ "]"
}

infer_type = {
    underscore_str
}

fn_ptr_type = {
    const_str? ~ async_str? ~ unsafe_str? ~ abi? ~ fn_str ~ param_list ~ ret_type?
}

fn_traits = {
    FnOnce_str
  | FnMut_str
  | FnSpec_str // note: fnspec is not _really_ a trait, but parses same as others, so we keep it here
  | Fn_str
  | spec_fn_str
}

fn_trait_type = {
    fn_traits ~ generic_param_list? ~ param_list? ~ ret_type?
}

proof_fn_type = {
    proof_fn_str ~ proof_fn_characteristics? ~ generic_param_list? ~ param_list? ~ ret_type?
}

for_type = {
    for_str ~ generic_param_list ~ type
}

impl_trait_type = {
    impl_str ~ type_bound_list
}

dyn_trait_type = {
    dyn_str ~ type_bound_list
}

type_bound_list = {
    type_bound ~ (plus_str ~ type_bound)* ~ plus_str?
}

type_bound = {
    lifetime_no_space
  | (question_str | tilde_str ~ const_str | lbracket_str ~ const_nospace_str ~ rbracket_space_str)? ~ type
}

//************************//
//        Patterns        //
//************************//


pat = {
    pat_inner ~ (
        // range_pat (for 1.. or 1..2)
        (dot_dot_eq_str | dot_dot_str) ~ pat?
        // or_pat
      | (pipe_str ~ pat_inner)* ~ pipe_str?
    )?
}

pat_no_top_alt = {
    pat_inner ~ (
        // range_pat (for 1.. or 1..2)
        (dot_dot_eq_str | dot_dot_str) ~ pat_no_top_alt?
    )?
}

pat_inner = {
    box_pat
//  | rest_pat
  | literal_pat
  | macro_pat
  | paren_pat
//  | wildcard_pat
  | end_only_range_pat
  | record_pat
  | ref_pat
  | slice_pat
  | tuple_pat
  | tuple_struct_pat
  | const_block_pat
  | path_pat
  | ident_pat
}

literal_pat = {
    dash_str? ~ literal
}

ident_pat = {
    attr* ~ ref_str? ~ mut_str? ~ name ~ (at_str ~ pat)?
}

//wildcard_pat = {
//    "_"
//}

end_only_range_pat = {
    (dot_dot_eq_str | dot_dot_str) ~ pat
}

ref_pat = {
    "&" ~ mut_str? ~ pat
}

record_pat = {
    path ~ record_pat_field_list
}

record_pat_field_list = {
    "{" ~
    record_pat_field* ~ ("," ~ record_pat_field)* ~ ","? ~
    rest_pat? ~
    "}"
}

record_pat_field = {
    attr* ~ (name_ref ~ colon_str)? ~ pat
}

tuple_struct_pat_inner = {
    "(" ~ (pat ~ ("," ~ pat)* ~ ","?)? ~ rest_pat? ~ ")"
}

tuple_struct_pat = {
    path ~ tuple_struct_pat_inner
}

tuple_pat = {
    "(" ~ (pat ~ ("," ~ pat)* ~ ","?)? ~ rest_pat? ~ ")"
}

paren_pat = {
    "(" ~ pat ~ ")"
}

slice_pat = {
    "[" ~ (pat ~ ("," ~ pat)* ~ ","?)? ~ "]"
}

path_pat = {
    !(name ~ at_str) ~ path
}

box_pat = {
    box_str ~ pat
}

rest_pat = {
    attr* ~ dot_dot_str
}

macro_pat = {
    macro_call
}

const_block_pat = {
    const_str ~ block_expr
}

//************************//
//        Verus           //
//************************//

publish = {
    closed_str
  | open_str ~ (lparen_str ~ (in_str)? ~ path ~ rparen_str)?
  | uninterp_str
}

fn_mode = {
    mode_spec_checked
  | spec_str
  | proof_str
  | exec_str
  | axiom_str
}

mode_spec_checked = {
    spec_str ~ lparen_str ~ checked_str ~ rparen_str
}

data_mode = {
    ghost_str
  | tracked_str
}

comma_delimited_exprs = {
    expr ~ ("," ~ expr)* ~ ","?
}

// Prohibit top-level struct_expr, to avoid ambiguity for something like:
//    pub fn alice_addr(a:int) -> (b:int)
//        ensures a == b 
//    {
//        a
//    }
// where we could interpret the ensures expression as `a == b { a }`
comma_delimited_exprs_for_verus_clauses = {
    !verus_clause_non_expr ~ expr_no_struct ~ ("," ~ !verus_clause_non_expr ~ expr_no_struct)* ~ ","?
}

groupable_comma_delimited_exprs_for_verus_clauses = {
    comma_delimited_exprs_for_verus_clauses
}

single_expr_for_verus_clause = {
    !verus_clause_non_expr ~ expr_no_struct ~ ","?
}

verus_clause_non_expr = _{
    "{"             // TODO: Why is this permitted here?
  | requires_str
  | ensures_str
  | default_ensures_str
  | returns_str
  | invariant_except_break_str
  | invariant_str
  | invariant_ensures_str
  | recommends_str
  | via_str
  | decreases_str
  | when_str
  | opens_invariants_str
  | no_unwind_str
}

requires_clause = {
    requires_str ~ comma_delimited_exprs_for_verus_clauses?
}

ensures_clause = {
    ensures_str ~ comma_delimited_exprs_for_verus_clauses?
}

default_ensures_clause = {
    default_ensures_str ~ comma_delimited_exprs_for_verus_clauses?
}

returns_clause = {
    returns_str ~ single_expr_for_verus_clause
}

invariant_except_break_clause = {
    invariant_except_break_str ~ comma_delimited_exprs_for_verus_clauses?
}

invariant_clause = {
    invariant_str ~ comma_delimited_exprs_for_verus_clauses?
}

invariant_ensures_clause = {
    invariant_ensures_str ~ comma_delimited_exprs_for_verus_clauses?
}

recommends_clause = {
    recommends_str ~ (comma_delimited_exprs_for_verus_clauses ~ (via_str ~ expr_no_struct)?)?
}

decreases_clause = {
    decreases_str ~ (groupable_comma_delimited_exprs_for_verus_clauses ~ (when_str ~ expr_no_struct)? ~ (via_str ~ expr_no_struct)?)?
}

unwind_clause = {
    no_unwind_str ~ (no_unwind_when_str ~ expr_no_struct)?
}

opens_invariants_mode = {
    any_str
  | none_str
  | lbracket_str ~ comma_delimited_exprs? ~ rbracket_str
  | expr_no_struct
}

opens_invariants_clause = {
    opens_invariants_str ~ opens_invariants_mode
}

assert_requires = {
    requires_clause
}

assert_expr_prefix = {
    attr* ~ assert_str ~ lparen_str ~ expr ~ rparen_str
}

assert_by_block_expr = {
    assert_expr_prefix ~ inline_prover ~ assert_requires? ~ block_expr
}

assert_by_prover_expr = {
    assert_by_block_expr
  | assert_expr_prefix ~ inline_prover ~ assert_requires?
}

assert_expr = {
    assert_by_prover_expr
  | assert_expr_prefix
}

assume_expr = {
    attr* ~ assume_str ~ lparen_str ~ expr ~ rparen_str
}

final_expr = {
    attr* ~ final_str ~ lparen_str ~ expr ~ rparen_str
}

assert_forall_expr = {
    attr* ~ assert_space_str ~ forall_str ~ closure_expr ~ (implies_str ~ expr)? ~ by_str_inline ~ block_expr
}

inline_prover = {
    prover
}

prover = {
    by_str ~ (lparen_str ~ name ~ rparen_str)?
}

trigger_attribute = {
    pound_str ~ bang_str? ~ "[" ~ trigger_str ~ comma_delimited_exprs? ~ "]"
}