parser.mly 52 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
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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

26 27 28 29 30 31
  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}

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

34 35 36 37 38
  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)
39

40 41
  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 }
42
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
43

44 45 46
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
47
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
48 49 50 51 52 53
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
54
    sp_reads   = [];
55
    sp_writes  = [];
56
    sp_alias   = [];
57
    sp_variant = [];
58 59
    sp_checkrw = false;
    sp_diverge = false;
60
    sp_partial = false;
61
  }
62

63 64 65 66
  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;
67
    sp_reads   = s1.sp_reads @ s2.sp_reads;
68
    sp_writes  = s1.sp_writes @ s2.sp_writes;
69
    sp_alias   = s1.sp_alias @ s2.sp_alias;
70
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
71 72
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
73
    sp_partial = s1.sp_partial || s2.sp_partial;
74
  }
75

Andrei Paskevich's avatar
Andrei Paskevich committed
76 77 78
  let break_id    = "'Break"
  let continue_id = "'Continue"
  let return_id   = "'Return"
79

80 81
  let apply_return pat sp =
    let apply = function
82
      | loc, [{pat_desc = Pvar {id_str = "result"; id_loc = l}}, f]
83 84 85 86 87 88
        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 }

89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
  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 }
111

Andrei Paskevich's avatar
Andrei Paskevich committed
112 113 114 115 116 117
  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
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
    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
Andrei Paskevich's avatar
Andrei Paskevich committed
137 138 139 140 141
    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
142 143
    let id = add_attr (ri any_loc) [ATstr Ity.break_attr] in
    let bl = [any_loc, Some id, false, Some ty] in
Andrei Paskevich's avatar
Andrei Paskevich committed
144 145 146
    let p = mk_t (Tquant (Dterm.DTexists, bl, [], join ql)) in
    [mk_t (Tattr (ATstr we_attr, p))]

147 148 149
  let double_ref {id_loc = loc} =
    Loc.errorm ~loc "this variable is already a reference"

150 151 152
  let set_ref id =
    List.iter (function
      | ATstr a when Ident.attr_equal a Pmodule.ref_attr ->
153
          double_ref id
154 155 156 157 158 159 160 161
      | _ -> ()) 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"

162 163 164 165 166
  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

167
  let lq_as_ref = function
168
    | Qident {id_str = "ref"} -> ()
169 170
    | _ -> raise Error

171 172
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
173

174 175 176
  let error_loc loc = Loc.error ~loc Error

  let () = Exn_printer.register (fun fmt exn -> match exn with
177
    | Error -> Format.fprintf fmt "syntax error"
178
    | _ -> raise exn)
179 180 181 182 183

  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."

184
  let add_record_projections (d: Ptree.decl) =
DAILLER Sylvain's avatar
DAILLER Sylvain committed
185
    let meta_id = {id_str = Theory.(meta_record.meta_name);
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202
                   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
    | _ -> ()
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
203 204
%}

205
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
206

207
%token <string> LIDENT CORE_LIDENT UIDENT CORE_UIDENT
208
%token <Number.integer_literal> INTEGER
209
%token <string> OP1 OP2 OP3 OP4 OPPREF
210
%token <Number.real_literal> REAL
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
211
%token <string> STRING
212
%token <string> ATTRIBUTE
213
%token <Loc.position> POSITION
214
%token <string> QUOTE_LIDENT
215 216
%token <string> RIGHTSQ_QUOTE (* ]'' *)
%token <string> RIGHTPAR_QUOTE (* )'spec *)
217
%token <string> RIGHTPAR_USCORE (* )_spec *)
218

219
(* keywords *)
220

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

227
(* program keywords *)
228

229
%token ABSTRACT ABSURD ALIAS ANY ASSERT ASSUME AT BEGIN BREAK CHECK
Andrei Paskevich's avatar
Andrei Paskevich committed
230
%token CONTINUE DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
231
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD PARTIAL
232
%token PRIVATE PURE RAISE RAISES READS REF REC REQUIRES
233
%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES
234

235
(* symbols *)
236

Andrei Paskevich's avatar
Andrei Paskevich committed
237
%token AND ARROW
238
%token AMP BAR
239
%token COLON COMMA
240
%token DOT DOTDOT EQUAL LT GT LTGT MINUS
241
%token LEFTPAR LEFTSQ
242
%token LARROW LRARROW OR
243
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
244
%token UNDERSCORE
245 246 247

%token EOF

248
(* program symbols *)
249

250
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
251

252
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
253

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

283
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284

Guillaume Melquiond's avatar
Guillaume Melquiond committed
285
%start <Pmodule.pmodule Wstdlib.Mstr.t> mlw_file
286
%start <Ptree.term> term_eof
287 288
%start <Ptree.qualid> qualid_eof
%start <Ptree.qualid list> qualid_comma_list_eof
289
%start <Ptree.term list> term_comma_list_eof
290
%start <Ptree.ident list> ident_comma_list_eof
291

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
292 293
%%

294 295 296 297 298
(* parsing of a single term *)

term_eof:
| term EOF { $1 }

299
(* Modules and scopes *)
300

301
mlw_file:
302 303 304 305 306
| mlw_module* EOF
    { Typing.close_file () }
| module_decl+ EOF
    { let loc = floc $startpos($2) $endpos($2) in
      Typing.close_module loc; Typing.close_file () }
307

308
mlw_module:
309 310
| module_head module_decl* END
    { Typing.close_module (floc $startpos($3) $endpos($3)) }
311

312
module_head:
Andrei Paskevich's avatar
Andrei Paskevich committed
313 314
| THEORY attrs(uident_nq)  { Typing.open_module $2 }
| MODULE attrs(uident_nq)  { Typing.open_module $2 }
315

Andrei Paskevich's avatar
Andrei Paskevich committed
316 317
scope_head:
| SCOPE boption(IMPORT) uident
318
    { Typing.open_scope (floc $startpos $endpos) $3; $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
319

320
module_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
321
| scope_head module_decl* END
322
    { Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 }
323 324
| IMPORT uqualid
    { Typing.import_scope (floc $startpos $endpos) $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
325
| d = pure_decl | d = prog_decl | d = meta_decl
326 327 328
    { Typing.add_decl (floc $startpos $endpos) d;
      add_record_projections d
    }
Andrei Paskevich's avatar
Andrei Paskevich committed
329
| use_clone { () }
330

331
(* Use and clone *)
332

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

357 358 359
use_as:
| n = tqualid q = option(preceded(AS, uident)) { (n, q) }

360
clone_subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
361 362 363 364
| (* epsilon *)                         { [] }
| WITH comma_list1(single_clone_subst)  { $2 }

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

Andrei Paskevich's avatar
Andrei Paskevich committed
384
(* Meta declarations *)
385

Andrei Paskevich's avatar
Andrei Paskevich committed
386 387
meta_decl:
| META sident comma_list1(meta_arg)  { Dmeta ($2, $3) }
388 389

meta_arg:
390 391 392 393
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
394 395 396
| AXIOM     qualid  { Max $2 }
| LEMMA     qualid  { Mlm $2 }
| GOAL      qualid  { Mgl $2 }
397
| STRING            { Mstr $1 }
398
| INTEGER           { Mint (Number.to_small_integer $1) }
399

Andrei Paskevich's avatar
Andrei Paskevich committed
400 401 402 403 404 405 406 407 408
(* 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
409 410 411
| 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
412

413
(* Type declarations *)
414 415

type_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
416
| attrs(lident_nq) ty_var* typedefn invariant* type_witness
417
  { let (vis, mut), def = $3 in
418
    { td_ident = $1; td_params = $2;
419
      td_vis = vis; td_mut = mut;
420
      td_inv = $4; td_wit = $5; td_def = def;
421
      td_loc = floc $startpos $endpos } }
422

423 424 425 426
type_witness:
| (* epsilon *)                           { [] }
| BY LEFTBRC field_list1(expr) RIGHTBRC   { $3 }

427
ty_var:
Andrei Paskevich's avatar
Andrei Paskevich committed
428
| attrs(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429 430

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

int_constant:
447 448
| INTEGER       { Number.compute_int_literal $1 }
| MINUS INTEGER { BigInt.minus (Number.compute_int_literal $2) }
449 450 451 452 453 454 455

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

abstract:
458 459
| PRIVATE           { Private }
| ABSTRACT          { Abstract }
460

461
type_field:
462 463 464 465 466 467 468 469
| 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 }
470 471 472 473 474
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

475 476 477 478 479
(* 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:
480 481
| lq_as_ref AMP attrs(lident_nq)  { true,  double_ref $3 }
| lq_as_ref_id attr*              { true,  add_attr $1 $2 }
482 483 484
| AMP attrs(lident_nq)            { false, set_ref $2 }
| attrs(lident_nq)                { false, $1 }

485 486
lq_as_ref:    lqualid             { lq_as_ref $1 }
lq_as_ref_id: lqualid lident_nq   { lq_as_ref $1; set_ref $2 }
487

488
type_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
489
| attrs(uident_nq) params { floc $startpos $endpos, $1, $2 }
490

491
(* Logic declarations *)
492

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

499
function_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
500
| attrs(lident_rich) params cast preceded(EQUAL,term)?
501 502
  { { 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
503

504
predicate_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
505
| attrs(lident_rich) params preceded(EQUAL,term)?
506 507
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
508

509
with_logic_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
510
| WITH attrs(lident_rich) params cast? preceded(EQUAL,term)?
511 512
  { { 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
513

514
(* Inductive declarations *)
515 516

inductive_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
517
| attrs(lident_rich) params ind_defn
518 519
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
520

521 522 523
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
524

525
ind_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
526
| attrs(ident_nq) COLON term  { floc $startpos $endpos, $1, $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
527

528
(* Type expressions *)
529

530 531 532 533
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
534

535 536
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
537
| quote_lident                      { PTtyvar $1 }
538 539 540 541
| uqualid DOT ty_block              { PTscope ($1, $3) }
| ty_block                          { $1 }

ty_block:
542 543 544
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
545
| LEFTBRC ty RIGHTBRC               { PTpure $2 }
546

547 548
cast:
| COLON ty  { $2 }
549

550
(* Parameters and binders *)
551

552 553
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
554 555
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
556 557
   names, whose type must be inferred. *)

558
params:  param*  { List.concat $1 }
559

560 561
params1: param+  { List.concat $1 }

562
binders: binder+ { List.concat $1 }
563 564

param:
565
| special_binder
566
    { error_param (floc $startpos $endpos) }
567 568
| lident_nq attr+
    { error_param (floc $startpos $endpos) }
569 570 571 572
| ty_arg
    { [floc $startpos $endpos, None, false, $1] }
| LEFTPAR GHOST ty RIGHTPAR
    { [floc $startpos $endpos, None, true, $3] }
573
| LEFTPAR binder_vars_rest RIGHTPAR
574
    { match snd $2 with [l,_] -> error_param l
575
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
576
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
577
    { match snd $3 with [l,_] -> error_param l
578 579
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
580 581
    { 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) }
582
| LEFTPAR GHOST binder_vars cast RIGHTPAR
583 584
    { 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) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
585

586
binder:
587
| special_binder
588
    { let l,i = $1 in [l, i, false, None] }
589 590
| lident_nq attr+
    { [floc $startpos $endpos, Some (add_attr $1 $2), false, None] }
591 592
| ty_arg
    { match $1 with
593 594
      | PTparen (PTtyapp (Qident {id_str="ref"}, [PTtyapp (Qident id, [])])) ->
              [floc $startpos $endpos, binder_of_id (set_ref id), false, None]
595 596
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
597 598
              [floc $startpos $endpos, binder_of_id id, false, None]
      | _ ->  [floc $startpos $endpos, None, false, Some $1] }
599 600
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
601 602
      | PTtyapp (Qident {id_str="ref"}, [PTtyapp (Qident id, [])]) ->
              [floc $startpos $endpos, binder_of_id (set_ref id), true, None]
603
      | PTtyapp (Qident id, []) ->
604 605
              [floc $startpos $endpos, binder_of_id id, true, None]
      | _ ->  [floc $startpos $endpos, None, true, Some $3] }
606
| LEFTPAR binder_vars_rest RIGHTPAR
607
    { match snd $2 with [l,i] -> [l, set_ref_opt l (fst $2) i, false, None]
608
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
609
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
610
    { match snd $3 with [l,i] -> [l, set_ref_opt l (fst $3) i, true, None]
611 612
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
613 614
    { 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) }
615
| LEFTPAR GHOST binder_vars cast RIGHTPAR
616 617
    { 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) }
618

619
binder_vars:
620
| binder_vars_head  { fst $1, match snd $1 with
621
                        | [] -> raise Error
622
                        | bl -> List.rev bl }
623
| binder_vars_rest  { $1 }
624

625
binder_vars_rest:
626
| binder_vars_head attr+ binder_var*
627 628
    { let l2 = floc $startpos($2) $endpos($2) in
      fst $1, List.rev_append (match snd $1 with
629
        | (l, Some id) :: bl ->
630
            (Loc.join l l2, Some (add_attr id $2)) :: bl
631
        | _ -> error_loc l2) $3 }
632 633 634 635
| binder_vars_head special_binder binder_var*
    { fst $1, List.rev_append (snd $1) ($2 :: $3) }
| special_binder binder_var*
    { false, $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
636

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

650
binder_var:
651 652
| attrs(lident_nq)      { floc $startpos $endpos, Some $1 }
| special_binder        { $1 }
653

654 655 656
special_binder:
| UNDERSCORE            { floc $startpos $endpos, None }
| AMP attrs(lident_nq)  { floc $startpos $endpos, Some (set_ref $2) }
657

658 659 660 661
(* Logical terms *)

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

662 663 664 665
term:
| single_term %prec below_COMMA   { $1 }
| single_term COMMA term_
    { mk_term (Ttuple ($1::$3)) $startpos $endpos }
666 667

term_:
668 669 670 671 672 673
| single_term %prec below_COMMA   { [$1] }
| single_term COMMA term_         { $1::$3 }

single_term: t = mk_term(single_term_) { t }

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

733
lam_defn:
734
| binders EQUAL term  { Tquant (Dterm.DTlambda, $1, [], $3) }
735

736 737 738 739 740
term_arg: mk_term(term_arg_) { $1 }
term_dot: mk_term(term_dot_) { $1 }

term_arg_:
| qualid                    { Tident $1 }
741
| AMP qualid                { Tasref $2 }
742 743 744 745 746 747 748 749 750 751 752
| 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 }

753
term_block_:
754
| BEGIN term END                                    { $2.term_desc }
755
| LEFTPAR term RIGHTPAR                             { $2.term_desc }
756
| BEGIN END                                         { Ttuple [] }
757 758 759
| 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
760 761

term_sub_:
762 763
| term_block_                                       { $1 }
| uqualid DOT mk_term(term_block_)                  { Tscope ($1, $3) }
Andrei Paskevich's avatar
M.()  
Andrei Paskevich committed
764
| term_dot DOT lqualid_rich                         { Tidapp ($3,[$1]) }
765 766 767 768 769 770 771 772 773 774
| 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]) }
775

776 777
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
778

779
match_cases(X):
780 781 782 783
| cl = bar_list1(match_case(X)) { cl }

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

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

788
triggers:
789 790
| (* epsilon *)                                                         { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(single_term)) RIGHTSQ  { $2 }
791

792
%inline bin_op:
793 794 795 796 797 798
| ARROW   { Dterm.DTimplies }
| LRARROW { Dterm.DTiff }
| OR      { Dterm.DTor }
| BARBAR  { Dterm.DTor_asym }
| AND     { Dterm.DTand }
| AMPAMP  { Dterm.DTand_asym }
799 800
| BY      { Dterm.DTby }
| SO      { Dterm.DTso }
801

802
quant:
803 804
| FORALL  { Dterm.DTforall }
| EXISTS  { Dterm.DTexists }
805

806
numeral:
807 808
| INTEGER { Number.ConstInt (mk_int_const false $1) }
| REAL    { Number.ConstReal (mk_real_const false $1) }
809

810
(* Program declarations *)
811

Andrei Paskevich's avatar
Andrei Paskevich committed
812
prog_decl:
813 814 815 816 817
| 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)
818 819 820
    { 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
| LET ghost kind attrs(lident_rich) mk_expr(fun_defn)
    { Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
823
| LET ghost kind sym_binder const_defn
824
    { Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
825 826 827 828
| 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) }
829 830 831 832 833 834
| LET REC with_list1(rec_defn)
    { Drec $3 }
| EXCEPTION attrs(uident_nq)
    { Dexn ($2, PTtuple [], Ity.MaskVisible) }
| EXCEPTION attrs