# 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 valid (defines a _black hole_).

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

ces_immediate = identifier "(" ")" ;

ces_instance = identifier "!" "(" { instance_args } ")" ;

instance_args = arg_value { ","  arg_value } [ "," ] ;

arg_value = identifier | size | name ;

## Context

context_block = prop_block
              | caps_block
              | unbounded_block
              | weights_block
              | inhibit_block
              | hold_block ;

prop_selector = "vis" | "sat" ;
prop_block = prop_selector "{" { prop_list } "}" ;
prop_list = prop_field { "," prop_field } [ "," ] ;
prop_field = identifier ":" prop_value ;
prop_value_array = prop_value { "," prop_value } [ "," ] ;

prop_value = name
           | size_list
           | node_list
           | "[" prop_value_array "]"
           | "{" prop_list "}" ;

caps_block = "caps" "{" { cap_list } "}" ;
cap_list = cap_field { "," cap_field } [ "," ] ;
cap_field = size node_list ;

unbounded_block = "unbounded" "{" { node_list } "}" ;

weights_block = "weights" "{" { weight_list } "}" ;
weight_list = weight_field { "," weight_field } [ "," ] ;
weight_field = size node_list ( "->" | "<-" ) node_list ;

inhibit_block = "inhibit" "{" { inhibit_list } "}" ;
inhibit_list = inhibit_field { "," inhibit_field } [ "," ] ;
inhibit_field = node_list ( "->" | "<-" ) node_list ;

hold_block = "hold" "{" { hold_list } "}" ;
hold_list = hold_field { "," hold_field } [ "," ] ;
hold_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 } ;
size_list = size { size } ;

# multi-polynomial rule with implicit node lists
fat_arrow_rule = polynomial ( "=>" | "<=" | "<=>" ) polynomial { ( "=>" | "<=" | "<=>" ) polynomial } ;

## Polynomial

polynomial = [ [ polynomial ] "+" ] poly_term { poly_term } ;
poly_term = identifier | "(" polynomial ")" ;