parser.mly 31.8 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 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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
  let model_label = Ident.create_label "model"

  let is_model_label l =
    match l with
    | Lpos _ -> false
    | Lstr lab ->
      lab = model_label

  let model_lab_present labels = 
    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
    | Lstr lab -> 
      try
	ignore(Str.search_forward model_trace_regexp lab.lab_string 0);
	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 =
    if (model_lab_present labels) && (not (model_trace_lab_present labels)) then 
      (Lstr (Ident.create_label ("model_trace:" ^ name)))::labels
    else
      labels  

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

81
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
82

83
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
84

85
86
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
87
88
89
  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)
90

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

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

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

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

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

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

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

140
141
142
143
144
  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
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
(* keywords *)
158

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
Andrei Paskevich's avatar
Andrei Paskevich committed
163
%token THEN THEORY TRUE TYPE USE WITH
164

165
(* program keywords *)
166

167
168
169
170
171
%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
172

173
(* symbols *)
174

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

%token EOF

186
(* program symbols *)
187

188
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
189

190
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
191

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

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

215
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
216

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

221
222
(* Theories, modules, namespaces *)

223
open_file:
224
225
(* Dummy token. Menhir does not accept epsilon. *)
| EOF { Incremental.open_file }
226

Andrei Paskevich's avatar
Andrei Paskevich committed
227
logic_file:
228
| theory* EOF   { Incremental.close_file () }
229

230
231
232
program_file:
| theory_or_module* EOF { Incremental.close_file () }

233
234
theory:
| theory_head theory_decl* END  { Incremental.close_theory () }
235

236
237
238
239
theory_or_module:
| theory                        { () }
| module_head module_decl* END  { Incremental.close_module () }

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

243
244
245
module_head:
| MODULE labels(uident)  { Incremental.open_module $2 }

246
247
248
249
250
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 }
251

252
253
254
255
256
257
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 }
258

259
260
261
namespace_head:
| NAMESPACE boption(IMPORT) uident
   { Incremental.open_namespace $3.id_str; $2 }
262

263
(* Use and clone *)
264

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

270
use:
271
| boption(IMPORT) tqualid
272
    { { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
273
274
| boption(IMPORT) tqualid AS uident
    { { use_theory = $2; use_import = Some ($1, $4.id_str) } }
275
276
| EXPORT tqualid
    { { use_theory = $2; use_import = None } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
277

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

288
289
290
ns:
| uqualid { Some $1 }
| DOT     { None }
291

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

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

(* Type declarations *)
317
318

type_decl:
319
| labels(lident) ty_var* typedefn
320
  { let model, vis, def, inv = $3 in
321
    let vis = if model then Abstract else vis in
322
323
324
    { 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
325

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

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

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

345
346
347
348
349
model:
| EQUAL         { false }
| MODEL         { true }

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

354
355
356
357
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 } }
358

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

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

369
(* Logic declarations *)
370

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

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

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

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

391
(* Inductive declarations *)
392
393

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

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

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

405
(* Type expressions *)
406

407
408
409
410
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
411

412
413
414
415
416
417
418
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 }
419

420
421
cast:
| COLON ty  { $2 }
422

423
(* Parameters and binders *)
424

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

431
params:  param*  { List.concat $1 }
432

433
binders: binder+ { List.concat $1 }
434
435
436

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

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

489
490
491
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
492

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

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

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

anon_binder:
520
521
| UNDERSCORE      { floc $startpos $endpos, None }

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
548
549
550
(* 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)
551
552
553
554
555
      | 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)
556
557
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
      | _ -> 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]) }
598
599
600
601
602
603
| 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]) }
604

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

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

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

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

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

626
627
628
629
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
630

631
632
633
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
634

635
(* Program declarations *)
636

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

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

(* Function declarations *)
651
652

type_v:
653
| arrow_type_v  { $1 }
654
| cast          { PTpure $1 }
655
656

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

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

simple_type_c:
664
665
666
| ty spec { PTpure $1, $2 }

(* Function definitions *)
667

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

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

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

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

687
expr: e = mk_expr(expr_) { e }
688
689
690

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

777
778
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
779
780

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

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

813
814
815
816
817
818
819
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 } }
820

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

824
825
val_expr:
| tail_type_c { Eany $1 }
826

827
828
829
%inline lazy_op:
| AMPAMP  { LazyAnd }
| BARBAR  { LazyOr }
830
831

assertion_kind:
832
833
834
| ASSERT  { Aassert }
| ASSUME  { Aassume }
| CHECK   { Acheck }
835
836

for_direction:
837
838
| TO      { To }
| DOWNTO  { Downto }
839

840
(* Specification *)
841

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

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

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

871
raises:
872
873
874
| uqualid ARROW term
    { $1, mk_pat (Ptuple []) $startpos($1) $endpos($1), $3 }
| uqualid pat_arg ARROW term