parser.mly 36.9 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 42
  let mk_pp_l loc d = { pp_loc = loc; pp_desc = d }
  let mk_pp d = { pp_loc = floc (); pp_desc = d }
Andrei Paskevich's avatar
Andrei Paskevich committed
43

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

/* keywords */

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

165 166
/* program keywords */

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

172 173
/* symbols */

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

%token EOF

185 186
/* program symbols */

187
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
188

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
214 215
/* Entry points */

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

224 225
open_file:
| /* epsilon */  { Incremental.open_file }
226 227
;

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

/* File, theory, namespace */
233

234 235 236
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
237 238
;

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

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

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

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

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

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

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

/* Declaration */

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

300 301 302 303 304
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

305 306
/* Use and clone */

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

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

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

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

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

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

349 350 351 352 353
ns:
| uqualid { Some $1 }
| DOT     { None }
;

354 355 356 357 358 359 360 361
/* Meta args */

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

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

371 372 373
/* Type declarations */

list1_type_decl:
374 375
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
376 377 378
;

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

387 388 389 390 391 392 393
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 } }
;

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

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

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
418 419 420 421 422
;

equal_model:
| EQUAL { false }
| MODEL { true }
423 424 425
;

record_type:
426
| LEFTBRC list1_record_field opt_semicolon RIGHTBRC { List.rev $2 }
427 428 429 430
;

list1_record_field:
| record_field                              { [$1] }
431
| list1_record_field SEMICOLON record_field { $3 :: $1 }
432 433
;

434 435 436 437 438 439 440 441
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

442
record_field:
443 444 445 446 447 448
| 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
449 450 451 452 453 454 455 456
;

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

typecase:
457
| uident labels list0_param   { (floc (), add_lab $1 $2, $3) }
458 459 460 461
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
462 463 464 465 466 467 468 469 470 471
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 }
;

472
list1_logic_decl:
473 474
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
475 476
;

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

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

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

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

506 507 508
/* Inductive declarations */

list1_inductive_decl:
509 510
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
511 512 513
;

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

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

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

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

533 534 535
/* Type expressions */

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

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

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

561 562 563 564
list2_primitive_type_sep_comma:
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

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

570 571
/* Logic expressions */

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

630 631 632 633 634 635 636 637 638
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

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

644
constant:
645 646
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
647 648
;

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

lexpr_dot:
660
| lqualid_copy      { mk_pp (PPident $1) }
661 662
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
663 664 665
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
684 685 686 687 688 689
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

690
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
691

692 693 694 695
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
696

697 698 699 700 701 702 703 704 705
list1_trigger_sep_bar:
| trigger                           { [$1] }
| trigger BAR list1_trigger_sep_bar { $1 :: $3 }
;

trigger:
| list1_lexpr_sep_comma { $1 }
;

706 707 708 709
list2_lexpr_sep_comma:
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

710 711 712 713 714 715
list1_lexpr_sep_comma:
| lexpr                             { [$1] }
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

/* Match expressions */
716

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

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

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

747
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
748 749 750
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
751

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

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
768 769
;

770
/* Binders */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
771

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

777
list1_param:
778 779
| param               { $1 }
| param list1_param   { $1 @ $2 }
780 781 782 783 784 785 786
;

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

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

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

852 853 854
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
855 856
;

857 858 859 860 861 862 863 864 865 866
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
867 868
;

869 870 871 872 873 874 875 876 877
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
878 879
;

880 881 882 883 884 885
list1_quant_vars:
| quant_vars                        { $1 }
| quant_vars COMMA list1_quant_vars { $1 @ $3 }
;

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

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

anon_binder:
906
| UNDERSCORE    { floc (), None }
907 908
;

909 910 911 912 913
/* Idents */

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

916 917 918 919 920 921 922 923 924 925 926 927 928
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

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

lident_keyword:
| MODEL           { "model" }
;

929 930 931 932 933 934 935 936 937 938 939 940
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 ()) }
;

941 942
/* Idents + symbolic operations' names */

943 944 945
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
946 947
;

948
lident_rich:
949 950 951 952 953
| lident        { $1 }
| lident_op_id  { $1 }
;

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

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

969
prefix_op:
970 971 972 973 974 975
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

976
/* Qualified idents */
977

978 979 980
qualid:
| ident_rich              { Qident $1 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }
981 982
;

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

lqualid:
989 990
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
991 992
;

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

999 1000 1001
uqualid:
| uident              { Qident $1 }
| uqualid DOT uident  { Qdot ($1, $3) }
1002 1003
;

1004 1005
/* Theory/Module names */

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

1011
any_qualid:
1012 1013 1014 1015 1016 1017 1018
| 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
1019
;
1020 1021 1022

/* Misc */

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

1028 1029 1030 1031 1032
labels:
| /* epsilon */ { [] }
| label labels  { $1 :: $2 }
;

1033 1034 1035
bar_:
| /* epsilon */ { () }
| BAR           { () }
1036 1037
;