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
802
    { { empty_spec with sp_writes = $3; sp_checkrw = true } }
803
804
| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC
    { { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
805
806
| DIVERGES
    { { empty_spec with sp_diverge = true } }
807
808
| variant
    { { empty_spec with sp_variant = $1 } }
809

810
ensures:
811
| term
812
    { let id = mk_id "result" $startpos $endpos in
813
      [mk_pat (Pvar id) $startpos $endpos, $1] }
814

815
raises:
816
817
818
| uqualid ARROW term
    { $1, mk_pat (Ptuple []) $startpos($1) $endpos($1), $3 }
| uqualid pat_arg ARROW term
819
    { $1, $2, $4 }
820

821
xsymbol:
822
| uqualid
823
    { $1, mk_pat Pwild $startpos $endpos, mk_term Ttrue $startpos $endpos }
824