parser.mly 52.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   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
(********************************************************************)
11 12 13 14

%{
  open Ptree

Andrei Paskevich's avatar
Andrei Paskevich committed
15 16 17
  let qualid_last = function Qident x | Qdot (_, x) -> x

  let use_as q = function Some x -> x | None -> qualid_last q
18

19
  let floc s e = Loc.extract (s,e)
20

21 22
  let add_attr id l = (* id.id_ats is usually nil *)
    { id with id_ats = List.rev_append id.id_ats l }
23

Andrei Paskevich's avatar
Andrei Paskevich committed
24
  let id_anonymous loc = { id_str = "_"; id_ats = []; id_loc = loc }
25

Andrei Paskevich's avatar
Andrei Paskevich committed
26
  let mk_id id s e = { id_str = id; id_ats = []; id_loc = floc s e }
27

28 29 30 31 32
  let get_op  q s e = Qident (mk_id (Ident.op_get q) s e)
  let upd_op  q s e = Qident (mk_id (Ident.op_update q) s e)
  let cut_op  q s e = Qident (mk_id (Ident.op_cut q) s e)
  let rcut_op q s e = Qident (mk_id (Ident.op_rcut q) s e)
  let lcut_op q s e = Qident (mk_id (Ident.op_lcut q) s e)
33

34 35
  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 }
36
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
37

38 39 40
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
41
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
42 43 44 45 46 47
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
48
    sp_reads   = [];
49
    sp_writes  = [];
50
    sp_alias   = [];
51
    sp_variant = [];
52 53
    sp_checkrw = false;
    sp_diverge = false;
54
    sp_partial = false;
55
  }
56

57 58 59 60
  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;
61
    sp_reads   = s1.sp_reads @ s2.sp_reads;
62
    sp_writes  = s1.sp_writes @ s2.sp_writes;
63
    sp_alias   = s1.sp_alias @ s2.sp_alias;
64
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
65 66
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
67
    sp_partial = s1.sp_partial || s2.sp_partial;
68
  }
69

70 71 72
  let break_id    = "'Break"
  let continue_id = "'Continue"
  let return_id   = "'Return"
73

74 75
  let apply_return pat sp =
    let apply = function
76
      | loc, [{pat_desc = Pvar {id_str = "result"; id_loc = l}}, f]
77 78 79 80 81 82
        when Loc.equal loc l -> loc, [pat, f]
      | post -> post in
    match pat.pat_desc with
    | Pwild -> sp
    | _ -> { sp with sp_post = List.map apply sp.sp_post }

83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
  type partial =
    | Regular
    | Partial
    | Ghost

  let ghost part = (part = Ghost)

  let apply_partial_sp part sp =
    if part <> Partial then sp else
    { sp with sp_partial = true }

  let apply_partial part e =
    if part <> Partial then e else
    let ed = match e.expr_desc with
      | Efun (_::_ as bl, op, m, s, ex) ->
          Efun (bl, op, m, apply_partial_sp part s, ex)
      | Eany (_::_ as pl, rsk, op, m, s) ->
          Eany (pl, rsk, op, m, apply_partial_sp part s)
      | _ ->
          Loc.errorm ~loc:e.expr_loc
            "this expression cannot be declared partial" in
    { e with expr_desc = ed }
105

106 107 108 109 110 111
  let we_attr = Ident.create_attribute "expl:witness existence"

  let pre_of_any any_loc ty ql =
    if ql = [] then [] else
    let ri loc = { id_str = "result"; id_loc = loc; id_ats = [] } in
    let rt loc = { term_desc = Tident (Qident (ri loc)); term_loc = loc } in
112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
    let cast t ty = { t with term_desc = Tcast (t,ty) } in
    let case (loc, pfl) =
      let mk_t d = { term_desc = d; term_loc = loc } in
      match pfl with
      | [pat, f] ->
          let rec unfold d p = match p.pat_desc with
            | Pparen p | Pscope (_,p) -> unfold d p
            | Pcast (p,ty) -> unfold (cast d ty) p
            | Ptuple [] -> unfold (cast d (PTtuple []))
                                  { p with pat_desc = Pwild }
            | Pvar { id_str = "result" } | Pwild ->
              begin match d.term_desc with
                | Tident (Qident _) -> f (* no type casts on d *)
                | _ -> mk_t (Tlet (id_anonymous p.pat_loc, d, f))
              end
            | Pvar id -> mk_t (Tlet (id, d, f))
            | _ -> mk_t (Tcase (d, pfl)) in
          unfold (rt loc) pat
      | _ -> mk_t (Tcase (rt loc, pfl)) in
131 132 133 134 135
    let mk_t desc = { term_desc = desc; term_loc = any_loc } in
    let rec join ql = match ql with
      | [] -> assert false (* never *)
      | [q] -> case q
      | q::ql -> mk_t (Tbinop (case q, Dterm.DTand_asym, join ql)) in
136 137
    let id = add_attr (ri any_loc) [ATstr Ity.break_attr] in
    let bl = [any_loc, Some id, false, Some ty] in
138 139 140
    let p = mk_t (Tquant (Dterm.DTexists, bl, [], join ql)) in
    [mk_t (Tattr (ATstr we_attr, p))]

141 142 143
  let double_ref {id_loc = loc} =
    Loc.errorm ~loc "this variable is already a reference"

144 145 146
  let set_ref id =
    List.iter (function
      | ATstr a when Ident.attr_equal a Pmodule.ref_attr ->
147
          double_ref id
148 149 150 151 152 153 154 155
      | _ -> ()) id.id_ats;
    { id with id_ats = ATstr Pmodule.ref_attr :: id.id_ats }

  let set_ref_opt loc r = function
    | id when not r -> id
    | Some id -> Some (set_ref id)
    | None -> Loc.errorm ~loc "anonymous parameters cannot be references"

156 157 158 159 160
  let binder_of_id id =
    if id.id_str = "ref" then Loc.error ~loc:id.id_loc Error;
    (* TODO: recognize and fail on core idents *)
    Some id

161
  let lq_as_ref = function
162
    | Qident {id_str = "ref"} -> ()
163 164
    | _ -> raise Error

165 166
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
167

168 169 170
  let error_loc loc = Loc.error ~loc Error

  let () = Exn_printer.register (fun fmt exn -> match exn with
171
    | Error -> Format.fprintf fmt "syntax error"
172
    | _ -> raise exn)
173 174 175 176 177

  let core_ident_error  = format_of_string
    "Symbol %s cannot be user-defined. User-defined symbol cannot use ' \
      before a letter. You can only use ' followed by _ or a number."

178
  let add_record_projections (d: Ptree.decl) =
DAILLER Sylvain's avatar
DAILLER Sylvain committed
179
    let meta_id = {id_str = Theory.(meta_record.meta_name);
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
                   id_ats = [];
                   id_loc = Loc.dummy_position}
    in
    match d with
    | Dtype dl ->
        List.iter (fun td ->
          match td.td_def with
          | TDrecord fl ->
              List.iter (fun field ->
                let m = Dmeta (meta_id, [Mfs (Qident field.f_ident)]) in
                Typing.add_decl field.f_loc m
                )
                fl
          | _ -> ()
          )
          dl
    | _ -> ()
197 198
%}

199
(* Tokens *)
200

201
%token <string> LIDENT CORE_LIDENT UIDENT CORE_UIDENT
202
%token <Number.int_constant> INTEGER
203
%token <string> OP1 OP2 OP3 OP4 OPPREF
204
%token <Number.real_constant> REAL
205
%token <string> STRING
206
%token <string> ATTRIBUTE
207
%token <Loc.position> POSITION
208
%token <string> QUOTE_LIDENT
209 210
%token <string> RIGHTSQ_QUOTE (* ]'' *)
%token <string> RIGHTPAR_QUOTE (* )'spec *)
211
%token <string> RIGHTPAR_USCORE (* )_spec *)
212

213
(* keywords *)
214

215
%token AS AXIOM BY CLONE COINDUCTIVE CONSTANT
Clément Fumex's avatar
Clément Fumex committed
216
%token ELSE END EPSILON EXISTS EXPORT FALSE FLOAT FORALL FUNCTION
217
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
218
%token LET MATCH META NOT PREDICATE RANGE SCOPE
219
%token SO THEN THEORY TRUE TYPE USE WITH
220

221
(* program keywords *)
222

223
%token ABSTRACT ABSURD ALIAS ANY ASSERT ASSUME AT BEGIN BREAK CHECK
224
%token CONTINUE DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
225
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD PARTIAL
226
%token PRIVATE PURE RAISE RAISES READS REF REC REQUIRES
227
%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES
228

229
(* symbols *)
230

231
%token AND ARROW
232
%token AMP BAR
233
%token COLON COMMA
234
%token DOT DOTDOT EQUAL LT GT LTGT MINUS
235
%token LEFTPAR LEFTSQ
236
%token LARROW LRARROW OR
237
%token RIGHTPAR RIGHTSQ
238
%token UNDERSCORE
239 240 241

%token EOF

242
(* program symbols *)
243

244
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
245

246
(* Precedences *)
247

248 249
%nonassoc below_SEMI
%nonassoc SEMICOLON
250
%nonassoc LET VAL EXCEPTION
251
%nonassoc prec_no_else
252
%nonassoc DOT ELSE RETURN
253
%nonassoc prec_no_spec
254
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES ALIAS DIVERGES VARIANT
255 256 257 258
%nonassoc below_LARROW
%nonassoc LARROW
%nonassoc below_COMMA
%nonassoc COMMA
259
%nonassoc AS
260
%nonassoc GHOST
Andrei Paskevich's avatar
Andrei Paskevich committed
261
%nonassoc prec_attr
262
%nonassoc COLON (* weaker than -> because of t: a -> b *)
263
%right ARROW LRARROW BY SO
264 265
%right OR BARBAR
%right AND AMPAMP
266
%nonassoc NOT
267
%right EQUAL LTGT LT GT OP1
268
%nonassoc AT OLD
269
%left OP2 MINUS
270
%left OP3
271
%left OP4
272
%nonassoc prec_prefix_op
273
%nonassoc INTEGER REAL (* stronger than MINUS *)
274 275
%nonassoc LEFTSQ
%nonassoc OPPREF
276

277
(* Entry points *)
278

279
%start <Pmodule.pmodule Wstdlib.Mstr.t> mlw_file
280
%start <Ptree.term> term_eof
281 282
%start <Ptree.qualid> qualid_eof
%start <Ptree.qualid list> qualid_comma_list_eof
283
%start <Ptree.term list> term_comma_list_eof
284
%start <Ptree.ident list> ident_comma_list_eof
285

286 287
%%

288 289 290 291 292
(* parsing of a single term *)

term_eof:
| term EOF { $1 }

293
(* Modules and scopes *)
294

295
mlw_file:
296 297 298 299 300
| mlw_module* EOF
    { Typing.close_file () }
| module_decl+ EOF
    { let loc = floc $startpos($2) $endpos($2) in
      Typing.close_module loc; Typing.close_file () }
301

302
mlw_module:
303 304
| module_head module_decl* END
    { Typing.close_module (floc $startpos($3) $endpos($3)) }
305

306
module_head:
Andrei Paskevich's avatar
Andrei Paskevich committed
307 308
| THEORY attrs(uident_nq)  { Typing.open_module $2 }
| MODULE attrs(uident_nq)  { Typing.open_module $2 }
309

Andrei Paskevich's avatar
Andrei Paskevich committed
310 311
scope_head:
| SCOPE boption(IMPORT) uident
312
    { Typing.open_scope (floc $startpos $endpos) $3; $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
313

314
module_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
315
| scope_head module_decl* END
316
    { Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 }
317 318
| IMPORT uqualid
    { Typing.import_scope (floc $startpos $endpos) $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
319
| d = pure_decl | d = prog_decl | d = meta_decl
320 321 322
    { Typing.add_decl (floc $startpos $endpos) d;
      add_record_projections d
    }
Andrei Paskevich's avatar
Andrei Paskevich committed
323
| use_clone { () }
324

325
(* Use and clone *)
326

327
use_clone:
Andrei Paskevich's avatar
Andrei Paskevich committed
328 329 330 331
| 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)) }
332
| USE boption(IMPORT) m_as_list = comma_list1(use_as)
Andrei Paskevich's avatar
Andrei Paskevich committed
333
    { let loc = floc $startpos $endpos in
334 335
      let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in
      if $2 && not exists_as then Warning.emit ~loc
336
        "the keyword `import' is redundant here and can be omitted";
337 338 339 340 341
      let add_import (m, q) = let import = $2 || q = None in
        Typing.open_scope loc (use_as m q);
        Typing.add_decl loc (Duse m);
        Typing.close_scope loc ~import  in
      List.iter add_import m_as_list }
Andrei Paskevich's avatar
Andrei Paskevich committed
342 343
| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst
    { let loc = floc $startpos $endpos in
344 345
      if $2 && $4 = None then Warning.emit ~loc
        "the keyword `import' is redundant here and can be omitted";
346
      let import = $2 || $4 = None in
347
      Typing.open_scope loc (use_as $3 $4);
Andrei Paskevich's avatar
Andrei Paskevich committed
348
      Typing.add_decl loc (Dclone ($3, $5));
349
      Typing.close_scope loc ~import }
350

351 352 353
use_as:
| n = tqualid q = option(preceded(AS, uident)) { (n, q) }

354
clone_subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
355 356 357 358
| (* epsilon *)                         { [] }
| WITH comma_list1(single_clone_subst)  { $2 }

single_clone_subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
359
| TYPE qualid ty_var* EQUAL ty  { CStsym  ($2,$3,$5) }
360
| TYPE qualid                   { CStsym  ($2, [], PTtyapp ($2, [])) }
Andrei Paskevich's avatar
Andrei Paskevich committed
361
| CONSTANT  qualid EQUAL qualid { CSfsym  ($2,$4) }
362
| CONSTANT  qualid              { CSfsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
363
| FUNCTION  qualid EQUAL qualid { CSfsym  ($2,$4) }
364
| FUNCTION  qualid              { CSfsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
365
| PREDICATE qualid EQUAL qualid { CSpsym  ($2,$4) }
366
| PREDICATE qualid              { CSpsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
367
| VAL       qualid EQUAL qualid { CSvsym  ($2,$4) }
368
| VAL       qualid              { CSvsym  ($2,$2) }
369 370
| EXCEPTION qualid EQUAL qualid { CSxsym  ($2,$4) }
| EXCEPTION qualid              { CSxsym  ($2,$2) }
371
| AXIOM     qualid              { CSaxiom ($2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
372 373
| LEMMA     qualid              { CSlemma ($2) }
| GOAL      qualid              { CSgoal  ($2) }
374 375 376
| AXIOM     DOT                 { CSprop  (Decl.Paxiom) }
| LEMMA     DOT                 { CSprop  (Decl.Plemma) }
| GOAL      DOT                 { CSprop  (Decl.Pgoal) }
377

Andrei Paskevich's avatar
Andrei Paskevich committed
378
(* Meta declarations *)
379

Andrei Paskevich's avatar
Andrei Paskevich committed
380 381
meta_decl:
| META sident comma_list1(meta_arg)  { Dmeta ($2, $3) }
382 383

meta_arg:
384 385 386 387
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
388 389 390
| AXIOM     qualid  { Max $2 }
| LEMMA     qualid  { Mlm $2 }
| GOAL      qualid  { Mgl $2 }
391
| STRING            { Mstr $1 }
392
| INTEGER           { Mint (Number.to_small_integer $1) }
393

Andrei Paskevich's avatar
Andrei Paskevich committed
394 395 396 397 398 399 400 401 402
(* 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) }
Andrei Paskevich's avatar
Andrei Paskevich committed
403 404 405
| AXIOM attrs(ident_nq) COLON term          { Dprop (Decl.Paxiom, $2, $4) }
| LEMMA attrs(ident_nq) COLON term          { Dprop (Decl.Plemma, $2, $4) }
| GOAL  attrs(ident_nq) COLON term          { Dprop (Decl.Pgoal, $2, $4) }
Andrei Paskevich's avatar
Andrei Paskevich committed
406

407
(* Type declarations *)
408 409

type_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
410
| attrs(lident_nq) ty_var* typedefn invariant* type_witness
411
  { let (vis, mut), def = $3 in
412
    { td_ident = $1; td_params = $2;
413
      td_vis = vis; td_mut = mut;
414
      td_inv = $4; td_wit = $5; td_def = def;
415
      td_loc = floc $startpos $endpos } }
416

417 418 419 420
type_witness:
| (* epsilon *)                           { [] }
| BY LEFTBRC field_list1(expr) RIGHTBRC   { $3 }

421
ty_var:
Andrei Paskevich's avatar
Andrei Paskevich committed
422
| attrs(quote_lident) { $1 }
423 424

typedefn:
425
| (* epsilon *)
426
    { (Abstract, false), TDrecord [] }
427 428
| EQUAL vis_mut bar_list1(type_case)
    { $2, TDalgebraic $3 }
429
| EQUAL vis_mut LEFTBRC loption(semicolon_list1(type_field)) RIGHTBRC
430 431 432
    { $2, TDrecord $4 }
| EQUAL vis_mut ty
    { $2, TDalias $3 }
Clément Fumex's avatar
Clément Fumex committed
433
(* FIXME: allow negative bounds *)
434
| EQUAL LT RANGE int_constant int_constant GT
435
    { (Public, false), TDrange ($4, $5) }
Clément Fumex's avatar
Clément Fumex committed
436
| EQUAL LT FLOAT INTEGER INTEGER GT
437
    { (Public, false),
438 439 440
      TDfloat (Number.to_small_integer $4, Number.to_small_integer $5) }

int_constant:
441 442
| INTEGER       { $1.Number.il_int }
| MINUS INTEGER { BigInt.minus ($2.Number.il_int) }
443 444 445 446 447 448 449

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

abstract:
452 453
| PRIVATE           { Private }
| ABSTRACT          { Abstract }
454

455
type_field:
456 457 458 459 460 461 462 463
| field_modifiers ref_amp_id cast
  { let mut, ghs = $1 and rff, id = $2 in
    let ty = if rff then PTref [$3] else $3 in
    { f_ident = id; f_mutable = mut; f_ghost = ghs;
      f_pty = ty; f_loc = floc $startpos $endpos } }

%inline field_modifiers:
| (* epsilon *) { false, false }
464 465 466 467 468
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

469 470 471 472 473
(* we have to use lqualid instead of REF after field_modifiers
   to avoid a conflict with ty. However, if the given lqualid
   is not REF, then we want to fail as soon as possible: either
   at AMP, if it occurs after the lqualid, or else at COLON. *)
ref_amp_id:
474 475
| lq_as_ref AMP attrs(lident_nq)  { true,  double_ref $3 }
| lq_as_ref_id attr*              { true,  add_attr $1 $2 }
476 477 478
| AMP attrs(lident_nq)            { false, set_ref $2 }
| attrs(lident_nq)                { false, $1 }

479 480
lq_as_ref:    lqualid             { lq_as_ref $1 }
lq_as_ref_id: lqualid lident_nq   { lq_as_ref $1; set_ref $2 }
481

482
type_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
483
| attrs(uident_nq) params { floc $startpos $endpos, $1, $2 }
484

485
(* Logic declarations *)
486

487
constant_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
488
| attrs(lident_rich) cast preceded(EQUAL,term)?
489
  { { ld_ident = $1;
490
      ld_params = []; ld_type = Some $2;
491
      ld_def = $3; ld_loc = floc $startpos $endpos } }
492

493
function_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
494
| attrs(lident_rich) params cast preceded(EQUAL,term)?
495 496
  { { ld_ident = $1; ld_params = $2; ld_type = Some $3;
      ld_def = $4; ld_loc = floc $startpos $endpos } }
497

498
predicate_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
499
| attrs(lident_rich) params preceded(EQUAL,term)?
500 501
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
502

503
with_logic_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
504
| WITH attrs(lident_rich) params cast? preceded(EQUAL,term)?
505 506
  { { ld_ident = $2; ld_params = $3; ld_type = $4;
      ld_def = $5; ld_loc = floc $startpos $endpos } }
507

508
(* Inductive declarations *)
509 510

inductive_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
511
| attrs(lident_rich) params ind_defn
512 513
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
514

515 516 517
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
518

519
ind_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
520
| attrs(ident_nq) COLON term  { floc $startpos $endpos, $1, $3 }
521

522
(* Type expressions *)
523

524 525 526 527
ty:
| ty_arg          { $1 }
| lqualid ty_arg+ { PTtyapp ($1, $2) }
| ty ARROW ty     { PTarrow ($1, $3) }
528

529 530
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
531
| quote_lident                      { PTtyvar $1 }
532 533 534 535
| uqualid DOT ty_block              { PTscope ($1, $3) }
| ty_block                          { $1 }

ty_block:
536 537 538
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
539
| LEFTBRC ty RIGHTBRC               { PTpure $2 }
540

541 542
cast:
| COLON ty  { $2 }
543

544
(* Parameters and binders *)
545

546 547
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
548 549
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
550 551
   names, whose type must be inferred. *)

552
params:  param*  { List.concat $1 }
553

554 555
params1: param+  { List.concat $1 }

556
binders: binder+ { List.concat $1 }
557 558

param:
559
| special_binder
560
    { error_param (floc $startpos $endpos) }
561 562
| lident_nq attr+
    { error_param (floc $startpos $endpos) }
563 564 565 566
| ty_arg
    { [floc $startpos $endpos, None, false, $1] }
| LEFTPAR GHOST ty RIGHTPAR
    { [floc $startpos $endpos, None, true, $3] }
567
| LEFTPAR binder_vars_rest RIGHTPAR
568
    { match snd $2 with [l,_] -> error_param l
569
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
570
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
571
    { match snd $3 with [l,_] -> error_param l
572 573
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
574 575
    { let r = fst $2 in let ty = if r then PTref [$3] else $3 in
      List.map (fun (l,i) -> l, set_ref_opt l r i, false, ty) (snd $2) }
576
| LEFTPAR GHOST binder_vars cast RIGHTPAR
577 578
    { let r = fst $3 in let ty = if r then PTref [$4] else $4 in
      List.map (fun (l,i) -> l, set_ref_opt l r i, true, ty) (snd $3) }
579

580
binder:
581
| special_binder
582
    { let l,i = $1 in [l, i, false, None] }
583 584
| lident_nq attr+
    { [floc $startpos $endpos, Some (add_attr $1 $2), false, None] }
585 586
| ty_arg
    { match $1 with
587 588
      | PTparen (PTtyapp (Qident {id_str="ref"}, [PTtyapp (Qident id, [])])) ->
              [floc $startpos $endpos, binder_of_id (set_ref id), false, None]
589 590
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
591 592
              [floc $startpos $endpos, binder_of_id id, false, None]
      | _ ->  [floc $startpos $endpos, None, false, Some $1] }
593 594
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
595 596
      | PTtyapp (Qident {id_str="ref"}, [PTtyapp (Qident id, [])]) ->
              [floc $startpos $endpos, binder_of_id (set_ref id), true, None]
597
      | PTtyapp (Qident id, []) ->
598 599
              [floc $startpos $endpos, binder_of_id id, true, None]
      | _ ->  [floc $startpos $endpos, None, true, Some $3] }
600
| LEFTPAR binder_vars_rest RIGHTPAR
601
    { match snd $2 with [l,i] -> [l, set_ref_opt l (fst $2) i, false, None]
602
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
603
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
604
    { match snd $3 with [l,i] -> [l, set_ref_opt l (fst $3) i, true, None]
605 606
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
607 608
    { let r = fst $2 in let ty = if r then PTref [$3] else $3 in
      List.map (fun (l,i) -> l, set_ref_opt l r i, false, Some ty) (snd $2) }
609
| LEFTPAR GHOST binder_vars cast RIGHTPAR
610 611
    { let r = fst $3 in let ty = if r then PTref [$4] else $4 in
      List.map (fun (l,i) -> l, set_ref_opt l r i, true, Some ty) (snd $3) }
612

613
binder_vars:
614
| binder_vars_head  { fst $1, match snd $1 with
615
                        | [] -> raise Error
616
                        | bl -> List.rev bl }
617
| binder_vars_rest  { $1 }
618

619
binder_vars_rest:
620
| binder_vars_head attr+ binder_var*
621 622
    { let l2 = floc $startpos($2) $endpos($2) in
      fst $1, List.rev_append (match snd $1 with
623
        | (l, Some id) :: bl ->
624
            (Loc.join l l2, Some (add_attr id $2)) :: bl
625
        | _ -> error_loc l2) $3 }
626 627 628 629
| binder_vars_head special_binder binder_var*
    { fst $1, List.rev_append (snd $1) ($2 :: $3) }
| special_binder binder_var*
    { false, $1 :: $2 }
630

631
binder_vars_head:
632
| ty {
633
    let of_id id = id.id_loc, binder_of_id id in
634
    let push acc = function
635
      | PTtyapp (Qident id, []) -> of_id id :: acc
636
      | _ -> raise Error in
637
    match $1 with
638 639
      | PTtyapp (Qident {id_str = "ref"}, l) ->
          true, List.fold_left push [] l
640
      | PTtyapp (Qident id, l) ->
641
          false, List.fold_left push [of_id id] l
642
      | _ -> raise Error }
643

644
binder_var:
645 646
| attrs(lident_nq)      { floc $startpos $endpos, Some $1 }
| special_binder        { $1 }
647

648 649 650
special_binder:
| UNDERSCORE            { floc $startpos $endpos, None }
| AMP attrs(lident_nq)  { floc $startpos $endpos, Some (set_ref $2) }
651

652 653 654 655
(* Logical terms *)

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

656 657 658 659
term:
| single_term %prec below_COMMA   { $1 }
| single_term COMMA term_
    { mk_term (Ttuple ($1::$3)) $startpos $endpos }
660 661

term_:
662 663 664 665 666 667
| single_term %prec below_COMMA   { [$1] }
| single_term COMMA term_         { $1::$3 }

single_term: t = mk_term(single_term_) { t }

single_term_:
668 669
| term_arg_
    { match $1 with (* break the infix relation chain *)
670 671 672
      | Tinfix (l,o,r) -> Tinnfix (l,o,r)
      | Tbinop (l,o,r) -> Tbinnop (l,o,r)
      | d -> d }
673
| NOT single_term
674
    { Tnot $2 }
675
| OLD single_term
Andrei Paskevich's avatar
Andrei Paskevich committed
676
    { Tat ($2, mk_id Dexpr.old_label $startpos($1) $endpos($1)) }
677
| single_term AT uident
678
    { Tat ($1, $3) }
679
| prefix_op single_term %prec prec_prefix_op
680
    { Tidapp (Qident $1, [$2]) }
681 682
| MINUS numeral
    { Tconst (Number.neg $2) }
683
| l = single_term ; o = bin_op ; r = single_term
684
    { Tbinop (l, o, r) }
685
| l = single_term ; o = infix_op_1 ; r = single_term
686
    { Tinfix (l, o, r) }
687
| l = single_term ; o = infix_op_234 ; r = single_term
688
    { Tidapp (Qident o, [l; r]) }
689
| term_arg located(term_arg)+
690 691 692 693 694
    { 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
695
    { let re_pat pat d = { pat with pat_desc = d } in
696 697
      let cast t ty = { t with term_desc = Tcast (t,ty) } in
      let rec unfold d p = match p.pat_desc with
698
        | Pparen p | Pscope (_,p) -> unfold d p
699 700 701 702 703 704
        | Pcast (p,ty) -> unfold (cast d ty) p
        | Ptuple [] -> unfold (cast d (PTtuple [])) (re_pat p Pwild)
        | Pvar id -> Tlet (id, d, $6)
        | Pwild -> Tlet (id_anonymous p.pat_loc, d, $6)
        | _ -> Tcase (d, [$2, $6]) in
      unfold $4 $2 }
705
| LET attrs(lident_op_nq) EQUAL term IN term
706
    { Tlet ($2, $4, $6) }
Andrei Paskevich's avatar
Andrei Paskevich committed
707
| LET attrs(lident_nq) mk_term(lam_defn) IN term
708
    { Tlet ($2, $3, $5) }
709
| LET attrs(lident_op_nq) mk_term(lam_defn) IN term
710
    { Tlet ($2, $3, $5) }
711
| MATCH term WITH match_cases(term) END
712
    { Tcase ($2, $4) }
713
| quant comma_list1(quant_vars) triggers DOT term
714
    { let l = List.concat $2 in
715
      Tquant ($1, l, $3, $5) }
716
| FUN binders ARROW term
717
    { Tquant (Dterm.DTlambda, $2, [], $4) }
718 719
| EPSILON
    { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
Andrei Paskevich's avatar
Andrei Paskevich committed
720 721
| attr single_term %prec prec_attr
    { Tattr ($1, $2) }
722
| single_term cast
723 724
    { Tcast ($1, $2) }

725
lam_defn:
726
| binders EQUAL term  { Tquant (Dterm.DTlambda, $1, [], $3) }
727

728 729 730 731 732
term_arg: mk_term(term_arg_) { $1 }
term_dot: mk_term(term_dot_) { $1 }

term_arg_:
| qualid                    { Tident $1 }
733
| AMP qualid                { Tasref $2 }
734 735 736 737 738 739 740 741 742 743 744
| 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 }

745
term_block_:
746
| BEGIN term END                                    { $2.term_desc }
747
| LEFTPAR term RIGHTPAR                             { $2.term_desc }
748
| BEGIN END                                         { Ttuple [] }
749 750 751
| 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
Andrei Paskevich committed
752 753

term_sub_:
754 755
| term_block_                                       { $1 }
| uqualid DOT mk_term(term_block_)                  { Tscope ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
756
| term_dot DOT lqualid_rich                         { Tidapp ($3,[$1]) }
757 758 759 760 761 762 763 764 765 766
| term_arg LEFTSQ term rightsq
    { Tidapp (get_op $4 $startpos($2) $endpos($2), [$1;$3]) }
| term_arg LEFTSQ term LARROW term rightsq
    { Tidapp (upd_op $6 $startpos($2) $endpos($2), [$1;$3;$5]) }
| term_arg LEFTSQ term DOTDOT term rightsq
    { Tidapp (cut_op $6 $startpos($2) $endpos($2), [$1;$3;$5]) }
| term_arg LEFTSQ term DOTDOT rightsq
    { Tidapp (rcut_op $5 $startpos($2) $endpos($2), [$1;$3]) }
| term_arg LEFTSQ DOTDOT term rightsq
    { Tidapp (lcut_op $5 $startpos($2) $endpos($2), [$1;$4]) }
767

768 769
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
770

771
match_cases(X):
772 773 774 775
| cl = bar_list1(match_case(X)) { cl }

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

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

780
triggers:
781 782
| (* epsilon *)                                                         { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(single_term)) RIGHTSQ  { $2 }
783

784
%inline bin_op:
785 786 787 788 789 790
| ARROW   { Dterm.DTimplies }
| LRARROW { Dterm.DTiff }
| OR      { Dterm.DTor }
| BARBAR  { Dterm.DTor_asym }
| AND     { Dterm.DTand }
| AMPAMP  { Dterm.DTand_asym }
791 792
| BY      { Dterm.DTby }
| SO      { Dterm.DTso }
793

794
quant:
795 796
| FORALL  { Dterm.DTforall }
| EXISTS  { Dterm.DTexists }
797

798
numeral:
799 800
| INTEGER { Number.ConstInt $1 }
| REAL    { Number.ConstReal $1 }
801

802
(* Program declarations *)
803

Andrei Paskevich's avatar
Andrei Paskevich committed
804
prog_decl:
805 806 807 808 809
| VAL ghost kind attrs(lident_rich) mk_expr(fun_decl)
    { Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
| VAL ghost kind sym_binder mk_expr(const_decl)
    { Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
| VAL ghost REF ref_binder mk_expr(const_decl)
810 811 812
    { let rf = mk_expr Eref $startpos($3) $endpos($3) in
      let ee = { $5 with expr_desc = Eapply (rf, $5) } in
      Dlet ($4, ghost $2, Expr.RKnone, apply_partial $2 ee) }
813 814
| LET ghost kind attrs(lident_rich) mk_expr(fun_defn)
    { Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
815
| LET ghost kind sym_binder const_defn
816
    { Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
817 818 819 820
| LET ghost REF ref_binder const_defn
    { let rf = mk_expr Eref $startpos($3) $endpos($3) in
      let ee = { $5 with expr_desc = Eapply (rf, $5) } in
      Dlet ($4, ghost $2, Expr.RKnone, apply_partial $2 ee) }
821 822 823 824 825 826
| LET REC with_list1(rec_defn)
    { Drec $3 }
| EXCEPTION attrs(uident_nq)
    { Dexn ($2, PTtuple [], Ity.MaskVisible) }
| EXCEPTION attrs(uident_nq) return
    { Dexn ($2, fst $3, snd $3) }
827 828

ghost:
829 830 831 832 833 834
| (* epsilon *) { Regular }
| PARTIAL       { Partial }
| GHOST         { Ghost }
| GHOST PARTIAL
| PARTIAL GHOST { Loc.errorm ~loc:(floc $startpos $endpos)
                    "Ghost functions cannot be partial" }
835 836 837 838 839 840 841

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

(* Function definitions *)
844

845
rec_defn:
846 847 848 849 850 851
| ghost kind attrs(lident_rich) binders return_opt spec EQUAL spec seq_expr
    { let pat, ty, mask = $5 in
      let spec = apply_return pat (spec_union $6 $8) in
      let id = mk_id return_id $startpos($7) $endpos($7) in
      let e = { $9 with expr_desc = Eoptexn (id, mask, $9) } in
      $3, ghost $1, $2, $4, ty, mask, apply_partial_sp $1 spec, e }
852

853
fun_defn:
854 855 856 857 858
| binders return_opt spec EQUAL spec seq_expr
    { let pat, ty, mask = $2 in
      let spec = apply_return pat (spec_union $3 $5) in
      let id = mk_id return_id $startpos($4) $endpos($4) in
      let e = { $6 with expr_desc = Eoptexn (id, mask, $6) } in
859
      Efun ($1, ty, mask, spec, e) }
860

861 862
fun_decl:
| params1 return_opt spec
863 864
    { let pat, ty, mask = $2 in
      Eany ($1, Expr.RKnone, ty, mask, apply_return pat $3) }
865

866
const_decl:
867 868 869 870
| return_opt spec
    { let pat, ty, mask = $1 in
      Eany ([], Expr.RKnone, ty, mask, apply_return pat $2) }

871 872 873 874
const_defn:
| cast EQUAL seq_expr   { { $3 with expr_desc = Ecast ($3, $1) } }
| EQUAL seq_expr        { $2 }

875 876 877 878 879
(* Program expressions *)

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

seq_expr:
880 881 882
| contract_expr %prec below_SEMI  { $1 }
| contract_expr SEMICOLON         { $1 }
| contract_expr SEMICOLON seq_expr
883
    { mk_expr (Esequence ($1, $3)) $startpos $endpos }
884

885 886 887 888
contract_expr:
| assign_expr %prec prec_no_spec  { $1 }
| assign_expr single_spec spec
    { let d = Efun ([], None, Ity.MaskVisible, spec_union $2 $3, $1) in
Andrei Paskevich's avatar
Andrei Paskevich committed
889
      let d = Eattr (ATstr Vc.wb_attr, mk_expr d $startpos $endpos) in
890 891
      mk_expr d $startpos $endpos }

892 893 894 895 896
assign_expr:
| expr %prec below_LARROW         { $1 }
| expr LARROW expr
    { let loc = floc $startpos $endpos in
      let rec down ll rl = match ll, rl with
897 898 899 900 901
        | ({expr_desc = Eident q} as e1)::ll, e2::rl ->
            let e1 = {e1 with expr_desc = Easref q} in
            (e1, None, e2) :: down ll rl
        | {expr_desc = Eidapp (q, [e1])}::ll, e2::rl ->
            (e1, Some q, e2) :: down ll rl
902 903 904 905 906 907 908
        | {expr_desc = Eidapp (Qident id, [_;_]); expr_loc = loc}::_, _::_ ->
            begin match Ident.sn_decode id.id_str with
              | Ident.SNget _ -> Loc.errorm ~loc
                  "Parallel array assignments are not allowed"
              | _ -> Loc.errorm ~loc
                  "Invalid left expression in an assignment"
            end
909 910 911 912 913
        | {expr_loc = loc}::_, _::_ -> Loc.errorm ~loc
            "Invalid left expression in an assignment"
        | [], [] -> []
        | _ -> Loc.errorm ~loc "Invalid parallel assignment" in
      let d = match $1.expr_desc, $3.expr_desc with
914 915 916 917 918 919 920
        | Eidapp (Qident id, [e1;e2]), _ ->
            begin match Ident.sn_decode id.id_str with
              | Ident.SNget q ->
                  Eidapp (Qident {id with id_str = Ident.op_set q}, [e1;e2;$3])
              | _ -> Loc.errorm ~loc:$1.expr_loc
                  "Invalid left expression in an assignment"
            end
921 922 923 924 925 926 927
        | Etuple ll, Etuple rl -> Eassign (down ll rl)
        | Etuple _, _ -> Loc.errorm ~loc "Invalid parallel assignment"
        | _, _ -> Eassign (down [$1] [$3]) in
      { expr_desc = d; expr_loc = loc } }

expr:
| single_expr %prec below_COMMA   { $1 }
928
| single_expr COMMA expr_list1
929
    { mk_expr (Etuple ($1::$3)) $startpos $endpos }
930

931
expr_list1:
932
| single_expr %prec below_COMMA   { [$1] }
933
| single_expr COMMA expr_list1    { $1::$3 }
934 935 936 937

single_expr: e = mk_expr(single_expr_)  { e }

single_expr_:
938
| expr_arg_
939 940
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
941
| single_expr AMPAMP single_expr
942
    { Eand ($1, $3) }
943
| single_expr BARBAR single_expr
944
    { Eor ($1, $3) }
945
| NOT single_expr
946
    { Enot $2 }
947
| prefix_op single_expr %prec prec_prefix_op
948
    { Eidapp (Qident $1, [$2]) }
949 950
| MINUS numeral
    { Econst (Number.neg $2) }
951
| l = single_expr ; o = infix_op_1 ; r = single_expr
952
    { Einfix (l,o,r) }
953
| l = single_expr ; o = infix_op_234 ; r = single_expr
954
    { Eidapp (Qident o, [l;r]) }
955
| expr_arg located(expr_arg)+
956 957
    { let join f (a,_,e) = mk_expr (Eapply (f,a)) $startpos e in
      (List.fold_left join $1 $2).expr_desc }
958
| IF seq_expr THEN contract_expr ELSE contract_expr
959
    { Eif ($2, $4, $6) }
960
| IF seq_expr THEN contract_expr %prec prec_no_else
961
    { Eif ($2, $4, mk_expr (Etuple []) $startpos $endpos) }
962 963
| LET ghost kind let_pattern EQUAL seq_expr IN seq_expr
    { let re_pat pat d = { pat with pat_desc = d } in
964 965 966 967 968 969 970
      let cast e ty = { e with expr_desc = Ecast (e,ty) } in
      let rec push pat = re_pat pat (match pat.pat_desc with
        | Ptuple (p::pl) -> Ptuple (push p :: pl)
        | Pcast (p,ty) -> Pcast (push p, ty)
        | Pas (p,v,g) -> Pas (push p, v, g)
        | Por (p,q) -> Por (push p, q)
        | _ -> Pghost pat) in
971
      let pat = if ghost $2 then push $4 else $4 in
972
      let rec unfold gh d p = match p.pat_desc with
973
        | Pparen p | Pscope (_,p) -> unfold gh d p
974 975 976
        | Pghost p -> unfold true d p
        | Pcast (p,ty) -> unfold gh (cast d ty) p
        | Ptuple [] -> unfold gh (cast d (PTtuple [])) (re_pat p Pwild)
977
        | Pvar id -> Elet (id, gh, $3, d, $8)
978 979
        | Pwild -> Elet (id_anonymous p.pat_loc, gh, $3, d, $8)
        | _ when $3 = Expr.RKnone -> Ematch (d, [pat, $8], [])
980 981
        | _ -> Loc.errorm ~loc:(floc $startpos($3) $endpos($3))
            "illegal kind qualifier" in
982
      unfold false (apply_partial $2 $6) pat }
983 984
| LET ghost kind attrs(lident_op_nq) const_defn IN seq_expr
    { Elet ($4, ghost $2, $3, apply_partial $2 $