//! 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 = { "]" }
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) }
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? ~
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? ~
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)? ~ 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? ~ "]"
}