diff options
Diffstat (limited to 'grammar.txt')
| -rw-r--r-- | grammar.txt | 34 |
1 files changed, 24 insertions, 10 deletions
diff --git a/grammar.txt b/grammar.txt index 9772501..e180bb0 100644 --- a/grammar.txt +++ b/grammar.txt @@ -7,6 +7,7 @@ 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 ; @@ -15,31 +16,40 @@ 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 ; +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" , "{" , [ case_arm { "|" , case_arm } ] , "}" ; -case_arm = inject_elem , elem_var , "=>" , element ; +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 | elem_var | record_elem | "(" , element , ")" ; +atom_elem = literal | record_elem | "(" , element , ")" | elem_var ; record_elem = "{" , [ elem_assign { "," , elem_assign } ] , "}" ; -elem_assign = project_elem , "=" , element ; +elem_assign = elem_field_label , "=" , element ; +elem_field_label = "." , lower_ident ; -instance = for_inst | app_inst ; +(* Instances *) +instance = for_inst | case_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 , ")" ; +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 = project_elem , "=" , instance ; +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 } ; @@ -47,6 +57,7 @@ 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 ; @@ -60,3 +71,6 @@ 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 ) ; |