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.2 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
4
5
6
7
8
9
10
/********************************************************************/
/*                                                                  */
/*  The Why3 Verification Platform   /   The Why3 Development Team  */
/*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  */
/*                                                                  */
/*  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
  let quote id = { id with id = "'" ^ id.id }

70
71
72
73
  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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
  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]))

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

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

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

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

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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
130
131
  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
132
  let ty_unit () = PPTtuple []
133

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

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

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

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
180
181
%}

182
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183

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

/* keywords */

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

199
200
/* program keywords */

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

206
207
/* symbols */

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

%token EOF

220
221
/* program symbols */

222
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
223

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
224
225
/* Precedences */

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

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

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

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

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

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

/* File, theory, namespace */
269

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

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

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

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

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

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

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

/* Declaration */

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

332
333
334
335
336
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

337
338
/* Use and clone */

339
340
use_clone:
| USE use
341
    { ($2, None) }
342
| CLONE use clone_subst
343
    { ($2, Some $3) }
344
345
;

346
use:
347
348
349
350
351
352
| 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
353
354
;

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

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

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

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

381
382
383
384
385
ns:
| uqualid { Some $1 }
| DOT     { None }
;

386
387
388
389
390
391
392
393
/* Meta args */

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

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

403
404
405
/* Type declarations */

list1_type_decl:
406
407
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
408
409
410
;

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

419
420
421
422
423
424
425
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 } }
;

426
type_args:
427
428
| /* epsilon */             { [] }
| type_var labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429
430
431
;

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

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
450
451
452
453
454
;

equal_model:
| EQUAL { false }
| MODEL { true }
455
456
457
;

record_type:
458
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
459
460
461
462
;

list1_record_field:
| record_field                              { [$1] }
463
| list1_record_field SEMICOLON record_field { $3 :: $1 }
464
465
;

466
467
468
469
470
471
472
473
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

474
record_field:
475
476
477
478
479
480
| 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
481
482
483
484
485
486
487
488
;

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

typecase:
489
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
490
491
492
493
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
494
495
496
497
498
499
500
501
502
503
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 }
;

504
list1_logic_decl:
505
506
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
507
508
;

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

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

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

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

538
539
540
/* Inductive declarations */

list1_inductive_decl:
541
542
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
543
544
545
;

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

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

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

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

565
566
567
568
/* Type expressions */

primitive_type:
| primitive_type_arg           { $1 }
569
| lqualid primitive_type_args  { PPTtyapp ($1, $2) }
570
571
572
;

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

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

582
583
584
585
586
primitive_type_args_non_lident:
| primitive_type_arg_non_lident                      { [$1] }
| primitive_type_arg_non_lident primitive_type_args  { $1 :: $2 }
;

587
primitive_type_arg:
588
| lident                         { PPTtyapp (Qident $1, []) }
589
590
591
592
| primitive_type_arg_non_lident  { $1 }
;

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

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

610
type_var:
611
| QUOTE lident { $2 }
612
613
;

614
615
/* Logic expressions */

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

674
675
676
677
678
679
680
681
682
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

683
684
685
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
686
;
687

688
constant:
689
690
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
691
692
;

693
lexpr_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
694
695
696
697
698
699
| 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 }
700
| QUOTE uident      { mk_pp (PPvar (Qident (quote $2))) }
Andrei Paskevich's avatar
Andrei Paskevich committed
701
702
703
;

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

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

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

736
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
737

738
739
740
741
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
742

743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
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 */
758

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

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

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

789
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
790
791
792
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
793

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

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
810
811
;

812
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
813

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

819
820
821
822
823
824
825
826
827
828
list1_param:
| list1_binder  { params_of_binders $1 }
;

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

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

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

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

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

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

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

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

921
922
923
924
925
/* Idents */

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

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

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

lident_keyword:
| MODEL           { "model" }
;

/* 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
;

999
1000
1001
1002
lqualid_qualified:
| uqualid DOT lident  { Qdot ($1, $3) }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
1003
1004
1005
uqualid:
| uident              { Qident $1 }
| uqualid DOT uident  { Qdot ($1, $3) }
1006
1007
;

Andrei Paskevich's avatar
Andrei Paskevich committed
1008
1009
/* Theory/Module names */