parser.mly 34 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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
221 222
%%

223 224
(* Theories, modules, namespaces *)

225
open_file:
226
(* Dummy token. Menhir does not accept epsilon. *)
227
| EOF { Increment.open_file }
228

229
logic_file:
230
| theory* EOF   { Increment.close_file () }
231

232
program_file:
233
| theory_or_module* EOF { Increment.close_file () }
234

235
theory:
236
| theory_head theory_decl* END  { Increment.close_theory () }
237

238 239
theory_or_module:
| theory                        { () }
240
| module_head module_decl* END  { Increment.close_module () }
241

242
theory_head:
Clément Fumex's avatar
Clément Fumex committed
243
| THEORY labels(uident_nq)  { Increment.open_theory $2 }
244

245
module_head:
Clément Fumex's avatar
Clément Fumex committed
246
| MODULE labels(uident_nq)  { Increment.open_module $2 }
247

248
theory_decl:
249 250
| decl            { Increment.new_decl  (floc $startpos $endpos) $1 }
| use_clone       { Increment.use_clone (floc $startpos $endpos) $1 }
251
| namespace_head theory_decl* END
252
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
253

254
module_decl:
255 256 257
| 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 }
258
| namespace_head module_decl* END
259
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
260

261
namespace_head:
Clément Fumex's avatar
Clément Fumex committed
262
| NAMESPACE boption(IMPORT) uident_nq
263
   { Increment.open_namespace $3.id_str; $2 }
264

265
(* Use and clone *)
266

267
use_clone:
268 269 270
| USE use                                 { ($2, None) }
| CLONE use                               { ($2, Some []) }
| CLONE use WITH comma_list1(clone_subst) { ($2, Some $4) }
271

272
use:
273
| boption(IMPORT) tqualid
274
    { { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
275 276
| boption(IMPORT) tqualid AS uident
    { { use_theory = $2; use_import = Some ($1, $4.id_str) } }
277 278
| EXPORT tqualid
    { { use_theory = $2; use_import = None } }
279

280
clone_subst:
281 282
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
283 284 285 286 287 288
| 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) }
289

290 291 292
ns:
| uqualid { Some $1 }
| DOT     { None }
293

294 295 296 297 298 299 300 301 302 303
(* 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
304 305 306
| 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) }
307
| META sident comma_list1(meta_arg)         { Dmeta ($2, $3) }
308 309

meta_arg:
310 311 312 313 314 315
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
| PROP      qualid  { Mpr $2 }
| STRING            { Mstr $1 }
316
| INTEGER           { Mint (Number.to_small_integer $1) }
317 318

(* Type declarations *)
319 320

type_decl:
Clément Fumex's avatar
Clément Fumex committed
321
| labels(lident_nq) ty_var* typedefn
322
  { let model, vis, def, inv = $3 in
323
    let vis = if model then Abstract else vis in
324 325 326
    { td_ident = $1; td_params = $2;
      td_model = model; td_vis = vis; td_def = def;
      td_inv = inv; td_loc = floc $startpos $endpos } }
327

328
late_invariant:
Clément Fumex's avatar
Clément Fumex committed
329
| labels(lident_nq) ty_var* invariant+
330 331 332
  { { td_ident = $1; td_params = $2;
      td_model = false; td_vis = Public; td_def = TDabstract;
      td_inv = $3; td_loc = floc $startpos $endpos } }
333

334
ty_var:
335
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
336 337

typedefn:
338
| (* epsilon *)
339
    { false, Public, TDabstract, [] }
340
| model abstract bar_list1(type_case) invariant*
341
    { $1, $2, TDalgebraic $3, $4 }
342
| model abstract LEFTBRC semicolon_list1(type_field) RIGHTBRC invariant*
343
    { $1, $2, TDrecord $4, $6 }
344 345
| model abstract ty invariant*
    { $1, $2, TDalias $3, $4 }
346 347
| EQUAL LT RANGE int_constant int_constant GT
    { false, Public, TDrange ($4, $5), [] }
Clément Fumex's avatar
Clément Fumex committed
348 349
| EQUAL LT FLOAT INTEGER INTEGER GT
    { false, Public,
350 351 352 353 354
      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) }
355

356 357 358 359 360
model:
| EQUAL         { false }
| MODEL         { true }

abstract:
361
| (* epsilon *) { Public }
362 363
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
364

365
type_field:
Clément Fumex's avatar
Clément Fumex committed
366
| field_modifiers labels(lident_nq) cast
367 368
  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
      f_pty = $3; f_loc = floc $startpos $endpos } }
369

370
field_modifiers:
371
| (* epsilon *) { false, false }
372 373 374 375 376
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

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

380
(* Logic declarations *)
381

382 383
constant_decl:
| labels(lident_rich) cast preceded(EQUAL,term)?
384 385
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
386

387 388
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
389 390
  { { 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
391

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

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

402
(* Inductive declarations *)
403 404

inductive_decl:
405
| labels(lident_rich) params ind_defn
406 407
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
408

409 410 411
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412

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

416
(* Type expressions *)
417

418 419 420 421
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
422

423 424 425 426 427 428 429
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 }
430

431 432
cast:
| COLON ty  { $2 }
433

434
(* Parameters and binders *)
435

436 437
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
438 439
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
440 441
   names, whose type must be inferred. *)

442
params:  param*  { List.concat $1 }
443

444
binders: binder+ { List.concat $1 }
445 446 447

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

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

500 501 502
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
503

504
binder_vars_rest:
505 506 507 508 509 510 511
| 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*
512
   { List.rev_append $1 ($2 :: $3) }
513
| anon_binder binder_var*
514
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
515

516
binder_vars_head:
517
| ty {
518 519
    let of_id id = id.id_loc, Some id in
    let push acc = function
520
      | PTtyapp (Qident id, []) -> of_id id :: acc
521
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
522
    match $1 with
523
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
524
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
525

526
binder_var:
Clément Fumex's avatar
Clément Fumex committed
527 528
| labels(lident_nq) { floc $startpos $endpos, Some $1 }
| anon_binder       { $1 }
529 530

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

533 534 535 536 537 538 539 540 541 542 543 544 545 546
(* 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]) }
547 548 549 550
| MINUS INTEGER
    { Tconst (Number.ConstInt (mk_int_const true $2)) }
| MINUS REAL
    { Tconst (Number.ConstReal (mk_real_const true $2)) }
551 552 553 554 555 556 557 558 559 560 561 562 563 564 565
| 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)
566 567 568 569 570
      | 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)
571 572 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
      | _ -> 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]) }
613 614 615 616 617 618
| 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]) }
619

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

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

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

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

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

643 644 645 646
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
647

648
numeral:
649 650 651
| INTEGER { Number.ConstInt (mk_int_const false $1) }
| REAL    { Number.ConstReal (mk_real_const false $1) }
 
652
(* Program declarations *)
653

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

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

(* Function declarations *)
668 669

type_v:
670
| arrow_type_v  { $1 }
671
| cast          { PTpure $1 }
672 673

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

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

simple_type_c:
681 682 683
| ty spec { PTpure $1, $2 }

(* Function definitions *)
684

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

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

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

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

704
expr: e = mk_expr(expr_) { e }
705 706 707

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

798 799
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
800 801

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

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

834 835 836 837 838 839 840
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 } }
841

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

845 846
val_expr:
| tail_type_c { Eany $1 }
847

848 849 850
%inline lazy_op:
| AMPAMP  { LazyAnd }
| BARBAR  { LazyOr }
851 852

assertion_kind:
853 854 855
| ASSERT  { Aassert }
| ASSUME  { Aassume }
| CHECK   { Acheck }
856 857

for_direction:
858 859
| TO      { To }
| DOWNTO  { Downto }
860

861
(* Specification *)
862

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

867
single_spec:
868
| REQUIRES LEFTBRC term RIGHTBRC
869 870
    { { empty_spec with sp_pre = [$3] } }
| ENSURES LEFTBRC ensures RIGHTBRC
871
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
872
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
873 874 875 876
    { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
| RAISES LEFTBRC bar_list1(raises) RIGHTBRC
    {