// Choreographic DSL Grammar (PureScript-inspired syntax)
//
// DSL comments use Haskell/PureScript style:
// -- single line comment
// {- multi-line comment -}
WHITESPACE = _{ " " | "\t" | "\r" | "\n" | COMMENT }
COMMENT = _{ "--" ~ (!"\n" ~ ANY)* ~ ("\n" | EOI) | "{-" ~ (!"-}" ~ ANY)* ~ "-}" }
// Top-level choreography definition
choreography = {
SOI ~ module_decl? ~ import_decl* ~ proof_bundle_decl* ~ role_set_decl* ~ topology_decl* ~ protocol_decl ~ EOI
}
// Module and imports (optional)
module_decl = { "module" ~ ident ~ "exposing" ~ "(" ~ expose_list? ~ ")" }
import_decl = { "import" ~ ident ~ ("as" ~ ident)? ~ ("exposing" ~ "(" ~ expose_list? ~ ")")? }
expose_list = { (!")" ~ ANY)* }
// Protocol definitions
protocol_decl = { "protocol" ~ ident ~ header_roles? ~ protocol_requires? ~ "=" ~ protocol_body ~ where_block? }
where_block = { "where" ~ locals_block }
locals_block = { "{" ~ local_protocol_decl+ ~ "}" | "(" ~ local_protocol_decl+ ~ ")" | local_protocol_decl+ }
local_protocol_decl = { "protocol" ~ ident ~ header_roles? ~ "=" ~ protocol_body }
// Proof-bundle declarations and protocol requirements
proof_bundle_decl = { "proof_bundle" ~ ident ~ proof_bundle_meta* ~ proof_bundle_requires? }
proof_bundle_meta = { proof_bundle_version | proof_bundle_issuer | proof_bundle_constraint }
proof_bundle_version = { "version" ~ string }
proof_bundle_issuer = { "issuer" ~ string }
proof_bundle_constraint = { "constraint" ~ string }
proof_bundle_requires = { "requires" ~ "[" ~ capability_list? ~ "]" }
capability_list = { ident ~ ("," ~ ident)* }
protocol_requires = { "requires" ~ ident ~ ("," ~ ident)* }
// Role-set and topology declarations
role_set_decl = { "role_set" ~ ident ~ "=" ~ role_set_expr }
role_set_expr = { role_set_subset | role_set_members }
role_set_members = { ident ~ ("," ~ ident)* }
role_set_subset = { "subset" ~ "(" ~ ident ~ "," ~ integer ~ ".." ~ integer ~ ")" }
topology_decl = { topology_kind ~ ident ~ "=" ~ topology_members }
topology_kind = { "cluster" | "ring" | "mesh" }
topology_members = { ident ~ ("," ~ ident)* }
header_roles = { "(" ~ role_list ~ ")" }
// Roles declaration
roles_decl = { "roles" ~ role_list }
role_list = { role_decl ~ ("," ~ role_decl)* }
role_decl = { ident ~ role_param? }
role_param = { "[" ~ role_param_expr ~ "]" }
role_param_expr = { integer | ident | "*" }
// Protocol body (sequence of statements)
protocol_body = { block_protocol }
block_protocol = { "{" ~ roles_decl? ~ statement* ~ "}" | "(" ~ roles_decl? ~ statement+ ~ ")" }
// Statement types
statement = _{
annotated_stmt
| send_stmt
| broadcast_stmt
| heartbeat_stmt
| timed_choice_stmt
| choice_stmt
| loop_stmt
| branch_stmt
| rec_stmt
| continue_stmt
| call_stmt
| handshake_stmt
| retry_stmt
| quorum_collect_stmt
| vm_acquire_stmt
| vm_release_stmt
| vm_fork_stmt
| vm_join_stmt
| vm_abort_stmt
| vm_transfer_stmt
| vm_tag_stmt
| vm_check_stmt
}
// Annotated statement - statement with prefix annotation(s)
// Syntax: @runtime_timeout(5s) Alice -> Bob: Message
annotated_stmt = { annotation+ ~ inner_stmt }
annotation = { "@" ~ annotation_kind }
annotation_kind = { runtime_timeout_annotation | custom_annotation }
runtime_timeout_annotation = { "runtime_timeout" ~ "(" ~ duration ~ ")" }
custom_annotation = { ident ~ ("(" ~ annotation_args ~ ")")? }
annotation_args = { (!(")" | ",") ~ ANY)* ~ ("," ~ (!(")" | ",") ~ ANY)*)* }
inner_stmt = _{
send_stmt
| broadcast_stmt
| choice_stmt
| loop_stmt
| branch_stmt
| rec_stmt
| call_stmt
| handshake_stmt
| retry_stmt
| quorum_collect_stmt
| vm_acquire_stmt
| vm_release_stmt
| vm_fork_stmt
| vm_join_stmt
| vm_abort_stmt
| vm_transfer_stmt
| vm_tag_stmt
| vm_check_stmt
}
// Timed choice statement - desugars to choice with timeout annotation
// Syntax: timed_choice at Alice(5s) { OnTime { ... } TimedOut { ... } }
timed_choice_stmt = { "timed_choice" ~ "at" ~ role_ref ~ "(" ~ duration ~ ")" ~ choice_block }
duration = { integer ~ time_unit }
time_unit = { "ms" | "s" | "m" | "h" }
// Heartbeat statement - desugars to recursive choice with liveness detection
// Syntax: heartbeat Sender -> Receiver every 1s on_missing(3) { timeout_body } body { normal_body }
heartbeat_stmt = { "heartbeat" ~ role_ref ~ "->" ~ role_ref ~ "every" ~ duration ~ heartbeat_on_missing ~ heartbeat_body }
heartbeat_on_missing = { "on_missing" ~ "(" ~ integer ~ ")" ~ block }
heartbeat_body = { "body" ~ block }
// Protocol call statement (for sub-protocols in where blocks)
call_stmt = { "call" ~ ident }
// First-class combinators
handshake_stmt = { "handshake" ~ role_ref ~ "<->" ~ role_ref ~ ":" ~ ident }
retry_stmt = { "retry" ~ int_expr ~ block }
quorum_collect_stmt = { "quorum_collect" ~ role_ref ~ "->" ~ role_ref ~ "min" ~ integer ~ ":" ~ message }
// VM-core operational statements
vm_acquire_stmt = { "acquire" ~ vm_layer ~ "as" ~ ident }
vm_release_stmt = { "release" ~ vm_layer ~ "using" ~ ident }
vm_fork_stmt = { "fork" ~ ident }
vm_join_stmt = { "join" }
vm_abort_stmt = { "abort" }
vm_transfer_stmt = { ("transfer" | "delegate") ~ ident ~ "to" ~ ident ~ ("with" ~ "bundle" ~ ident)? }
vm_tag_stmt = { "tag" ~ ident ~ "as" ~ ident }
vm_check_stmt = { "check" ~ ident ~ "for" ~ role_ref ~ "into" ~ ident }
vm_layer = { ident | string }
// Continue statement (for recursive back-references)
continue_stmt = { "continue" ~ ident }
// Send statement
send_stmt = { role_ref ~ "->" ~ role_ref ~ ":" ~ message }
// Broadcast statement
broadcast_stmt = { role_ref ~ "->*" ~ ":" ~ message }
// Role reference (can be simple or indexed)
role_ref = { ident ~ role_index? }
role_index = { "[" ~ role_index_expr ~ "]" }
role_index_expr = { range_expr | integer | ident | "*" }
range_expr = { (integer | ident) ~ ".." ~ (integer | ident) }
// Choice statement
choice_stmt = { choice_head ~ choice_block }
choice_head = { ("case" ~ "choose" ~ role_ref ~ "of") | ("choice" ~ "at" ~ role_ref) }
choice_block = { block_choice }
block_choice = { "{" ~ choice_branch+ ~ "}" | "(" ~ choice_branch+ ~ ")" }
choice_branch = { ident ~ guard? ~ "->" ~ block }
// Guard condition for choice branches
guard = { "when" ~ "(" ~ guard_expr ~ ")" }
guard_expr = { (!")" ~ ANY)+ }
// Loop statement
loop_stmt = { "loop" ~ loop_spec ~ block }
loop_spec = { loop_decide | loop_repeat | loop_while | loop_forever }
loop_decide = { "decide" ~ "by" ~ role_ref }
loop_repeat = { "repeat" ~ int_expr }
loop_while = { "while" ~ string }
loop_forever = { "forever" }
int_expr = { integer | ident }
// Parallel branch statement
branch_stmt = { "branch" ~ block }
// Recursive protocol
rec_stmt = { "rec" ~ ident ~ block }
// Block
block = { "{" ~ statement* ~ "}" | "(" ~ statement+ ~ ")" }
// Message specification
message = { ident ~ message_type? ~ payload? }
message_type = { "<" ~ type_spec ~ ("," ~ type_spec)* ~ ">" }
type_spec = { type_path ~ type_generics? }
type_path = { ident ~ ("::" ~ ident)* }
type_generics = { "<" ~ type_spec ~ ("," ~ type_spec)* ~ ">" }
payload = { payload_paren | payload_brace }
payload_paren = { "(" ~ (!")" ~ ANY)* ~ ")" }
payload_brace = { "{" ~ (!"}" ~ ANY)* ~ "}" }
// Basic tokens
ident = @{ ASCII_ALPHA ~ (ASCII_ALPHANUMERIC | "_")* }
integer = @{ ASCII_DIGIT+ }
string = @{ "\"" ~ (!"\"" ~ ANY)* ~ "\"" }