Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

parser.mly 29.7 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
14

%{
  open Ptree

15
  let infix  s = "infix "  ^ s
16
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
17
  let mixfix s = "mixfix " ^ s
18

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

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

23
  let add_lab id l = { id with id_lab = l }
24

25
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
26

27
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
28

29
30
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
31
32
33
  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)
34

35
36
  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 }
37
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
38

39
40
41
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
42
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
43
44
45
46
47
48
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
49
    sp_reads   = [];
50
51
    sp_writes  = [];
    sp_variant = [];
52
53
    sp_checkrw = false;
    sp_diverge = false;
54
  }
55

56
57
58
59
  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;
60
    sp_reads   = s1.sp_reads @ s2.sp_reads;
61
62
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
63
64
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
65
  }
66

67
(* dead code
68
  let add_init_mark e =
69
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
70
    { e with expr_desc = Emark (init, e) }
71
*)
72

73
  let small_integer i =
74
    try match i with
75
76
77
78
      | 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)
79
    with Failure _ -> raise Error
80

81
82
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
83

84
85
86
87
88
  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
89
90
%}

91
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
92

93
%token <string> LIDENT UIDENT
94
%token <Ptree.integer_constant> INTEGER
95
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96
97
%token <Ptree.real_constant> FLOAT
%token <string> STRING
98
%token <Loc.position> POSITION
99
%token <string> QUOTE_UIDENT QUOTE_LIDENT
100

101
(* keywords *)
102

103
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
104
105
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
106
%token LET MATCH META NOT PREDICATE PROP SCOPE
Andrei Paskevich's avatar
Andrei Paskevich committed
107
%token THEN THEORY TRUE TYPE USE WITH
108

109
(* program keywords *)
110

111
112
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
113
%token FUN GHOST INVARIANT LOOP MODULE MUTABLE
114
115
%token PRIVATE RAISE RAISES READS REC REQUIRES RETURNS
%token TO TRY VAL VARIANT WHILE WRITES
116

117
(* symbols *)
118

Andrei Paskevich's avatar
Andrei Paskevich committed
119
%token AND ARROW
120
%token BAR
121
%token COLON COMMA
122
%token DOT DOTDOT EQUAL LTGT
123
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
124
%token LARROW LRARROW OR
125
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
126
%token UNDERSCORE
127
128
129

%token EOF

130
(* program symbols *)
131

132
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
133

134
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
135

136
%nonassoc IN
137
138
139
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
140
%nonassoc prec_no_else
141
%nonassoc DOT ELSE GHOST
142
%nonassoc prec_named
143
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
144

Andrei Paskevich's avatar
Andrei Paskevich committed
145
%right ARROW LRARROW
146
147
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
148
%nonassoc NOT
149
%left EQUAL LTGT OP1
150
%nonassoc LARROW
151
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
152
%left OP2
153
%left OP3
154
%left OP4
155
%nonassoc prec_prefix_op
156
157
%nonassoc LEFTSQ
%nonassoc OPPREF
158

159
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
160

161
%start <Pmodule.pmodule Stdlib.Mstr.t> mlw_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
162
163
%%

164
165
(* Theories, modules, namespaces *)

166
167
168
169
170
mlw_file:
| theory_or_module* EOF { Typing.close_file () }
(* TODO
| module_decl* EOF { Typing.close_file () }
*)
171

172
theory_or_module:
173
174
| module_head module_decl* END
    { Typing.close_module (floc $startpos($3) $endpos($3)) }
175

176
module_head:
177
178
| THEORY labels(uident)  { Typing.open_module $2 ~theory:true  }
| MODULE labels(uident)  { Typing.open_module $2 ~theory:false }
179

180
module_decl:
181
182
| decl            { Typing.add_decl  (floc $startpos $endpos) $1 }
| use_clone       { Typing.use_clone (floc $startpos $endpos) $1 }
183
| namespace_head module_decl* END
184
    { Typing.close_namespace (floc $startpos($1) $endpos($1)) ~import:$1 }
185

186
namespace_head:
187
| SCOPE boption(IMPORT) uident  { Typing.open_namespace $3; $2 }
188

189
(* Use and clone *)
190

191
use_clone:
192
193
194
| USE use                                 { ($2, None) }
| CLONE use                               { ($2, Some []) }
| CLONE use WITH comma_list1(clone_subst) { ($2, Some $4) }
195

196
use:
197
| boption(IMPORT) tqualid
Andrei Paskevich's avatar
Andrei Paskevich committed
198
    { { use_module = $2; use_import = Some ($1, qualid_last $2) } }
199
| boption(IMPORT) tqualid AS uident
Andrei Paskevich's avatar
Andrei Paskevich committed
200
    { { use_module = $2; use_import = Some ($1, $4.id_str) } }
201
| EXPORT tqualid
Andrei Paskevich's avatar
Andrei Paskevich committed
202
    { { use_module = $2; use_import = None } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
203

204
clone_subst:
205
| SCOPE     ns     EQUAL ns     { CSns    (floc $startpos $endpos, $2,$4) }
206
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
207
208
209
210
211
212
| 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) }
213

214
215
216
ns:
| uqualid { Some $1 }
| DOT     { None }
217

218
219
220
221
222
223
224
225
226
227
228
229
230
(* Theory declarations *)

decl:
| TYPE with_list1(type_decl)                { 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) }
231
| pdecl                                     { $1 }
232
233

meta_arg:
234
235
236
237
238
239
240
| 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) }
241
242

(* Type declarations *)
243
244

type_decl:
245
246
| labels(lident) ty_var* typedefn invariant*
  { let (vis, mut), def = $3 in
247
    { td_ident = $1; td_params = $2;
248
249
250
      td_vis = vis; td_mut = mut;
      td_inv = $4; td_def = def;
      td_loc = floc $startpos $endpos } }
251

252
ty_var:
253
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
254

255
256
257
258
259
260
261
262
(* TODO: should global "mutable" imply "private"?
  "type t 'a = mutable { x : int }"
    - if "x" is immutable then the type can only be private
    - if "x" is automatically mutable then I don't like it
    - if there are known mutable fields, then a global "mutable"
      is redundant, unless it also means "private" *)
(* TODO: what should be the syntax for mutable private records
    without known fields? *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
263
typedefn:
264
| (* epsilon *)
265
266
267
268
269
270
271
272
273
274
275
276
277
278
    { (Public, false), TDabstract }
| EQUAL vis_mut bar_list1(type_case)
    { $2, TDalgebraic $3 }
| EQUAL vis_mut LEFTBRC semicolon_list1(type_field) RIGHTBRC
    { $2, TDrecord $4 }
| EQUAL vis_mut ty
    { $2, TDalias $3 }

vis_mut:
| (* epsilon *)     { Public, false }
| MUTABLE           { Public, true  }
| abstract          { $1, false }
| abstract MUTABLE  { $1, true }
| MUTABLE abstract  { $2, true }
279
280

abstract:
281
282
| PRIVATE           { Private }
| ABSTRACT          { Abstract }
283

284
285
286
287
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 } }
288

289
field_modifiers:
290
| (* epsilon *) { false, false }
291
292
293
294
295
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

296
type_case:
297
| labels(uident) params { floc $startpos $endpos, $1, $2 }
298

299
(* Logic declarations *)
300

301
302
constant_decl:
| labels(lident_rich) cast preceded(EQUAL,term)?
303
304
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
305

306
307
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
308
309
  { { 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
310

311
312
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
313
314
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
315

316
with_logic_decl:
317
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
318
319
  { { 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
320

321
(* Inductive declarations *)
322
323

inductive_decl:
324
| labels(lident_rich) params ind_defn
325
326
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
327

328
329
330
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331

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

335
(* Type expressions *)
336

337
338
339
340
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
341

342
343
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
344
| quote_lident                      { PTtyvar $1 }
345
346
347
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
348

349
350
cast:
| COLON ty  { $2 }
351

352
(* Parameters and binders *)
353

354
355
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
356
357
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
358
359
   names, whose type must be inferred. *)

360
params:  param*  { List.concat $1 }
361

362
binders: binder+ { List.concat $1 }
363
364
365

param:
| anon_binder
366
367
368
369
370
371
372
373
    { 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 _, []) ->
374
375
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
376
| LEFTPAR binder_vars_rest RIGHTPAR
377
    { match $2 with [l,_] -> error_param l
378
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
379
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
380
    { match $3 with [l,_] -> error_param l
381
382
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
383
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
384
| LEFTPAR GHOST binder_vars cast RIGHTPAR
385
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
386

387
388
binder:
| anon_binder
389
390
391
392
393
    { error_param (floc $startpos $endpos) }
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
394
395
             [floc $startpos $endpos, Some id, false, None]
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
396
397
398
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
399
400
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
401
402
403
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident id, []) ->
404
405
406
             let id = add_lab id ($2::$3) in
             [floc $startpos $endpos, Some id, false, None]
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
407
| LEFTPAR binder_vars_rest RIGHTPAR
408
    { match $2 with [l,i] -> [l, i, false, None]
409
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
410
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
411
    { match $3 with [l,i] -> [l, i, true, None]
412
413
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
414
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
415
| LEFTPAR GHOST binder_vars cast RIGHTPAR
416
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
417

418
419
420
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
421

422
binder_vars_rest:
423
424
425
426
427
428
429
| 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*
430
   { List.rev_append $1 ($2 :: $3) }
431
| anon_binder binder_var*
432
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
433

434
binder_vars_head:
435
| ty {
436
437
    let of_id id = id.id_loc, Some id in
    let push acc = function
438
      | PTtyapp (Qident id, []) -> of_id id :: acc
439
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
440
    match $1 with
441
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
442
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
443

444
binder_var:
445
446
| labels(lident)  { floc $startpos $endpos, Some $1 }
| anon_binder     { $1 }
447
448

anon_binder:
449
450
| UNDERSCORE      { floc $startpos $endpos, None }

451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
(* 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)
480
481
482
483
484
      | 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)
485
      | _ -> Tmatch ($4, [$2, $6]) }
486
487
488
489
490
491
| LET labels(lident_op_id) EQUAL term IN term
    { Tlet ($2, $4, $6) }
| LET labels(lident) mk_term(lam_defn) IN term
    { Tlet ($2, $3, $5) }
| LET labels(lident_op_id) mk_term(lam_defn) IN term
    { Tlet ($2, $3, $5) }
492
493
494
495
496
497
| 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) }
498
499
| FUN binders ARROW term
    { Tquant (Tlambda, $2, [], $4) }
500
501
502
503
504
505
506
| EPSILON
    { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
| label term %prec prec_named
    { Tnamed ($1, $2) }
| term cast
    { Tcast ($1, $2) }

507
508
509
lam_defn:
| binders EQUAL term  { Tquant (Tlambda, $1, [], $3) }

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
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]) }
538
539
540
541
542
543
| 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]) }
544

545
546
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
547

548
549
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
550

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

554
555
556
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
557

558
559
560
561
562
563
564
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
565

566
567
568
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
569

570
571
572
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
573

574
(* Program declarations *)
575

576
pdecl:
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
| VAL ghost kind labels(lident_rich) mk_expr(val_defn) { Dlet ($4, $2, $3, $5) }
| LET ghost kind labels(lident_rich) mk_expr(fun_defn) { Dlet ($4, $2, $3, $5) }
| LET ghost kind labels(lident_rich) EQUAL expr        { Dlet ($4, $2, $3, $6) }
| LET REC with_list1(rec_defn)                         { Drec $3 }
| EXCEPTION labels(uident)                             { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident) ty                          { Dexn ($2, $3) }

ghost:
| (* epsilon *) { false }
| GHOST         { true }

kind:
| (* epsilon *) { Expr.RKnone }
| FUNCTION      { Expr.RKfunc }
| CONSTANT      { Expr.RKfunc }
| PREDICATE     { Expr.RKpred }
| LEMMA         { Expr.RKlemma }
594
595

(* Function definitions *)
596

597
rec_defn:
598
599
| ghost kind labels(lident_rich) binders cast? spec EQUAL spec seq_expr
    { $3, $1, $2, $4, $5, spec_union $6 $8, $9 }
600

601
fun_defn:
602
| binders cast? spec EQUAL spec seq_expr
603
    { Efun ($1, $2, spec_union $3 $5, $6) }
604

605
606
val_defn:
| params cast spec  { Eany ($1, $2, $3) }
607

608
609
610
611
612
613
614
615
(* 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 }
616

617
expr: e = mk_expr(expr_) { e }
618
619
620

expr_:
| expr_arg_
621
622
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
623
624
625
626
| expr AMPAMP expr
    { Eand ($1, $3) }
| expr BARBAR expr
    { Eor ($1, $3) }
627
| NOT expr %prec prec_prefix_op
628
    { Enot $2 }
629
| prefix_op expr %prec prec_prefix_op
630
631
632
633
634
635
    { Eidapp (Qident $1, [$2]) }
| 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 }
636
| IF seq_expr THEN expr ELSE expr
637
    { Eif ($2, $4, $6) }
638
| IF seq_expr THEN expr %prec prec_no_else
639
640
641
642
643
644
645
    { 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 }
646
647
648
649
650
651
| LET ghost kind pattern EQUAL seq_expr IN seq_expr
    { match $4.pat_desc with
      | Pvar id -> Elet (id, $2, $3, $6, $8)
      | Pwild -> Elet (id_anonymous $4.pat_loc, $2, $3, $6, $8)
      | Ptuple [] -> Elet (id_anonymous $4.pat_loc, $2, $3,
          { $6 with expr_desc = Ecast ($6, PTtuple []) }, $8)
652
      | Pcast ({pat_desc = Pvar id}, ty) ->
653
          Elet (id, $2, $3, { $6 with expr_desc = Ecast ($6, ty) }, $8)
654
      | Pcast ({pat_desc = Pwild}, ty) ->
655
656
          let id = id_anonymous $4.pat_loc in
          Elet (id, $2, $3, { $6 with expr_desc = Ecast ($6, ty) }, $8)
657
      | _ ->
658
659
660
661
662
663
664
665
666
667
668
          let e = if $2 then { $6 with expr_desc = Eghost $6 } else $6 in
          (match $3 with
          | Expr.RKnone -> Ematch (e, [$4, $8])
          | _ -> Loc.errorm ~loc:($4.pat_loc)
              "`let <kind>' cannot be used with complex patterns") }
| LET ghost kind labels(lident_op_id) EQUAL seq_expr IN seq_expr
    { Elet ($4, $2, $3, $6, $8) }
| LET ghost kind labels(lident) mk_expr(fun_defn) IN seq_expr
    { Elet ($4, $2, $3, $5, $7) }
| LET ghost kind labels(lident_op_id) mk_expr(fun_defn) IN seq_expr
    { Elet ($4, $2, $3, $5, $7) }
669
| LET REC with_list1(rec_defn) IN seq_expr
670
    { Erec ($3, $5) }
671
| FUN binders spec ARROW spec seq_expr
672
673
674
    { Efun ($2, None, spec_union $3 $5, $6) }
| ABSTRACT spec seq_expr END
    { Efun ([], None, $2, $3) }
675
676
| ANY ty spec
    { Eany ([], $2, $3) }
677
678
| VAL ghost kind labels(lident_rich) mk_expr(val_defn) IN seq_expr
    { Elet ($4, $2, $3, $5, $7) }
679
680
681
682
| 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) }
683
| quote_uident COLON seq_expr
684
    { Emark ($1, $3) }
685
| LOOP loop_annotation seq_expr END
686
    { let inv, var = $2 in Eloop (inv, var, $3) }
687
| WHILE seq_expr DO loop_annotation seq_expr DONE
688
    { let inv, var = $4 in Ewhile ($2, inv, var, $5) }
689
690
| FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
    { Efor ($2, $4, $5, $6, $8, $9) }
691
| ABSURD
692
    { Eabsurd }
693
| RAISE uqualid
694
    { Eraise ($2, None) }
695
| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
696
697
698
    { Eraise ($3, Some $4) }
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
699
| GHOST expr
700
701
702
    { Eghost $2 }
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
703
| label expr %prec prec_named
704
705
706
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
707

708
709
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
710
711

expr_arg_:
712
713
714
715
716
717
718
719
720
721
722
| 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 }
723
724

expr_sub:
725
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
726
727
728
729
730
731
732
| 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) }
733
| expr_arg LEFTSQ expr RIGHTSQ
734
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
735
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
736
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
737
738
739
740
741
742
| 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]) }
743

744
745
loop_annotation:
| (* epsilon *)
746
    { [], [] }
747
| invariant loop_annotation
748
    { let inv, var = $2 in $1 :: inv, var }
749
| variant loop_annotation
750
    { let inv, var = $2 in inv, variant_union $1 var }
751

752
753
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
754
755

assertion_kind:
756
757
758
| ASSERT  { Expr.Assert }
| ASSUME  { Expr.Assume }
| CHECK   { Expr.Check }
759
760

for_direction:
761
762
| TO      { Expr.To }
| DOWNTO  { Expr.DownTo }
763

764
(* Specification *)
765

766
spec:
767
| (* epsilon *)     { empty_spec }
768
| single_spec spec  { spec_union $1 $2 }
769

770
single_spec:
771
| REQUIRES LEFTBRC term RIGHTBRC
772
773
    { { empty_spec with sp_pre = [$3] } }
| ENSURES LEFTBRC ensures RIGHTBRC
774
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
775
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
776
777
778
779
    { { 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
780
    { { empty_spec with sp_reads = $3; sp_checkrw = true } }
781
| WRITES LEFTBRC comma_list0(term) RIGHTBRC
782
    { { empty_spec with sp_writes = $3; sp_checkrw = true } }
783
784
| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC
    { { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
785
786
| DIVERGES
    { { empty_spec with sp_diverge = true } }
787
788
| variant
    { { empty_spec with sp_variant = $1 } }
789

790
ensures:
791
| term
792
    { let id = mk_id "result" $startpos $endpos in
793
      [mk_pat (Pvar id) $startpos $endpos, $1] }
794

795
raises:
796
797
798
| uqualid ARROW term
    { $1, mk_pat (Ptuple []) $startpos($1) $endpos($1), $3 }
| uqualid pat_arg ARROW term
799
    { $1, $2, $4 }
800

801
xsymbol:
802
| uqualid
803
    { $1, mk_pat Pwild $startpos $endpos, mk_term Ttrue $startpos $endpos }
804

805
invariant:
806
| INVARIANT LEFTBRC term RIGHTBRC { $3 }
807

808
variant:
809
| VARIANT LEFTBRC comma_list1(single_variant) RIGHTBRC { $3 }
810

811
single_variant:
812
| term preceded(WITH,lqualid)? { $1, $2 }
813

814
(* Patterns *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
815

816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
mk_pat(X): X { mk_pat $1 $startpos $endpos }

pattern: mk_pat(pattern_) { $1 }
pat_arg: mk_pat(pat_arg_) { $1 }

pattern_:
| pat_conj_                             { $1 }
| mk_pat(pat_conj_) BAR pattern         { Por ($1,$3) }

pat_conj_:
| pat_uni_                              { $1 }
| comma_list2(mk_pat(pat_uni_))         { Ptuple $1 }

pat_uni_:
| pat_arg_                              { $1 }
| uqualid pat_arg+                      { Papp ($1,$2) }
| mk_pat(pat_uni_) AS labels(lident)    { Pas ($1,$3) }
833
| mk_pat(pat_uni_) cast                 { Pcast($1,$2) }
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882

pat_arg_:
| UNDERSCORE                            { Pwild }
| labels(lident)                        { Pvar $1 }
| uqualid                               { Papp ($1,[]) }
| LEFTPAR RIGHTPAR                      { Ptuple [] }
| LEFTPAR pattern_ RIGHTPAR             { $2 }
| LEFTBRC field_list1(pattern) RIGHTBRC { Prec $2 }

(* Idents *)

ident:
| uident { $1 }
| lident { $1 }

uident:
| UIDENT          { mk_id $1 $startpos $endpos }

lident:
| LIDENT          { mk_id $1 $startpos $endpos }

quote_uident:
| QUOTE_UIDENT  { mk_id ("'" ^ $1) $startpos $endpos }

quote_lident:
| QUOTE_LIDENT  { mk_id $1 $startpos $endpos }

(* Idents + symbolic operation names *)

ident_rich:
| uident        { $1 }
| lident_rich   { $1 }

lident_rich:
| lident        { $1 }
| lident_op_id  { $1 }

lident_op_id:
| LEFTPAR lident_op RIGHTPAR  { mk_id $2 $startpos $endpos }
| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") $startpos $endpos }

lident_op:
| op_symbol               { infix $1 }
| op_symbol UNDERSCORE    { prefix $1 }
| EQUAL                   { infix "=" }
| OPPREF                  { prefix $1 }
| LEFTSQ RIGHTSQ          { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ   { mixfix "[<-]" }
| LEFTSQ RIGHTSQ LARROW   { mixfix "[]<-" }
883
884
885
| LEFTSQ UNDERSCORE DOTDOT UNDERSCORE RIGHTSQ { mixfix "[_.._]" }
| LEFTSQ            DOTDOT UNDERSCORE RIGHTSQ { mixfix "[.._]" }
| LEFTSQ UNDERSCORE DOTDOT            RIGHTSQ { mixfix "[_..]" }
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947