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_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 SCOPE
Andrei Paskevich's avatar
Andrei Paskevich committed
107
%token THEN THEORY TRUE TYPE USE WITH
108

109
(* program keywords *)
110

111
%token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN CHECK
112
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
113
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
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 AT OLD
151
%nonassoc LARROW
152
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
153
%left OP2
154
%left OP3
155
%left OP4
156
%nonassoc prec_prefix_op
157
158
%nonassoc LEFTSQ
%nonassoc OPPREF
159

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

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

165
(* Modules and namespaces *)
166

167
mlw_file:
168
169
170
171
172
| mlw_module* EOF
    { Typing.close_file () }
| module_decl+ EOF
    { let loc = floc $startpos($2) $endpos($2) in
      Typing.close_module loc; Typing.close_file () }
173

174
mlw_module:
175
176
| module_head module_decl* END
    { Typing.close_module (floc $startpos($3) $endpos($3)) }
177

178
module_head:
179
180
| THEORY labels(uident)  { Typing.open_module $2 }
| MODULE labels(uident)  { Typing.open_module $2 }
181

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

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

191
(* Use and clone *)
192

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

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

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

216
217
218
ns:
| uqualid { Some $1 }
| DOT     { None }
219

220
221
222
223
224
225
226
227
228
229
230
231
232
(* 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) }
233
| pdecl                                     { $1 }
234
235

meta_arg:
236
237
238
239
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
240
241
242
| AXIOM     qualid  { Max $2 }
| LEMMA     qualid  { Mlm $2 }
| GOAL      qualid  { Mgl $2 }
243
244
| STRING            { Mstr $1 }
| INTEGER           { Mint (small_integer $1) }
245
246

(* Type declarations *)
247
248

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

256
ty_var:
257
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
258

259
260
261
262
263
264
265
266
(* 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
267
typedefn:
268
| (* epsilon *)
269
270
271
272
273
274
275
276
277
278
279
280
281
282
    { (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 }
283
284

abstract:
285
286
| PRIVATE           { Private }
| ABSTRACT          { Abstract }
287

288
289
290
291
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 } }
292

293
field_modifiers:
294
| (* epsilon *) { false, false }
295
296
297
298
299
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

300
type_case:
301
| labels(uident) params { floc $startpos $endpos, $1, $2 }
302

303
(* Logic declarations *)
304

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

310
311
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
312
313
  { { 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
314

315
316
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
317
318
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
319

320
with_logic_decl:
321
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
322
323
  { { 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
324

325
(* Inductive declarations *)
326
327

inductive_decl:
328
| labels(lident_rich) params ind_defn
329
330
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
331

332
333
334
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
335

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

339
(* Type expressions *)
340

341
342
343
344
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
345

346
347
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
348
| quote_lident                      { PTtyvar $1 }
349
350
351
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
352

353
354
cast:
| COLON ty  { $2 }
355

356
(* Parameters and binders *)
357

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

364
params:  param*  { List.concat $1 }
365

366
binders: binder+ { List.concat $1 }
367
368
369

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

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

422
423
424
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
425

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

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

448
binder_var:
449
450
| labels(lident)  { floc $startpos $endpos, Some $1 }
| anon_binder     { $1 }
451
452

anon_binder:
453
454
| UNDERSCORE      { floc $startpos $endpos, None }

455
456
457
458
459
460
461
462
463
464
465
466
(* 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) }
467
468
469
470
| OLD term
    { Tat ($2, mk_id "0" $startpos($1) $endpos($1)) }
| term AT uident
    { Tat ($1, $3) }
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
| 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)
488
489
490
491
492
      | 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)
493
      | _ -> Tmatch ($4, [$2, $6]) }
494
495
496
497
498
499
| 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) }
500
501
502
503
504
505
| 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) }
506
507
| FUN binders ARROW term
    { Tquant (Tlambda, $2, [], $4) }
508
509
510
511
512
513
514
| EPSILON
    { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
| label term %prec prec_named
    { Tnamed ($1, $2) }
| term cast
    { Tcast ($1, $2) }

515
516
517
lam_defn:
| binders EQUAL term  { Tquant (Tlambda, $1, [], $3) }

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
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 }
| 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]) }
545
546
547
548
549
550
| 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]) }
551

552
553
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
554

555
556
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
557

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

561
562
563
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
564

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

573
574
575
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
576

577
578
579
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
580

581
(* Program declarations *)
582

583
pdecl:
584
585
| 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) }
586
| LET ghost kind labels(lident_rich) EQUAL seq_expr    { Dlet ($4, $2, $3, $6) }
587
588
589
590
591
592
593
594
595
596
597
598
599
600
| 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 }
601
602

(* Function definitions *)
603

604
rec_defn:
605
606
| ghost kind labels(lident_rich) binders cast? spec EQUAL spec seq_expr
    { $3, $1, $2, $4, $5, spec_union $6 $8, $9 }
607

608
fun_defn:
609
| binders cast? spec EQUAL spec seq_expr
610
    { Efun ($1, $2, spec_union $3 $5, $6) }
611

612
613
val_defn:
| params cast spec  { Eany ($1, $2, $3) }
614

615
616
617
618
619
620
621
622
(* 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 }
623

624
expr: e = mk_expr(expr_) { e }
625
626
627

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

713
714
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
715
716

expr_arg_:
717
718
719
720
721
722
723
724
725
726
727
| 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 }
728
729

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

749
750
loop_annotation:
| (* epsilon *)
751
    { [], [] }
752
| invariant loop_annotation
753
    { let inv, var = $2 in $1 :: inv, var }
754
| variant loop_annotation
755
    { let inv, var = $2 in inv, variant_union $1 var }
756

757
758
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
759
760

assertion_kind:
761
762
763
| ASSERT  { Expr.Assert }
| ASSUME  { Expr.Assume }
| CHECK   { Expr.Check }
764
765

for_direction:
766
767
| TO      { Expr.To }
| DOWNTO  { Expr.DownTo }
768

769
(* Specification *)
770

771
spec:
772
| (* epsilon *)     { empty_spec }
773
| single_spec spec  { spec_union $1 $2 }
774

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

795
ensures:
796
| term
797
    { let id = mk_id "result" $startpos $endpos in
798
      [mk_pat (Pvar id) $startpos $endpos, $1] }
799

800
raises:
801
802
803
| uqualid ARROW term
    { $1, mk_pat (Ptuple []) $startpos($1) $endpos($1), $3 }
| uqualid pat_arg ARROW term
804
    { $1, $2, $4 }
805

806
xsymbol:
807
| uqualid
808
    { $1, mk_pat Pwild $startpos $endpos, mk_term Ttrue $startpos $endpos }
809

810
invariant:
811
| INVARIANT LEFTBRC term RIGHTBRC { $3 }
812

813
variant:
814
| VARIANT LEFTBRC comma_list1(single_variant) RIGHTBRC { $3 }
815

816
single_variant:
817
| term preceded(WITH,lqualid)? { $1, $2 }
818

819
(* Patterns *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
820

821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
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) }
838
| mk_pat(pat_uni_) cast                 { Pcast($1,$2) }
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854

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:
855
| UIDENT        { mk_id $1 $startpos $endpos }
856
857

lident:
858
| LIDENT        { mk_id $1 $startpos $endpos }
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884

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 }
|