MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

parser.mly 36.5 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
    sp_writes  = [];
    sp_variant = [];
123
124
    sp_checkrw = false;
    sp_diverge = false;
125
  }
126

127
128
129
130
  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;
131
    sp_reads   = s1.sp_reads @ s2.sp_reads;
132
133
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
134
135
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
136
  }
137

138
(* dead code
139
  let add_init_mark e =
140
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
141
    { e with expr_desc = Emark (init, e) }
142
*)
143

144
145
146
  let small_integer i =
    try
      match i with
147
148
149
150
      | 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)
151
152
    with Failure _ -> raise Parsing.Parse_error

153
154
155
  let qualid_last = function
    | Qident x | Qdot (_, x) -> x.id

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
156
157
%}

158
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
159

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

/* keywords */

170
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
171
172
173
%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
174
%token THEN THEORY TRUE TYPE USE WITH
175

176
177
/* program keywords */

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

183
184
/* symbols */

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

%token EOF

196
197
/* program symbols */

198
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
199

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
200
201
/* Precedences */

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
227
228
/* Entry points */

229
230
231
%type <Ptree.incremental -> unit> open_file
%start open_file
%type <unit> logic_file
Andrei Paskevich's avatar
Andrei Paskevich committed
232
%start logic_file
233
%type <unit> program_file
234
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
235
236
%%

237
238
open_file:
| /* epsilon */  { Incremental.open_file }
239
240
;

Andrei Paskevich's avatar
Andrei Paskevich committed
241
logic_file:
242
| list0_theory EOF  { Incremental.close_file () }
243
244
245
;

/* File, theory, namespace */
246

247
248
249
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
250
251
;

252
theory_head:
253
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
254
255
;

256
theory:
257
| theory_head list0_decl END  { Incremental.close_theory () }
258
259
;

260
list0_decl:
261
262
| /* epsilon */        { () }
| new_decl list0_decl  { () }
263
| new_ns_th list0_decl { () }
264
265
266
267
;

new_decl:
| decl
268
   { Incremental.new_decl (floc ()) $1 }
269
| use_clone
270
   { Incremental.use_clone (floc ()) $1 }
271
272
273
;

new_ns_th:
274
275
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
276
277
;

278
namespace_head:
279
280
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
281
282
283
284
285
286
287
288
289
;

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

/* Declaration */

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

313
314
315
316
317
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

318
319
/* Use and clone */

320
321
use_clone:
| USE use
322
    { ($2, None) }
323
| CLONE use clone_subst
324
    { ($2, Some $3) }
325
326
;

327
use:
328
329
330
331
332
333
| 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
334
335
;

336
337
338
opt_import:
| /* epsilon */ { false }
| IMPORT        { true  }
339
340
341
342
343
344
345
346
347
348
349
350
351
;

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

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

subst:
352
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
353
354
| TYPE qualid type_args EQUAL primitive_type
                                { CStsym (floc (), $2, $3, $5) }
355
356
357
358
359
| 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) }
360
361
;

362
363
364
365
366
ns:
| uqualid { Some $1 }
| DOT     { None }
;

367
368
369
370
371
372
373
374
/* Meta args */

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

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

384
385
386
/* Type declarations */

list1_type_decl:
387
388
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
389
390
391
;

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

400
401
402
403
404
405
406
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 } }
;

407
type_args:
408
409
| /* epsilon */                 { [] }
| quote_lident labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410
411
412
;

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

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
431
432
433
434
435
;

equal_model:
| EQUAL { false }
| MODEL { true }
436
437
438
;

record_type:
439
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
440
441
442
443
;

list1_record_field:
| record_field                              { [$1] }
444
| list1_record_field SEMICOLON record_field { $3 :: $1 }
445
446
;

447
448
449
450
451
452
453
454
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

455
record_field:
456
457
458
459
460
461
| 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
462
463
464
465
466
467
468
469
;

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

typecase:
470
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
471
472
473
474
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
475
476
477
478
479
480
481
482
483
484
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 }
;

485
list1_logic_decl:
486
487
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
488
489
;

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

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

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

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

519
520
521
/* Inductive declarations */

list1_inductive_decl:
522
523
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
524
525
526
;

inductive_decl:
527
| lident_rich labels list0_param inddefn
528
  { { in_loc = floc (); in_ident = add_lab $1 $2;
529
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
530
;
531

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

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

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

546
547
548
/* Type expressions */

primitive_type:
549
550
551
| primitive_type_arg                  { $1 }
| lqualid primitive_type_args         { PPTtyapp ($1, $2) }
| primitive_type ARROW primitive_type { PPTarrow ($1, $3) }
552
553
554
555
556
557
558
559
;

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
574
575
576
577
578
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

579
580
/* Logic expressions */

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

639
640
641
642
643
644
645
646
647
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

648
649
650
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
651
;
652

653
constant:
654
655
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
656
657
;

658
lexpr_arg:
659
| qualid            { mk_pp (PPident $1) }
660
661
662
663
| lexpr_arg_noid    { $1 }
;

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

lexpr_dot:
673
| lqualid_copy      { mk_pp (PPident $1) }
Andrei Paskevich's avatar
Andrei Paskevich committed
674
675
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
676
677
678
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
697
698
699
700
701
702
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

703
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
704

705
706
707
708
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
709

710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
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 */
725

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
726
727
728
729
730
731
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
732
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
733
734
735
;

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

756
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
757
758
759
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
760

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

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
777
778
;

779
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
780

781
782
783
list0_param:
| /* epsilon */ { [] }
| list1_param   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
784
785
;

786
list1_param:
787
788
| param               { $1 }
| param list1_param   { $1 @ $2 }
789
790
791
792
793
794
795
;

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

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
823
824
825
826
/* [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
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
855
856
857
858
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 }
859
860
;

861
862
863
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
864
865
;

866
867
868
869
870
871
872
873
874
875
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
876
877
;

878
879
880
881
882
883
884
885
886
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
887
888
;

889
890
891
892
893
894
list1_quant_vars:
| quant_vars                        { $1 }
| quant_vars COMMA list1_quant_vars { $1 @ $3 }
;

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

901
list0_lident_labels:
902
903
904
905
906
907
908
909
910
911
| /* 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) }
912
913
914
| anon_binder   { $1 }

anon_binder:
915
| UNDERSCORE    { floc (), None }
916
917
;

918
919
920
921
922
/* Idents */

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

Andrei Paskevich's avatar
Andrei Paskevich committed
925
926
927
928
929
930
931
932
933
934
935
936
937
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

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

lident_keyword:
| MODEL           { "model" }
;

938
939
940
941
942
943
944
945
946
947
948
949
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
950
951
/* Idents + symbolic operations' names */

952
953
954
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
955
956
;

957
lident_rich:
Andrei Paskevich's avatar
Andrei Paskevich committed
958
959
960
961
962
| lident        { $1 }
| lident_op_id  { $1 }
;

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

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