parser.mly 33.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
/********************************************************************/
/*                                                                  */
/*  The Why3 Verification Platform   /   The Why3 Development Team  */
/*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  */
/*                                                                  */
/*  This software is distributed under the terms of the GNU Lesser  */
/*  General Public License version 2.1, with the special exception  */
/*  on linking described in file LICENSE.                           */
/*                                                                  */
/********************************************************************/
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11 12

%{
13
module Incremental = struct
14 15 16 17 18 19 20
  let stack = Stack.create ()
  let open_file inc = Stack.push inc stack
  let close_file () = ignore (Stack.pop stack)
  let open_theory id = (Stack.top stack).Ptree.open_theory id
  let close_theory () = (Stack.top stack).Ptree.close_theory ()
  let open_module id = (Stack.top stack).Ptree.open_module id
  let close_module () = (Stack.top stack).Ptree.close_module ()
21 22
  let open_namespace n = (Stack.top stack).Ptree.open_namespace n
  let close_namespace l b = (Stack.top stack).Ptree.close_namespace l b
23 24 25
  let new_decl loc d = (Stack.top stack).Ptree.new_decl loc d
  let new_pdecl loc d = (Stack.top stack).Ptree.new_pdecl loc d
  let use_clone loc use = (Stack.top stack).Ptree.use_clone loc use
26
end
27

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28 29 30
  open Ptree

  let loc () = (symbol_start_pos (), symbol_end_pos ())
31 32
  let floc () = Loc.extract (loc ())

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
33
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
34
  let floc_i i = Loc.extract (loc_i i)
35
(* dead code
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
36
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
37
  let floc_ij i j = Loc.extract (loc_ij i j)
38
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
39 40

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
41
  let mk_pp d = mk_ppl (floc ()) d
42
(* dead code
43
  let mk_pp_i i d = mk_ppl (floc_i i) d
44
*)
45
  let mk_pat p = { pat_loc = floc (); pat_desc = p }
Andrei Paskevich's avatar
Andrei Paskevich committed
46

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

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

53
  let infix  s = "infix "  ^ s
54
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
55
  let mixfix s = "mixfix " ^ s
56

57 58
  let quote id = { id with id = "'" ^ id.id }

59 60 61 62
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

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

Andrei Paskevich's avatar
Andrei Paskevich committed
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
  let mk_l_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
    mk_pp (PPapp (Qident id, [e1]))

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

  let mk_l_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
    mk_pp (PPapp (Qident id, [e1;e2]))

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

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

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

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

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

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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
119 120
  let exit_exn () = Qident (mk_id "%Exit" (floc ()))
  let id_anonymous () = mk_id "_" (floc ())
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
121
  let ty_unit () = PPTtuple []
122

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

127 128 129 130 131 132 133 134 135 136 137 138 139 140
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
    | _, _ -> Loc.errorm ~loc:(floc ())
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
    sp_reads   = [];
    sp_writes  = [];
    sp_variant = [];
  }
141

142 143 144 145 146 147 148
  let spec_union s1 s2 = {
    sp_pre     = s1.sp_pre @ s2.sp_pre;
    sp_post    = s1.sp_post @ s2.sp_post;
    sp_xpost   = s1.sp_xpost @ s2.sp_xpost;
    sp_reads   = s1.sp_reads @ s2.sp_reads;
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
149
  }
150

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

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

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

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

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

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

/* keywords */

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

188 189
/* program keywords */

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

195 196
/* symbols */

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

%token EOF

209 210
/* program symbols */

211
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
212

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

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

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

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

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

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

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

/* File, theory, namespace */
258

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

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

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

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

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

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

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

/* Declaration */

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

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

326 327
/* Use and clone */

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

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

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

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

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

subst:
359 360 361 362 363 364 365
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
| TYPE      qualid EQUAL qualid { CStsym (floc (), $2, $4) }
| CONSTANT  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| FUNCTION  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }
| LEMMA     qualid              { CSlemma (floc (), $2) }
| GOAL      qualid              { CSgoal  (floc (), $2) }
366 367
;

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

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

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

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

389 390 391
/* Type declarations */

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

type_decl:
397
| lident labels type_args typedefn
398
  { let model, vis, def, inv = $4 in
399
    let vis = if model then Abstract else vis in
400
    { td_loc = floc (); td_ident = add_lab $1 $2;
401 402
      td_params = $3; td_model = model;
      td_vis = vis; td_def = def; td_inv = inv } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
403 404
;

405 406 407 408 409 410 411
late_invariant:
| lident labels type_args invariant type_invariant
  { { td_loc = floc (); td_ident = add_lab $1 $2;
      td_params = $3; td_model = false;
      td_vis = Public; td_def = TDabstract; td_inv = $4::$5 } }
;

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

typedefn:
418
| /* epsilon */
419
    { false, Public, TDabstract, [] }
420
| equal_model visibility typecases type_invariant
421
    { $1, $2, TDalgebraic $3, $4 }
422
| equal_model visibility BAR typecases type_invariant
423
    { $1, $2, TDalgebraic $4, $5 }
424
| equal_model visibility record_type type_invariant
425
    { $1, $2, TDrecord $3, $4 }
426 427 428
/* abstract/private is not allowed for alias type */
| equal_model visibility primitive_type
    { if $2 <> Public then Loc.error ~loc:(floc_i 2) Parsing.Parse_error;
429
      $1, Public, TDalias $3, [] }
430 431 432 433 434 435
;

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

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

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

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

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

460
record_field:
461 462 463 464 465 466
| field_modifiers lident labels COLON primitive_type
   { { f_loc = floc ();
       f_ident = add_lab $2 $3;
       f_mutable = fst $1;
       f_ghost = snd $1;
       f_pty = $5 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
467 468 469 470 471 472 473 474
;

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

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

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
480 481 482 483 484 485 486 487 488 489
list1_logic_decl_function:
| logic_decl_function                        { [$1] }
| logic_decl_function WITH list1_logic_decl  { $1 :: $3 }
;

list1_logic_decl_predicate:
| logic_decl_predicate                        { [$1] }
| logic_decl_predicate WITH list1_logic_decl  { $1 :: $3 }
;

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

495 496 497 498 499 500
logic_decl_constant:
| lident_rich labels COLON primitive_type logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = []; ld_type = Some $4; ld_def = $5 } }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
501 502 503 504 505 506 507 508 509 510 511 512
logic_decl_function:
| lident_rich labels params COLON primitive_type logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;

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

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

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

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

529 530 531
/* Inductive declarations */

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

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

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

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

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

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

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

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

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

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

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

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

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

600 601
/* Logic expressions */

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

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

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

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

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

677
lexpr_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
678 679 680 681 682 683
| qualid            { mk_pp (PPvar $1) }
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
684
| QUOTE uident      { mk_pp (PPvar (Qident (quote $2))) }
Andrei Paskevich's avatar
Andrei Paskevich committed
685 686 687
;

lexpr_dot:
Andrei Paskevich's avatar
Andrei Paskevich committed
688 689 690
| lqualid_copy      { mk_pp (PPvar $1) }
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
691 692 693
;

lexpr_sub:
694
| lexpr_dot DOT lqualid_rich
Andrei Paskevich's avatar
Andrei Paskevich committed
695
   { mk_pp (PPapp ($3, [$1])) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
696 697
| LEFTPAR lexpr RIGHTPAR
   { $2 }
698 699 700 701
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
702
| LEFTBRC list1_field_value opt_semicolon RIGHTBRC
703
   { mk_pp (PPrecord (List.rev $2)) }
704
| LEFTBRC lexpr_arg WITH list1_field_value opt_semicolon RIGHTBRC
Andrei Paskevich's avatar
Andrei Paskevich committed
705
   { mk_pp (PPupdate ($2, List.rev $4)) }
706
| lexpr_arg LEFTSQ lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
707
   { mk_l_mixfix2 "[]" $1 $3 }
708
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
709
   { mk_l_mixfix3 "[<-]" $1 $3 $5 }
Andrei Paskevich's avatar
Andrei Paskevich committed
710
;
711

Andrei Paskevich's avatar
Andrei Paskevich committed
712 713 714 715
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
716 717
| FUNC    { PPfunc }
| PRED    { PPpred }
Andrei Paskevich's avatar
Andrei Paskevich committed
718 719
;

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

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

727 728 729 730 731 732 733 734 735 736 737 738 739 740 741
list1_trigger_sep_bar:
| trigger                           { [$1] }
| trigger BAR list1_trigger_sep_bar { $1 :: $3 }
;

trigger:
| list1_lexpr_sep_comma { $1 }
;

list1_lexpr_sep_comma:
| lexpr                             { [$1] }
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

/* Match expressions */
742

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

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

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
753 754 755 756 757 758 759 760 761 762 763 764 765 766 767
| pat_conj              { $1 }
| pat_conj BAR pattern  { mk_pat (PPpor ($1, $3)) }
;

pat_conj:
| pat_uni                      { $1 }
| pat_uni COMMA list1_pat_uni  { mk_pat (PPptuple ($1::$3)) }
;

list1_pat_uni:
| pat_uni                      { [$1] }
| pat_uni COMMA list1_pat_uni  { $1::$3 }
;

pat_uni:
768 769 770
| pat_arg                   { $1 }
| uqualid list1_pat_arg     { mk_pat (PPpapp ($1, $2)) }
| pat_uni AS lident labels  { mk_pat (PPpas ($1, add_lab $3 $4)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
771
;
772

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

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

pfields:
| pat_field opt_semicolon       { [$1] }
| pat_field SEMICOLON pfields   { $1::$3 }
;

pat_field:
| lqualid EQUAL pattern   { ($1, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
794 795
;

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

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

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

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

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

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

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

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

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

860 861 862 863 864
/* Idents */

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

Andrei Paskevich's avatar
Andrei Paskevich committed
867 868 869 870 871 872 873 874 875 876 877 878 879 880 881
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

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

lident_keyword:
| MODEL           { "model" }
;

/* Idents + symbolic operations' names */

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

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

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

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

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

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

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

lqualid:
Andrei Paskevich's avatar
Andrei Paskevich committed