parser.mly 29.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 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
181
(* Dummy token. Menhir does not accept epsilon. *)
| EOF { Incremental.open_file }
182

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

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

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

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

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

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

202
203
204
205
206
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 }
207

208
209
210
211
212
213
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 }
214

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

219
(* Use and clone *)
220

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

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

234
clone_subst:
235
236
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
237
238
239
240
241
242
| 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) }
243

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

248
249
250
251
252
253
254
255
256
257
258
259
260
261
(* 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) }
262
263

meta_arg:
264
265
266
267
268
269
270
| 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) }
271
272

(* Type declarations *)
273
274

type_decl:
275
| labels(lident) ty_var* typedefn
276
  { let model, vis, def, inv = $3 in
277
    let vis = if model then Abstract else vis in
278
279
280
    { 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
281

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

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

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

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

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

310
311
312
313
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 } }
314

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

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

325
(* Logic declarations *)
326

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

332
333
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
334
335
  { { 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
336

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

342
with_logic_decl:
343
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
344
345
  { { 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
346

347
(* Inductive declarations *)
348
349

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

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

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

361
(* Type expressions *)
362

363
364
365
366
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
367

368
369
370
371
372
373
374
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 }
375

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

379
(* Parameters and binders *)
380

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

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

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

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

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

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

449
binder_vars_rest:
450
451
452
453
454
455
456
| 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*
457
   { List.rev_append $1 ($2 :: $3) }
458
| anon_binder binder_var*
459
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
460

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

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

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

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
(* 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)
507
508
509
510
511
      | 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)
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
548
549
550
551
552
553
      | _ -> 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]) }
554

555
556
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
557

558
559
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
560

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

564
565
566
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
567

568
569
570
571
572
573
574
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
575

576
577
578
579
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
580

581
582
583
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
584

585
(* Program declarations *)
586

587
pdecl:
588
| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
589
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
590
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
591
| LET REC with_list1(rec_defn)                      { Drec $3 }
592
593
| EXCEPTION labels(uident)                          { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident) ty                       { Dexn ($2, $3) }
594

595
596
597
598
599
600
top_ghost:
| (* epsilon *) { Gnone  }
| GHOST         { Gghost }
| LEMMA         { Glemma }

(* Function declarations *)
601
602

type_v:
603
| arrow_type_v  { $1 }
604
| cast          { PTpure $1 }
605
606

arrow_type_v:
607
| param params tail_type_c  { PTfunc ($1 @ $2, $3) }
608
609

tail_type_c:
610
611
| single_spec spec arrow_type_v { $3, spec_union $1 $2 }
| COLON simple_type_c           { $2 }
612
613

simple_type_c:
614
615
616
| ty spec { PTpure $1, $2 }

(* Function definitions *)
617

618
rec_defn:
619
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
620
    { $2, $1, ($3, $4, $8, spec_union $5 $7) }
621

622
fun_defn:
623
| binders cast? spec EQUAL spec seq_expr { ($1, $2, $6, spec_union $3 $5) }
624

625
fun_expr:
626
627
| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }

628
629
630
631
632
633
634
635
(* 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 }
636

637
expr: e = mk_expr(expr_) { e }
638
639
640

expr_:
| expr_arg_
641
642
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
643
| NOT expr %prec prec_prefix_op
644
    { Enot $2 }
645
| prefix_op expr %prec prec_prefix_op
646
647
648
649
650
651
652
653
    { 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 }
654
| IF seq_expr THEN expr ELSE expr
655
    { Eif ($2, $4, $6) }
656
| IF seq_expr THEN expr %prec prec_no_else
657
658
659
660
661
662
663
    { 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 }
664
| LET top_ghost pattern EQUAL seq_expr IN seq_expr
665
    { match $3.pat_desc with
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
      | 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) }
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

825
invariant:
826
| INVARIANT LEFTBRC term RIGHTBRC { $3 }
827

828
variant:
829
| VARIANT LEFTBRC comma_list1(single_variant) RIGHTBRC { $3 }
830

831
single_variant:
832
| term preceded(WITH,lqualid)? { $1, $2 }
833