parser.mly 36.5 KB
Newer Older
1 2 3
/********************************************************************/
/*                                                                  */
/*  The Why3 Verification Platform   /   The Why3 Development Team  */
4
/*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  */
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

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
42 43
  let mk_pp d = mk_ppl (floc ()) d
  let mk_pat p = { pat_loc = floc (); pat_desc = p }
Andrei Paskevich's avatar
Andrei Paskevich committed
44

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

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

51
  let infix  s = "infix "  ^ s
52
  let prefix s = "prefix " ^ s
53
  let mixfix s = "mixfix " ^ s
54

55 56 57 58
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

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

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

63 64
  let mk_l_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
65
    mk_pp (PPidapp (Qident id, [e1]))
66 67 68 69 70 71 72

  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
73
    mk_pp (PPidapp (Qident id, [e1;e2]))
74 75 76

  let mk_l_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
77
    mk_pp (PPidapp (Qident id, [e1;e2;e3]))
78

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
  let mk_expr d = { expr_loc = floc (); expr_desc = d }
85

86 87
  let mk_expr_i i d = { expr_loc = floc_i i; expr_desc = d }

88
  let mk_apply f a =
89 90
    let loc = Loc.join f.expr_loc a.expr_loc in
    { expr_loc = loc; expr_desc = Eapply (f,a) }
91

92 93 94 95 96 97 98
  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))
99

100 101
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
102
    mk_expr (Eidapp (Qident id, [e1; e2]))
103

104 105
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
106
    mk_expr (Eidapp (Qident id, [e1; e2; e3]))
107

108
  let id_anonymous () = mk_id "_" (floc ())
109

110 111 112 113 114 115 116 117 118 119
  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   = [];
120
    sp_reads   = [];
121 122
    sp_writes  = [];
    sp_variant = [];
123 124
    sp_checkrw = false;
    sp_diverge = false;
125
  }
126

127 128 129 130
  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;
131
    sp_reads   = s1.sp_reads @ s2.sp_reads;
132 133
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
134 135
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
136
  }
137

138
(* dead code
139
  let add_init_mark e =
140
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
141
    { e with expr_desc = Emark (init, e) }
142
*)
143

144 145 146
  let small_integer i =
    try
      match i with
147 148 149 150
      | 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)
151 152
    with Failure _ -> raise Parsing.Parse_error

153 154 155
  let qualid_last = function
    | Qident x | Qdot (_, x) -> x.id

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
156 157
%}

158
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
159

160
%token <string> LIDENT UIDENT
161
%token <Ptree.integer_constant> INTEGER
162
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
163 164
%token <Ptree.real_constant> FLOAT
%token <string> STRING
165
%token <Loc.position> POSITION
166
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
167 168 169

/* keywords */

170
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
171 172 173
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
174
%token THEN THEORY TRUE TYPE USE WITH
175

176 177
/* program keywords */

178
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DIVERGES DO DONE DOWNTO
179
%token ENSURES EXCEPTION FOR
180
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE PRIVATE RAISE
181
%token RAISES READS REC REQUIRES RETURNS TO TRY VAL VARIANT WHILE WRITES
182

183 184
/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
185
%token AND ARROW
186
%token BAR
187
%token COLON COMMA
188
%token DOT EQUAL LAMBDA LTGT
189
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
190
%token LARROW LRARROW OR
191
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
192
%token UNDERSCORE
193 194 195

%token EOF

196 197
/* program symbols */

198
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
199

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
200 201
/* Precedences */

202
%nonassoc prec_mark
203
%nonassoc prec_fun
204 205 206
%nonassoc IN
%right SEMICOLON
%nonassoc prec_no_else
207
%nonassoc DOT ELSE GHOST
208
%nonassoc prec_no_spec
209
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES DIVERGES VARIANT
210
%nonassoc prec_named
211
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
212

Andrei Paskevich's avatar
Andrei Paskevich committed
213
%right ARROW LRARROW
214 215
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
216
%nonassoc NOT
217
%left EQUAL LTGT OP1
218 219
%nonassoc LARROW
%nonassoc RIGHTSQ    /* stronger than <- for e1[e2 <- e3] */
220
%left OP2
221
%left OP3
222
%left OP4
223
%nonassoc prec_prefix_op
224 225
%nonassoc LEFTSQ
%nonassoc OPPREF
226

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
227 228
/* Entry points */

229 230 231
%type <Ptree.incremental -> unit> open_file
%start open_file
%type <unit> logic_file
232
%start logic_file
233
%type <unit> program_file
234
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
235 236
%%

237 238
open_file:
| /* epsilon */  { Incremental.open_file }
239 240
;

241
logic_file:
242
| list0_theory EOF  { Incremental.close_file () }
243 244 245
;

/* File, theory, namespace */
246

247 248 249
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
250 251
;

252
theory_head:
253
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
254 255
;

256
theory:
257
| theory_head list0_decl END  { Incremental.close_theory () }
258 259
;

260
list0_decl:
261 262
| /* epsilon */        { () }
| new_decl list0_decl  { () }
263
| new_ns_th list0_decl { () }
264 265 266 267
;

new_decl:
| decl
268
   { Incremental.new_decl (floc ()) $1 }
269
| use_clone
270
   { Incremental.use_clone (floc ()) $1 }
271 272 273
;

new_ns_th:
274 275
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
276 277
;

278
namespace_head:
279 280
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
281 282 283 284 285 286 287 288 289
;

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

/* Declaration */

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

313 314 315 316 317
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

318 319
/* Use and clone */

320 321
use_clone:
| USE use
322
    { ($2, None) }
323
| CLONE use clone_subst
324
    { ($2, Some $3) }
325 326
;

327
use:
328 329 330 331 332 333
| 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 } }
334 335
;

336 337 338
opt_import:
| /* epsilon */ { false }
| IMPORT        { true  }
339 340 341 342 343 344 345 346 347 348 349 350 351
;

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

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

subst:
352
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
353 354
| TYPE qualid type_args EQUAL primitive_type
                                { CStsym (floc (), $2, $3, $5) }
355 356 357 358 359
| 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) }
360 361
;

362 363 364 365 366
ns:
| uqualid { Some $1 }
| DOT     { None }
;

367 368 369 370 371 372 373 374
/* Meta args */

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

meta_arg:
375 376
| TYPE primitive_type { PMAty $2 }
| CONSTANT  qualid { PMAfs  $2 }
377 378
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
379 380
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
381
| INTEGER          { PMAint (small_integer $1) }
382 383
;

384 385 386
/* Type declarations */

list1_type_decl:
387 388
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
389 390 391
;

type_decl:
392
| lident labels type_args typedefn
393
  { let model, vis, def, inv = $4 in
394
    let vis = if model then Abstract else vis in
395
    { td_loc = floc (); td_ident = add_lab $1 $2;
396 397
      td_params = $3; td_model = model;
      td_vis = vis; td_def = def; td_inv = inv } }
398 399
;

400 401 402 403 404 405 406
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 } }
;

407
type_args:
408 409
| /* epsilon */                 { [] }
| quote_lident labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410 411 412
;

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

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
431 432 433 434 435
;

equal_model:
| EQUAL { false }
| MODEL { true }
436 437 438
;

record_type:
439
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
440 441 442 443
;

list1_record_field:
| record_field                              { [$1] }
444
| list1_record_field SEMICOLON record_field { $3 :: $1 }
445 446
;

447 448 449 450 451 452 453 454
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

455
record_field:
456 457 458 459 460 461
| 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
462 463 464 465 466 467 468 469
;

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

typecase:
470
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
471 472 473 474
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
475 476 477 478 479 480 481 482 483 484
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 }
;

485
list1_logic_decl:
486 487
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
488 489
;

490 491 492 493 494 495
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
496
logic_decl_function:
497
| lident_rich labels list0_param COLON primitive_type logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
498 499 500 501 502
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;

logic_decl_predicate:
503
| lident_rich labels list0_param logic_def_option
Andrei Paskevich's avatar
Andrei Paskevich committed
504 505 506 507
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = None; ld_def = $4 } }
;

508
logic_decl:
509
| lident_rich labels list0_param opt_cast logic_def_option
510
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
511
      ld_params = $3; ld_type = $4; ld_def = $5 } }
512 513 514 515 516
;

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

519 520 521
/* Inductive declarations */

list1_inductive_decl:
522 523
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
524 525 526
;

inductive_decl:
527
| lident_rich labels list0_param inddefn
528
  { { in_loc = floc (); in_ident = add_lab $1 $2;
529
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
530
;
531

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
532 533 534 535 536 537 538 539 540 541 542
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

546 547 548
/* Type expressions */

primitive_type:
549 550 551
| primitive_type_arg                  { $1 }
| lqualid primitive_type_args         { PPTtyapp ($1, $2) }
| primitive_type ARROW primitive_type { PPTarrow ($1, $3) }
552 553 554 555 556 557 558 559
;

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

primitive_type_arg:
560 561
| lqualid
   { PPTtyapp ($1, []) }
562 563 564 565
| quote_lident
   { PPTtyvar ($1, false) }
| opaque_quote_lident
   { PPTtyvar ($1, true) }
566 567
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
568 569 570
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
571
   { PPTparen $2 }
572 573
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
574 575 576 577 578
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

579 580
/* Logic expressions */

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

639 640 641 642 643 644 645 646 647
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

648 649 650
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
651
;
652

653
constant:
654 655
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
656 657
;

658
lexpr_arg:
659
| qualid            { mk_pp (PPident $1) }
660 661 662 663
| lexpr_arg_noid    { $1 }
;

lexpr_arg_noid:
664 665 666 667 668
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
669
| quote_uident      { mk_pp (PPident (Qident $1)) }
670 671 672
;

lexpr_dot:
673
| lqualid_copy      { mk_pp (PPident $1) }
674 675
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
676 677 678
;

lexpr_sub:
679
| lexpr_dot DOT lqualid_rich
680
   { mk_pp (PPidapp ($3, [$1])) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
681 682
| LEFTPAR lexpr RIGHTPAR
   { $2 }
683 684 685 686
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
687
| LEFTBRC list1_field_value opt_semicolon RIGHTBRC
688
   { mk_pp (PPrecord (List.rev $2)) }
689
| LEFTBRC lexpr_arg WITH list1_field_value opt_semicolon RIGHTBRC
Andrei Paskevich's avatar
Andrei Paskevich committed
690
   { mk_pp (PPupdate ($2, List.rev $4)) }
691
| lexpr_arg LEFTSQ lexpr RIGHTSQ
692
   { mk_l_mixfix2 "[]" $1 $3 }
693
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
694
   { mk_l_mixfix3 "[<-]" $1 $3 $5 }
Andrei Paskevich's avatar
Andrei Paskevich committed
695
;
696

Andrei Paskevich's avatar
Andrei Paskevich committed
697 698 699 700 701 702
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

703
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
704

705 706 707 708
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
709

710 711 712 713 714 715 716 717 718 719 720 721 722 723 724
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 */
725

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
726 727 728 729 730 731
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
732
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
733 734 735
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
736 737 738 739 740 741 742 743 744 745 746 747 748 749 750
| 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:
751 752 753
| 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
754
;
755

756
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
757 758 759
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
760

761
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
762
| UNDERSCORE                { mk_pat (PPpwild) }
763
| lident labels             { mk_pat (PPpvar (add_lab $1 $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
764 765 766
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
767
| LEFTBRC pfields RIGHTBRC  { mk_pat (PPprec $2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
768 769 770 771 772 773 774 775 776
;

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
777 778
;

779
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
780

781 782 783
list0_param:
| /* epsilon */ { [] }
| list1_param   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
784 785
;

786
list1_param:
787 788
| param               { $1 }
| param list1_param   { $1 @ $2 }
789 790 791 792 793 794 795
;

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

796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826
/* [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
827 828
;

829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858
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 }
859 860
;

861 862 863
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
864 865
;

866 867 868 869 870 871 872 873 874 875
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
876 877
;

878 879 880 881 882 883 884 885 886
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
887 888
;

889 890 891 892 893 894
list1_quant_vars:
| quant_vars                        { $1 }
| quant_vars COMMA list1_quant_vars { $1 @ $3 }
;

quant_vars:
895 896 897 898
| list1_lident_labels opt_cast {
    List.map (function
      | loc, None -> Loc.errorm ~loc "anonymous binders are not allowed here"
      | _, Some i -> i, $2) $1 }
899 900
;

901
list0_lident_labels:
902 903 904 905 906 907 908 909 910 911
| /* 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) }
912 913 914
| anon_binder   { $1 }

anon_binder:
915
| UNDERSCORE    { floc (), None }
916 917
;

918 919 920 921 922
/* Idents */

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

925 926 927 928 929 930 931 932 933 934 935 936 937
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

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

lident_keyword:
| MODEL           { "model" }
;

938 939 940 941 942 943 944 945 946 947 948 949
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 ()) }
;

950 951
/* Idents + symbolic operations' names */

952 953 954
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
955 956
;

957
lident_rich:
958 959 960 961 962
| lident        { $1 }
| lident_op_id  { $1 }
;

lident_op_id:
963
| LEFTPAR lident_op RIGHTPAR  { mk_id $2 (floc_i 2) }
964
| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") (floc ()) }
965
  /* FIXME: use location of operator star rather than left parenthesis */
966 967
;

968
lident_op:
969 970 971 972 973 974
| prefix_op             { infix $1 }
| prefix_op UNDERSCORE  { prefix $1 }
| EQUAL                 { infix "=" }
| OPPREF                { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
975
| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
976 977
;

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

985
/* Qualified idents */
986

987 988 989
qualid:
| ident_rich              { Qident $1 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }
990 991
;

992 993 994
lqualid_rich:
| lident_rich             { Qident $1 }
| uqualid DOT lident_rich { Qdot ($1, $3) }
995 996 997
;

lqualid:
998 999
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
1000 1001
;

1002 1003 1004 1005
/* copy of lqualid to avoid yacc conflicts */
lqualid_copy:
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
1006 1007
;

1008 1009 1010
uqualid:
| uident              { Qident $1 }
| uqualid DOT uident  { Qdot ($1, $3) }
1011 1012
;

1013 1014
/* Theory/Module names */

1015 1016 1017
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
1018
;
1019

1020
any_qualid:
1021 1022 1023 1024 1025 1026 1027
| 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
1028
;