parser.mly 29.8 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 9
(*                                                                  *)
(*  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.                           *)
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
10 11

%{
12
module Incremental = struct
13 14 15 16 17 18 19
  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 ()
20 21
  let open_namespace n = (Stack.top stack).Ptree.open_namespace n
  let close_namespace l b = (Stack.top stack).Ptree.close_namespace l b
22 23 24
  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
25
end
26

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

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

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

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

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

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

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

43 44
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
45

46 47
  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 }
48
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
49

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

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

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

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

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

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

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

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

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

112
(* keywords *)
113

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

120
(* program keywords *)
121

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

128
(* symbols *)
129

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

%token EOF

141
(* program symbols *)
142

143
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
144

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

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

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

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

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

176 177
(* Theories, modules, namespaces *)

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

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

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

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

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

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

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

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

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

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

218
(* Use and clone *)
219

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

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

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

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

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

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

(* Type declarations *)
272 273

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

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

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

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

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

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

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

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

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

324
(* Logic declarations *)
325

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

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

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

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

346
(* Inductive declarations *)
347 348

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

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

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

360
(* Type expressions *)
361

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

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

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

378
(* Parameters and binders *)
379

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

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

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

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

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

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

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

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

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

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

477 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
(* 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)
506 507 508 509 510
      | 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)
511 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
      | _ -> 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]) }
553

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

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

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

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

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

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

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

584
(* Program declarations *)
585

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

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

(* Function declarations *)
600 601

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

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

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

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

(* Function definitions *)
616

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

783
(* Specification *)
784

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

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

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

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

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

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

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

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

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

835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851
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) }
852
| mk_pat(pat_uni_) cast                 { Pcast($1,$2) }
853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 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

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 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }

lqualid_rich:
| lident_rich             { Qident $1 }
| uqualid DOT lident_rich { Qdot ($1, $3) }

lqualid:
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }

uqualid:
| uident              { Qident $1 }
| uqualid DOT uident  { Qdot ($1, $3) }

(* Theory/Module names *)
<