// 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*
~ type_decl*
~ effect_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_uses? ~ "=" ~ 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)* }
protocol_uses = { "uses" ~ ident ~ ("," ~ ident)* }
type_decl = { type_alias_decl | union_type_decl }
type_alias_decl = { "type" ~ "alias" ~ ident ~ "=" ~ type_expr }
union_type_decl = { "type" ~ ident ~ union_ctor_decl+ }
union_ctor_decl = { "|" ~ ident ~ ("of" ~ type_expr)? }
effect_decl = { "effect" ~ ident ~ effect_body }
effect_body = { "{" ~ effect_op_decl+ ~ "}" | effect_op_decl+ }
effect_op_decl = { ident ~ ":" ~ type_expr ~ "->" ~ type_expr }
type_expr = { type_record | type_result | type_maybe | type_unit | type_path }
type_record = { "{" ~ (!"}" ~ ANY)* ~ "}" }
type_result = { "Result" ~ type_expr ~ type_expr }
type_maybe = { "Maybe" ~ type_expr }
type_unit = { "Unit" }
// 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 = _{
let_in_stmt
| let_stmt
| case_stmt
| timeout_stmt
| send_stmt
| broadcast_stmt
| heartbeat_stmt
| timed_choice_stmt
| choice_stmt
| par_stmt
| loop_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
}
let_in_stmt = { "let" ~ ident ~ "=" ~ authority_expr ~ "in" ~ block }
let_stmt = { "let" ~ ident ~ "=" ~ authority_expr }
case_stmt = { "case" ~ authority_expr ~ "of" ~ case_block }
case_block = { "{" ~ case_branch+ ~ "}" | "(" ~ case_branch+ ~ ")" }
case_branch = { "|" ~ match_pattern ~ "->" ~ block }
match_pattern = { ident ~ ident* }
timeout_stmt = {
"timeout" ~ duration ~ "at" ~ role_ref ~ block
~ "on" ~ "timeout" ~ block
~ ("on" ~ "cancel" ~ block)?
}
authority_expr = { check_expr | transfer_expr | result_ctor_expr | maybe_ctor_expr | call_expr | ident_expr }
check_expr = { "check" ~ effect_call }
transfer_expr = { "transfer" ~ ident ~ "from" ~ role_ref ~ "to" ~ role_ref }
result_ctor_expr = { ("Ok" | "Err") ~ ident_expr? }
maybe_ctor_expr = { ("Just" ~ ident_expr) | "Nothing" }
effect_call = { ident ~ "." ~ ident ~ "(" ~ argument_list? ~ ")" }
call_expr = { ident ~ "(" ~ argument_list? ~ ")" }
argument_list = { authority_atom ~ ("," ~ authority_atom)* }
authority_atom = { effect_call | ident_expr | string | integer }
ident_expr = { ident ~ ("." ~ ident)* }
// 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 = { annotated_sender_ref ~ "->" ~ role_ref ~ ":" ~ message }
// Broadcast statement
broadcast_stmt = { annotated_sender_ref ~ "->*" ~ ":" ~ message }
annotated_sender_ref = { role_ref ~ role_metadata_record? }
role_metadata_record = { "{" ~ role_annotation_entries? ~ "}" }
role_annotation_entries = { role_annotation_entry ~ ("," ~ role_annotation_entry)* ~ ","? }
role_annotation_entry = { ident ~ "=" ~ role_annotation_value }
role_annotation_value = { string | duration | integer | ident }
// 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 = { "choice" ~ "at" ~ role_ref }
choice_block = { block_choice }
block_choice = { "{" ~ choice_branch+ ~ "}" | "(" ~ choice_branch+ ~ ")" }
choice_branch = { "|" ~ ident ~ guard? ~ "->" ~ block }
// Parallel block with bar-prefixed branches
par_stmt = { "par" ~ par_block }
par_block = { "{" ~ par_branch+ ~ "}" | "(" ~ par_branch+ ~ ")" }
par_branch = { "|" ~ (block | statement) }
// Guard condition for choice branches
guard = { evidence_guard | predicate_guard }
predicate_guard = { "when" ~ "(" ~ guard_expr ~ ")" }
evidence_guard = { "when" ~ "check" ~ effect_call ~ "yields" ~ ident }
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 }
// Recursive protocol
rec_stmt = { "rec" ~ ident ~ block }
// Block
block = { "{" ~ statement* ~ "}" | "(" ~ statement+ ~ ")" }
// Message specification
message = { ident ~ message_of? ~ payload? }
message_of = { "of" ~ type_spec }
type_spec = { type_path ~ type_generics? }
type_path = { ident ~ type_path_segment* }
type_path_segment = { "." ~ 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)* ~ "\"" }