parser.mly 34.5 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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 86 87 88 89 90
  let mk_int_const neg lit =
    Number.{ ic_negative = neg ; ic_abs = lit}

  let mk_real_const neg lit =
    Number.{ rc_negative = neg ; rc_abs = lit}

91
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
92

93 94
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
95 96 97
  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)
98

99 100
  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 }
101
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
102

103 104 105
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
106
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
107 108 109 110 111 112
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
113
    sp_reads   = [];
114 115
    sp_writes  = [];
    sp_variant = [];
116 117
    sp_checkrw = false;
    sp_diverge = false;
118
  }
119

120 121 122 123
  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;
124
    sp_reads   = s1.sp_reads @ s2.sp_reads;
125 126
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
127 128
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
129
  }
130

131
(* dead code
132
  let add_init_mark e =
133
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
134
    { e with expr_desc = Emark (init, e) }
135
*)
136

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

140 141 142 143 144
  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
145 146
%}

147
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
148

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

157
(* keywords *)
158

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

165
(* program keywords *)
166

167 168 169 170 171
%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
172

173
(* symbols *)
174

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

%token EOF

186
(* program symbols *)
187

188
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
189

190
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
191

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

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

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

219 220
%start <Ptree.incremental -> unit> open_file
%start <unit> logic_file program_file
221
%start <Ptree.term> term_eof
222 223
%start <Ptree.qualid> qualid_eof
%start <Ptree.qualid list> qualid_comma_list_eof
224
%start <Ptree.term list> term_comma_list_eof
225
%start <Ptree.ident list> ident_comma_list_eof
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
226 227
%%

228 229 230 231 232
(* parsing of a single term *)

term_eof:
| term EOF { $1 }

233 234
(* Theories, modules, namespaces *)

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

239
logic_file:
240
| theory* EOF   { Increment.close_file () }
241

242
program_file:
243
| theory_or_module* EOF { Increment.close_file () }
244

245
theory:
246
| theory_head theory_decl* END  { Increment.close_theory () }
247

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

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

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

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

264
module_decl:
265 266 267
| 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 }
268
| namespace_head module_decl* END
269
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
270

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

275
(* Use and clone *)
276

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

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

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

300 301 302
ns:
| uqualid { Some $1 }
| DOT     { None }
303

304 305 306 307 308 309 310 311 312 313
(* 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
314 315 316
| 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) }
317
| META sident comma_list1(meta_arg)         { Dmeta ($2, $3) }
318 319

meta_arg:
320 321 322 323 324 325
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
| PROP      qualid  { Mpr $2 }
| STRING            { Mstr $1 }
326
| INTEGER           { Mint (Number.to_small_integer $1) }
327 328

(* Type declarations *)
329 330

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

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

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

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

int_constant:
| INTEGER       { Number.compute_int_literal $1 }
| MINUS INTEGER { BigInt.minus (Number.compute_int_literal $2) }
365

366 367 368 369 370
model:
| EQUAL         { false }
| MODEL         { true }

abstract:
371
| (* epsilon *) { Public }
372 373
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
374

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

380
field_modifiers:
381
| (* epsilon *) { false, false }
382 383 384 385 386
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

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

390
(* Logic declarations *)
391

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

397 398
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
399 400
  { { 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
401

402 403
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
404 405
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
406

407
with_logic_decl:
408
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
409 410
  { { 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
411

412
(* Inductive declarations *)
413 414

inductive_decl:
415
| labels(lident_rich) params ind_defn
416 417
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
418

419 420 421
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
422

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

426
(* Type expressions *)
427

428 429 430 431
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
432

433 434 435 436 437 438 439
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 }
440

441 442
cast:
| COLON ty  { $2 }
443

444
(* Parameters and binders *)
445

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

452
params:  param*  { List.concat $1 }
453

454
binders: binder+ { List.concat $1 }
455 456 457

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

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

510 511 512
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
513

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

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

536
binder_var:
Clément Fumex's avatar
Clément Fumex committed
537 538
| labels(lident_nq) { floc $startpos $endpos, Some $1 }
| anon_binder       { $1 }
539 540

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

543 544 545 546 547 548 549 550 551 552 553 554 555 556
(* 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]) }
557 558 559 560
| MINUS INTEGER
    { Tconst (Number.ConstInt (mk_int_const true $2)) }
| MINUS REAL
    { Tconst (Number.ConstReal (mk_real_const true $2)) }
561 562 563 564 565 566 567 568 569 570 571 572 573 574 575
| 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)
576 577 578 579 580
      | 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)
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 615 616 617 618 619 620 621 622
      | _ -> 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]) }
623 624 625 626 627 628
| 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]) }
629

630 631
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
632

633 634
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
635

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

639 640 641
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
642

643 644 645 646 647 648 649
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
Martin Clochard's avatar
Martin Clochard committed
650 651
| BY      { Tby }
| SO      { Tso }
652

653 654 655 656
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
657

658
numeral:
659 660 661
| INTEGER { Number.ConstInt (mk_int_const false $1) }
| REAL    { Number.ConstReal (mk_real_const false $1) }
 
662
(* Program declarations *)
663

664
pdecl:
665
| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
666
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
667
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
668
| LET REC with_list1(rec_defn)                      { Drec $3 }
Clément Fumex's avatar
Clément Fumex committed
669 670
| EXCEPTION labels(uident_nq)                       { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident_nq) ty                    { Dexn ($2, $3) }
671

672 673 674 675 676 677
top_ghost:
| (* epsilon *) { Gnone  }
| GHOST         { Gghost }
| LEMMA         { Glemma }

(* Function declarations *)
678 679

type_v:
680
| arrow_type_v  { $1 }
681
| cast          { PTpure $1 }
682 683

arrow_type_v:
684
| param params tail_type_c  { PTfunc ($1 @ $2, $3) }
685 686

tail_type_c:
687 688
| single_spec spec arrow_type_v { $3, spec_union $1 $2 }
| COLON simple_type_c           { $2 }
689 690

simple_type_c:
691 692 693
| ty spec { PTpure $1, $2 }

(* Function definitions *)
694

695
rec_defn:
696
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
697
    { $2, $1, ($3, $4, $8, spec_union $5 $7) }
698

699
fun_defn:
700
| binders cast? spec EQUAL spec seq_expr { ($1, $2, $6, spec_union $3 $5) }
701

702
fun_expr:
703 704
| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }

705 706 707 708 709 710 711 712
(* 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 }
713

714
expr: e = mk_expr(expr_) { e }
715 716 717

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

808 809
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
810 811

expr_arg_:
812 813 814 815 816 817 818 819 820 821 822
| 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 }
823 824

expr_sub:
825
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
826 827 828 829 830 831 832
| 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) }
833
| expr_arg LEFTSQ expr RIGHTSQ
834
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
835
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
836
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
837 838 839 840 841 842
| 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]) }
843

844 845 846 847 848 849 850
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 } }
851

852 853
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
854

855 856
val_expr:
| tail_type_c { Eany $1 }
857

858 859 860
%inline lazy_op:
| AMPAMP  { LazyAnd }
| BARBAR  { LazyOr }
861 862

assertion_kind:
863 864 865
| ASSERT  { Aassert }
| ASSUME  { Aassume }
| CHECK   { Acheck }
866 867

for_direction:
868 869
| TO      { To }
| DOWNTO  { Downto }
870

871
(* Specification *)
872

873
spec:
874
| (* epsilon *)     { empty_spec }
875
| single_spec spec  { spec_union $1 $2 }
876

877
single_spec: