program           = { declaration } ;

declaration       = set_decl | element_decl | theory_decl | instance_decl ;

set_decl          = "let set" , set_var , "=" , set ;
element_decl      = "let element" , elem_var , ":" , set , "=" , element ;
theory_decl       = "let signature" , sig_var , "=" , signature ;
instance_decl     = "let instance" , inst_var , "::" , signature , "=" , instance ;

set               = record_set | variant_set | builtin_set | claimed_set | set_var | "(" , set , ")" ;
record_set        = "record" , "{" , [ set_field { "," , set_field } ] , "}" ;
set_field         = lower_ident , ":" , set ;
variant_set       = "variant" , "[" , [ variant_field { "|" , variant_field } ] , "]" ;
variant_field     = lower_ident , ":" , set ;
builtin_set       = "Nat" | "Int" | "Float" | "Str" | "Bool" ;
claimed_set       = "set-of" , "(" , instance , ")" ;

signature         = "Set" | theory_sig | function_sig | sig_var | "(" , signature , ")" ;
theory_sig        = "theory" , "{" , [ sig_field { "," , sig_field } ] , "}" ;
sig_field         = "." , upper_ident , "::" , signature ;
function_sig      = param_list , "->" , signature ;
param_list        = param { param } ;
param             = "(" , elem_var , ":" , set , ")" ;

element           = case_elem | dot_elem ;
case_elem         = "case" , element , "of" , "{" , [ case_arm { "|" , case_arm } ] , "}" ;
case_arm          = inject_elem , elem_var , "=>" , element ;
dot_elem          = { inject_elem } , atom_elem , { project_elem } ;
inject_elem       = ident , "." ;
project_elem      = "." , ident ;
atom_elem         = literal | elem_var | record_elem | "(" , element , ")" ;
record_elem       = "{" , [ elem_assign { "," , elem_assign } ] , "}" ;
elem_assign       = project_elem , "=" , element ;

instance          = for_inst | app_inst ;
for_inst          = "for" , param_list , "," , instance ;
app_inst          = dot_inst { dot_elem } ;
dot_inst          = atom_inst { project_elem } ;
atom_inst         = set ":: Set" | inst_var | record_inst | "(" , instance , ")" ;
record_inst       = "{" , [ inst_assign { "," , inst_assign } ] , "}" ;
inst_assign       = project_elem , "=" , instance ;

literal           = nat_lit | int_lit | float_lit | str_lit | bool_lit ;
nat_lit           = digit , { digit } ;
int_lit           = "-" , digit , { digit } ;
float_lit         = [ "-" ] , digit , { digit } , "." , digit , { digit } ;
str_lit           = '"' , { any_character_except_quote } , '"' ;
bool_lit          = "true" | "false" ;

set_var           = upper_ident ;
sig_var           = upper_ident ;
elem_var          = lower_ident ;
inst_var          = lower_ident ;

upper_ident       = upper_case_letter , { ident_char } ;
lower_ident       = lower_case_letter , { ident_char } ;
ident             = (upper_case_letter | lower_case_letter) , { ident_char } ;

upper_case_letter = "A"..."Z" ;
lower_case_letter = "a"..."z" ;
digit             = "0"..."9" ;
ident_char        = upper_case_letter | lower_case_letter | digit | "_" | "'" ;