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 35.9 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
(* dead code
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
36
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
37
  let floc_ij i j = Loc.extract (loc_ij i j)
38
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
39

40
41
42
43
44
45
46
47
48
49
50
  let pty_of_id i = PPTtyapp (Qident i, [])

  let params_of_binders bl = List.map (function
    | l, None, _, None -> Loc.errorm ~loc:l "cannot determine the type"
    | l, Some i, gh, None -> l, None, gh, pty_of_id i
    | l, i, gh, Some t -> l, i, gh, t) bl

  let quvars_of_lidents ty ll = List.map (function
    | l, None -> Loc.errorm ~loc:l "anonymous binders are not allowed here"
    | _, Some i -> i, ty) ll

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
51
  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
52
  let mk_pp d = mk_ppl (floc ()) d
53
(* dead code
54
  let mk_pp_i i d = mk_ppl (floc_i i) d
55
*)
56
  let mk_pat p = { pat_loc = floc (); pat_desc = p }
Andrei Paskevich's avatar
Andrei Paskevich committed
57

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

61
  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
62
  let prefix_pp p a = prefix_ppl (floc ()) p a
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
63

64
  let infix  s = "infix "  ^ s
65
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
66
  let mixfix s = "mixfix " ^ s
67

68
69
70
71
  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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
  let mk_l_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
    mk_pp (PPapp (Qident id, [e1]))

  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
    mk_pp (PPapp (Qident id, [e1;e2]))

  let mk_l_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
    mk_pp (PPapp (Qident id, [e1;e2;e3]))

88
89
90
  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
91
      | _ -> raise exn)
92

93
94
  let mk_expr d = { expr_loc = floc (); expr_desc = d }
  let mk_expr_i i d = { expr_loc = floc_i i; expr_desc = d }
95

96
97
98
  let cast_body c e = match c with
    | Some pt -> { e with expr_desc = Ecast (e, pt) }
    | None -> e
99
100
101

  let rec mk_apply f = function
    | [] ->
102
        assert false
103
    | [a] ->
104
        Eapply (f, a)
105
    | a :: l ->
106
107
        let loc = Loc.join f.expr_loc a.expr_loc in
        mk_apply { expr_loc = loc; expr_desc = Eapply (f, a) } l
108
109

  let mk_apply_id id =
110
    mk_apply { expr_desc = Eident (Qident id); expr_loc = id.id_loc }
111

Andrei Paskevich's avatar
Andrei Paskevich committed
112
113
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
114
115
    mk_expr (mk_apply_id id [e1; e2])

Andrei Paskevich's avatar
Andrei Paskevich committed
116
117
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
118
119
    mk_expr (mk_apply_id id [e1; e2; e3])

120
  let mk_infix e1 op e2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
121
    let id = mk_id (infix op) (floc_i 2) in
122
    mk_expr (Einfix (e1, id, e2))
123
124

  let mk_prefix op e1 =
Andrei Paskevich's avatar
Andrei Paskevich committed
125
    let id = mk_id (prefix op) (floc_i 1) in
126
127
    mk_expr (mk_apply_id id [e1])

Andrei Paskevich's avatar
Andrei Paskevich committed
128
129
  let exit_exn () = Qident (mk_id "%Exit" (floc ()))
  let id_anonymous () = mk_id "_" (floc ())
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
130
  let ty_unit () = PPTtuple []
131

132
(* dead code
Andrei Paskevich's avatar
Andrei Paskevich committed
133
  let id_lt_nat () = Qident (mk_id "lt_nat" (floc ()))
134
*)
135

136
137
138
139
140
141
142
143
144
145
  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   = [];
146
    sp_reads   = [];
147
148
149
    sp_writes  = [];
    sp_variant = [];
  }
150

151
152
153
154
  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;
155
    sp_reads   = s1.sp_reads @ s2.sp_reads;
156
157
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
158
  }
159

160
(* dead code
161
  let add_init_mark e =
162
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
163
    { e with expr_desc = Emark (init, e) }
164
*)
165

166
167
168
  let small_integer i =
    try
      match i with
169
170
171
172
      | 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)
173
174
    with Failure _ -> raise Parsing.Parse_error

175
176
177
  let qualid_last = function
    | Qident x | Qdot (_, x) -> x.id

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
178
179
%}

180
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181

182
%token <string> LIDENT UIDENT
183
%token <Ptree.integer_constant> INTEGER
184
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
185
186
%token <Ptree.real_constant> FLOAT
%token <string> STRING
187
%token <Loc.position> POSITION
188
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
189
190
191

/* keywords */

192
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
193
194
195
%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
196
%token THEN THEORY TRUE TYPE USE WITH
197

198
199
/* program keywords */

200
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO
201
%token ENSURES EXCEPTION FOR
202
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE PRIVATE RAISE
203
%token RAISES READS REC REQUIRES RETURNS TO TRY VAL VARIANT WHILE WRITES
204

205
206
/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
207
%token AND ARROW
208
%token BAR
209
%token COLON COMMA
210
%token DOT EQUAL FUNC LAMBDA LTGT
211
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
212
%token LARROW LRARROW OR PRED
213
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
214
%token UNDERSCORE
215
216
217

%token EOF

218
219
/* program symbols */

220
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
221

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
222
223
/* Precedences */

224
%nonassoc prec_mark
225
%nonassoc prec_fun
226
227
228
%nonassoc IN
%right SEMICOLON
%nonassoc prec_no_else
229
%nonassoc DOT ELSE GHOST
230
231
%nonassoc prec_no_spec
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES VARIANT
232
%nonassoc prec_named
233
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
234

Andrei Paskevich's avatar
Andrei Paskevich committed
235
%right ARROW LRARROW
236
237
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
238
%nonassoc NOT
239
%left EQUAL LTGT OP1
240
241
%nonassoc LARROW
%nonassoc RIGHTSQ    /* stronger than <- for e1[e2 <- e3] */
242
%left OP2
243
%left OP3
244
%left OP4
245
%nonassoc prec_prefix_op
246
247
%nonassoc LEFTSQ
%nonassoc OPPREF
248

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
249
250
/* Entry points */

251
252
253
%type <Ptree.incremental -> unit> open_file
%start open_file
%type <unit> logic_file
Andrei Paskevich's avatar
Andrei Paskevich committed
254
%start logic_file
255
%type <unit> program_file
256
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
257
258
%%

259
260
open_file:
| /* epsilon */  { Incremental.open_file }
261
262
;

Andrei Paskevich's avatar
Andrei Paskevich committed
263
logic_file:
264
| list0_theory EOF  { Incremental.close_file () }
265
266
267
;

/* File, theory, namespace */
268

269
270
271
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
272
273
;

274
theory_head:
275
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
276
277
;

278
theory:
279
| theory_head list0_decl END  { Incremental.close_theory () }
280
281
;

282
list0_decl:
283
284
| /* epsilon */        { () }
| new_decl list0_decl  { () }
285
| new_ns_th list0_decl { () }
286
287
288
289
;

new_decl:
| decl
290
   { Incremental.new_decl (floc ()) $1 }
291
| use_clone
292
   { Incremental.use_clone (floc ()) $1 }
293
294
295
;

new_ns_th:
296
297
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
298
299
;

300
namespace_head:
301
302
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
303
304
305
306
307
308
309
310
311
;

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

/* Declaration */

312
decl:
313
314
| TYPE list1_type_decl
    { TypeDecl $2 }
315
316
| TYPE late_invariant
    { TypeDecl [$2] }
317
318
| CONSTANT logic_decl_constant
    { LogicDecl [$2] }
Andrei Paskevich's avatar
Andrei Paskevich committed
319
320
321
| FUNCTION list1_logic_decl_function
    { LogicDecl $2 }
| PREDICATE list1_logic_decl_predicate
322
    { LogicDecl $2 }
323
324
| inductive list1_inductive_decl
    { IndDecl ($1, $2) }
325
| AXIOM ident labels COLON lexpr
326
    { PropDecl (Kaxiom, add_lab $2 $3, $5) }
327
| LEMMA ident labels COLON lexpr
328
    { PropDecl (Klemma, add_lab $2 $3, $5) }
329
| GOAL ident labels COLON lexpr
330
    { PropDecl (Kgoal, add_lab $2 $3, $5) }
331
| META sident list1_meta_arg_sep_comma
332
    { Meta ($2, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
333
334
;

335
336
337
338
339
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

340
341
/* Use and clone */

342
343
use_clone:
| USE use
344
    { ($2, None) }
345
| CLONE use clone_subst
346
    { ($2, Some $3) }
347
348
;

349
use:
350
351
352
353
354
355
| 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
356
357
;

358
359
360
opt_import:
| /* epsilon */ { false }
| IMPORT        { true  }
361
362
363
364
365
366
367
368
369
370
371
372
373
;

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

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

subst:
374
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
375
376
| TYPE qualid type_args EQUAL primitive_type
                                { CStsym (floc (), $2, $3, $5) }
377
378
379
380
381
| 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) }
382
383
;

384
385
386
387
388
ns:
| uqualid { Some $1 }
| DOT     { None }
;

389
390
391
392
393
394
395
396
/* Meta args */

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

meta_arg:
397
398
| TYPE primitive_type { PMAty $2 }
| CONSTANT  qualid { PMAfs  $2 }
399
400
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
401
402
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
403
| INTEGER          { PMAint (small_integer $1) }
404
405
;

406
407
408
/* Type declarations */

list1_type_decl:
409
410
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
411
412
413
;

type_decl:
414
| lident labels type_args typedefn
415
  { let model, vis, def, inv = $4 in
416
    let vis = if model then Abstract else vis in
417
    { td_loc = floc (); td_ident = add_lab $1 $2;
418
419
      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
420
421
;

422
423
424
425
426
427
428
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 } }
;

429
type_args:
430
431
| /* epsilon */                 { [] }
| quote_lident labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
432
433
434
;

typedefn:
435
| /* epsilon */
436
    { false, Public, TDabstract, [] }
437
| equal_model visibility typecases type_invariant
438
    { $1, $2, TDalgebraic $3, $4 }
439
| equal_model visibility BAR typecases type_invariant
440
    { $1, $2, TDalgebraic $4, $5 }
441
| equal_model visibility record_type type_invariant
442
    { $1, $2, TDrecord $3, $4 }
443
444
445
/* 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;
446
      $1, Public, TDalias $3, [] }
447
448
449
450
451
452
;

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
453
454
455
456
457
;

equal_model:
| EQUAL { false }
| MODEL { true }
458
459
460
;

record_type:
461
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
462
463
464
465
;

list1_record_field:
| record_field                              { [$1] }
466
| list1_record_field SEMICOLON record_field { $3 :: $1 }
467
468
;

469
470
471
472
473
474
475
476
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

477
record_field:
478
479
480
481
482
483
| 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
484
485
486
487
488
489
490
491
;

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

typecase:
492
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
493
494
495
496
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
497
498
499
500
501
502
503
504
505
506
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 }
;

507
list1_logic_decl:
508
509
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
510
511
;

512
513
514
515
516
517
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
518
logic_decl_function:
519
| lident_rich labels list0_param COLON primitive_type logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
520
521
522
523
524
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;

logic_decl_predicate:
525
| lident_rich labels list0_param logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
526
527
528
529
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = None; ld_def = $4 } }
;

530
logic_decl:
531
| lident_rich labels list0_param opt_cast logic_def_option
532
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
533
      ld_params = $3; ld_type = $4; ld_def = $5 } }
534
535
536
537
538
;

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

541
542
543
/* Inductive declarations */

list1_inductive_decl:
544
545
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
546
547
548
;

inductive_decl:
549
| lident_rich labels list0_param inddefn
550
  { { in_loc = floc (); in_ident = add_lab $1 $2;
551
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
552
;
553

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
554
555
556
557
558
559
560
561
562
563
564
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

568
569
570
571
/* Type expressions */

primitive_type:
| primitive_type_arg           { $1 }
572
| lqualid primitive_type_args  { PPTtyapp ($1, $2) }
573
574
575
;

primitive_type_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
576
| primitive_type_arg_non_lident           { $1 }
577
| uqualid DOT lident primitive_type_args  { PPTtyapp (Qdot ($1, $3), $4) }
578
579
580
581
582
583
584
;

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

585
586
587
588
589
primitive_type_args_non_lident:
| primitive_type_arg_non_lident                      { [$1] }
| primitive_type_arg_non_lident primitive_type_args  { $1 :: $2 }
;

590
primitive_type_arg:
591
| lident                         { PPTtyapp (Qident $1, []) }
592
593
594
595
| primitive_type_arg_non_lident  { $1 }
;

primitive_type_arg_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
596
| uqualid DOT lident
597
   { PPTtyapp (Qdot ($1, $3), []) }
598
599
600
601
| quote_lident
   { PPTtyvar ($1, false) }
| opaque_quote_lident
   { PPTtyvar ($1, true) }
602
603
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
604
605
606
607
608
609
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
610
611
612
613
614
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

615
616
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
617
lexpr:
618
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
619
   { infix_pp $1 PPimplies $3 }
620
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
621
   { infix_pp $1 PPiff $3 }
622
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
623
   { infix_pp $1 PPor $3 }
624
| lexpr BARBAR lexpr
625
   { infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPor $3 }
626
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
627
   { infix_pp $1 PPand $3 }
628
| lexpr AMPAMP lexpr
629
   { infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPand $3 }
630
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
631
   { prefix_pp PPnot $2 }
632
| lexpr EQUAL lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
633
   { mk_l_infix $1 "=" $3 }
634
| lexpr LTGT lexpr
635
   { mk_l_infix $1 "<>" $3 }
636
| lexpr OP1 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
637
   { mk_l_infix $1 $2 $3 }
638
| lexpr OP2 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
639
   { mk_l_infix $1 $2 $3 }
640
| lexpr OP3 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
641
   { mk_l_infix $1 $2 $3 }
642
| lexpr OP4 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
643
   { mk_l_infix $1 $2 $3 }
644
| prefix_op lexpr %prec prec_prefix_op
Andrei Paskevich's avatar
Andrei Paskevich committed
645
   { mk_l_prefix $1 $2 }
646
647
| qualid list1_lexpr_arg
   { mk_pp (PPapp ($1, $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
648
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
649
   { mk_pp (PPif ($2, $4, $6)) }
650
| quant list1_quant_vars triggers DOT lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
651
   { mk_pp (PPquant ($1, $2, $3, $5)) }
652
653
| label lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
654
| LET pattern EQUAL lexpr IN lexpr
655
   { match $2.pat_desc with
656
657
658
659
660
     | 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
661
| MATCH lexpr WITH bar_ match_cases END
662
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
663
664
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
   { mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
665
/*
666
| EPSILON lident labels COLON primitive_type DOT lexpr
667
   { mk_pp (PPeps ((add_lab $2 $3, Some $5), $7)) }
668
*/
669
| lexpr COLON primitive_type
670
   { mk_pp (PPcast ($1, $3)) }
671
| lexpr_arg
672
673
674
   { match $1.pp_desc with (* break the infix relation chain *)
     | PPinfix (l,o,r) -> { $1 with pp_desc = PPinnfix (l,o,r) }
     | _ -> $1 }
675
676
;

677
678
679
680
681
682
683
684
685
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

686
687
688
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
689
;
690

691
constant:
692
693
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
694
695
;

696
lexpr_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
697
698
699
700
701
702
| qualid            { mk_pp (PPvar $1) }
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
703
| quote_uident      { mk_pp (PPvar (Qident $1)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
704
705
706
;

lexpr_dot:
Andrei Paskevich's avatar
Andrei Paskevich committed
707
708
709
| lqualid_copy      { mk_pp (PPvar $1) }
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
710
711
712
;

lexpr_sub:
713
| lexpr_dot DOT lqualid_rich
Andrei Paskevich's avatar
Andrei Paskevich committed
714
   { mk_pp (PPapp ($3, [$1])) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
715
716
| LEFTPAR lexpr RIGHTPAR
   { $2 }
717
718
719
720
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
721
| LEFTBRC list1_field_value opt_semicolon RIGHTBRC
722
   { mk_pp (PPrecord (List.rev $2)) }
723
| LEFTBRC lexpr_arg WITH list1_field_value opt_semicolon RIGHTBRC
Andrei Paskevich's avatar
Andrei Paskevich committed
724
   { mk_pp (PPupdate ($2, List.rev $4)) }
725
| lexpr_arg LEFTSQ lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
726
   { mk_l_mixfix2 "[]" $1 $3 }
727
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
728
   { mk_l_mixfix3 "[<-]" $1 $3 $5 }
Andrei Paskevich's avatar
Andrei Paskevich committed
729
;
730

Andrei Paskevich's avatar
Andrei Paskevich committed
731
732
733
734
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
735
736
| FUNC    { PPfunc }
| PRED    { PPpred }
Andrei Paskevich's avatar
Andrei Paskevich committed
737
738
;

739
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
740

741
742
743
744
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
745

746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
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 */
761

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
762
763
764
765
766
767
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
768
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
769
770
771
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
| 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:
787
788
789
| 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
790
;
791

792
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
793
794
795
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
796

797
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
798
| UNDERSCORE                { mk_pat (PPpwild) }
799
| lident labels             { mk_pat (PPpvar (add_lab $1 $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
800
801
802
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
803
| LEFTBRC pfields RIGHTBRC  { mk_pat (PPprec $2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
804
805
806
807
808
809
810
811
812
;

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
813
814
;

815
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
816

817
818
819
list0_param:
| /* epsilon */ { [] }
| list1_param   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
820
821
;

822
823
824
825
826
827
828
829
830
831
list1_param:
| list1_binder  { params_of_binders $1 }
;

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

binder:
832
833
834
835
| quote_lident
   { [floc (), None, false, Some (PPTtyvar ($1, false))] }
| opaque_quote_lident
   { [floc (), None, false, Some (PPTtyvar ($1, true))] }
836
837
838
839
840
841
842
843
844
845
846
847
848
849
| lqualid_qualified
   { [floc (), None, false, Some (PPTtyapp ($1, []))] }
| lident labels
   { [floc (), Some (add_lab $1 $2), false, None] }
| UNDERSCORE
   { Loc.errorm ~loc:(floc ()) "untyped anonymous parameters are not allowed" }
| LEFTPAR RIGHTPAR
   { [floc (), None, false, Some (PPTtuple [])] }
| LEFTPAR binder_in RIGHTPAR
   { $2 }
| LEFTPAR GHOST binder_in RIGHTPAR
   { List.map (fun (l,i,_,t) -> (l,i,true,t)) $3 }
| LEFTPAR binder_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { [floc (), None, false, Some (PPTtuple ($2::$4))] }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
850
851
;

852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
binder_in:
| lident labels
   { [floc (), Some (add_lab $1 $2), false, None] }
| UNDERSCORE
   { Loc.errorm ~loc:(floc ()) "untyped anonymous parameters are not allowed" }
| binder_type_rest
   { [floc (), None, false, Some $1] }
| binder_vars COLON primitive_type
   { List.map (fun (l,v) -> l, v, false, Some $3) $1 }
;

binder_type:
| lident            { PPTtyapp (Qident $1, []) }
| binder_type_rest  { $1 }
;

binder_type_rest:
| lident list1_lident
   { PPTtyapp (Qident $1, List.map pty_of_id $2) }
| lident list0_lident primitive_type_args_non_lident
   { PPTtyapp (Qident $1, List.map pty_of_id $2 @ $3) }
873
874
| primitive_type_non_lident
   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
875
876
;

877
878
879
880
881
882
883
884
885
886
887
888
889
890
binder_vars:
| list1_lident
   { List.map (fun id -> id.id_loc, Some id) $1 }
| list1_lident UNDERSCORE list0_lident_labels
   { List.map (fun id -> id.id_loc, Some id) $1 @ (floc_i 2, None) :: $3 }
| lident list1_lident label labels list0_lident_labels
   { let l = match List.rev ($1 :: $2) with
       | i :: l -> add_lab i ($3 :: $4) :: l
       | [] -> assert false in
     List.fold_left (fun acc id -> (id.id_loc, Some id) :: acc) $5 l }
| lident label labels list0_lident_labels
   { ($1.id_loc, Some (add_lab $1 ($2 :: $3))) :: $4 }
| UNDERSCORE list0_lident_labels
   { (floc_i 1, None) :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
891
892
;

893
894
895
list0_lident:
| /* epsilon */ { [] }
| list1_lident  { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
896
897
;

898
899
list1_lident:
| lident list0_lident  { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
900
901
;

902
903
904
905
906
907
908
909
list1_quant_vars:
| quant_vars                        { $1 }
| quant_vars COMMA list1_quant_vars { $1 @ $3 }
;

quant_vars:
| list1_lident_labels COLON primitive_type
   { quvars_of_lidents (Some $3) $1 }
910
911
;

912
list0_lident_labels:
913
914
915
916
917
918
919
920
921
922
923
| /* 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) }
| UNDERSCORE    { floc (), None }
924
925
;

926
927
928
929
930
/* Idents */

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

Andrei Paskevich's avatar
Andrei Paskevich committed
933
934
935
936
937
938
939
940
941
942
943
944
945
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

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

lident_keyword:
| MODEL           { "model" }
;

946
947
948
949
950
951
952
953
954
955
956
957
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
958
959
/* Idents + symbolic operations' names */

960
961
962
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
963
964
;

965
lident_rich:
Andrei Paskevich's avatar
Andrei Paskevich committed
966
967
968
969
970
| lident        { $1 }
| lident_op_id  { $1 }
;

lident_op_id:
971
| LEFTPAR lident_op RIGHTPAR  { mk_id $2 (floc_i 2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
972
| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") (floc ()) }