1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
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 | "_" | "'" ;
|
