// nibli KR grammar — THE EXECUTABLE SPEC (NIBLI_KR.md §15, full v0.1 surface).
//
// This file is the normative grammar: pest_derive compiles it into the parser,
// so grammar and implementation cannot drift (the property that motivated the
// 2026-07-12 switch from the hand recursive-descent parser).
//
// Scannerless discipline: pest has no separate lexer, so the keyword-boundary
// hazard (`everyday` must NEVER parse as `every` + `day`) is handled by two
// mechanical rules, both pinned by behavioral tests in parser.rs:
// 1. every keyword rule is SELF-GUARDED with `~ !ident_char`, so a keyword
// never matches a prefix of a longer identifier — and because each
// alternative guards itself, alternation order can't recreate the
// `you`/`you_all` ordered-choice bug;
// 2. `ident` starts with `!keyword`, so a keyword can never be an identifier.
//
// Structure rules (no `@`/`$`) skip WHITESPACE/COMMENT between elements; atomic
// `@` and compound-atomic `$` rules do not. Two rules are DELIBERATELY
// compound-atomic because they denote word identity where internal whitespace
// or comments would be a hazard:
// - `selected` (`loves.loved` — the place selector): adjacency on BOTH sides
// of the dot keeps the selector from colliding with the statement
// terminator (`Kim = every dog. eats(me).` must be two statements; see
// NIBLI_KR O8). A selected restr also takes NO linked args, so the
// compact collision `Kim = every dog.eats(me).` is a PARSE ERROR, never a
// silent statement merge. `selected` must stay FIRST in its alternation —
// pest commits to a succeeding alternative and never re-opens it.
// - `pred_name` (`a+b` — zei compounds): compound identity may not contain
// whitespace or comments (`computer + user(…)` is a parse error).
//
// The §6 errata (prefix ordering, `~past P`, `~~P`, prefixes/`~` over compound
// claims), positional-before-named args, `exactly N` integrality, the
// mandatory-`it` rule for full-claim clause bodies, and all dictionary-driven
// checks (resolve.rs) are deliberately NOT encoded here: `modifiers` and the
// shapes below parse permissively and the walker/resolver reject with
// TARGETED, positioned errors — generic "expected …" messages would bury the
// spec guidance.
WHITESPACE = _{ " " | "\t" | "\r" | "\n" }
COMMENT = _{ ("#" ~ (!"\n" ~ ANY)*) | ("/*" ~ (!"*/" ~ ANY)* ~ "*/") }
ident_char = _{ ASCII_ALPHA_LOWER | ASCII_DIGIT | "_" }
// ── Keywords (NIBLI_KR §2; single source nibli-kr-dictionary/src/reserved.rs,
// pinned by the grammar↔reserved-list conformance test) ──
kw_all = @{ "all" ~ !ident_char }
kw_also = @{ "also" ~ !ident_char }
kw_amount = @{ "amount" ~ !ident_char }
kw_concept = @{ "concept" ~ !ident_char }
kw_event = @{ "event" ~ !ident_char }
kw_every = @{ "every" ~ !ident_char }
kw_exactly = @{ "exactly" ~ !ident_char }
kw_fact = @{ "fact" ~ !ident_char }
kw_future = @{ "future" ~ !ident_char }
kw_it = @{ "it" ~ !ident_char }
kw_it_a = @{ "it_a" ~ !ident_char }
kw_it_e = @{ "it_e" ~ !ident_char }
kw_it_i = @{ "it_i" ~ !ident_char }
kw_it_o = @{ "it_o" ~ !ident_char }
kw_it_u = @{ "it_u" ~ !ident_char }
kw_may = @{ "may" ~ !ident_char }
kw_me = @{ "me" ~ !ident_char }
kw_must = @{ "must" ~ !ident_char }
kw_no = @{ "no" ~ !ident_char }
kw_now = @{ "now" ~ !ident_char }
kw_past = @{ "past" ~ !ident_char }
kw_property = @{ "property" ~ !ident_char }
kw_slot = @{ "slot" ~ !ident_char }
kw_some = @{ "some" ~ !ident_char }
kw_that = @{ "that" ~ !ident_char }
kw_the = @{ "the" ~ !ident_char }
kw_this = @{ "this" ~ !ident_char }
kw_via = @{ "via" ~ !ident_char }
kw_we = @{ "we" ~ !ident_char }
kw_we_all = @{ "we_all" ~ !ident_char }
kw_we_others = @{ "we_others" ~ !ident_char }
kw_where = @{ "where" ~ !ident_char }
kw_yonder = @{ "yonder" ~ !ident_char }
kw_you = @{ "you" ~ !ident_char }
kw_you_all = @{ "you_all" ~ !ident_char }
// Longest-first within shared-prefix families as belt-and-suspenders (the
// per-alternative guards already make order semantically irrelevant).
keyword = _{
kw_we_others | kw_we_all | kw_you_all
| kw_it_a | kw_it_e | kw_it_i | kw_it_o | kw_it_u
| kw_all | kw_also | kw_amount | kw_concept | kw_event | kw_every
| kw_exactly | kw_fact | kw_future | kw_it | kw_may | kw_me | kw_must
| kw_no | kw_now | kw_past | kw_property | kw_slot | kw_some
| kw_that | kw_the | kw_this | kw_via | kw_we | kw_where | kw_yonder | kw_you
}
// ── Identifier classes / literals ──
ident = @{ !keyword ~ ASCII_ALPHA_LOWER ~ ident_char* }
name = @{ ASCII_ALPHA_UPPER ~ (ASCII_ALPHANUMERIC | "_")* }
var = @{ "$" ~ ASCII_ALPHA_LOWER ~ ident_char* }
number = @{ ASCII_DIGIT+ ~ ("." ~ ASCII_DIGIT+)? }
// `\"` and `\\` are the only escapes; anything else after `\` fails the match
// (fail closed). Payloads may carry arbitrary UTF-8 — the ASCII-only rule
// applies to syntax, not string payloads (NIBLI_KR §9). No other rule
// matches non-ASCII, so the ASCII-only property holds automatically.
string = @{ "\"" ~ (("\\" ~ ("\"" | "\\")) | (!("\"" | "\\" | "\n") ~ ANY))* ~ "\"" }
// ── File / statements ──
file = { SOI ~ statement* ~ EOI }
statement = { claim ~ "." }
// ── Claims (NIBLI_KR §6) ──
// The three claim families have pairwise-incompatible commit points (`all`,
// det-keyword…`$var:`, everything else), so pest's alternative-failure
// backtracking keeps e.g. `every dog = Adam.` an equality, never a broken
// det_block.
claim = { prenex | det_block | impl_chain }
// `all $x, $y: C` — nested ForAll wrapping the body DIRECTLY (prenex shape).
prenex = { kw_all ~ var ~ ("," ~ var)* ~ ":" ~ claim }
// `every dog $d: C` — named-binder block form (emission shape pinned by O7).
det_block = { block_det ~ restr ~ var ~ ":" ~ claim }
block_det = { (kw_every ~ kw_the?) | kw_some | (kw_exactly ~ number ~ kw_the?) | kw_no | kw_the }
// The operator ladder (tightest first: modifiers · & · | · ^ · <-> · ->).
impl_chain = { iff_chain ~ (op_impl ~ impl_chain)? } // -> right-assoc
iff_chain = { xor_chain ~ (op_iff ~ xor_chain)* }
xor_chain = { or_chain ~ (op_xor ~ or_chain)* }
or_chain = { and_chain ~ (op_or ~ and_chain)* }
and_chain = { unary ~ (op_and ~ unary)* }
op_impl = { "->" }
op_iff = { "<->" }
op_xor = { "^" }
op_or = { "|" }
op_and = { "&" }
// Modifiers parse PERMISSIVELY in any order/count; the walker enforces the §6
// shape (≤1 deontic, ≤1 tense, deontic-before-tense, ≤1 `~`, `~` innermost)
// with targeted errors.
unary = { modifier* ~ atom }
modifier = { kw_must | kw_may | kw_past | kw_now | kw_future | tilde }
tilde = { "~" }
atom = { paren | predication | equality }
paren = { "(" ~ claim ~ ")" }
predication = { pred_seq ~ args ~ tag* }
// `via cause(X)` — BAI/fi'o modal tag (NIBLI_KR §5).
tag = { kw_via ~ pred_name ~ "(" ~ term ~ ")" }
args = { "(" ~ (arg ~ ("," ~ arg)*)? ~ ")" }
arg = { (label ~ ":")? ~ term }
label = { ident }
equality = { term ~ "=" ~ term }
// ── Predicate sequences (pair; NIBLI_KR §5) ──
pred_seq = { pred_unit+ } // 2+ units = pair, LAST = head
pred_unit = { ("[" ~ pred_seq ~ "]") | pred_name }
pred_name = ${ ident ~ ("+" ~ ident)* } // a+b zei compound — word identity,
// compound-atomic (no WS/comments)
// ── Terms (NIBLI_KR §3) ──
term = { underscore | question | number | string | var | keyterm
| abstraction | det_phrase | rigid }
underscore = { "_" }
question = { "?" }
keyterm = {
kw_we_others | kw_we_all | kw_you_all
| kw_it_a | kw_it_e | kw_it_i | kw_it_o | kw_it_u
| kw_me | kw_you | kw_we | kw_this | kw_that | kw_yonder | kw_it | kw_slot
}
abstraction = { abs_kind ~ "{" ~ claim ~ "}" }
abs_kind = { kw_event | kw_fact | kw_property | kw_amount | kw_concept }
rigid = { name ~ rel_cl* } // Adam where dog — rel clause on a
// rigid term
det_phrase = { det ~ restr }
det = { kw_some | (kw_every ~ kw_the?) | kw_the
| (kw_exactly ~ number ~ kw_the?) | kw_no }
// ── Restrictors (NIBLI_KR §4) ──
// `selected` first — see the header note (PEG commit + O8).
restr = { tilde? ~ (selected | pred_seq ~ args?) ~ rel_cl* }
selected = ${ ident ~ "." ~ ident } // place selector: every loves.loved
rel_cl = { (kw_where | kw_also) ~ clause_body }
// Bare-predicate sugar: a body with no argument list applies to `it` at x1.
// The claim branch is tried first; full-claim bodies must contain `it`
// (mandatory-`it`, enforced by the walker per NIBLI_KR §7).
clause_body = { claim | (tilde? ~ pred_seq) }