parser.mly 33.4 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11 12

%{
13
module Increment = struct
14 15 16 17 18 19 20
  let stack = Stack.create ()
  let open_file inc = Stack.push inc stack
  let close_file () = ignore (Stack.pop stack)
  let open_theory id = (Stack.top stack).Ptree.open_theory id
  let close_theory () = (Stack.top stack).Ptree.close_theory ()
  let open_module id = (Stack.top stack).Ptree.open_module id
  let close_module () = (Stack.top stack).Ptree.close_module ()
21 22
  let open_namespace n = (Stack.top stack).Ptree.open_namespace n
  let close_namespace l b = (Stack.top stack).Ptree.close_namespace l b
23 24 25
  let new_decl loc d = (Stack.top stack).Ptree.new_decl loc d
  let new_pdecl loc d = (Stack.top stack).Ptree.new_pdecl loc d
  let use_clone loc use = (Stack.top stack).Ptree.use_clone loc use
26
end
27

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

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

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

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

38
  let model_label = Ident.create_label "model"
39
  let model_projected = Ident.create_label "model_projected"
40 41 42 43 44

  let is_model_label l =
    match l with
    | Lpos _ -> false
    | Lstr lab ->
45 46
      (lab = model_label) || (lab = model_projected)

47

48
  let model_lab_present labels =
49 50 51 52 53 54 55 56 57 58 59
    try
      ignore(List.find is_model_label labels);
      true
    with Not_found ->
      false

  let model_trace_regexp = Str.regexp "model_trace:"

  let is_model_trace_label l =
    match l with
    | Lpos _ -> false
60
    | Lstr lab ->
61
      try
62
	ignore(Str.search_forward model_trace_regexp lab.Ident.lab_string 0);
63 64 65 66 67 68 69 70 71 72 73
	true
      with Not_found -> false

  let model_trace_lab_present labels =
    try
      ignore(List.find is_model_trace_label labels);
      true
    with Not_found ->
      false

  let add_model_trace name labels =
74
    if (model_lab_present labels) && (not (model_trace_lab_present labels)) then
75 76
      (Lstr (Ident.create_label ("model_trace:" ^ name)))::labels
    else
77
      labels
78 79 80 81

  let add_lab id l =
    let l = add_model_trace id.id_str l in
    { id with id_lab = l }
82

83
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
84

85
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
86

87 88
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
89 90 91
  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)
92

93 94
  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 }
95
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
96

97 98 99
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
100
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
101 102 103 104 105 106
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
107
    sp_reads   = [];
108 109
    sp_writes  = [];
    sp_variant = [];
110 111
    sp_checkrw = false;
    sp_diverge = false;
112
  }
113

114 115 116 117
  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;
118
    sp_reads   = s1.sp_reads @ s2.sp_reads;
119 120
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
121 122
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
123
  }
124

125
(* dead code
126
  let add_init_mark e =
127
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
128
    { e with expr_desc = Emark (init, e) }
129
*)
130

131
  let small_integer i =
132
    try match i with
133 134 135 136
      | 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)
137
    with Failure _ -> raise Error
138

139 140
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
141

142 143 144 145 146
  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
147 148
%}

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

Clément Fumex's avatar
Clément Fumex committed
151
%token <string> LIDENT LIDENT_QUOTE UIDENT UIDENT_QUOTE
152
%token <Ptree.integer_constant> INTEGER
153
%token <string> OP1 OP2 OP3 OP4 OPPREF
Clément Fumex's avatar
Clément Fumex committed
154
%token <Ptree.real_constant> REAL
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155
%token <string> STRING
156
%token <Loc.position> POSITION
157
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
158

159
(* keywords *)
160

Martin Clochard's avatar
Martin Clochard committed
161
%token AS AXIOM BY CLONE COINDUCTIVE CONSTANT
Clément Fumex's avatar
Clément Fumex committed
162
%token ELSE END EPSILON EXISTS EXPORT FALSE FLOAT FORALL FUNCTION
Andrei Paskevich's avatar
Andrei Paskevich committed
163
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
Clément Fumex's avatar
Clément Fumex committed
164
%token LET MATCH META NAMESPACE NOT PROP PREDICATE RANGE
Martin Clochard's avatar
Martin Clochard committed
165
%token SO THEN THEORY TRUE TYPE USE WITH
166

167
(* program keywords *)
168

169 170 171 172 173
%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
174

175
(* symbols *)
176

Andrei Paskevich's avatar
Andrei Paskevich committed
177
%token AND ARROW
178
%token BAR
179
%token COLON COMMA
Clément Fumex's avatar
Clément Fumex committed
180
%token DOT DOTDOT EQUAL LAMBDA LT GT LTGT
181
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
182
%token LARROW LRARROW OR
183
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
184
%token UNDERSCORE
185 186 187

%token EOF

188
(* program symbols *)
189

190
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
191

192
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193

194
%nonassoc IN
195 196 197
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
198
%nonassoc prec_no_else
199
%nonassoc DOT ELSE GHOST
200
%nonassoc prec_named
201
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
202

Andrei Paskevich's avatar
Andrei Paskevich committed
203
%right ARROW LRARROW
Martin Clochard's avatar
Martin Clochard committed
204
%right BY SO
205 206
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
207
%nonassoc NOT
Clément Fumex's avatar
Clément Fumex committed
208
%left EQUAL LTGT LT GT OP1
209
%nonassoc LARROW
210
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
211
%left OP2
212
%left OP3
213
%left OP4
214
%nonassoc prec_prefix_op
215 216
%nonassoc LEFTSQ
%nonassoc OPPREF
217

218
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
219

220 221
%start <Ptree.incremental -> unit> open_file
%start <unit> logic_file program_file
222
%start <Ptree.term> term_eof
223
%start <Ptree.ident list> ident_comma_list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
224 225
%%

226 227 228 229 230
(* parsing of a single term *)

term_eof:
| term EOF { $1 }

231 232
(* Theories, modules, namespaces *)

233
open_file:
234
(* Dummy token. Menhir does not accept epsilon. *)
235
| EOF { Increment.open_file }
236

237
logic_file:
238
| theory* EOF   { Increment.close_file () }
239

240
program_file:
241
| theory_or_module* EOF { Increment.close_file () }
242

243
theory:
244
| theory_head theory_decl* END  { Increment.close_theory () }
245

246 247
theory_or_module:
| theory                        { () }
248
| module_head module_decl* END  { Increment.close_module () }
249

250
theory_head:
Clément Fumex's avatar
Clément Fumex committed
251
| THEORY labels(uident_nq)  { Increment.open_theory $2 }
252

253
module_head:
Clément Fumex's avatar
Clément Fumex committed
254
| MODULE labels(uident_nq)  { Increment.open_module $2 }
255

256
theory_decl:
257 258
| decl            { Increment.new_decl  (floc $startpos $endpos) $1 }
| use_clone       { Increment.use_clone (floc $startpos $endpos) $1 }
259
| namespace_head theory_decl* END
260
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
261

262
module_decl:
263 264 265
| decl            { Increment.new_decl  (floc $startpos $endpos) $1 }
| pdecl           { Increment.new_pdecl (floc $startpos $endpos) $1 }
| use_clone       { Increment.use_clone (floc $startpos $endpos) $1 }
266
| namespace_head module_decl* END
267
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
268

269
namespace_head:
Clément Fumex's avatar
Clément Fumex committed
270
| NAMESPACE boption(IMPORT) uident_nq
271
   { Increment.open_namespace $3.id_str; $2 }
272

273
(* Use and clone *)
274

275
use_clone:
276 277 278
| USE use                                 { ($2, None) }
| CLONE use                               { ($2, Some []) }
| CLONE use WITH comma_list1(clone_subst) { ($2, Some $4) }
279

280
use:
281
| boption(IMPORT) tqualid
282
    { { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
283 284
| boption(IMPORT) tqualid AS uident
    { { use_theory = $2; use_import = Some ($1, $4.id_str) } }
285 286
| EXPORT tqualid
    { { use_theory = $2; use_import = None } }
287

288
clone_subst:
289 290
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
291 292 293 294 295 296
| 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) }
297

298 299 300
ns:
| uqualid { Some $1 }
| DOT     { None }
301

302 303 304 305 306 307 308 309 310 311
(* 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) }
Clément Fumex's avatar
Clément Fumex committed
312 313 314
| AXIOM labels(ident_nq) COLON term         { Dprop (Decl.Paxiom, $2, $4) }
| LEMMA labels(ident_nq) COLON term         { Dprop (Decl.Plemma, $2, $4) }
| GOAL  labels(ident_nq) COLON term         { Dprop (Decl.Pgoal, $2, $4) }
315
| META sident comma_list1(meta_arg)         { Dmeta ($2, $3) }
316 317

meta_arg:
318 319 320 321 322 323 324
| 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) }
325 326

(* Type declarations *)
327 328

type_decl:
Clément Fumex's avatar
Clément Fumex committed
329
| labels(lident_nq) ty_var* typedefn
330
  { let model, vis, def, inv = $3 in
331
    let vis = if model then Abstract else vis in
332 333 334
    { td_ident = $1; td_params = $2;
      td_model = model; td_vis = vis; td_def = def;
      td_inv = inv; td_loc = floc $startpos $endpos } }
335

336
late_invariant:
Clément Fumex's avatar
Clément Fumex committed
337
| labels(lident_nq) ty_var* invariant+
338 339 340
  { { td_ident = $1; td_params = $2;
      td_model = false; td_vis = Public; td_def = TDabstract;
      td_inv = $3; td_loc = floc $startpos $endpos } }
341

342
ty_var:
343
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
344 345

typedefn:
346
| (* epsilon *)
347
    { false, Public, TDabstract, [] }
348
| model abstract bar_list1(type_case) invariant*
349
    { $1, $2, TDalgebraic $3, $4 }
350
| model abstract LEFTBRC semicolon_list1(type_field) RIGHTBRC invariant*
351
    { $1, $2, TDrecord $4, $6 }
352 353
| model abstract ty invariant*
    { $1, $2, TDalias $3, $4 }
Clément Fumex's avatar
Clément Fumex committed
354 355 356 357 358 359 360
(* FIXME: allow negative bounds *)
| EQUAL LT RANGE INTEGER INTEGER GT
    { false, Public,
      TDrange (Number.compute_int $4, Number.compute_int $5), [] }
| EQUAL LT FLOAT INTEGER INTEGER GT
    { false, Public,
      TDfloat (small_integer $4, small_integer $5), [] }
361

362 363 364 365 366
model:
| EQUAL         { false }
| MODEL         { true }

abstract:
367
| (* epsilon *) { Public }
368 369
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
370

371
type_field:
Clément Fumex's avatar
Clément Fumex committed
372
| field_modifiers labels(lident_nq) cast
373 374
  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
      f_pty = $3; f_loc = floc $startpos $endpos } }
375

376
field_modifiers:
377
| (* epsilon *) { false, false }
378 379 380 381 382
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

383
type_case:
Clément Fumex's avatar
Clément Fumex committed
384
| labels(uident_nq) params { floc $startpos $endpos, $1, $2 }
385

386
(* Logic declarations *)
387

388 389
constant_decl:
| labels(lident_rich) cast preceded(EQUAL,term)?
390 391
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
392

393 394
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
395 396
  { { 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
397

398 399
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
400 401
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
402

403
with_logic_decl:
404
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
405 406
  { { 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
407

408
(* Inductive declarations *)
409 410

inductive_decl:
411
| labels(lident_rich) params ind_defn
412 413
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
414

415 416 417
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
418

419
ind_case:
Clément Fumex's avatar
Clément Fumex committed
420
| labels(ident_nq) COLON term  { floc $startpos $endpos, $1, $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
421

422
(* Type expressions *)
423

424 425 426 427
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
428

429 430 431 432 433 434 435
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 }
436

437 438
cast:
| COLON ty  { $2 }
439

440
(* Parameters and binders *)
441

442 443
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
444 445
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
446 447
   names, whose type must be inferred. *)

448
params:  param*  { List.concat $1 }
449

450
binders: binder+ { List.concat $1 }
451 452 453

param:
| anon_binder
454 455 456 457 458 459 460 461
    { 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 _, []) ->
462 463
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
464
| LEFTPAR binder_vars_rest RIGHTPAR
465
    { match $2 with [l,_] -> error_param l
466
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
467
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
468
    { match $3 with [l,_] -> error_param l
469 470
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
471
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
472
| LEFTPAR GHOST binder_vars cast RIGHTPAR
473
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
474

475 476
binder:
| anon_binder
477 478 479 480 481
    { error_param (floc $startpos $endpos) }
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
482 483
             [floc $startpos $endpos, Some id, false, None]
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
484 485 486
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
487 488
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
489 490 491
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident id, []) ->
492 493 494
             let id = add_lab id ($2::$3) in
             [floc $startpos $endpos, Some id, false, None]
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
495
| LEFTPAR binder_vars_rest RIGHTPAR
496
    { match $2 with [l,i] -> [l, i, false, None]
497
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
498
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
499
    { match $3 with [l,i] -> [l, i, true, None]
500 501
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
502
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
503
| LEFTPAR GHOST binder_vars cast RIGHTPAR
504
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
505

506 507 508
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
509

510
binder_vars_rest:
511 512 513 514 515 516 517
| 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*
518
   { List.rev_append $1 ($2 :: $3) }
519
| anon_binder binder_var*
520
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
521

522
binder_vars_head:
523
| ty {
524 525
    let of_id id = id.id_loc, Some id in
    let push acc = function
526
      | PTtyapp (Qident id, []) -> of_id id :: acc
527
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
528
    match $1 with
529
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
530
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
531

532
binder_var:
Clément Fumex's avatar
Clément Fumex committed
533 534
| labels(lident_nq) { floc $startpos $endpos, Some $1 }
| anon_binder       { $1 }
535 536

anon_binder:
Clément Fumex's avatar
Clément Fumex committed
537
| UNDERSCORE        { floc $startpos $endpos, None }
538

539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567
(* 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)
568 569 570 571 572
      | 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)
573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614
      | _ -> 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]) }
615 616 617 618 619 620
| 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]) }
621

622 623
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
624

625 626
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
627

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

631 632 633
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
634

635 636 637 638 639 640 641
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
Martin Clochard's avatar
Martin Clochard committed
642 643
| BY      { Tby }
| SO      { Tso }
644

645 646 647 648
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
649

650 651
numeral:
| INTEGER { Number.ConstInt $1 }
Clément Fumex's avatar
Clément Fumex committed
652
| REAL    { Number.ConstReal $1 }
653

654
(* Program declarations *)
655

656
pdecl:
657
| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
658
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
659
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
660
| LET REC with_list1(rec_defn)                      { Drec $3 }
Clément Fumex's avatar
Clément Fumex committed
661 662
| EXCEPTION labels(uident_nq)                       { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident_nq) ty                    { Dexn ($2, $3) }
663

664 665 666 667 668 669
top_ghost:
| (* epsilon *) { Gnone  }
| GHOST         { Gghost }
| LEMMA         { Glemma }

(* Function declarations *)
670 671

type_v:
672
| arrow_type_v  { $1 }
673
| cast          { PTpure $1 }
674 675

arrow_type_v:
676
| param params tail_type_c  { PTfunc ($1 @ $2, $3) }
677 678

tail_type_c:
679 680
| single_spec spec arrow_type_v { $3, spec_union $1 $2 }
| COLON simple_type_c           { $2 }
681 682

simple_type_c:
683 684 685
| ty spec { PTpure $1, $2 }

(* Function definitions *)
686

687
rec_defn:
688
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
689
    { $2, $1, ($3, $4, $8, spec_union $5 $7) }
690

691
fun_defn:
692
| binders cast? spec EQUAL spec seq_expr { ($1, $2, $6, spec_union $3 $5) }
693

694
fun_expr:
695 696
| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }

697 698 699 700 701 702 703 704
(* 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 }
705

706
expr: e = mk_expr(expr_) { e }
707 708 709

expr_:
| expr_arg_
710 711
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
712
| NOT expr %prec prec_prefix_op
713
    { Enot $2 }
714
| prefix_op expr %prec prec_prefix_op
715 716 717 718 719 720 721 722
    { 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 }
723
| IF seq_expr THEN expr ELSE expr
724
    { Eif ($2, $4, $6) }
725
| IF seq_expr THEN expr %prec prec_no_else
726 727 728 729 730 731 732
    { 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 }
733
| LET top_ghost pattern EQUAL seq_expr IN seq_expr
734
    { match $3.pat_desc with
735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752
      | 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) }
Clément Fumex's avatar
Clément Fumex committed
753
| LET top_ghost labels(lident_nq) fun_defn IN seq_expr
754 755 756
    { Efun ($3, $2, $4, $6) }
| LET top_ghost labels(lident_op_id) fun_defn IN seq_expr
    { Efun ($3, $2, $4, $6) }
757
| LET REC with_list1(rec_defn) IN seq_expr
758
    { Erec ($3, $5) }
759
| fun_expr
760 761 762 763 764 765 766
    { 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) }
767
| quote_uident COLON seq_expr
768
    { Emark ($1, $3) }
769
| LOOP loop_annotation seq_expr END
770
    { Eloop ($2, $3) }
771
| WHILE seq_expr DO loop_annotation seq_expr DONE
772 773 774
    { 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) }
775
| ABSURD
776
    { Eabsurd }
777
| RAISE uqualid
778
    { Eraise ($2, None) }
779
| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
780 781 782
    { Eraise ($3, Some $4) }
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
783
| ANY simple_type_c
784
    { Eany $2 }
785
| GHOST expr
786
    { Eghost $2 }
787
| ABSTRACT spec seq_expr END
788 789 790
    { Eabstract($3, $2) }
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
791
| label expr %prec prec_named
792 793 794
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
795

796 797
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
798 799

expr_arg_:
800 801 802 803 804 805 806 807 808 809 810
| 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 }
811 812

expr_sub:
813
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
814 815 816 817 818 819 820
| 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) }
821
| expr_arg LEFTSQ expr RIGHTSQ
822
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
823
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
824
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
825 826 827 828 829 830
| 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]) }
831

832 833 834 835 836 837 838
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 } }
839

840 841
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
842

843 844
val_expr:
| tail_type_c { Eany $1 }
845

846 847 848
%inline lazy_op:
| AMPAMP  { LazyAnd }
| BARBAR  { LazyOr }
849 850

assertion_kind:
851 852 853
| ASSERT  { Aassert }
| ASSUME  { Aassume }
| CHECK   { Acheck }
854 855

for_direction:
856 857
| TO      { To }
| DOWNTO  { Downto }
858

859
(* Specification *)
860

861
spec:
862
| (* epsilon *)     { empty_spec }
863
| single_spec spec  { spec_union $1 $2 }
864

865
single_spec:
866
| REQUIRES LEFTBRC term RIGHTBRC
867 868
    { { empty_spec with sp_pre = [$3] } }
| ENSURES LEFTBRC ensures RIGHTBRC
869
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
870
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
871 872 873 874
    { { 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