parser.mly 37 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
(* 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
55
  let mixfix s = "mixfix " ^ s
56

57 58 59 60
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

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

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

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

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

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

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

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

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

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

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

105 106
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
107 108
    mk_expr (mk_apply_id id [e1; e2])

109 110
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
111 112
    mk_expr (mk_apply_id id [e1; e2; e3])

113
  let mk_infix e1 op e2 =
114
    let id = mk_id (infix op) (floc_i 2) in
115
    mk_expr (Einfix (e1, id, e2))
116 117

  let mk_prefix op e1 =
118
    let id = mk_id (prefix op) (floc_i 1) in
119 120
    mk_expr (mk_apply_id id [e1])

121 122
  let exit_exn () = Qident (mk_id "%Exit" (floc ()))
  let id_anonymous () = mk_id "_" (floc ())
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
123
  let ty_unit () = PPTtuple []
124

125
(* dead code
126
  let id_lt_nat () = Qident (mk_id "lt_nat" (floc ()))
127
*)
128

129 130 131 132 133 134 135 136 137 138
  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   = [];
139
    sp_reads   = [];
140 141 142
    sp_writes  = [];
    sp_variant = [];
  }
143

144 145 146 147
  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;
148
    sp_reads   = s1.sp_reads @ s2.sp_reads;
149 150
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
151
  }
152

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

159 160 161
  let small_integer i =
    try
      match i with
162 163 164 165
      | 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)
166 167
    with Failure _ -> raise Parsing.Parse_error

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
171 172
%}

173
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174

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

/* keywords */

185
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
186 187 188
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
189
%token THEN THEORY TRUE TYPE USE WITH
190

191 192
/* program keywords */

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

198 199
/* symbols */

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

%token EOF

211 212
/* program symbols */

213
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
214

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
215 216
/* Precedences */

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
242 243
/* Entry points */

244 245 246
%type <Ptree.incremental -> unit> open_file
%start open_file
%type <unit> logic_file
247
%start logic_file
248
%type <unit> program_file
249
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
250 251
%%

252 253
open_file:
| /* epsilon */  { Incremental.open_file }
254 255
;

256
logic_file:
257
| list0_theory EOF  { Incremental.close_file () }
258 259 260
;

/* File, theory, namespace */
261

262 263 264
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
265 266
;

267
theory_head:
268
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
269 270
;

271
theory:
272
| theory_head list0_decl END  { Incremental.close_theory () }
273 274
;

275
list0_decl:
276 277
| /* epsilon */        { () }
| new_decl list0_decl  { () }
278
| new_ns_th list0_decl { () }
279 280 281 282
;

new_decl:
| decl
283
   { Incremental.new_decl (floc ()) $1 }
284
| use_clone
285
   { Incremental.use_clone (floc ()) $1 }
286 287 288
;

new_ns_th:
289 290
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
291 292
;

293
namespace_head:
294 295
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
296 297 298 299 300 301 302 303 304
;

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

/* Declaration */

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

328 329 330 331 332
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

333 334
/* Use and clone */

335 336
use_clone:
| USE use
337
    { ($2, None) }
338
| CLONE use clone_subst
339
    { ($2, Some $3) }
340 341
;

342
use:
343 344 345 346 347 348
| 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 } }
349 350
;

351 352 353
opt_import:
| /* epsilon */ { false }
| IMPORT        { true  }
354 355 356 357 358 359 360 361 362 363 364 365 366
;

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

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

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

377 378 379 380 381
ns:
| uqualid { Some $1 }
| DOT     { None }
;

382 383 384 385 386 387 388 389
/* Meta args */

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

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

399 400 401
/* Type declarations */

list1_type_decl:
402 403
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
404 405 406
;

type_decl:
407
| lident labels type_args typedefn
408
  { let model, vis, def, inv = $4 in
409
    let vis = if model then Abstract else vis in
410
    { td_loc = floc (); td_ident = add_lab $1 $2;
411 412
      td_params = $3; td_model = model;
      td_vis = vis; td_def = def; td_inv = inv } }
413 414
;

415 416 417 418 419 420 421
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 } }
;

422
type_args:
423 424
| /* epsilon */                 { [] }
| quote_lident labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
425 426 427
;

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

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
446 447 448 449 450
;

equal_model:
| EQUAL { false }
| MODEL { true }
451 452 453
;

record_type:
454
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
455 456 457 458
;

list1_record_field:
| record_field                              { [$1] }
459
| list1_record_field SEMICOLON record_field { $3 :: $1 }
460 461
;

462 463 464 465 466 467 468 469
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

470
record_field:
471 472 473 474 475 476
| 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
477 478 479 480 481 482 483 484
;

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

typecase:
485
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
486 487 488 489
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
490 491 492 493 494 495 496 497 498 499
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 }
;

500
list1_logic_decl:
501 502
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
503 504
;

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

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

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

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

534 535 536
/* Inductive declarations */

list1_inductive_decl:
537 538
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
539 540 541
;

inductive_decl:
542
| lident_rich labels list0_param inddefn
543
  { { in_loc = floc (); in_ident = add_lab $1 $2;
544
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
545
;
546

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

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

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

561 562 563
/* Type expressions */

primitive_type:
564 565 566
| primitive_type_arg                  { $1 }
| lqualid primitive_type_args         { PPTtyapp ($1, $2) }
| primitive_type ARROW primitive_type { PPTarrow ($1, $3) }
567 568 569 570 571 572 573 574
;

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

primitive_type_arg:
575 576
| lqualid
   { PPTtyapp ($1, []) }
577 578 579 580
| quote_lident
   { PPTtyvar ($1, false) }
| opaque_quote_lident
   { PPTtyvar ($1, true) }
581 582
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
583 584 585
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
586
   { PPTparen $2 }
587 588
;

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

594 595
/* Logic expressions */

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

654 655 656 657 658 659 660 661 662
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

663 664 665
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
666
;
667

668
constant:
669 670
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
671 672
;

673
lexpr_arg:
674
| qualid            { mk_pp (PPident $1) }
675 676 677 678
| lexpr_arg_noid    { $1 }
;

lexpr_arg_noid:
679 680 681 682 683
| 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 (PPident (Qident $1)) }
685 686 687
;

lexpr_dot:
688
| lqualid_copy      { mk_pp (PPident $1) }
689 690
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
691 692 693
;

lexpr_sub:
694
| lexpr_dot DOT lqualid_rich
695
   { mk_pp (PPidapp ($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
707
   { mk_l_mixfix2 "[]" $1 $3 }
708
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
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 716 717
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

718
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
719

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

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

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

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

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

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

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

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
792 793
;

794
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
795

796 797 798
list0_param:
| /* epsilon */ { [] }
| list1_param   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
799 800
;

801
list1_param:
802 803
| param               { $1 }
| param list1_param   { $1 @ $2 }
804 805 806 807 808 809 810
;

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

811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841
/* [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
842 843
;

844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873
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 }
874 875
;

876 877 878
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
879 880
;

881 882 883 884 885 886 887 888 889 890
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
891 892
;

893 894 895 896 897 898 899 900 901
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
902 903
;

904 905 906 907 908 909
list1_quant_vars:
| quant_vars                        { $1 }
| quant_vars COMMA list1_quant_vars { $1 @ $3 }
;

quant_vars:
910 911 912 913
| list1_lident_labels opt_cast {
    List.map (function
      | loc, None -> Loc.errorm ~loc "anonymous binders are not allowed here"
      | _, Some i -> i, $2) $1 }
914 915
;

916
list0_lident_labels:
917 918 919 920 921 922 923 924 925 926
| /* 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) }
927 928 929
| anon_binder   { $1 }

anon_binder:
930
| UNDERSCORE    { floc (), None }
931 932
;

933 934 935 936 937
/* Idents */

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

940 941 942 943 944 945 946 947 948 949 950 951 952
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

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

lident_keyword:
| MODEL           { "model" }
;

953 954 955 956 957 958 959 960 961 962 963 964
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 ()) }
;

965 966
/* Idents + symbolic operations' names */

967 968 969
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
970 971
;

972
lident_rich:
973 974 975 976 977
| lident        { $1 }
| lident_op_id  { $1 }
;

lident_op_id:
978
| LEFTPAR lident_op RIGHTPAR  { mk_id $2 (floc_i 2) }
979
| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") (floc ()) }
980
  /* FIXME: use location of operator star rather than left parenthesis */
981 982
;

983
lident_op:
984 985 986 987 988 989
| prefix_op             { infix $1 }
| prefix_op UNDERSCORE  { prefix $1 }
| EQUAL                 { infix "=" }
| OPPREF                { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
990
| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
991 992
;

993
prefix_op:
994 995 996 997 998 999
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

1000
/* Qualified idents */
1001

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

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

lqualid:
1013 1014
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
1015 1016
;

1017 1018 1019 1020
/* copy of lqualid to avoid yacc conflicts */
lqualid_copy:
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }