parser.mly 43.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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

Andrei Paskevich's avatar
Andrei Paskevich committed
15 16 17
  let qualid_last = function Qident x | Qdot (_, x) -> x

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

19
  let floc s e = Loc.extract (s,e)
20

Andrei Paskevich's avatar
Andrei Paskevich committed
21 22 23
  let debug_auto_model = Debug.register_flag
    ~desc:"When set, model attributes are not added during parsing"
    "no_auto_model"
24

Andrei Paskevich's avatar
Andrei Paskevich committed
25 26
  let add_attr id l =
    { id with id_ats = l }
27

Andrei Paskevich's avatar
Andrei Paskevich committed
28
  let add_model_trace_attr id =
29
    if Debug.test_flag debug_auto_model then id else
Andrei Paskevich's avatar
Andrei Paskevich committed
30
    let is_model_trace_attr l =
31
      match l with
Andrei Paskevich's avatar
Andrei Paskevich committed
32 33
      | ATpos _ -> false
      | ATstr attr -> Ident.is_model_trace_attr attr
34
    in
Andrei Paskevich's avatar
Andrei Paskevich committed
35
    if List.exists is_model_trace_attr id.id_ats then id else
36
      let l =
Andrei Paskevich's avatar
Andrei Paskevich committed
37 38 39
        (ATstr (Ident.create_model_trace_attr id.id_str))
        ::(ATstr Ident.model_attr) :: id.id_ats in
      { id with id_ats = l }
40

Andrei Paskevich's avatar
Andrei Paskevich committed
41
  let add_model_attrs (b : binder) =
42 43
    match b with
    | (loc, Some id, ghost, ty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
44
      (loc, Some (add_model_trace_attr id), ghost, ty)
45 46
    | _ -> b

Andrei Paskevich's avatar
Andrei Paskevich committed
47
  let id_anonymous loc = { id_str = "_"; id_ats = []; id_loc = loc }
48

49 50 51 52 53 54
  let mk_int_const neg lit =
    Number.{ ic_negative = neg ; ic_abs = lit}

  let mk_real_const neg lit =
    Number.{ rc_negative = neg ; rc_abs = lit}

Andrei Paskevich's avatar
Andrei Paskevich committed
55
  let mk_id id s e = { id_str = id; id_ats = []; id_loc = floc s e }
56

57 58
  let get_op s e = Qident (mk_id (Ident.mixfix "[]") s e)
  let set_op s e = Qident (mk_id (Ident.mixfix "[<-]") s e)
59
  let sub_op s e = Qident (mk_id (Ident.mixfix "[..]") s e)
60 61
  let above_op s e = Qident (mk_id (Ident.mixfix "[_..]") s e)
  let below_op s e = Qident (mk_id (Ident.mixfix "[.._]") s e)
62

63 64
  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 }
65
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
66

67 68 69
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
70
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
71 72 73 74 75 76
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
77
    sp_reads   = [];
78
    sp_writes  = [];
79
    sp_alias   = [];
80
    sp_variant = [];
81 82
    sp_checkrw = false;
    sp_diverge = false;
83
  }
84

85 86 87 88
  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;
89
    sp_reads   = s1.sp_reads @ s2.sp_reads;
90
    sp_writes  = s1.sp_writes @ s2.sp_writes;
91
    sp_alias   = s1.sp_alias @ s2.sp_alias;
92
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
93 94
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
95
  }
96

Andrei Paskevich's avatar
Andrei Paskevich committed
97 98 99
  let break_id    = "'Break"
  let continue_id = "'Continue"
  let return_id   = "'Return"
100

101 102 103 104 105 106 107 108 109
  let apply_return pat sp =
    let apply = function
      | loc, [{pat_desc = Pvar ({id_str = "result"; id_loc = l}, false)}, f]
        when Loc.equal loc l -> loc, [pat, f]
      | post -> post in
    match pat.pat_desc with
    | Pwild -> sp
    | _ -> { sp with sp_post = List.map apply sp.sp_post }

110 111
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
112

113 114 115
  let error_loc loc = Loc.error ~loc Error

  let () = Exn_printer.register (fun fmt exn -> match exn with
116
    | Error -> Format.fprintf fmt "syntax error %s" (Parser_messages.message 1)
117
    | _ -> raise exn)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
118 119
%}

120
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
121

122
%token <string> LIDENT CORE_LIDENT UIDENT CORE_UIDENT
123
%token <Number.integer_literal> INTEGER
124
%token <string> OP1 OP2 OP3 OP4 OPPREF
125
%token <Number.real_literal> REAL
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
126
%token <string> STRING
127
%token <string> ATTRIBUTE
128
%token <Loc.position> POSITION
129
%token <string> QUOTE_LIDENT
130

131
(* keywords *)
132

Martin Clochard's avatar
Martin Clochard committed
133
%token AS AXIOM BY CLONE COINDUCTIVE CONSTANT
Clément Fumex's avatar
Clément Fumex committed
134
%token ELSE END EPSILON EXISTS EXPORT FALSE FLOAT FORALL FUNCTION
Andrei Paskevich's avatar
Andrei Paskevich committed
135
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
136
%token LET MATCH META NOT PREDICATE RANGE SCOPE
Martin Clochard's avatar
Martin Clochard committed
137
%token SO THEN THEORY TRUE TYPE USE WITH
138

139
(* program keywords *)
140

141
%token ABSTRACT ABSURD ALIAS ANY ASSERT ASSUME AT BEGIN BREAK CHECK
Andrei Paskevich's avatar
Andrei Paskevich committed
142
%token CONTINUE DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
143
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
144 145
%token PRIVATE PURE RAISE RAISES READS REC REQUIRES
%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES
146

147
(* symbols *)
148

Andrei Paskevich's avatar
Andrei Paskevich committed
149
%token AND ARROW
150
%token BAR
151
%token COLON COMMA
152
%token DOT DOTDOT EQUAL LT GT LTGT MINUS
153
%token LEFTPAR LEFTSQ
154
%token LARROW LRARROW OR
155
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
156
%token UNDERSCORE
157 158 159

%token EOF

160
(* program symbols *)
161

162
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
163

164
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
165

166 167
%nonassoc below_SEMI
%nonassoc SEMICOLON
168
%nonassoc LET VAL EXCEPTION
169
%nonassoc prec_no_else
170
%nonassoc DOT ELSE RETURN
Andrei Paskevich's avatar
Andrei Paskevich committed
171
%nonassoc prec_no_spec
172
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES ALIAS DIVERGES VARIANT
173 174 175 176 177
%nonassoc below_LARROW
%nonassoc LARROW
%nonassoc below_COMMA
%nonassoc COMMA
%nonassoc GHOST
Andrei Paskevich's avatar
Andrei Paskevich committed
178
%nonassoc prec_attr
179
%nonassoc COLON (* weaker than -> because of t: a -> b *)
180
%right ARROW LRARROW BY SO
181 182
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
183
%nonassoc NOT
184
%right EQUAL LTGT LT GT OP1
185
%nonassoc AT OLD
186
%left OP2 MINUS
187
%left OP3
188
%left OP4
189
%nonassoc prec_prefix_op
190
%nonassoc INTEGER REAL (* stronger than MINUS *)
191 192
%nonassoc LEFTSQ
%nonassoc OPPREF
193

194
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
195

Guillaume Melquiond's avatar
Guillaume Melquiond committed
196
%start <Pmodule.pmodule Wstdlib.Mstr.t> mlw_file
197
%start <Ptree.term> term_eof
198 199
%start <Ptree.qualid> qualid_eof
%start <Ptree.qualid list> qualid_comma_list_eof
200
%start <Ptree.term list> term_comma_list_eof
201
%start <Ptree.ident list> ident_comma_list_eof
202

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
203 204
%%

205 206 207 208 209
(* parsing of a single term *)

term_eof:
| term EOF { $1 }

210
(* Modules and scopes *)
211

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

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

223
module_head:
Andrei Paskevich's avatar
Andrei Paskevich committed
224 225
| THEORY attrs(uident_nq)  { Typing.open_module $2 }
| MODULE attrs(uident_nq)  { Typing.open_module $2 }
226

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

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

240
(* Use and clone *)
241

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

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

single_clone_subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
263
| TYPE qualid ty_var* EQUAL ty  { CStsym  ($2,$3,$5) }
264
| TYPE qualid                   { CStsym  ($2, [], PTtyapp ($2, [])) }
Andrei Paskevich's avatar
Andrei Paskevich committed
265
| CONSTANT  qualid EQUAL qualid { CSfsym  ($2,$4) }
266
| CONSTANT  qualid              { CSfsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
267
| FUNCTION  qualid EQUAL qualid { CSfsym  ($2,$4) }
268
| FUNCTION  qualid              { CSfsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
269
| PREDICATE qualid EQUAL qualid { CSpsym  ($2,$4) }
270
| PREDICATE qualid              { CSpsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
271
| VAL       qualid EQUAL qualid { CSvsym  ($2,$4) }
272
| VAL       qualid              { CSvsym  ($2,$2) }
273 274
| EXCEPTION qualid EQUAL qualid { CSxsym  ($2,$4) }
| EXCEPTION qualid              { CSxsym  ($2,$2) }
275
| AXIOM     qualid              { CSaxiom ($2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
276 277
| LEMMA     qualid              { CSlemma ($2) }
| GOAL      qualid              { CSgoal  ($2) }
278 279 280
| AXIOM     DOT                 { CSprop  (Decl.Paxiom) }
| LEMMA     DOT                 { CSprop  (Decl.Plemma) }
| GOAL      DOT                 { CSprop  (Decl.Pgoal) }
281

Andrei Paskevich's avatar
Andrei Paskevich committed
282
(* Meta declarations *)
283

Andrei Paskevich's avatar
Andrei Paskevich committed
284 285
meta_decl:
| META sident comma_list1(meta_arg)  { Dmeta ($2, $3) }
286 287

meta_arg:
288 289 290 291
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
292 293 294
| AXIOM     qualid  { Max $2 }
| LEMMA     qualid  { Mlm $2 }
| GOAL      qualid  { Mgl $2 }
295
| STRING            { Mstr $1 }
296
| INTEGER           { Mint (Number.to_small_integer $1) }
297

Andrei Paskevich's avatar
Andrei Paskevich committed
298 299 300 301 302 303 304 305 306
(* 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) }
Andrei Paskevich's avatar
Andrei Paskevich committed
307 308 309
| AXIOM attrs(ident_nq) COLON term          { Dprop (Decl.Paxiom, $2, $4) }
| LEMMA attrs(ident_nq) COLON term          { Dprop (Decl.Plemma, $2, $4) }
| GOAL  attrs(ident_nq) COLON term          { Dprop (Decl.Pgoal, $2, $4) }
Andrei Paskevich's avatar
Andrei Paskevich committed
310

311
(* Type declarations *)
312 313

type_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
314
| attrs(lident_nq) ty_var* typedefn invariant* type_witness
315
  { let (vis, mut), def = $3 in
316
    { td_ident = $1; td_params = $2;
317
      td_vis = vis; td_mut = mut;
318
      td_inv = $4; td_wit = $5; td_def = def;
319
      td_loc = floc $startpos $endpos } }
320

321 322 323 324
type_witness:
| (* epsilon *)                           { [] }
| BY LEFTBRC field_list1(expr) RIGHTBRC   { $3 }

325
ty_var:
Andrei Paskevich's avatar
Andrei Paskevich committed
326
| attrs(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
327 328

typedefn:
329
| (* epsilon *)
330
    { (Abstract, false), TDrecord [] }
331 332
| EQUAL vis_mut bar_list1(type_case)
    { $2, TDalgebraic $3 }
333
| EQUAL vis_mut LEFTBRC loption(semicolon_list1(type_field)) RIGHTBRC
334 335 336
    { $2, TDrecord $4 }
| EQUAL vis_mut ty
    { $2, TDalias $3 }
Clément Fumex's avatar
Clément Fumex committed
337
(* FIXME: allow negative bounds *)
338
| EQUAL LT RANGE int_constant int_constant GT
339
    { (Public, false), TDrange ($4, $5) }
Clément Fumex's avatar
Clément Fumex committed
340
| EQUAL LT FLOAT INTEGER INTEGER GT
341
    { (Public, false),
342 343 344
      TDfloat (Number.to_small_integer $4, Number.to_small_integer $5) }

int_constant:
345 346
| INTEGER       { Number.compute_int_literal $1 }
| MINUS INTEGER { BigInt.minus (Number.compute_int_literal $2) }
347 348 349 350 351 352 353

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

abstract:
356 357
| PRIVATE           { Private }
| ABSTRACT          { Abstract }
358

359
type_field:
Andrei Paskevich's avatar
Andrei Paskevich committed
360
| attrs(lident_nq) cast
Andrei Paskevich's avatar
Andrei Paskevich committed
361 362
  { { f_ident = $1; f_mutable = false; f_ghost = false;
      f_pty = $2; f_loc = floc $startpos $endpos } }
Andrei Paskevich's avatar
Andrei Paskevich committed
363
| field_modifiers attrs(lident_nq) cast
364 365
  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
      f_pty = $3; f_loc = floc $startpos $endpos } }
366

367 368 369 370 371 372
field_modifiers:
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

373
type_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
374
| attrs(uident_nq) params { floc $startpos $endpos, $1, $2 }
375

376
(* Logic declarations *)
377

378
constant_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
379 380
| attrs(lident_rich) cast preceded(EQUAL,term)?
  { { ld_ident = add_model_trace_attr $1;
381
      ld_params = []; ld_type = Some $2;
382
      ld_def = $3; ld_loc = floc $startpos $endpos } }
383

384
function_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
385
| attrs(lident_rich) params cast preceded(EQUAL,term)?
386 387
  { { 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
388

389
predicate_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
390
| attrs(lident_rich) params preceded(EQUAL,term)?
391 392
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
393

394
with_logic_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
395
| WITH attrs(lident_rich) params cast? preceded(EQUAL,term)?
396 397
  { { 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
398

399
(* Inductive declarations *)
400 401

inductive_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
402
| attrs(lident_rich) params ind_defn
403 404
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
405

406 407 408
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
409

410
ind_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
411
| attrs(ident_nq) COLON term  { floc $startpos $endpos, $1, $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412

413
(* Type expressions *)
414

415 416 417 418
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
419

420 421
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
422
| quote_lident                      { PTtyvar $1 }
423 424 425
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
426
| LEFTBRC ty RIGHTBRC               { PTpure $2 }
427

428 429
cast:
| COLON ty  { $2 }
430

431
(* Parameters and binders *)
432

433 434
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
435 436
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
437 438
   names, whose type must be inferred. *)

439
params:  param*  { List.concat $1 }
440

441
binders: binder+ { List.concat $1 }
442 443 444

param:
| anon_binder
445
    { error_param (floc $startpos $endpos) }
446 447
| lident_nq attr+
    { error_param (floc $startpos $endpos) }
448 449 450 451
| ty_arg
    { [floc $startpos $endpos, None, false, $1] }
| LEFTPAR GHOST ty RIGHTPAR
    { [floc $startpos $endpos, None, true, $3] }
452
| LEFTPAR binder_vars_rest RIGHTPAR
453
    { match $2 with [l,_] -> error_param l
454
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
455
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
456
    { match $3 with [l,_] -> error_param l
457 458
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
459
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
460
| LEFTPAR GHOST binder_vars cast RIGHTPAR
461
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
462

463 464
binder:
| anon_binder
465
    { let l,i = $1 in [l, i, false, None] }
466 467
| lident_nq attr+
    { [floc $startpos $endpos, Some (add_attr $1 $2), false, None] }
468 469 470 471
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
472
          [floc $startpos $endpos, Some id, false, None]
473
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
474 475 476
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
477 478
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
479
| LEFTPAR binder_vars_rest RIGHTPAR
480
    { match $2 with [l,i] -> [l, i, false, None]
481
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
482
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
483
    { match $3 with [l,i] -> [l, i, true, None]
484 485
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
486
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
487
| LEFTPAR GHOST binder_vars cast RIGHTPAR
488
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
489

490 491 492
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
493

494
binder_vars_rest:
495
| binder_vars_head attr+ binder_var*
496 497
    { List.rev_append (match $1 with
        | (l, Some id) :: bl ->
498 499 500
            let l2 = floc $startpos($2) $endpos($2) in
            (Loc.join l l2, Some (add_attr id $2)) :: bl
        | _ -> assert false) $3 }
501
| binder_vars_head anon_binder binder_var*
502
    { List.rev_append $1 ($2 :: $3) }
503
| anon_binder binder_var*
504
    { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
505

506
binder_vars_head:
507
| ty {
508 509
    let of_id id = id.id_loc, Some id in
    let push acc = function
510
      | PTtyapp (Qident id, []) -> of_id id :: acc
511
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
512
    match $1 with
513
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
514
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
515

516
binder_var:
Andrei Paskevich's avatar
Andrei Paskevich committed
517
| attrs(lident_nq)  { floc $startpos $endpos, Some $1 }
Clément Fumex's avatar
Clément Fumex committed
518
| anon_binder       { $1 }
519 520

anon_binder:
Clément Fumex's avatar
Clément Fumex committed
521
| UNDERSCORE        { floc $startpos $endpos, None }
522

523 524 525 526
(* Logical terms *)

mk_term(X): d = X { mk_term d $startpos $endpos }

527 528 529 530
term:
| single_term %prec below_COMMA   { $1 }
| single_term COMMA term_
    { mk_term (Ttuple ($1::$3)) $startpos $endpos }
531 532

term_:
533 534 535 536 537 538
| single_term %prec below_COMMA   { [$1] }
| single_term COMMA term_         { $1::$3 }

single_term: t = mk_term(single_term_) { t }

single_term_:
539 540
| term_arg_
    { match $1 with (* break the infix relation chain *)
541 542 543
      | Tinfix (l,o,r) -> Tinnfix (l,o,r)
      | Tbinop (l,o,r) -> Tbinnop (l,o,r)
      | d -> d }
544
| NOT single_term
545
    { Tnot $2 }
546
| OLD single_term
Andrei Paskevich's avatar
Andrei Paskevich committed
547
    { Tat ($2, mk_id Dexpr.old_label $startpos($1) $endpos($1)) }
548
| single_term AT uident
549
    { Tat ($1, $3) }
550
| prefix_op single_term %prec prec_prefix_op
551
    { Tidapp (Qident $1, [$2]) }
552
| MINUS INTEGER
553
    { Tconst (Number.ConstInt (mk_int_const true $2)) }
554
| MINUS REAL
555
    { Tconst (Number.ConstReal (mk_real_const true $2)) }
556
| l = single_term ; o = bin_op ; r = single_term
557
    { Tbinop (l, o, r) }
558
| l = single_term ; o = infix_op_1 ; r = single_term
559
    { Tinfix (l, o, r) }
560
| l = single_term ; o = infix_op_234 ; r = single_term
561
    { Tidapp (Qident o, [l; r]) }
562 563 564 565 566 567
| 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
568 569 570 571 572 573 574 575
    { 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)
576
      | _ -> Tcase (def, [pat, $6]) }
Andrei Paskevich's avatar
Andrei Paskevich committed
577
| LET attrs(lident_op_id) EQUAL term IN term
578
    { Tlet ($2, $4, $6) }
Andrei Paskevich's avatar
Andrei Paskevich committed
579
| LET attrs(lident_nq) mk_term(lam_defn) IN term
580
    { Tlet ($2, $3, $5) }
Andrei Paskevich's avatar
Andrei Paskevich committed
581
| LET attrs(lident_op_id) mk_term(lam_defn) IN term
582
    { Tlet ($2, $3, $5) }
583
| MATCH term WITH match_cases(term) END
584
    { Tcase ($2, $4) }
585
| quant comma_list1(quant_vars) triggers DOT term
Andrei Paskevich's avatar
Andrei Paskevich committed
586
    { let l = List.map add_model_attrs (List.concat $2) in
587
      Tquant ($1, l, $3, $5) }
588
| FUN binders ARROW term
589
    { Tquant (Dterm.DTlambda, $2, [], $4) }
590 591
| EPSILON
    { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
Andrei Paskevich's avatar
Andrei Paskevich committed
592 593
| attr single_term %prec prec_attr
    { Tattr ($1, $2) }
594
| single_term cast
595 596
    { Tcast ($1, $2) }

597
lam_defn:
598
| binders EQUAL term  { Tquant (Dterm.DTlambda, $1, [], $3) }
599

600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615
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 }

Andrei Paskevich's avatar
M.()  
Andrei Paskevich committed
616
term_block:
617
| BEGIN term END                                    { $2.term_desc }
618
| LEFTPAR term RIGHTPAR                             { $2.term_desc }
619
| BEGIN END                                         { Ttuple [] }
620 621 622
| LEFTPAR RIGHTPAR                                  { Ttuple [] }
| LEFTBRC field_list1(term) RIGHTBRC                { Trecord $2 }
| LEFTBRC term_arg WITH field_list1(term) RIGHTBRC  { Tupdate ($2,$4) }
Andrei Paskevich's avatar
M.()  
Andrei Paskevich committed
623 624 625 626 627

term_sub_:
| term_block                                        { $1 }
| uqualid DOT mk_term(term_block)                   { Tscope ($1, $3) }
| term_dot DOT lqualid_rich                         { Tidapp ($3,[$1]) }
628 629 630 631
| 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]) }
632 633 634 635 636 637
| 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]) }
638

639 640
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
641

642
match_cases(X):
643 644 645 646
| cl = bar_list1(match_case(X)) { cl }

match_case(X):
| mc = separated_pair(pattern, ARROW, X) { mc }
647

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

651
triggers:
652 653
| (* epsilon *)                                                         { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(single_term)) RIGHTSQ  { $2 }
654

655
%inline bin_op:
656 657 658 659 660 661
| ARROW   { Dterm.DTimplies }
| LRARROW { Dterm.DTiff }
| OR      { Dterm.DTor }
| BARBAR  { Dterm.DTor_asym }
| AND     { Dterm.DTand }
| AMPAMP  { Dterm.DTand_asym }
662 663
| BY      { Dterm.DTby }
| SO      { Dterm.DTso }
664

665
quant:
666 667
| FORALL  { Dterm.DTforall }
| EXISTS  { Dterm.DTexists }
668

669
numeral:
670 671
| INTEGER { Number.ConstInt (mk_int_const false $1) }
| REAL    { Number.ConstReal (mk_real_const false $1) }
672

673
(* Program declarations *)
674

Andrei Paskevich's avatar
Andrei Paskevich committed
675
prog_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
676 677 678 679 680 681
| VAL ghost kind attrs(lident_rich) mk_expr(val_defn) { Dlet (add_model_trace_attr $4, $2, $3, $5) }
| LET ghost kind attrs(lident_rich) mk_expr(fun_defn) { Dlet ($4, $2, $3, $5) }
| LET ghost kind attrs(lident_rich) const_defn        { Dlet ($4, $2, $3, $5) }
| LET REC with_list1(rec_defn)                        { Drec $3 }
| EXCEPTION attrs(uident_nq)        { Dexn ($2, PTtuple [], Ity.MaskVisible) }
| EXCEPTION attrs(uident_nq) return { Dexn ($2, fst $3, snd $3) }
682 683 684 685 686 687 688 689 690 691 692

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

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

(* Function definitions *)
695

696
rec_defn:
697 698 699 700 701 702
| ghost kind attrs(lident_rich) binders return_opt spec EQUAL spec seq_expr
    { let pat, ty, mask = $5 in
      let spec = apply_return pat (spec_union $6 $8) in
      let id = mk_id return_id $startpos($7) $endpos($7) in
      let e = { $9 with expr_desc = Eoptexn (id, mask, $9) } in
      $3, $1, $2, $4, ty, mask, spec, e }
703

704
fun_defn:
705 706 707 708 709 710
| binders return_opt spec EQUAL spec seq_expr
    { let pat, ty, mask = $2 in
      let spec = apply_return pat (spec_union $3 $5) in
      let id = mk_id return_id $startpos($4) $endpos($4) in
      let e = { $6 with expr_desc = Eoptexn (id, mask, $6) } in
      Efun (List.map add_model_attrs $1, ty, mask, spec, e) }
711

712
val_defn:
713 714 715
| params return_opt spec
    { let pat, ty, mask = $2 in
      Eany ($1, Expr.RKnone, ty, mask, apply_return pat $3) }
716

717 718 719 720
const_defn:
| cast EQUAL seq_expr   { { $3 with expr_desc = Ecast ($3, $1) } }
| EQUAL seq_expr        { $2 }

721 722 723 724 725
(* Program expressions *)

mk_expr(X): d = X { mk_expr d $startpos $endpos }

seq_expr:
Andrei Paskevich's avatar
Andrei Paskevich committed
726 727 728
| contract_expr %prec below_SEMI  { $1 }
| contract_expr SEMICOLON         { $1 }
| contract_expr SEMICOLON seq_expr
729
    { mk_expr (Esequence ($1, $3)) $startpos $endpos }
730

Andrei Paskevich's avatar
Andrei Paskevich committed
731 732 733 734
contract_expr:
| assign_expr %prec prec_no_spec  { $1 }
| assign_expr single_spec spec
    { let d = Efun ([], None, Ity.MaskVisible, spec_union $2 $3, $1) in
Andrei Paskevich's avatar
Andrei Paskevich committed
735
      let d = Eattr (ATstr Vc.wb_attr, mk_expr d $startpos $endpos) in
Andrei Paskevich's avatar
Andrei Paskevich committed
736 737
      mk_expr d $startpos $endpos }

738 739 740 741 742 743 744
assign_expr:
| expr %prec below_LARROW         { $1 }
| expr LARROW expr
    { 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}::_, _::_
Guillaume Melquiond's avatar
Guillaume Melquiond committed
745
          when id.id_str = Ident.mixfix "[]" -> Loc.errorm ~loc
746 747 748 749 750 751
            "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
      let d = match $1.expr_desc, $3.expr_desc with
Guillaume Melquiond's avatar
Guillaume Melquiond committed
752 753
        | Eidapp (Qident id, [e1;e2]), _ when id.id_str = Ident.mixfix "[]" ->
            Eidapp (Qident {id with id_str = Ident.mixfix "[]<-"}, [e1;e2;$3])
754 755 756 757 758 759 760
        | Etuple ll, Etuple rl -> Eassign (down ll rl)
        | Etuple _, _ -> Loc.errorm ~loc "Invalid parallel assignment"
        | _, _ -> Eassign (down [$1] [$3]) in
      { expr_desc = d; expr_loc = loc } }

expr:
| single_expr %prec below_COMMA   { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
761
| single_expr COMMA expr_list1
762
    { mk_expr (Etuple ($1::$3)) $startpos $endpos }
763

Andrei Paskevich's avatar
Andrei Paskevich committed
764
expr_list1:
765
| single_expr %prec below_COMMA   { [$1] }
Andrei Paskevich's avatar
Andrei Paskevich committed
766
| single_expr COMMA expr_list1    { $1::$3 }
767 768 769 770

single_expr: e = mk_expr(single_expr_)  { e }

single_expr_:
771
| expr_arg_
772 773
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
774
| single_expr AMPAMP single_expr
775
    { Eand ($1, $3) }
776
| single_expr BARBAR single_expr
777
    { Eor ($1, $3) }
778
| NOT single_expr
779
    { Enot $2 }
780
| prefix_op single_expr %prec prec_prefix_op
781
    { Eidapp (Qident $1, [$2]) }
782
| MINUS INTEGER
783
    { Econst (Number.ConstInt (mk_int_const true $2)) }
784
| MINUS REAL
785
    { Econst (Number.ConstReal (mk_real_const true $2)) }
786
| l = single_expr ; o = infix_op_1 ; r = single_expr
787
    { Einfix (l,o,r) }
788
| l = single_expr ; o = infix_op_234 ; r = single_expr
789
    { Eidapp (Qident o, [l;r]) }
790 791 792
| 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 }
Andrei Paskevich's avatar
Andrei Paskevich committed
793
| IF seq_expr THEN contract_expr ELSE contract_expr
794
    { Eif ($2, $4, $6) }
Andrei Paskevich's avatar
Andrei Paskevich committed
795
| IF seq_expr THEN contract_expr %prec prec_no_else
Andrei Paskevich's avatar