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.8 KB
Newer Older
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5
6
7
8
9
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
10
11

%{
12
module Incremental = struct
13
14
15
16
17
18
19
  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 ()
20
21
  let open_namespace n = (Stack.top stack).Ptree.open_namespace n
  let close_namespace l b = (Stack.top stack).Ptree.close_namespace l b
22
23
24
  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
25
end
26

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
27
28
  open Ptree

29
  let infix  s = "infix "  ^ s
30
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
31
  let mixfix s = "mixfix " ^ s
32

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

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

37
  let add_lab id l = { id with id_lab = l }
38

39
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
40

41
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
42

43
44
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
45

46
47
  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 }
48
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
49

50
51
52
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
53
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
54
55
56
57
58
59
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
60
    sp_reads   = [];
61
62
    sp_writes  = [];
    sp_variant = [];
63
64
    sp_checkrw = false;
    sp_diverge = false;
65
  }
66

67
68
69
70
  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;
71
    sp_reads   = s1.sp_reads @ s2.sp_reads;
72
73
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
74
75
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
76
  }
77

78
(* dead code
79
  let add_init_mark e =
80
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
81
    { e with expr_desc = Emark (init, e) }
82
*)
83

84
  let small_integer i =
85
    try match i with
86
87
88
89
      | 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)
90
    with Failure _ -> raise Error
91

92
93
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
94

95
96
97
98
99
  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
100
101
%}

102
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
103

104
%token <string> LIDENT UIDENT
105
%token <Ptree.integer_constant> INTEGER
106
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107
108
%token <Ptree.real_constant> FLOAT
%token <string> STRING
109
%token <Loc.position> POSITION
110
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
111

112
(* keywords *)
113

114
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
115
116
117
%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
118
%token THEN THEORY TRUE TYPE USE WITH
119

120
(* program keywords *)
121

122
123
124
125
126
%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
127

128
(* symbols *)
129

Andrei Paskevich's avatar
Andrei Paskevich committed
130
%token AND ARROW
131
%token BAR
132
%token COLON COMMA
133
%token DOT EQUAL LAMBDA LTGT
134
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
135
%token LARROW LRARROW OR
136
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
137
%token UNDERSCORE
138
139
140

%token EOF

141
(* program symbols *)
142

143
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
144

145
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
146

147
%nonassoc IN
148
149
150
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
151
%nonassoc prec_no_else
152
%nonassoc DOT ELSE GHOST
153
%nonassoc prec_named
154
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155

Andrei Paskevich's avatar
Andrei Paskevich committed
156
%right ARROW LRARROW
157
158
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
159
%nonassoc NOT
160
%left EQUAL LTGT OP1
161
%nonassoc LARROW
162
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
163
%left OP2
164
%left OP3
165
%left OP4
166
%nonassoc prec_prefix_op
167
168
%nonassoc LEFTSQ
%nonassoc OPPREF
169

170
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
171

172
173
%start <Ptree.incremental -> unit> open_file
%start <unit> logic_file program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174
175
%%

176
177
(* Theories, modules, namespaces *)

178
open_file:
179
180
(* Dummy token. Menhir does not accept epsilon. *)
| EOF { Incremental.open_file }
181

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

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

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

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

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

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

201
202
203
204
205
theory_decl:
| decl            { Incremental.new_decl  (floc $startpos $endpos) $1 }
| use_clone       { Incremental.use_clone (floc $startpos $endpos) $1 }
| namespace_head theory_decl* END
    { Incremental.close_namespace (floc $startpos($1) $endpos($1)) $1 }
206

207
208
209
210
211
212
module_decl:
| decl            { Incremental.new_decl  (floc $startpos $endpos) $1 }
| pdecl           { Incremental.new_pdecl (floc $startpos $endpos) $1 }
| use_clone       { Incremental.use_clone (floc $startpos $endpos) $1 }
| namespace_head module_decl* END
    { Incremental.close_namespace (floc $startpos($1) $endpos($1)) $1 }
213

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

218
(* Use and clone *)
219

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

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

233
clone_subst:
234
235
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
236
237
238
239
240
241
| CONSTANT  qualid EQUAL qualid { CSfsym  (floc $startpos $endpos, $2,$4) }
| FUNCTION  qualid EQUAL qualid { CSfsym  (floc $startpos $endpos, $2,$4) }
| PREDICATE qualid EQUAL qualid { CSpsym  (floc $startpos $endpos, $2,$4) }
| VAL       qualid EQUAL qualid { CSvsym  (floc $startpos $endpos, $2,$4) }
| LEMMA     qualid              { CSlemma (floc $startpos $endpos, $2) }
| GOAL      qualid              { CSgoal  (floc $startpos $endpos, $2) }
242

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

247
248
249
250
251
252
253
254
255
256
257
258
259
260
(* Theory declarations *)

decl:
| TYPE with_list1(type_decl)                { Dtype $2 }
| TYPE late_invariant                       { Dtype [$2] }
| CONSTANT  constant_decl                   { Dlogic [$2] }
| FUNCTION  function_decl  with_logic_decl* { Dlogic ($2::$3) }
| PREDICATE predicate_decl with_logic_decl* { Dlogic ($2::$3) }
| INDUCTIVE   with_list1(inductive_decl)    { Dind (Decl.Ind, $2) }
| COINDUCTIVE with_list1(inductive_decl)    { Dind (Decl.Coind, $2) }
| AXIOM labels(ident) COLON term            { Dprop (Decl.Paxiom, $2, $4) }
| LEMMA labels(ident) COLON term            { Dprop (Decl.Plemma, $2, $4) }
| GOAL  labels(ident) COLON term            { Dprop (Decl.Pgoal, $2, $4) }
| META sident comma_list1(meta_arg)         { Dmeta ($2, $3) }
261
262

meta_arg:
263
264
265
266
267
268
269
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
| PROP      qualid  { Mpr $2 }
| STRING            { Mstr $1 }
| INTEGER           { Mint (small_integer $1) }
270
271

(* Type declarations *)
272
273

type_decl:
274
| labels(lident) ty_var* typedefn
275
  { let model, vis, def, inv = $3 in
276
    let vis = if model then Abstract else vis in
277
278
279
    { td_ident = $1; td_params = $2;
      td_model = model; td_vis = vis; td_def = def;
      td_inv = inv; td_loc = floc $startpos $endpos } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
280

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

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

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

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

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

309
310
311
312
type_field:
| field_modifiers labels(lident) cast
  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
      f_pty = $3; f_loc = floc $startpos $endpos } }
313

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

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

324
(* Logic declarations *)
325

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

331
332
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
333
334
  { { ld_ident = $1; ld_params = $2; ld_type = Some $3;
      ld_def = $4; ld_loc = floc $startpos $endpos } }
Andrei Paskevich's avatar
Andrei Paskevich committed
335

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

341
with_logic_decl:
342
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
343
344
  { { ld_ident = $2; ld_params = $3; ld_type = $4;
      ld_def = $5; ld_loc = floc $startpos $endpos } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
345

346
(* Inductive declarations *)
347
348

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

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

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

360
(* Type expressions *)
361

362
363
364
365
ty:
| ty_arg          { $1 }
| lqualid ty_arg+ { PTtyapp ($1, $2) }
| ty ARROW ty     { PTarrow ($1, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
366

367
368
369
370
371
372
373
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
| quote_lident                      { PTtyvar ($1, false) }
| opaque_quote_lident               { PTtyvar ($1, true) }
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
374

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

378
(* Parameters and binders *)
379

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

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

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

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

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

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

448
binder_vars_rest:
449
450
451
452
453
454
455
| binder_vars_head label label* binder_var*
    { List.rev_append (match $1 with
        | (l, Some id) :: bl ->
            let l3 = floc $startpos($3) $endpos($3) in
            (Loc.join l l3, Some (add_lab id ($2::$3))) :: bl
        | _ -> assert false) $4 }
| binder_vars_head anon_binder binder_var*
456
   { List.rev_append $1 ($2 :: $3) }
457
| anon_binder binder_var*
458
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
459

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

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

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

477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
(* 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)
506
507
508
509
510
      | 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)
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
      | _ -> 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]) }
553

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

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

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

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

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

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

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

584
(* Program declarations *)
585

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

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

(* Function declarations *)
600
601

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

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

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

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

(* Function definitions *)
616

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

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

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

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

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

expr_:
| expr_arg_
640
641
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
642
| NOT expr %prec prec_prefix_op
643
    { Enot $2 }
644
| prefix_op expr %prec prec_prefix_op
645
646
647
648
649
650
651
652
    { 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 }
653
| IF seq_expr THEN expr ELSE expr
654
    { Eif ($2, $4, $6) }
655
| IF seq_expr THEN expr %prec prec_no_else
656
657
658
659
660
661
662
    { 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 }
663
| LET top_ghost pattern EQUAL seq_expr IN seq_expr
664
    { match $3.pat_desc with
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
      | 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) }
687
| LET REC with_list1(rec_defn) IN seq_expr
688
    { Erec ($3, $5) }
689
| fun_expr
690
691
692
693
694
695
696
    { 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) }
697
| quote_uident COLON seq_expr
698
    { Emark ($1, $3) }
699
| LOOP loop_annotation seq_expr END
700
    { Eloop ($2, $3) }
701
| WHILE seq_expr DO loop_annotation seq_expr DONE
702
703
704
    { 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) }
705
| ABSURD
706
    { Eabsurd }
707
| RAISE uqualid
708
    { Eraise ($2, None) }
709
| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
710
711
712
    { Eraise ($3, Some $4) }
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
713
| ANY simple_type_c
714
    { Eany $2 }
715
| GHOST expr
716
    { Eghost $2 }
717
| ABSTRACT spec seq_expr END
718
719
720
    { Eabstract($3, $2) }
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
721
| label expr %prec prec_named
722
723
724
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
725

726
727
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
728
729

expr_arg_:
730
731
732
733
734
735
736
737
738
739
740
| 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 }
741
742

expr_sub:
743
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
744
745
746
747
748
749
750
| 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) }
751
| expr_arg LEFTSQ expr RIGHTSQ
752
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
753
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
754
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
755

756
757
758
759
760
761
762
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 } }
763

764
765
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
766

767
768
val_expr:
| tail_type_c { Eany $1 }
769

770
771
772
%inline lazy_op:
| AMPAMP  { LazyAnd }
| BARBAR  { LazyOr }
773
774

assertion_kind:
775
776
777
| ASSERT  { Aassert }
| ASSUME  { Aassume }
| CHECK   { Acheck }
778
779

for_direction:
780
781
| TO      { To }
| DOWNTO  { Downto }
782

783
(* Specification *)
784

785
spec:
786
| (* epsilon *)     { empty_spec }
787
| single_spec spec  { spec_union $1 $2 }
788

789
single_spec:
790
| REQUIRES LEFTBRC term RIGHTBRC
791
792
    { { empty_spec with sp_pre = [$3] } }
| ENSURES LEFTBRC ensures RIGHTBRC
793
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
794
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
795
796
797
798
    { { 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
799
    { { empty_spec with sp_reads = $3; sp_checkrw = true } }
800
| WRITES LEFTBRC comma_list0(term) RIGHTBRC
801
    { { empty_spec with sp_writes = $3; sp_checkrw = true } }
802
803
| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC
    { { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
804
805
| DIVERGES
    { { empty_spec with sp_diverge = true } }
806
807
| variant
    { { empty_spec with sp_variant = $1 } }
808

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

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

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

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

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

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

833
(* Patterns *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
834

835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
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) }
852
| mk_pat(pat_uni_) cast                 { Pcast($1,$2) }
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
883
884
885
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
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962