commit grammar, format code (macro sigh), add pretty printing of AST

1 files changed, 63 insertions, 0 deletions

diff --git a/grammar.txt b/grammar.txt
new file mode 100644
index 0000000..34d8e1b
--- /dev/null
+++ b/grammar.txt
@@ -0,0 +1,63 @@
+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" , "(" , 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 | app_elem ;
+case_elem         = "case" , element , "of" , "{" , [ case_arm { "|" , case_arm } ] , "}" ;
+case_arm          = inject_elem , elem_var , "=>" , element ;
+app_elem          = dot_elem { dot_elem } ;
+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 | 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 | "_" | "'" ;