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
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
|
/* $Id: CMparser.mly,v 1.2 2005/03/21 15:53:00 xleroy Exp $ */
%{
open Datatypes
open CList
open Camlcoq
open BinPos
open BinInt
open Integers
open AST
open Op
open Cminor
let intconst n =
Eop(Ointconst(coqint_of_camlint n), Enil)
let andbool e1 e2 =
Cmconstr.conditionalexpr e1 e2 (intconst 0l)
let orbool e1 e2 =
Cmconstr.conditionalexpr e1 (intconst 1l) e2
%}
%token ABSF
%token AMPERSAND
%token AMPERSANDAMPERSAND
%token ALLOC
%token BANG
%token BANGEQUAL
%token BANGEQUALF
%token BANGEQUALU
%token BAR
%token BARBAR
%token CARET
%token COLON
%token COMMA
%token DOLLAR
%token ELSE
%token EQUAL
%token EQUALEQUAL
%token EQUALEQUALF
%token EQUALEQUALU
%token EOF
%token EXIT
%token EXTERN
%token FLOAT
%token FLOAT32
%token FLOAT64
%token <float> FLOATLIT
%token FLOATOFINT
%token FLOATOFINTU
%token GREATER
%token GREATERF
%token GREATERU
%token GREATEREQUAL
%token GREATEREQUALF
%token GREATEREQUALU
%token GREATERGREATER
%token GREATERGREATERU
%token <AST.ident> IDENT
%token IF
%token IN
%token INT
%token INT16S
%token INT16U
%token INT32
%token INT8S
%token INT8U
%token <int32> INTLIT
%token INTOFFLOAT
%token LBRACE
%token LBRACELBRACE
%token LBRACKET
%token LESS
%token LESSU
%token LESSF
%token LESSEQUAL
%token LESSEQUALU
%token LESSEQUALF
%token LESSLESS
%token LET
%token LOOP
%token LPAREN
%token MINUS
%token MINUSF
%token MINUSGREATER
%token PERCENT
%token PERCENTU
%token PLUS
%token PLUSF
%token QUESTION
%token RBRACE
%token RBRACERBRACE
%token RBRACKET
%token RETURN
%token RPAREN
%token SEMICOLON
%token SLASH
%token SLASHF
%token SLASHU
%token STACK
%token STAR
%token STARF
%token <AST.ident> STRINGLIT
%token SWITCH
%token TILDE
%token VAR
%token VOID
/* Precedences from low to high */
%left COMMA
%left p_let
%right EQUAL
%right QUESTION COLON
%left BARBAR
%left AMPERSANDAMPERSAND
%left BAR
%left CARET
%left AMPERSAND
%left EQUALEQUAL BANGEQUAL LESS LESSEQUAL GREATER GREATEREQUAL EQUALEQUALU BANGEQUALU LESSU LESSEQUALU GREATERU GREATEREQUALU EQUALEQUALF BANGEQUALF LESSF LESSEQUALF GREATERF GREATEREQUALF
%left LESSLESS GREATERGREATER GREATERGREATERU
%left PLUS PLUSF MINUS MINUSF
%left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU
%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC
%left LPAREN
/* Entry point */
%start prog
%type <Cminor.program> prog
%%
/* Programs */
prog:
global_declarations proc_list EOF
{ { prog_funct = CList.rev $2;
prog_main = intern_string "main";
prog_vars = CList.rev $1; } }
;
global_declarations:
/* empty */ { Coq_nil }
| global_declarations global_declaration { Coq_cons($2, $1) }
;
global_declaration:
VAR STRINGLIT LBRACKET INTLIT RBRACKET
{ Coq_pair($2, Coq_cons(Init_space (z_of_camlint $4), Coq_nil)) }
;
proc_list:
/* empty */ { Coq_nil }
| proc_list proc { Coq_cons($2, $1) }
;
/* Procedures */
proc:
STRINGLIT LPAREN parameters RPAREN COLON signature
LBRACE
stack_declaration
var_declarations
stmt_list
RBRACE
{ Coq_pair($1,
Internal { fn_sig = $6;
fn_params = CList.rev $3;
fn_vars = CList.rev $9;
fn_stackspace = $8;
fn_body = $10 }) }
| EXTERN STRINGLIT COLON signature
{ Coq_pair($2,
External { ef_id = $2;
ef_sig = $4 }) }
;
signature:
type_
{ {sig_args = Coq_nil; sig_res = Some $1} }
| VOID
{ {sig_args = Coq_nil; sig_res = None} }
| type_ MINUSGREATER signature
{ let s = $3 in {s with sig_args = Coq_cons($1, s.sig_args)} }
;
parameters:
/* empty */ { Coq_nil }
| parameter_list { $1 }
;
parameter_list:
IDENT { Coq_cons($1, Coq_nil) }
| parameter_list COMMA IDENT { Coq_cons($3, $1) }
;
stack_declaration:
/* empty */ { Z0 }
| STACK INTLIT { z_of_camlint $2 }
;
var_declarations:
/* empty */ { Coq_nil }
| var_declarations var_declaration { CList.app $2 $1 }
;
var_declaration:
VAR parameter_list SEMICOLON { $2 }
;
/* Statements */
stmt:
expr SEMICOLON { Sexpr $1 }
| IF LPAREN expr RPAREN stmts ELSE stmts { Cmconstr.ifthenelse $3 $5 $7 }
| IF LPAREN expr RPAREN stmts { Cmconstr.ifthenelse $3 $5 Sskip }
| LOOP stmts { Sloop($2) }
| LBRACELBRACE stmt_list RBRACERBRACE { Sblock($2) }
| EXIT SEMICOLON { Sexit O }
| EXIT INTLIT SEMICOLON { Sexit (nat_of_camlint(Int32.pred $2)) }
| RETURN SEMICOLON { Sreturn None }
| RETURN expr SEMICOLON { Sreturn (Some $2) }
;
stmts:
LBRACE stmt_list RBRACE { $2 }
| stmt { $1 }
;
stmt_list:
/* empty */ { Sskip }
| stmt stmt_list { Sseq($1, $2) }
;
/* Expressions */
expr:
LPAREN expr RPAREN { $2 }
| IDENT { Evar $1 }
| IDENT EQUAL expr { Eassign($1, $3) }
| INTLIT { intconst $1 }
| FLOATLIT { Eop(Ofloatconst $1, Enil) }
| STRINGLIT { Eop(Oaddrsymbol($1, Int.zero), Enil) }
| AMPERSAND INTLIT { Eop(Oaddrstack(coqint_of_camlint $2), Enil) }
| MINUS expr %prec p_uminus { Cmconstr.negint $2 }
| MINUSF expr %prec p_uminus { Cmconstr.negfloat $2 }
| ABSF expr { Cmconstr.absfloat $2 }
| INTOFFLOAT expr { Cmconstr.intoffloat $2 }
| FLOATOFINT expr { Cmconstr.floatofint $2 }
| FLOATOFINTU expr { Cmconstr.floatofintu $2 }
| TILDE expr { Cmconstr.notint $2 }
| BANG expr { Cmconstr.notbool $2 }
| INT8S expr { Cmconstr.cast8signed $2 }
| INT8U expr { Cmconstr.cast8unsigned $2 }
| INT16S expr { Cmconstr.cast16signed $2 }
| INT16U expr { Cmconstr.cast16unsigned $2 }
| FLOAT32 expr { Cmconstr.singleoffloat $2 }
| ALLOC expr { Ealloc $2 }
| expr PLUS expr { Cmconstr.add $1 $3 }
| expr MINUS expr { Cmconstr.sub $1 $3 }
| expr STAR expr { Cmconstr.mul $1 $3 }
| expr SLASH expr { Cmconstr.divs $1 $3 }
| expr PERCENT expr { Cmconstr.mods $1 $3 }
| expr SLASHU expr { Cmconstr.divu $1 $3 }
| expr PERCENTU expr { Cmconstr.modu $1 $3 }
| expr AMPERSAND expr { Cmconstr.coq_and $1 $3 }
| expr BAR expr { Cmconstr.coq_or $1 $3 }
| expr CARET expr { Cmconstr.xor $1 $3 }
| expr LESSLESS expr { Cmconstr.shl $1 $3 }
| expr GREATERGREATER expr { Cmconstr.shr $1 $3 }
| expr GREATERGREATERU expr { Cmconstr.shru $1 $3 }
| expr PLUSF expr { Cmconstr.addf $1 $3 }
| expr MINUSF expr { Cmconstr.subf $1 $3 }
| expr STARF expr { Cmconstr.mulf $1 $3 }
| expr SLASHF expr { Cmconstr.divf $1 $3 }
| expr EQUALEQUAL expr { Cmconstr.cmp Ceq $1 $3 }
| expr BANGEQUAL expr { Cmconstr.cmp Cne $1 $3 }
| expr LESS expr { Cmconstr.cmp Clt $1 $3 }
| expr LESSEQUAL expr { Cmconstr.cmp Cle $1 $3 }
| expr GREATER expr { Cmconstr.cmp Cgt $1 $3 }
| expr GREATEREQUAL expr { Cmconstr.cmp Cge $1 $3 }
| expr EQUALEQUALU expr { Cmconstr.cmpu Ceq $1 $3 }
| expr BANGEQUALU expr { Cmconstr.cmpu Cne $1 $3 }
| expr LESSU expr { Cmconstr.cmpu Clt $1 $3 }
| expr LESSEQUALU expr { Cmconstr.cmpu Cle $1 $3 }
| expr GREATERU expr { Cmconstr.cmpu Cgt $1 $3 }
| expr GREATEREQUALU expr { Cmconstr.cmpu Cge $1 $3 }
| expr EQUALEQUALF expr { Cmconstr.cmpf Ceq $1 $3 }
| expr BANGEQUALF expr { Cmconstr.cmpf Cne $1 $3 }
| expr LESSF expr { Cmconstr.cmpf Clt $1 $3 }
| expr LESSEQUALF expr { Cmconstr.cmpf Cle $1 $3 }
| expr GREATERF expr { Cmconstr.cmpf Cgt $1 $3 }
| expr GREATEREQUALF expr { Cmconstr.cmpf Cge $1 $3 }
| memory_chunk LBRACKET expr RBRACKET { Cmconstr.load $1 $3 }
| memory_chunk LBRACKET expr RBRACKET EQUAL expr
{ Cmconstr.store $1 $3 $6 }
| expr LPAREN expr_list RPAREN COLON signature
{ Ecall($6, $1, $3) }
| expr AMPERSANDAMPERSAND expr { andbool $1 $3 }
| expr BARBAR expr { orbool $1 $3 }
| expr QUESTION expr COLON expr { Cmconstr.conditionalexpr $1 $3 $5 }
| LET expr IN expr %prec p_let { Elet($2, $4) }
| DOLLAR INTLIT { Eletvar (nat_of_camlint $2) }
;
expr_list:
/* empty */ { Enil }
| expr_list_1 { $1 }
;
expr_list_1:
expr %prec COMMA { Econs($1, Enil) }
| expr COMMA expr_list_1 { Econs($1, $3) }
;
memory_chunk:
INT8S { Mint8signed }
| INT8U { Mint8unsigned }
| INT16S { Mint16signed }
| INT16U { Mint16unsigned }
| INT32 { Mint32 }
| INT { Mint32 }
| FLOAT32 { Mfloat32 }
| FLOAT64 { Mfloat64 }
| FLOAT { Mfloat64 }
;
/* Types */
type_:
INT { Tint }
| FLOAT { Tfloat }
;
|
