parser.mly 30.9 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
module Incremental = struct
14 15 16 17 18 19 20
  let stack = Stack.create ()
  let open_file inc = Stack.push inc stack
  let close_file () = ignore (Stack.pop stack)
  let open_theory id = (Stack.top stack).Ptree.open_theory id
  let close_theory () = (Stack.top stack).Ptree.close_theory ()
  let open_module id = (Stack.top stack).Ptree.open_module id
  let close_module () = (Stack.top stack).Ptree.close_module ()
21 22
  let open_namespace n = (Stack.top stack).Ptree.open_namespace n
  let close_namespace l b = (Stack.top stack).Ptree.close_namespace l b
23 24 25
  let new_decl loc d = (Stack.top stack).Ptree.new_decl loc d
  let new_pdecl loc d = (Stack.top stack).Ptree.new_pdecl loc d
  let use_clone loc use = (Stack.top stack).Ptree.use_clone loc use
26
end
27

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

30
  let infix  s = "infix "  ^ s
31
  let prefix s = "prefix " ^ s
32
  let mixfix s = "mixfix " ^ s
33

34
  let qualid_last = function Qident x | Qdot (_, x) -> x.id_str
35

36
  let floc s e = Loc.extract (s,e)
37

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

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

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

44 45
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
46 47 48
  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)
49

50 51
  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 }
52
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
53

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

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
64
    sp_reads   = [];
65 66
    sp_writes  = [];
    sp_variant = [];
67 68
    sp_checkrw = false;
    sp_diverge = false;
69
  }
70

71 72 73 74
  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;
75
    sp_reads   = s1.sp_reads @ s2.sp_reads;
76 77
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
78 79
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
80
  }
81

82
(* dead code
83
  let add_init_mark e =
84
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
85
    { e with expr_desc = Emark (init, e) }
86
*)
87

88
  let small_integer i =
89
    try match i with
90 91 92 93
      | 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)
94
    with Failure _ -> raise Error
95

96 97
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
98

99 100 101 102 103
  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
104 105
%}

106
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107

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

116
(* keywords *)
117

118
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
119 120 121
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
122
%token THEN THEORY TRUE TYPE USE WITH
123

124
(* program keywords *)
125

126 127 128 129 130
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE
%token PRIVATE RAISE RAISES READS REC REQUIRES RETURNS
%token TO TRY VAL VARIANT WHILE WRITES
131

132
(* symbols *)
133

Andrei Paskevich's avatar
Andrei Paskevich committed
134
%token AND ARROW
135
%token BAR
136
%token COLON COMMA
137
%token DOT DOTDOT EQUAL LAMBDA LTGT
138
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
139
%token LARROW LRARROW OR
140
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
141
%token UNDERSCORE
142 143 144

%token EOF

145
(* program symbols *)
146

147
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
148

149
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
150

151
%nonassoc IN
152 153 154
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
155
%nonassoc prec_no_else
156
%nonassoc DOT ELSE GHOST
157
%nonassoc prec_named
158
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
159

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

174
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
175

176 177
%start <Ptree.incremental -> unit> open_file
%start <unit> logic_file program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
178 179
%%

180 181
(* Theories, modules, namespaces *)

182
open_file:
183 184
(* Dummy token. Menhir does not accept epsilon. *)
| EOF { Incremental.open_file }
185

186
logic_file:
187
| theory* EOF   { Incremental.close_file () }
188

189 190 191
program_file:
| theory_or_module* EOF { Incremental.close_file () }

192 193
theory:
| theory_head theory_decl* END  { Incremental.close_theory () }
194

195 196 197 198
theory_or_module:
| theory                        { () }
| module_head module_decl* END  { Incremental.close_module () }

199
theory_head:
200
| THEORY labels(uident)  { Incremental.open_theory $2 }
201

202 203 204
module_head:
| MODULE labels(uident)  { Incremental.open_module $2 }

205 206 207 208 209
theory_decl:
| decl            { Incremental.new_decl  (floc $startpos $endpos) $1 }
| use_clone       { Incremental.use_clone (floc $startpos $endpos) $1 }
| namespace_head theory_decl* END
    { Incremental.close_namespace (floc $startpos($1) $endpos($1)) $1 }
210

211 212 213 214 215 216
module_decl:
| decl            { Incremental.new_decl  (floc $startpos $endpos) $1 }
| pdecl           { Incremental.new_pdecl (floc $startpos $endpos) $1 }
| use_clone       { Incremental.use_clone (floc $startpos $endpos) $1 }
| namespace_head module_decl* END
    { Incremental.close_namespace (floc $startpos($1) $endpos($1)) $1 }
217

218 219 220
namespace_head:
| NAMESPACE boption(IMPORT) uident
   { Incremental.open_namespace $3.id_str; $2 }
221

222
(* Use and clone *)
223

224
use_clone:
225 226 227
| USE use                                 { ($2, None) }
| CLONE use                               { ($2, Some []) }
| CLONE use WITH comma_list1(clone_subst) { ($2, Some $4) }
228

229
use:
230
| boption(IMPORT) tqualid
231
    { { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
232 233
| boption(IMPORT) tqualid AS uident
    { { use_theory = $2; use_import = Some ($1, $4.id_str) } }
234 235
| EXPORT tqualid
    { { use_theory = $2; use_import = None } }
236

237
clone_subst:
238 239
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
240 241 242 243 244 245
| 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) }
246

247 248 249
ns:
| uqualid { Some $1 }
| DOT     { None }
250

251 252 253 254 255 256 257 258 259 260 261 262 263 264
(* Theory declarations *)

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

meta_arg:
267 268 269 270 271 272 273
| 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) }
274 275

(* Type declarations *)
276 277

type_decl:
278
| labels(lident) ty_var* typedefn
279
  { let model, vis, def, inv = $3 in
280
    let vis = if model then Abstract else vis in
281 282 283
    { td_ident = $1; td_params = $2;
      td_model = model; td_vis = vis; td_def = def;
      td_inv = inv; td_loc = floc $startpos $endpos } }
284

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

291
ty_var:
292
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
293 294

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

304 305 306 307 308
model:
| EQUAL         { false }
| MODEL         { true }

abstract:
309
| (* epsilon *) { Public }
310 311
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
312

313 314 315 316
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 } }
317

318
field_modifiers:
319
| (* epsilon *) { false, false }
320 321 322 323 324
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

325
type_case:
326
| labels(uident) params { floc $startpos $endpos, $1, $2 }
327

328
(* Logic declarations *)
329

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

335 336
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
337 338
  { { 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
339

340 341
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
342 343
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
344

345
with_logic_decl:
346
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
347 348
  { { 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
349

350
(* Inductive declarations *)
351 352

inductive_decl:
353
| labels(lident_rich) params ind_defn
354 355
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
356

357 358 359
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
360

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

364
(* Type expressions *)
365

366 367 368 369
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
370

371 372 373 374 375 376 377
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
| quote_lident                      { PTtyvar ($1, false) }
| opaque_quote_lident               { PTtyvar ($1, true) }
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
378

379 380
cast:
| COLON ty  { $2 }
381

382
(* Parameters and binders *)
383

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

390
params:  param*  { List.concat $1 }
391

392
binders: binder+ { List.concat $1 }
393 394 395

param:
| anon_binder
396 397 398 399 400 401 402 403
    { 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 _, []) ->
404 405
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
406
| LEFTPAR binder_vars_rest RIGHTPAR
407
    { match $2 with [l,_] -> error_param l
408
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
409
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
410
    { match $3 with [l,_] -> error_param l
411 412
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
413
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
414
| LEFTPAR GHOST binder_vars cast RIGHTPAR
415
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
416

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

448 449 450
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
451

452
binder_vars_rest:
453 454 455 456 457 458 459
| 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*
460
   { List.rev_append $1 ($2 :: $3) }
461
| anon_binder binder_var*
462
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
463

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

474
binder_var:
475 476
| labels(lident)  { floc $startpos $endpos, Some $1 }
| anon_binder     { $1 }
477 478

anon_binder:
479 480
| UNDERSCORE      { floc $startpos $endpos, None }

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

564 565
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
566

567 568
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
569

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

573 574 575
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
576

577 578 579 580 581 582 583
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
584

585 586 587 588
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
589

590 591 592
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
593

594
(* Program declarations *)
595

596
pdecl:
597
| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
598
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
599
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
600
| LET REC with_list1(rec_defn)                      { Drec $3 }
601 602
| EXCEPTION labels(uident)                          { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident) ty                       { Dexn ($2, $3) }
603

604 605 606 607 608 609
top_ghost:
| (* epsilon *) { Gnone  }
| GHOST         { Gghost }
| LEMMA         { Glemma }

(* Function declarations *)
610 611

type_v:
612
| arrow_type_v  { $1 }
613
| cast          { PTpure $1 }
614 615

arrow_type_v:
616
| param params tail_type_c  { PTfunc ($1 @ $2, $3) }
617 618

tail_type_c:
619 620
| single_spec spec arrow_type_v { $3, spec_union $1 $2 }
| COLON simple_type_c           { $2 }
621 622

simple_type_c:
623 624 625
| ty spec { PTpure $1, $2 }

(* Function definitions *)
626

627
rec_defn:
628
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
629
    { $2, $1, ($3, $4, $8, spec_union $5 $7) }
630

631
fun_defn:
632
| binders cast? spec EQUAL spec seq_expr { ($1, $2, $6, spec_union $3 $5) }
633

634
fun_expr:
635 636
| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }

637 638 639 640 641 642 643 644
(* 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 }
645

646
expr: e = mk_expr(expr_) { e }
647 648 649

expr_:
| expr_arg_
650 651
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
652
| NOT expr %prec prec_prefix_op
653
    { Enot $2 }
654
| prefix_op expr %prec prec_prefix_op
655 656 657 658 659 660 661 662
    { Eidapp (Qident $1, [$2]) }
| l = expr ; o = lazy_op ; r = expr
    { Elazy (l,o,r) }
| l = expr ; o = infix_op ; r = expr
    { Einfix (l,o,r) }
| expr_arg located(expr_arg)+ (* FIXME/TODO: "expr expr_arg" *)
    { let join f (a,_,e) = mk_expr (Eapply (f,a)) $startpos e in
      (List.fold_left join $1 $2).expr_desc }
663
| IF seq_expr THEN expr ELSE expr
664
    { Eif ($2, $4, $6) }
665
| IF seq_expr THEN expr %prec prec_no_else
666 667 668 669 670 671 672
    { 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 }
673
| LET top_ghost pattern EQUAL seq_expr IN seq_expr
674
    { match $3.pat_desc with
675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696
      | 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) }
697
| LET REC with_list1(rec_defn) IN seq_expr
698
    { Erec ($3, $5) }
699
| fun_expr
700 701 702 703 704 705 706
    { 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) }
707
| quote_uident COLON seq_expr
708
    { Emark ($1, $3) }
709
| LOOP loop_annotation seq_expr END
710
    { Eloop ($2, $3) }
711
| WHILE seq_expr DO loop_annotation seq_expr DONE
712 713 714
    { Ewhile ($2, $4, $5) }
| FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
    { Efor ($2, $4, $5, $6, $8, $9) }
715
| ABSURD
716
    { Eabsurd }
717
| RAISE uqualid
718
    { Eraise ($2, None) }
719
| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
720 721 722
    { Eraise ($3, Some $4) }
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
723
| ANY simple_type_c
724
    { Eany $2 }
725
| GHOST expr
726
    { Eghost $2 }
727
| ABSTRACT spec seq_expr END
728 729 730
    { Eabstract($3, $2) }
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
731
| label expr %prec prec_named
732 733 734
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
735

736 737
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
738 739

expr_arg_:
740 741 742 743 744 745 746 747 748 749 750
| 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 }
751 752

expr_sub:
753
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
754 755 756 757 758 759 760
| 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) }
761
| expr_arg LEFTSQ expr RIGHTSQ
762
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
763
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
764
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
765 766 767 768 769 770
| 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]) }
771

772 773 774 775 776 777 778
loop_annotation:
| (* epsilon *)
    { { loop_invariant = []; loop_variant = [] } }
| invariant loop_annotation
    { let a = $2 in { a with loop_invariant = $1 :: a.loop_invariant } }
| variant loop_annotation
    { let a = $2 in { a with loop_variant = variant_union $1 a.loop_variant } }
779

780 781
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
782

783 784
val_expr:
| tail_type_c { Eany $1 }
785

786 787 788
%inline lazy_op:
| AMPAMP  { LazyAnd }
| BARBAR  { LazyOr }
789 790

assertion_kind:
791 792 793
| ASSERT  { Aassert }
| ASSUME  { Aassume }
| CHECK   { Acheck }
794 795

for_direction:
796 797
| TO      { To }
| DOWNTO  { Downto }
798

799
(* Specification *)
800

801
spec:
802
| (* epsilon *)     { empty_spec }
803
| single_spec spec  { spec_union $1 $2 }
804

805
single_spec:
806
| REQUIRES LEFTBRC term RIGHTBRC
807 808
    { { empty_spec with sp_pre = [$3] } }
| ENSURES LEFTBRC ensures RIGHTBRC
809
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
810
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
811 812 813 814
    { { 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
815
    { { empty_spec with sp_reads = $3; sp_checkrw = true } }
816
| WRITES LEFTBRC comma_list0(term) RIGHTBRC
817
    { { empty_spec with sp_writes = $3; sp_checkrw = true } }
818 819
| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC
    { { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
820 821
| DIVERGES
    { { empty_spec with sp_diverge = true } }
822 823
| variant
    { { empty_spec with sp_variant = $1 } }
824

825
ensures:
826
| term
827
    { let id = mk_id "result" $startpos $endpos in
828
      [mk_pat (Pvar id) $startpos $endpos, $1] }
829

830
raises:
831 832 833
| uqualid ARROW term
    { $1, mk_pat (Ptuple []) $startpos($1) $endpos($1), $3 }
| uqualid pat_arg ARROW term
834
    { $1, $2, $4 }
835

836
xsymbol:
837
| uqualid
838
    { $1, mk_pat Pwild $startpos $endpos, mk_term Ttrue $startpos $endpos }
839

840
invariant:
841
| INVARIANT LEFTBRC term RIGHTBRC { $3 }
842

843
variant:
844
| VARIANT LEFTBRC comma_list1(single_variant) RIGHTBRC { $3 }
845

846
single_variant:
847
| term preceded(WITH,lqualid)? { $1, $2 }
848

849
(* Patterns *)
Jean-Christophe's avatar
Jean-Christophe committed
850

851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867
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) }
868
| mk_pat(pat_uni_) cast                 { Pcast($1,$2) }
869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924

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 }
| lident_keyword  { mk_id $1 $startpos $endpos }

lident_keyword:
| MODEL           { "model" }

quote_uident:
| QUOTE_UIDENT  { mk_id ("'" ^ $1) $startpos $endpos }

quote_lident:
| QUOTE_LIDENT  { mk_id $1 $startpos $endpos }

opaque_quote_lident:
| OPAQUE_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 "[]<-" }