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

  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
  let quote id = { id with id = "'" ^ id.id }

59
60
61
62
  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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
  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]))

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

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

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

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

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

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

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

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

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

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

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

127
128
129
130
131
132
133
134
135
136
137
138
139
140
  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 = [];
  }
141

142
143
144
145
146
147
148
  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;
149
  }
150

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

157
158
159
160
161
162
163
164
165
  let small_integer i =
    try
      match i with
      | Term.IConstDecimal s -> int_of_string s
      | Term.IConstHexa    s -> int_of_string ("0x"^s)
      | Term.IConstOctal   s -> int_of_string ("0o"^s)
      | Term.IConstBinary  s -> int_of_string ("0b"^s)
    with Failure _ -> raise Parsing.Parse_error

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
169
170
%}

171
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
172

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

/* keywords */

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

188
189
/* program keywords */

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

195
196
/* symbols */

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

%token EOF

209
210
/* program symbols */

211
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
212

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
213
214
/* Precedences */

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
239
240
/* Entry points */

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

249
250
open_file:
| /* epsilon */  { Incremental.open_file }
251
252
;

Andrei Paskevich's avatar
Andrei Paskevich committed
253
logic_file:
254
| list0_theory EOF  { Incremental.close_file () }
255
256
257
;

/* File, theory, namespace */
258

259
260
261
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
262
263
;

264
theory_head:
265
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
266
267
;

268
theory:
269
| theory_head list0_decl END  { Incremental.close_theory () }
270
271
;

272
list0_decl:
273
274
275
276
277
278
| /* epsilon */        { () }
| new_decl list0_decl  { () }
;

new_decl:
| decl
279
   { Incremental.new_decl (floc ()) $1 }
280
| use_clone
281
   { Incremental.use_clone (floc ()) $1 }
282
283
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
284
285
;

286
namespace_head:
287
288
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
289
290
291
292
293
294
295
296
297
;

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

/* Declaration */

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

321
322
323
324
325
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

326
327
/* Use and clone */

328
329
use_clone:
| USE use
330
    { ($2, None) }
331
| CLONE use clone_subst
332
    { ($2, Some $3) }
333
334
;

335
336
use:
| imp_exp tqualid
Andrei Paskevich's avatar
Andrei Paskevich committed
337
    { { use_theory = $2; use_as = qualid_last $2; use_imp_exp = $1 } }
338
| imp_exp tqualid AS uident
Andrei Paskevich's avatar
Andrei Paskevich committed
339
    { { use_theory = $2; use_as = $4.id; use_imp_exp = $1 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
340
341
;

342
imp_exp:
343
344
345
| IMPORT        { Some true }
| EXPORT        { None }
| /* epsilon */ { Some false }
346
347
348
349
350
351
352
353
354
355
356
357
358
;

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

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

subst:
359
360
361
362
363
364
365
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
| TYPE      qualid EQUAL qualid { CStsym (floc (), $2, $4) }
| 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) }
366
367
;

368
369
370
371
372
ns:
| uqualid { Some $1 }
| DOT     { None }
;

373
374
375
376
377
378
379
380
/* Meta args */

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

meta_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
381
| TYPE      qualid { PMAts  $2 }
382
383
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
384
385
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
386
| INTEGER          { PMAint (small_integer $1) }
387
388
;

389
390
391
/* Type declarations */

list1_type_decl:
392
393
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
394
395
396
;

type_decl:
397
| lident labels type_args typedefn
398
  { let model, vis, def, inv = $4 in
399
    let vis = if model then Abstract else vis in
400
    { td_loc = floc (); td_ident = add_lab $1 $2;
401
402
      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
403
404
;

405
406
407
408
409
410
411
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 } }
;

412
type_args:
413
414
| /* epsilon */             { [] }
| type_var labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
415
416
417
;

typedefn:
418
| /* epsilon */
419
    { false, Public, TDabstract, [] }
420
| equal_model visibility typecases type_invariant
421
    { $1, $2, TDalgebraic $3, $4 }
422
| equal_model visibility BAR typecases type_invariant
423
    { $1, $2, TDalgebraic $4, $5 }
424
| equal_model visibility record_type type_invariant
425
    { $1, $2, TDrecord $3, $4 }
426
427
428
/* 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;
429
      $1, Public, TDalias $3, [] }
430
431
432
433
434
435
;

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
436
437
438
439
440
;

equal_model:
| EQUAL { false }
| MODEL { true }
441
442
443
;

record_type:
444
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
445
446
447
448
;

list1_record_field:
| record_field                              { [$1] }
449
| list1_record_field SEMICOLON record_field { $3 :: $1 }
450
451
;

452
453
454
455
456
457
458
459
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

460
record_field:
461
462
463
464
465
466
| 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
467
468
469
470
471
472
473
474
;

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

typecase:
475
| uident labels params   { (floc (), add_lab $1 $2, $3) }
476
477
478
479
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
480
481
482
483
484
485
486
487
488
489
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 }
;

490
list1_logic_decl:
491
492
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
493
494
;

495
496
497
498
499
500
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
501
502
503
504
505
506
507
508
509
510
511
512
logic_decl_function:
| lident_rich labels params COLON primitive_type logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;

logic_decl_predicate:
| lident_rich labels params logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = None; ld_def = $4 } }
;

513
logic_decl:
514
| lident_rich labels params logic_type_option logic_def_option
515
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
516
      ld_params = $3; ld_type = $4; ld_def = $5 } }
517
518
519
520
521
522
523
524
525
526
;

logic_type_option:
| /* epsilon */        { None }
| COLON primitive_type { Some $2 }
;

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

529
530
531
/* Inductive declarations */

list1_inductive_decl:
532
533
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
534
535
536
;

inductive_decl:
537
| lident_rich labels params inddefn
538
  { { in_loc = floc (); in_ident = add_lab $1 $2;
539
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
540
;
541

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
542
543
544
545
546
547
548
549
550
551
552
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

556
557
558
559
560
561
562
563
/* Type expressions */

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

primitive_type_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
564
565
| primitive_type_arg_non_lident           { $1 }
| uqualid DOT lident primitive_type_args  { PPTtyapp ($4, Qdot ($1, $3)) }
566
567
568
569
570
571
572
573
;

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

primitive_type_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
574
| lident                         { PPTtyapp ([], Qident $1) }
575
576
577
578
| primitive_type_arg_non_lident  { $1 }
;

primitive_type_arg_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
579
580
| uqualid DOT lident
   { PPTtyapp ([], Qdot ($1, $3)) }
581
582
583
584
| type_var
   { PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
585
586
587
588
589
590
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

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

596
type_var:
597
| QUOTE lident { $2 }
598
599
;

600
601
/* Logic expressions */

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

658
659
660
661
662
663
664
665
666
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

667
668
669
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
670
;
671

672
constant:
Andrei Paskevich's avatar
Andrei Paskevich committed
673
674
| INTEGER   { Term.ConstInt $1 }
| FLOAT     { Term.ConstReal $1 }
675
676
;

677
lexpr_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
678
679
680
681
682
683
| 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 }
684
| QUOTE uident      { mk_pp (PPvar (Qident (quote $2))) }
Andrei Paskevich's avatar
Andrei Paskevich committed
685
686
687
;

lexpr_dot:
Andrei Paskevich's avatar
Andrei Paskevich committed
688
689
690
| lqualid_copy      { mk_pp (PPvar $1) }
| 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
Andrei Paskevich's avatar
Andrei Paskevich committed
695
   { mk_pp (PPapp ($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
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
716
717
| FUNC    { PPfunc }
| PRED    { PPpred }
Andrei Paskevich's avatar
Andrei Paskevich committed
718
719
;

720
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
721

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

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

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

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

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

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

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

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
794
795
;

796
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
797

798
799
800
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
801
802
;

803
804
805
806
807
808
809
810
811
812
813
814
815
param:
| LEFTPAR param_var RIGHTPAR
   { $2 }
| LEFTPAR param_type RIGHTPAR
   { [None, $2] }
| LEFTPAR param_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { [None, PPTtuple ($2::$4)] }
| LEFTPAR RIGHTPAR
   { [None, PPTtuple []] }
| type_var
   { [None, PPTtyvar $1] }
| lqualid
   { [None, PPTtyapp ([], $1)] }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
816
817
;

818
819
820
821
822
823
824
825
param_type:
| lident param_type_cont
   { PPTtyapp ($2, Qident $1) }
| lident list1_lident param_type_cont
   { let id2ty i = PPTtyapp ([], Qident i) in
     PPTtyapp (List.map id2ty $2 @ $3, Qident $1) }
| primitive_type_non_lident
   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
826
827
;

828
829
830
831
param_type_cont:
| /* epsilon */                                      { [] }
| primitive_type_arg_non_lident                      { [$1] }
| primitive_type_arg_non_lident primitive_type_args  { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
832
833
;

834
835
836
list1_param_var_sep_comma:
| param_var                                  { $1 }
| param_var COMMA list1_param_var_sep_comma  { $1 @ $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
837
838
;

839
840
841
param_var:
| list1_lident COLON primitive_type
   { List.map (fun id -> (Some id, $3)) $1 }
842
843
844
845
846
847
| list1_lident label labels list0_lident_labels COLON primitive_type
   { let l = match List.rev $1 with
       | i :: l -> add_lab i ($2 :: $3) :: l
       | [] -> assert false
     in
     List.map (fun id -> (Some id, $6)) (List.rev_append l $4) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
848
849
;

850
list1_lident:
851
852
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
853
854
;

855
856
857
858
859
list0_lident_labels:
| /* epsilon */                      { [] }
| lident labels list0_lident_labels  { add_lab $1 $2 :: $3 }
;

860
861
862
863
864
/* Idents */

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

Andrei Paskevich's avatar
Andrei Paskevich committed
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
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 */

882
883
884
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
885
886
;

887
lident_rich:
Andrei Paskevich's avatar
Andrei Paskevich committed
888
| lident                      { $1 }
889
| LEFTPAR lident_op RIGHTPAR  { mk_id $2 (floc_i 2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
890
| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") (floc ()) }
891
  /* FIXME: use location of operator star rather than left parenthesis */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
892
893
;

894
lident_op:
Andrei Paskevich's avatar
Andrei Paskevich committed
895
896
897
898
899
900
| prefix_op             { infix $1 }
| prefix_op UNDERSCORE  { prefix $1 }
| EQUAL                 { infix "=" }
| OPPREF                { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
901
| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
902
903
;

904
prefix_op:
905
906
907
908
909
910
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
911
/* Qualified idents */
912

Andrei Paskevich's avatar
Andrei Paskevich committed
913
914
915
qualid:
| ident_rich              { Qident $1 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }
916
917
;

Andrei Paskevich's avatar
Andrei Paskevich committed
918
919
920
lqualid_rich:
| lident_rich             { Qident $1 }
| uqualid DOT lident_rich { Qdot ($1, $3) }
921
922
923
;

lqualid:
Andrei Paskevich's avatar
Andrei Paskevich committed
924
925
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
926
927
;

Andrei Paskevich's avatar
Andrei Paskevich committed
928
929
930
931
/* copy of lqualid to avoid yacc conflicts */
lqualid_copy:
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
932
933
;

Andrei Paskevich's avatar
Andrei Paskevich committed
934
935
936
uqualid:
| uident              { Qident $1 }
| uqualid DOT uident  { Qdot ($1, $3) }
937
938
;

Andrei Paskevich's avatar
Andrei Paskevich committed
939
940
/* Theory/Module names */

941
942
943
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
944
;
945

Andrei Paskevich's avatar
Andrei Paskevich committed
946
any_qualid:
947
948
949
950
951
952
953
| sident                { Qident $1 }
| any_qualid DOT sident { Qdot ($1, $3) }
;

sident:
| ident   { $1 }
| STRING  { mk_id $1 (floc ()) }
Andrei Paskevich's avatar
Andrei Paskevich committed
954
;
955
956
957

/* Misc */

958
label:
Andrei Paskevich's avatar
Andrei Paskevich committed
959
| STRING    { Lstr (Ident.create_label $1) }
Andrei Paskevich's avatar
Andrei Paskevich committed
960
| POSITION  { Lpos $1 }
961
962
;

963
964
965
966
967
labels:
| /* epsilon */ { [] }
| label labels  { $1 :: $2 }
;

968
969
970
bar_:
| /* epsilon */ { () }
| BAR           { () }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
971
972
;

973
974
975
/****************************************************************************/

program_file:
976
| list0_theory_or_module EOF { Incremental.close_file () }
977
978
;

979
980
981
982
list0_theory_or_module:
| /* epsilon */                   { () }
| theory list0_theory_or_module   { () }
| module_ list0_theory_or_module  { () }
983
984
;

985
986
module_head:
| MODULE uident labels  { Incremental.open_module (add_lab $2 $3) }
987
988
;

989
990
module_:
| module_head list0_pdecl END  { Incremental.close_module () }
991
992
;

993
994
995
996
list0_pdecl:
| /* epsilon */         { () }
| new_decl  list0_pdecl { () }
| new_pdecl list0_pdecl { () }
997
998
;

999
new_pdecl:
1000
| pdecl { Incremental.new_pdecl (floc ()) $1 }
1001
1002
;