From ac0694074630f1308e44e42eb9bf0d228460fbf1 Mon Sep 17 00:00:00 2001 From: tslil Date: Thu, 7 May 2026 16:20:25 +0100 Subject: grammar.txt is too difficult to maintain by hand anymore :( --- grammar.txt | 76 ------------------------------------------------------------- 1 file changed, 76 deletions(-) delete mode 100644 grammar.txt diff --git a/grammar.txt b/grammar.txt deleted file mode 100644 index e180bb0..0000000 --- a/grammar.txt +++ /dev/null @@ -1,76 +0,0 @@ -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 ; - -(* Sets *) -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 , ")" ; - -(* Signatures *) -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 , ")" ; - -(* Elements *) -element = case_elem | dot_elem ; -case_elem = "case" , element , "of" , "[" , [ elem_case_arm { "|" , elem_case_arm } ] , "]" ; -elem_case_arm = inject_elem , elem_var , "=>" , element ; -dot_elem = { inject_elem } , atom_elem , { project_elem } ; -inject_elem = ident , "." ; -project_elem = "." , ident ; -atom_elem = literal | record_elem | "(" , element , ")" | elem_var ; -record_elem = "{" , [ elem_assign { "," , elem_assign } ] , "}" ; -elem_assign = elem_field_label , "=" , element ; -elem_field_label = "." , lower_ident ; - -(* Instances *) -instance = for_inst | case_inst | app_inst ; -for_inst = "for" , param_list , "," , instance ; -case_inst = "case" , element , "of" , "[" , [ inst_case_arm { "|" , inst_case_arm } ] , "]" ; -inst_case_arm = inject_elem , elem_var , "=>" , instance ; -app_inst = dot_inst , { dot_elem } ; -dot_inst = atom_inst , { project_elem } ; -atom_inst = set_coerce | inst_var | sig_var | record_inst | "(" , instance , ")" ; -set_coerce = set , "::" , "Set" ; -record_inst = "{" , [ inst_assign { "," , inst_assign } ] , "}" ; -inst_assign = inst_field_label , "=" , instance ; -inst_field_label = "." , upper_ident ; - -(* Literals *) -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" ; - -(* Identifiers *) -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 | "_" | "'" ; - -(* Lexical *) -comment = "//" , { any_character_except_newline } , ( newline | end_of_input ) ; -- cgit v1.3.1