parser.mly 36.1 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 123
    sp_writes  = [];
    sp_variant = [];
  }
124

125 126 127 128
  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;
129
    sp_reads   = s1.sp_reads @ s2.sp_reads;
130 131
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
132
  }
133

134
(* dead code
135
  let add_init_mark e =
136
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
137
    { e with expr_desc = Emark (init, e) }
138
*)
139

140 141 142
  let small_integer i =
    try
      match i with
143 144 145 146
      | 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)
147 148
    with Failure _ -> raise Parsing.Parse_error

149 150 151
  let qualid_last = function
    | Qident x | Qdot (_, x) -> x.id

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152 153
%}

154
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155

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

/* keywords */

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

172 173
/* program keywords */

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

179 180
/* symbols */

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

%token EOF

192 193
/* program symbols */

194
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
195

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196 197
/* Precedences */

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
223 224
/* Entry points */

225 226 227
%type <Ptree.incremental -> unit> open_file
%start open_file
%type <unit> logic_file
228
%start logic_file
229
%type <unit> program_file
230
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
231 232
%%

233 234
open_file:
| /* epsilon */  { Incremental.open_file }
235 236
;

237
logic_file:
238
| list0_theory EOF  { Incremental.close_file () }
239 240 241
;

/* File, theory, namespace */
242

243 244 245
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
246 247
;

248
theory_head:
249
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
250 251
;

252
theory:
253
| theory_head list0_decl END  { Incremental.close_theory () }
254 255
;

256
list0_decl:
257 258
| /* epsilon */        { () }
| new_decl list0_decl  { () }
259
| new_ns_th list0_decl { () }
260 261 262 263
;

new_decl:
| decl
264
   { Incremental.new_decl (floc ()) $1 }
265
| use_clone
266
   { Incremental.use_clone (floc ()) $1 }
267 268 269
;

new_ns_th:
270 271
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
272 273
;

274
namespace_head:
275 276
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
277 278 279 280 281 282 283 284 285
;

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

/* Declaration */

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

309 310 311 312 313
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

314 315
/* Use and clone */

316 317
use_clone:
| USE use
318
    { ($2, None) }
319
| CLONE use clone_subst
320
    { ($2, Some $3) }
321 322
;

323
use:
324 325 326 327 328 329
| 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 } }
330 331
;

332 333 334
opt_import:
| /* epsilon */ { false }
| IMPORT        { true  }
335 336 337 338 339 340 341 342 343 344 345 346 347
;

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

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

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

358 359 360 361 362
ns:
| uqualid { Some $1 }
| DOT     { None }
;

363 364 365 366 367 368 369 370
/* Meta args */

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

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

380 381 382
/* Type declarations */

list1_type_decl:
383 384
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
385 386 387
;

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

396 397 398 399 400 401 402
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 } }
;

403
type_args:
404 405
| /* epsilon */                 { [] }
| quote_lident labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
406 407 408
;

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

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
427 428 429 430 431
;

equal_model:
| EQUAL { false }
| MODEL { true }
432 433 434
;

record_type:
435
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
436 437 438 439
;

list1_record_field:
| record_field                              { [$1] }
440
| list1_record_field SEMICOLON record_field { $3 :: $1 }
441 442
;

443 444 445 446 447 448 449 450
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

451
record_field:
452 453 454 455 456 457
| 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
458 459 460 461 462 463 464 465
;

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

typecase:
466
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
467 468 469 470
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
471 472 473 474 475 476 477 478 479 480
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 }
;

481
list1_logic_decl:
482 483
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
484 485
;

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

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

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

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

515 516 517
/* Inductive declarations */

list1_inductive_decl:
518 519
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
520 521 522
;

inductive_decl:
523
| lident_rich labels list0_param inddefn
524
  { { in_loc = floc (); in_ident = add_lab $1 $2;
525
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
526
;
527

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

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

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

542 543 544
/* Type expressions */

primitive_type:
545 546 547
| primitive_type_arg                  { $1 }
| lqualid primitive_type_args         { PPTtyapp ($1, $2) }
| primitive_type ARROW primitive_type { PPTarrow ($1, $3) }
548 549 550 551 552 553 554 555
;

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

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

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

575 576
/* Logic expressions */

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

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

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

644 645 646
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
647
;
648

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

654
lexpr_arg:
655
| qualid            { mk_pp (PPident $1) }
656 657 658 659
| lexpr_arg_noid    { $1 }
;

lexpr_arg_noid:
660 661 662 663 664
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
665
| quote_uident      { mk_pp (PPident (Qident $1)) }
666 667 668
;

lexpr_dot:
669
| lqualid_copy      { mk_pp (PPident $1) }
670 671
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
672 673 674
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
693 694 695 696 697 698
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

699
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
700

701 702 703 704
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
705

706 707 708 709 710 711 712 713 714 715 716 717 718 719 720
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 */
721

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

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

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

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

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

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
773 774
;

775
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
776

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

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

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

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 821 822
/* [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
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 853 854
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 }
855 856
;

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

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

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

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

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

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

anon_binder:
911
| UNDERSCORE    { floc (), None }
912 913
;

914 915 916 917 918
/* Idents */

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

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

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

lident_keyword:
| MODEL           { "model" }
;

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

946 947
/* Idents + symbolic operations' names */

948 949 950
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
951 952
;

953
lident_rich:
954 955 956 957 958
| lident        { $1 }
| lident_op_id  { $1 }
;

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

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

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

981
/* Qualified idents */
982

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

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

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

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

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

1009 1010
/* Theory/Module names */

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

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

/* Misc */

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