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

%{
  open Ptree

15
  let infix  s = "infix "  ^ s
16
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
17
  let mixfix s = "mixfix " ^ s
18

Andrei Paskevich's avatar
Andrei Paskevich committed
19 20 21
  let qualid_last = function Qident x | Qdot (_, x) -> x

  let use_as q = function Some x -> x | None -> qualid_last q
Andrei Paskevich's avatar
Andrei Paskevich committed
22

23
  let floc s e = Loc.extract (s,e)
Andrei Paskevich's avatar
Andrei Paskevich committed
24

25
  let model_label = Ident.create_label "model"
26
  let model_projected = Ident.create_label "model_projected"
27

28 29 30
  let is_model_label l = match l with
    | Lstr lab -> Ident.lab_equal lab model_label ||
                  Ident.lab_equal lab model_projected
31
    | Lpos _ -> false
32

33
  let model_lab_present labels = List.exists is_model_label labels
34

35 36
  let is_model_trace_label l = match l with
    | Lstr lab -> Strings.has_prefix "model_trace:" lab.Ident.lab_string
37
    | Lpos _ -> false
38 39

  let model_trace_lab_present labels = List.exists is_model_trace_label labels
40 41

  let add_model_trace name labels =
42
    if model_lab_present labels && not (model_trace_lab_present labels) then
43 44
      (Lstr (Ident.create_label ("model_trace:" ^ name)))::labels
    else
45
      labels
46

47
  let add_lab id l = { id with id_lab = add_model_trace id.id_str l }
48

49
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
50

51 52 53 54 55 56
  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}

57
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
58

59 60
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
61 62 63
  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)
64

65 66
  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 }
67
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
68

69 70 71
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
72
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
73 74 75 76 77 78
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
79
    sp_reads   = [];
80 81
    sp_writes  = [];
    sp_variant = [];
82 83
    sp_checkrw = false;
    sp_diverge = false;
84
  }
85

86 87 88 89
  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;
90
    sp_reads   = s1.sp_reads @ s2.sp_reads;
91 92
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
93 94
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
95
  }
96

97
(* dead code
98
  let add_init_mark e =
99
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
100
    { e with expr_desc = Emark (init, e) }
101
*)
102

103 104
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
105

106 107 108 109 110
  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
111 112
%}

113
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114

Clément Fumex's avatar
Clément Fumex committed
115
%token <string> LIDENT LIDENT_QUOTE UIDENT UIDENT_QUOTE
116
%token <Number.integer_literal> INTEGER
117
%token <string> OP1 OP2 OP3 OP4 OPPREF
118
%token <Number.real_literal> REAL
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
119
%token <string> STRING
120
%token <Loc.position> POSITION
121
%token <string> QUOTE_LIDENT
122

123
(* keywords *)
124

Martin Clochard's avatar
Martin Clochard committed
125
%token AS AXIOM BY CLONE COINDUCTIVE CONSTANT
Clément Fumex's avatar
Clément Fumex committed
126
%token ELSE END EPSILON EXISTS EXPORT FALSE FLOAT FORALL FUNCTION
Andrei Paskevich's avatar
Andrei Paskevich committed
127
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
128
%token LET MATCH META NOT PREDICATE RANGE SCOPE
Martin Clochard's avatar
Martin Clochard committed
129
%token SO THEN THEORY TRUE TYPE USE WITH
130

131
(* program keywords *)
132

133
%token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN CHECK
134
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
135
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
136 137
%token PRIVATE PURE RAISE RAISES READS REC REQUIRES
%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES
138

139
(* symbols *)
140

Andrei Paskevich's avatar
Andrei Paskevich committed
141
%token AND ARROW
142
%token BAR
143
%token COLON COMMA
144
%token DOT DOTDOT EQUAL LT GT LTGT MINUS
145
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
146
%token LARROW LRARROW OR
147
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
148
%token UNDERSCORE
149 150 151

%token EOF

152
(* program symbols *)
153

154
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
155

156
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
157

158 159
%nonassoc below_SEMI
%nonassoc SEMICOLON
160
%nonassoc LET VAL EXCEPTION
161
%nonassoc prec_no_else
162
%nonassoc DOT ELSE RETURN
Andrei Paskevich's avatar
Andrei Paskevich committed
163 164
%nonassoc prec_no_spec
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES DIVERGES VARIANT
165 166 167 168 169
%nonassoc below_LARROW
%nonassoc LARROW
%nonassoc below_COMMA
%nonassoc COMMA
%nonassoc GHOST
170
%nonassoc prec_named
171
%nonassoc COLON (* weaker than -> because of t: a -> b *)
172
%right ARROW LRARROW BY SO
173 174
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
175
%nonassoc NOT
176
%right EQUAL LTGT LT GT OP1
177
%nonassoc AT OLD
178
%left OP2 MINUS
179
%left OP3
180
%left OP4
181
%nonassoc prec_prefix_op
182
%nonassoc INTEGER REAL (* stronger than MINUS *)
183 184
%nonassoc LEFTSQ
%nonassoc OPPREF
185

186
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
187

188
%start <Pmodule.pmodule Stdlib.Mstr.t> mlw_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189 190
%%

191
(* Modules and scopes *)
192

193
mlw_file:
194 195 196 197 198
| mlw_module* EOF
    { Typing.close_file () }
| module_decl+ EOF
    { let loc = floc $startpos($2) $endpos($2) in
      Typing.close_module loc; Typing.close_file () }
199

200
mlw_module:
201 202
| module_head module_decl* END
    { Typing.close_module (floc $startpos($3) $endpos($3)) }
203

204
module_head:
205 206
| THEORY labels(uident_nq)  { Typing.open_module $2 }
| MODULE labels(uident_nq)  { Typing.open_module $2 }
207

Andrei Paskevich's avatar
Andrei Paskevich committed
208 209
scope_head:
| SCOPE boption(IMPORT) uident
210
    { Typing.open_scope (floc $startpos $endpos) $3; $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
211

212
module_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
213
| scope_head module_decl* END
214
    { Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 }
215 216
| IMPORT uqualid
    { Typing.import_scope (floc $startpos $endpos) $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
217 218 219
| d = pure_decl | d = prog_decl | d = meta_decl
    { Typing.add_decl (floc $startpos $endpos) d }
| use_clone { () }
220

221
(* Use and clone *)
222

223
use_clone:
Andrei Paskevich's avatar
Andrei Paskevich committed
224 225 226 227 228 229
| USE EXPORT tqualid
    { Typing.add_decl (floc $startpos $endpos) (Duse $3) }
| CLONE EXPORT tqualid clone_subst
    { Typing.add_decl (floc $startpos $endpos) (Dclone ($3, $4)) }
| USE boption(IMPORT) tqualid option(preceded(AS, uident))
    { let loc = floc $startpos $endpos in
230
      Typing.open_scope loc (use_as $3 $4);
Andrei Paskevich's avatar
Andrei Paskevich committed
231
      Typing.add_decl loc (Duse $3);
232
      Typing.close_scope loc ~import:$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
233 234
| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst
    { let loc = floc $startpos $endpos in
235
      Typing.open_scope loc (use_as $3 $4);
Andrei Paskevich's avatar
Andrei Paskevich committed
236
      Typing.add_decl loc (Dclone ($3, $5));
237
      Typing.close_scope loc ~import:$2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
238

239
clone_subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
240 241 242 243
| (* epsilon *)                         { [] }
| WITH comma_list1(single_clone_subst)  { $2 }

single_clone_subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
244
| TYPE qualid ty_var* EQUAL ty  { CStsym  ($2,$3,$5) }
245
| TYPE qualid                   { CStsym  ($2, [], PTtyapp ($2, [])) }
Andrei Paskevich's avatar
Andrei Paskevich committed
246
| CONSTANT  qualid EQUAL qualid { CSfsym  ($2,$4) }
247
| CONSTANT  qualid              { CSfsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
248
| FUNCTION  qualid EQUAL qualid { CSfsym  ($2,$4) }
249
| FUNCTION  qualid              { CSfsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
250
| PREDICATE qualid EQUAL qualid { CSpsym  ($2,$4) }
251
| PREDICATE qualid              { CSpsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
252
| VAL       qualid EQUAL qualid { CSvsym  ($2,$4) }
253
| VAL       qualid              { CSvsym  ($2,$2) }
254 255
| EXCEPTION qualid EQUAL qualid { CSxsym  ($2,$4) }
| EXCEPTION qualid              { CSxsym  ($2,$2) }
256
| AXIOM     qualid              { CSaxiom ($2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
257 258
| LEMMA     qualid              { CSlemma ($2) }
| GOAL      qualid              { CSgoal  ($2) }
259

Andrei Paskevich's avatar
Andrei Paskevich committed
260
(* Meta declarations *)
261

Andrei Paskevich's avatar
Andrei Paskevich committed
262 263
meta_decl:
| META sident comma_list1(meta_arg)  { Dmeta ($2, $3) }
264 265

meta_arg:
266 267 268 269
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
270 271 272
| AXIOM     qualid  { Max $2 }
| LEMMA     qualid  { Mlm $2 }
| GOAL      qualid  { Mgl $2 }
273
| STRING            { Mstr $1 }
274
| INTEGER           { Mint (Number.to_small_integer $1) }
275

Andrei Paskevich's avatar
Andrei Paskevich committed
276 277 278 279 280 281 282 283 284
(* Theory declarations *)

pure_decl:
| TYPE with_list1(type_decl)                { Dtype $2 }
| CONSTANT  constant_decl                   { Dlogic [$2] }
| FUNCTION  function_decl  with_logic_decl* { Dlogic ($2::$3) }
| PREDICATE predicate_decl with_logic_decl* { Dlogic ($2::$3) }
| INDUCTIVE   with_list1(inductive_decl)    { Dind (Decl.Ind, $2) }
| COINDUCTIVE with_list1(inductive_decl)    { Dind (Decl.Coind, $2) }
Clément Fumex's avatar
Clément Fumex committed
285 286 287
| 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) }
Andrei Paskevich's avatar
Andrei Paskevich committed
288

289
(* Type declarations *)
290 291

type_decl:
292
| labels(lident_nq) ty_var* typedefn invariant*
293
  { let (vis, mut), def = $3 in
294
    { td_ident = $1; td_params = $2;
295 296 297
      td_vis = vis; td_mut = mut;
      td_inv = $4; td_def = def;
      td_loc = floc $startpos $endpos } }
298

299
ty_var:
300
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
301 302

typedefn:
303
| (* epsilon *)
304
    { (Abstract, false), TDrecord [] }
305 306
| EQUAL vis_mut bar_list1(type_case)
    { $2, TDalgebraic $3 }
307
| EQUAL vis_mut LEFTBRC loption(semicolon_list1(type_field)) RIGHTBRC
308 309 310
    { $2, TDrecord $4 }
| EQUAL vis_mut ty
    { $2, TDalias $3 }
Clément Fumex's avatar
Clément Fumex committed
311
(* FIXME: allow negative bounds *)
312
| EQUAL LT RANGE int_constant int_constant GT
313
    { (Public, false),
314
      TDrange ($4,$5) }
Clément Fumex's avatar
Clément Fumex committed
315
| EQUAL LT FLOAT INTEGER INTEGER GT
316
    { (Public, false),
317 318 319 320 321
      TDfloat (Number.to_small_integer $4, Number.to_small_integer $5) }

int_constant:
| INTEGER       { mk_int_const false $1 }
| MINUS INTEGER { mk_int_const true $2 }
322 323 324 325 326 327 328

vis_mut:
| (* epsilon *)     { Public, false }
| MUTABLE           { Public, true  }
| abstract          { $1, false }
| abstract MUTABLE  { $1, true }
| MUTABLE abstract  { $2, true }
329 330

abstract:
331 332
| PRIVATE           { Private }
| ABSTRACT          { Abstract }
333

334
type_field:
335
| labels(lident_nq) cast
Andrei Paskevich's avatar
Andrei Paskevich committed
336 337
  { { f_ident = $1; f_mutable = false; f_ghost = false;
      f_pty = $2; f_loc = floc $startpos $endpos } }
Clément Fumex's avatar
Clément Fumex committed
338
| field_modifiers labels(lident_nq) cast
339 340
  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
      f_pty = $3; f_loc = floc $startpos $endpos } }
341

342 343 344 345 346 347
field_modifiers:
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

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

351
(* Logic declarations *)
352

353 354
constant_decl:
| labels(lident_rich) cast preceded(EQUAL,term)?
355 356
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
357

358 359
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
360 361
  { { 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
362

363 364
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
365 366
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
367

368
with_logic_decl:
369
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
370 371
  { { 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
372

373
(* Inductive declarations *)
374 375

inductive_decl:
376
| labels(lident_rich) params ind_defn
377 378
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
379

380 381 382
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
383

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

387
(* Type expressions *)
388

389 390 391 392
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
393

394 395
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
396
| quote_lident                      { PTtyvar $1 }
397 398 399
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
400
| LEFTBRC ty RIGHTBRC               { PTpure $2 }
401

402 403
cast:
| COLON ty  { $2 }
404

405
(* Parameters and binders *)
406

407 408
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
409 410
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
411 412
   names, whose type must be inferred. *)

413
params:  param*  { List.concat $1 }
414

415
binders: binder+ { List.concat $1 }
416 417 418

param:
| anon_binder
419 420 421 422 423 424 425 426
    { 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 _, []) ->
427 428
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
429
| LEFTPAR binder_vars_rest RIGHTPAR
430
    { match $2 with [l,_] -> error_param l
431
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
432
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
433
    { match $3 with [l,_] -> error_param l
434 435
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
436
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
437
| LEFTPAR GHOST binder_vars cast RIGHTPAR
438
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
439

440 441
binder:
| anon_binder
442
    { let l,i = $1 in [l, i, false, None] }
443 444 445 446
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
447 448
             [floc $startpos $endpos, Some id, false, None]
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
449 450 451
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
452 453
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
454 455 456
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident id, []) ->
457 458 459
             let id = add_lab id ($2::$3) in
             [floc $startpos $endpos, Some id, false, None]
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
460
| LEFTPAR binder_vars_rest RIGHTPAR
461
    { match $2 with [l,i] -> [l, i, false, None]
462
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
463
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
464
    { match $3 with [l,i] -> [l, i, true, None]
465 466
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
467
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
468
| LEFTPAR GHOST binder_vars cast RIGHTPAR
469
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
470

471 472 473
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
474

475
binder_vars_rest:
476 477 478 479 480 481 482
| 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*
483
    { List.rev_append $1 ($2 :: $3) }
484
| anon_binder binder_var*
485
    { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
486

487
binder_vars_head:
488
| ty {
489 490
    let of_id id = id.id_loc, Some id in
    let push acc = function
491
      | PTtyapp (Qident id, []) -> of_id id :: acc
492
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
493
    match $1 with
494
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
495
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
496

497
binder_var:
Clément Fumex's avatar
Clément Fumex committed
498 499
| labels(lident_nq) { floc $startpos $endpos, Some $1 }
| anon_binder       { $1 }
500 501

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

504 505 506 507
(* Logical terms *)

mk_term(X): d = X { mk_term d $startpos $endpos }

508 509 510 511
term:
| single_term %prec below_COMMA   { $1 }
| single_term COMMA term_
    { mk_term (Ttuple ($1::$3)) $startpos $endpos }
512 513

term_:
514 515 516 517 518 519
| single_term %prec below_COMMA   { [$1] }
| single_term COMMA term_         { $1::$3 }

single_term: t = mk_term(single_term_) { t }

single_term_:
520 521
| term_arg_
    { match $1 with (* break the infix relation chain *)
Andrei Paskevich's avatar
Andrei Paskevich committed
522 523 524
      | Tinfix (l,o,r) -> Tinnfix (l,o,r)
      | Tbinop (l,o,r) -> Tbinnop (l,o,r)
      | d -> d }
525
| NOT single_term
Andrei Paskevich's avatar
Andrei Paskevich committed
526
    { Tnot $2 }
527
| OLD single_term
528
    { Tat ($2, mk_id Dexpr.old_mark $startpos($1) $endpos($1)) }
529
| single_term AT uident
530
    { Tat ($1, $3) }
531
| prefix_op single_term %prec prec_prefix_op
532
    { Tidapp (Qident $1, [$2]) }
533
| MINUS INTEGER
534
    { Tconst (Number.ConstInt (mk_int_const true $2)) }
535
| MINUS REAL
536
    { Tconst (Number.ConstReal (mk_real_const true $2)) }
537
| l = single_term ; o = bin_op ; r = single_term
538
    { Tbinop (l, o, r) }
539
| l = single_term ; o = infix_op_1 ; r = single_term
540
    { Tinfix (l, o, r) }
541
| l = single_term ; o = infix_op_234 ; r = single_term
542
    { Tidapp (Qident o, [l; r]) }
543 544 545 546 547 548
| 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
549 550 551 552 553 554 555 556 557
    { let cast ty = { $4 with term_desc = Tcast ($4, ty) } in
      let pat, def = match $2.pat_desc with
        | Ptuple [] -> { $2 with pat_desc = Pwild }, cast (PTtuple [])
        | Pcast ({pat_desc = (Pvar (_,false)|Pwild)} as p, ty) -> p, cast ty
        | _ -> $2, $4 in
      match pat.pat_desc with
      | Pvar (id,false) -> Tlet (id, def, $6)
      | Pwild -> Tlet (id_anonymous pat.pat_loc, def, $6)
      | _ -> Tmatch (def, [pat, $6]) }
558 559
| LET labels(lident_op_id) EQUAL term IN term
    { Tlet ($2, $4, $6) }
560
| LET labels(lident_nq) mk_term(lam_defn) IN term
561 562 563
    { Tlet ($2, $3, $5) }
| LET labels(lident_op_id) mk_term(lam_defn) IN term
    { Tlet ($2, $3, $5) }
564 565 566 567
| MATCH term WITH match_cases(term) END
    { Tmatch ($2, $4) }
| quant comma_list1(quant_vars) triggers DOT term
    { Tquant ($1, List.concat $2, $3, $5) }
568
| FUN binders ARROW term
Andrei Paskevich's avatar
Andrei Paskevich committed
569
    { Tquant (Dterm.DTlambda, $2, [], $4) }
570 571
| EPSILON
    { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
572
| label single_term %prec prec_named
573
    { Tnamed ($1, $2) }
574
| single_term cast
575 576
    { Tcast ($1, $2) }

577
lam_defn:
Andrei Paskevich's avatar
Andrei Paskevich committed
578
| binders EQUAL term  { Tquant (Dterm.DTlambda, $1, [], $3) }
579

580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595
term_arg: mk_term(term_arg_) { $1 }
term_dot: mk_term(term_dot_) { $1 }

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

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

Andrei Paskevich's avatar
M.()  
Andrei Paskevich committed
596
term_block:
597
| BEGIN term END                                    { $2.term_desc }
598
| LEFTPAR term RIGHTPAR                             { $2.term_desc }
599
| BEGIN END                                         { Ttuple [] }
600 601 602
| LEFTPAR RIGHTPAR                                  { Ttuple [] }
| LEFTBRC field_list1(term) RIGHTBRC                { Trecord $2 }
| LEFTBRC term_arg WITH field_list1(term) RIGHTBRC  { Tupdate ($2,$4) }
Andrei Paskevich's avatar
M.()  
Andrei Paskevich committed
603 604 605 606 607

term_sub_:
| term_block                                        { $1 }
| uqualid DOT mk_term(term_block)                   { Tscope ($1, $3) }
| term_dot DOT lqualid_rich                         { Tidapp ($3,[$1]) }
608 609 610 611
| 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]) }
612 613 614 615 616 617
| 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]) }
618

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

622
match_cases(X):
623 624 625 626
| cl = bar_list1(match_case(X)) { cl }

match_case(X):
| mc = separated_pair(pattern, ARROW, X) { mc }
627

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

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

635
%inline bin_op:
Andrei Paskevich's avatar
Andrei Paskevich committed
636 637 638 639 640 641
| ARROW   { Dterm.DTimplies }
| LRARROW { Dterm.DTiff }
| OR      { Dterm.DTor }
| BARBAR  { Dterm.DTor_asym }
| AND     { Dterm.DTand }
| AMPAMP  { Dterm.DTand_asym }
642 643
| BY      { Dterm.DTby }
| SO      { Dterm.DTso }
644

645
quant:
Andrei Paskevich's avatar
Andrei Paskevich committed
646 647
| FORALL  { Dterm.DTforall }
| EXISTS  { Dterm.DTexists }
648

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

653
(* Program declarations *)
654

Andrei Paskevich's avatar
Andrei Paskevich committed
655
prog_decl:
656 657
| VAL ghost kind labels(lident_rich) mk_expr(val_defn) { Dlet ($4, $2, $3, $5) }
| LET ghost kind labels(lident_rich) mk_expr(fun_defn) { Dlet ($4, $2, $3, $5) }
658
| LET ghost kind labels(lident_rich) const_defn        { Dlet ($4, $2, $3, $5) }
659
| LET REC with_list1(rec_defn)                         { Drec $3 }
660 661
| EXCEPTION labels(uident_nq)         { Dexn ($2, PTtuple [], Ity.MaskVisible) }
| EXCEPTION labels(uident_nq) return  { Dexn ($2, fst $3, snd $3) }
662 663 664 665 666 667 668 669 670 671 672

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

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

(* Function definitions *)
675

676
rec_defn:
677 678
| ghost kind labels(lident_rich) binders ret_opt spec EQUAL spec seq_expr
    { $3, $1, $2, $4, fst $5, snd $5, spec_union $6 $8, $9 }
679

680
fun_defn:
681 682
| binders ret_opt spec EQUAL spec seq_expr
    { Efun ($1, fst $2, snd $2, spec_union $3 $5, $6) }
683

684
val_defn:
685 686
| params ret_opt spec
    { Eany ($1, Expr.RKnone, fst $2, snd $2, $3) }
687

688 689 690 691
const_defn:
| cast EQUAL seq_expr   { { $3 with expr_desc = Ecast ($3, $1) } }
| EQUAL seq_expr        { $2 }

692 693 694 695 696
(* Program expressions *)

mk_expr(X): d = X { mk_expr d $startpos $endpos }

seq_expr:
Andrei Paskevich's avatar
Andrei Paskevich committed