Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

parser.mly 35.6 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
146
147
148
  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   = [];
    sp_writes  = [];
    sp_variant = [];
  }
149

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

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
176
177
%}

178
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
179

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

/* keywords */

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

196
197
/* program keywords */

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

203
204
/* symbols */

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

%token EOF

216
217
/* program symbols */

218
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
219

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
220
221
/* Precedences */

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
247
248
/* Entry points */

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

257
258
open_file:
| /* epsilon */  { Incremental.open_file }
259
260
;

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

/* File, theory, namespace */
266

267
268
269
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
270
271
;

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

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

280
list0_decl:
281
282
283
284
285
286
| /* epsilon */        { () }
| new_decl list0_decl  { () }
;

new_decl:
| decl
287
   { Incremental.new_decl (floc ()) $1 }
288
| use_clone
289
   { Incremental.use_clone (floc ()) $1 }
290
291
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
292
293
;

294
namespace_head:
295
296
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
297
298
299
300
301
302
303
304
305
;

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

/* Declaration */

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

329
330
331
332
333
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

334
335
/* Use and clone */

336
337
use_clone:
| USE use
338
    { ($2, None) }
339
| CLONE use clone_subst
340
    { ($2, Some $3) }
341
342
;

343
use:
344
345
346
347
348
349
| 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
350
351
;

352
353
354
opt_import:
| /* epsilon */ { false }
| IMPORT        { true  }
355
356
357
358
359
360
361
362
363
364
365
366
367
;

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

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

subst:
368
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
369
370
| TYPE qualid type_args EQUAL primitive_type
                                { CStsym (floc (), $2, $3, $5) }
371
372
373
374
375
| 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) }
376
377
;

378
379
380
381
382
ns:
| uqualid { Some $1 }
| DOT     { None }
;

383
384
385
386
387
388
389
390
/* Meta args */

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

meta_arg:
391
392
| TYPE primitive_type { PMAty $2 }
| CONSTANT  qualid { PMAfs  $2 }
393
394
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
395
396
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
397
| INTEGER          { PMAint (small_integer $1) }
398
399
;

400
401
402
/* Type declarations */

list1_type_decl:
403
404
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
405
406
407
;

type_decl:
408
| lident labels type_args typedefn
409
  { let model, vis, def, inv = $4 in
410
    let vis = if model then Abstract else vis in
411
    { td_loc = floc (); td_ident = add_lab $1 $2;
412
413
      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
414
415
;

416
417
418
419
420
421
422
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 } }
;

423
type_args:
424
425
| /* epsilon */                 { [] }
| quote_lident labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
426
427
428
;

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

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
447
448
449
450
451
;

equal_model:
| EQUAL { false }
| MODEL { true }
452
453
454
;

record_type:
455
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
456
457
458
459
;

list1_record_field:
| record_field                              { [$1] }
460
| list1_record_field SEMICOLON record_field { $3 :: $1 }
461
462
;

463
464
465
466
467
468
469
470
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

471
record_field:
472
473
474
475
476
477
| 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
478
479
480
481
482
483
484
485
;

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

typecase:
486
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
487
488
489
490
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
491
492
493
494
495
496
497
498
499
500
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 }
;

501
list1_logic_decl:
502
503
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
504
505
;

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

logic_decl_predicate:
519
| lident_rich labels list0_param logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
520
521
522
523
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = None; ld_def = $4 } }
;

524
logic_decl:
525
| lident_rich labels list0_param opt_cast logic_def_option
526
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
527
      ld_params = $3; ld_type = $4; ld_def = $5 } }
528
529
530
531
532
;

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

535
536
537
/* Inductive declarations */

list1_inductive_decl:
538
539
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
540
541
542
;

inductive_decl:
543
| lident_rich labels list0_param inddefn
544
  { { in_loc = floc (); in_ident = add_lab $1 $2;
545
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
546
;
547

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
548
549
550
551
552
553
554
555
556
557
558
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

562
563
564
565
/* Type expressions */

primitive_type:
| primitive_type_arg           { $1 }
566
| lqualid primitive_type_args  { PPTtyapp ($1, $2) }
567
568
569
;

primitive_type_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
570
| primitive_type_arg_non_lident           { $1 }
571
| uqualid DOT lident primitive_type_args  { PPTtyapp (Qdot ($1, $3), $4) }
572
573
574
575
576
577
578
;

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

579
580
581
582
583
primitive_type_args_non_lident:
| primitive_type_arg_non_lident                      { [$1] }
| primitive_type_arg_non_lident primitive_type_args  { $1 :: $2 }
;

584
primitive_type_arg:
585
| lident                         { PPTtyapp (Qident $1, []) }
586
587
588
589
| primitive_type_arg_non_lident  { $1 }
;

primitive_type_arg_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
590
| uqualid DOT lident
591
   { PPTtyapp (Qdot ($1, $3), []) }
592
593
594
595
| quote_lident
   { PPTtyvar ($1, false) }
| opaque_quote_lident
   { PPTtyvar ($1, true) }
596
597
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
598
599
600
601
602
603
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
604
605
606
607
608
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

609
610
/* Logic expressions */

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

671
672
673
674
675
676
677
678
679
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

680
681
682
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
683
;
684

685
constant:
686
687
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
688
689
;

690
lexpr_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
691
692
693
694
695
696
| 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 }
697
| quote_uident      { mk_pp (PPvar (Qident $1)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
698
699
700
;

lexpr_dot:
Andrei Paskevich's avatar
Andrei Paskevich committed
701
702
703
| lqualid_copy      { mk_pp (PPvar $1) }
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
704
705
706
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
725
726
727
728
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
729
730
| FUNC    { PPfunc }
| PRED    { PPpred }
Andrei Paskevich's avatar
Andrei Paskevich committed
731
732
;

733
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
734

735
736
737
738
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
739

740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
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 */
755

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
756
757
758
759
760
761
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
762
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
763
764
765
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
| 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:
781
782
783
| 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
784
;
785

786
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
787
788
789
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
790

791
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
792
| UNDERSCORE                { mk_pat (PPpwild) }
793
| lident labels             { mk_pat (PPpvar (add_lab $1 $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
794
795
796
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
797
| LEFTBRC pfields RIGHTBRC  { mk_pat (PPprec $2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
798
799
800
801
802
803
804
805
806
;

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
807
808
;

809
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
810

811
812
813
list0_param:
| /* epsilon */ { [] }
| list1_param   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
814
815
;

816
817
818
819
820
821
822
823
824
825
list1_param:
| list1_binder  { params_of_binders $1 }
;

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

binder:
826
827
828
829
| quote_lident
   { [floc (), None, false, Some (PPTtyvar ($1, false))] }
| opaque_quote_lident
   { [floc (), None, false, Some (PPTtyvar ($1, true))] }
830
831
832
833
834
835
836
837
838
839
840
841
842
843
| 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
844
845
;

846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
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) }
867
868
| primitive_type_non_lident
   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
869
870
;

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

887
888
889
list0_lident:
| /* epsilon */ { [] }
| list1_lident  { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
890
891
;

892
893
list1_lident:
| lident list0_lident  { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
894
895
;

896
897
898
899
900
901
902
903
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 }
904
905
;

906
list0_lident_labels:
907
908
909
910
911
912
913
914
915
916
917
| /* 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 }
918
919
;

920
921
922
923
924
/* Idents */

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

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

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

lident_keyword:
| MODEL           { "model" }
;

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

954
955
956
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
957
958
;

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

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

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

980
prefix_op:
981
982
983
984
985
986
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
987
/* Qualified idents */
988

Andrei Paskevich's avatar
Andrei Paskevich committed
989
990
991
qualid:
| ident_rich              { Qident $1 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }
992
993
;

Andrei Paskevich's avatar
Andrei Paskevich committed
994
995
996
lqualid_rich:
| lident_rich             { Qident $1 }
| uqualid DOT lident_rich { Qdot ($1, $3) }
997
998
999
;

lqualid:
Andrei Paskevich's avatar
Andrei Paskevich committed
1000
1001
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
1002
1003
;

Andrei Paskevich's avatar
Andrei Paskevich committed
1004
1005
1006
1007
/* copy of lqualid to avoid yacc conflicts */
lqualid_copy:
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
1008
1009
;