parser.mly 36.7 KB
Newer Older
1 2 3
/********************************************************************/
/*                                                                  */
/*  The Why3 Verification Platform   /   The Why3 Development Team  */
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
4
/*  Copyright 2010-2014   --   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 42
  let mk_pp_l loc d = { pp_loc = loc; pp_desc = d }
  let mk_pp d = { pp_loc = floc (); pp_desc = d }
Andrei Paskevich's avatar
Andrei Paskevich committed
43

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

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

49
  let infix  s = "infix "  ^ s
50
  let prefix s = "prefix " ^ s
51
  let mixfix s = "mixfix " ^ s
52

53 54 55 56
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

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

57 58
  let mk_l_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
59
    mk_pp (PPidapp (Qident id, [e1]))
60 61 62 63 64 65 66

  let mk_l_infix e1 op e2 =
    let id = mk_id (infix op) (floc_i 2) in
    mk_pp (PPinfix (e1, id, e2))

  let mk_l_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
67
    mk_pp (PPidapp (Qident id, [e1;e2]))
68 69 70

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

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

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

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

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

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

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

97
  let id_anonymous () = mk_id "_" (floc ())
98

99 100 101 102 103 104 105 106 107 108
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
    | _, _ -> Loc.errorm ~loc:(floc ())
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
109
    sp_reads   = [];
110 111
    sp_writes  = [];
    sp_variant = [];
112 113
    sp_checkrw = false;
    sp_diverge = false;
114
  }
115

116 117 118 119
  let spec_union s1 s2 = {
    sp_pre     = s1.sp_pre @ s2.sp_pre;
    sp_post    = s1.sp_post @ s2.sp_post;
    sp_xpost   = s1.sp_xpost @ s2.sp_xpost;
120
    sp_reads   = s1.sp_reads @ s2.sp_reads;
121 122
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
123 124
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
125
  }
126

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

133 134 135
  let small_integer i =
    try
      match i with
136 137 138 139
      | Number.IConstDec s -> int_of_string s
      | Number.IConstHex s -> int_of_string ("0x"^s)
      | Number.IConstOct s -> int_of_string ("0o"^s)
      | Number.IConstBin s -> int_of_string ("0b"^s)
140 141
    with Failure _ -> raise Parsing.Parse_error

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

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

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

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

/* keywords */

159
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
160 161 162
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
163
%token THEN THEORY TRUE TYPE USE WITH
164

165 166
/* program keywords */

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

172 173
/* symbols */

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

%token EOF

185 186
/* program symbols */

187
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
188

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
216 217
/* Entry points */

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

226 227
open_file:
| /* epsilon */  { Incremental.open_file }
228 229
;

230
logic_file:
231
| list0_theory EOF  { Incremental.close_file () }
232 233 234
;

/* File, theory, namespace */
235

236 237 238
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
239 240
;

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

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

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

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

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

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

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

/* Declaration */

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

302 303 304 305 306
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

307 308
/* Use and clone */

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

316
use:
317 318 319 320 321 322
| 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 } }
323 324
;

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

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

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

subst:
341
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
342 343
| TYPE qualid type_args EQUAL primitive_type
                                { CStsym (floc (), $2, $3, $5) }
344 345 346
| CONSTANT  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| FUNCTION  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }
347
| VAL       qualid EQUAL qualid { CSvsym (floc (), $2, $4) }
348 349
| LEMMA     qualid              { CSlemma (floc (), $2) }
| GOAL      qualid              { CSgoal  (floc (), $2) }
350 351
;

352 353 354 355 356
ns:
| uqualid { Some $1 }
| DOT     { None }
;

357 358 359 360 361 362 363 364
/* Meta args */

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

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

374 375 376
/* Type declarations */

list1_type_decl:
377 378
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
379 380 381
;

type_decl:
382
| lident labels type_args typedefn
383
  { let model, vis, def, inv = $4 in
384
    let vis = if model then Abstract else vis in
385
    { td_loc = floc (); td_ident = add_lab $1 $2;
386 387
      td_params = $3; td_model = model;
      td_vis = vis; td_def = def; td_inv = inv } }
388 389
;

390 391 392 393 394 395 396
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 } }
;

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

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

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
421 422 423 424 425
;

equal_model:
| EQUAL { false }
| MODEL { true }
426 427 428
;

record_type:
429
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
430 431 432 433
;

list1_record_field:
| record_field                              { [$1] }
434
| list1_record_field SEMICOLON record_field { $3 :: $1 }
435 436
;

437 438 439 440 441 442 443 444
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

445
record_field:
446 447 448 449 450 451
| 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
452 453 454 455 456 457 458 459
;

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

typecase:
460
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
461 462 463 464
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
465 466 467 468 469 470 471 472 473 474
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 }
;

475
list1_logic_decl:
476 477
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
478 479
;

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

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

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

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

509 510 511
/* Inductive declarations */

list1_inductive_decl:
512 513
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
514 515 516
;

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

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

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

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

536 537 538
/* Type expressions */

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

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

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

564 565 566 567
list2_primitive_type_sep_comma:
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

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

573 574
/* Logic expressions */

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

633 634 635 636 637 638 639 640 641
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

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

647
constant:
648 649
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
650 651
;

652
lexpr_arg:
653
| qualid            { mk_pp (PPident $1) }
654 655 656 657 658
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
659
| quote_uident      { mk_pp (PPident (Qident $1)) }
660 661 662
;

lexpr_dot:
663
| lqualid_copy      { mk_pp (PPident $1) }
664 665
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
666 667 668
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
687 688 689 690 691 692
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

693
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
694

695 696 697 698
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
699

700 701 702 703 704 705 706 707 708
list1_trigger_sep_bar:
| trigger                           { [$1] }
| trigger BAR list1_trigger_sep_bar { $1 :: $3 }
;

trigger:
| list1_lexpr_sep_comma { $1 }
;

709 710 711 712
list2_lexpr_sep_comma:
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

713 714 715 716 717 718
list1_lexpr_sep_comma:
| lexpr                             { [$1] }
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

/* Match expressions */
719

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

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

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

750
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
751 752 753
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
754

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

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
771 772
;

773
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
774

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

780
list1_param:
781 782
| param               { $1 }
| param list1_param   { $1 @ $2 }
783 784 785 786 787 788 789
;

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

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

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

855 856 857
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
858 859
;

860 861 862 863 864 865 866 867 868 869
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
870 871
;

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

883 884 885 886 887 888
list1_quant_vars:
| quant_vars                        { $1 }
| quant_vars COMMA list1_quant_vars { $1 @ $3 }
;

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

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

anon_binder:
909
| UNDERSCORE    { floc (), None }
910 911
;

912 913 914 915 916
/* Idents */

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

919 920 921 922 923 924 925 926 927 928 929 930 931
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

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

lident_keyword:
| MODEL           { "model" }
;

932 933 934 935 936 937 938 939 940 941 942 943
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 ()) }
;

944 945
/* Idents + symbolic operations' names */

946 947 948
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
949 950
;

951
lident_rich:
952 953 954 955 956
| lident        { $1 }
| lident_op_id  { $1 }
;

lident_op_id:
957
| LEFTPAR lident_op RIGHTPAR  { mk_id $2 (floc_i 2) }
958
| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") (floc ()) }
959
  /* FIXME: use location of operator star rather than left parenthesis */
960 961
;

962
lident_op:
963 964 965 966 967 968
| prefix_op             { infix $1 }
| prefix_op UNDERSCORE  { prefix $1 }
| EQUAL                 { infix "=" }
| OPPREF                { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
969
| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
970 971
;

972
prefix_op:
973 974 975 976 977 978
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

979
/* Qualified idents */
980

981 982 983
qualid:
| ident_rich              { Qident $1 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }
984 985
;

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

lqualid:
992 993
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
994 995
;

996 997 998 999
/* copy of lqualid to avoid yacc conflicts */
lqualid_copy:
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
1000 1001
;

1002 1003 1004
uqualid:
| uident              { Qident $1 }
| uqualid DOT uident  { Qdot ($1, $3) }
1005 1006
;

1007 1008
/* Theory/Module names */

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

1014
any_qualid:
1015 1016 1017 1018 1019 1020 1021
| 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
1022
;
1023 1024 1025

/* Misc */

1026
label:
Andrei Paskevich's avatar
Andrei Paskevich committed
1027
| STRING    { Lstr (Ident.create_label $1) }
1028
| POSITION  { Lpos $1 }
1029 1030
;