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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
|
%{
type constr_ast =
Pair of constr_ast * constr_ast
| Prod of binder list * constr_ast
| Lambda of binder list * constr_ast
| Cast of constr_ast * constr_ast
| Let of string * constr_ast * constr_ast
| LetCase of binder list * constr_ast * constr_ast
| IfCase of constr_ast * constr_ast * constr_ast
| Eval of red_fun * constr_ast
| Infix of string * constr_ast * constr_ast
| Prefix of string * constr_ast
| Postfix of string * constr_ast
| Appl of constr_ast * constr_arg list
| ApplExpl of constr_ast * constr_ast list
| Scope of string * constr_ast
| Qualid of string list
| Prop | Set | Type
| Int of string
| Hole
| Meta of string
| Fixp of fix_kind *
(string * binder list * constr_ast * string option * constr_ast) list *
string
| Match of case_item list * constr_ast option *
(pattern list * constr_ast) list
and redfun = Simpl
and binder = string * constr_ast
and constr_arg = string option * constr_ast
and fix_kind = Fix | CoFix
and case_item = constr_ast * (string option * constr_ast option)
and pattern =
PatAs of pattern * string
| PatType of pattern * constr_ast
| PatConstr of string * pattern list
| PatVar of string
%}
%token <string> META
%token <string> INT
%token <string> IDENT
%token <string> INFIX
%token <string> PREFIX
%token <string> POSTFIX
%token LPAR RPAR BAR COMMA COLON BANG FUN DOT RARROW LET COLONEQ IN IF THEN ELSE EVAL AT FOR BQUOTE PROP SET TYPE WILDCARD FIX COFIX MATCH WITH ENDKW AND LBRACE RBRACE STRUCT AS SIMPL
%start constr
%type <constr_ast> constr
%%
paren_constr:
constr COMMA paren_constr { Pair($1,$3) }
| constr { $1 }
;
constr:
binder_constr { $1 }
| oper_constr { $1}
;
binder_constr:
BANG ne_binders DOT constr { Prod($2, $4) }
| FUN ne_binders type RARROW constr
{ Lambda($2,Cast($5,$3)) }
| LET IDENT binders type COLONEQ constr IN constr
{ Let($2,$6,Lambda($3,Cast($8,4))) }
| LET LPAR comma_binders RPAR COLONEQ constr IN constr
{ LetCase($3,$6,$8) }
| IF constr THEN constr ELSE constr { IfCase($2,$4,$6) }
| fix_constr { $1 }
| EVAL rfun IN constr { Eval($2,$4) }
;
comma_binders:
ne_comma_binders { $1 }
| { [] }
;
ne_comma_binders:
binder COMMA ne_comma_binders { $1 :: $3 }
| binder { [$1] }
;
rfun:
SIMPL { Simpl }
;
oper_constr:
oper_constr INFIX oper_constr { Infix($2,$1,$3) }
| PREFIX oper_constr { Prefix($1,$2) }
| oper_constr POSTFIX { Postfix($2,$1) }
| appl_constr { $1 }
;
appl_constr:
simple_constr ne_appl_args { Appl($1,$2) }
| AT global simple_constrs { ApplExpl($2,$3) }
| simple_constr { $1 }
;
appl_arg:
AT INT COLONEQ simple_constr { (Some $2,$4) }
| simple_constr { (None,$1) }
;
ne_appl_args:
appl_arg { [$1] }
| appl_arg ne_appl_args { $1::$2 }
;
simple_constr:
atomic_constr { $1 }
| match_constr { $1 }
| LPAR paren_constr RPAR { $2 }
| BQUOTE IDENT COLON paren_constr BQUOTE { Scope($2,$4) }
;
simple_constrs:
simple_constr simple_constrs { $1::$2 }
| { [] }
;
atomic_constr:
global { Qualid $1 }
| PROP { Prop }
| SET { Set }
| TYPE { Type }
| INT { Int $1 }
| WILDCARD { Hole }
| META { Meta $1 }
;
global:
IDENT DOT global { $1 :: $3 }
| IDENT { [$1] }
;
fix_constr:
fix_kw fix_decl
{ let (id,_,_,_,_ as fx) = $2 in Fixp($1,[fx],id) }
| fix_kw fix_decl fix_decls FOR IDENT { ($1, $2::$3, $5) }
;
fix_kw: FIX {Fix} | COFIX {CoFix}
;
fix_decl:
IDENT binders type annot COLONEQ constr { ($1,$2,$3,$4,$6) }
;
fix_decls:
AND fix_decl fix_decls { $2::$3 }
| AND fix_decl { [$2] }
;
annot:
LBRACE STRUCT IDENT RBRACE { Some $3 }
| { None }
;
match_constr:
MATCH case_items case_type WITH branches ENDKW { Match($2,$3,$5) }
;
case_items:
case_item { [$1] }
| case_item COMMA case_items { $1::$3 }
;
case_item:
constr pred_pattern { ($1,$2) }
;
case_type:
RARROW constr { Some $2 }
| { None }
;
pred_pattern:
AS IDENT COLON constr { (Some $2, Some $4) }
| AS IDENT { (Some $2, None) }
| COLON constr { (None, Some $2) }
| { (None,None) }
;
branches:
BAR branch_list { $2 }
| branch_list { $1 }
| { [] }
;
branch_list:
patterns RARROW constr { [$1, $3] }
| patterns RARROW constr BAR branch_list { ($1,$3)::$5 }
;
patterns:
pattern { [$1] }
| pattern COMMA patterns { $1::$3 }
;
pattern:
pattern AS IDENT { PatAs($1,$3) }
| pattern COLON constr { PatType($1,$3) }
| IDENT simple_patterns { PatConstr($1,$2) }
| simple_pattern { $1 }
;
simple_pattern:
IDENT { PatVar $1 }
| LPAR pattern RPAR { $2 }
;
simple_patterns:
simple_pattern { [$1] }
| simple_pattern simple_patterns { $1::$2 }
;
binder:
IDENT { ($1,Hole) }
| LPAR IDENT type RPAR { ($2,$3) }
;
binders:
ne_binders { $1 }
| { [] }
ne_binders:
binder { $1 }
| binder ne_binders { $1::$2 }
;
type:
COLON constr { $2 }
| { Hole }
;
|
