grammar.ebnf

(* Strata/K surface grammar — source of truth for strata-front. [FRONT-1, D8]

   Priority: optimized for LLM writing (D3). Datalog `:-`, mandatory predicate
   signatures, Prolog lexical convention (Var = Uppercase/_-leading, const =
   lowercase). The WHOLE language surface is grammatical (D5); constructs outside
   Phase-0 execution parse into valid High-IR and then get a stable
   "not implemented in Phase 0" diagnostic — they are never syntax errors.

   Surface is a projection of High-IR (D2): parse(surface) -> High-IR, and the
   canonical printer is the inverse on canonical form. *)

program      = { item } ;
item         = domain_decl | pred_decl | neural_decl | rule | fact | input_decl
             | query | pragma | forbid_decl | example_decl | total_on_decl ;

(* --- declarations --- *)
domain_decl  = "domain" , const_ident , "." ;
pred_decl    = "pred" , const_ident , "(" , [ arg_type { "," , arg_type } ] , ")" ,
               ":" , annotation , { effect } , "." ;
arg_type     = const_ident        (* a declared domain *)
             | "int"              (* i64 column / Trop weight source *)
             | "term" , const_ident ;  (* @terms structural-term column *)
annotation   = "Bool" | "Trop" | "Prov"
             | "Prov_k" , [ "(" , integer , ")" ] ;    (* bare Prov_k = Prov_k(3); k ≥ 1 *)
effect       = "total" | "partial" | "complete" | "sound_only"
             | "deterministic" | "stochastic" ;

(* neural predicate — its facts are the model's soft outputs (p :: n(...)) *)
neural_decl  = "neural" , const_ident , "(" , [ const_ident { "," , const_ident } ] , ")" ,
               "from" , "model" , string , "." ;

(* --- rules and facts --- *)
rule         = atom , ":-" , body , "." ;
body         = literal , { "," , literal } ;
literal      = [ "not" ] , atom | comparison ;

(* A comparison guard: a pure filter over bound values — `=` is a test, never
   unification. Operands are scalars; the checker enforces boundedness by a
   positive literal (like negation) and kind discipline: order ops are
   integer-only, equality stays within one kind (E1015). *)
comparison   = cmp_term , cmp_op , cmp_term ;
cmp_term     = var_ident | const_ident | integer ;
cmp_op       = "=" | "!=" | "<" | "<=" | ">" | ">=" ;
atom         = const_ident , "(" , [ term { "," , term } ] , ")" ;
term         = var_ident | const_ident | integer | aggregate | compound ;
compound     = const_ident , "(" , [ term { "," , term } ] , ")" ;  (* @terms constructor *)
aggregate    = agg_op , "<" , var_ident , ">" ;     (* head-only, e.g. count<Y> *)
agg_op       = "min" | "max" | "sum" | "count" | "prob_or" ;

fact         = [ annotated ] , atom , "." ;
annotated    = number , "::" ;   (* integer :: -> Trop weight; float :: -> probabilistic fact *)

input_decl   = "input" , const_ident , "from" , string , "." ;

(* --- contracts: after the fixpoint, the body must have no witnesses --- *)
forbid_decl  = "forbid" , const_ident , ":" , body , "." ;
example_decl = "example" , const_ident , ":" , body , "." ;  (* positive dual: body must have a witness *)

(* total_on: the cases partition the domain — every domain tuple in at least
   one case (exhaustive) and at most one (exclusive). Sugar over forbid +
   stratified negation; the verdict reports ONE obligation of kind total_on.
   Atoms bind pairwise-distinct variables only, identical tuples across atoms
   (the tuple identity is a checker rule; variables-only is grammatical). *)
total_on_decl = "total_on" , const_ident , ":" , flat_atom , "->" ,
                flat_atom , { "|" , flat_atom } , "." ;
flat_atom     = const_ident , "(" , [ var_ident { "," , var_ident } ] , ")" ;

(* --- queries: plain, marginal (режим B), and gradient --- *)
query        = ( "?" | "?prob" | "?grad" ) , atom , "." ;

(* --- module pragmas: @terms structural terms, @asp stable models --- *)
pragma       = ( "@terms" | "@asp" ) , "." ;

(* --- lexical --- *)
var_ident    = ( uppercase | "_" ) , { ident_char } ;
const_ident  = lowercase , { ident_char } ;   (* also predicate and domain names *)
ident_char   = letter | digit | "_" ;
integer      = [ "-" ] , digit , { digit } ;
number       = integer | ( integer , "." , digit , { digit } ) ;
string       = '"' , { ? any char except '"' ? } , '"' ;
comment      = "%" , { ? any char except newline ? } ;   (* trivia; attached to nearest node *)

(* Reserved words (cannot be predicate/domain/variable names): pred, domain,
   input, from, model, neural, forbid, example, total_on, not, int, term,
   min, max, sum, count, prob_or,
   Bool, Trop, Prov, Prov_k, total, partial, complete, sound_only,
   deterministic, stochastic. *)