# Ascesis syntax in EBNF
# Some aspects of the language are described informally in other
# files: lexer-implementation.md, parser-implementation.md.
ces_file = { immediate_def | template_def | context_block } ;
## Structure definition, immediate form
immediate_def = immediate_sig "{" rex "}" ;
immediate_sig = "ces" identifier ;
## Structure definition, template form
# Empty argument list is disallowed.
template_def = template_sig "{" rex "}" ;
template_sig = "ces" identifier "(" template_args ")" ;
template_args = arg_decl { "," arg_decl } [ "," ] ;
arg_decl = identifier ":" ( "Node" | "CES" | "Size" | "Name" ) ;
## Structure instantiation
# Empty argument list is syntactically valid, but used only for
# instantiating immediate definitions.
ces_instance = identifier "(" ")"
| identifier "!" "(" instance_args ")" ;
instance_args = arg_value { "," arg_value } [ "," ] ;
arg_value = identifier | size | name ;
## Context
context_block = prop_block | cap_block | mul_block | inh_block ;
prop_selector = "vis" | "sat" ;
prop_block = prop_selector "{" prop_list "}" ;
prop_list = prop_field { "," prop_field } [ "," ] ;
prop_field = identifier ":" prop_value ;
prop_value = size
| name
| identifier
| "{" prop_list "}" ;
cap_block = "cap" "{" cap_list "}" ;
cap_list = cap_field { "," cap_field } [ "," ] ;
cap_field = size node_list ;
mul_block = "mul" "{" mul_list "}" ;
mul_list = mul_field { "," mul_field } [ "," ] ;
mul_field = size node_list ( "->" | "<-" ) node_list ;
inh_block = "inh" "{" inh_list "}" ;
inh_list = inh_field { "," inh_field } [ "," ] ;
inh_field = node_list ( "->" | "<-" ) node_list ;
## Rule expression
rex = thin_arrow_rule
| fat_arrow_rule
| rex_term { [ "+" ] rex_term } ;
rex_term = ces_instance | "{" rex "}" ;
## Arrow rules
thin_arrow_rule = e_rule | c_rule | ec_rule | ce_rule | fw_rule | bw_rule ;
# effect polynomial with explicit node list on the left
e_rule = node_list "->" polynomial ;
# cause polynomial with explicit node list on the left
c_rule = node_list "<-" polynomial ;
# effect-then-cause polynomial with explicit node list on the left
ec_rule = node_list "->" polynomial "<-" polynomial ;
# cause-then-effect polynomial with explicit node list on the left
ce_rule = node_list "<-" polynomial "->" polynomial ;
# cause-then-effect pair of polynomials with explicit node list in the
# middle
fw_rule = "+" plain_polynomial "->" node_list "->" polynomial ;
# effect-then-cause pair of polynomials with explicit node list in the
# middle
bw_rule = "+" plain_polynomial "<-" node_list "<-" polynomial ;
node_list = identifier { identifier } ;
# multi-polynomial rule with implicit node lists
fat_arrow_rule = polynomial ( "=>" | "<=" | "<=>" ) polynomial { ( "=>" | "<=" | "<=>" ) polynomial } ;
## Polynomial
polynomial = [ [ polynomial ] "+" ] poly_term { poly_term } ;
poly_term = identifier | "(" polynomial ")" ;