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.3 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
106
%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
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 LAMBDA 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
| NAMESPACE 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
206
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| 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
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
      | _ -> 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]) }
527
528
529
530
531
532
| 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]) }
533

534
535
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
536

537
538
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
539

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

543
544
545
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
546

547
548
549
550
551
552
553
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
554

555
556
557
558
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
559

560
561
562
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
563

564
(* Program declarations *)
565

566
pdecl:
567
| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
568
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
569
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
570
| LET REC with_list1(rec_defn)                      { Drec $3 }
571
572
| EXCEPTION labels(uident)                          { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident) ty                       { Dexn ($2, $3) }
573

574
575
576
577
578
579
top_ghost:
| (* epsilon *) { Gnone  }
| GHOST         { Gghost }
| LEMMA         { Glemma }

(* Function declarations *)
580
581

type_v:
582
| params cast spec  { ($1, $2, $3) }
583

584
(*
585
simple_type_c:
586
| ty spec { PTpure $1, $2 }
587
*)
588
589

(* Function definitions *)
590

591
rec_defn:
592
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
593
    { $2, $1, ($3, $4, spec_union $5 $7, $8) }
594

595
fun_defn:
596
| binders cast? spec EQUAL spec seq_expr { ($1, $2, spec_union $3 $5, $6) }
597

598
fun_expr:
599
| FUN binders spec ARROW spec seq_expr { ($2, None, spec_union $3 $5, $6) }
600

601
602
603
604
605
606
607
608
(* 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 }
609

610
expr: e = mk_expr(expr_) { e }
611
612
613

expr_:
| expr_arg_
614
615
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
616
617
618
619
| expr AMPAMP expr
    { Eand ($1, $3) }
| expr BARBAR expr
    { Eor ($1, $3) }
620
| NOT expr %prec prec_prefix_op
621
    { Enot $2 }
622
| prefix_op expr %prec prec_prefix_op
623
624
625
626
627
628
    { 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 }
629
| IF seq_expr THEN expr ELSE expr
630
    { Eif ($2, $4, $6) }
631
| IF seq_expr THEN expr %prec prec_no_else
632
633
634
635
636
637
638
    { 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 }
639
| LET top_ghost pattern EQUAL seq_expr IN seq_expr
640
    { match $3.pat_desc with
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
      | 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) }
663
| LET REC with_list1(rec_defn) IN seq_expr
664
    { Erec ($3, $5) }
665
| fun_expr
666
667
668
669
670
671
672
    { 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) }
673
| quote_uident COLON seq_expr
674
    { Emark ($1, $3) }
675
| LOOP loop_annotation seq_expr END
676
    { let inv, var = $2 in Eloop (inv, var, $3) }
677
| WHILE seq_expr DO loop_annotation seq_expr DONE
678
    { let inv, var = $4 in Ewhile ($2, inv, var, $5) }
679
680
| FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
    { Efor ($2, $4, $5, $6, $8, $9) }
681
| ABSURD
682
    { Eabsurd }
683
| RAISE uqualid
684
    { Eraise ($2, None) }
685
| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
686
687
688
    { Eraise ($3, Some $4) }
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
689
690
| ANY ty spec
    { Eany ([], $2, $3) }
691
| GHOST expr
692
    { Eghost $2 }
693
| ABSTRACT spec seq_expr END
694
    { Eabstract($2, $3) }
695
696
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
697
| label expr %prec prec_named
698
699
700
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
701

702
703
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
704
705

expr_arg_:
706
707
708
709
710
711
712
713
714
715
716
| 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 }
717
718

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

738
739
loop_annotation:
| (* epsilon *)
740
    { [], [] }
741
| invariant loop_annotation
742
    { let inv, var = $2 in $1 :: inv, var }
743
| variant loop_annotation
744
    { let inv, var = $2 in inv, variant_union $1 var }
745

746
747
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
748

749
val_expr:
750
| type_v { Eany $1 }
751
752

assertion_kind:
753
754
755
| ASSERT  { Expr.Assert }
| ASSUME  { Expr.Assume }
| CHECK   { Expr.Check }
756
757

for_direction:
758
759
| TO      { Expr.To }
| DOWNTO  { Expr.DownTo }
760

761
(* Specification *)
762

763
spec:
764
| (* epsilon *)     { empty_spec }
765
| single_spec spec  { spec_union $1 $2 }
766

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

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

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

798
xsymbol:
799
| uqualid
800
    { $1, mk_pat Pwild $startpos $endpos, mk_term Ttrue $startpos $endpos }
801

802
invariant:
803
| INVARIANT LEFTBRC term RIGHTBRC { $3 }
804

805
variant:
806
| VARIANT LEFTBRC comma_list1(single_variant) RIGHTBRC { $3 }
807

808
single_variant:
809
| term preceded(WITH,lqualid)? { $1, $2 }
810

811
(* Patterns *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
812

813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
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) }
830
| mk_pat(pat_uni_) cast                 { Pcast($1,$2) }
831
832
833
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

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 "[]<-" }
880
881
882
| LEFTSQ UNDERSCORE DOTDOT UNDERSCORE RIGHTSQ { mixfix "[_.._]" }
| LEFTSQ            DOTDOT UNDERSCORE RIGHTSQ { mixfix "[.._]" }
| LEFTSQ UNDERSCORE DOTDOT            RIGHTSQ { mixfix "[_..]" }
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