parser.mly 31.9 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11 12

%{
13
module Increment = 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
32
  let mixfix s = "mixfix " ^ s
33

34
  let qualid_last = function Qident x | Qdot (_, x) -> x.id_str
35

36
  let floc s e = Loc.extract (s,e)
37

38
  let model_label = Ident.create_label "model"
39
  let model_projected = Ident.create_label "model_projected"
40 41 42 43 44

  let is_model_label l =
    match l with
    | Lpos _ -> false
    | Lstr lab ->
45 46
      (lab = model_label) || (lab = model_projected)

47

48
  let model_lab_present labels =
49 50 51 52 53 54 55 56 57 58 59
    try
      ignore(List.find is_model_label labels);
      true
    with Not_found ->
      false

  let model_trace_regexp = Str.regexp "model_trace:"

  let is_model_trace_label l =
    match l with
    | Lpos _ -> false
60
    | Lstr lab ->
61
      try
62
	ignore(Str.search_forward model_trace_regexp lab.Ident.lab_string 0);
63 64 65 66 67 68 69 70 71 72 73
	true
      with Not_found -> false

  let model_trace_lab_present labels =
    try
      ignore(List.find is_model_trace_label labels);
      true
    with Not_found ->
      false

  let add_model_trace name labels =
74
    if (model_lab_present labels) && (not (model_trace_lab_present labels)) then
75 76
      (Lstr (Ident.create_label ("model_trace:" ^ name)))::labels
    else
77
      labels
78 79 80 81

  let add_lab id l =
    let l = add_model_trace id.id_str l in
    { id with id_lab = l }
82

83
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
84

85
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
86

87 88
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
89 90 91
  let sub_op s e = Qident (mk_id (mixfix "[_.._]") s e)
  let above_op s e = Qident (mk_id (mixfix "[_..]") s e)
  let below_op s e = Qident (mk_id (mixfix "[.._]") s e)
92

93 94
  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 }
95
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
96

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

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

114 115 116 117
  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;
118
    sp_reads   = s1.sp_reads @ s2.sp_reads;
119 120
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
121 122
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
123
  }
124

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

131
  let small_integer i =
132
    try match i with
133 134 135 136
      | 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)
137
    with Failure _ -> raise Error
138

139 140
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
141

142 143 144 145 146
  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
147 148
%}

149
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
150

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

159
(* keywords *)
160

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

167
(* program keywords *)
168

169 170 171 172 173
%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
174

175
(* symbols *)
176

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

%token EOF

188
(* program symbols *)
189

190
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
191

192
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193

194
%nonassoc IN
195 196 197
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
198
%nonassoc prec_no_else
199
%nonassoc DOT ELSE GHOST
200
%nonassoc prec_named
201
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
202

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

217
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
218

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

223 224
(* Theories, modules, namespaces *)

225
open_file:
226
(* Dummy token. Menhir does not accept epsilon. *)
227
| EOF { Increment.open_file }
228

229
logic_file:
230
| theory* EOF   { Increment.close_file () }
231

232
program_file:
233
| theory_or_module* EOF { Increment.close_file () }
234

235
theory:
236
| theory_head theory_decl* END  { Increment.close_theory () }
237

238 239
theory_or_module:
| theory                        { () }
240
| module_head module_decl* END  { Increment.close_module () }
241

242
theory_head:
243
| THEORY labels(uident)  { Increment.open_theory $2 }
244

245
module_head:
246
| MODULE labels(uident)  { Increment.open_module $2 }
247

248
theory_decl:
249 250
| decl            { Increment.new_decl  (floc $startpos $endpos) $1 }
| use_clone       { Increment.use_clone (floc $startpos $endpos) $1 }
251
| namespace_head theory_decl* END
252
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
253

254
module_decl:
255 256 257
| decl            { Increment.new_decl  (floc $startpos $endpos) $1 }
| pdecl           { Increment.new_pdecl (floc $startpos $endpos) $1 }
| use_clone       { Increment.use_clone (floc $startpos $endpos) $1 }
258
| namespace_head module_decl* END
259
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
260

261 262
namespace_head:
| NAMESPACE boption(IMPORT) uident
263
   { Increment.open_namespace $3.id_str; $2 }
264

265
(* Use and clone *)
266

267
use_clone:
268 269 270
| USE use                                 { ($2, None) }
| CLONE use                               { ($2, Some []) }
| CLONE use WITH comma_list1(clone_subst) { ($2, Some $4) }
271

272
use:
273
| boption(IMPORT) tqualid
274
    { { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
275 276
| boption(IMPORT) tqualid AS uident
    { { use_theory = $2; use_import = Some ($1, $4.id_str) } }
277 278
| EXPORT tqualid
    { { use_theory = $2; use_import = None } }
279

280
clone_subst:
281 282
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
283 284 285 286 287 288
| 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) }
289

290 291 292
ns:
| uqualid { Some $1 }
| DOT     { None }
293

294 295 296 297 298 299 300 301 302 303 304 305 306 307
(* 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) }
308 309

meta_arg:
310 311 312 313 314 315 316
| 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) }
317 318

(* Type declarations *)
319 320

type_decl:
321
| labels(lident) ty_var* typedefn
322
  { let model, vis, def, inv = $3 in
323
    let vis = if model then Abstract else vis in
324 325 326
    { td_ident = $1; td_params = $2;
      td_model = model; td_vis = vis; td_def = def;
      td_inv = inv; td_loc = floc $startpos $endpos } }
327

328
late_invariant:
329
| labels(lident) ty_var* invariant+
330 331 332
  { { td_ident = $1; td_params = $2;
      td_model = false; td_vis = Public; td_def = TDabstract;
      td_inv = $3; td_loc = floc $startpos $endpos } }
333

334
ty_var:
335
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
336 337

typedefn:
338
| (* epsilon *)
339
    { false, Public, TDabstract, [] }
340
| model abstract bar_list1(type_case) invariant*
341
    { $1, $2, TDalgebraic $3, $4 }
342
| model abstract LEFTBRC semicolon_list1(type_field) RIGHTBRC invariant*
343
    { $1, $2, TDrecord $4, $6 }
344 345
| model abstract ty invariant*
    { $1, $2, TDalias $3, $4 }
346

347 348 349 350 351
model:
| EQUAL         { false }
| MODEL         { true }

abstract:
352
| (* epsilon *) { Public }
353 354
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
355

356 357 358 359
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 } }
360

361
field_modifiers:
362
| (* epsilon *) { false, false }
363 364 365 366 367
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

368
type_case:
369
| labels(uident) params { floc $startpos $endpos, $1, $2 }
370

371
(* Logic declarations *)
372

373 374
constant_decl:
| labels(lident_rich) cast preceded(EQUAL,term)?
375 376
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
377

378 379
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
380 381
  { { 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
382

383 384
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
385 386
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
387

388
with_logic_decl:
389
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
390 391
  { { 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
392

393
(* Inductive declarations *)
394 395

inductive_decl:
396
| labels(lident_rich) params ind_defn
397 398
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
399

400 401 402
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
403

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

407
(* Type expressions *)
408

409 410 411 412
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
413

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

422 423
cast:
| COLON ty  { $2 }
424

425
(* Parameters and binders *)
426

427 428
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
429 430
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
431 432
   names, whose type must be inferred. *)

433
params:  param*  { List.concat $1 }
434

435
binders: binder+ { List.concat $1 }
436 437 438

param:
| anon_binder
439 440 441 442 443 444 445 446
    { 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 _, []) ->
447 448
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
449
| LEFTPAR binder_vars_rest RIGHTPAR
450
    { match $2 with [l,_] -> error_param l
451
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
452
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
453
    { match $3 with [l,_] -> error_param l
454 455
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
456
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
457
| LEFTPAR GHOST binder_vars cast RIGHTPAR
458
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
459

460 461
binder:
| anon_binder
462 463 464 465 466
    { error_param (floc $startpos $endpos) }
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
467 468
             [floc $startpos $endpos, Some id, false, None]
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
469 470 471
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
472 473
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
474 475 476
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident id, []) ->
477 478 479
             let id = add_lab id ($2::$3) in
             [floc $startpos $endpos, Some id, false, None]
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
480
| LEFTPAR binder_vars_rest RIGHTPAR
481
    { match $2 with [l,i] -> [l, i, false, None]
482
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
483
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
484
    { match $3 with [l,i] -> [l, i, true, None]
485 486
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
487
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
488
| LEFTPAR GHOST binder_vars cast RIGHTPAR
489
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
490

491 492 493
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
494

495
binder_vars_rest:
496 497 498 499 500 501 502
| 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*
503
   { List.rev_append $1 ($2 :: $3) }
504
| anon_binder binder_var*
505
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
506

507
binder_vars_head:
508
| ty {
509 510
    let of_id id = id.id_loc, Some id in
    let push acc = function
511
      | PTtyapp (Qident id, []) -> of_id id :: acc
512
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
513
    match $1 with
514
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
515
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
516

517
binder_var:
518 519
| labels(lident)  { floc $startpos $endpos, Some $1 }
| anon_binder     { $1 }
520 521

anon_binder:
522 523
| UNDERSCORE      { floc $startpos $endpos, None }

524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552
(* 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)
553 554 555 556 557
      | Pcast ({pat_desc = Pvar id}, ty) ->
          Tlet (id, { $4 with term_desc = Tcast ($4, ty) }, $6)
      | Pcast ({pat_desc = Pwild}, ty) ->
          let id = id_anonymous $2.pat_loc in
          Tlet (id, { $4 with term_desc = Tcast ($4, ty) }, $6)
558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599
      | _ -> 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]) }
600 601 602 603 604 605
| term_arg LEFTSQ term DOTDOT term RIGHTSQ
    { Tidapp (sub_op $startpos($2) $endpos($2), [$1;$3;$5]) }
| term_arg LEFTSQ term DOTDOT RIGHTSQ
    { Tidapp (above_op $startpos($2) $endpos($2), [$1;$3]) }
| term_arg LEFTSQ DOTDOT term RIGHTSQ
    { Tidapp (below_op $startpos($2) $endpos($2), [$1;$4]) }
606

607 608
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
609

610 611
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
612

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

616 617 618
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
619

620 621 622 623 624 625 626
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
627

628 629 630 631
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
632

633 634 635
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
636

637
(* Program declarations *)
638

639
pdecl:
640
| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
641
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
642
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
643
| LET REC with_list1(rec_defn)                      { Drec $3 }
644 645
| EXCEPTION labels(uident)                          { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident) ty                       { Dexn ($2, $3) }
646

647 648 649 650 651 652
top_ghost:
| (* epsilon *) { Gnone  }
| GHOST         { Gghost }
| LEMMA         { Glemma }

(* Function declarations *)
653 654

type_v:
655
| arrow_type_v  { $1 }
656
| cast          { PTpure $1 }
657 658

arrow_type_v:
659
| param params tail_type_c  { PTfunc ($1 @ $2, $3) }
660 661

tail_type_c:
662 663
| single_spec spec arrow_type_v { $3, spec_union $1 $2 }
| COLON simple_type_c           { $2 }
664 665

simple_type_c:
666 667 668
| ty spec { PTpure $1, $2 }

(* Function definitions *)
669

670
rec_defn:
671
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
672
    { $2, $1, ($3, $4, $8, spec_union $5 $7) }
673

674
fun_defn:
675
| binders cast? spec EQUAL spec seq_expr { ($1, $2, $6, spec_union $3 $5) }
676

677
fun_expr:
678 679
| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }

680 681 682 683 684 685 686 687
(* 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 }
688

689
expr: e = mk_expr(expr_) { e }
690 691 692

expr_:
| expr_arg_
693 694
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
695
| NOT expr %prec prec_prefix_op
696
    { Enot $2 }
697
| prefix_op expr %prec prec_prefix_op
698 699 700 701 702 703 704 705
    { 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 }
706
| IF seq_expr THEN expr ELSE expr
707
    { Eif ($2, $4, $6) }
708
| IF seq_expr THEN expr %prec prec_no_else
709 710 711 712 713 714 715
    { 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 }
716
| LET top_ghost pattern EQUAL seq_expr IN seq_expr
717
    { match $3.pat_desc with
718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739
      | Pvar id -> Elet (id, $2, $5, $7)
      | Pwild -> Elet (id_anonymous $3.pat_loc, $2, $5, $7)
      | Ptuple [] -> Elet (id_anonymous $3.pat_loc, $2,
          { $5 with expr_desc = Ecast ($5, PTtuple []) }, $7)
      | Pcast ({pat_desc = Pvar id}, ty) ->
          Elet (id, $2, { $5 with expr_desc = Ecast ($5, ty) }, $7)
      | Pcast ({pat_desc = Pwild}, ty) ->
          let id = id_anonymous $3.pat_loc in
          Elet (id, $2, { $5 with expr_desc = Ecast ($5, ty) }, $7)
      | _ ->
          let e = match $2 with
            | Glemma -> Loc.errorm ~loc:($3.pat_loc)
                "`let lemma' cannot be used with complex patterns"
            | Gghost -> { $5 with expr_desc = Eghost $5 }
            | Gnone -> $5 in
          Ematch (e, [$3, $7]) }
| LET top_ghost labels(lident_op_id) EQUAL seq_expr IN seq_expr
    { Elet ($3, $2, $5, $7) }
| LET top_ghost labels(lident) fun_defn IN seq_expr
    { Efun ($3, $2, $4, $6) }
| LET top_ghost labels(lident_op_id) fun_defn IN seq_expr
    { Efun ($3, $2, $4, $6) }
740
| LET REC with_list1(rec_defn) IN seq_expr
741
    { Erec ($3, $5) }
742
| fun_expr
743 744 745 746 747 748 749
    { 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) }
750
| quote_uident COLON seq_expr
751
    { Emark ($1, $3) }
752
| LOOP loop_annotation seq_expr END
753
    { Eloop ($2, $3) }
754
| WHILE seq_expr DO loop_annotation seq_expr DONE
755 756 757
    { 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) }
758
| ABSURD
759
    { Eabsurd }
760
| RAISE uqualid
761
    { Eraise ($2, None) }
762
| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
763 764 765
    { Eraise ($3, Some $4) }
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
766
| ANY simple_type_c
767
    { Eany $2 }
768
| GHOST expr
769
    { Eghost $2 }
770
| ABSTRACT spec seq_expr END
771 772 773
    { Eabstract($3, $2) }
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
774
| label expr %prec prec_named
775 776 777
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
778

779 780
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
781 782

expr_arg_:
783 784 785 786 787 788 789 790 791 792 793
| 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 }
794 795

expr_sub:
796
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
797 798 799 800 801 802 803
| 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) }
804
| expr_arg LEFTSQ expr RIGHTSQ
805
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
806
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
807
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
808 809 810 811 812 813
| expr_arg LEFTSQ expr DOTDOT expr RIGHTSQ
    { Eidapp (sub_op $startpos($2) $endpos($2), [$1;$3;$5]) }
| expr_arg LEFTSQ expr DOTDOT RIGHTSQ
    { Eidapp (above_op $startpos($2) $endpos($2), [$1;$3]) }
| expr_arg LEFTSQ DOTDOT expr RIGHTSQ
    { Eidapp (below_op $startpos($2) $endpos($2), [$1;$4]) }
814

815 816 817 818 819 820 821
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 } }
822

823 824
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
825

826 827
val_expr:
| tail_type_c { Eany $1 }
828

829 830 831
%inline lazy_op:
| AMPAMP  { LazyAnd }
| BARBAR  { LazyOr }
832 833

assertion_kind:
834 835 836
| ASSERT  { Aassert }
| ASSUME  { Aassume }
| CHECK   { Acheck }
837 838

for_direction:
839 840
| TO      { To }
| DOWNTO  { Downto }
841

842
(* Specification *)
843

844
spec:
845
| (* epsilon *)     { empty_spec }
846
| single_spec spec  { spec_union $1 $2 }
847

848
single_spec:
849
| REQUIRES LEFTBRC term RIGHTBRC
850 851
    { { empty_spec with sp_pre = [$3] } }
| ENSURES LEFTBRC ensures RIGHTBRC
852
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
853
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
854 855 856 857
    { { 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
858
    { { empty_spec with sp_reads = $3; sp_checkrw = true } }
859
| WRITES LEFTBRC comma_list0(term) RIGHTBRC
860
    { { empty_spec with sp_writes = $3; sp_checkrw = true } }
861 862
| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC
    { { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
863 864
| DIVERGES
    { { empty_spec with sp_diverge = true } }
865 866
| variant
    { { empty_spec with sp_variant = $1 } }
867

868
ensures:
869
| term
870
    { let id = mk_id "result" $startpos $endpos in
871
      [mk_pat (Pvar id) $startpos $endpos, $1] }
872

873
raises:
874 875 876
| uqualid ARROW term
    { $1, mk_pat (Ptuple []) $startpos($1) $endpos($1), $3 }
| uqualid pat_arg ARROW term
877
    { $1, $2, $4 }
878

879
xsymbol: