parser.mly 29.6 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_LIDENT
100

101
(* keywords *)
102

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

109
(* program keywords *)
110

111
%token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN CHECK
112
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
113
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
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 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 AT OLD
151
%nonassoc LARROW
152
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
153
%left OP2
154
%left OP3
155
%left OP4
156
%nonassoc prec_prefix_op
157 158
%nonassoc LEFTSQ
%nonassoc OPPREF
159

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

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

165 166
(* Theories, modules, namespaces *)

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

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

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

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

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

190
(* Use and clone *)
191

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

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

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

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

219 220 221 222 223 224 225 226 227 228 229 230 231
(* 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) }
232
| pdecl                                     { $1 }
233 234

meta_arg:
235 236 237 238
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
239 240 241
| AXIOM     qualid  { Max $2 }
| LEMMA     qualid  { Mlm $2 }
| GOAL      qualid  { Mgl $2 }
242 243
| STRING            { Mstr $1 }
| INTEGER           { Mint (small_integer $1) }
244 245

(* Type declarations *)
246 247

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

255
ty_var:
256
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
257

258 259 260 261 262 263 264 265
(* 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
266
typedefn:
267
| (* epsilon *)
268 269 270 271 272 273 274 275 276 277 278 279 280 281
    { (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 }
282 283

abstract:
284 285
| PRIVATE           { Private }
| ABSTRACT          { Abstract }
286

287 288 289 290
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 } }
291

292
field_modifiers:
293
| (* epsilon *) { false, false }
294 295 296 297 298
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

299
type_case:
300
| labels(uident) params { floc $startpos $endpos, $1, $2 }
301

302
(* Logic declarations *)
303

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

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

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

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

324
(* Inductive declarations *)
325 326

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

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

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

338
(* Type expressions *)
339

340 341 342 343
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
344

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

352 353
cast:
| COLON ty  { $2 }
354

355
(* Parameters and binders *)
356

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

363
params:  param*  { List.concat $1 }
364

365
binders: binder+ { List.concat $1 }
366 367 368

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

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

421 422 423
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
424

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

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

447
binder_var:
448 449
| labels(lident)  { floc $startpos $endpos, Some $1 }
| anon_binder     { $1 }
450 451

anon_binder:
452 453
| UNDERSCORE      { floc $startpos $endpos, None }

454 455 456 457 458 459 460 461 462 463 464 465
(* 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) }
466 467 468 469
| OLD term
    { Tat ($2, mk_id "0" $startpos($1) $endpos($1)) }
| term AT uident
    { Tat ($1, $3) }
470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
| 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)
487 488 489 490 491
      | 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)
492
      | _ -> Tmatch ($4, [$2, $6]) }
493 494 495 496 497 498
| LET labels(lident_op_id) EQUAL term IN term
    { Tlet ($2, $4, $6) }
| LET labels(lident) mk_term(lam_defn) IN term
    { Tlet ($2, $3, $5) }
| LET labels(lident_op_id) mk_term(lam_defn) IN term
    { Tlet ($2, $3, $5) }
499 500 501 502 503 504
| 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) }
505 506
| FUN binders ARROW term
    { Tquant (Tlambda, $2, [], $4) }
507 508 509 510 511 512 513
| EPSILON
    { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
| label term %prec prec_named
    { Tnamed ($1, $2) }
| term cast
    { Tcast ($1, $2) }

514 515 516
lam_defn:
| binders EQUAL term  { Tquant (Tlambda, $1, [], $3) }

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
term_arg: mk_term(term_arg_) { $1 }
term_dot: mk_term(term_dot_) { $1 }

term_arg_:
| qualid                    { Tident $1 }
| numeral                   { Tconst $1 }
| TRUE                      { Ttrue }
| FALSE                     { Tfalse }
| o = oppref ; a = term_arg { Tidapp (Qident o, [a]) }
| term_sub_                 { $1 }

term_dot_:
| lqualid                   { Tident $1 }
| o = oppref ; a = term_dot { Tidapp (Qident o, [a]) }
| term_sub_                 { $1 }

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]) }
544 545 546 547 548 549
| 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]) }
550

551 552
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
553

554 555
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
556

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

560 561 562
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
563

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

572 573 574
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
575

576 577 578
numeral:
| INTEGER { Number.ConstInt $1 }
| FLOAT   { Number.ConstReal $1 }
579

580
(* Program declarations *)
581

582
pdecl:
583 584
| VAL ghost kind labels(lident_rich) mk_expr(val_defn) { Dlet ($4, $2, $3, $5) }
| LET ghost kind labels(lident_rich) mk_expr(fun_defn) { Dlet ($4, $2, $3, $5) }
585
| LET ghost kind labels(lident_rich) EQUAL seq_expr    { Dlet ($4, $2, $3, $6) }
586 587 588 589 590 591 592 593 594 595 596 597 598 599
| LET REC with_list1(rec_defn)                         { Drec $3 }
| EXCEPTION labels(uident)                             { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident) ty                          { Dexn ($2, $3) }

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

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

(* Function definitions *)
602

603
rec_defn:
604 605
| ghost kind labels(lident_rich) binders cast? spec EQUAL spec seq_expr
    { $3, $1, $2, $4, $5, spec_union $6 $8, $9 }
606

607
fun_defn:
608
| binders cast? spec EQUAL spec seq_expr
609
    { Efun ($1, $2, spec_union $3 $5, $6) }
610

611 612
val_defn:
| params cast spec  { Eany ($1, $2, $3) }
613

614 615 616 617 618 619 620 621
(* 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 }
622

623
expr: e = mk_expr(expr_) { e }
624 625 626

expr_:
| expr_arg_
627 628
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
629 630 631 632
| expr AMPAMP expr
    { Eand ($1, $3) }
| expr BARBAR expr
    { Eor ($1, $3) }
633
| NOT expr
634
    { Enot $2 }
635
| prefix_op expr %prec prec_prefix_op
636 637 638 639 640 641
    { 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 }
642
| IF seq_expr THEN expr ELSE expr
643
    { Eif ($2, $4, $6) }
644
| IF seq_expr THEN expr %prec prec_no_else
645 646 647 648 649 650 651
    { 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 }
652 653 654 655 656 657
| LET ghost kind pattern EQUAL seq_expr IN seq_expr
    { match $4.pat_desc with
      | Pvar id -> Elet (id, $2, $3, $6, $8)
      | Pwild -> Elet (id_anonymous $4.pat_loc, $2, $3, $6, $8)
      | Ptuple [] -> Elet (id_anonymous $4.pat_loc, $2, $3,
          { $6 with expr_desc = Ecast ($6, PTtuple []) }, $8)
658
      | Pcast ({pat_desc = Pvar id}, ty) ->
659
          Elet (id, $2, $3, { $6 with expr_desc = Ecast ($6, ty) }, $8)
660
      | Pcast ({pat_desc = Pwild}, ty) ->
661 662
          let id = id_anonymous $4.pat_loc in
          Elet (id, $2, $3, { $6 with expr_desc = Ecast ($6, ty) }, $8)
663
      | _ ->
664 665 666 667 668 669 670 671 672 673 674
          let e = if $2 then { $6 with expr_desc = Eghost $6 } else $6 in
          (match $3 with
          | Expr.RKnone -> Ematch (e, [$4, $8])
          | _ -> Loc.errorm ~loc:($4.pat_loc)
              "`let <kind>' cannot be used with complex patterns") }
| LET ghost kind labels(lident_op_id) EQUAL seq_expr IN seq_expr
    { Elet ($4, $2, $3, $6, $8) }
| LET ghost kind labels(lident) mk_expr(fun_defn) IN seq_expr
    { Elet ($4, $2, $3, $5, $7) }
| LET ghost kind labels(lident_op_id) mk_expr(fun_defn) IN seq_expr
    { Elet ($4, $2, $3, $5, $7) }
675
| LET REC with_list1(rec_defn) IN seq_expr
676
    { Erec ($3, $5) }
677
| FUN binders spec ARROW spec seq_expr
678 679 680
    { Efun ($2, None, spec_union $3 $5, $6) }
| ABSTRACT spec seq_expr END
    { Efun ([], None, $2, $3) }
681 682
| ANY ty spec
    { Eany ([], $2, $3) }
683 684
| VAL ghost kind labels(lident_rich) mk_expr(val_defn) IN seq_expr
    { Elet ($4, $2, $3, $5, $7) }
685 686 687 688
| 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) }
689 690
| LABEL labels(uident) IN seq_expr
    { Emark ($2, $4) }
691
| WHILE seq_expr DO loop_annotation seq_expr DONE
692
    { let inv, var = $4 in Ewhile ($2, inv, var, $5) }
693 694
| FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
    { Efor ($2, $4, $5, $6, $8, $9) }
695
| ABSURD
696
    { Eabsurd }
697 698 699 700
| RAISE uqualid expr_arg?
    { Eraise ($2, $3) }
| RAISE LEFTPAR uqualid expr_arg? RIGHTPAR
    { Eraise ($3, $4) }
701 702
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
703
| GHOST expr
704 705 706
    { Eghost $2 }
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
707
| label expr %prec prec_named
708 709 710
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
711

712 713
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
714 715

expr_arg_:
716 717 718 719 720 721 722 723 724 725 726
| 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 }
727 728

expr_sub:
729
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
730 731 732 733 734 735 736
| 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) }
737
| expr_arg LEFTSQ expr RIGHTSQ
738
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
739
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
740
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
741 742 743 744 745 746
| 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]) }
747

748 749
loop_annotation:
| (* epsilon *)
750
    { [], [] }
751
| invariant loop_annotation
752
    { let inv, var = $2 in $1 :: inv, var }
753
| variant loop_annotation
754
    { let inv, var = $2 in inv, variant_union $1 var }
755

756 757
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
758 759

assertion_kind:
760 761 762
| ASSERT  { Expr.Assert }
| ASSUME  { Expr.Assume }
| CHECK   { Expr.Check }
763 764

for_direction:
765 766
| TO      { Expr.To }
| DOWNTO  { Expr.DownTo }
767

768
(* Specification *)
769

770
spec:
771
| (* epsilon *)     { empty_spec }
772
| single_spec spec  { spec_union $1 $2 }
773

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

794
ensures:
795
| term
796
    { let id = mk_id "result" $startpos $endpos in
797
      [mk_pat (Pvar id) $startpos $endpos, $1] }
798

799
raises:
800 801 802
| uqualid ARROW term
    { $1, mk_pat (Ptuple []) $startpos($1) $endpos($1), $3 }
| uqualid pat_arg ARROW term
803
    { $1, $2, $4 }
804

805
xsymbol:
806
| uqualid
807
    { $1, mk_pat Pwild $startpos $endpos, mk_term Ttrue $startpos $endpos }
808

809
invariant:
810
| INVARIANT LEFTBRC term RIGHTBRC { $3 }
811

812
variant:
813
| VARIANT LEFTBRC comma_list1(single_variant) RIGHTBRC { $3 }
814

815
single_variant:
816
| term preceded(WITH,lqualid)? { $1, $2 }
817

818
(* Patterns *)
Jean-Christophe's avatar
Jean-Christophe committed
819

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

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:
854
| UIDENT        { mk_id $1 $startpos $endpos }
855 856

lident:
857
| LIDENT        { mk_id $1 $startpos $endpos }
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

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 "[]<-" }
884 885 886
| LEFTSQ UNDERSCORE DOTDOT UNDERSCORE RIGHTSQ { mixfix "[_.._]" }
| LEFTSQ            DOTDOT UNDERSCORE RIGHTSQ { mixfix "[.._]" }
| LEFTSQ UNDERSCORE DOTDOT            RIGHTSQ { mixfix "[_..]" }
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

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: