// 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*
~ top_level_decl*
~ protocol_decl
~ EOI
}
top_level_decl = _{
proof_bundle_decl
| profile_decl
| agreement_profile_decl
| role_set_decl
| topology_decl
| type_decl
| effect_decl
| fragment_decl
| operation_decl
| guest_runtime_decl
}
// 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_profiles? ~ "=" ~ 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)* }
protocol_profiles = { "under" ~ ident ~ ("," ~ ident)* }
profile_decl = { "profile" ~ ident ~ profile_meta* }
profile_meta = { profile_fairness | profile_admissibility | profile_escalation_window }
profile_fairness = { "fairness" ~ ident }
profile_admissibility = { "admissibility" ~ ident }
profile_escalation_window = { "escalation_window" ~ ident }
agreement_profile_decl = { "agreement_profile" ~ ident ~ agreement_profile_body }
agreement_profile_body = { "{" ~ agreement_profile_meta+ ~ "}" | agreement_profile_meta+ }
agreement_profile_meta = {
agreement_profile_visibility
| agreement_profile_rule
| agreement_profile_usable_at
| agreement_profile_finalized_at
| agreement_profile_evidence
}
agreement_profile_visibility = { "visibility" ~ ident }
agreement_profile_rule = { "rule" ~ ident }
agreement_profile_usable_at = { "usable_at" ~ ident }
agreement_profile_finalized_at = { "finalized_at" ~ ident }
agreement_profile_evidence = { "evidence" ~ ident }
type_decl = { type_alias_decl | union_type_decl }
type_alias_decl = { "type" ~ "alias" ~ ident ~ "=" ~ type_expr }
union_type_decl = { "type" ~ ident ~ "=" ~ union_ctor_block }
union_ctor_block = { union_ctor_decl+ | "{" ~ union_ctor_decl+ ~ "}" | "(" ~ union_ctor_decl+ ~ ")" }
union_ctor_decl = { "|" ~ ident ~ ctor_type_payload? }
ctor_type_payload = { "(" ~ type_expr ~ ")" }
effect_decl = { "effect" ~ ident ~ effect_body }
effect_body = { "{" ~ effect_op_decl+ ~ "}" | effect_op_decl+ }
effect_op_decl = { effect_op_head ~ effect_op_meta_body? }
effect_op_head = { effect_op_authority_class? ~ ident ~ ":" ~ type_expr ~ "->" ~ type_expr }
effect_op_authority_class = { "authoritative" | "command" | "observe" }
effect_op_meta_body = { "{" ~ effect_op_meta* ~ "}" }
effect_op_meta = _{
effect_op_semantic_class
| effect_op_progress
| effect_op_region
| effect_op_agreement_use
| effect_op_reentrancy
}
effect_op_semantic_class = { "class" ~ ":" ~ ident ~ ","? }
effect_op_progress = { "progress" ~ ":" ~ ident ~ ","? }
effect_op_region = { "region" ~ ":" ~ ident ~ ","? }
effect_op_agreement_use = { "agreement_use" ~ ":" ~ ident ~ ","? }
effect_op_reentrancy = { "reentrancy" ~ ":" ~ ident ~ ","? }
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)* }
fragment_decl = { "fragment" ~ ident ~ ident_list? }
ident_list = { "(" ~ ident ~ ("," ~ ident)* ~ ")" }
operation_decl = { "operation" ~ ident ~ operation_params? ~ "at" ~ role_ref ~ operation_within? ~ operation_progress? ~ operation_agreement? ~ operation_compose? ~ "=" ~ protocol_body }
operation_params = { "(" ~ operation_param_decl ~ ("," ~ operation_param_decl)* ~ ")" }
operation_param_decl = { ident ~ ":" ~ type_expr }
operation_within = { "within" ~ ident ~ ident_list? }
operation_progress = { progress_attachment }
operation_agreement = { "agreement" ~ ident ~ operation_prestate? }
operation_prestate = { "prestate" ~ ident }
operation_compose = { "compose" ~ ident ~ ("(" ~ integer ~ ")")? }
guest_runtime_decl = { "guest" ~ "runtime" ~ ident ~ "=" ~ guest_runtime_body }
guest_runtime_body = { "{" ~ guest_runtime_stmt+ ~ "}" | guest_runtime_stmt+ }
guest_runtime_stmt = { guest_runtime_uses | guest_runtime_entry }
guest_runtime_uses = { "uses" ~ ident ~ ("," ~ ident)* }
guest_runtime_entry = { "entry" ~ 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 = _{
begin_stmt
| await_stmt
| resolve_stmt
| invalidate_stmt
|
authority_let_in_stmt
| authority_let_stmt
| observe_let_in_stmt
| observe_let_stmt
|
let_in_stmt
| let_stmt
| case_stmt
| timeout_stmt
| send_stmt
| broadcast_stmt
| choice_stmt
| par_stmt
| loop_stmt
| rec_stmt
| continue_stmt
| call_stmt
| publish_authority_stmt
| publish_stmt
| materialize_stmt
| handoff_stmt
| dependent_work_stmt
}
progress_attachment = { "progress" ~ ident ~ progress_meta* }
progress_meta = _{ progress_requires | progress_within | progress_on_timeout | progress_on_stall }
progress_requires = { "requires" ~ ident }
progress_within = { "within" ~ ident }
progress_on_timeout = { "on" ~ "timeout" ~ "=>" ~ ident }
progress_on_stall = { "on" ~ "stall" ~ "=>" ~ ident }
begin_stmt = { "begin" ~ ident ~ begin_args? ~ progress_attachment? }
begin_args = { "(" ~ argument_list? ~ ")" }
await_stmt = { "await" ~ ident }
resolve_stmt = { "resolve" ~ ident ~ "as" ~ resolve_outcome }
resolve_outcome = { resolve_success | resolve_failure | resolve_timeout | resolve_cancelled }
resolve_success = { "Success" ~ ctor_value_payload? }
resolve_failure = { "Failure" ~ ctor_value_payload? }
resolve_timeout = { "Timeout" ~ ctor_value_payload? }
resolve_cancelled = { "Cancelled" }
invalidate_stmt = { "invalidate" ~ ident }
authority_let_in_stmt = { "authoritative" ~ "let" ~ ident ~ "=" ~ authority_expr ~ "in" ~ block }
authority_let_stmt = { "authoritative" ~ "let" ~ ident ~ "=" ~ authority_expr }
observe_let_in_stmt = { "observe" ~ "let" ~ ident ~ "=" ~ authority_expr ~ "in" ~ block }
observe_let_stmt = { "observe" ~ "let" ~ ident ~ "=" ~ authority_expr }
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 ~ "=>" ~ branch_body }
match_pattern = { ident ~ match_pattern_payload? }
match_pattern_payload = { "(" ~ ident ~ ("," ~ ident)* ~ ")" }
timeout_stmt = {
"timeout" ~ duration ~ role_ref ~ "at" ~ block
~ "on" ~ "timeout" ~ "=>" ~ branch_body
~ ("on" ~ "cancel" ~ "=>" ~ branch_body)?
}
authority_expr = { check_expr | observe_expr | transfer_expr | result_ctor_expr | maybe_ctor_expr | call_expr | ident_expr }
check_expr = { "check" ~ effect_call }
observe_expr = { "observe" ~ effect_call }
transfer_expr = { "transfer" ~ ident ~ "from" ~ role_ref ~ "to" ~ role_ref }
result_ctor_expr = { ("Ok" | "Err") ~ ctor_value_payload? }
maybe_ctor_expr = { ("Just" ~ ctor_value_payload) | "Nothing" }
ctor_value_payload = { "(" ~ ident_expr ~ ")" }
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)* }
duration = { integer ~ time_unit }
time_unit = { "ms" | "s" | "m" | "h" }
// Protocol call statement (for sub-protocols in where blocks)
call_stmt = { "call" ~ ident }
publish_authority_stmt = { "publish" ~ ident ~ "as" ~ ident }
publish_stmt = { "publish" ~ ident ~ ctor_value_payload? }
materialize_stmt = { "materialize" ~ ident ~ "from" ~ ident }
handoff_stmt = { "handoff" ~ ident ~ "to" ~ role_ref ~ "with" ~ ident }
dependent_work_stmt = { "dependent" ~ "work" ~ ident ~ ctor_value_payload? ~ "required" ~ "for" ~ ident }
// 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" ~ role_ref ~ "at" }
choice_block = { block_choice }
block_choice = { "{" ~ choice_branch+ ~ "}" | "(" ~ choice_branch+ ~ ")" }
choice_branch = { "|" ~ ident ~ guard? ~ "=>" ~ branch_body }
// 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+ ~ ")" }
branch_body = { block | 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)* ~ "\"" }