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 37 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

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
41
  let mk_pp d = mk_ppl (floc ()) d
42
(* dead code
43
  let mk_pp_i i d = mk_ppl (floc_i i) d
44
*)
45
  let mk_pat p = { pat_loc = floc (); pat_desc = p }
Andrei Paskevich's avatar
Andrei Paskevich committed
46

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

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

53
  let infix  s = "infix "  ^ s
54
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
55
  let mixfix s = "mixfix " ^ s
56

57
58
59
60
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

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

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

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

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

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

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

86
87
  let mk_expr d = { expr_loc = floc (); expr_desc = d }
  let mk_expr_i i d = { expr_loc = floc_i i; expr_desc = d }
88

89
90
91
  let cast_body c e = match c with
    | Some pt -> { e with expr_desc = Ecast (e, pt) }
    | None -> e
92
93
94

  let rec mk_apply f = function
    | [] ->
95
        assert false
96
    | [a] ->
97
        Eapply (f, a)
98
    | a :: l ->
99
100
        let loc = Loc.join f.expr_loc a.expr_loc in
        mk_apply { expr_loc = loc; expr_desc = Eapply (f, a) } l
101
102

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

Andrei Paskevich's avatar
Andrei Paskevich committed
105
106
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
107
108
    mk_expr (mk_apply_id id [e1; e2])

Andrei Paskevich's avatar
Andrei Paskevich committed
109
110
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
111
112
    mk_expr (mk_apply_id id [e1; e2; e3])

113
  let mk_infix e1 op e2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
114
    let id = mk_id (infix op) (floc_i 2) in
115
    mk_expr (Einfix (e1, id, e2))
116
117

  let mk_prefix op e1 =
Andrei Paskevich's avatar
Andrei Paskevich committed
118
    let id = mk_id (prefix op) (floc_i 1) in
119
120
    mk_expr (mk_apply_id id [e1])

Andrei Paskevich's avatar
Andrei Paskevich committed
121
122
  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
123
  let ty_unit () = PPTtuple []
124

125
(* dead code
Andrei Paskevich's avatar
Andrei Paskevich committed
126
  let id_lt_nat () = Qident (mk_id "lt_nat" (floc ()))
127
*)
128

129
130
131
132
133
134
135
136
137
138
  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   = [];
139
    sp_reads   = [];
140
141
142
    sp_writes  = [];
    sp_variant = [];
  }
143

144
145
146
147
  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;
148
    sp_reads   = s1.sp_reads @ s2.sp_reads;
149
150
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
151
  }
152

153
(* dead code
154
  let add_init_mark e =
155
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
156
    { e with expr_desc = Emark (init, e) }
157
*)
158

159
160
161
  let small_integer i =
    try
      match i with
162
163
164
165
      | 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)
166
167
    with Failure _ -> raise Parsing.Parse_error

168
169
170
  let qualid_last = function
    | Qident x | Qdot (_, x) -> x.id

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
171
172
%}

173
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174

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

/* keywords */

185
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
186
187
188
%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
189
%token THEN THEORY TRUE TYPE USE WITH
190

191
192
/* program keywords */

193
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO
194
%token ENSURES EXCEPTION FOR
195
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE PRIVATE RAISE
196
%token RAISES READS REC REQUIRES RETURNS TO TRY VAL VARIANT WHILE WRITES
197

198
199
/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
200
%token AND ARROW
201
%token BAR
202
%token COLON COMMA
203
%token DOT EQUAL LAMBDA LTGT
204
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
205
%token LARROW LRARROW OR
206
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
207
%token UNDERSCORE
208
209
210

%token EOF

211
212
/* program symbols */

213
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
214

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
215
216
/* Precedences */

217
%nonassoc prec_mark
218
%nonassoc prec_fun
219
220
221
%nonassoc IN
%right SEMICOLON
%nonassoc prec_no_else
222
%nonassoc DOT ELSE GHOST
223
224
%nonassoc prec_no_spec
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES VARIANT
225
%nonassoc prec_named
226
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
227

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
242
243
/* Entry points */

244
245
246
%type <Ptree.incremental -> unit> open_file
%start open_file
%type <unit> logic_file
Andrei Paskevich's avatar
Andrei Paskevich committed
247
%start logic_file
248
%type <unit> program_file
249
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
250
251
%%

252
253
open_file:
| /* epsilon */  { Incremental.open_file }
254
255
;

Andrei Paskevich's avatar
Andrei Paskevich committed
256
logic_file:
257
| list0_theory EOF  { Incremental.close_file () }
258
259
260
;

/* File, theory, namespace */
261

262
263
264
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
265
266
;

267
theory_head:
268
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
269
270
;

271
theory:
272
| theory_head list0_decl END  { Incremental.close_theory () }
273
274
;

275
list0_decl:
276
277
| /* epsilon */        { () }
| new_decl list0_decl  { () }
278
| new_ns_th list0_decl { () }
279
280
281
282
;

new_decl:
| decl
283
   { Incremental.new_decl (floc ()) $1 }
284
| use_clone
285
   { Incremental.use_clone (floc ()) $1 }
286
287
288
;

new_ns_th:
289
290
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
291
292
;

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

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

/* Declaration */

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

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

333
334
/* Use and clone */

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

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

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

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

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

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

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

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

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

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

399
400
401
/* Type declarations */

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

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

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

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

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

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

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

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

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

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

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

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

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

/* Logic declarations */

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

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

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

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

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

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

534
535
536
/* Inductive declarations */

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

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

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

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

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

561
562
563
/* Type expressions */

primitive_type:
564
565
566
| primitive_type_arg                  { $1 }
| lqualid primitive_type_args         { PPTtyapp ($1, $2) }
| primitive_type ARROW primitive_type { PPTarrow ($1, $3) }
567
568
569
570
571
572
573
574
;

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

primitive_type_arg:
575
576
| lqualid
   { PPTtyapp ($1, []) }
577
578
579
580
| quote_lident
   { PPTtyvar ($1, false) }
| opaque_quote_lident
   { PPTtyvar ($1, true) }
581
582
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
583
584
585
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
586
   { PPTparen $2 }
587
588
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
589
590
591
592
593
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

594
595
/* Logic expressions */

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

654
655
656
657
658
659
660
661
662
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

663
664
665
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
666
;
667

668
constant:
669
670
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
671
672
;

673
lexpr_arg:
674
| qualid            { mk_pp (PPident $1) }
675
676
677
678
| lexpr_arg_noid    { $1 }
;

lexpr_arg_noid:
Andrei Paskevich's avatar
Andrei Paskevich committed
679
680
681
682
683
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
684
| quote_uident      { mk_pp (PPident (Qident $1)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
685
686
687
;

lexpr_dot:
688
| lqualid_copy      { mk_pp (PPident $1) }
Andrei Paskevich's avatar
Andrei Paskevich committed
689
690
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
691
692
693
;

lexpr_sub:
694
| lexpr_dot DOT lqualid_rich
695
   { mk_pp (PPidapp ($3, [$1])) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
696
697
| LEFTPAR lexpr RIGHTPAR
   { $2 }
698
699
700
701
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
702
| LEFTBRC list1_field_value opt_semicolon RIGHTBRC
703
   { mk_pp (PPrecord (List.rev $2)) }
704
| LEFTBRC lexpr_arg WITH list1_field_value opt_semicolon RIGHTBRC
Andrei Paskevich's avatar
Andrei Paskevich committed
705
   { mk_pp (PPupdate ($2, List.rev $4)) }
706
| lexpr_arg LEFTSQ lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
707
   { mk_l_mixfix2 "[]" $1 $3 }
708
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
709
   { mk_l_mixfix3 "[<-]" $1 $3 $5 }
Andrei Paskevich's avatar
Andrei Paskevich committed
710
;
711

Andrei Paskevich's avatar
Andrei Paskevich committed
712
713
714
715
716
717
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

718
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
719

720
721
722
723
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
724

725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
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 */
740

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
741
742
743
744
745
746
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
747
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
748
749
750
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
| 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:
766
767
768
| 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
769
;
770

771
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
772
773
774
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
775

776
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
777
| UNDERSCORE                { mk_pat (PPpwild) }
778
| lident labels             { mk_pat (PPpvar (add_lab $1 $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
779
780
781
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
782
| LEFTBRC pfields RIGHTBRC  { mk_pat (PPprec $2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
783
784
785
786
787
788
789
790
791
;

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
792
793
;

794
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
795

796
797
798
list0_param:
| /* epsilon */ { [] }
| list1_param   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
799
800
;

801
list1_param:
802
803
| param               { $1 }
| param list1_param   { $1 @ $2 }
804
805
806
807
808
809
810
;

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

811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
/* [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
842
843
;

844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
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 }
874
875
;

876
877
878
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
879
880
;

881
882
883
884
885
886
887
888
889
890
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
891
892
;

893
894
895
896
897
898
899
900
901
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
902
903
;

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

quant_vars:
910
911
912
913
| list1_lident_labels opt_cast {
    List.map (function
      | loc, None -> Loc.errorm ~loc "anonymous binders are not allowed here"
      | _, Some i -> i, $2) $1 }
914
915
;

916
list0_lident_labels:
917
918
919
920
921
922
923
924
925
926
| /* 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) }
927
928
929
| anon_binder   { $1 }

anon_binder:
930
| UNDERSCORE    { floc (), None }
931
932
;

933
934
935
936
937
/* Idents */

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

Andrei Paskevich's avatar
Andrei Paskevich committed
940
941
942
943
944
945
946
947
948
949
950
951
952
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

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

lident_keyword:
| MODEL           { "model" }
;

953
954
955
956
957
958
959
960
961
962
963
964
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
965
966
/* Idents + symbolic operations' names */

967
968
969
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
970
971
;

972
lident_rich:
Andrei Paskevich's avatar
Andrei Paskevich committed
973
974
975
976
977
| lident        { $1 }
| lident_op_id  { $1 }
;

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

983
lident_op:
Andrei Paskevich's avatar
Andrei Paskevich committed
984
985
986
987
988
989
| prefix_op             { infix $1 }
| prefix_op UNDERSCORE  { prefix $1 }
| EQUAL                 { infix "=" }
| OPPREF                { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
990
| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
991
992
;

993
prefix_op:
994
995
996
997
998
999
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

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