grammar.ebnf

(* SPDX-License-Identifier: MPL-2.0 *)
(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *)
(*                                                          *)
(* 007 Agent Meta-Language — Formal Grammar (EBNF)          *)
(* Version: 0.5.0-draft                                     *)
(* Date: 2026-03-24                                         *)
(*                                                          *)
(* INVARIANT 1 (Harvard Architecture):                      *)
(*   data_expr CANNOT contain control_stmt.                 *)
(*   control_stmt CANNOT appear in data context.            *)
(*   This makes agent injection a parse error.              *)
(*                                                          *)
(* INVARIANT 2 (Hermeneutic Instrumentation):               *)
(*   Every branch point MAY carry `given` clauses (Layer 4  *)
(*   decision contexts) and `traced` instrumentation.       *)
(*   `given` clauses are Data expressions — they cannot     *)
(*   contain control flow. Decision traces are immutable    *)
(*   Data records protected by Harvard separation.          *)
(*                                                          *)
(* DESIGN NOTE: This grammar optimises for ZERO AMBIGUITY   *)
(* over brevity. Agents generate 007; they don't type it.   *)
(* Every construct is explicitly marked. No syntactic sugar  *)
(* that could blur the data/control boundary.               *)

(* ========================================================= *)
(* 1. TOP-LEVEL PROGRAM STRUCTURE                            *)
(* ========================================================= *)

program = { top_level_decl } ;

top_level_decl = agent_decl
               | supervisor_decl
               | choreography_decl
               | protocol_decl
               | behaviour_decl
               | locale_decl
               | type_decl
               | function_decl
               | import_decl
               | data_binding ;

(* ========================================================= *)
(* 2. AGENT DECLARATIONS                                     *)
(* ========================================================= *)

agent_decl = "agent" , agent_name , [ "(" , agent_params , ")" ] ,
             [ "implements" , protocol_role_list ] ,
             [ "on" , "locale" , locale_expr ] ,
             "{" , agent_body , "}" ;

agent_name = upper_ident ;

agent_params = agent_param , { "," , agent_param } ;

(* agent_param — see Section 18.1 for extended definition     *)
(* with budget annotation                                     *)

agent_body = { agent_member } ;

agent_member = data_block
             | control_block
             | state_decl
             | residue_decl ;

(* ========================================================= *)
(* 3. HARVARD ARCHITECTURE — DATA LANGUAGE                   *)
(* ========================================================= *)
(* CRITICAL: data_block and data_expr are TOTAL and PURE.    *)
(* No loops, no conditionals, no I/O, no agent operations.   *)
(* Arithmetic: +, -, *, /, % (all total; division by zero    *)
(* yields Unit, preserving totality).                         *)
(* Only @total and @pure function calls.                     *)
(*                                                           *)
(* The Data Language serves two roles:                        *)
(*   1. SAFETY — prevents injection (original purpose)       *)
(*   2. EPISTEMOLOGICAL — structures the hermeneutic act     *)
(*      by cleanly separating what agents KNOW from what     *)
(*      agents DO, making interpretation observable           *)

data_block = "@total" , "data" , [ ident , "=" ] ,
             "{" , data_fields , "}" ;

data_binding = "@total" , "data" , ident , "=" , data_expr ;

data_fields = data_field , { "," , data_field } , [ "," ] ;

data_field = ident , ":" , data_expr ;

data_expr = data_additive ;

data_additive = data_multiplicative , { ( "+" | "-" ) , data_multiplicative } ;

data_multiplicative = data_term , { ( "*" | "/" | "%" ) , data_term } ;

data_term = data_literal
          | data_record
          | data_list
          | data_fn_call         (* @total/@pure functions only *)
          | data_field_access
          | ident
          | "(" , data_expr , ")" ;

data_literal = integer_literal
             | float_literal
             | string_literal
             | bool_literal ;

data_record = "{" , data_fields , "}" ;

data_list = "[" , [ data_expr , { "," , data_expr } , [ "," ] ] , "]" ;

data_fn_call = pure_fn_name , "(" , [ data_expr , { "," , data_expr } ] , ")" ;

data_field_access = data_term , "." , ident ;

pure_fn_name = ident ;  (* Must resolve to @total or @pure function *)

(* ========================================================= *)
(* 4. HARVARD ARCHITECTURE — CONTROL LANGUAGE                *)
(* ========================================================= *)
(* Control context: Turing-complete, may have side effects.  *)
(* Agent behaviour lives here.                               *)

control_block = [ "@impure" ] , "control" , "{" , { control_item } , "}" ;

control_item = handler
             | control_stmt ;

handler = "on" , handler_event , "(" , [ param_list ] , ")" ,
          [ "->" , control_expr ]
        | "on" , handler_event , "(" , [ param_list ] , ")" ,
          "{" , { control_stmt } , "}" ;

handler_event = "receive" | "error" | "terminate"
              | "timeout" | "child_crash" | ident ;

control_stmt = let_binding
             | set_stmt
             | send_stmt
             | spawn_stmt
             | match_stmt
             | if_stmt
             | branch_stmt
             | loop_stmt
             | return_stmt
             | reversible_block
             | irreversible_block
             | reverse_named
             | reverse_block
             | control_expr , ";" ;

let_binding = [ "linear" ] , "let" , pattern , "=" , control_expr ;

(* `set <field> = <expr>` assigns to a declared agent `state` field      *)
(* (mutable agent state). The type checker requires <field> to name a    *)
(* `state` on the enclosing agent.                                       *)
set_stmt = "set" , ident , "=" , control_expr ;

(* Natural-language order: send message to target.                *)
(* Function-call order preserved for backward compat.             *)
(* Agent-ergonomic: natural language reads left-to-right.         *)
send_stmt = "send" , control_expr , "to" , control_expr
          | "send_final" , control_expr , "to" , control_expr
          | "send" , "(" , control_expr , "," , control_expr , ")"
          | "send_final" , "(" , control_expr , "," , control_expr , ")" ;

spawn_stmt = [ "linear" ] , "let" , ident , "=" ,
             "spawn" , agent_name ,
             "(" , spawn_args , ")" ;

spawn_args = spawn_arg , { "," , spawn_arg } ;

spawn_arg = "caps" , ":" , capability_list
          | "behaviour" , ":" , ( behaviour_ref | behaviour_hash )
          | ident , ":" , control_expr ;

match_stmt = "match" , control_expr , "{" ,
             { "|" , pattern , "->" , control_expr_or_block } ,
             "}" ;

if_stmt = "if" , control_expr ,
          "{" , { control_stmt } , "}" ,
          [ "else" , "{" , { control_stmt } , "}" ] ;

loop_stmt = "loop" , [ ident ] ,
            "{" , { control_stmt } , "}" ;

return_stmt = "return" , [ control_expr ] ;

control_expr = control_primary
             | control_expr , "." , ident , [ "(" , arg_list , ")" ]
             | "exchange" , "(" , control_expr , "," , control_expr , ")"
             | "receive" , "(" , ")"
             | "migrate" , "(" , control_expr , "," ,
               "from" , ":" , locale_expr , "," ,
               "to" , ":" , locale_expr , ")"
             | fn_call
             | control_expr , binop , control_expr ;

control_expr_or_block = control_expr
                      | "{" , { control_stmt } , "}" ;

control_primary = data_literal
                | ident
                | data_record
                | data_list
                | "(" , control_expr , ")" ;

fn_call = ident , "(" , [ arg_list ] , ")" ;

arg_list = control_expr , { "," , control_expr } ;

binop = "+" | "-" | "*" | "/" | "%"
      | "==" | "!=" | "<" | ">" | "<=" | ">="
      | "and" | "or" | "++" ;

(* Note: the binop list above is the full Control-context     *)
(* operator set. Data context permits scalar arithmetic       *)
(* (+, -, *, /, %) via the data_additive / data_multiplicative*)
(* productions below. Division and modulo are total:          *)
(* n/0 = Unit and n%0 = Unit, preserving termination. JTV's   *)
(* historical addition-only restriction has been generalised  *)
(* in 007 — see §3 header, docs/DESIGN-RATIONALE.adoc, and    *)
(* proofs/idris2/Harvard.idr for the current formal model.    *)

(* ========================================================= *)
(* 5. BRANCH STATEMENTS — THE HERMENEUTIC LAYER (Layer 4)   *)
(* ========================================================= *)
(* Branch statements are where agent JUDGEMENT occurs.        *)
(* The grammar provides two constructs for Layer 4:           *)
(*                                                            *)
(*   `given`  — what the agent sees when it decides           *)
(*              (Data expr: cannot contain control flow)       *)
(*                                                            *)
(*   `traced` — instrumentation for observing decisions       *)
(*              (Data expr: immutable, tamper-proof)           *)
(*                                                            *)
(* Together these form 007's "telescope" — the instrument     *)
(* through which the structure of agent interpretive acts     *)
(* may become observable.                                      *)
(*                                                            *)
(* CRITICAL: `given` clauses are DATA. They are subject to    *)
(* Harvard separation. An agent's decision context CANNOT     *)
(* contain executable code. This is what makes the            *)
(* hermeneutic act observable — data and control are cleanly  *)
(* separated, so interpretation doesn't blur with execution.  *)

(* branch_stmt — see Section 18.2 for extended definition     *)
(* with speculative and cached modifiers                       *)

branch_arm = "|" , branch_label , [ given_clause ] ,
             "->" , branch_body ;

branch_label = ident
             | upper_ident , [ "(" , pattern_list , ")" ] ;

branch_body = control_expr_or_block
            | "{" , { control_stmt } , [ trace_clause ] , "}" ;

(* --------------------------------------------------------- *)
(* 5.1 THE `given` CLAUSE                                    *)
(* --------------------------------------------------------- *)
(* Declares what information is RELEVANT to this branch.      *)
(* Does NOT determine the choice — shapes the interpretive    *)
(* context. The agent reads the `given` and interprets.       *)
(*                                                            *)
(* Properties:                                                *)
(*   - `given` is a Data expression (Harvard-separated)       *)
(*   - `given` clauses may overlap between branches           *)
(*   - `given` is not exhaustive — agents may consider        *)
(*     information beyond what is listed                       *)
(*   - `given` is part of the branch's TYPE — changing what   *)
(*     is given changes the type signature of the decision    *)
(*   - `given` with a predicate (data_predicate) suggests     *)
(*     conditions under which this branch is coherent, but    *)
(*     does NOT enforce them — the agent may override         *)

(* given_clause — see Section 18.4 for extended definition    *)
(* with @focus attention budgeting                             *)

given_items = given_item , { "," , given_item } , [ "," ] ;

given_item = data_expr                       (* bare evidence *)
           | ident , ":" , data_expr         (* named evidence *)
           | data_predicate ;                (* suggested condition *)

(* Predicates in `given` are SUGGESTIONS, not guards.         *)
(* They indicate when this branch would be coherent, but      *)
(* the agent has interpretive freedom to override.            *)
(* This is the de Man parabasis — the ability to turn away.   *)

data_predicate = data_expr , pred_op , data_expr ;

pred_op = ">" | "<" | ">=" | "<=" | "==" | "!=" ;

(* --------------------------------------------------------- *)
(* 5.2 THE `trace` CLAUSE                                    *)
(* --------------------------------------------------------- *)
(* Captures the agent's self-report of its interpretive act.  *)
(* Recorded immutably by the runtime for later analysis.      *)
(*                                                            *)
(* The trace is DATA — Harvard-separated. The agent cannot    *)
(* inject control flow into its own trace. The observation    *)
(* must not disturb the phenomenon.                           *)
(*                                                            *)
(* Traces accumulate into decision trace datasets that may    *)
(* reveal the structure of Layer 4 — or may reveal that       *)
(* Layer 4 has no structure. Either result is valuable.       *)

trace_clause = "trace" , "{" , trace_fields , "}" ;

trace_fields = trace_field , { "," , trace_field } , [ "," ] ;

trace_field = ident , ":" , data_expr ;

(* A trace record, as stored by the runtime, contains:        *)
(*   - branch_id: the `traced` label (string)                 *)
(*   - branch_options: all available arms                      *)
(*   - given_contexts: the `given` clause of each arm         *)
(*   - chosen: which arm was selected                          *)
(*   - trace_report: the agent's `trace` self-report          *)
(*   - timestamp: when the decision was made                   *)
(*   - agent_id: which agent instance made it                  *)
(*   - hermeneutic_context: full Data state at decision time   *)
(*                                                             *)
(* This record is a Data value. It cannot be modified after    *)
(* creation. It cannot contain control flow. It is an          *)
(* immutable fossil of an interpretive act.                    *)

(* ========================================================= *)
(* 6. SUPERVISORS                                            *)
(* ========================================================= *)

supervisor_decl = "supervisor" , upper_ident ,
                  "{" , supervisor_body , "}" ;

supervisor_body = { supervisor_field } ;

supervisor_field = "strategy" , ":" , strategy_name
                 | "max_restarts" , ":" , integer_literal , "per" , integer_literal , time_unit
                 | "children" , ":" , "[" , child_list , "]"
                 | handler ;

strategy_name = "one_for_one" | "one_for_all" | "rest_for_one" ;

time_unit = "s" | "ms" | "m" | "h" ;

child_list = child_spec , { "," , child_spec } , [ "," ] ;

child_spec = "agent" , agent_name , "(" , spawn_args , ")" ;

(* ========================================================= *)
(* 7. SESSION TYPES AND PROTOCOLS                            *)
(* ========================================================= *)

protocol_decl = "session" , "protocol" , upper_ident ,
                "{" , { protocol_step } , "}" ;

protocol_step = message_step
              | protocol_branch_step
              | protocol_loop_step
              | rec_step ;

message_step = role_name , "->" , role_name , ":" ,
               upper_ident , [ "(" , typed_fields , ")" ] ;

(* Protocol branches also support `given` clauses.            *)
(* At the protocol level, `given` declares what information   *)
(* the DECIDING role should consider for each branch.         *)
(* This is part of the protocol's type — both sides agree     *)
(* on what evidence is relevant to each branch.               *)

protocol_branch_step = "branch" , [ "by" , role_name ] ,
                       "{" , { protocol_branch_arm } , "}" ;

protocol_branch_arm = "|" , ident , [ given_clause ] ,
                      "->" , { protocol_step } ;

protocol_loop_step = "loop" , ident , "{" , { protocol_step } , "}" ;

rec_step = "rec" , upper_ident ;

role_name = upper_ident ;

protocol_role_list = protocol_role , { "," , protocol_role } ;

protocol_role = upper_ident , "." , upper_ident ;

(* ========================================================= *)
(* 8. CHOREOGRAPHIES                                         *)
(* ========================================================= *)

choreography_decl = "choreography" , ident ,
                    "(" , choreo_params , ")" ,
                    "{" , { choreo_step } , "}" ;

choreo_params = choreo_param , { "," , choreo_param } ;

choreo_param = ident , ":" , type_expr ;

(* choreo_step — see Section 18.5 for extended definition     *)
(* with batch block                                            *)

choreo_comm = ident , "->" , ident , ":" ,
              ident , [ "(" , [ arg_list ] , ")" ] ;

choreo_parallel = "parallel" , [ "for" , ident , "in" , ident ] ,
                  "{" , { choreo_step } , "}" ;

(* Choreographic branches also support `given` — declaring    *)
(* what the deciding participant sees at the global level.     *)
(* The projection algorithm preserves `given` clauses into    *)
(* the projected local code, so each participant knows what   *)
(* evidence the decider is considering.                        *)

choreo_branch = "branch" , [ "traced" , string_literal ] ,
                "{" , { choreo_branch_arm } , "}" ;

choreo_branch_arm = "|" , ident , [ given_clause ] ,
                    "->" , { choreo_step } ;

choreo_loop = "loop" , [ ident ] , "{" , { choreo_step } , "}" ;

choreo_decision = ident , "decides" , ident , "?" ;

choreo_goto = "goto" , ident ;

(* ========================================================= *)
(* 9. BEHAVIOURS (Content-Addressable)                       *)
(* ========================================================= *)
(* A behaviour's hash covers its syntactic form. Two          *)
(* behaviours with the same hash have identical syntax —      *)
(* but may have different INTERPRETIVE outcomes when given     *)
(* different Data contexts. The hash guarantees syntactic      *)
(* identity; it does not guarantee semantic identity.          *)
(* This is a consequence of Layer 4.                           *)

behaviour_decl = "behaviour" , upper_ident , "=" ,
                 "{" , { handler } , "}" ;

behaviour_ref = upper_ident ;

behaviour_hash = "#" , hex_string ;

(* ========================================================= *)
(* 10. LOCALES                                               *)
(* ========================================================= *)

locale_decl = "locale" , ident , "=" , locale_constructor ;

(* locale_constructor — see Section 18.6 for extended          *)
(* definition with model-routing parameters                    *)

locale_expr = ident | locale_constructor ;

(* ========================================================= *)
(* 11. TYPE EXPRESSIONS                                      *)
(* ========================================================= *)

(* type_expr — see Section 19 for full definition with         *)
(* Kategoria levels 5-10 and frontier type extensions          *)

primitive_type = "Int" | "Float" | "String" | "Bool" | "Data" | "Unit" ;

(* ========================================================= *)
(* 12. CAPABILITIES                                          *)
(* ========================================================= *)

capability_set = "Cap" , "[" , capability_list , "]" ;

capability_list = capability , { "," , capability } ;

capability = ident
           | ident , "(" , string_literal , ")" ;  (* parameterised cap *)

(* ========================================================= *)
(* 13. REVERSIBILITY                                         *)
(* ========================================================= *)

(* `reversible as <name> { ... }` binds the echo residue to <name> so a later
   `reverse <name>` can replay it (L10 phase 3). Anonymous form unchanged. *)
reversible_block = "reversible" , [ "as" , ident ] , "{" , { control_stmt } , "}" ;

reverse_block = "reverse" , "{" , { control_stmt } , "}" ;

(* `reverse <name>` replays the named residue bound by `reversible as <name>`. *)
reverse_named = "reverse" , ident ;

irreversible_block = "irreversible" , "{" , { control_stmt } , "}" ;

(* ========================================================= *)
(* 14. FUNCTIONS                                             *)
(* ========================================================= *)
(* Functions have explicit purity annotations.                *)
(* @total functions can be called from Data context.          *)
(* @pure functions can be called from Data context.           *)
(* Unmarked functions are @impure (default).                  *)

function_decl = [ purity_annotation ] , "fn" , ident ,
                "(" , [ param_list ] , ")" ,
                [ "->" , type_expr ] ,
                "{" , function_body , "}" ;

(* purity_annotation — see Section 18.3 for extended definition *)
(* with @neural dispatch                                        *)

(* @total function bodies can only contain data_expr.         *)
(* @pure function bodies can contain data_expr + pure calls.  *)
(* @impure function bodies can contain any control_stmt.      *)
function_body = { control_stmt }
              | data_expr ;

(* ========================================================= *)
(* 15. IMPORTS                                               *)
(* ========================================================= *)

import_decl = "import" , module_path , [ "as" , ident ]
            | "from" , module_path , "import" , import_list ;

module_path = ident , { "." , ident }
            | string_literal ;                (* URL or hash *)

import_list = import_item , { "," , import_item } ;

import_item = ident | upper_ident ;

(* ========================================================= *)
(* 16. PATTERNS                                              *)
(* ========================================================= *)

pattern = ident
        | "_"
        | data_literal
        | upper_ident , [ "(" , pattern_list , ")" ]
        | "(" , pattern , "," , pattern , { "," , pattern } , ")" ;

pattern_list = pattern , { "," , pattern } ;

(* ========================================================= *)
(* 17. LEXICAL PRIMITIVES                                    *)
(* ========================================================= *)

param_list = param , { "," , param } ;

param = ident , ":" , type_expr ;

typed_fields = typed_field , { "," , typed_field } ;

typed_field = ident , ":" , type_expr ;

state_decl = "state" , ident , ":" , type_expr , "=" , data_expr ;

(* `residue <name>` declares an echo-residue cell (L10 rung-3b): a            *)
(* `reversible as <name>` snapshots it and a `reverse <name>` restores it.    *)
residue_decl = "residue" , ident ;

(* Type declarations for user-defined types                   *)
type_decl = "type" , upper_ident , [ type_params ] , "=" , type_body ;

type_params = "<" , ident , { "," , ident } , ">" ;

type_body = type_expr
          | "{" , typed_fields , "}"           (* record type *)
          | enum_variants ;                    (* sum type *)

enum_variants = enum_variant , { "|" , enum_variant } ;

enum_variant = upper_ident , [ "(" , typed_fields , ")" ] ;

upper_ident = uppercase_letter , { letter | digit | "_" } ;

ident = lowercase_letter , { letter | digit | "_" } ;

integer_literal = [ "-" ] , digit , { digit } ;

float_literal = [ "-" ] , digit , { digit } , "." , digit , { digit } ,
                [ ( "e" | "E" ) , [ "+" | "-" ] , digit , { digit } ] ;

string_literal = '"' , { string_char } , '"' ;

string_char = (* any Unicode character except '"' and '\' *)
            | '\' , escape_char ;

escape_char = '"' | '\' | 'n' | 't' | 'r' | '0'
            | 'u' , '{' , hex_digit , { hex_digit } , '}' ;

bool_literal = "true" | "false" ;

string_list = "[" , [ string_literal , { "," , string_literal } ] , "]" ;

hex_string = hex_digit , { hex_digit } ;

letter = uppercase_letter | lowercase_letter ;

uppercase_letter = "A" | "B" | (* ... *) | "Z" ;

lowercase_letter = "a" | "b" | (* ... *) | "z" ;

digit = "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ;

hex_digit = digit | "a" | "b" | "c" | "d" | "e" | "f"
                   | "A" | "B" | "C" | "D" | "E" | "F" ;

(* ========================================================= *)
(* 18. TOKEN ECONOMICS — THE FIVE FACETS                     *)
(* ========================================================= *)
(* These constructs arise from the convergence of 007,        *)
(* Eclexia, Ephapax, JTV, and Oblibeny around the question:  *)
(* what is computation when agents are the consumers?         *)
(*                                                            *)
(*   @budget  — Eclexia's shadow pricing as linear type       *)
(*   speculative — Chapel-style parallel branch evaluation    *)
(*   @neural  — Hypatia hook, zero-token inference            *)
(*   cached   — Oblibeny's reduction via trace memoisation    *)
(*   @focus   — Ephapax-style attention budgeting             *)
(*   batch    — GPU-style token amortisation                  *)
(*                                                            *)
(* INVARIANT 4 (Economic): The Data Language is free          *)
(* computation (CPU-evaluated, deterministic). The Control    *)
(* Language costs tokens (LLM inference, nondeterministic).   *)
(* The Harvard boundary IS the economic boundary.             *)

(* --------------------------------------------------------- *)
(* 18.1 BUDGET — Token budget as linear resource              *)
(* --------------------------------------------------------- *)
(* A @budget annotation on an agent parameter declares a      *)
(* finite token budget. The type system tracks consumption.   *)
(* Exceeding the budget is a TYPE ERROR, not a runtime crash. *)
(* This is Eclexia's resource constraint applied to tokens.   *)

budget_annotation = "@budget" , "(" , integer_literal , ")" ;

(* Budget appears in agent params alongside caps:             *)
(* agent Analyst(caps: Cap[net], budget: @budget(2000)) { }   *)
(* The grammar extends agent_param:                           *)

agent_param = "caps" , ":" , capability_set
            | "budget" , ":" , budget_annotation
            | ident , ":" , type_expr ;

(* --------------------------------------------------------- *)
(* 18.2 SPECULATIVE — Parallel branch evaluation              *)
(* --------------------------------------------------------- *)
(* A speculative branch evaluates ALL arms in parallel on     *)
(* separate inference streams. The branch strategy selects    *)
(* the best result. Cost is max(arm_costs) not sum.           *)
(* This is Chapel's coforall applied to LLM inference.        *)

branch_stmt = "branch" , [ branch_modifier ] ,
              [ "traced" , string_literal ] ,
              "{" , branch_arm , { branch_arm } , "}" ;

branch_modifier = "speculative"     (* parallel evaluation *)
                | "cached" ;        (* trace memoisation   *)

(* --------------------------------------------------------- *)
(* 18.3 NEURAL — Neurosymbolic dispatch                      *)
(* --------------------------------------------------------- *)
(* A fourth purity level. @neural functions route to a        *)
(* trained neurosymbolic system (e.g., Hypatia ESN/RBF),     *)
(* NOT to the LLM. Cost: ~zero tokens.                        *)
(*                                                            *)
(* Decision traces are the training data. @neural functions   *)
(* learn from traces, progressively offloading expensive LLM  *)
(* decisions to cheap neural inference.                        *)

purity_annotation = "@total" | "@pure" | "@impure" | "@neural" ;

(* @neural function bodies contain a dispatch specification:  *)
(* which model, what input mapping, what output type.         *)

neural_dispatch = "dispatch" , "(" , neural_target , ")" ;

neural_target = "hypatia" , "(" , string_literal , ")"  (* model name  *)
              | "onnx" , "(" , string_literal , ")"     (* ONNX model  *)
              | "custom" , "(" , string_literal , ")" ; (* custom backend *)

(* --------------------------------------------------------- *)
(* 18.4 FOCUS — Attention budget on given clauses             *)
(* --------------------------------------------------------- *)
(* @focus(N) on a given clause allocates N tokens of context  *)
(* window to that evidence. Prevents wasted attention.        *)
(* This is Ephapax's material view applied to context:        *)
(* attention tokens are consumed, finite, allocated.          *)

given_clause = "given" , [ focus_annotation ] ,
               "{" , given_items , "}" ;

focus_annotation = "@focus" , "(" , integer_literal , ")" ;

(* --------------------------------------------------------- *)
(* 18.5 BATCH — Amortised decisions in choreographies         *)
(* --------------------------------------------------------- *)
(* A batch block presents N decisions to the LLM as one       *)
(* structured prompt. Cost: ~1.5x one decision, not Nx.       *)
(* Like GPU kernel batching for inference.                     *)

choreo_step = choreo_comm
            | choreo_parallel
            | choreo_branch
            | choreo_loop
            | choreo_decision
            | choreo_goto
            | choreo_batch ;

choreo_batch = "batch" , "{" , { choreo_step } , "}" ;

(* --------------------------------------------------------- *)
(* 18.6 LOCALE — Model-routing extensions                     *)
(* --------------------------------------------------------- *)
(* Locales gain optional model routing. A locale can specify  *)
(* which LLM or inference backend to use, enabling cost-aware *)
(* dispatch: cheap models for easy decisions, expensive for   *)
(* hard ones, ensembles for consensus.                        *)

locale_constructor = "Local"
                   | "GPU" , "(" , "device" , ":" , integer_literal , ")"
                   | "Remote" , "(" , remote_params , ")"
                   | "Edge" , "(" , edge_params , ")"
                   | "Cluster" , "(" , cluster_params , ")" ;

(* Extended constructors with optional model routing:         *)
remote_params = remote_param , { "," , remote_param } ;
remote_param = "url" , ":" , string_literal
             | "model" , ":" , string_literal ;

edge_params = edge_param , { "," , edge_param } ;
edge_param = "region" , ":" , string_literal
           | "model" , ":" , string_literal ;

cluster_params = cluster_param , { "," , cluster_param } ;
cluster_param = "nodes" , ":" , string_list
              | "models" , ":" , string_list ;

(* ========================================================= *)
(* 19. ADVANCED TYPE EXPRESSIONS — KATEGORIA LEVELS 5-10      *)
(* ========================================================= *)
(* These express the full Kategoria 10-level taxonomy.         *)
(*                                                             *)
(* type_expr covers:                                           *)
(*   L1 basic types, L2 ADTs (enum_variants in type_decl),     *)
(*   L3 parametric polymorphism (type_params), L4 HKTs,        *)
(*   L5 GADTs, L6 dependent types, L7 linear/affine,           *)
(*   L8 refinement types, L9 session types, L10 path types,    *)
(*   plus graded types and effect types.                        *)

type_expr = primitive_type
          | "Agent" , "<" , upper_ident , ">"
          | "Handle" , "<" , upper_ident , ">"
          | "Supervisor" , "<" , upper_ident , ">"
          | "Session" , "<" , upper_ident , ">"
          | "Cap" , "[" , capability_list , "]"
          | "Trace" , "<" , string_literal , ">"
          | "[" , type_expr , "]"
          | "(" , type_expr , "," , type_expr , { "," , type_expr } , ")"
          | upper_ident
          | "linear" , type_expr
          (* Level 5: GADTs — type indices constrain constructors   *)
          | upper_ident , "<" , type_expr , { "," , type_expr } , ">"
          (* Level 6: Dependent types — types depend on values      *)
          | dependent_type
          (* Level 7: Linear/Affine — already present via `linear`  *)
          (* Level 8: Refinement — predicates on values             *)
          | refinement_type
          (* Level 9: Session — already present via Session<P>      *)
          (* Level 10: Homotopy/Cubical — path types                *)
          | path_type
          (* Frontier: Graded types — semiring-indexed resources    *)
          | graded_type
          (* Frontier: Effect types — tracked side effects          *)
          | effect_type ;

(* --------------------------------------------------------- *)
(* 19.1 DEPENDENT TYPES (Kategoria Level 6)                   *)
(* --------------------------------------------------------- *)
(* Types that depend on runtime values.                        *)
(* E.g., Vect(n, Int) — a vector of exactly n integers.       *)
(* The value `n` is a term, not a type parameter.              *)

dependent_type = upper_ident , "(" , dep_arg , { "," , dep_arg } , ")" ;

dep_arg = data_expr      (* value argument — Data only, Harvard-separated *)
        | type_expr ;    (* type argument *)

(* Note: dep_args are Data expressions. You cannot put control *)
(* flow in a dependent type index. This is the Harvard         *)
(* Architecture protecting the type system itself.             *)

(* --------------------------------------------------------- *)
(* 19.2 REFINEMENT TYPES (Kategoria Level 8)                  *)
(* --------------------------------------------------------- *)
(* Types with predicates: { x : T | P(x) }                    *)
(* The predicate is a Data expression (Harvard-separated).     *)
(* Checked at compile time via SMT or proof obligation.        *)

refinement_type = "{" , ident , ":" , type_expr , "|" , data_predicate , "}" ;

(* Example: { n : Int | n > 0 }                               *)
(* Example: { s : String | length(s) < 256 }                  *)
(* The predicate uses data_predicate from Section 5.1.         *)
(* This reuses given-clause predicates — same Harvard rules.   *)

(* --------------------------------------------------------- *)
(* 19.3 PATH TYPES (Kategoria Level 10 — Homotopy/Cubical)   *)
(* --------------------------------------------------------- *)
(* Type equivalences as first-class values.                    *)
(* Path(A, B) witnesses that types A and B are equivalent.     *)
(* Required for univalence and transport.                      *)

path_type = "Path" , "(" , type_expr , "," , type_expr , ")" ;

(* Path types. Semantics follow cubicaltt/Agda --cubical.      *)

(* --------------------------------------------------------- *)
(* 19.4 GRADED TYPES (Frontier — Kategoria Level 11+)         *)
(* --------------------------------------------------------- *)
(* Semiring-indexed resource tracking. Generalises linear      *)
(* types: instead of "use exactly once" (1), you can say       *)
(* "use at most N times" (N), "use any number of times" (ω),  *)
(* or "never use" (0).                                         *)
(*                                                             *)
(* In 007, grading tracks TOKEN COST: a graded type carries    *)
(* how many tokens evaluating it will consume.                  *)

graded_type = "@graded" , "(" , grade , ")" , type_expr ;

grade = integer_literal   (* exact count *)
      | "omega"           (* unrestricted *)
      | "zero"            (* phantom/unused *)
      | ident ;           (* symbolic grade from semiring *)

(* Example: @graded(500) Handle<Worker> — this handle will     *)
(*          cost ~500 tokens to use                             *)
(* Example: @graded(zero) Trace<"audit"> — phantom trace type, *)
(*          proves the trace exists without consuming it        *)

(* --------------------------------------------------------- *)
(* 19.5 EFFECT TYPES (Frontier — Kategoria Level 11+)         *)
(* --------------------------------------------------------- *)
(* Tracked side effects in the type system. In 007, effects    *)
(* include: token consumption, message sending, spawning,      *)
(* state mutation, locale migration.                           *)
(*                                                             *)
(* Effect types make the Harvard boundary GRADUAL — instead    *)
(* of binary pure/impure, you can declare exactly which        *)
(* effects a function may perform.                             *)

effect_type = type_expr , "!" , effect_set ;

effect_set = "{" , effect , { "," , effect } , "}" ;

effect = "send"           (* may send messages *)
       | "spawn"          (* may spawn agents *)
       | "tokens" , "(" , integer_literal , ")"  (* costs N tokens *)
       | "migrate"        (* may move between locales *)
       | "state"          (* may mutate state *)
       | "trace"          (* produces decision traces *)
       | "neural"         (* invokes neurosymbolic system *)
       | ident ;          (* user-defined effect *)

(* Example: fn analyse(data: Data) -> Result !{tokens(200), trace}   *)
(*          — this function costs ~200 tokens and produces traces    *)
(* Example: fn pure_calc(x: Int) -> Int !{}                          *)
(*          — no effects, equivalent to @pure                        *)
(* Example: fn route(task: String) -> Unit !{send, migrate, spawn}   *)
(*          — may send messages, migrate computation, spawn agents   *)

(* ========================================================= *)
(* 20. AGENT ERGONOMICS                                       *)
(* ========================================================= *)
(* Constructs designed specifically for LLM agent consumers.  *)
(* These arise from direct experience of an LLM (Claude)      *)
(* building and using 007 — the target user providing          *)
(* feedback on its own language.                               *)

(* --------------------------------------------------------- *)
(* 20.1 REFERENCE ANNOTATIONS — Code→Database pointers        *)
(* --------------------------------------------------------- *)
(* Agents don't need inline comments. They need queryable      *)
(* documentation. @ref links a code location to a VeriSimDB    *)
(* entry containing rationale, decisions, cross-references.    *)
(*                                                             *)
(* For humans: comments explain inline.                        *)
(* For agents: @ref points to a database query.                *)
(* This separates documentation from code, reducing token      *)
(* cost of parsing while preserving full traceability.         *)

ref_annotation = "@ref" , "(" , string_literal , ")" ;

(* @ref may appear after any top-level declaration, statement, *)
(* or expression as an annotation. It is syntactic sugar for   *)
(* "the rationale for this construct is in VeriSimDB at this   *)
(* key." It has no operational semantics — it is metadata.     *)
(*                                                             *)
(* Example:                                                    *)
(*   data_additive = data_multiplicative ,                     *)
(*                   { ( "+" | "-" ) , data_multiplicative }   *)
(*     @ref("harvard-data-scalar-arithmetic")                  *)
(*                                                             *)
(* An agent queries:                                           *)
(*   VQL-UT: SELECT * FROM design_decisions                    *)
(*           WHERE ref = "harvard-data-scalar-arithmetic"      *)
(*                                                             *)
(* The VeriSimDB instance contains:                            *)
(*   - Rationale, ADR reference, date, who-proposed            *)
(*   - Cross-references to related decisions                   *)
(*   - Kategoria level relevance                               *)
(*   - Five Facets mapping                                     *)

(* --------------------------------------------------------- *)
(* 20.2 QUERY EXPRESSION — Trace database lookup               *)
(* --------------------------------------------------------- *)
(* Agents want to check: "has this decision been made before?" *)
(* query_trace returns a prior decision record if one exists,  *)
(* enabling explicit memoization beyond the `cached` keyword.  *)

control_expr = (* ... existing alternatives ... *)
             | "query_trace" , "(" , string_literal , "," , data_expr , ")" ;

(* query_trace("branch_label", given_context) → Data | null    *)
(* Returns the prior trace record matching this label+context, *)
(* or null if no prior decision exists.                        *)
(* The result is DATA (Harvard-separated, immutable).          *)

(* ========================================================= *)
(* 21. HARVARD SENTINEL — Runtime integrity verification      *)
(* ========================================================= *)
(* The Harvard Architecture provides compile-time safety:     *)
(* parse errors catch syntactic violations, type errors catch *)
(* type-level violations. But what if someone tampers with    *)
(* the grammar or type checker ITSELF?                        *)
(*                                                            *)
(* The sentinel is a Data-language construct that hashes the  *)
(* grammar rules and type judgements. Because it lives in     *)
(* Data, it is total, pure, and Harvard-protected — it        *)
(* cannot be tampered with without breaking the grammar,      *)
(* which is a parse error.                                    *)
(*                                                            *)
(* Threat model: humans can't attack because they can't       *)
(* write 007 at scale. Compromised agents can't attack        *)
(* because the sentinel catches them. The only vector is      *)
(* compromising the sentinel itself, but the sentinel is      *)
(* Data, protected by the grammar it monitors.                *)
(*                                                            *)
(* This is circular, but productively so — like a TPM whose   *)
(* measurement chain includes itself.                         *)

(* --------------------------------------------------------- *)
(* 21.1 SENTINEL DECLARATION — integrity hash set             *)
(* --------------------------------------------------------- *)
(* A sentinel is a @total data block containing hashes of     *)
(* grammar rules, type checker judgements, and invariants.     *)
(* It is evaluated at compile time (total = guaranteed to     *)
(* terminate) and stored as immutable Data.                    *)

sentinel_decl = "@sentinel" , ident , "=" ,
                "{" , sentinel_fields , "}" ;

sentinel_fields = sentinel_field , { "," , sentinel_field } , [ "," ] ;

sentinel_field = "grammar_hash" , ":" , sentinel_hash_call
               | "type_rules_hash" , ":" , sentinel_hash_call
               | "invariant" , ":" , sentinel_invariant_list
               | ident , ":" , data_expr ;

sentinel_hash_call = "hash_grammar" , "(" , ")"
                   | "hash_type_rules" , "(" , ")"
                   | "hash_invariant" , "(" , string_literal , ")" ;

sentinel_invariant_list = "[" , sentinel_hash_call ,
                          { "," , sentinel_hash_call } , [ "," ] , "]" ;

(* Example:                                                    *)
(*   @sentinel integrity = {                                   *)
(*     grammar_hash: hash_grammar(),                           *)
(*     type_rules_hash: hash_type_rules(),                     *)
(*     invariant: [                                            *)
(*       hash_invariant("harvard_separation"),                 *)
(*       hash_invariant("hermeneutic_data_only"),              *)
(*       hash_invariant("economic_boundary"),                  *)
(*       hash_invariant("kategoria_harvard")                   *)
(*     ]                                                       *)
(*   }                                                         *)

(* --------------------------------------------------------- *)
(* 21.2 SENTINEL-GUARDED AGENTS                               *)
(* --------------------------------------------------------- *)
(* An agent may declare a sentinel guard. Before the agent's  *)
(* control block executes, the runtime verifies the sentinel  *)
(* hashes match the actual grammar and type rules. If ANY     *)
(* mismatch is detected, the agent REFUSES TO START.          *)
(* This is not a type error — it is a RUNTIME HALT.           *)

agent_decl = "agent" , agent_name , [ "(" , agent_params , ")" ] ,
             [ "implements" , protocol_role_list ] ,
             [ "on" , "locale" , locale_expr ] ,
             [ "@sentinel" , "(" , ident , ")" ] ,
             "{" , agent_body , "}" ;

(* --------------------------------------------------------- *)
(* 21.3 ATTESTED SPAWN — Chain of trust                       *)
(* --------------------------------------------------------- *)
(* When spawning with `attested`, the parent agent demands    *)
(* that the child's sentinel hash matches its own. If the     *)
(* child has been compiled with a different grammar or type   *)
(* checker (i.e., tampered), the spawn FAILS.                 *)
(*                                                            *)
(* This creates a chain of trust between agents. Every agent  *)
(* in the chain has verified integrity. A compromised agent   *)
(* cannot join the chain.                                      *)

spawn_stmt = [ "linear" ] , "let" , ident , "=" ,
             "spawn" , [ "attested" ] , agent_name ,
             "(" , spawn_args , ")" ;

(* --------------------------------------------------------- *)
(* 21.4 INTEGRITY VERIFICATION EXPRESSION                     *)
(* --------------------------------------------------------- *)
(* verify_integrity() is a @total Data function that checks   *)
(* a sentinel against the current runtime. Returns Bool.      *)
(* Because it is @total and Data, it cannot be suppressed,    *)
(* cannot lie (deterministic), and cannot be tampered with     *)
(* without breaking the grammar.                               *)

control_expr = (* ... existing alternatives ... *)
             | "verify_integrity" , "(" , ident , ")" ;

(* verify_integrity(sentinel_name) → Bool                      *)
(* Returns true if all sentinel hashes match the runtime.     *)
(* Returns false if ANY hash mismatches (tampered grammar,    *)
(* modified type rules, broken invariants).                    *)
(* This is a Data expression despite appearing in Control —   *)
(* it performs no side effects, only reads immutable state.    *)

(* --------------------------------------------------------- *)
(* 21.5 CROSS-AGENT ATTESTATION PROTOCOL                      *)
(* --------------------------------------------------------- *)
(* Agents may exchange sentinel hashes as part of session     *)
(* type protocols. This extends the chain of trust to         *)
(* multi-agent choreographies.                                 *)

(* Example protocol with attestation:                          *)
(*   session protocol SecureReview {                            *)
(*     Reviewer -> Author : Attest(sentinel_hash: String)      *)
(*     Author -> Reviewer : Attest(sentinel_hash: String)      *)
(*     branch by Reviewer {                                    *)
(*       | proceed given { hashes_match: true } -> {           *)
(*         Reviewer -> Author : Feedback(score: Int)           *)
(*       }                                                     *)
(*       | abort given { hashes_match: false } -> {            *)
(*         Reviewer -> Author : Abort(reason: String)          *)
(*       }                                                     *)
(*     }                                                       *)
(*   }                                                         *)

(* --------------------------------------------------------- *)
(* 21.6 SENTINEL V2 — Supply chain defence                     *)
(* --------------------------------------------------------- *)
(* Sentinel v1 hashes the grammar and type rules. But a       *)
(* compromised parser generator (pest) or compiler (rustc)     *)
(* could produce a binary that doesn't match the grammar.      *)
(* Sentinel v2 extends to hash the BINARY itself.              *)

sentinel_hash_call = "hash_grammar" , "(" , ")"
                   | "hash_type_rules" , "(" , ")"
                   | "hash_invariant" , "(" , string_literal , ")"
                   | "hash_binary" , "(" , ")"            (* v2 *)
                   | "hash_deps" , "(" , ")"              (* v2 *)
                   | "hash_neural_model" , "(" , string_literal , ")" ; (* v2 *)

(* hash_binary() — SHA-256 of the compiled parser+typechecker *)
(*   binary. Detects if the compiler produced unexpected       *)
(*   output, or if the binary was modified after compilation.  *)
(*                                                             *)
(* hash_deps() — Merkle root of all dependency hashes          *)
(*   (Cargo.lock resolved). Detects transitive supply chain    *)
(*   changes.                                                  *)
(*                                                             *)
(* hash_neural_model(name) — hash of @neural model weights     *)
(*   and training data provenance. Detects poisoned models.    *)

(* Full sentinel v2 example:                                   *)
(*   @sentinel integrity_v2 = {                                *)
(*     grammar_hash: hash_grammar(),                           *)
(*     type_rules_hash: hash_type_rules(),                     *)
(*     binary_hash: hash_binary(),                             *)
(*     deps_hash: hash_deps(),                                 *)
(*     neural_integrity: hash_neural_model("triage_classifier"),*)
(*     invariant: [                                            *)
(*       hash_invariant("harvard_separation"),                 *)
(*       hash_invariant("economic_boundary"),                  *)
(*       hash_invariant("supply_chain")                        *)
(*     ]                                                       *)
(*   }                                                         *)

(* ========================================================= *)
(* END OF GRAMMAR — VERSION 0.5.0-draft                       *)
(* ========================================================= *)
(*                                                            *)
(* INVARIANT 1 (Harvard): data_expr is a strict subset that   *)
(* CANNOT contain control_stmt, handler, spawn_stmt,          *)
(* send_stmt, if_stmt, loop_stmt, match_stmt, branch_stmt,    *)
(* or any I/O operations.                                     *)
(*                                                            *)
(* INVARIANT 2 (Hermeneutic): `given` clauses and `trace`     *)
(* clauses are Data expressions — they CANNOT contain control *)
(* flow. Decision traces are immutable records. The           *)
(* observation must not disturb the phenomenon.               *)
(*                                                            *)
(* INVARIANT 3 (Telescope): `traced` branch points produce    *)
(* decision records that accumulate into datasets for         *)
(* Layer 4 analysis. The grammar provides the instrument;     *)
(* the structure (if any) emerges from use.                   *)
(*                                                            *)
(* INVARIANT 4 (Economic): The Data Language is free           *)
(* computation (CPU-evaluated, deterministic). The Control     *)
(* Language costs tokens (LLM inference, nondeterministic).    *)
(* The Harvard boundary IS the economic boundary.              *)
(* @budget tracks cost as a linear type. @neural offloads to   *)
(* zero-token computation. cached/speculative optimise spend.  *)
(*                                                            *)
(* INVARIANT 5 (Kategoria): Type expressions span Kategoria   *)
(* levels 1-10. Dependent type indices (L6), refinement        *)
(* predicates (L8), and path types (L10) are Harvard-          *)
(* separated — they contain only Data expressions, not         *)
(* Control. The type system cannot inject side effects.        *)
(*                                                            *)
(*                                                            *)
(* INVARIANT 6 (Integrity): The Harvard sentinel lives in      *)
(* Data. It hashes the grammar and type rules. Because it is   *)
(* Data, it is total, pure, and Harvard-protected. Tampering   *)
(* with the sentinel requires breaking the grammar, which is   *)
(* a parse error. Attested spawn creates chains of trust       *)
(* between agents — a compromised agent cannot join the chain. *)
(*                                                            *)
(* FIVE FACETS (language family convergence):                  *)
(*   007    — computation as interpretation (hermeneutic)      *)
(*   Eclexia — computation as economics (shadow prices)        *)
(*   Ephapax — computation as matter (linear, consumed once)   *)
(*   JTV    — computation as governed (total, provably halting) *)
(*   Oblibeny — computation as reducible (reversible, minimal) *)
(* Each facet maps to grammar constructs in this file.         *)
(*                                                            *)
(* LAYER MODEL:                                               *)
(*   Layer 1 — Grammar (this file)                            *)
(*   Layer 2 — Types (TYPE-SYSTEM-SPEC.adoc, Kategoria L1-10) *)
(*   Layer 3 — Operational Semantics (OPERATIONAL-SEM.adoc)   *)
(*   Layer 4 — Interpretive Semantics (provisional, emergent) *)
(* ========================================================= *)