parser.mly 35.7 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 qualid_last = function Qident x | Qdot (_, x) -> x.id_str
31

32
  let floc s e = Loc.extract (s,e)
33

34 35 36 37
  let debug_auto_model =
    Debug.register_flag ~desc:"When set, model labels are not added during parsing"
      "no_auto_model"

38
  let model_label = Ident.create_label "model"
39
(*  let model_projected = Ident.create_label "model_projected"*)
40

41
(*
42 43 44 45
  let is_model_label l =
    match l with
    | Lpos _ -> false
    | Lstr lab ->
46 47
      (lab = model_label) || (lab = model_projected)

48
  let model_lab_present labels =
49 50
    List.exists is_model_label labels
*)
51 52 53 54 55 56

  let model_trace_regexp = Str.regexp "model_trace:"

  let is_model_trace_label l =
    match l with
    | Lpos _ -> false
57
    | Lstr lab ->
58
      try
59
	ignore(Str.search_forward model_trace_regexp lab.Ident.lab_string 0);
60 61 62 63
	true
      with Not_found -> false

  let model_trace_lab_present labels =
64 65 66
    List.exists is_model_trace_label labels

  let add_model_trace id =
67 68
    if Debug.test_flag debug_auto_model || model_trace_lab_present id.id_lab
    then
69
      id
70
    else
71 72 73 74
      let l =
        (Lstr (Ident.create_label ("model_trace:" ^ id.id_str)))
        ::(Lstr model_label) :: id.id_lab in
      { id with id_lab = l }
75 76 77

  let add_lab id l =
    { id with id_lab = l }
78

79 80 81 82 83 84
  let add_model_labels (b : binder) =
    match b with
    | (loc, Some id, ghost, ty) ->
      (loc, Some (add_model_trace id), ghost, ty)
    | _ -> b

85 86 87 88 89 90 91 92 93 94 95
  let model_vc_label = Ident.create_label "model_vc"

  let model_vc_post_label = Ident.create_label "model_vc_post"

  let add_model_vc_label t =
    {t with term_desc = Tnamed (Lstr model_vc_label, t)}

  let add_model_vc_post_label t =
    {t with term_desc = Tnamed (Lstr model_vc_post_label, t)}


96
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
97

98 99 100 101 102 103
  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}

104
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
105

106 107 108 109 110
  let get_op s e = Qident (mk_id (Ident.mixfix "[]") s e)
  let set_op s e = Qident (mk_id (Ident.mixfix "[<-]") s e)
  let sub_op s e = Qident (mk_id (Ident.mixfix "[_.._]") s e)
  let above_op s e = Qident (mk_id (Ident.mixfix "[_..]") s e)
  let below_op s e = Qident (mk_id (Ident.mixfix "[.._]") s e)
111

112 113
  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 }
114
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
115

116 117 118
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
119
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
120 121 122 123 124 125
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
126
    sp_reads   = [];
127 128
    sp_writes  = [];
    sp_variant = [];
129 130
    sp_checkrw = false;
    sp_diverge = false;
131
  }
132

133 134 135 136
  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;
137
    sp_reads   = s1.sp_reads @ s2.sp_reads;
138 139
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
140 141
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
142
  }
143

144
(* dead code
145
  let add_init_mark e =
146
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
147
    { e with expr_desc = Emark (init, e) }
148
*)
149

150 151
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
152

153 154 155 156 157
  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
158 159
%}

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

Clément Fumex's avatar
Clément Fumex committed
162
%token <string> LIDENT LIDENT_QUOTE UIDENT UIDENT_QUOTE
163
%token <Number.integer_literal> INTEGER
164
%token <string> OP1 OP2 OP3 OP4 OPPREF
165
%token <Number.real_literal> REAL
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
166
%token <string> STRING
167
%token <Loc.position> POSITION
168
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
169

170
(* keywords *)
171

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

178
(* program keywords *)
179

180 181 182 183 184
%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
185

186
(* symbols *)
187

Andrei Paskevich's avatar
Andrei Paskevich committed
188
%token AND ARROW
189
%token BAR
190
%token COLON COMMA
191
%token DOT DOTDOT EQUAL LAMBDA LT GT LTGT MINUS
192
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
193
%token LARROW LRARROW OR
194
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
195
%token UNDERSCORE
196 197 198

%token EOF

199
(* program symbols *)
200

201
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
202

203
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
204

205
%nonassoc IN
206 207 208
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
209
%nonassoc prec_no_else
210
%nonassoc DOT ELSE GHOST
211
%nonassoc prec_named
212
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
213

Andrei Paskevich's avatar
Andrei Paskevich committed
214
%right ARROW LRARROW
Martin Clochard's avatar
Martin Clochard committed
215
%right BY SO
216 217
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
218
%nonassoc NOT
Clément Fumex's avatar
Clément Fumex committed
219
%left EQUAL LTGT LT GT OP1
220
%nonassoc LARROW
221
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
222
%left OP2 MINUS
223
%left OP3
224
%left OP4
225
%nonassoc prec_prefix_op
226
%nonassoc INTEGER REAL
227 228
%nonassoc LEFTSQ
%nonassoc OPPREF
229

230
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
231

232 233
%start <Ptree.incremental -> unit> open_file
%start <unit> logic_file program_file
234
%start <Ptree.term> term_eof
235 236
%start <Ptree.qualid> qualid_eof
%start <Ptree.qualid list> qualid_comma_list_eof
237
%start <Ptree.term list> term_comma_list_eof
238
%start <Ptree.ident list> ident_comma_list_eof
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
239 240
%%

241 242 243 244 245
(* parsing of a single term *)

term_eof:
| term EOF { $1 }

246 247
(* Theories, modules, namespaces *)

248
open_file:
249
(* Dummy token. Menhir does not accept epsilon. *)
250
| EOF { Increment.open_file }
251

252
logic_file:
253
| theory* EOF   { Increment.close_file () }
254

255
program_file:
256
| theory_or_module* EOF { Increment.close_file () }
257

258
theory:
259
| theory_head theory_decl* END  { Increment.close_theory () }
260

261 262
theory_or_module:
| theory                        { () }
263
| module_head module_decl* END  { Increment.close_module () }
264

265
theory_head:
Clément Fumex's avatar
Clément Fumex committed
266
| THEORY labels(uident_nq)  { Increment.open_theory $2 }
267

268
module_head:
Clément Fumex's avatar
Clément Fumex committed
269
| MODULE labels(uident_nq)  { Increment.open_module $2 }
270

271
theory_decl:
272 273
| decl            { Increment.new_decl  (floc $startpos $endpos) $1 }
| use_clone       { Increment.use_clone (floc $startpos $endpos) $1 }
274
| namespace_head theory_decl* END
275
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
276

277
module_decl:
278 279 280
| 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 }
281
| namespace_head module_decl* END
282
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
283

284
namespace_head:
Clément Fumex's avatar
Clément Fumex committed
285
| NAMESPACE boption(IMPORT) uident_nq
286
   { Increment.open_namespace $3.id_str; $2 }
287

288
(* Use and clone *)
289

290
use_clone:
291 292 293
| USE use                                 { ($2, None) }
| CLONE use                               { ($2, Some []) }
| CLONE use WITH comma_list1(clone_subst) { ($2, Some $4) }
294

295
use:
296
| boption(IMPORT) tqualid
297
    { { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
298 299
| boption(IMPORT) tqualid AS uident
    { { use_theory = $2; use_import = Some ($1, $4.id_str) } }
300 301
| EXPORT tqualid
    { { use_theory = $2; use_import = None } }
302

303
clone_subst:
304 305
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
306 307 308 309 310 311
| 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) }
312

313 314 315
ns:
| uqualid { Some $1 }
| DOT     { None }
316

317 318 319 320 321 322 323 324 325 326
(* 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
327 328 329
| 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) }
330
| META sident comma_list1(meta_arg)         { Dmeta ($2, $3) }
331 332

meta_arg:
333 334 335 336 337 338
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
| PROP      qualid  { Mpr $2 }
| STRING            { Mstr $1 }
339
| INTEGER           { Mint (Number.to_small_integer $1) }
340 341

(* Type declarations *)
342 343

type_decl:
Clément Fumex's avatar
Clément Fumex committed
344
| labels(lident_nq) ty_var* typedefn
345
  { let model, vis, def, inv = $3 in
346
    let vis = if model then Abstract else vis in
347 348 349
    { td_ident = $1; td_params = $2;
      td_model = model; td_vis = vis; td_def = def;
      td_inv = inv; td_loc = floc $startpos $endpos } }
350

351
late_invariant:
Clément Fumex's avatar
Clément Fumex committed
352
| labels(lident_nq) ty_var* invariant+
353 354 355
  { { td_ident = $1; td_params = $2;
      td_model = false; td_vis = Public; td_def = TDabstract;
      td_inv = $3; td_loc = floc $startpos $endpos } }
356

357
ty_var:
358
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
359 360

typedefn:
361
| (* epsilon *)
362
    { false, Public, TDabstract, [] }
363
| model abstract bar_list1(type_case) invariant*
364
    { $1, $2, TDalgebraic $3, $4 }
365
| model abstract LEFTBRC semicolon_list1(type_field) RIGHTBRC invariant*
366
    { $1, $2, TDrecord $4, $6 }
367 368
| model abstract ty invariant*
    { $1, $2, TDalias $3, $4 }
369 370
| EQUAL LT RANGE int_constant int_constant GT
    { false, Public, TDrange ($4, $5), [] }
Clément Fumex's avatar
Clément Fumex committed
371 372
| EQUAL LT FLOAT INTEGER INTEGER GT
    { false, Public,
373 374 375 376 377
      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) }
378

379 380 381 382 383
model:
| EQUAL         { false }
| MODEL         { true }

abstract:
384
| (* epsilon *) { Public }
385 386
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
387

388
type_field:
Clément Fumex's avatar
Clément Fumex committed
389
| field_modifiers labels(lident_nq) cast
390 391
  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
      f_pty = $3; f_loc = floc $startpos $endpos } }
392

393
field_modifiers:
394
| (* epsilon *) { false, false }
395 396 397 398 399
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

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

403
(* Logic declarations *)
404

405 406
constant_decl:
| labels(lident_rich) cast preceded(EQUAL,term)?
407 408
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
409

410 411
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
412 413
  { { 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
414

415 416
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
417 418
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
419

420
with_logic_decl:
421
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
422 423
  { { 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
424

425
(* Inductive declarations *)
426 427

inductive_decl:
428
| labels(lident_rich) params ind_defn
429 430
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
431

432 433 434
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
435

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

439
(* Type expressions *)
440

441 442 443 444
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
445

446 447 448 449 450 451 452
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 }
453

454 455
cast:
| COLON ty  { $2 }
456

457
(* Parameters and binders *)
458

459 460
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
461 462
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
463 464
   names, whose type must be inferred. *)

465
params:  param*  { List.concat $1 }
466

467
binders: binder+ { List.concat $1 }
468 469 470

param:
| anon_binder
471 472 473 474 475 476 477 478
    { 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 _, []) ->
479 480
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
481
| LEFTPAR binder_vars_rest RIGHTPAR
482
    { match $2 with [l,_] -> error_param l
483
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
484
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
485
    { match $3 with [l,_] -> error_param l
486 487
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
488
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
489
| LEFTPAR GHOST binder_vars cast RIGHTPAR
490
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
491

492 493
binder:
| anon_binder
494 495 496 497 498
    { error_param (floc $startpos $endpos) }
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
499
          [floc $startpos $endpos, Some id, false, None]
500
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
501 502 503
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
504 505
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
506 507 508
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident id, []) ->
509 510 511
             let id = add_lab id ($2::$3) in
             [floc $startpos $endpos, Some id, false, None]
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
512
| LEFTPAR binder_vars_rest RIGHTPAR
513
    { match $2 with [l,i] -> [l, i, false, None]
514
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
515
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
516
    { match $3 with [l,i] -> [l, i, true, None]
517 518
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
519
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
520
| LEFTPAR GHOST binder_vars cast RIGHTPAR
521
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
522

523 524 525
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
526

527
binder_vars_rest:
528 529 530 531 532 533 534
| 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*
535
   { List.rev_append $1 ($2 :: $3) }
536
| anon_binder binder_var*
537
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
538

539
binder_vars_head:
540
| ty {
541 542
    let of_id id = id.id_loc, Some id in
    let push acc = function
543
      | PTtyapp (Qident id, []) -> of_id id :: acc
544
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
545
    match $1 with
546
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
547
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
548

549
binder_var:
Clément Fumex's avatar
Clément Fumex committed
550 551
| labels(lident_nq) { floc $startpos $endpos, Some $1 }
| anon_binder       { $1 }
552 553

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

556 557 558 559 560 561 562 563 564 565 566 567 568 569
(* 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]) }
570 571 572 573
| MINUS INTEGER
    { Tconst (Number.ConstInt (mk_int_const true $2)) }
| MINUS REAL
    { Tconst (Number.ConstReal (mk_real_const true $2)) }
574 575 576 577 578 579 580 581 582 583 584 585 586 587 588
| 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)
589 590 591 592 593
      | 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)
594 595 596 597 598 599
      | _ -> 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
600 601
    { let l = List.map add_model_labels (List.concat $2) in
      Tquant ($1, l, $3, $5) }
602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636
| 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]) }
637 638 639 640 641 642
| 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]) }
643

644 645
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
646

647 648
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
649

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

653 654 655
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
656

657 658 659 660 661 662 663
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
Martin Clochard's avatar
Martin Clochard committed
664 665
| BY      { Tby }
| SO      { Tso }
666

667 668 669 670
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
671

672
numeral:
673 674
| INTEGER { Number.ConstInt (mk_int_const false $1) }
| REAL    { Number.ConstReal (mk_real_const false $1) }
675

676
(* Program declarations *)
677

678
pdecl:
679
| VAL top_ghost labels(lident_rich) type_v          { Dval (add_model_trace $3, $2, $4) }
680
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
681
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
682
| LET REC with_list1(rec_defn)                      { Drec $3 }
Clément Fumex's avatar
Clément Fumex committed
683 684
| EXCEPTION labels(uident_nq)                       { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident_nq) ty                    { Dexn ($2, $3) }
685

686 687 688 689 690 691
top_ghost:
| (* epsilon *) { Gnone  }
| GHOST         { Gghost }
| LEMMA         { Glemma }

(* Function declarations *)
692 693

type_v:
694
| arrow_type_v  { $1 }
695
| cast          { PTpure $1 }
696 697

arrow_type_v:
698
| param params tail_type_c  { PTfunc ($1 @ $2, $3) }
699 700

tail_type_c:
701 702
| single_spec spec arrow_type_v { $3, spec_union $1 $2 }
| COLON simple_type_c           { $2 }
703 704

simple_type_c:
705 706 707
| ty spec { PTpure $1, $2 }

(* Function definitions *)
708

709
rec_defn:
710
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
711
    { $2, $1, ($3, $4, $8, spec_union $5 $7) }
712

713
fun_defn:
714 715
| binders cast? spec EQUAL spec seq_expr {
  (List.map add_model_labels $1, $2, $6, spec_union $3 $5) }
716

717
fun_expr:
718 719
| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }

720 721 722 723 724 725 726 727
(* 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 }
728

729
expr: e = mk_expr(expr_) { e }
730 731 732

expr_:
| expr_arg_
733 734
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
735
| NOT expr %prec prec_prefix_op
736
    { Enot $2 }
737
| prefix_op expr %prec prec_prefix_op
738
    { Eidapp (Qident $1, [$2]) }
739 740 741 742
| MINUS INTEGER
    { Econst (Number.ConstInt (mk_int_const true $2)) }
| MINUS REAL
    { Econst (Number.ConstReal (mk_real_const true $2)) }
743 744 745 746 747 748 749
| 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 }
750
| IF seq_expr THEN expr ELSE expr
751
    { Eif ($2, $4, $6) }
752
| IF seq_expr THEN expr %prec prec_no_else
753 754 755 756
    { Eif ($2, $4, mk_expr (Etuple []) $startpos $endpos) }
| expr LARROW expr
    { match $1.expr_desc with
      | Eidapp (q, [e1]) -> Eassign (e1, q, $3)
757 758
      | Eidapp (Qident id, [e1;e2]) when id.id_str = Ident.mixfix "[]" ->
          Eidapp (Qident {id with id_str = Ident.mixfix "[]<-"}, [e1;e2;$3])
759
      | _ -> raise Error }
760
| LET top_ghost pattern EQUAL seq_expr IN seq_expr
761
    { match $3.pat_desc with
762 763 764
      | Pvar id ->
          let id = add_model_trace id in
          Elet (id, $2, $5, $7)
765 766 767 768
      | 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) ->
769
          let id = add_model_trace id in
770 771 772 773 774 775 776 777 778 779 780 781
          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
782 783
    { let id = add_model_trace $3 in
      Elet (id, $2, $5, $7) }
Clément Fumex's avatar
Clément Fumex committed
784
| LET top_ghost labels(lident_nq) fun_defn IN seq_expr
785 786 787
    { Efun ($3, $2, $4, $6) }
| LET top_ghost labels(lident_op_id) fun_defn IN seq_expr
    { Efun ($3, $2, $4, $6) }
788
| LET REC with_list1(rec_defn) IN seq_expr
789
    { Erec ($3, $5) }
790
| fun_expr
791 792 793 794 795 796 797
    { 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) }
798
| quote_uident COLON seq_expr
799
    { Emark ($1, $3) }
800
| LOOP loop_annotation seq_expr END
801
    { Eloop ($2, $3) }
802
| WHILE seq_expr DO loop_annotation seq_expr DONE
803 804
    { Ewhile ($2, $4, $5) }
| FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
805 806
    { let id = add_model_trace $2 in
      Efor (id, $4, $5, $6, $8, $9) }
807
| ABSURD
808
    { Eabsurd }
809
| RAISE uqualid
810
    { Eraise ($2, None) }
811
| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
812 813 814
    { Eraise ($3, Some $4) }
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
815
| ANY simple_type_c
816
    { Eany $2 }
817
| GHOST expr
818
    { Eghost $2 }
819
| ABSTRACT spec seq_expr END
820 821
    { Eabstract($3, $2) }
| assertion_kind LEFTBRC term RIGHTBRC
822 823
    { let t = add_model_vc_label $3 in
      Eassert ($1, t) }
824
| label expr %prec prec_named
825 826 827
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
828

829 830
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
831 832

expr_arg_:
833 834 835 836 837 838 839 840 841 842 843
| 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 }
844 845

expr_sub:
846
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
847 848 849 850 851 852 853
| 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) }
854
| expr_arg LEFTSQ expr RIGHTSQ
855
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
856
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
857
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
858 859 860 861 862 863
| 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]) }
864

865 866 867 868 869 870 871
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 } }
872

873 874
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
875