parser.mly 34 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   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
17
  let mixfix s = "mixfix " ^ s
18

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

  let use_as q = function Some x -> x | None -> qualid_last q
22

23
  let floc s e = Loc.extract (s,e)
24

25
  let model_label = Ident.create_label "model"
26
  let model_projected = Ident.create_label "model_projected"
27 28 29 30 31

  let is_model_label l =
    match l with
    | Lpos _ -> false
    | Lstr lab ->
32 33
      (lab = model_label) || (lab = model_projected)

34

35
  let model_lab_present labels =
36 37 38 39 40 41 42 43 44 45 46
    try
      ignore(List.find is_model_label labels);
      true
    with Not_found ->
      false

  let model_trace_regexp = Str.regexp "model_trace:"

  let is_model_trace_label l =
    match l with
    | Lpos _ -> false
47
    | Lstr lab ->
48
      try
49
	ignore(Str.search_forward model_trace_regexp lab.Ident.lab_string 0);
50 51 52 53 54 55 56 57 58 59 60
	true
      with Not_found -> false

  let model_trace_lab_present labels =
    try
      ignore(List.find is_model_trace_label labels);
      true
    with Not_found ->
      false

  let add_model_trace name labels =
61
    if (model_lab_present labels) && (not (model_trace_lab_present labels)) then
62 63
      (Lstr (Ident.create_label ("model_trace:" ^ name)))::labels
    else
64
      labels
65 66 67 68

  let add_lab id l =
    let l = add_model_trace id.id_str l in
    { id with id_lab = l }
69

70
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
71

72
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
73

74 75
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
76 77 78
  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)
79

80 81
  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 }
82
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
83

84 85 86
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
87
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
88 89 90 91 92 93
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
94
    sp_reads   = [];
95 96
    sp_writes  = [];
    sp_variant = [];
97 98
    sp_checkrw = false;
    sp_diverge = false;
99
  }
100

101 102 103 104
  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;
105
    sp_reads   = s1.sp_reads @ s2.sp_reads;
106 107
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
108 109
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
110
  }
111

112
(* dead code
113
  let add_init_mark e =
114
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
115
    { e with expr_desc = Emark (init, e) }
116
*)
117

118
  let small_integer i =
119
    try match i with
120 121 122 123
      | 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)
124
    with Failure _ -> raise Error
125

126 127
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
128

129 130 131 132 133
  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
134 135
%}

136
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
137

138
%token <string> LIDENT UIDENT
Andrei Paskevich's avatar
Andrei Paskevich committed
139
%token <Number.integer_constant> INTEGER
140
%token <string> OP1 OP2 OP3 OP4 OPPREF
Andrei Paskevich's avatar
Andrei Paskevich committed
141
%token <Number.real_constant> FLOAT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
142
%token <string> STRING
143
%token <Loc.position> POSITION
144
%token <string> QUOTE_LIDENT
145

146
(* keywords *)
147

Martin Clochard's avatar
Martin Clochard committed
148
%token AS AXIOM BY CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
149 150
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
151
%token LET MATCH META NOT PREDICATE SCOPE
Martin Clochard's avatar
Martin Clochard committed
152
%token SO THEN THEORY TRUE TYPE USE WITH
153

154
(* program keywords *)
155

156
%token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN CHECK
157
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
158
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
159 160
%token PRIVATE RAISE RAISES READS REC REQUIRES RETURNS
%token TO TRY VAL VARIANT WHILE WRITES
161

162
(* symbols *)
163

Andrei Paskevich's avatar
Andrei Paskevich committed
164
%token AND ARROW
165
%token BAR
166
%token COLON COMMA
167
%token DOT DOTDOT EQUAL LTGT
168
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
169
%token LARROW LRARROW OR
170
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
171
%token UNDERSCORE
172 173 174

%token EOF

175
(* program symbols *)
176

177
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
178

179
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
180

181
%nonassoc IN
182 183 184
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
185
%nonassoc prec_no_else
186
%nonassoc DOT ELSE GHOST
187
%nonassoc prec_named
188
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189

Andrei Paskevich's avatar
Andrei Paskevich committed
190
%right ARROW LRARROW
Martin Clochard's avatar
Martin Clochard committed
191
%right BY SO
192 193
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
194
%nonassoc NOT
195
%right EQUAL LTGT OP1
196
%nonassoc AT OLD
197
%nonassoc LARROW
198
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
199
%left OP2
200
%left OP3
201
%left OP4
202
%nonassoc prec_prefix_op
203 204
%nonassoc LEFTSQ
%nonassoc OPPREF
205

206
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
207

208
%start <Pmodule.pmodule Stdlib.Mstr.t> mlw_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
209 210
%%

211
(* Modules and scopes *)
212

213
mlw_file:
214 215 216 217 218
| mlw_module* EOF
    { Typing.close_file () }
| module_decl+ EOF
    { let loc = floc $startpos($2) $endpos($2) in
      Typing.close_module loc; Typing.close_file () }
219

220
mlw_module:
221 222
| module_head module_decl* END
    { Typing.close_module (floc $startpos($3) $endpos($3)) }
223

224
module_head:
225 226
| THEORY labels(uident)  { Typing.open_module $2 }
| MODULE labels(uident)  { Typing.open_module $2 }
227

Andrei Paskevich's avatar
Andrei Paskevich committed
228 229
scope_head:
| SCOPE boption(IMPORT) uident
230
    { Typing.open_scope (floc $startpos $endpos) $3; $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
231

232
module_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
233
| scope_head module_decl* END
234
    { Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
235 236 237
| d = pure_decl | d = prog_decl | d = meta_decl
    { Typing.add_decl (floc $startpos $endpos) d }
| use_clone { () }
238

239
(* Use and clone *)
240

241
use_clone:
Andrei Paskevich's avatar
Andrei Paskevich committed
242 243 244 245 246 247
| USE EXPORT tqualid
    { Typing.add_decl (floc $startpos $endpos) (Duse $3) }
| CLONE EXPORT tqualid clone_subst
    { Typing.add_decl (floc $startpos $endpos) (Dclone ($3, $4)) }
| USE boption(IMPORT) tqualid option(preceded(AS, uident))
    { let loc = floc $startpos $endpos in
248
      Typing.open_scope loc (use_as $3 $4);
Andrei Paskevich's avatar
Andrei Paskevich committed
249
      Typing.add_decl loc (Duse $3);
250
      Typing.close_scope loc ~import:$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
251 252
| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst
    { let loc = floc $startpos $endpos in
253
      Typing.open_scope loc (use_as $3 $4);
Andrei Paskevich's avatar
Andrei Paskevich committed
254
      Typing.add_decl loc (Dclone ($3, $5));
255
      Typing.close_scope loc ~import:$2 }
256

257
clone_subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
258 259 260 261
| (* epsilon *)                         { [] }
| WITH comma_list1(single_clone_subst)  { $2 }

single_clone_subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
262 263 264 265 266
| TYPE qualid ty_var* EQUAL ty  { CStsym  ($2,$3,$5) }
| CONSTANT  qualid EQUAL qualid { CSfsym  ($2,$4) }
| FUNCTION  qualid EQUAL qualid { CSfsym  ($2,$4) }
| PREDICATE qualid EQUAL qualid { CSpsym  ($2,$4) }
| VAL       qualid EQUAL qualid { CSvsym  ($2,$4) }
267
| AXIOM     qualid              { CSaxiom ($2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
268 269
| LEMMA     qualid              { CSlemma ($2) }
| GOAL      qualid              { CSgoal  ($2) }
270

Andrei Paskevich's avatar
Andrei Paskevich committed
271
(* Meta declarations *)
272

Andrei Paskevich's avatar
Andrei Paskevich committed
273 274
meta_decl:
| META sident comma_list1(meta_arg)  { Dmeta ($2, $3) }
275 276

meta_arg:
277 278 279 280
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
281 282 283
| AXIOM     qualid  { Max $2 }
| LEMMA     qualid  { Mlm $2 }
| GOAL      qualid  { Mgl $2 }
284 285
| STRING            { Mstr $1 }
| INTEGER           { Mint (small_integer $1) }
286

Andrei Paskevich's avatar
Andrei Paskevich committed
287 288 289 290 291 292 293 294 295 296 297 298 299
(* Theory declarations *)

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

300
(* Type declarations *)
301 302

type_decl:
303 304
| labels(lident) ty_var* typedefn invariant*
  { let (vis, mut), def = $3 in
305
    { td_ident = $1; td_params = $2;
306 307 308
      td_vis = vis; td_mut = mut;
      td_inv = $4; td_def = def;
      td_loc = floc $startpos $endpos } }
309

310
ty_var:
311
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
312 313

typedefn:
314
| (* epsilon *)
315
    { (Abstract, false), TDrecord [] }
316 317
| EQUAL vis_mut bar_list1(type_case)
    { $2, TDalgebraic $3 }
318
| EQUAL vis_mut LEFTBRC loption(semicolon_list1(type_field)) RIGHTBRC
319 320 321 322 323 324 325 326 327 328
    { $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 }
329 330

abstract:
331 332
| PRIVATE           { Private }
| ABSTRACT          { Abstract }
333

334 335 336 337
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 } }
338

339
field_modifiers:
340
| (* epsilon *) { false, false }
341 342 343 344 345
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

346
type_case:
347
| labels(uident) params { floc $startpos $endpos, $1, $2 }
348

349
(* Logic declarations *)
350

351 352
constant_decl:
| labels(lident_rich) cast preceded(EQUAL,term)?
353 354
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
355

356 357
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
358 359
  { { 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
360

361 362
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
363 364
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
365

366
with_logic_decl:
367
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
368 369
  { { 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
370

371
(* Inductive declarations *)
372 373

inductive_decl:
374
| labels(lident_rich) params ind_defn
375 376
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
377

378 379 380
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
381

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

385
(* Type expressions *)
386

387 388 389 390
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
391

392 393
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
394
| quote_lident                      { PTtyvar $1 }
395 396 397
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
398

399 400
cast:
| COLON ty  { $2 }
401

402
(* Parameters and binders *)
403

404 405
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
406 407
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
408 409
   names, whose type must be inferred. *)

410
params:  param*  { List.concat $1 }
411

412
binders: binder+ { List.concat $1 }
413 414 415

param:
| anon_binder
416 417 418 419 420 421 422 423
    { 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 _, []) ->
424 425
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
426
| LEFTPAR binder_vars_rest RIGHTPAR
427
    { match $2 with [l,_] -> error_param l
428
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
429
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
430
    { match $3 with [l,_] -> error_param l
431 432
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
433
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
434
| LEFTPAR GHOST binder_vars cast RIGHTPAR
435
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
436

437 438
binder:
| anon_binder
439
    { let l,i = $1 in [l, i, false, None] }
440 441 442 443
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
444 445
             [floc $startpos $endpos, Some id, false, None]
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
446 447 448
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
449 450
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
451 452 453
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident id, []) ->
454 455 456
             let id = add_lab id ($2::$3) in
             [floc $startpos $endpos, Some id, false, None]
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
457
| LEFTPAR binder_vars_rest RIGHTPAR
458
    { match $2 with [l,i] -> [l, i, false, None]
459
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
460
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
461
    { match $3 with [l,i] -> [l, i, true, None]
462 463
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
464
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
465
| LEFTPAR GHOST binder_vars cast RIGHTPAR
466
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
467

468 469 470
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
471

472
binder_vars_rest:
473 474 475 476 477 478 479
| 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*
480
    { List.rev_append $1 ($2 :: $3) }
481
| anon_binder binder_var*
482
    { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
483

484
binder_vars_head:
485
| ty {
486 487
    let of_id id = id.id_loc, Some id in
    let push acc = function
488
      | PTtyapp (Qident id, []) -> of_id id :: acc
489
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
490
    match $1 with
491
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
492
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
493

494
binder_var:
495 496
| labels(lident)  { floc $startpos $endpos, Some $1 }
| anon_binder     { $1 }
497 498

anon_binder:
499 500
| UNDERSCORE      { floc $startpos $endpos, None }

501 502 503 504 505 506 507 508 509
(* 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 *)
510 511 512
      | Tinfix (l,o,r) -> Tinnfix (l,o,r)
      | Tbinop (l,o,r) -> Tbinnop (l,o,r)
      | d -> d }
513
| NOT term
514
    { Tnot $2 }
515 516 517 518
| OLD term
    { Tat ($2, mk_id "0" $startpos($1) $endpos($1)) }
| term AT uident
    { Tat ($1, $3) }
519 520 521 522
| prefix_op term %prec prec_prefix_op
    { Tidapp (Qident $1, [$2]) }
| l = term ; o = bin_op ; r = term
    { Tbinop (l, o, r) }
523
| l = term ; o = infix_op_1 ; r = term
524
    { Tinfix (l, o, r) }
525 526
| l = term ; o = infix_op_234 ; r = term
    { Tidapp (Qident o, [l; r]) }
527 528 529 530 531 532
| 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
533 534 535 536 537 538 539 540 541
    { let cast ty = { $4 with term_desc = Tcast ($4, ty) } in
      let pat, def = match $2.pat_desc with
        | Ptuple [] -> { $2 with pat_desc = Pwild }, cast (PTtuple [])
        | Pcast ({pat_desc = (Pvar (_,false)|Pwild)} as p, ty) -> p, cast ty
        | _ -> $2, $4 in
      match pat.pat_desc with
      | Pvar (id,false) -> Tlet (id, def, $6)
      | Pwild -> Tlet (id_anonymous pat.pat_loc, def, $6)
      | _ -> Tmatch (def, [pat, $6]) }
542 543 544 545 546 547
| 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) }
548 549 550 551 552 553
| 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) }
554
| FUN binders ARROW term
555
    { Tquant (Dterm.DTlambda, $2, [], $4) }
556 557 558 559 560 561 562
| EPSILON
    { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
| label term %prec prec_named
    { Tnamed ($1, $2) }
| term cast
    { Tcast ($1, $2) }

563
lam_defn:
564
| binders EQUAL term  { Tquant (Dterm.DTlambda, $1, [], $3) }
565

566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592
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]) }
593 594 595 596 597 598
| 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]) }
599

600 601
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
602

603 604
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
605

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

609 610 611
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
612

613
%inline bin_op:
614 615 616 617 618 619
| ARROW   { Dterm.DTimplies }
| LRARROW { Dterm.DTiff }
| OR      { Dterm.DTor }
| BARBAR  { Dterm.DTor_asym }
| AND     { Dterm.DTand }
| AMPAMP  { Dterm.DTand_asym }
620 621
| BY      { Dterm.DTby }
| SO      { Dterm.DTso }
622

623
quant:
624 625
| FORALL  { Dterm.DTforall }
| EXISTS  { Dterm.DTexists }
626

627 628 629
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
630

631
(* Program declarations *)
632

Andrei Paskevich's avatar
Andrei Paskevich committed
633
prog_decl:
634 635
| 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) }
636
| LET ghost kind labels(lident_rich) const_defn        { Dlet ($4, $2, $3, $5) }
637
| LET REC with_list1(rec_defn)                         { Drec $3 }
638 639
| EXCEPTION labels(uident)            { Dexn ($2, PTtuple [], Ity.MaskVisible) }
| EXCEPTION labels(uident) return     { Dexn ($2, fst $3, snd $3) }
640 641 642 643 644 645 646 647 648 649 650

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

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

(* Function definitions *)
653

654
rec_defn:
655 656
| ghost kind labels(lident_rich) binders ret_opt spec EQUAL spec seq_expr
    { $3, $1, $2, $4, fst $5, snd $5, spec_union $6 $8, $9 }
657

658
fun_defn:
659 660
| binders ret_opt spec EQUAL spec seq_expr
    { Efun ($1, fst $2, snd $2, spec_union $3 $5, $6) }
661

662
val_defn:
663 664
| params ret_opt spec
    { Eany ($1, Expr.RKnone, fst $2, snd $2, $3) }
665

666 667 668 669
const_defn:
| cast EQUAL seq_expr   { { $3 with expr_desc = Ecast ($3, $1) } }
| EQUAL seq_expr        { $2 }

670 671 672 673 674 675 676 677
(* 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 }
678

679
expr: e = mk_expr(expr_) { e }
680 681 682

expr_:
| expr_arg_
683 684
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
685 686 687 688
| expr AMPAMP expr
    { Eand ($1, $3) }
| expr BARBAR expr
    { Eor ($1, $3) }
689
| NOT expr
690
    { Enot $2 }
691
| prefix_op expr %prec prec_prefix_op
692
    { Eidapp (Qident $1, [$2]) }
693
| l = expr ; o = infix_op_1 ; r = expr
694
    { Einfix (l,o,r) }
695 696
| l = expr ; o = infix_op_234 ; r = expr
    { Eidapp (Qident o, [l;r]) }
697 698 699
| 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 }
700
| IF seq_expr THEN expr ELSE expr
701
    { Eif ($2, $4, $6) }
702
| IF seq_expr THEN expr %prec prec_no_else
703 704
    { Eif ($2, $4, mk_expr (Etuple []) $startpos $endpos) }
| expr LARROW expr
705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720
    { let loc = floc $startpos $endpos in
      let rec down ll rl = match ll, rl with
        | {expr_desc = Eidapp (q, [e1])}::ll, e2::rl -> (e1,q,e2) :: down ll rl
        | {expr_desc = Eidapp (Qident id, [_;_]); expr_loc = loc}::_, _::_
          when id.id_str = mixfix "[]" -> Loc.errorm ~loc
            "Parallel array assignments are not allowed"
        | {expr_loc = loc}::_, _::_ -> Loc.errorm ~loc
            "Invalid left expression in an assignment"
        | [], [] -> []
        | _ -> Loc.errorm ~loc "Invalid parallel assignment" in
      match $1.expr_desc, $3.expr_desc with
        | Eidapp (Qident id, [e1;e2]), _ when id.id_str = mixfix "[]" ->
            Eidapp (Qident {id with id_str = mixfix "[]<-"}, [e1;e2;$3])
        | Etuple ll, Etuple rl -> Eassign (down ll rl)
        | Etuple _, _ -> Loc.errorm ~loc "Invalid parallel assignment"
        | _, _ -> Eassign (down [$1] [$3]) }
721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747
| LET ghost kind let_pattern EQUAL seq_expr IN seq_expr
    { let re_pat pat d = { pat with pat_desc = d } in
      let rec ghostify pat = match pat.pat_desc with
        (* let_pattern marks the opening variable with Ptuple [_] *)
        | Ptuple [{pat_desc = Pvar (id,_)}] -> re_pat pat (Pvar (id,$2))
        | Ptuple (p::pl) -> re_pat pat (Ptuple (ghostify p :: pl))
        | Pas (p,id,gh) -> re_pat pat (Pas (ghostify p, id, gh))
        | Por (p1,p2) -> re_pat pat (Por (ghostify p1, p2))
        | Pcast (p,t) -> re_pat pat (Pcast (ghostify p, t))
        | _ when $2 -> Loc.errorm ~loc:(floc $startpos($2) $endpos($2))
            "illegal ghost qualifier" (* $4 does not start with a Pvar *)
        | _ -> pat in
      let pat = ghostify $4 in
      let kind = match pat.pat_desc with
        | _ when $3 = Expr.RKnone -> $3
        | Pvar (_,_) | Pcast ({pat_desc = Pvar (_,_)},_) -> $3
        | _ -> Loc.errorm ~loc:(floc $startpos($3) $endpos($3))
            "illegal kind qualifier" in
      let cast ty = { $6 with expr_desc = Ecast ($6, ty) } in
      let pat, def = match pat.pat_desc with
        | Ptuple [] -> re_pat pat Pwild, cast (PTtuple [])
        | Pcast ({pat_desc = (Pvar _|Pwild)} as pat, ty) -> pat, cast ty
        | _ -> pat, $6 in
      match pat.pat_desc with
      | Pvar (id, gh) -> Elet (id, gh, kind, def, $8)
      | Pwild -> Elet (id_anonymous pat.pat_loc, false, kind, def, $8)
      | _ -> Ematch (def, [pat, $8]) }
748 749 750 751 752 753
| 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) }
754
| LET REC with_list1(rec_defn) IN seq_expr
755
    { Erec ($3, $5) }
756
| FUN binders spec ARROW spec seq_expr
757
    { Efun ($2, None, Ity.MaskVisible, spec_union $3 $5, $6) }
758
| ABSTRACT spec seq_expr END
759 760 761
    { Efun ([], None, Ity.MaskVisible, $2, $3) }
| ANY return spec
    { Eany ([], Expr.RKnone, Some (fst $2), snd $2, $3) }
762 763
| VAL ghost kind labels(lident_rich) mk_expr(val_defn) IN seq_expr
    { Elet ($4, $2, $3, $5, $7) }
764 765 766 767
| 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) }
768 769
| LABEL labels(uident) IN seq_expr
    { Emark ($2, $4) }
770
| WHILE seq_expr DO loop_annotation seq_expr DONE
771
    { let inv, var = $4 in Ewhile ($2, inv, var, $5) }
772 773
| FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
    { Efor ($2, $4, $5, $6, $8, $9) }
774
| ABSURD
775
    { Eabsurd }
776 777 778 779
| RAISE uqualid expr_arg?
    { Eraise ($2, $3) }
| RAISE LEFTPAR uqualid expr_arg? RIGHTPAR
    { Eraise ($3, $4) }
780 781
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
782
| GHOST expr
783 784 785
    { Eghost $2 }
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
786
| label expr %prec prec_named
787 788 789
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
790

791 792
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
793 794

expr_arg_:
795 796 797 798 799 800 801 802 803 804 805
| 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 }
806 807

expr_sub:
808
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
809 810 811 812 813 814 815
| 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) }
816
| expr_arg LEFTSQ expr RIGHTSQ
817
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
818
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
819
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
820 821 822 823 824 825
| 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]) }
826

827 828
loop_annotation:
| (* epsilon *)
829
    { [], [] }
830
| invariant loop_annotation
831
    { let inv, var = $2 in $1 :: inv, var }
832
| variant loop_annotation
833
    { let inv, var = $2 in inv, variant_union $1 var }
834

835 836
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
837 838

assertion_kind:
839 840 841
| ASSERT  { Expr.Assert }
| ASSUME  { Expr.Assume }
| CHECK   { Expr.Check }
842 843

for_direction:
844 845
| TO      { Expr.To }
| DOWNTO  { Expr.DownTo }
846

847
(* Specification *)
848

849
spec:
850
| (* epsilon *)     { empty_spec }
851
| single_spec spec  { spec_union $1 $2 }
852

853
single_spec:
854
| REQUIRES LEFTBRC term RIGHTBRC
855 856
    { { empty_spec with sp_pre = [$3] } }
| ENSURES LEFTBRC ensures RIGHTBRC
857
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
858
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
859 860 861 862
    { { 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
863
    { { empty_spec with sp_reads = $3; sp_checkrw = true } }
864
| WRITES LEFTBRC comma_list0(term) RIGHTBRC
865
    { { empty_spec with sp_writes = $3; sp_checkrw = true } }
866 867
| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC
    { { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
868 869
| DIVERGES
    { { empty_spec with sp_diverge = true } }
870 871
| variant
    { { empty_spec with sp_variant = $1 } }
872

873
ensures:
874
| term
875
    { let id = mk_id "result" $startpos $endpos in
876
      [mk_pat (Pvar (id,false)) $startpos $endpos, $1] }
877

878
raises:
879
| uqualid ARROW term