// Event-B Grammar Definition for pest parser
// This grammar defines the syntax for Event-B formal modeling language

WHITESPACE = _{ " " | "\t" | "\r" | "\n" }
COMMENT = _{ ("/*" ~ (!"*/" ~ ANY)* ~ "*/") | ("//" ~ (!"\n" ~ ANY)* ~ "\n"?) }

// ==========================
// Basic Tokens
// ==========================

// Word-boundary guards (single source of truth). `word_char` is the set of
// characters that continue a mathematical identifier; a keyword counts as a
// keyword only when not immediately followed by one (otherwise it is an
// identifier prefix, e.g. `events_of_partition` is one name). Math/logic
// keywords keep the narrow guard so a trailing `-` reads as subtraction
// (`NAT-1` = `ℕ − 1`); structural keywords also treat `-` as a word char so a
// hyphenated `component_name` (`end-to-end`, `variant-x`) is never split at an
// embedded keyword.
word_char = _{ ASCII_ALPHANUMERIC | "_" }
word_boundary = _{ !word_char }
struct_word_boundary = _{ !(word_char | "-") }

// Prime-less, hyphen-less identifier core, shared by `identifier` and
// `component_name`; built on the single `word_char` alnum+`_` source.
ident_core = _{ (ASCII_ALPHA | "_") ~ word_char* }

// Identifier (mathematical: kernel_lang §2.2 — no hyphens; see names.rs).
// An optional single trailing prime marks an Event-B after-state variable
// (`x'`). The prime never repeats nor appears interior (`x''`, `x'y` are two
// tokens), matching Rodin's lexer, where a prime attaches only to a plain
// identifier — never to a keyword.
identifier = @{ ident_core ~ "'"? }

// Component name: machine/context names, REFINES/SEES/EXTENDS targets and
// event names. Rodin stores these as file names / labels (bare strings, not
// mathematical identifiers), so real models use hyphens (`A-C0`, `CTX-1`).
// Hyphens join non-empty segments which may start with a digit (`ENV_C-1`);
// leading/trailing/doubled hyphens never match. File labels carry no prime.
// Kept in sync with `names::check_component_name` by a parity test.
component_name = @{ ident_core ~ ("-" ~ word_char+)* }

// Typed identifier: x⦂ℤ (bound variable with optional type annotation).
// The type uses `ident_binder_type` rather than `maplet_expr` so that
// `λx⦂T₁ ↦ y⦂T₂ · …` parses with `↦` as the lambda-pattern separator, not
// as a maplet inside T₁ (the spec uses `↦` only as a value constructor —
// types use `×` and the relation arrows but never a top-level `↦`).
typed_identifier = { identifier ~ (op_oftype ~ ident_binder_type)? }
ident_binder_type = {
    set_operator_expr ~ ((op_total_surj | op_partial_surj | op_bijection
                          | op_total_inj | op_partial_inj
                          | op_total_fn | op_partial_fn
                          | op_total_surjective_relation | op_surjective_relation
                          | op_total_relation | op_relation) ~ set_operator_expr)?
}

// Numbers
integer = @{ "-"? ~ ASCII_DIGIT+ }

// ==========================
// Keywords
// ==========================

// Context Keywords (case-insensitive). Atomic rules carrying a trailing
// `struct_word_boundary` so a keyword never matches an identifier/component_name
// prefix; see the word-boundary guards above for why structural keywords admit
// `-` while math keywords (further down) use the narrower `word_boundary`.
kw_context = @{ ^"context" ~ struct_word_boundary }
kw_extends = @{ ^"extends" ~ struct_word_boundary }
kw_sets = @{ ^"sets" ~ struct_word_boundary }
kw_constants = @{ ^"constants" ~ struct_word_boundary }
kw_axioms = @{ ^"axioms" ~ struct_word_boundary }
// THEOREMS section header. Distinct from the singular inline `kw_theorem` flag:
// the trailing word-boundary guard means `THEOREMS` never matches `kw_theorem`
// (the `s` fails its boundary) and vice-versa.
kw_theorems = @{ ^"theorems" ~ struct_word_boundary }
kw_end = @{ ^"end" ~ struct_word_boundary }

// Machine Keywords (case-insensitive)
kw_machine = @{ ^"machine" ~ struct_word_boundary }
kw_refines = @{ ^"refines" ~ struct_word_boundary }
kw_sees = @{ ^"sees" ~ struct_word_boundary }
kw_variables = @{ ^"variables" ~ struct_word_boundary }
kw_invariants = @{ ^"invariants" ~ struct_word_boundary }
kw_variant = @{ ^"variant" ~ struct_word_boundary }
kw_events = @{ ^"events" ~ struct_word_boundary }
kw_initialisation = @{ ^"initialisation" ~ struct_word_boundary }

// Event Keywords (case-insensitive)
kw_event = @{ ^"event" ~ struct_word_boundary }
kw_any = @{ ^"any" ~ struct_word_boundary }
kw_where = @{ ^"where" ~ struct_word_boundary }
kw_when = @{ ^"when" ~ struct_word_boundary }
kw_with = @{ ^"with" ~ struct_word_boundary }
kw_then = @{ ^"then" ~ struct_word_boundary }
kw_begin = @{ ^"begin" ~ struct_word_boundary }
kw_witness = @{ ^"witness" ~ struct_word_boundary }
kw_status = @{ ^"status" ~ struct_word_boundary }
kw_ordinary = @{ ^"ordinary" ~ struct_word_boundary }
kw_convergent = @{ ^"convergent" ~ struct_word_boundary }
kw_anticipated = @{ ^"anticipated" ~ struct_word_boundary }

// Action Keywords
kw_skip = @{ ^"skip" ~ word_boundary }

// Logic keywords — predicate literals. Lowercase ASCII `true`/`false` or the
// Unicode glyphs ⊤/⊥; the uppercase boolean values/type are the kw_bool_*
// rules below. ASCII spellings are exact-case, matching the kernel language.
kw_true = @{ ("true" ~ word_boundary) | "⊤" }
kw_false = @{ ("false" ~ word_boundary) | "⊥" }
kw_theorem = @{ ^"theorem" ~ word_boundary }

// Built-in types. ASCII spellings are exact-case (uppercase), matching the
// kernel language; the Unicode forms ℕ/ℤ are the canonical ones.
kw_nat1 = @{ ("ℕ1" | "NAT1") ~ word_boundary }
kw_nat = @{ ("ℕ" | "NAT") ~ word_boundary }
kw_int = @{ ("ℤ" | "INT") ~ word_boundary }
// `bool(P)` conversion operator (lowercase); the BOOL type is kw_bool_type.
kw_bool = @{ "bool" ~ word_boundary }

// Boolean values (TRUE/FALSE) and the BOOL type — uppercase, distinct from the
// lowercase predicate literals true/false and the bool(…) conversion operator.
kw_bool_true = @{ "TRUE" ~ word_boundary }
kw_bool_false = @{ "FALSE" ~ word_boundary }
kw_bool_type = @{ "BOOL" ~ word_boundary }

// Quantified set operation keywords (uppercase ASCII or the Unicode glyphs)
kw_UNION = @{ "⋃" | ("UNION" ~ word_boundary) }
kw_INTER = @{ "⋂" | ("INTER" ~ word_boundary) }

// ==========================
// Operators and Symbols
// ==========================

// Logical Operators
op_and = { "∧" | "&" }
op_or = @{ "∨" | ("or" ~ word_boundary) }
op_implies = { "⇒" | "=>" }
op_equivalent = { "⇔" | "<=>" }
op_not = @{ "¬" | ("not" ~ word_boundary) }

// Quantifiers
op_forall = { "∀" | "!" }
op_exists = { "∃" | "#" }

// Set Operators
op_in = { "∈" | ":" }
op_notin = { "∉" | "/:" }
op_subset = { "⊆" | "<:" }
op_subset_strict = { "⊂" | "<<:" }
op_not_subset = { "⊈" | "/<:" }
op_not_subset_strict = { "⊄" | "/<<:" }
op_union = { "∪" | "\\/" }
op_intersection = { "∩" | "/\\" }
op_difference = { "∖" | "\\" }
op_cartesian = { "×" | "**" }
op_powerset = @{ "ℙ" | ("POW" ~ word_boundary) }
op_powerset1 = @{ "ℙ1" | ("POW1" ~ word_boundary) }
op_emptyset = { "∅" | "{}" }
op_oftype = @{ "⦂" | ("oftype" ~ word_boundary) }

// Relation Operators
// `,,` is an accepted alternative input spelling for the maplet ↦.
op_maplet = { "↦" | "|->" | ",," }
op_relation = { "↔" | "<->" }
op_partial_fn = { "⇸" | "+->" }
op_total_fn = { "→" | "-->" }
op_partial_inj = { "⤔" | ">+>" }
op_total_inj = { "↣" | ">->" }
op_partial_surj = { "⤀" | "+>>" }
op_total_surj = { "↠" | "->>" }
op_bijection = { "⤖" | ">->>" }
op_domain = @{ "dom" ~ word_boundary }
op_range = @{ "ran" ~ word_boundary }
op_inverse = { "\u{223C}" | "~" }
op_semicolon = { ";" }
op_composition = @{ "∘" | ("circ" ~ word_boundary) }
op_domain_restrict = { "◁" | "<|" }
op_domain_subtract = { "⩤" | "<<|" }
op_range_restrict = { "▷" | "|>" }
op_range_subtract = { "⩥" | "|>>" }
op_overwrite = { "\u{E103}" | "<+" }
op_direct_product = { "⊗" | "><" }
op_parallel_product = { "∥" | "||" }

// Additional relation types (total relation, surjective relation, total surjective relation)
// PEG ordering: <<->> before <<-> and <->>, all before <->
op_total_surjective_relation = { "\u{E102}" | "<<->>" }
op_surjective_relation = { "\u{E101}" | "<->>" }
op_total_relation = { "\u{E100}" | "<<->" }

// Arithmetic Operators
op_plus = { "+" }
op_minus = { "−" | "-" }
op_multiply = { "∗" | "*" }
op_divide = { "/" | "÷" }
op_modulo = @{ "mod" ~ word_boundary }
op_exponent = { "^" }
op_range_op = { ".." | "‥" }

// Comparison Operators
op_eq = { "=" }
op_neq = { "≠" | "/=" }
op_lt = { "<" }
op_le = { "≤" | "<=" }
op_gt = { ">" }
op_ge = { "≥" | ">=" }

// Assignment Operators
op_becomes_equal = { "≔" | ":=" }
op_becomes_in = { ":∈" | "::" }
op_becomes_such = { ":∣" | ":|" }

// Delimiters
dot = { "." | "·" }
comma = { "," }
colon = { ":" }
lparen = { "(" }
rparen = { ")" }
lbrace = { "{" }
rbrace = { "}" }
lbracket = { "[" }
rbracket = { "]" }
pipe = { "|" | "∣" }

// ==========================
// Expressions
// ==========================

// Bool expression: bool(P) — converts a predicate to boolean
bool_expr = { kw_bool ~ lparen ~ predicate ~ rparen }

// Primary Expressions
primary_expr = {
    kw_bool_true
  | kw_bool_false
  | op_emptyset
  | kw_nat1
  | kw_nat
  | kw_int
  | bool_expr
  | kw_bool_type
  | integer
  | identifier
  | lparen ~ expression ~ rparen
  | set_enumeration
  | set_comprehension
}

// Set Enumeration: {1, 2, 3}
set_enumeration = {
    lbrace ~ (expression ~ (comma ~ expression)*)? ~ rbrace
}

// Set Comprehension:
// Extended form:   {x · P | E}  (identifiers, dot, predicate, pipe, expression)
// Basic form:      {x | P}      (identifiers, pipe, predicate)
// Expression form: {E | P}      (expression, pipe, predicate) — e.g., {x ↦ y | P}
// PEG ordering: identifier-based forms before expression form, extended before basic
set_comprehension = {
    lbrace ~ typed_identifier ~ (comma ~ typed_identifier)* ~ dot ~ predicate ~ pipe ~ expression ~ rbrace
  | lbrace ~ typed_identifier ~ (comma ~ typed_identifier)* ~ pipe ~ predicate ~ rbrace
  | lbrace ~ expression ~ pipe ~ predicate ~ rbrace
}

// Lambda ident-pattern (per kernel_lang.pdf §3.3.6).
// ⟨ident-pattern⟩ ::= ⟨ident-pattern⟩ { '↦' ⟨ident-pattern⟩ } | '(' ⟨ident-pattern⟩ ')' | ⟨ident⟩ ['⦂' ⟨type⟩]
// Left-associative maplet chain. Each leaf may carry a `⦂` type annotation,
// which is what Rodin's bcc emits after type-checking (`λx⦂T · …`).
ident_pattern = { ident_pattern_atom ~ (op_maplet ~ ident_pattern_atom)* }
ident_pattern_atom = { lparen ~ ident_pattern ~ rparen | typed_identifier }

// Lambda Expression: λ pattern · P ∣ E
lambda_expr = {
    ("λ" | "%") ~ ident_pattern ~ dot ~ predicate ~ pipe ~ expression
}

// Function/Relation Application, Relational Image, and Function Update
// f(x)        function application
// r[S]        relational image
// f{x ↦ y}   Rodin's compact serialization of f <+ {x ↦ y} (functional override).
//              Lowered by the parser to the same AST as the explicit <+ form
//              so consumers don't need to handle a separate variant.
// r∼         postfix inverse
// `dom`/`ran` are closed unary applications: the operand is exactly the
// parenthesized expression, matching Rodin (UnaryExpressionParser mandates
// the paren) and kernel_lang §3.3.6 (⟨unary-op⟩ '(' E ')'). Two consequences:
// - `dom end` no longer greedily swallows a following structural keyword
//   (issue #30): a bare `dom`/`ran` falls through to `identifier`, where the
//   AST builder rejects it as a reserved word, the same way the other
//   builtin words (card, min, …) are handled when not applied.
// - sitting at the function_application base, postfix operators bind to the
//   whole application like in Rodin: `dom(f)(x) = (dom(f))(x)`,
//   `dom(f)∼ = (dom(f))∼`, `dom(f)[S] = (dom(f))[S]`.
closed_unary_expr = { (op_domain | op_range) ~ lparen ~ expression ~ rparen }

// Function application is single-argument (Rodin's FUNIMAGE is binary): `f(x)`,
// with a pair written as a maplet `f(x ↦ y)` — never a comma list `f(a, b)`.
// The `lbrace … rbrace` form is the function-update set `f{x ↦ y, …}` (a set
// of maplets, so it keeps its commas); `lbracket … rbracket` is relational
// image `r[S]`; `op_inverse` is postfix `∼`.
function_application = {
    (closed_unary_expr | primary_expr) ~ (lparen ~ expression ~ rparen | lbracket ~ expression ~ rbracket | lbrace ~ expression ~ (comma ~ expression)* ~ rbrace | op_inverse)*
}

// Unary Expressions
unary_expr = {
    (op_minus | op_powerset1 | op_powerset) ~ unary_expr
  | function_application
}

// Binary Expressions (with precedence, lowest to highest)

// Exponent (non-associative) — highest arithmetic precedence per spec §3.3.6
exponent_expr = {
    unary_expr ~ (op_exponent ~ unary_expr)?
}

// Multiplicative operators (arithmetic only)
multiplicative_expr = {
    exponent_expr ~ ((op_multiply | op_divide | op_modulo) ~ exponent_expr)*
}

// Additive operators (arithmetic only)
additive_expr = {
    multiplicative_expr ~ ((op_plus | op_minus) ~ multiplicative_expr)*
}

// Range/interval operator (non-associative)
relational_expr = {
    additive_expr ~ (op_range_op ~ additive_expr)?
}

// Binary set operators (between the relation arrows and interval in precedence)
set_operator_expr = {
    relational_expr ~ ((op_cartesian | op_intersection | op_union | op_difference
                       | op_overwrite | op_semicolon | op_composition
                       | op_domain_subtract | op_domain_restrict
                       | op_range_subtract | op_range_restrict
                       | op_direct_product | op_parallel_product) ~ relational_expr)*
}

// Relation/function type operators (non-associative, V2). Bind tighter than
// maplet per kernel_lang Table 3.1: group 3 (relation-set arrows) sits inside
// group 2 (pair constructor): `a ↦ b ↔ c = a ↦ (b ↔ c)`.
// PEG ordering: longer operators before shorter sharing a prefix
relation_type_expr = {
    set_operator_expr ~ ((op_total_surj | op_partial_surj | op_bijection | op_total_inj | op_partial_inj
                         | op_total_fn | op_partial_fn
                         | op_total_surjective_relation | op_surjective_relation | op_total_relation
                         | op_relation | op_oftype) ~ set_operator_expr)?
}

// Maplet (lowest binary expression precedence; left-associative, flat-list
// form folded left at AST build).
// Spec p.18 / EVENTB_LANGUAGE_REFERENCE.md: `a ↦ b ↦ c = (a ↦ b) ↦ c`.
maplet_expr = {
    relation_type_expr ~ (op_maplet ~ relation_type_expr)*
}

// Quantified union: ⋃x·P ∣ E  or  UNION x·P ∣ E
quantified_union_expr = {
    kw_UNION ~ typed_identifier ~ (comma ~ typed_identifier)* ~ dot ~ predicate ~ pipe ~ expression
}

// Quantified intersection: ⋂x·P ∣ E  or  INTER x·P ∣ E
quantified_inter_expr = {
    kw_INTER ~ typed_identifier ~ (comma ~ typed_identifier)* ~ dot ~ predicate ~ pipe ~ expression
}

// Top-level expression: quantified forms (lambda, union, inter) tried before binary chain
// because they start with keywords that would otherwise match as identifiers
expression = {
    lambda_expr
  | quantified_union_expr
  | quantified_inter_expr
  | maplet_expr
}

// ==========================
// Predicates
// ==========================

comparison_predicate = {
    expression ~ (op_eq | op_neq | op_le | op_ge | op_not_subset_strict | op_not_subset | op_subset_strict | op_subset | op_lt | op_gt | op_notin | op_in) ~ expression
}

// Predicate function application (e.g., finite(S), partition(S, A, B))
predicate_application = {
    identifier ~ lparen ~ expression ~ (comma ~ expression)* ~ rparen
}

atomic_predicate = {
    comparison_predicate
  | predicate_application
  | kw_true
  | kw_false
  | lparen ~ predicate ~ rparen
}

negation_predicate = {
    op_not ~ negation_predicate
  | (op_forall | op_exists) ~ typed_identifier ~ (comma ~ typed_identifier)* ~ dot ~ predicate
  | atomic_predicate
}

// Conjunction and disjunction share one precedence level: ∧ and ∨ are not a
// precedence ladder, they are incompatible and must be parenthesised when
// mixed (rejected at AST build). Folding them flat keeps the operator sequence
// visible to that check, the same way set operators are folded flat.
connective_predicate = {
    negation_predicate ~ ((op_and | op_or) ~ negation_predicate)*
}

// Implication and equivalence share one precedence level: ⇒ and ⇔ are not a
// precedence ladder either — each is non-associative and the two are mutually
// incompatible, so chaining or mixing them needs parentheses (rejected at AST
// build). Folding them flat keeps the operator sequence visible to that check,
// the same way ∧/∨ above are folded flat.
implies_equiv_predicate = {
    connective_predicate ~ ((op_implies | op_equivalent) ~ connective_predicate)*
}

quantified_predicate = {
    (op_forall | op_exists) ~ typed_identifier ~ (comma ~ typed_identifier)* ~ dot ~ predicate
  | implies_equiv_predicate
}

predicate = {
    quantified_predicate
}

// _no_semi predicate variants: used in BecomesSuchThat actions where ";"
// is the action separator, not forward composition.  Expressions inside
// parentheses/brackets use regular (semicolon-including) rules because the
// closing delimiter naturally bounds the expression.

comparison_predicate_no_semi = {
    action_expression ~ (op_eq | op_neq | op_le | op_ge | op_not_subset_strict | op_not_subset | op_subset_strict | op_subset | op_lt | op_gt | op_notin | op_in) ~ action_expression
}

atomic_predicate_no_semi = {
    comparison_predicate_no_semi
  | predicate_application            // args inside parens — regular expression is fine
  | kw_true
  | kw_false
  | lparen ~ predicate ~ rparen      // inside parens — regular predicate is fine
}

negation_predicate_no_semi = {
    op_not ~ negation_predicate_no_semi
  | (op_forall | op_exists) ~ typed_identifier ~ (comma ~ typed_identifier)* ~ dot ~ predicate_no_semi
  | atomic_predicate_no_semi
}

connective_predicate_no_semi = {
    negation_predicate_no_semi ~ ((op_and | op_or) ~ negation_predicate_no_semi)*
}

implies_equiv_predicate_no_semi = {
    connective_predicate_no_semi ~ ((op_implies | op_equivalent) ~ connective_predicate_no_semi)*
}

quantified_predicate_no_semi = {
    (op_forall | op_exists) ~ typed_identifier ~ (comma ~ typed_identifier)* ~ dot ~ predicate_no_semi
  | implies_equiv_predicate_no_semi
}

predicate_no_semi = {
    quantified_predicate_no_semi
}

// ==========================
// Actions (Event Actions)
// ==========================

// Expression variants that exclude op_semicolon (composition).
// Used inside actions so that ";" unambiguously separates actions in action_list.
exponent_expr_no_semi = {
    unary_expr ~ (op_exponent ~ unary_expr)?
}
multiplicative_expr_no_semi = {
    exponent_expr_no_semi ~ ((op_multiply | op_divide | op_modulo) ~ exponent_expr_no_semi)*
}
additive_expr_no_semi = {
    multiplicative_expr_no_semi ~ ((op_plus | op_minus) ~ multiplicative_expr_no_semi)*
}
relational_expr_no_semi = {
    additive_expr_no_semi ~ (op_range_op ~ additive_expr_no_semi)?
}
set_operator_expr_no_semi = {
    relational_expr_no_semi ~ ((op_cartesian | op_intersection | op_union | op_difference
                               | op_overwrite | op_composition
                               | op_domain_subtract | op_domain_restrict
                               | op_range_subtract | op_range_restrict
                               | op_direct_product | op_parallel_product) ~ relational_expr_no_semi)*
}
relation_type_expr_no_semi = {
    set_operator_expr_no_semi ~ ((op_total_surj | op_partial_surj | op_bijection | op_total_inj | op_partial_inj
                                 | op_total_fn | op_partial_fn
                                 | op_total_surjective_relation | op_surjective_relation | op_total_relation
                                 | op_relation | op_oftype) ~ set_operator_expr_no_semi)?
}
maplet_expr_no_semi = {
    relation_type_expr_no_semi ~ (op_maplet ~ relation_type_expr_no_semi)*
}
// No-semi quantified expression variants: body uses action_expression so that ";"
// is unambiguously the action separator, not forward composition.
lambda_expr_no_semi = {
    ("λ" | "%") ~ ident_pattern ~ dot ~ predicate ~ pipe ~ action_expression
}
quantified_union_expr_no_semi = {
    kw_UNION ~ typed_identifier ~ (comma ~ typed_identifier)* ~ dot ~ predicate ~ pipe ~ action_expression
}
quantified_inter_expr_no_semi = {
    kw_INTER ~ typed_identifier ~ (comma ~ typed_identifier)* ~ dot ~ predicate ~ pipe ~ action_expression
}
action_expression = {
    lambda_expr_no_semi
  | quantified_union_expr_no_semi
  | quantified_inter_expr_no_semi
  | maplet_expr_no_semi
}

action = {
    kw_skip                                                                      // Skip (no-op)
  | identifier ~ lparen ~ action_expression ~ rparen ~ op_becomes_equal ~ action_expression  // Function override: f(x) ≔ E (single arg; pair as maplet f(x ↦ y))
  | identifier ~ (comma ~ identifier)* ~ op_becomes_equal ~ action_expression ~ (comma ~ action_expression)*  // Deterministic (parallel) assignment
  | identifier ~ (comma ~ identifier)* ~ op_becomes_in ~ action_expression     // Non-deterministic assignment (becomes member of)
  | identifier ~ (comma ~ identifier)* ~ op_becomes_such ~ predicate_no_semi   // Non-deterministic assignment (becomes such that)
}

// Standalone action: the same alternatives as `action`, but with the full
// (semicolon-including) expression/predicate rules. Used for single-action
// strings (e.g. Rodin XML assignment attributes), where there is no
// following action for a bare ";" (forward composition) to swallow. The
// `action` rule above keeps its _no_semi variants because actions in a
// THEN block are juxtaposed.
standalone_action = {
    kw_skip                                                                      // Skip (no-op)
  | identifier ~ lparen ~ expression ~ rparen ~ op_becomes_equal ~ expression  // Function override: f(x) ≔ E (single arg; pair as maplet f(x ↦ y))
  | identifier ~ (comma ~ identifier)* ~ op_becomes_equal ~ expression ~ (comma ~ expression)*  // Deterministic (parallel) assignment
  | identifier ~ (comma ~ identifier)* ~ op_becomes_in ~ expression            // Non-deterministic assignment (becomes member of)
  | identifier ~ (comma ~ identifier)* ~ op_becomes_such ~ predicate           // Non-deterministic assignment (becomes such that)
}

labeled_action = {
    label? ~ action
}

// Bound the action list with `event_section_kw` (which includes `kw_end`): an
// action LHS is a keyword-permissive `identifier`, so without the guard the
// terminating `END` parses as a speculative next action. Mirrors the ANY/SEES guards.
action_list = {
    labeled_action ~ (!event_section_kw ~ labeled_action)*
}

// ==========================
// Context
// ==========================

// Structural identifier/reference lists are whitespace-separated — a comma is
// never a separator here (it is meaningful only inside formulas). Items are
// juxtaposed and the list runs until a section keyword opens the next clause.
//
// Follow-set guard (single source of truth): the keywords that may open the
// next context section. Bounds the lists below; silent, since it only ever
// appears inside a negative lookahead.
context_section_kw = _{ kw_extends | kw_sets | kw_constants | kw_axioms | kw_theorems | kw_end }

context_clause_extends = {
    kw_extends ~ component_name ~ (!context_section_kw ~ component_name)*
}

// Set declaration: deferred set (S) or enumerated set (S = {a, b, c})
set_declaration = {
    identifier ~ (op_eq ~ lbrace ~ identifier ~ (comma ~ identifier)* ~ rbrace)?
}

context_clause_sets = {
    kw_sets ~ set_declaration ~ (!context_section_kw ~ set_declaration)*
}

context_clause_constants = {
    kw_constants ~ identifier ~ (!context_section_kw ~ identifier)*
}

// Label: "@" followed by any non-whitespace characters, per the TextEditor EBNF spec:
// "all characters following '@' belong to the label until the next whitespace character is found."
// This supports labels with non-identifier chars like SAF5" from Rodin XML &quot; escapes.
// The optional trailing colon supports eventb-to-txt reference output (e.g. "@inv1:").
label_text = @{ (!(" " | "\t" | "\n" | "\r") ~ ANY)+ }
label = ${ "@" ~ label_text }

// Accepts both orderings: "@label theorem pred" and "theorem @label pred"
// as well as "@label pred", "theorem pred", and bare "pred".
labeled_predicate = {
    (kw_theorem ~ label | label ~ kw_theorem?)? ~ predicate
}

context_clause_axioms = {
    kw_axioms ~ labeled_predicate ~ (labeled_predicate)*
}

// A THEOREMS section is sugar for theorem-flagged axioms: the parser lowers each
// member into `Context.axioms` with `is_theorem = true` (Rodin models a theorem as
// a boolean attribute on an axiom, not as a separate container).
context_clause_theorems = {
    kw_theorems ~ labeled_predicate ~ (labeled_predicate)*
}

context_body = {
    (context_clause_extends | context_clause_sets | context_clause_constants
     | context_clause_axioms | context_clause_theorems)*
}

context = {
    kw_context ~ component_name ~ context_body ~ kw_end
}

// ==========================
// Machine
// ==========================

// Follow-set guard (single source of truth): the keywords that may open the
// next machine section. Bounds the sees/variables lists below; silent, since it
// only ever appears inside a negative lookahead.
machine_section_kw = _{ kw_refines | kw_sees | kw_variables | kw_invariants | kw_theorems | kw_variant | kw_events | kw_end }

machine_clause_refines = {
    kw_refines ~ component_name
}

machine_clause_sees = {
    kw_sees ~ component_name ~ (!machine_section_kw ~ component_name)*
}

machine_clause_variables = {
    kw_variables ~ identifier ~ (!machine_section_kw ~ identifier)*
}

machine_clause_invariants = {
    kw_invariants ~ labeled_predicate ~ (labeled_predicate)*
}

// A THEOREMS section is sugar for theorem-flagged invariants: the parser lowers each
// member into `Machine.invariants` with `is_theorem = true` (Rodin models a theorem
// as a boolean attribute on an invariant, not as a separate container).
machine_clause_theorems = {
    kw_theorems ~ labeled_predicate ~ (labeled_predicate)*
}

machine_clause_variant = {
    kw_variant ~ expression
}

// ==========================
// Events
// ==========================

event_status = {
    kw_status ~ (kw_ordinary | kw_convergent | kw_anticipated)
}

event_refines = {
    kw_refines ~ component_name
}

// Follow-set guard (single source of truth): the keywords that may open the
// next event clause. Bounds the ANY parameter list; silent, since it only ever
// appears inside a negative lookahead.
event_section_kw = _{ kw_where | kw_when | kw_with | kw_witness | kw_then | kw_begin | kw_end }

event_any = {
    kw_any ~ identifier ~ (!event_section_kw ~ identifier)*
}

event_where = {
    (kw_where | kw_when) ~ labeled_predicate ~ (labeled_predicate)*
}

event_with = {
    kw_with ~ labeled_predicate+
}

event_witness = {
    kw_witness ~ labeled_predicate+
}

event_then = {
    (kw_then | kw_begin) ~ action_list
}

event_body = {
    event_status?
  ~ event_refines?
  ~ event_any?
  ~ event_where?
  ~ event_with?
  ~ event_witness?
  ~ event_then?
}

// Inline status (before event keyword): "convergent event foo ..."
event_inline_status = { kw_ordinary | kw_convergent | kw_anticipated }

event = {
    event_inline_status?
  ~ kw_event ~ component_name
  ~ ((kw_extends | kw_refines) ~ component_name)?
  ~ event_body ~ kw_end
}

initialisation_event = {
    kw_event ~ kw_initialisation ~ (kw_extends ~ kw_initialisation)? ~ (kw_then ~ action_list)? ~ kw_end
}

machine_clause_events = {
    kw_events ~ (initialisation_event | event)+
}

// Event-B defines no structural syntax (Abrial: "there is no such syntax in the
// Event-B notation"), and Rodin processes sections as unordered element sets — so
// the non-event clauses may appear in any order. The EVENTS block is the sole
// exception: it is a list of `EVENT … END` closed by the machine `END`, so it is
// the final section. Keeping it terminal is what lets a parse error inside the
// block report just `EVENT`/`END` instead of every clause keyword.
machine_body = {
    (machine_clause_refines | machine_clause_sees | machine_clause_variables
     | machine_clause_invariants | machine_clause_theorems | machine_clause_variant)*
  ~ machine_clause_events?
}

machine = {
    kw_machine ~ component_name ~ machine_body ~ kw_end
}

// ==========================
// Full-input wrapper rules (for parse_*_str functions)
// ==========================
// These silent rules ensure the entire input is consumed when parsing
// standalone expressions, predicates, or actions from XML attributes.
expression_complete = _{ SOI ~ expression ~ EOI }
predicate_complete = _{ SOI ~ predicate ~ EOI }
action_complete = _{ SOI ~ standalone_action ~ EOI }
labeled_predicate_complete = _{ SOI ~ labeled_predicate ~ EOI }

// ==========================
// Root
// ==========================

component = {
    SOI ~ (context | machine) ~ EOI
}

components = {
    SOI ~ (context | machine)+ ~ EOI
}
