strata.gbnf

# Strata/K surface grammar in GBNF (llama.cpp constrained-decoding format).
#
# A projection of docs/grammar.ebnf for the Strata arms of the benchmark
# (metric M): the sampler mask admits only surface syntax, so generate->judge
# iterations measure semantic repair, not grammar unfamiliarity.
#
# Two oracles keep this artifact honest:
#   1. The real parser (strata-front) is the differential oracle:
#      crates/strata-front/tests/gbnf.rs replays every tracked .strata file,
#      every ```strata-tagged fenced example of docs/language.md, book/en and
#      book/ru (membership from the tag, never from a judge's own verdict),
#      a per-construct corpus, and a negative corpus through BOTH grammars.
#   2. The real consumer: .github/gbnf_consumer_check.sh feeds these exact
#      bytes to llama.cpp's official test-gbnf-validator (pinned commit
#      0badc06ab53a8eb96e01242b92ec1365c4465a2a) — a grammar the consumer
#      cannot even load must be red here, not at generation time.
#
# Line discipline (the consumer's, stricter than it looks): a rule lives on
# one line; a newline continues it only after a trailing alternate marker `|`.
# The in-tree GBNF parser enforces the same rule, so a leading-`|`
# continuation is red locally before it ever reaches the consumer.
#
# The committed artifact is export-stable: `strata grammar gbnf` prints
# exactly these bytes.
#
# source: docs/grammar.ebnf sha256=0311398abc3b886d8ca7a2de468cdffa07e2aecc351b4299b726c24bab33feea
# (the test recomputes this hash: editing grammar.ebnf without regenerating
# and re-reviewing this projection is a red test, not a silent drift)
#
# KNOWN OVER-ACCEPTANCE (declared and pinned by tests; the parser stays the
# judge, the mask only reduces syntactic noise):
#   1. Reserved words as identifiers (known_gap_keywords_as_idents): a pure
#      CFG cannot subtract the keyword list from the identifier rule, so the
#      grammar admits e.g. `not(a).` where the lexer keywordizes `not`.
#   2. Numeric value ranges (known_gap_numeric_ranges): a CFG does not count —
#      integer literals beyond i64 and Prov_k bounds outside 1..=u32::MAX are
#      grammatical here and rejected by the lexer/parser (E0001/E0002).
# No other over-acceptance class is known; the corpora are finite evidence,
# not a proof. The `?prob`/`?grad` maximal-munch boundary IS encoded exactly.

root ::= ws (item ws)*
item ::= domain-decl | pred-decl | neural-decl | rule | fact | input-decl |
        query | pragma | forbid-decl | example-decl | total-on-decl

# --- declarations ---
domain-decl ::= "domain" ws1 const-ident ws "."
pred-decl ::= "pred" ws1 const-ident ws "(" ws arg-type-list? ws ")" ws ":" ws annotation effects ws "."
arg-type-list ::= arg-type (ws "," ws arg-type)*
arg-type ::= "int" | "term" ws1 const-ident | const-ident
annotation ::= "Bool" | "Trop" | "Prov_k" (ws "(" ws integer ws ")")? | "Prov"
effects ::= (ws1 effect)*
effect ::= "total" | "partial" | "complete" | "sound_only" | "deterministic" |
           "stochastic"

# neural predicate — its facts are the model's soft outputs (p :: n(...))
neural-decl ::= "neural" ws1 const-ident ws "(" ws const-ident-list? ws ")" ws1 "from" ws1 "model" ws1 string ws "."
const-ident-list ::= const-ident (ws "," ws const-ident)*

# --- rules and facts ---
rule ::= atom ws ":-" ws body ws "."
body ::= literal (ws "," ws literal)*
literal ::= ("not" ws1)? atom | comparison

# A comparison guard: scalar operands only. `<=`/`>=`/`!=` need no munch
# tricks here: after a bare "<" the next thing must be a cmp-term and no
# cmp-term starts with "=", so the two-char branch is the only path.
comparison ::= cmp-term ws cmp-op ws cmp-term
cmp-term ::= var-ident | integer | const-ident
cmp-op ::= "!=" | "<=" | ">=" | "=" | "<" | ">"
atom ::= const-ident ws "(" ws term-list? ws ")"
term-list ::= term (ws "," ws term)*
term ::= aggregate | var-ident | integer | compound | const-ident
compound ::= const-ident ws "(" ws term-list? ws ")"
aggregate ::= agg-op ws "<" ws var-ident ws ">"
agg-op ::= "min" | "max" | "sum" | "count" | "prob_or"

fact ::= (number ws "::" ws)? atom ws "."
input-decl ::= "input" ws1 const-ident ws1 "from" ws1 string ws "."

# --- contracts: `forbid` must end with no witnesses, `example` with at least one ---
forbid-decl ::= "forbid" ws1 const-ident ws ":" ws body ws "."
example-decl ::= "example" ws1 const-ident ws ":" ws body ws "."

# total_on: the cases partition the domain. Atoms bind variables only —
# grammatical here, so the mask cannot emit a constant argument; identical
# variable tuples across atoms stay a checker rule (a CFG cannot compare them).
total-on-decl ::= "total_on" ws1 const-ident ws ":" ws flat-atom ws "->" ws flat-atom (ws "|" ws flat-atom)* ws "."
flat-atom ::= const-ident ws "(" ws var-ident-list? ws ")"
var-ident-list ::= var-ident (ws "," ws var-ident)*

# --- queries ---
# Maximal munch, encoded: `?prob`/`?grad` lex as single tokens, so `?prob(x).`
# is NOT `?` applied to prob(x) — it is a ?prob query missing its atom, a parse
# error. The collision exists only when the name follows `?` with no space:
# the adjacent bare-`?` branch excludes predicate names beginning with "prob"
# or "grad" (qname), while `? prob(x).` — whitespace defeats the munch — stays
# reachable through the whitespace branch with an unrestricted atom.
query ::= ("?prob" | "?grad") ws atom ws "." | "?" ws1 atom ws "." |
          "?" atom-q ws "."
atom-q ::= qname ws "(" ws term-list? ws ")"
qname ::= [a-fh-oq-z] ident-tail | "g" g1? | "p" p1?
g1 ::= [A-Za-qs-z0-9_] ident-tail | "r" g2?
g2 ::= [A-Zb-z0-9_] ident-tail | "a" g3?
g3 ::= [A-Za-ce-z0-9_] ident-tail
p1 ::= [A-Za-qs-z0-9_] ident-tail | "r" p2?
p2 ::= [A-Za-np-z0-9_] ident-tail | "o" p3?
p3 ::= [A-Za-ac-z0-9_] ident-tail

# --- module pragmas ---
pragma ::= ("@terms" | "@asp") ws "."

# --- lexical ---
var-ident ::= [A-Z_] ident-tail
const-ident ::= [a-z] ident-tail
ident-tail ::= [A-Za-z0-9_]*
integer ::= "-"? [0-9]+
number ::= "-"? [0-9]+ ("." [0-9]+)?
string ::= "\"" [^"]* "\""
comment ::= "%" [^\n]*
ws ::= ([ \t\r\n] | comment)*
ws1 ::= ([ \t\r\n] | comment) ws