pgm_parser.mly 13.2 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
/**************************************************************************/
/*                                                                        */
/*  Copyright (C) 2010-                                                   */
/*    Francois Bobot                                                      */
/*    Jean-Christophe Filliatre                                           */
/*    Johannes Kanig                                                      */
/*    Andrei Paskevich                                                    */
/*                                                                        */
/*  This software is free software; you can redistribute it and/or        */
/*  modify it under the terms of the GNU Library General Public           */
/*  License version 2.1, with the special exception on linking            */
/*  described in file LICENSE.                                            */
/*                                                                        */
/*  This software is distributed in the hope that it will be useful,      */
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  */
/*                                                                        */
/**************************************************************************/

%{

  open Parsing
23
  open Lexing
24
  open Why
25
  open Ptree
26
27
28
29
30
31
  open Pgm_ptree

  let loc () = (symbol_start_pos (), symbol_end_pos ())
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)

32
33
  let mk_expr d = { expr_loc = loc (); expr_desc = d }
  let mk_expr_i i d = { expr_loc = loc_i i; expr_desc = d }
34
35
36

  let mk_pat p = { pat_loc = loc (); pat_desc = p }

37
38
39
40
  (* FIXME: factorize with parser/parser.mly *)
  let infix s = "infix " ^ s
  let prefix s = "prefix " ^ s
  let postfix s = "postfix " ^ s
41
42
43

  let join (b,_) (_,e) = (b,e)

44
  let rec mk_apply f = function
45
46
47
    | [] -> 
	assert false
    | [a] -> 
48
	Eapply (f, a)
49
    | a :: l -> 
50
	let loc = join f.expr_loc a.expr_loc in 
51
	mk_apply { expr_loc = loc; expr_desc = Eapply (f, a) } l
52
53

  let mk_apply_id id = 
54
    let e = 
55
      { expr_desc = Eident (Qident id); expr_loc = id.id_loc } 
56
    in
57
    mk_apply e
58
      
59
60
61
62
  let mk_infix e1 op e2 =
    let id = { id = infix op; id_loc = loc_i 2 } in
    mk_expr (mk_apply_id id [e1; e2])
     
63
64
65
66
  let mk_binop e1 op e2 =
    let id = { id = op; id_loc = loc_i 2 } in
    mk_expr (mk_apply_id id [e1; e2])
     
67
68
69
  let mk_prefix op e1 =
    let id = { id = prefix op; id_loc = loc_i 1 } in
    mk_expr (mk_apply_id id [e1])
70

71
  let id_unit () = { id = "unit"; id_loc = loc () }
72
  let id_result () = { id = "result"; id_loc = loc () }
73
  let id_anonymous () = { id = "_"; id_loc = loc () }
74
  let exit_exn () = { id = "%Exit"; id_loc = loc () }
75

76
  let id_lt_nat () = Qident { id = "lt_nat"; id_loc = loc () }
77

78
  let ty_unit () = Tpure (PPTtyapp ([], Qident (id_unit ())))
79

80
81
  let lexpr_true () = symbol_start_pos (), "true"
  let lexpr_false () = symbol_start_pos (), "false"
82

83
84
  let empty_effect = { pe_reads = []; pe_writes = []; pe_raises = [] }

85
  let type_c p ty ef q =
86
    { pc_result_type = ty;
87
88
89
90
      pc_effect      = ef;
      pc_pre         = p;
      pc_post        = q; }

91
92
93
94
  let cast_body c ((p,e,q) as t) = match c with
    | None -> t
    | Some pt -> p, { e with expr_desc = Ecast (e, pt) }, q

95
96
97
98
99
100
101
%}

/* Tokens */ 

%token <string> LIDENT UIDENT
%token <string> INTEGER
%token <string> OP0 OP1 OP2 OP3
102
%token <Why.Ptree.real_constant> REAL
103
%token <string> STRING
104
%token <Lexing.position * string> LOGIC
105
106
107

/* keywords */

108
%token ABSURD AND ANY AS ASSERT ASSUME BEGIN CHECK DO DONE ELSE END
109
%token EXCEPTION FOR
110
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH NOT OF PARAMETER
111
%token RAISE RAISES READS REC 
112
%token THEN TRY TYPE VARIANT WHILE WITH WRITES
113
114
115

/* symbols */

116
%token UNDERSCORE QUOTE COMMA LEFTPAR RIGHTPAR COLON SEMICOLON
117
%token COLONEQUAL ARROW EQUAL AT DOT LEFTSQ RIGHTSQ BANG
118
%token LEFTBLEFTB RIGHTBRIGHTB BAR BARBAR AMPAMP
119
%token EOF
120
121
122

/* Precedences */

123
124
125
%nonassoc prec_post
%nonassoc BAR

126
%nonassoc prec_id_pattern
127
%nonassoc prec_recfun
128
129
%nonassoc prec_triple
%left LEFTBLEFTB
130
131
132
133
134
135
%left prec_simple

%left COLON 

%left prec_letrec
%left IN
136
%nonassoc GHOST
137
138
139
140
141
142
143

%right SEMICOLON

%left prec_no_else
%left ELSE

%left COLONEQUAL
144
145
%right BARBAR
%right AMPAMP
146
147
148
149
%right prec_if
%left EQUAL OP0
%left OP1
%left OP2
150
%left OP3
151
%nonassoc prefix_op
152
153
154
155
156
157
158
159
%right unary_op
%left prec_app
%left prec_ident
%left LEFTSQ

%nonassoc prec_decls
%nonassoc LOGIC TYPE INDUCTIVE

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
/* Entry points */

%type <Pgm_ptree.file> file
%start file

%%

file:
| list0_decl EOF { $1 }
;

list0_decl:
| /* epsilon */
   { [] }
| list1_decl 
   { $1 }
;

list1_decl:
| decl 
   { [$1] }
| decl list1_decl 
   { $1 :: $2 }
;

decl:
188
| LOGIC
189
190
191
    { Dlogic $1 }
| LET lident list1_type_v_binder opt_cast EQUAL triple
    { Dlet ($2, mk_expr_i 3 (Efun ($3, cast_body $4 $6))) }
192
193
| LET REC list1_recfun_sep_and 
    { Dletrec $3 }
194
195
| PARAMETER lident COLON type_v
    { Dparam ($2, $4) }
196
197
198
199
| EXCEPTION uident 
    { Dexn ($2, None) }
| EXCEPTION uident OF pure_type
    { Dexn ($2, Some $4) }
200
201
202
203
204
205
206
207
;

list1_recfun_sep_and:
| recfun                          { [ $1 ] }
| recfun AND list1_recfun_sep_and { $1 :: $3 }
;

recfun:
208
209
| lident list1_type_v_binder opt_cast opt_variant EQUAL triple
   { $1, $2, $4, cast_body $3 $6 }
210
211
212
;

lident:
213
214
215
216
217
218
219
220
221
222
| LIDENT { { id = $1; id_loc = loc () } }
;

uident:
| UIDENT { { id = $1; id_loc = loc () } }
;

ident:
| uident { $1 }
| lident { $1 }
223
224
225
226
227
228
229
230
;

any_op:
| OP0   { $1 }
| OP2   { $1 }
| OP3   { $1 }
;

231
232
233
qualid:
| ident             { Qident $1 }
| uqualid DOT ident { Qdot ($1, $3) }
234
235
236
237
238
239
240
241
242
243
244
245
246
;

lqualid:
| lident             { Qident $1 }
| uqualid DOT lident { Qdot ($1, $3) }
;

uqualid:
| uident             { Qident $1 }
| uqualid DOT uident { Qdot ($1, $3) }
;

expr:
247
248
| simple_expr %prec prec_simple 
   { $1 }
249
| expr EQUAL expr 
250
   { mk_binop $1 "eq_bool" $3 }
251
| expr OP0 expr 
252
   { mk_binop $1 ($2 ^ "_bool") $3 }
253
| expr OP1 expr 
254
   { mk_infix $1 $2 $3 }
255
| expr OP2 expr 
256
   { mk_infix $1 $2 $3 }
257
| expr OP3 expr 
258
   { mk_infix $1 $2 $3 }
259
260
| NOT expr %prec prefix_op
   { mk_expr (mk_apply_id { id = "notb"; id_loc = loc () } [$2]) }
261
| any_op expr %prec prefix_op
262
   { mk_prefix $1 $2 }
263
264
| expr COLONEQUAL expr 
   { mk_infix $1 ":=" $3 }
265
266
| simple_expr list1_simple_expr %prec prec_app
   { mk_expr (mk_apply $1 $2) }
267
268
269
270
271
272
| IF expr THEN expr ELSE expr
   { mk_expr (Eif ($2, $4, $6)) }
| IF expr THEN expr %prec prec_no_else
   { mk_expr (Eif ($2, $4, mk_expr Eskip)) }
| expr SEMICOLON expr
   { mk_expr (Esequence ($1, $3)) }
273
| assertion_kind LOGIC
274
   { mk_expr (Eassert ($1, $2)) }
275
| expr AMPAMP expr
276
   { mk_expr (Elazy (LazyAnd, $1, $3)) }
277
| expr BARBAR expr
278
   { mk_expr (Elazy (LazyOr, $1, $3)) }
279
280
| LET lident EQUAL expr IN expr
   { mk_expr (Elet ($2, $4, $6)) }
281
282
| LET pattern EQUAL expr IN expr 
   { mk_expr (Ematch ([$4], [[$2], $6])) }
283
| LET lident list1_type_v_binder EQUAL triple IN expr
284
285
286
   { mk_expr (Elet ($2, mk_expr_i 3 (Efun ($3, $5)), $7)) }
| LET REC list1_recfun_sep_and IN expr
   { mk_expr (Eletrec ($3, $5)) }
287
| FUN list1_type_v_binder ARROW triple
288
   { mk_expr (Efun ($2, $4)) }
289
290
| MATCH list1_expr_sep_comma WITH option_bar match_cases END
   { mk_expr (Ematch ($2, $5)) }
291
292
| LABEL uident COLON expr
   { mk_expr (Elabel ($2, $4)) }
293
| WHILE expr DO loop_annotation expr DONE
294
295
296
297
298
299
300
   { mk_expr 
       (Etry 
	  (mk_expr
	     (Eloop ($4, 
		     mk_expr (Eif ($2, $5,
				   mk_expr (Eraise (exit_exn (), None)))))),
	   [exit_exn (), None, mk_expr Eskip])) }
301
302
| ABSURD
   { mk_expr Eabsurd }
303
| expr COLON pure_type
304
   { mk_expr (Ecast ($1, $3)) }
305
306
307
308
| RAISE uident
   { mk_expr (Eraise ($2, None)) }
| RAISE LEFTPAR uident expr RIGHTPAR
   { mk_expr (Eraise ($3, Some $4)) }
309
310
311
312
| TRY expr WITH option_bar list1_handler_sep_bar END
   { mk_expr (Etry ($2, $5)) }
| ANY simple_type_c
   { mk_expr (Eany $2) }
313
314
| LEFTPAR expr COMMA list1_expr_sep_comma RIGHTPAR
   { mk_expr (Etuple ($2 :: $4)) }
315
316
;

317
triple:
318
319
| pre expr post
  { $1, $2, $3 }
320
| expr %prec prec_triple
321
  { lexpr_true (), $1, (lexpr_true (), []) }
322
323
;

324
325
326
simple_expr:
| constant
    { mk_expr (Econstant $1) }
327
| BANG simple_expr
328
    { mk_prefix "!" $2 }
329
| qualid 
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
    { mk_expr (Eident $1) }
| LEFTPAR expr RIGHTPAR
    { $2 }
| BEGIN expr END
    { $2 }
| LEFTPAR RIGHTPAR
    { mk_expr Eskip }
| BEGIN END
    { mk_expr Eskip }
;

list1_simple_expr:
| simple_expr %prec prec_simple { [$1] }
| simple_expr list1_simple_expr { $1 :: $2 }
;

346
347
348
349
350
351
352
353
354
355
list1_expr_sep_comma:
| expr                            { [$1] }
| expr COMMA list1_expr_sep_comma { $1 :: $3 }
;

option_bar:
| /* epsilon */ { () }
| BAR           { () }
;

356
357
358
359
360
361
362
363
364
365
366
list1_handler_sep_bar:
| handler                           { [$1] }
| handler BAR list1_handler_sep_bar { $1 :: $3 }
;

handler:
| ident ARROW expr            { ($1, None, $3) }
| ident ident ARROW expr      { ($1, Some $2, $4) }
| ident UNDERSCORE ARROW expr { ($1, Some (id_anonymous ()), $4) }
;

367
368
369
370
371
372
373
374
375
376
377
378
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
| list1_pat_sep_comma ARROW expr { ($1,$3) }
;

list1_pat_sep_comma:
| pattern                           { [$1] }
| pattern COMMA list1_pat_sep_comma { $1::$3 }
379
;
380
381

pattern:
382
383
384
385
386
387
388
389
390
391
392
393
394
| pat_arg           { $1 }
| uqualid pat_args  { mk_pat (PPpapp ($1, $2)) }
| pattern AS lident { mk_pat (PPpas ($1,$3)) }
;

pat_args:
| pat_arg          { [$1] }
| pat_arg pat_args { $1 :: $2 }
;

pat_arg:
| UNDERSCORE
   { mk_pat (PPpwild) }
395
| lident %prec prec_id_pattern
396
397
398
   { mk_pat (PPpvar $1) }
| uqualid                                       
   { mk_pat (PPpapp ($1, [])) }
399
| LEFTPAR pattern COMMA list1_pat_sep_comma RIGHTPAR          
400
401
402
403
404
405
406
   { mk_pat (PPptuple ($2 :: $4)) }
/*
| LEFTPAR RIGHTPAR          
   { mk_pat (PPptuple []) }
*/
| LEFTPAR pattern RIGHTPAR
   { $2 }
407
408
;

409
410
411
412
413
414
415
assertion_kind:
| ASSERT { Aassert }
| ASSUME { Aassume }
| CHECK  { Acheck  }
;

loop_annotation:
416
| loop_invariant opt_variant { { loop_invariant = $1; loop_variant = $2 } }
417
418
419
;

loop_invariant:
420
421
| INVARIANT LOGIC { Some $2 }
| /* epsilon */   { None    }
422
423
;

424
425
426
427
428
constant:
| INTEGER
   { Term.ConstInt $1 }
| REAL
   { Term.ConstReal $1 }
429
430
;

431
432
433
434
type_var:
| QUOTE ident { $2 }
;

435
436
437
pure_type:
| pure_type_arg_no_paren { $1 }
| lqualid pure_type_args { PPTtyapp ($2, $1) }
438
439
;

440
441
442
pure_type_args:
| pure_type_arg                { [$1] }
| pure_type_arg pure_type_args { $1 :: $2 }
443
444
;

445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
pure_type_arg:
| LEFTPAR pure_type RIGHTPAR { $2 }
| pure_type_arg_no_paren     { $1 }
;

pure_type_arg_no_paren:
| type_var 
   { PPTtyvar $1 }
| lqualid
   { PPTtyapp ([], $1) }
| LEFTPAR pure_type COMMA list1_pure_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
/*
| LEFTPAR RIGHTPAR
   { PPTtuple ([]) }
*/
461
462
;

463
list1_pure_type_sep_comma:
464
| pure_type                                 { [$1] }
465
466
467
| pure_type COMMA list1_pure_type_sep_comma { $1 :: $3 }
;

468
list1_type_v_binder:
469
470
| type_v_binder                     { $1 }
| type_v_binder list1_type_v_binder { $1 @ $2 }
471
472
473
;

type_v_binder:
474
475
476
477
478
479
480
481
482
483
484
| lident
   { [$1, None] }
| LEFTPAR RIGHTPAR                      
   { [id_anonymous (), Some (ty_unit ())] }
| LEFTPAR lidents COLON type_v RIGHTPAR
   { List.map (fun i -> (i, Some $4)) $2 }
;

lidents:
| lident         { [$1] }
| lident lidents { $1 :: $2 }
485
486
;

487
488
489
490
491
492
493
type_v:
| simple_type_v
   { $1 }
| simple_type_v ARROW type_c
   { Tarrow ([id_anonymous (), Some $1], $3) }
| lident COLON simple_type_v ARROW type_c
   { Tarrow ([$1, Some $3], $5) }
494
495
   /* TODO: we could alllow lidents instead, e.g. x y : int -> ... */
   /*{ Tarrow (List.map (fun x -> x, Some $3) $1, $5) }*/
496
497
498
499
500
501
502
503
504
;

simple_type_v:
| pure_type
    { Tpure $1 }
| LEFTPAR type_v RIGHTPAR
    { $2 }
;

505
506
type_c:
| type_v 
507
508
509
510
511
    { type_c (lexpr_true ()) $1 empty_effect (lexpr_true (), []) }
| pre type_v effects post
    { type_c $1 $2 $3 $4 }
;

512
/* for ANY */
513
simple_type_c:
514
| pure_type
515
516
517
    { type_c (lexpr_true ()) (Tpure $1) empty_effect (lexpr_true (), []) }
| LEFTPAR type_v RIGHTPAR
    { type_c (lexpr_true ()) $2 empty_effect (lexpr_true (), []) }
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
| pre type_v effects post
    { type_c $1 $2 $3 $4 }
;

pre:
| LOGIC { $1 }
;

post:
| LOGIC list0_post_exn { $1, $2 }
;

list0_post_exn:
| /* epsilon */  %prec prec_post { [] }
| list1_post_exn                 { $1 }
;

list1_post_exn:
| post_exn                %prec prec_post { [$1] }
| post_exn list1_post_exn                 { $1 :: $2 }
;

post_exn:
| BAR uident ARROW LOGIC { $2, $4 }
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
;

effects:
| opt_reads opt_writes opt_raises
    { { pe_reads = $1; pe_writes = $2; pe_raises = $3 } }
;

opt_reads:
| /* epsilon */               { [] }
| READS list0_lident_sep_comma { $2 }
;

opt_writes:
| /* epsilon */                { [] }
| WRITES list0_lident_sep_comma { $2 }
;

opt_raises:
| /* epsilon */                { [] }
| RAISES list0_uident_sep_comma { $2 }
562
563
564
;

opt_variant:
565
| /* epsilon */             { None }
566
| VARIANT LOGIC             { Some ($2, id_lt_nat ()) }
567
| VARIANT LOGIC FOR lqualid { Some ($2, $4) }
568
569
;

570
571
572
573
574
opt_cast:
| /* epsilon */   { None }
| COLON pure_type { Some $2 }
;

575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
list0_lident_sep_comma:
| /* epsilon */          { [] }
| list1_lident_sep_comma { $1 }
;

list1_lident_sep_comma:
| lident                              { [$1] }
| lident COMMA list1_lident_sep_comma { $1 :: $3 }
;

list0_uident_sep_comma:
| /* epsilon */          { [] }
| list1_uident_sep_comma { $1 }
;

list1_uident_sep_comma:
| uident                              { [$1] }
| uident COMMA list1_uident_sep_comma { $1 :: $3 }
;

/*
Local Variables: 
compile-command: "unset LANG; make -C ../.. testl"
End: 
*/

601