parser.mly 36.7 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
/********************************************************************/
/*                                                                  */
/*  The Why3 Verification Platform   /   The Why3 Development Team  */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
/*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  */
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
9
10
/*                                                                  */
/*  This software is distributed under the terms of the GNU Lesser  */
/*  General Public License version 2.1, with the special exception  */
/*  on linking described in file LICENSE.                           */
/*                                                                  */
/********************************************************************/
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11
12

%{
13
module Incremental = struct
14
15
16
17
18
19
20
  let stack = Stack.create ()
  let open_file inc = Stack.push inc stack
  let close_file () = ignore (Stack.pop stack)
  let open_theory id = (Stack.top stack).Ptree.open_theory id
  let close_theory () = (Stack.top stack).Ptree.close_theory ()
  let open_module id = (Stack.top stack).Ptree.open_module id
  let close_module () = (Stack.top stack).Ptree.close_module ()
21
22
  let open_namespace n = (Stack.top stack).Ptree.open_namespace n
  let close_namespace l b = (Stack.top stack).Ptree.close_namespace l b
23
24
25
  let new_decl loc d = (Stack.top stack).Ptree.new_decl loc d
  let new_pdecl loc d = (Stack.top stack).Ptree.new_pdecl loc d
  let use_clone loc use = (Stack.top stack).Ptree.use_clone loc use
26
end
27

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28
29
30
  open Ptree

  let loc () = (symbol_start_pos (), symbol_end_pos ())
31
32
  let floc () = Loc.extract (loc ())

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
33
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
34
  let floc_i i = Loc.extract (loc_i i)
35

36
(* dead code
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
37
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
38
  let floc_ij i j = Loc.extract (loc_ij i j)
39
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
40

41
42
  let mk_pp_l loc d = { pp_loc = loc; pp_desc = d }
  let mk_pp d = { pp_loc = floc (); pp_desc = d }
Andrei Paskevich's avatar
Andrei Paskevich committed
43

44
  let mk_pat p = { pat_loc = floc (); pat_desc = p }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45

46
47
  let infix_pp a i b = mk_pp (PPbinop (a, i, b))
  let prefix_pp p a = mk_pp (PPunop (p, a))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
48

49
  let infix  s = "infix "  ^ s
50
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
51
  let mixfix s = "mixfix " ^ s
52

53
54
55
56
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

  let add_lab id l = { id with id_lab = l }

Andrei Paskevich's avatar
Andrei Paskevich committed
57
58
  let mk_l_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
59
    mk_pp (PPidapp (Qident id, [e1]))
Andrei Paskevich's avatar
Andrei Paskevich committed
60
61
62
63
64
65
66

  let mk_l_infix e1 op e2 =
    let id = mk_id (infix op) (floc_i 2) in
    mk_pp (PPinfix (e1, id, e2))

  let mk_l_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
67
    mk_pp (PPidapp (Qident id, [e1;e2]))
Andrei Paskevich's avatar
Andrei Paskevich committed
68
69
70

  let mk_l_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
71
    mk_pp (PPidapp (Qident id, [e1;e2;e3]))
Andrei Paskevich's avatar
Andrei Paskevich committed
72

73
74
75
  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
76
      | _ -> raise exn)
77

78
  let mk_expr_l loc d = { expr_loc = loc; expr_desc = d }
79
  let mk_expr d = { expr_loc = floc (); expr_desc = d }
80

81
82
83
84
85
86
87
  let mk_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
    mk_expr (Eidapp (Qident id, [e1]))

  let mk_infix e1 op e2 =
    let id = mk_id (infix op) (floc_i 2) in
    mk_expr (Einfix (e1, id, e2))
88

Andrei Paskevich's avatar
Andrei Paskevich committed
89
90
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
91
    mk_expr (Eidapp (Qident id, [e1; e2]))
92

Andrei Paskevich's avatar
Andrei Paskevich committed
93
94
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
95
    mk_expr (Eidapp (Qident id, [e1; e2; e3]))
96

Andrei Paskevich's avatar
Andrei Paskevich committed
97
  let id_anonymous () = mk_id "_" (floc ())
98

99
100
101
102
103
104
105
106
107
108
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
    | _, _ -> Loc.errorm ~loc:(floc ())
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
109
    sp_reads   = [];
110
111
    sp_writes  = [];
    sp_variant = [];
112
113
    sp_checkrw = false;
    sp_diverge = false;
114
  }
115

116
117
118
119
  let spec_union s1 s2 = {
    sp_pre     = s1.sp_pre @ s2.sp_pre;
    sp_post    = s1.sp_post @ s2.sp_post;
    sp_xpost   = s1.sp_xpost @ s2.sp_xpost;
120
    sp_reads   = s1.sp_reads @ s2.sp_reads;
121
122
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
123
124
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
125
  }
126

127
(* dead code
128
  let add_init_mark e =
129
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
130
    { e with expr_desc = Emark (init, e) }
131
*)
132

133
134
135
  let small_integer i =
    try
      match i with
136
137
138
139
      | Number.IConstDec s -> int_of_string s
      | Number.IConstHex s -> int_of_string ("0x"^s)
      | Number.IConstOct s -> int_of_string ("0o"^s)
      | Number.IConstBin s -> int_of_string ("0b"^s)
140
141
    with Failure _ -> raise Parsing.Parse_error

142
143
144
  let qualid_last = function
    | Qident x | Qdot (_, x) -> x.id

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
145
146
%}

147
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
148

149
%token <string> LIDENT UIDENT
150
%token <Ptree.integer_constant> INTEGER
151
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152
153
%token <Ptree.real_constant> FLOAT
%token <string> STRING
154
%token <Loc.position> POSITION
155
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
156
157
158

/* keywords */

159
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
160
161
162
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
Andrei Paskevich's avatar
Andrei Paskevich committed
163
%token THEN THEORY TRUE TYPE USE WITH
164

165
166
/* program keywords */

167
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DIVERGES DO DONE DOWNTO
168
%token ENSURES EXCEPTION FOR
169
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE PRIVATE RAISE
170
%token RAISES READS REC REQUIRES RETURNS TO TRY VAL VARIANT WHILE WRITES
171

172
173
/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
174
%token AND ARROW
175
%token BAR
176
%token COLON COMMA
177
%token DOT EQUAL LAMBDA LTGT
178
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
179
%token LARROW LRARROW OR
180
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
181
%token UNDERSCORE
182
183
184

%token EOF

185
186
/* program symbols */

187
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
188

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189
190
/* Precedences */

191
%nonassoc prec_mark
192
%nonassoc prec_fun
193
%nonassoc IN
194
195
196
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
197
%nonassoc prec_no_else
198
%nonassoc DOT ELSE GHOST
199
%nonassoc prec_named
200
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
201

Andrei Paskevich's avatar
Andrei Paskevich committed
202
%right ARROW LRARROW
203
204
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
205
%nonassoc NOT
206
%left EQUAL LTGT OP1
207
208
%nonassoc LARROW
%nonassoc RIGHTSQ    /* stronger than <- for e1[e2 <- e3] */
209
%left OP2
210
%left OP3
211
%left OP4
212
%nonassoc prec_prefix_op
213
214
%nonassoc LEFTSQ
%nonassoc OPPREF
215

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
216
217
/* Entry points */

218
219
220
%type <Ptree.incremental -> unit> open_file
%start open_file
%type <unit> logic_file
Andrei Paskevich's avatar
Andrei Paskevich committed
221
%start logic_file
222
%type <unit> program_file
223
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
224
225
%%

226
227
open_file:
| /* epsilon */  { Incremental.open_file }
228
229
;

Andrei Paskevich's avatar
Andrei Paskevich committed
230
logic_file:
231
| list0_theory EOF  { Incremental.close_file () }
232
233
234
;

/* File, theory, namespace */
235

236
237
238
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
239
240
;

241
theory_head:
242
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
243
244
;

245
theory:
246
| theory_head list0_decl END  { Incremental.close_theory () }
247
248
;

249
list0_decl:
250
251
| /* epsilon */        { () }
| new_decl list0_decl  { () }
252
| new_ns_th list0_decl { () }
253
254
255
256
;

new_decl:
| decl
257
   { Incremental.new_decl (floc ()) $1 }
258
| use_clone
259
   { Incremental.use_clone (floc ()) $1 }
260
261
262
;

new_ns_th:
263
264
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
265
266
;

267
namespace_head:
268
269
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
270
271
272
273
274
275
276
277
278
;

namespace_import:
| /* epsilon */  { false }
| IMPORT         { true }
;

/* Declaration */

279
decl:
280
281
| TYPE list1_type_decl
    { TypeDecl $2 }
282
283
| TYPE late_invariant
    { TypeDecl [$2] }
284
285
| CONSTANT logic_decl_constant
    { LogicDecl [$2] }
Andrei Paskevich's avatar
Andrei Paskevich committed
286
287
288
| FUNCTION list1_logic_decl_function
    { LogicDecl $2 }
| PREDICATE list1_logic_decl_predicate
289
    { LogicDecl $2 }
290
291
| inductive list1_inductive_decl
    { IndDecl ($1, $2) }
292
| AXIOM ident labels COLON lexpr
293
    { PropDecl (Kaxiom, add_lab $2 $3, $5) }
294
| LEMMA ident labels COLON lexpr
295
    { PropDecl (Klemma, add_lab $2 $3, $5) }
296
| GOAL ident labels COLON lexpr
297
    { PropDecl (Kgoal, add_lab $2 $3, $5) }
298
| META sident list1_meta_arg_sep_comma
299
    { Meta ($2, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
300
301
;

302
303
304
305
306
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

307
308
/* Use and clone */

309
310
use_clone:
| USE use
311
    { ($2, None) }
312
| CLONE use clone_subst
313
    { ($2, Some $3) }
314
315
;

316
use:
317
318
319
320
321
322
| opt_import tqualid
    { { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
| opt_import tqualid AS uident
    { { use_theory = $2; use_import = Some ($1, $4.id) } }
| EXPORT tqualid
    { { use_theory = $2; use_import = None } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
323
324
;

325
326
327
opt_import:
| /* epsilon */ { false }
| IMPORT        { true  }
328
329
330
331
332
333
334
335
336
337
338
339
340
;

clone_subst:
| /* epsilon */          { [] }
| WITH list1_comma_subst { $2 }
;

list1_comma_subst:
| subst                         { [$1] }
| subst COMMA list1_comma_subst { $1 :: $3 }
;

subst:
341
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
342
343
| TYPE qualid type_args EQUAL primitive_type
                                { CStsym (floc (), $2, $3, $5) }
344
345
346
| CONSTANT  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| FUNCTION  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }
Andrei Paskevich's avatar
Andrei Paskevich committed
347
| VAL       qualid EQUAL qualid { CSvsym (floc (), $2, $4) }
348
349
| LEMMA     qualid              { CSlemma (floc (), $2) }
| GOAL      qualid              { CSgoal  (floc (), $2) }
350
351
;

352
353
354
355
356
ns:
| uqualid { Some $1 }
| DOT     { None }
;

357
358
359
360
361
362
363
364
/* Meta args */

list1_meta_arg_sep_comma:
| meta_arg                                { [$1] }
| meta_arg COMMA list1_meta_arg_sep_comma { $1 :: $3 }
;

meta_arg:
365
366
| TYPE primitive_type { PMAty $2 }
| CONSTANT  qualid { PMAfs  $2 }
367
368
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
369
370
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
371
| INTEGER          { PMAint (small_integer $1) }
372
373
;

374
375
376
/* Type declarations */

list1_type_decl:
377
378
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
379
380
381
;

type_decl:
382
| lident labels type_args typedefn
383
  { let model, vis, def, inv = $4 in
384
    let vis = if model then Abstract else vis in
385
    { td_loc = floc (); td_ident = add_lab $1 $2;
386
387
      td_params = $3; td_model = model;
      td_vis = vis; td_def = def; td_inv = inv } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
388
389
;

390
391
392
393
394
395
396
late_invariant:
| lident labels type_args invariant type_invariant
  { { td_loc = floc (); td_ident = add_lab $1 $2;
      td_params = $3; td_model = false;
      td_vis = Public; td_def = TDabstract; td_inv = $4::$5 } }
;

397
type_args:
398
399
| /* epsilon */                 { [] }
| quote_lident labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
400
401
402
;

typedefn:
403
| /* epsilon */
404
    { false, Public, TDabstract, [] }
405
| equal_model visibility typecases type_invariant
406
    { $1, $2, TDalgebraic $3, $4 }
407
| equal_model visibility BAR typecases type_invariant
408
    { $1, $2, TDalgebraic $4, $5 }
409
| equal_model visibility record_type type_invariant
410
    { $1, $2, TDrecord $3, $4 }
411
412
413
/* abstract/private is not allowed for alias type */
| equal_model visibility primitive_type
    { if $2 <> Public then Loc.error ~loc:(floc_i 2) Parsing.Parse_error;
414
      $1, Public, TDalias $3, [] }
415
416
417
418
419
420
;

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
421
422
423
424
425
;

equal_model:
| EQUAL { false }
| MODEL { true }
426
427
428
;

record_type:
429
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
430
431
432
433
;

list1_record_field:
| record_field                              { [$1] }
434
| list1_record_field SEMICOLON record_field { $3 :: $1 }
435
436
;

437
438
439
440
441
442
443
444
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

445
record_field:
446
447
448
449
450
451
| field_modifiers lident labels COLON primitive_type
   { { f_loc = floc ();
       f_ident = add_lab $2 $3;
       f_mutable = fst $1;
       f_ghost = snd $1;
       f_pty = $5 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
452
453
454
455
456
457
458
459
;

typecases:
| typecase                { [$1] }
| typecase BAR typecases  { $1::$3 }
;

typecase:
460
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
461
462
463
464
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
465
466
467
468
469
470
471
472
473
474
list1_logic_decl_function:
| logic_decl_function                        { [$1] }
| logic_decl_function WITH list1_logic_decl  { $1 :: $3 }
;

list1_logic_decl_predicate:
| logic_decl_predicate                        { [$1] }
| logic_decl_predicate WITH list1_logic_decl  { $1 :: $3 }
;

475
list1_logic_decl:
476
477
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
478
479
;

480
481
482
483
484
485
logic_decl_constant:
| lident_rich labels COLON primitive_type logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = []; ld_type = Some $4; ld_def = $5 } }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
486
logic_decl_function:
487
| lident_rich labels list0_param COLON primitive_type logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
488
489
490
491
492
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;

logic_decl_predicate:
493
| lident_rich labels list0_param logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
494
495
496
497
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = None; ld_def = $4 } }
;

498
logic_decl:
499
| lident_rich labels list0_param opt_cast logic_def_option
500
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
501
      ld_params = $3; ld_type = $4; ld_def = $5 } }
502
503
504
505
506
;

logic_def_option:
| /* epsilon */ { None }
| EQUAL lexpr   { Some $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
507
508
;

509
510
511
/* Inductive declarations */

list1_inductive_decl:
512
513
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
514
515
516
;

inductive_decl:
517
| lident_rich labels list0_param inddefn
518
  { { in_loc = floc (); in_ident = add_lab $1 $2;
519
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
520
;
521

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
522
523
524
525
526
527
528
529
530
531
532
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

indcases:
| indcase               { [$1] }
| indcase BAR indcases  { $1::$3 }
;

indcase:
533
| ident labels COLON lexpr { (floc (), add_lab $1 $2, $4) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
534
535
;

536
537
538
/* Type expressions */

primitive_type:
539
540
541
| primitive_type_arg                  { $1 }
| lqualid primitive_type_args         { PPTtyapp ($1, $2) }
| primitive_type ARROW primitive_type { PPTarrow ($1, $3) }
542
543
544
545
546
547
548
549
;

primitive_type_args:
| primitive_type_arg                      { [$1] }
| primitive_type_arg primitive_type_args  { $1 :: $2 }
;

primitive_type_arg:
550
551
| lqualid
   { PPTtyapp ($1, []) }
552
553
554
555
| quote_lident
   { PPTtyvar ($1, false) }
| opaque_quote_lident
   { PPTtyvar ($1, true) }
556
557
| LEFTPAR list2_primitive_type_sep_comma RIGHTPAR
   { PPTtuple $2 }
558
559
560
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
561
   { PPTparen $2 }
562
563
;

564
565
566
567
list2_primitive_type_sep_comma:
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
568
569
570
571
572
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

573
574
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
575
lexpr:
576
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
577
   { infix_pp $1 PPimplies $3 }
578
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
579
   { infix_pp $1 PPiff $3 }
580
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
581
   { infix_pp $1 PPor $3 }
582
| lexpr BARBAR lexpr
583
   { infix_pp $1 PPor_asym $3 }
584
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
585
   { infix_pp $1 PPand $3 }
586
| lexpr AMPAMP lexpr
587
   { infix_pp $1 PPand_asym $3 }
588
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
589
   { prefix_pp PPnot $2 }
590
| lexpr EQUAL lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
591
   { mk_l_infix $1 "=" $3 }
592
| lexpr LTGT lexpr
593
   { mk_l_infix $1 "<>" $3 }
594
| lexpr OP1 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
595
   { mk_l_infix $1 $2 $3 }
596
| lexpr OP2 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
597
   { mk_l_infix $1 $2 $3 }
598
| lexpr OP3 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
599
   { mk_l_infix $1 $2 $3 }
600
| lexpr OP4 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
601
   { mk_l_infix $1 $2 $3 }
602
| prefix_op lexpr %prec prec_prefix_op
Andrei Paskevich's avatar
Andrei Paskevich committed
603
   { mk_l_prefix $1 $2 }
604
605
606
607
| lexpr_arg list1_lexpr_arg /* FIXME/TODO: "lexpr lexpr_arg" */
   { let b = rhs_start_pos 1 in
     List.fold_left (fun f (e,a) ->
       mk_pp_l (Loc.extract (b,e)) (PPapply (f,a))) $1 $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
608
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
609
   { mk_pp (PPif ($2, $4, $6)) }
610
| quant list1_quant_vars triggers DOT lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
611
   { mk_pp (PPquant ($1, $2, $3, $5)) }
612
613
| label lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
614
| LET pattern EQUAL lexpr IN lexpr
615
   { match $2.pat_desc with
616
617
618
619
620
     | PPpvar id -> mk_pp (PPlet (id, $4, $6))
     | PPpwild -> mk_pp (PPlet (id_anonymous (), $4, $6))
     | PPptuple [] -> mk_pp (PPlet (id_anonymous (),
          { $4 with pp_desc = PPcast ($4, PPTtuple []) }, $6))
     | _ -> mk_pp (PPmatch ($4, [$2, $6])) }
Andrei Paskevich's avatar
Andrei Paskevich committed
621
| MATCH lexpr WITH bar_ match_cases END
622
   { mk_pp (PPmatch ($2, $5)) }
623
624
| MATCH list2_lexpr_sep_comma WITH bar_ match_cases END
   { mk_pp (PPmatch (mk_pp (PPtuple $2), $5)) }
625
| lexpr COLON primitive_type
626
   { mk_pp (PPcast ($1, $3)) }
627
| lexpr_arg
628
629
630
   { match $1.pp_desc with (* break the infix relation chain *)
     | PPinfix (l,o,r) -> { $1 with pp_desc = PPinnfix (l,o,r) }
     | _ -> $1 }
631
632
;

633
634
635
636
637
638
639
640
641
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

field_value:
| lqualid EQUAL lexpr { $1, $3 }
;

642
list1_lexpr_arg:
643
644
| lexpr_arg                 { [rhs_end_pos 1, $1] }
| lexpr_arg list1_lexpr_arg { (rhs_end_pos 1, $1) :: $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
645
;
646

647
constant:
648
649
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
650
651
;

652
lexpr_arg:
653
| qualid            { mk_pp (PPident $1) }
Andrei Paskevich's avatar
Andrei Paskevich committed
654
655
656
657
658
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
659
| quote_uident      { mk_pp (PPident (Qident $1)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
660
661
662
;

lexpr_dot:
663
| lqualid_copy      { mk_pp (PPident $1) }
Andrei Paskevich's avatar
Andrei Paskevich committed
664
665
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
666
667
668
;

lexpr_sub:
669
| lexpr_dot DOT lqualid_rich
670
   { mk_pp (PPidapp ($3, [$1])) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
671
672
| LEFTPAR lexpr RIGHTPAR
   { $2 }
673
674
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
675
676
| LEFTPAR list2_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple $2) }
677
| LEFTBRC list1_field_value opt_semicolon RIGHTBRC
678
   { mk_pp (PPrecord (List.rev $2)) }
679
| LEFTBRC lexpr_arg WITH list1_field_value opt_semicolon RIGHTBRC
Andrei Paskevich's avatar
Andrei Paskevich committed
680
   { mk_pp (PPupdate ($2, List.rev $4)) }
681
| lexpr_arg LEFTSQ lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
682
   { mk_l_mixfix2 "[]" $1 $3 }
683
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
684
   { mk_l_mixfix3 "[<-]" $1 $3 $5 }
Andrei Paskevich's avatar
Andrei Paskevich committed
685
;
686

Andrei Paskevich's avatar
Andrei Paskevich committed
687
688
689
690
691
692
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

693
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
694

695
696
697
698
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
699

700
701
702
703
704
705
706
707
708
list1_trigger_sep_bar:
| trigger                           { [$1] }
| trigger BAR list1_trigger_sep_bar { $1 :: $3 }
;

trigger:
| list1_lexpr_sep_comma { $1 }
;

709
710
711
712
list2_lexpr_sep_comma:
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

713
714
715
716
717
718
list1_lexpr_sep_comma:
| lexpr                             { [$1] }
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

/* Match expressions */
719

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
720
721
722
723
724
725
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
726
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
727
728
729
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
| pat_conj              { $1 }
| pat_conj BAR pattern  { mk_pat (PPpor ($1, $3)) }
;

pat_conj:
| pat_uni                      { $1 }
| pat_uni COMMA list1_pat_uni  { mk_pat (PPptuple ($1::$3)) }
;

list1_pat_uni:
| pat_uni                      { [$1] }
| pat_uni COMMA list1_pat_uni  { $1::$3 }
;

pat_uni:
745
746
747
| pat_arg                   { $1 }
| uqualid list1_pat_arg     { mk_pat (PPpapp ($1, $2)) }
| pat_uni AS lident labels  { mk_pat (PPpas ($1, add_lab $3 $4)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
748
;
749

750
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
751
752
753
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
754

755
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
756
| UNDERSCORE                { mk_pat (PPpwild) }
757
| lident labels             { mk_pat (PPpvar (add_lab $1 $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
758
759
760
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
761
| LEFTBRC pfields RIGHTBRC  { mk_pat (PPprec $2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
762
763
764
765
766
767
768
769
770
;

pfields:
| pat_field opt_semicolon       { [$1] }
| pat_field SEMICOLON pfields   { $1::$3 }
;

pat_field:
| lqualid EQUAL pattern   { ($1, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
771
772
;

773
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
774

775
776
777
list0_param:
| /* epsilon */ { [] }
| list1_param   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
778
779
;

780
list1_param:
781
782
| param               { $1 }
| param list1_param   { $1 @ $2 }
783
784
785
786
787
788
789
;

list1_binder:
| binder              { $1 }
| binder list1_binder { $1 @ $2 }
;

790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
/* [param] and [binder] below must have the same grammar and
   raise [Parse_error] in the same cases. Interpretaion of
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
   names, whose type must be inferred. */

param:
| anon_binder
   { Loc.errorm ~loc:(floc ())
      "cannot determine the type of the parameter" }
| primitive_type_arg
   { [floc (), None, false, $1] }
| LEFTPAR GHOST primitive_type RIGHTPAR
   { [floc (), None, true, $3] }
| primitive_type_arg label labels
   { match $1 with
      | PPTtyapp (Qident _, []) -> Loc.errorm ~loc:(floc ())
          "cannot determine the type of the parameter"
      | _ -> Loc.error ~loc:(floc_i 2) Parsing.Parse_error }
| LEFTPAR binder_vars_rest RIGHTPAR
   { match $2 with [l,_] -> Loc.errorm ~loc:l
          "cannot determine the type of the parameter"
      | _ -> Loc.error ~loc:(floc_i 3) Parsing.Parse_error }
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
   { match $3 with [l,_] -> Loc.errorm ~loc:l
          "cannot determine the type of the parameter"
      | _ -> Loc.error ~loc:(floc_i 4) Parsing.Parse_error }
| LEFTPAR binder_vars COLON primitive_type RIGHTPAR
   { List.map (fun (l,i) -> l, i, false, $4) $2 }
| LEFTPAR GHOST binder_vars COLON primitive_type RIGHTPAR
   { List.map (fun (l,i) -> l, i, true, $5) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
821
822
;

823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
binder:
| anon_binder
   { Loc.errorm ~loc:(floc ())
      "cannot determine the type of the parameter" }
| primitive_type_arg
   { match $1 with
      | PPTtyapp (Qident id, [])
      | PPTparen (PPTtyapp (Qident id, [])) ->
             [floc (), Some id, false, None]
      | _ -> [floc (), None, false, Some $1] }
| LEFTPAR GHOST primitive_type RIGHTPAR
   { match $3 with
      | PPTtyapp (Qident id, []) ->
             [floc (), Some id, true, None]
      | _ -> [floc (), None, true, Some $3] }
| primitive_type_arg label labels
   { match $1 with
      | PPTtyapp (Qident id, []) ->
          [floc (), Some (add_lab id ($2::$3)), false, None]
      | _ -> Loc.error ~loc:(floc_i 2) Parsing.Parse_error }
| LEFTPAR binder_vars_rest RIGHTPAR
   { match $2 with [l,i] -> [l, i, false, None]
      | _ -> Loc.error ~loc:(floc_i 3) Parsing.Parse_error }
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
   { match $3 with [l,i] -> [l, i, true, None]
      | _ -> Loc.error ~loc:(floc_i 4) Parsing.Parse_error }
| LEFTPAR binder_vars COLON primitive_type RIGHTPAR
   { List.map (fun (l,i) -> l, i, false, Some $4) $2 }
| LEFTPAR GHOST binder_vars COLON primitive_type RIGHTPAR
   { List.map (fun (l,i) -> l, i, true, Some $5) $3 }
853
854
;

855
856
857
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
858
859
;

860
861
862
863
864
865
866
867
868
869
binder_vars_rest:
| binder_vars_head label labels list0_lident_labels
   { List.rev_append (match $1 with
      | (l, Some id) :: bl ->
          (Loc.join l (floc_i 3), Some (add_lab id ($2::$3))) :: bl
      | _ -> assert false) $4 }
| binder_vars_head anon_binder list0_lident_labels
   { List.rev_append $1 ($2 :: $3) }
| anon_binder list0_lident_labels
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
870
871
;

872
873
874
875
876
877
878
879
880
binder_vars_head:
| primitive_type {
    let of_id id = id.id_loc, Some id in
    let push acc = function
      | PPTtyapp (Qident id, []) -> of_id id :: acc
      | _ -> Loc.error ~loc:(floc ()) Parsing.Parse_error in
    match $1 with
      | PPTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
      | _ -> Loc.error ~loc:(floc ()) Parsing.Parse_error }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
881
882
;

883
884
885
886
887
888
list1_quant_vars:
| quant_vars                        { $1 }
| quant_vars COMMA list1_quant_vars { $1 @ $3 }
;

quant_vars:
889
890
891
892
| list1_lident_labels opt_cast {
    List.map (function
      | loc, None -> Loc.errorm ~loc "anonymous binders are not allowed here"
      | _, Some i -> i, $2) $1 }
893
894
;

895
list0_lident_labels:
896
897
898
899
900
901
902
903
904
905
| /* epsilon */        { [] }
| list1_lident_labels  { $1 }
;

list1_lident_labels:
| lident_labels list0_lident_labels  { $1 :: $2 }
;

lident_labels:
| lident labels { floc (), Some (add_lab $1 $2) }
906
907
908
| anon_binder   { $1 }

anon_binder:
909
| UNDERSCORE    { floc (), None }
910
911
;

912
913
914
915
916
/* Idents */

ident:
| uident { $1 }
| lident { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
917
918
;

Andrei Paskevich's avatar
Andrei Paskevich committed
919
920
921
922
923
924
925
926
927
928
929
930
931
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

lident:
| LIDENT          { mk_id $1 (floc ()) }
| lident_keyword  { mk_id $1 (floc ()) }
;

lident_keyword:
| MODEL           { "model" }
;

932
933
934
935
936
937
938
939
940
941
942
943
quote_uident:
| QUOTE_UIDENT    { mk_id ("'" ^ $1) (floc ()) }
;

quote_lident:
| QUOTE_LIDENT    { mk_id $1 (floc ()) }
;

opaque_quote_lident:
| OPAQUE_QUOTE_LIDENT { mk_id $1 (floc ()) }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
944
945
/* Idents + symbolic operations' names */

946
947
948
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
949
950
;

951
lident_rich:
Andrei Paskevich's avatar
Andrei Paskevich committed
952
953
954
955
956
| lident        { $1 }
| lident_op_id  { $1 }
;

lident_op_id:
957
| LEFTPAR lident_op RIGHTPAR  { mk_id $2 (floc_i 2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
958
| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") (floc ()) }
959
  /* FIXME: use location of operator star rather than left parenthesis */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
960
961
;

962
lident_op:
Andrei Paskevich's avatar
Andrei Paskevich committed
963
964
965
966
967
968
| prefix_op             { infix $1 }
| prefix_op UNDERSCORE  { prefix $1 }
| EQUAL                 { infix "=" }
| OPPREF                { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
969
| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
970
971
;

972
prefix_op:
973
974
975
976
977
978
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
979
/* Qualified idents */
980

Andrei Paskevich's avatar
Andrei Paskevich committed