parser.mly 29.3 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 14

%{
  open Ptree

15
  let infix  s = "infix "  ^ s
16
  let prefix s = "prefix " ^ s
17
  let mixfix s = "mixfix " ^ s
18

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

21
  let floc s e = Loc.extract (s,e)
22

23
  let add_lab id l = { id with id_lab = l }
24

25
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
26

27
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
28

29 30
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
31 32 33
  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)
34

35 36
  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 }
37
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
38

39 40 41
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
42
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
43 44 45 46 47 48
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
49
    sp_reads   = [];
50 51
    sp_writes  = [];
    sp_variant = [];
52 53
    sp_checkrw = false;
    sp_diverge = false;
54
  }
55

56 57 58 59
  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;
60
    sp_reads   = s1.sp_reads @ s2.sp_reads;
61 62
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
63 64
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
65
  }
66

67
(* dead code
68
  let add_init_mark e =
69
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
70
    { e with expr_desc = Emark (init, e) }
71
*)
72

73
  let small_integer i =
74
    try match i with
75 76 77 78
      | 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)
79
    with Failure _ -> raise Error
80

81 82
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
83

84 85 86 87 88
  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
89 90
%}

91
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
92

93
%token <string> LIDENT UIDENT
94
%token <Ptree.integer_constant> INTEGER
95
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96 97
%token <Ptree.real_constant> FLOAT
%token <string> STRING
98
%token <Loc.position> POSITION
99
%token <string> QUOTE_UIDENT QUOTE_LIDENT
100

101
(* keywords *)
102

103
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
104 105 106
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
107
%token THEN THEORY TRUE TYPE USE WITH
108

109
(* program keywords *)
110

111 112
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
113
%token FUN GHOST INVARIANT LOOP MODULE MUTABLE
114 115
%token PRIVATE RAISE RAISES READS REC REQUIRES RETURNS
%token TO TRY VAL VARIANT WHILE WRITES
116

117
(* symbols *)
118

Andrei Paskevich's avatar
Andrei Paskevich committed
119
%token AND ARROW
120
%token BAR
121
%token COLON COMMA
122
%token DOT DOTDOT EQUAL LAMBDA LTGT
123
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
124
%token LARROW LRARROW OR
125
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
126
%token UNDERSCORE
127 128 129

%token EOF

130
(* program symbols *)
131

132
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
133

134
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
135

136
%nonassoc IN
137 138 139
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
140
%nonassoc prec_no_else
141
%nonassoc DOT ELSE GHOST
142
%nonassoc prec_named
143
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
144

Andrei Paskevich's avatar
Andrei Paskevich committed
145
%right ARROW LRARROW
146 147
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
148
%nonassoc NOT
149
%left EQUAL LTGT OP1
150
%nonassoc LARROW
151
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
152
%left OP2
153
%left OP3
154
%left OP4
155
%nonassoc prec_prefix_op
156 157
%nonassoc LEFTSQ
%nonassoc OPPREF
158

159
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
160

161
%start <Pmodule.pmodule Stdlib.Mstr.t> mlw_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
162 163
%%

164 165
(* Theories, modules, namespaces *)

166 167 168 169 170
mlw_file:
| theory_or_module* EOF { Typing.close_file () }
(* TODO
| module_decl* EOF { Typing.close_file () }
*)
171

172
theory_or_module:
173 174
| module_head module_decl* END
    { Typing.close_module (floc $startpos($3) $endpos($3)) }
175

176
module_head:
177 178
| THEORY labels(uident)  { Typing.open_module $2 ~theory:true  }
| MODULE labels(uident)  { Typing.open_module $2 ~theory:false }
179

180
module_decl:
181 182
| decl            { Typing.add_decl  (floc $startpos $endpos) $1 }
| use_clone       { Typing.use_clone (floc $startpos $endpos) $1 }
183
| namespace_head module_decl* END
184
    { Typing.close_namespace (floc $startpos($1) $endpos($1)) ~import:$1 }
185

186
namespace_head:
187
| NAMESPACE boption(IMPORT) uident  { Typing.open_namespace $3; $2 }
188

189
(* Use and clone *)
190

191
use_clone:
192 193 194
| USE use                                 { ($2, None) }
| CLONE use                               { ($2, Some []) }
| CLONE use WITH comma_list1(clone_subst) { ($2, Some $4) }
195

196
use:
197
| boption(IMPORT) tqualid
Andrei Paskevich's avatar
Andrei Paskevich committed
198
    { { use_module = $2; use_import = Some ($1, qualid_last $2) } }
199
| boption(IMPORT) tqualid AS uident
Andrei Paskevich's avatar
Andrei Paskevich committed
200
    { { use_module = $2; use_import = Some ($1, $4.id_str) } }
201
| EXPORT tqualid
Andrei Paskevich's avatar
Andrei Paskevich committed
202
    { { use_module = $2; use_import = None } }
203

204
clone_subst:
205 206
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
207 208 209 210 211 212
| 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) }
213

214 215 216
ns:
| uqualid { Some $1 }
| DOT     { None }
217

218 219 220 221 222 223 224 225 226 227 228 229 230
(* Theory declarations *)

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

meta_arg:
234 235 236 237 238 239 240
| 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) }
241 242

(* Type declarations *)
243 244

type_decl:
245 246
| labels(lident) ty_var* typedefn invariant*
  { let (vis, mut), def = $3 in
247
    { td_ident = $1; td_params = $2;
248 249 250
      td_vis = vis; td_mut = mut;
      td_inv = $4; td_def = def;
      td_loc = floc $startpos $endpos } }
251

252
ty_var:
253
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
254

255 256 257 258 259 260 261 262
(* TODO: should global "mutable" imply "private"?
  "type t 'a = mutable { x : int }"
    - if "x" is immutable then the type can only be private
    - if "x" is automatically mutable then I don't like it
    - if there are known mutable fields, then a global "mutable"
      is redundant, unless it also means "private" *)
(* TODO: what should be the syntax for mutable private records
    without known fields? *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
263
typedefn:
264
| (* epsilon *)
265 266 267 268 269 270 271 272 273 274 275 276 277 278
    { (Public, false), TDabstract }
| EQUAL vis_mut bar_list1(type_case)
    { $2, TDalgebraic $3 }
| EQUAL vis_mut LEFTBRC semicolon_list1(type_field) RIGHTBRC
    { $2, TDrecord $4 }
| EQUAL vis_mut ty
    { $2, TDalias $3 }

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

abstract:
281 282
| PRIVATE           { Private }
| ABSTRACT          { Abstract }
283

284 285 286 287
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 } }
288

289
field_modifiers:
290
| (* epsilon *) { false, false }
291 292 293 294 295
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

296
type_case:
297
| labels(uident) params { floc $startpos $endpos, $1, $2 }
298

299
(* Logic declarations *)
300

301 302
constant_decl:
| labels(lident_rich) cast preceded(EQUAL,term)?
303 304
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
305

306 307
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
308 309
  { { 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
310

311 312
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
313 314
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
315

316
with_logic_decl:
317
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
318 319
  { { 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
320

321
(* Inductive declarations *)
322 323

inductive_decl:
324
| labels(lident_rich) params ind_defn
325 326
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
327

328 329 330
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331

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

335
(* Type expressions *)
336

337 338 339 340
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
341

342 343
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
344
| quote_lident                      { PTtyvar $1 }
345 346 347
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
348

349 350
cast:
| COLON ty  { $2 }
351

352
(* Parameters and binders *)
353

354 355
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
356 357
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
358 359
   names, whose type must be inferred. *)

360
params:  param*  { List.concat $1 }
361

362
binders: binder+ { List.concat $1 }
363 364 365

param:
| anon_binder
366 367 368 369 370 371 372 373
    { 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 _, []) ->
374 375
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
376
| LEFTPAR binder_vars_rest RIGHTPAR
377
    { match $2 with [l,_] -> error_param l
378
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
379
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
380
    { match $3 with [l,_] -> error_param l
381 382
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
383
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
384
| LEFTPAR GHOST binder_vars cast RIGHTPAR
385
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
386

387 388
binder:
| anon_binder
389 390 391 392 393
    { error_param (floc $startpos $endpos) }
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
394 395
             [floc $startpos $endpos, Some id, false, None]
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
396 397 398
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
399 400
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
401 402 403
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident id, []) ->
404 405 406
             let id = add_lab id ($2::$3) in
             [floc $startpos $endpos, Some id, false, None]
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
407
| LEFTPAR binder_vars_rest RIGHTPAR
408
    { match $2 with [l,i] -> [l, i, false, None]
409
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
410
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
411
    { match $3 with [l,i] -> [l, i, true, None]
412 413
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
414
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
415
| LEFTPAR GHOST binder_vars cast RIGHTPAR
416
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
417

418 419 420
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
421

422
binder_vars_rest:
423 424 425 426 427 428 429
| 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*
430
   { List.rev_append $1 ($2 :: $3) }
431
| anon_binder binder_var*
432
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
433

434
binder_vars_head:
435
| ty {
436 437
    let of_id id = id.id_loc, Some id in
    let push acc = function
438
      | PTtyapp (Qident id, []) -> of_id id :: acc
439
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
440
    match $1 with
441
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
442
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
443

444
binder_var:
445 446
| labels(lident)  { floc $startpos $endpos, Some $1 }
| anon_binder     { $1 }
447 448

anon_binder:
449 450
| UNDERSCORE      { floc $startpos $endpos, None }

451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479
(* 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)
480 481 482 483 484
      | 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)
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 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526
      | _ -> 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]) }
527 528 529 530 531 532
| 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]) }
533

534 535
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
536

537 538
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
539

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

543 544 545
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
546

547 548 549 550 551 552 553
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
554

555 556 557 558
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
559

560 561 562
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
563

564
(* Program declarations *)
565

566
pdecl:
567
| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
568
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
569
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
570
| LET REC with_list1(rec_defn)                      { Drec $3 }
571 572
| EXCEPTION labels(uident)                          { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident) ty                       { Dexn ($2, $3) }
573

574 575 576 577 578 579
top_ghost:
| (* epsilon *) { Gnone  }
| GHOST         { Gghost }
| LEMMA         { Glemma }

(* Function declarations *)
580 581

type_v:
582
| params cast spec  { ($1, $2, $3) }
583

584
(*
585
simple_type_c:
586
| ty spec { PTpure $1, $2 }
587
*)
588 589

(* Function definitions *)
590

591
rec_defn:
592
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
593
    { $2, $1, ($3, $4, spec_union $5 $7, $8) }
594

595
fun_defn:
596
| binders cast? spec EQUAL spec seq_expr { ($1, $2, spec_union $3 $5, $6) }
597

598
fun_expr:
599
| FUN binders spec ARROW spec seq_expr { ($2, None, spec_union $3 $5, $6) }
600

601 602 603 604 605 606 607 608
(* 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 }
609

610
expr: e = mk_expr(expr_) { e }
611 612 613

expr_:
| expr_arg_
614 615
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
616 617 618 619
| expr AMPAMP expr
    { Eand ($1, $3) }
| expr BARBAR expr
    { Eor ($1, $3) }
620
| NOT expr %prec prec_prefix_op
621
    { Enot $2 }
622
| prefix_op expr %prec prec_prefix_op
623 624 625 626 627 628
    { Eidapp (Qident $1, [$2]) }
| 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 }
629
| IF seq_expr THEN expr ELSE expr
630
    { Eif ($2, $4, $6) }
631
| IF seq_expr THEN expr %prec prec_no_else
632 633 634 635 636 637 638
    { 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 }
639
| LET top_ghost pattern EQUAL seq_expr IN seq_expr
640
    { match $3.pat_desc with
641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662
      | 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) }
663
| LET REC with_list1(rec_defn) IN seq_expr
664
    { Erec ($3, $5) }
665
| fun_expr
666 667 668 669 670 671 672
    { 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) }
673
| quote_uident COLON seq_expr
674
    { Emark ($1, $3) }
675
| LOOP loop_annotation seq_expr END
676
    { let inv, var = $2 in Eloop (inv, var, $3) }
677
| WHILE seq_expr DO loop_annotation seq_expr DONE
678
    { let inv, var = $4 in Ewhile ($2, inv, var, $5) }
679 680
| FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
    { Efor ($2, $4, $5, $6, $8, $9) }
681
| ABSURD
682
    { Eabsurd }
683
| RAISE uqualid
684
    { Eraise ($2, None) }
685
| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
686 687 688
    { Eraise ($3, Some $4) }
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
689 690
| ANY ty spec
    { Eany ([], $2, $3) }
691
| GHOST expr
692
    { Eghost $2 }
693
| ABSTRACT spec seq_expr END
694
    { Eabstract($2, $3) }
695 696
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
697
| label expr %prec prec_named
698 699 700
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
701

702 703
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
704 705

expr_arg_:
706 707 708 709 710 711 712 713 714 715 716
| 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 }
717 718

expr_sub:
719
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
720 721 722 723 724 725 726
| 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) }
727
| expr_arg LEFTSQ expr RIGHTSQ
728
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
729
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
730
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
731 732 733 734 735 736
| 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]) }
737

738 739
loop_annotation:
| (* epsilon *)
740
    { [], [] }
741
| invariant loop_annotation
742
    { let inv, var = $2 in $1 :: inv, var }
743
| variant loop_annotation
744
    { let inv, var = $2 in inv, variant_union $1 var }
745

746 747
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
748

749
val_expr:
750
| type_v { Eany $1 }
751 752

assertion_kind:
753 754 755
| ASSERT  { Expr.Assert }
| ASSUME  { Expr.Assume }
| CHECK   { Expr.Check }
756 757

for_direction:
758 759
| TO      { Expr.To }
| DOWNTO  { Expr.DownTo }
760

761
(* Specification *)
762

763
spec:
764
| (* epsilon *)     { empty_spec }
765
| single_spec spec  { spec_union $1 $2 }
766

767
single_spec:
768
| REQUIRES LEFTBRC term RIGHTBRC
769 770
    { { empty_spec with sp_pre = [$3] } }
| ENSURES LEFTBRC ensures RIGHTBRC
771
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
772
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
773 774 775 776
    { { 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
777
    { { empty_spec with sp_reads = $3; sp_checkrw = true } }
778
| WRITES LEFTBRC comma_list0(term) RIGHTBRC
779
    { { empty_spec with sp_writes = $3; sp_checkrw = true } }
780 781
| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC
    { { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
782 783
| DIVERGES
    { { empty_spec with sp_diverge = true } }
784 785
| variant
    { { empty_spec with sp_variant = $1 } }
786

787
ensures:
788
| term
789
    { let id = mk_id "result" $startpos $endpos in
790
      [mk_pat (Pvar id) $startpos $endpos, $1] }
791

792
raises:
793 794 795
| uqualid ARROW term
    { $1, mk_pat (Ptuple []) $startpos($1) $endpos($1), $3 }
| uqualid pat_arg ARROW term
796
    { $1, $2, $4 }
797

798
xsymbol:
799
| uqualid
800
    { $1, mk_pat Pwild $startpos $endpos, mk_term Ttrue $startpos $endpos }
801

802
invariant:
803
| INVARIANT LEFTBRC term RIGHTBRC { $3 }
804

805
variant:
806
| VARIANT LEFTBRC comma_list1(single_variant) RIGHTBRC { $3 }
807

808
single_variant:
809
| term preceded(WITH,lqualid)? { $1, $2 }
810

811
(* Patterns *)
Jean-Christophe's avatar
Jean-Christophe committed
812

813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829
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) }
830
| mk_pat(pat_uni_) cast                 { Pcast($1,$2) }
831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 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

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 }

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

quote_lident:
| 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 "[]<-" }
880 881 882
| LEFTSQ UNDERSCORE DOTDOT UNDERSCORE RIGHTSQ { mixfix "[_.._]" }
| LEFTSQ            DOTDOT UNDERSCORE RIGHTSQ { mixfix "[.._]" }
| LEFTSQ UNDERSCORE DOTDOT            RIGHTSQ { mixfix "[_..]" }
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

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 *)

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

any_qualid:
| sident                { Qident $1 }
| any_qualid DOT sident { Qdot ($1, $3) }

sident:
| ident   { $1 }
| STRING  { mk_id $1 $startpos $endpos }

(* Labels and position markers *)

labels(X): X label* { add_lab $1 $2 }

label:
| STRING    { Lstr (Ident.create_label $1) }
| POSITION  { Lpos $1 }

(* Miscellaneous *)
945 946

bar_list1(X):
947
| ioption(BAR) ; xl = separated_nonempty_list(BAR, X) { xl }
948 949