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
|
%{
open Ast
open Parse
%}
%token <string> META INT IDENT
%token <string> OPER
%token LPAR RPAR BAR COMMA COLON BANG FUN DOT RARROW LET COLONEQ IN IF
%token THEN ELSE EVAL AT FOR PROP SET TYPE WILDCARD FIX
%token COFIX MATCH WITH END AND LBRACE RBRACE STRUCT AS SIMPL PERCENT
%token EOF
%start main
%type <Ast.constr_ast> main
%start constr
%type <Ast.constr_ast> constr
%start simple_constr
%type <Ast.constr_ast> simple_constr
%%
main:
constr EOF { $1 }
;
paren_constr:
constr COMMA paren_constr { Pair($1,$3) }
| constr { $1 }
;
constr:
binder_constr { $1 }
| oper_constr { close_stack $1 }
;
binder_constr:
BANG ne_binders DOT constr { Prod($2, $4) }
| FUN ne_binders type_cstr RARROW constr { Lambda($2,mk_cast $5 $3) }
| LET IDENT binders type_cstr COLONEQ constr IN constr
{ Let($2,mk_lambda $3 (mk_cast $6 $4),$8) }
| 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 }
;
/* 2 Conflits shift/reduce */
oper_constr:
oper_constr oper appl_constr
{ parse_term $3 (parse_oper $2 $1) }
| oper_constr oper binder_constr
{ parse_term $3 (parse_oper $2 $1) }
| oper_constr oper { parse_oper $2 $1 }
| { empty }
| appl_constr { parse_term $1 empty }
;
oper:
OPER {$1}
| COLON {":"}
;
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 }
| simple_constr PERCENT IDENT { Scope($3,$1) }
;
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] }
;
/* Conflit normal */
fix_constr:
fix_kw fix_decl
{ let (id,_,_,_,_ as fx) = $2 in Fixp($1,[fx],id) }
| fix_kw fix_decl fix_decls FOR IDENT { Fixp($1, $2::$3, $5) }
;
fix_kw: FIX {Fix} | COFIX {CoFix}
;
fix_decl:
IDENT binders type_cstr 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 END { 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_cstr RPAR { ($2,$3) }
;
binders:
ne_binders { $1 }
| { [] }
ne_binders:
binder { [$1] }
| binder ne_binders { $1::$2 }
;
type_cstr:
COLON constr { $2 }
| { Hole }
;
|
