parser.mly 36.1 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
/********************************************************************/
/*                                                                  */
/*  The Why3 Verification Platform   /   The Why3 Development Team  */
4
/*  Copyright 2010-2013   --   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

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
42
43
  let mk_pp d = mk_ppl (floc ()) d
  let mk_pat p = { pat_loc = floc (); pat_desc = p }
Andrei Paskevich's avatar
Andrei Paskevich committed
44

45
  let infix_ppl loc a i b = mk_ppl loc (PPbinop (a, i, b))
46
  let infix_pp a i b = infix_ppl (floc ()) a i b
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
47

48
  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
49
  let prefix_pp p a = prefix_ppl (floc ()) p a
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
50

51
  let infix  s = "infix "  ^ s
52
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
53
  let mixfix s = "mixfix " ^ s
54

55
56
57
58
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

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

59
  let mk_l_apply f a =
60
    let loc = Loc.join f.pp_loc a.pp_loc in
61
    { pp_loc = loc; pp_desc = PPapply (f,a) }
62

Andrei Paskevich's avatar
Andrei Paskevich committed
63
64
  let mk_l_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
65
    mk_pp (PPidapp (Qident id, [e1]))
Andrei Paskevich's avatar
Andrei Paskevich committed
66
67
68
69
70
71
72

  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
73
    mk_pp (PPidapp (Qident id, [e1;e2]))
Andrei Paskevich's avatar
Andrei Paskevich committed
74
75
76

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

79
80
81
  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
82
      | _ -> raise exn)
83

84
  let mk_expr d = { expr_loc = floc (); expr_desc = d }
85

86
87
  let mk_expr_i i d = { expr_loc = floc_i i; expr_desc = d }

88
  let mk_apply f a =
89
90
    let loc = Loc.join f.expr_loc a.expr_loc in
    { expr_loc = loc; expr_desc = Eapply (f,a) }
91

92
93
94
95
96
97
98
  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))
99

Andrei Paskevich's avatar
Andrei Paskevich committed
100
101
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
102
    mk_expr (Eidapp (Qident id, [e1; e2]))
103

Andrei Paskevich's avatar
Andrei Paskevich committed
104
105
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
106
    mk_expr (Eidapp (Qident id, [e1; e2; e3]))
107

Andrei Paskevich's avatar
Andrei Paskevich committed
108
  let id_anonymous () = mk_id "_" (floc ())
109

110
111
112
113
114
115
116
117
118
119
  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   = [];
120
    sp_reads   = [];
121
122
123
    sp_writes  = [];
    sp_variant = [];
  }
124

125
126
127
128
  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;
129
    sp_reads   = s1.sp_reads @ s2.sp_reads;
130
131
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
132
  }
133

134
(* dead code
135
  let add_init_mark e =
136
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
137
    { e with expr_desc = Emark (init, e) }
138
*)
139

140
141
142
  let small_integer i =
    try
      match i with
143
144
145
146
      | 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)
147
148
    with Failure _ -> raise Parsing.Parse_error

149
150
151
  let qualid_last = function
    | Qident x | Qdot (_, x) -> x.id

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152
153
%}

154
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155

156
%token <string> LIDENT UIDENT
157
%token <Ptree.integer_constant> INTEGER
158
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
159
160
%token <Ptree.real_constant> FLOAT
%token <string> STRING
161
%token <Loc.position> POSITION
162
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
163
164
165

/* keywords */

166
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
167
168
169
%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
170
%token THEN THEORY TRUE TYPE USE WITH
171

172
173
/* program keywords */

174
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO
175
%token ENSURES EXCEPTION FOR
176
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE PRIVATE RAISE
177
%token RAISES READS REC REQUIRES RETURNS TO TRY VAL VARIANT WHILE WRITES
178

179
180
/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
181
%token AND ARROW
182
%token BAR
183
%token COLON COMMA
184
%token DOT EQUAL LAMBDA LTGT
185
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
186
%token LARROW LRARROW OR
187
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
188
%token UNDERSCORE
189
190
191

%token EOF

192
193
/* program symbols */

194
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
195

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196
197
/* Precedences */

198
%nonassoc prec_mark
199
%nonassoc prec_fun
200
201
202
%nonassoc IN
%right SEMICOLON
%nonassoc prec_no_else
203
%nonassoc DOT ELSE GHOST
204
205
%nonassoc prec_no_spec
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES VARIANT
206
%nonassoc prec_named
207
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
208

Andrei Paskevich's avatar
Andrei Paskevich committed
209
%right ARROW LRARROW
210
211
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
212
%nonassoc NOT
213
%left EQUAL LTGT OP1
214
215
%nonassoc LARROW
%nonassoc RIGHTSQ    /* stronger than <- for e1[e2 <- e3] */
216
%left OP2
217
%left OP3
218
%left OP4
219
%nonassoc prec_prefix_op
220
221
%nonassoc LEFTSQ
%nonassoc OPPREF
222

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
223
224
/* Entry points */

225
226
227
%type <Ptree.incremental -> unit> open_file
%start open_file
%type <unit> logic_file
Andrei Paskevich's avatar
Andrei Paskevich committed
228
%start logic_file
229
%type <unit> program_file
230
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
231
232
%%

233
234
open_file:
| /* epsilon */  { Incremental.open_file }
235
236
;

Andrei Paskevich's avatar
Andrei Paskevich committed
237
logic_file:
238
| list0_theory EOF  { Incremental.close_file () }
239
240
241
;

/* File, theory, namespace */
242

243
244
245
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
246
247
;

248
theory_head:
249
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
250
251
;

252
theory:
253
| theory_head list0_decl END  { Incremental.close_theory () }
254
255
;

256
list0_decl:
257
258
| /* epsilon */        { () }
| new_decl list0_decl  { () }
259
| new_ns_th list0_decl { () }
260
261
262
263
;

new_decl:
| decl
264
   { Incremental.new_decl (floc ()) $1 }
265
| use_clone
266
   { Incremental.use_clone (floc ()) $1 }
267
268
269
;

new_ns_th:
270
271
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
272
273
;

274
namespace_head:
275
276
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
277
278
279
280
281
282
283
284
285
;

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

/* Declaration */

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

309
310
311
312
313
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

314
315
/* Use and clone */

316
317
use_clone:
| USE use
318
    { ($2, None) }
319
| CLONE use clone_subst
320
    { ($2, Some $3) }
321
322
;

323
use:
324
325
326
327
328
329
| 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
330
331
;

332
333
334
opt_import:
| /* epsilon */ { false }
| IMPORT        { true  }
335
336
337
338
339
340
341
342
343
344
345
346
347
;

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

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

subst:
348
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
349
350
| TYPE qualid type_args EQUAL primitive_type
                                { CStsym (floc (), $2, $3, $5) }
351
352
353
354
355
| CONSTANT  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| FUNCTION  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }
| LEMMA     qualid              { CSlemma (floc (), $2) }
| GOAL      qualid              { CSgoal  (floc (), $2) }
356
357
;

358
359
360
361
362
ns:
| uqualid { Some $1 }
| DOT     { None }
;

363
364
365
366
367
368
369
370
/* Meta args */

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

meta_arg:
371
372
| TYPE primitive_type { PMAty $2 }
| CONSTANT  qualid { PMAfs  $2 }
373
374
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
375
376
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
377
| INTEGER          { PMAint (small_integer $1) }
378
379
;

380
381
382
/* Type declarations */

list1_type_decl:
383
384
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
385
386
387
;

type_decl:
388
| lident labels type_args typedefn
389
  { let model, vis, def, inv = $4 in
390
    let vis = if model then Abstract else vis in
391
    { td_loc = floc (); td_ident = add_lab $1 $2;
392
393
      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
394
395
;

396
397
398
399
400
401
402
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 } }
;

403
type_args:
404
405
| /* epsilon */                 { [] }
| quote_lident labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
406
407
408
;

typedefn:
409
| /* epsilon */
410
    { false, Public, TDabstract, [] }
411
| equal_model visibility typecases type_invariant
412
    { $1, $2, TDalgebraic $3, $4 }
413
| equal_model visibility BAR typecases type_invariant
414
    { $1, $2, TDalgebraic $4, $5 }
415
| equal_model visibility record_type type_invariant
416
    { $1, $2, TDrecord $3, $4 }
417
418
419
/* 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;
420
      $1, Public, TDalias $3, [] }
421
422
423
424
425
426
;

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
427
428
429
430
431
;

equal_model:
| EQUAL { false }
| MODEL { true }
432
433
434
;

record_type:
435
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
436
437
438
439
;

list1_record_field:
| record_field                              { [$1] }
440
| list1_record_field SEMICOLON record_field { $3 :: $1 }
441
442
;

443
444
445
446
447
448
449
450
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

451
record_field:
452
453
454
455
456
457
| 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
458
459
460
461
462
463
464
465
;

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

typecase:
466
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
467
468
469
470
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
471
472
473
474
475
476
477
478
479
480
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 }
;

481
list1_logic_decl:
482
483
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
484
485
;

486
487
488
489
490
491
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
492
logic_decl_function:
493
| lident_rich labels list0_param COLON primitive_type logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
494
495
496
497
498
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;

logic_decl_predicate:
499
| lident_rich labels list0_param logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
500
501
502
503
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = None; ld_def = $4 } }
;

504
logic_decl:
505
| lident_rich labels list0_param opt_cast logic_def_option
506
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
507
      ld_params = $3; ld_type = $4; ld_def = $5 } }
508
509
510
511
512
;

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

515
516
517
/* Inductive declarations */

list1_inductive_decl:
518
519
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
520
521
522
;

inductive_decl:
523
| lident_rich labels list0_param inddefn
524
  { { in_loc = floc (); in_ident = add_lab $1 $2;
525
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
526
;
527

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
528
529
530
531
532
533
534
535
536
537
538
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

542
543
544
/* Type expressions */

primitive_type:
545
546
547
| primitive_type_arg                  { $1 }
| lqualid primitive_type_args         { PPTtyapp ($1, $2) }
| primitive_type ARROW primitive_type { PPTarrow ($1, $3) }
548
549
550
551
552
553
554
555
;

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

primitive_type_arg:
556
557
| lqualid
   { PPTtyapp ($1, []) }
558
559
560
561
| quote_lident
   { PPTtyvar ($1, false) }
| opaque_quote_lident
   { PPTtyvar ($1, true) }
562
563
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
564
565
566
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
567
   { PPTparen $2 }
568
569
;

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

575
576
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
577
lexpr:
578
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
579
   { infix_pp $1 PPimplies $3 }
580
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
581
   { infix_pp $1 PPiff $3 }
582
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
583
   { infix_pp $1 PPor $3 }
584
| lexpr BARBAR lexpr
585
   { infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPor $3 }
586
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
587
   { infix_pp $1 PPand $3 }
588
| lexpr AMPAMP lexpr
589
   { infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPand $3 }
590
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
591
   { prefix_pp PPnot $2 }
592
| lexpr EQUAL lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
593
   { mk_l_infix $1 "=" $3 }
594
| lexpr LTGT lexpr
595
   { mk_l_infix $1 "<>" $3 }
596
| lexpr OP1 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
597
   { mk_l_infix $1 $2 $3 }
598
| lexpr OP2 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
599
   { mk_l_infix $1 $2 $3 }
600
| lexpr OP3 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
601
   { mk_l_infix $1 $2 $3 }
602
| lexpr OP4 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
603
   { mk_l_infix $1 $2 $3 }
604
| prefix_op lexpr %prec prec_prefix_op
Andrei Paskevich's avatar
Andrei Paskevich committed
605
   { mk_l_prefix $1 $2 }
606
| qualid list1_lexpr_arg
607
   { mk_pp (PPidapp ($1, $2)) }
608
609
| lexpr_arg_noid list1_lexpr_arg
   { List.fold_left mk_l_apply $1 $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
610
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
611
   { mk_pp (PPif ($2, $4, $6)) }
612
| quant list1_quant_vars triggers DOT lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
613
   { mk_pp (PPquant ($1, $2, $3, $5)) }
614
615
| label lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
616
| LET pattern EQUAL lexpr IN lexpr
617
   { match $2.pat_desc with
618
619
620
621
622
     | 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
623
| MATCH lexpr WITH bar_ match_cases END
624
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
625
626
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
   { mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
627
| lexpr COLON primitive_type
628
   { mk_pp (PPcast ($1, $3)) }
629
| lexpr_arg
630
631
632
   { match $1.pp_desc with (* break the infix relation chain *)
     | PPinfix (l,o,r) -> { $1 with pp_desc = PPinnfix (l,o,r) }
     | _ -> $1 }
633
634
;

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

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

644
645
646
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
647
;
648

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

654
lexpr_arg:
655
| qualid            { mk_pp (PPident $1) }
656
657
658
659
| lexpr_arg_noid    { $1 }
;

lexpr_arg_noid:
Andrei Paskevich's avatar
Andrei Paskevich committed
660
661
662
663
664
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
665
| quote_uident      { mk_pp (PPident (Qident $1)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
666
667
668
;

lexpr_dot:
669
| lqualid_copy      { mk_pp (PPident $1) }
Andrei Paskevich's avatar
Andrei Paskevich committed
670
671
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
672
673
674
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
693
694
695
696
697
698
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

699
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
700

701
702
703
704
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
705

706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
list1_trigger_sep_bar:
| trigger                           { [$1] }
| trigger BAR list1_trigger_sep_bar { $1 :: $3 }
;

trigger:
| list1_lexpr_sep_comma { $1 }
;

list1_lexpr_sep_comma:
| lexpr                             { [$1] }
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

/* Match expressions */
721

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

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

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
| 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:
747
748
749
| 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
750
;
751

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

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

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
773
774
;

775
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
776

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

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

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

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
821
822
/* [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
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
853
854
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 }
855
856
;

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

862
863
864
865
866
867
868
869
870
871
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
872
873
;

874
875
876
877
878
879
880
881
882
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
883
884
;

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

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

897
list0_lident_labels:
898
899
900
901
902
903
904
905
906
907
| /* 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) }
908
909
910
| anon_binder   { $1 }

anon_binder:
911
| UNDERSCORE    { floc (), None }
912
913
;

914
915
916
917
918
/* Idents */

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

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

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

lident_keyword:
| MODEL           { "model" }
;

934
935
936
937
938
939
940
941
942
943
944
945
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
946
947
/* Idents + symbolic operations' names */

948
949
950
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
951
952
;

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
981
/* Qualified idents */