parser.mly 29.9 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2014   --   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
  open Ptree

30
  let infix  s = "infix "  ^ s
31
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
32
  let mixfix s = "mixfix " ^ s
33

34
  let qualid_last = function Qident x | Qdot (_, x) -> x.id_str
Andrei Paskevich's avatar
Andrei Paskevich committed
35

36
  let floc s e = Loc.extract (s,e)
Andrei Paskevich's avatar
Andrei Paskevich committed
37

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

40
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
41

42
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
43

44 45
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
46

47 48
  let mk_pat  d s e = { pat_desc  = d; pat_loc  = floc s e }
  let mk_term d s e = { term_desc = d; term_loc = floc s e }
49
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
50

51 52 53
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
54
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
55 56 57 58 59 60
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
61
    sp_reads   = [];
62 63
    sp_writes  = [];
    sp_variant = [];
64 65
    sp_checkrw = false;
    sp_diverge = false;
66
  }
67

68 69 70 71
  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;
72
    sp_reads   = s1.sp_reads @ s2.sp_reads;
73 74
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
75 76
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
77
  }
78

79
(* dead code
80
  let add_init_mark e =
81
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
82
    { e with expr_desc = Emark (init, e) }
83
*)
84

85
  let small_integer i =
86
    try match i with
87 88 89 90
      | 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)
91
    with Failure _ -> raise Error
92

93 94
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
95

96 97 98 99 100
  let error_loc loc = Loc.error ~loc Error

  let () = Exn_printer.register (fun fmt exn -> match exn with
    | Error -> Format.fprintf fmt "syntax error"
    | _ -> raise exn)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
101 102
%}

103
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104

105
%token <string> LIDENT UIDENT
106
%token <Ptree.integer_constant> INTEGER
107
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108 109
%token <Ptree.real_constant> FLOAT
%token <string> STRING
110
%token <Loc.position> POSITION
111
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
112

113
(* keywords *)
114

115
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
116 117 118
%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
119
%token THEN THEORY TRUE TYPE USE WITH
120

121
(* program keywords *)
122

123 124 125 126 127
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE
%token PRIVATE RAISE RAISES READS REC REQUIRES RETURNS
%token TO TRY VAL VARIANT WHILE WRITES
128

129
(* symbols *)
130

Andrei Paskevich's avatar
Andrei Paskevich committed
131
%token AND ARROW
132
%token BAR
133
%token COLON COMMA
134
%token DOT EQUAL LAMBDA LTGT
135
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
136
%token LARROW LRARROW OR
137
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
138
%token UNDERSCORE
139 140 141

%token EOF

142
(* program symbols *)
143

144
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
145

146
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
147

148
%nonassoc IN
149 150 151
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
152
%nonassoc prec_no_else
153
%nonassoc DOT ELSE GHOST
154
%nonassoc prec_named
155
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
156

Andrei Paskevich's avatar
Andrei Paskevich committed
157
%right ARROW LRARROW
158 159
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
160
%nonassoc NOT
161
%left EQUAL LTGT OP1
162
%nonassoc LARROW
163
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
164
%left OP2
165
%left OP3
166
%left OP4
167
%nonassoc prec_prefix_op
168 169
%nonassoc LEFTSQ
%nonassoc OPPREF
170

171
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
172

173 174
%start <Ptree.incremental -> unit> open_file
%start <unit> logic_file program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
175 176
%%

177 178
(* Theories, modules, namespaces *)

179
open_file:
180
| (* epsilon *) { Incremental.open_file }
181

Andrei Paskevich's avatar
Andrei Paskevich committed
182
logic_file:
183
| theory* EOF   { Incremental.close_file () }
184

185 186 187
program_file:
| theory_or_module* EOF { Incremental.close_file () }

188 189
theory:
| theory_head theory_decl* END  { Incremental.close_theory () }
190

191 192 193 194
theory_or_module:
| theory                        { () }
| module_head module_decl* END  { Incremental.close_module () }

195
theory_head:
196
| THEORY labels(uident)  { Incremental.open_theory $2 }
197

198 199 200
module_head:
| MODULE labels(uident)  { Incremental.open_module $2 }

201 202 203 204 205
theory_decl:
| decl            { Incremental.new_decl  (floc $startpos $endpos) $1 }
| use_clone       { Incremental.use_clone (floc $startpos $endpos) $1 }
| namespace_head theory_decl* END
    { Incremental.close_namespace (floc $startpos($1) $endpos($1)) $1 }
206

207 208 209 210 211 212
module_decl:
| decl            { Incremental.new_decl  (floc $startpos $endpos) $1 }
| pdecl           { Incremental.new_pdecl (floc $startpos $endpos) $1 }
| use_clone       { Incremental.use_clone (floc $startpos $endpos) $1 }
| namespace_head module_decl* END
    { Incremental.close_namespace (floc $startpos($1) $endpos($1)) $1 }
213

214 215 216
namespace_head:
| NAMESPACE boption(IMPORT) uident
   { Incremental.open_namespace $3.id_str; $2 }
217

218
(* Use and clone *)
219

220
use_clone:
221 222 223
| USE use                                 { ($2, None) }
| CLONE use                               { ($2, Some []) }
| CLONE use WITH comma_list1(clone_subst) { ($2, Some $4) }
224

225
use:
226
| boption(IMPORT) tqualid
227
    { { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
228 229
| boption(IMPORT) tqualid AS uident
    { { use_theory = $2; use_import = Some ($1, $4.id_str) } }
230 231
| EXPORT tqualid
    { { use_theory = $2; use_import = None } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
232

233
clone_subst:
234 235
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
236 237 238 239 240 241
| CONSTANT  qualid EQUAL qualid { CSfsym  (floc $startpos $endpos, $2,$4) }
| FUNCTION  qualid EQUAL qualid { CSfsym  (floc $startpos $endpos, $2,$4) }
| PREDICATE qualid EQUAL qualid { CSpsym  (floc $startpos $endpos, $2,$4) }
| VAL       qualid EQUAL qualid { CSvsym  (floc $startpos $endpos, $2,$4) }
| LEMMA     qualid              { CSlemma (floc $startpos $endpos, $2) }
| GOAL      qualid              { CSgoal  (floc $startpos $endpos, $2) }
242

243 244 245
ns:
| uqualid { Some $1 }
| DOT     { None }
246

247 248 249 250 251 252 253 254 255 256 257 258 259 260
(* Theory declarations *)

decl:
| TYPE with_list1(type_decl)                { Dtype $2 }
| TYPE late_invariant                       { Dtype [$2] }
| CONSTANT  constant_decl                   { Dlogic [$2] }
| FUNCTION  function_decl  with_logic_decl* { Dlogic ($2::$3) }
| PREDICATE predicate_decl with_logic_decl* { Dlogic ($2::$3) }
| INDUCTIVE   with_list1(inductive_decl)    { Dind (Decl.Ind, $2) }
| COINDUCTIVE with_list1(inductive_decl)    { Dind (Decl.Coind, $2) }
| AXIOM labels(ident) COLON term            { Dprop (Decl.Paxiom, $2, $4) }
| LEMMA labels(ident) COLON term            { Dprop (Decl.Plemma, $2, $4) }
| GOAL  labels(ident) COLON term            { Dprop (Decl.Pgoal, $2, $4) }
| META sident comma_list1(meta_arg)         { Dmeta ($2, $3) }
261 262

meta_arg:
263 264 265 266 267 268 269
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
| PROP      qualid  { Mpr $2 }
| STRING            { Mstr $1 }
| INTEGER           { Mint (small_integer $1) }
270 271

(* Type declarations *)
272 273

type_decl:
274
| labels(lident) ty_var* typedefn
275
  { let model, vis, def, inv = $3 in
276
    let vis = if model then Abstract else vis in
277 278 279
    { td_ident = $1; td_params = $2;
      td_model = model; td_vis = vis; td_def = def;
      td_inv = inv; td_loc = floc $startpos $endpos } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
280

281
late_invariant:
282
| labels(lident) ty_var* invariant+
283 284 285
  { { td_ident = $1; td_params = $2;
      td_model = false; td_vis = Public; td_def = TDabstract;
      td_inv = $3; td_loc = floc $startpos $endpos } }
286

287
ty_var:
288
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
289 290

typedefn:
291
| (* epsilon *)
292
    { false, Public, TDabstract, [] }
293
| model abstract bar_list1(type_case) invariant*
294
    { $1, $2, TDalgebraic $3, $4 }
295
| model abstract LEFTBRC semicolon_list1(type_field) RIGHTBRC invariant*
296
    { $1, $2, TDrecord $4, $6 }
297 298
| model abstract ty invariant*
    { $1, $2, TDalias $3, $4 }
299

300 301 302 303 304
model:
| EQUAL         { false }
| MODEL         { true }

abstract:
305
| (* epsilon *) { Public }
306 307
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
308

309 310 311 312
type_field:
| field_modifiers labels(lident) cast
  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
      f_pty = $3; f_loc = floc $startpos $endpos } }
313

314
field_modifiers:
315
| (* epsilon *) { false, false }
316 317 318 319 320
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

321
type_case:
322
| labels(uident) params { floc $startpos $endpos, $1, $2 }
323

324
(* Logic declarations *)
325

326 327
constant_decl:
| labels(lident_rich) cast preceded(EQUAL,term)?
328 329
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
330

331 332
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
333 334
  { { ld_ident = $1; ld_params = $2; ld_type = Some $3;
      ld_def = $4; ld_loc = floc $startpos $endpos } }
Andrei Paskevich's avatar
Andrei Paskevich committed
335

336 337
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
338 339
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
340

341
with_logic_decl:
342
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
343 344
  { { ld_ident = $2; ld_params = $3; ld_type = $4;
      ld_def = $5; ld_loc = floc $startpos $endpos } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
345

346
(* Inductive declarations *)
347 348

inductive_decl:
349
| labels(lident_rich) params ind_defn
350 351
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
352

353 354 355
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
356

357 358
ind_case:
| labels(ident) COLON term  { floc $startpos $endpos, $1, $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
359

360
(* Type expressions *)
361

362 363 364 365
ty:
| ty_arg          { $1 }
| lqualid ty_arg+ { PTtyapp ($1, $2) }
| ty ARROW ty     { PTarrow ($1, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
366

367 368 369 370 371 372 373
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
| quote_lident                      { PTtyvar ($1, false) }
| opaque_quote_lident               { PTtyvar ($1, true) }
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
374

375 376
cast:
| COLON ty  { $2 }
377

378
(* Parameters and binders *)
379

380 381
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
382 383
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
384 385
   names, whose type must be inferred. *)

386
params:  param*  { List.concat $1 }
387

388
binders: binder+ { List.concat $1 }
389 390 391

param:
| anon_binder
392 393 394 395 396 397 398 399
    { error_param (floc $startpos $endpos) }
| ty_arg
    { [floc $startpos $endpos, None, false, $1] }
| LEFTPAR GHOST ty RIGHTPAR
    { [floc $startpos $endpos, None, true, $3] }
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident _, []) ->
400 401
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
402
| LEFTPAR binder_vars_rest RIGHTPAR
403
    { match $2 with [l,_] -> error_param l
404
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
405
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
406
    { match $3 with [l,_] -> error_param l
407 408
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
409
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
410
| LEFTPAR GHOST binder_vars cast RIGHTPAR
411
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412

413 414
binder:
| anon_binder
415 416 417 418 419
    { error_param (floc $startpos $endpos) }
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
420 421
             [floc $startpos $endpos, Some id, false, None]
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
422 423 424
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
425 426
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
427 428 429
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident id, []) ->
430 431 432
             let id = add_lab id ($2::$3) in
             [floc $startpos $endpos, Some id, false, None]
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
433
| LEFTPAR binder_vars_rest RIGHTPAR
434
    { match $2 with [l,i] -> [l, i, false, None]
435
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
436
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
437
    { match $3 with [l,i] -> [l, i, true, None]
438 439
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
440
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
441
| LEFTPAR GHOST binder_vars cast RIGHTPAR
442
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
443

444 445 446
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
447

448
binder_vars_rest:
449 450 451 452 453 454 455
| binder_vars_head label label* binder_var*
    { List.rev_append (match $1 with
        | (l, Some id) :: bl ->
            let l3 = floc $startpos($3) $endpos($3) in
            (Loc.join l l3, Some (add_lab id ($2::$3))) :: bl
        | _ -> assert false) $4 }
| binder_vars_head anon_binder binder_var*
456
   { List.rev_append $1 ($2 :: $3) }
457
| anon_binder binder_var*
458
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
459

460
binder_vars_head:
461
| ty {
462 463
    let of_id id = id.id_loc, Some id in
    let push acc = function
464
      | PTtyapp (Qident id, []) -> of_id id :: acc
465
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
466
    match $1 with
467
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
468
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
469

470
binder_var:
471 472
| labels(lident)  { floc $startpos $endpos, Some $1 }
| anon_binder     { $1 }
473 474

anon_binder:
475 476
| UNDERSCORE      { floc $startpos $endpos, None }

477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547
(* Logical terms *)

mk_term(X): d = X { mk_term d $startpos $endpos }

term: t = mk_term(term_) { t }

term_:
| term_arg_
    { match $1 with (* break the infix relation chain *)
      | Tinfix (l,o,r) -> Tinnfix (l,o,r) | d -> d }
| NOT term
    { Tunop (Tnot, $2) }
| prefix_op term %prec prec_prefix_op
    { Tidapp (Qident $1, [$2]) }
| l = term ; o = bin_op ; r = term
    { Tbinop (l, o, r) }
| l = term ; o = infix_op ; r = term
    { Tinfix (l, o, r) }
| term_arg located(term_arg)+ (* FIXME/TODO: "term term_arg" *)
    { let join f (a,_,e) = mk_term (Tapply (f,a)) $startpos e in
      (List.fold_left join $1 $2).term_desc }
| IF term THEN term ELSE term
    { Tif ($2, $4, $6) }
| LET pattern EQUAL term IN term
    { match $2.pat_desc with
      | Pvar id -> Tlet (id, $4, $6)
      | Pwild -> Tlet (id_anonymous $2.pat_loc, $4, $6)
      | Ptuple [] -> Tlet (id_anonymous $2.pat_loc,
          { $4 with term_desc = Tcast ($4, PTtuple []) }, $6)
      | _ -> Tmatch ($4, [$2, $6]) }
| MATCH term WITH match_cases(term) END
    { Tmatch ($2, $4) }
| MATCH comma_list2(term) WITH match_cases(term) END
    { Tmatch (mk_term (Ttuple $2) $startpos($2) $endpos($2), $4) }
| quant comma_list1(quant_vars) triggers DOT term
    { Tquant ($1, List.concat $2, $3, $5) }
| EPSILON
    { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
| label term %prec prec_named
    { Tnamed ($1, $2) }
| term cast
    { Tcast ($1, $2) }

term_arg: mk_term(term_arg_) { $1 }
term_dot: mk_term(term_dot_) { $1 }

term_arg_:
| qualid                    { Tident $1 }
| numeral                   { Tconst $1 }
| TRUE                      { Ttrue }
| FALSE                     { Tfalse }
| quote_uident              { Tident (Qident $1) }
| o = oppref ; a = term_arg { Tidapp (Qident o, [a]) }
| term_sub_                 { $1 }

term_dot_:
| lqualid                   { Tident $1 }
| o = oppref ; a = term_dot { Tidapp (Qident o, [a]) }
| term_sub_                 { $1 }

term_sub_:
| term_dot DOT lqualid_rich                         { Tidapp ($3,[$1]) }
| LEFTPAR term RIGHTPAR                             { $2.term_desc }
| LEFTPAR RIGHTPAR                                  { Ttuple [] }
| LEFTPAR comma_list2(term) RIGHTPAR                { Ttuple $2 }
| LEFTBRC field_list1(term) RIGHTBRC                { Trecord $2 }
| LEFTBRC term_arg WITH field_list1(term) RIGHTBRC  { Tupdate ($2,$4) }
| term_arg LEFTSQ term RIGHTSQ
    { Tidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
| term_arg LEFTSQ term LARROW term RIGHTSQ
    { Tidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
548

549 550
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
551

552 553
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
554

555 556
quant_vars:
| binder_var+ cast? { List.map (fun (l,i) -> l, i, false, $2) $1 }
557

558 559 560
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
561

562 563 564 565 566 567 568
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
569

570 571 572 573
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
574

575 576 577
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
578

579
(* Program declarations *)
580

581
pdecl:
582
| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
583
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
584
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
585
| LET REC with_list1(rec_defn)                      { Drec $3 }
586 587
| EXCEPTION labels(uident)                          { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident) ty                       { Dexn ($2, $3) }
588

589 590 591 592 593 594
top_ghost:
| (* epsilon *) { Gnone  }
| GHOST         { Gghost }
| LEMMA         { Glemma }

(* Function declarations *)
595 596

type_v:
597
| arrow_type_v  { $1 }
598
| cast          { PTpure $1 }
599 600

arrow_type_v:
601
| param params tail_type_c  { PTfunc ($1 @ $2, $3) }
602 603

tail_type_c:
604 605
| single_spec spec arrow_type_v { $3, spec_union $1 $2 }
| COLON simple_type_c           { $2 }
606 607

simple_type_c:
608 609 610
| ty spec { PTpure $1, $2 }

(* Function definitions *)
611

612
rec_defn:
613
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
614
    { $2, $1, ($3, $4, $8, spec_union $5 $7) }
615

616
fun_defn:
617
| binders cast? spec EQUAL spec seq_expr { ($1, $2, $6, spec_union $3 $5) }
618

619
fun_expr:
620 621
| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }

622 623 624 625 626 627 628 629
(* Program expressions *)

mk_expr(X): d = X { mk_expr d $startpos $endpos }

seq_expr:
| expr %prec below_SEMI   { $1 }
| expr SEMICOLON          { $1 }
| expr SEMICOLON seq_expr { mk_expr (Esequence ($1, $3)) $startpos $endpos }
630

631
expr: e = mk_expr(expr_) { e }
632 633 634

expr_:
| expr_arg_
635 636
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
637
| NOT expr %prec prec_prefix_op
638
    { Enot $2 }
639
| prefix_op expr %prec prec_prefix_op
640 641 642 643 644 645 646 647
    { Eidapp (Qident $1, [$2]) }
| l = expr ; o = lazy_op ; r = expr
    { Elazy (l,o,r) }
| l = expr ; o = infix_op ; r = expr
    { Einfix (l,o,r) }
| expr_arg located(expr_arg)+ (* FIXME/TODO: "expr expr_arg" *)
    { let join f (a,_,e) = mk_expr (Eapply (f,a)) $startpos e in
      (List.fold_left join $1 $2).expr_desc }
648
| IF seq_expr THEN expr ELSE expr
649
    { Eif ($2, $4, $6) }
650
| IF seq_expr THEN expr %prec prec_no_else
651 652 653 654 655 656 657
    { Eif ($2, $4, mk_expr (Etuple []) $startpos $endpos) }
| expr LARROW expr
    { match $1.expr_desc with
      | Eidapp (q, [e1]) -> Eassign (e1, q, $3)
      | Eidapp (Qident id, [e1;e2]) when id.id_str = mixfix "[]" ->
          Eidapp (Qident {id with id_str = mixfix "[]<-"}, [e1;e2;$3])
      | _ -> raise Error }
658
| LET pattern EQUAL seq_expr IN seq_expr
659 660 661 662 663 664
    { match $2.pat_desc with
      | Pvar id -> Elet (id, Gnone, $4, $6)
      | Pwild -> Elet (id_anonymous $2.pat_loc, Gnone, $4, $6)
      | Ptuple [] -> Elet (id_anonymous $2.pat_loc, Gnone,
            { $4 with expr_desc = Ecast ($4, PTtuple []) }, $6)
      | _ -> Ematch ($4, [$2, $6]) }
665
| LET GHOST pat_arg EQUAL seq_expr IN seq_expr
666 667 668 669 670 671
    { match $3.pat_desc with
      | Pvar id -> Elet (id, Gghost, $5, $7)
      | Pwild -> Elet (id_anonymous $3.pat_loc, Gghost, $5, $7)
      | Ptuple [] -> Elet (id_anonymous $3.pat_loc, Gghost,
            { $5 with expr_desc = Ecast ($5, PTtuple []) }, $7)
      | _ -> Ematch ({ $5 with expr_desc = Eghost $5 }, [$3, $7]) }
672
| LET labels(lident) fun_defn IN seq_expr
673
    { Efun ($2, Gnone, $3, $5) }
674
| LET labels(lident_op_id) fun_defn IN seq_expr
675
    { Efun ($2, Gnone, $3, $5) }
676
| LET GHOST labels(lident) fun_defn IN seq_expr
677
    { Efun ($3, Gghost, $4, $6) }
678
| LET GHOST labels(lident_op_id) fun_defn IN seq_expr
679
    { Efun ($3, Gghost, $4, $6) }
680
| LET labels(lident_op_id) EQUAL seq_expr IN seq_expr
681
    { Elet ($2, Gnone, $4, $6) }
682
| LET GHOST labels(lident_op_id) EQUAL seq_expr IN seq_expr
683
    { Elet ($3, Gghost, $5, $7) }
684
| LET LEMMA labels(lident_rich) EQUAL seq_expr IN seq_expr
685
    { Elet ($3, Glemma, $5, $7) }
686
| LET LEMMA labels(lident_rich) fun_defn IN seq_expr
687
    { Efun ($3, Glemma, $4, $6) }
688
| LET REC with_list1(rec_defn) IN seq_expr
689
    { Erec ($3, $5) }
690
| fun_expr
691 692 693 694 695 696 697
    { Elam $1 }
| VAL top_ghost labels(lident_rich) mk_expr(val_expr) IN seq_expr
    { Elet ($3, $2, $4, $6) }
| MATCH seq_expr WITH match_cases(seq_expr) END
    { Ematch ($2, $4) }
| MATCH comma_list2(expr) WITH match_cases(seq_expr) END
    { Ematch (mk_expr (Etuple $2) $startpos($2) $endpos($2), $4) }
698
| quote_uident COLON seq_expr
699
    { Emark ($1, $3) }
700
| LOOP loop_annotation seq_expr END
701
    { Eloop ($2, $3) }
702
| WHILE seq_expr DO loop_annotation seq_expr DONE
703 704 705
    { Ewhile ($2, $4, $5) }
| FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
    { Efor ($2, $4, $5, $6, $8, $9) }
706
| ABSURD
707
    { Eabsurd }
708
| RAISE uqualid
709
    { Eraise ($2, None) }
710
| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
711 712 713
    { Eraise ($3, Some $4) }
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
714
| ANY simple_type_c
715
    { Eany $2 }
716
| GHOST expr
717
    { Eghost $2 }
718
| ABSTRACT spec seq_expr END
719 720 721
    { Eabstract($3, $2) }
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
722
| label expr %prec prec_named
723 724 725
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
726

727 728
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
729 730

expr_arg_:
731 732 733 734 735 736 737 738 739 740 741
| qualid                    { Eident $1 }
| numeral                   { Econst $1 }
| TRUE                      { Etrue }
| FALSE                     { Efalse }
| o = oppref ; a = expr_arg { Eidapp (Qident o, [a]) }
| expr_sub                  { $1 }

expr_dot_:
| lqualid                   { Eident $1 }
| o = oppref ; a = expr_dot { Eidapp (Qident o, [a]) }
| expr_sub                  { $1 }
742 743

expr_sub:
744
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
745 746 747 748 749 750 751
| BEGIN seq_expr END                                { $2.expr_desc }
| LEFTPAR seq_expr RIGHTPAR                         { $2.expr_desc }
| BEGIN END                                         { Etuple [] }
| LEFTPAR RIGHTPAR                                  { Etuple [] }
| LEFTPAR comma_list2(expr) RIGHTPAR                { Etuple $2 }
| LEFTBRC field_list1(expr) RIGHTBRC                { Erecord $2 }
| LEFTBRC expr_arg WITH field_list1(expr) RIGHTBRC  { Eupdate ($2, $4) }
752
| expr_arg LEFTSQ expr RIGHTSQ
753
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
754
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
755
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
756

757 758 759 760 761 762 763
loop_annotation:
| (* epsilon *)
    { { loop_invariant = []; loop_variant = [] } }
| invariant loop_annotation
    { let a = $2 in { a with loop_invariant = $1 :: a.loop_invariant } }
| variant loop_annotation
    { let a = $2 in { a with loop_variant = variant_union $1 a.loop_variant } }
764

765 766
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
767

768 769
val_expr:
| tail_type_c { Eany $1 }
770

771 772 773
%inline lazy_op:
| AMPAMP  { LazyAnd }
| BARBAR  { LazyOr }
774 775

assertion_kind:
776 777 778
| ASSERT  { Aassert }
| ASSUME  { Aassume }
| CHECK   { Acheck }
779 780

for_direction:
781 782
| TO      { To }
| DOWNTO  { Downto }
783

784
(* Specification *)
785

786
spec:
787
| (* epsilon *)     { empty_spec }
788
| single_spec spec  { spec_union $1 $2 }
789

790
single_spec:
791
| REQUIRES LEFTBRC term RIGHTBRC
792 793
    { { empty_spec with sp_pre = [$3] } }
| ENSURES LEFTBRC ensures RIGHTBRC
794
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
795
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
796 797 798 799
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
| RAISES LEFTBRC bar_list1(raises) RIGHTBRC
    { { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
| READS  LEFTBRC comma_list0(lqualid) RIGHTBRC
800
    { { empty_spec with sp_reads = $3; sp_checkrw = true } }
801
| WRITES LEFTBRC comma_list0(term) RIGHTBRC