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 36.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

36
(* dead code
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
37
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
38
  let floc_ij i j = Loc.extract (loc_ij i j)
39
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
40

41
42
  let mk_pp_l loc d = { pp_loc = loc; pp_desc = d }
  let mk_pp d = { pp_loc = floc (); pp_desc = d }
Andrei Paskevich's avatar
Andrei Paskevich committed
43

44
  let mk_pat p = { pat_loc = floc (); pat_desc = p }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45

46
47
  let infix_pp a i b = mk_pp (PPbinop (a, i, b))
  let prefix_pp p a = mk_pp (PPunop (p, a))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
48

49
  let infix  s = "infix "  ^ s
50
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
51
  let mixfix s = "mixfix " ^ s
52

53
54
55
56
  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
57
58
  let mk_l_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
59
    mk_pp (PPidapp (Qident id, [e1]))
Andrei Paskevich's avatar
Andrei Paskevich committed
60
61
62
63
64
65
66

  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
67
    mk_pp (PPidapp (Qident id, [e1;e2]))
Andrei Paskevich's avatar
Andrei Paskevich committed
68
69
70

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

73
74
75
  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
76
      | _ -> raise exn)
77

78
  let mk_expr_l loc d = { expr_loc = loc; expr_desc = d }
79
  let mk_expr d = { expr_loc = floc (); expr_desc = d }
80

81
82
83
84
85
86
87
  let mk_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
    mk_expr (Eidapp (Qident id, [e1]))

  let mk_infix e1 op e2 =
    let id = mk_id (infix op) (floc_i 2) in
    mk_expr (Einfix (e1, id, e2))
88

Andrei Paskevich's avatar
Andrei Paskevich committed
89
90
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
91
    mk_expr (Eidapp (Qident id, [e1; e2]))
92

Andrei Paskevich's avatar
Andrei Paskevich committed
93
94
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
95
    mk_expr (Eidapp (Qident id, [e1; e2; e3]))
96

Andrei Paskevich's avatar
Andrei Paskevich committed
97
  let id_anonymous () = mk_id "_" (floc ())
98

99
100
101
102
103
104
105
106
107
108
  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   = [];
109
    sp_reads   = [];
110
111
    sp_writes  = [];
    sp_variant = [];
112
113
    sp_checkrw = false;
    sp_diverge = false;
114
  }
115

116
117
118
119
  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;
120
    sp_reads   = s1.sp_reads @ s2.sp_reads;
121
122
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
123
124
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
125
  }
126

127
(* dead code
128
  let add_init_mark e =
129
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
130
    { e with expr_desc = Emark (init, e) }
131
*)
132

133
134
135
  let small_integer i =
    try
      match i with
136
137
138
139
      | 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)
140
141
    with Failure _ -> raise Parsing.Parse_error

142
143
144
  let qualid_last = function
    | Qident x | Qdot (_, x) -> x.id

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
145
146
%}

147
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
148

149
%token <string> LIDENT UIDENT
150
%token <Ptree.integer_constant> INTEGER
151
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152
153
%token <Ptree.real_constant> FLOAT
%token <string> STRING
154
%token <Loc.position> POSITION
155
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
156
157
158

/* keywords */

159
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
160
161
162
%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
163
%token THEN THEORY TRUE TYPE USE WITH
164

165
166
/* program keywords */

167
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DIVERGES DO DONE DOWNTO
168
%token ENSURES EXCEPTION FOR
169
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE PRIVATE RAISE
170
%token RAISES READS REC REQUIRES RETURNS TO TRY VAL VARIANT WHILE WRITES
171

172
173
/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
174
%token AND ARROW
175
%token BAR
176
%token COLON COMMA
177
%token DOT EQUAL LAMBDA LTGT
178
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
179
%token LARROW LRARROW OR
180
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
181
%token UNDERSCORE
182
183
184

%token EOF

185
186
/* program symbols */

187
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
188

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189
190
/* Precedences */

191
%nonassoc prec_mark
192
%nonassoc prec_fun
193
194
195
%nonassoc IN
%right SEMICOLON
%nonassoc prec_no_else
196
%nonassoc DOT ELSE GHOST
197
%nonassoc prec_named
198
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
199

Andrei Paskevich's avatar
Andrei Paskevich committed
200
%right ARROW LRARROW
201
202
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
203
%nonassoc NOT
204
%left EQUAL LTGT OP1
205
206
%nonassoc LARROW
%nonassoc RIGHTSQ    /* stronger than <- for e1[e2 <- e3] */
207
%left OP2
208
%left OP3
209
%left OP4
210
%nonassoc prec_prefix_op
211
212
%nonassoc LEFTSQ
%nonassoc OPPREF
213

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
214
215
/* Entry points */

216
217
218
%type <Ptree.incremental -> unit> open_file
%start open_file
%type <unit> logic_file
Andrei Paskevich's avatar
Andrei Paskevich committed
219
%start logic_file
220
%type <unit> program_file
221
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
222
223
%%

224
225
open_file:
| /* epsilon */  { Incremental.open_file }
226
227
;

Andrei Paskevich's avatar
Andrei Paskevich committed
228
logic_file:
229
| list0_theory EOF  { Incremental.close_file () }
230
231
232
;

/* File, theory, namespace */
233

234
235
236
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
237
238
;

239
theory_head:
240
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
241
242
;

243
theory:
244
| theory_head list0_decl END  { Incremental.close_theory () }
245
246
;

247
list0_decl:
248
249
| /* epsilon */        { () }
| new_decl list0_decl  { () }
250
| new_ns_th list0_decl { () }
251
252
253
254
;

new_decl:
| decl
255
   { Incremental.new_decl (floc ()) $1 }
256
| use_clone
257
   { Incremental.use_clone (floc ()) $1 }
258
259
260
;

new_ns_th:
261
262
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
263
264
;

265
namespace_head:
266
267
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
268
269
270
271
272
273
274
275
276
;

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

/* Declaration */

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

300
301
302
303
304
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

305
306
/* Use and clone */

307
308
use_clone:
| USE use
309
    { ($2, None) }
310
| CLONE use clone_subst
311
    { ($2, Some $3) }
312
313
;

314
use:
315
316
317
318
319
320
| 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
321
322
;

323
324
325
opt_import:
| /* epsilon */ { false }
| IMPORT        { true  }
326
327
328
329
330
331
332
333
334
335
336
337
338
;

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

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

subst:
339
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
340
341
| TYPE qualid type_args EQUAL primitive_type
                                { CStsym (floc (), $2, $3, $5) }
342
343
344
345
346
| 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) }
347
348
;

349
350
351
352
353
ns:
| uqualid { Some $1 }
| DOT     { None }
;

354
355
356
357
358
359
360
361
/* Meta args */

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

meta_arg:
362
363
| TYPE primitive_type { PMAty $2 }
| CONSTANT  qualid { PMAfs  $2 }
364
365
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
366
367
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
368
| INTEGER          { PMAint (small_integer $1) }
369
370
;

371
372
373
/* Type declarations */

list1_type_decl:
374
375
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
376
377
378
;

type_decl:
379
| lident labels type_args typedefn
380
  { let model, vis, def, inv = $4 in
381
    let vis = if model then Abstract else vis in
382
    { td_loc = floc (); td_ident = add_lab $1 $2;
383
384
      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
385
386
;

387
388
389
390
391
392
393
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 } }
;

394
type_args:
395
396
| /* epsilon */                 { [] }
| quote_lident labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
397
398
399
;

typedefn:
400
| /* epsilon */
401
    { false, Public, TDabstract, [] }
402
| equal_model visibility typecases type_invariant
403
    { $1, $2, TDalgebraic $3, $4 }
404
| equal_model visibility BAR typecases type_invariant
405
    { $1, $2, TDalgebraic $4, $5 }
406
| equal_model visibility record_type type_invariant
407
    { $1, $2, TDrecord $3, $4 }
408
409
410
/* 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;
411
      $1, Public, TDalias $3, [] }
412
413
414
415
416
417
;

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
418
419
420
421
422
;

equal_model:
| EQUAL { false }
| MODEL { true }
423
424
425
;

record_type:
426
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
427
428
429
430
;

list1_record_field:
| record_field                              { [$1] }
431
| list1_record_field SEMICOLON record_field { $3 :: $1 }
432
433
;

434
435
436
437
438
439
440
441
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

442
record_field:
443
444
445
446
447
448
| 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
449
450
451
452
453
454
455
456
;

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

typecase:
457
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
458
459
460
461
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
462
463
464
465
466
467
468
469
470
471
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 }
;

472
list1_logic_decl:
473
474
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
475
476
;

477
478
479
480
481
482
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
483
logic_decl_function:
484
| lident_rich labels list0_param COLON primitive_type logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
485
486
487
488
489
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;

logic_decl_predicate:
490
| lident_rich labels list0_param logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
491
492
493
494
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = None; ld_def = $4 } }
;

495
logic_decl:
496
| lident_rich labels list0_param opt_cast logic_def_option
497
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
498
      ld_params = $3; ld_type = $4; ld_def = $5 } }
499
500
501
502
503
;

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

506
507
508
/* Inductive declarations */

list1_inductive_decl:
509
510
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
511
512
513
;

inductive_decl:
514
| lident_rich labels list0_param inddefn
515
  { { in_loc = floc (); in_ident = add_lab $1 $2;
516
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
517
;
518

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
519
520
521
522
523
524
525
526
527
528
529
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

533
534
535
/* Type expressions */

primitive_type:
536
537
538
| primitive_type_arg                  { $1 }
| lqualid primitive_type_args         { PPTtyapp ($1, $2) }
| primitive_type ARROW primitive_type { PPTarrow ($1, $3) }
539
540
541
542
543
544
545
546
;

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

primitive_type_arg:
547
548
| lqualid
   { PPTtyapp ($1, []) }
549
550
551
552
| quote_lident
   { PPTtyvar ($1, false) }
| opaque_quote_lident
   { PPTtyvar ($1, true) }
553
554
| LEFTPAR list2_primitive_type_sep_comma RIGHTPAR
   { PPTtuple $2 }
555
556
557
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
558
   { PPTparen $2 }
559
560
;

561
562
563
564
list2_primitive_type_sep_comma:
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
565
566
567
568
569
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

570
571
/* Logic expressions */

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

630
631
632
633
634
635
636
637
638
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

639
list1_lexpr_arg:
640
641
| lexpr_arg                 { [rhs_end_pos 1, $1] }
| lexpr_arg list1_lexpr_arg { (rhs_end_pos 1, $1) :: $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
642
;
643

644
constant:
645
646
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
647
648
;

649
lexpr_arg:
650
| qualid            { mk_pp (PPident $1) }
Andrei Paskevich's avatar
Andrei Paskevich committed
651
652
653
654
655
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
656
| quote_uident      { mk_pp (PPident (Qident $1)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
657
658
659
;

lexpr_dot:
660
| lqualid_copy      { mk_pp (PPident $1) }
Andrei Paskevich's avatar
Andrei Paskevich committed
661
662
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
663
664
665
;

lexpr_sub:
666
| lexpr_dot DOT lqualid_rich
667
   { mk_pp (PPidapp ($3, [$1])) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
668
669
| LEFTPAR lexpr RIGHTPAR
   { $2 }
670
671
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
672
673
| LEFTPAR list2_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple $2) }
674
| LEFTBRC list1_field_value opt_semicolon RIGHTBRC
675
   { mk_pp (PPrecord (List.rev $2)) }
676
| LEFTBRC lexpr_arg WITH list1_field_value opt_semicolon RIGHTBRC
Andrei Paskevich's avatar
Andrei Paskevich committed
677
   { mk_pp (PPupdate ($2, List.rev $4)) }
678
| lexpr_arg LEFTSQ lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
679
   { mk_l_mixfix2 "[]" $1 $3 }
680
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
681
   { mk_l_mixfix3 "[<-]" $1 $3 $5 }
Andrei Paskevich's avatar
Andrei Paskevich committed
682
;
683

Andrei Paskevich's avatar
Andrei Paskevich committed
684
685
686
687
688
689
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

690
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
691

692
693
694
695
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
696

697
698
699
700
701
702
703
704
705
list1_trigger_sep_bar:
| trigger                           { [$1] }
| trigger BAR list1_trigger_sep_bar { $1 :: $3 }
;

trigger:
| list1_lexpr_sep_comma { $1 }
;

706
707
708
709
list2_lexpr_sep_comma:
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

710
711
712
713
714
715
list1_lexpr_sep_comma:
| lexpr                             { [$1] }
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

/* Match expressions */
716

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
717
718
719
720
721
722
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
723
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
724
725
726
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
| 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:
742
743
744
| 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
745
;
746

747
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
748
749
750
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
751

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

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
768
769
;

770
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
771

772
773
774
list0_param:
| /* epsilon */ { [] }
| list1_param   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
775
776
;

777
list1_param:
778
779
| param               { $1 }
| param list1_param   { $1 @ $2 }
780
781
782
783
784
785
786
;

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

787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
/* [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
818
819
;

820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
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 }
850
851
;

852
853
854
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
855
856
;

857
858
859
860
861
862
863
864
865
866
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
867
868
;

869
870
871
872
873
874
875
876
877
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
878
879
;

880
881
882
883
884
885
list1_quant_vars:
| quant_vars                        { $1 }
| quant_vars COMMA list1_quant_vars { $1 @ $3 }
;

quant_vars:
886
887
888
889
| list1_lident_labels opt_cast {
    List.map (function
      | loc, None -> Loc.errorm ~loc "anonymous binders are not allowed here"
      | _, Some i -> i, $2) $1 }
890
891
;

892
list0_lident_labels:
893
894
895
896
897
898
899
900
901
902
| /* 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) }
903
904
905
| anon_binder   { $1 }

anon_binder:
906
| UNDERSCORE    { floc (), None }
907
908
;

909
910
911
912
913
/* Idents */

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

Andrei Paskevich's avatar
Andrei Paskevich committed
916
917
918
919
920
921
922
923
924
925
926
927
928
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

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

lident_keyword:
| MODEL           { "model" }
;

929
930
931
932
933
934
935
936
937
938
939
940
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
941
942
/* Idents + symbolic operations' names */

943
944
945
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
946
947
;

948
lident_rich:
Andrei Paskevich's avatar
Andrei Paskevich committed
949
950
951
952
953
| lident        { $1 }
| lident_op_id  { $1 }
;

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

959
lident_op:
Andrei Paskevich's avatar
Andrei Paskevich committed
960
961
962
963
964
965
| prefix_op             { infix $1 }
| prefix_op UNDERSCORE  { prefix $1 }
| EQUAL                 { infix "=" }
| OPPREF                { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
966
| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
967
968
;

969
prefix_op:
970
971
972
973
974
975
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
976
/* Qualified idents */
977

Andrei Paskevich's avatar
Andrei Paskevich committed
978
979
980
qualid:
| ident_rich              { Qident $1 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }
981
982
;

Andrei Paskevich's avatar
Andrei Paskevich committed
983
984
985
lqualid_rich:
| lident_rich             { Qident $1 }
| uqualid DOT lident_rich { Qdot ($1, $3) }
986
987
988
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
993
994
995
996
/* copy of lqualid to avoid yacc conflicts */
lqualid_copy:
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
997
998
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
1004
1005
/* Theory/Module names */

1006
1007
1008
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
1009
;
1010

Andrei Paskevich's avatar
Andrei Paskevich committed
1011
any_qualid:
1012
1013
1014
1015
1016
1017
1018
| sident                { Qident $1 }