parser.mly 29.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 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 }
49
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
50

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

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

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

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

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

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

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

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

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

113
(* keywords *)
114

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

121
(* program keywords *)
122

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

129
(* symbols *)
130

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

%token EOF

142
(* program symbols *)
143

144
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
145

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

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

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

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

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

177 178
(* Theories, modules, namespaces *)

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

183
logic_file:
184
| theory* EOF   { Incremental.close_file () }
185

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

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

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

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

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

202 203 204 205 206
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 }
207

208 209 210 211 212 213
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 }
214

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

219
(* Use and clone *)
220

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

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

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

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

248 249 250 251 252 253 254 255 256 257 258 259 260 261
(* 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) }
262 263

meta_arg:
264 265 266 267 268 269 270
| 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) }
271 272

(* Type declarations *)
273 274

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

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

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

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

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

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

310 311 312 313
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 } }
314

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

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

325
(* Logic declarations *)
326

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

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

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

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

347
(* Inductive declarations *)
348 349

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

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

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

361
(* Type expressions *)
362

363 364 365 366
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
367

368 369 370 371 372 373 374
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 }
375

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

379
(* Parameters and binders *)
380

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

585
(* Program declarations *)
586

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

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

(* Function declarations *)
601 602

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

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

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

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

(* Function definitions *)
617

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

784
(* Specification *)
785

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

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

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

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

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

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

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

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

834
(* Patterns *)
Jean-Christophe's avatar
Jean-Christophe committed
835

836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852
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) }
853
| mk_pat(pat_uni_) cast                 { Pcast($1,$2) }
854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971

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

op_symbol:
| OP1 { $1 }
| OP2 { $1 }
| OP3 { $1 }
| OP4 { $1 }

%inline oppref:
| o = OPPREF { mk_id (prefix o)  $startpos $endpos }

prefix_op:
| op_symbol { mk_id (prefix $1)  $startpos $endpos }

%inline infix_op:
| o = OP1   { mk_id (infix o)    $startpos $endpos }
| o = OP2   { mk_id (infix o)    $startpos $endpos }
| o = OP3   { mk_id (infix o)    $startpos $endpos }
| o = OP4   { mk_id (infix o)    $startpos $endpos }
| EQUAL     { mk_id (infix "=")  $startpos $endpos }
| LTGT      { mk_id (infix "<>") $startpos $endpos }

(* Qualified idents *)

qualid:
| ident_rich              { Qident $1</