parser.mly 47.9 KB
Newer Older
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5
6
7
8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11
12
13
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
Andrei Paskevich's avatar
Andrei Paskevich committed
18

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

Andrei Paskevich's avatar
Andrei Paskevich committed
21
22
23
  let debug_auto_model = Debug.register_flag
    ~desc:"When set, model attributes are not added during parsing"
    "no_auto_model"
24

25
  let add_attr id l = { id with id_ats = l }
26

Andrei Paskevich's avatar
Andrei Paskevich committed
27
  let add_model_trace_attr id =
28
    if Debug.test_flag debug_auto_model then id else
Andrei Paskevich's avatar
Andrei Paskevich committed
29
    let is_model_trace_attr l =
30
      match l with
Andrei Paskevich's avatar
Andrei Paskevich committed
31
32
      | ATpos _ -> false
      | ATstr attr -> Ident.is_model_trace_attr attr
33
    in
Andrei Paskevich's avatar
Andrei Paskevich committed
34
    if List.exists is_model_trace_attr id.id_ats then id else
35
      let l =
Andrei Paskevich's avatar
Andrei Paskevich committed
36
        (ATstr (Ident.create_model_trace_attr id.id_str))
37
        :: id.id_ats in
Andrei Paskevich's avatar
Andrei Paskevich committed
38
      { id with id_ats = l }
39

Andrei Paskevich's avatar
Andrei Paskevich committed
40
  let add_model_attrs (b : binder) =
41
42
    match b with
    | (loc, Some id, ghost, ty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
43
      (loc, Some (add_model_trace_attr id), ghost, ty)
44
45
    | _ -> b

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

48
49
50
51
52
53
  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
54
  let mk_id id s e = { id_str = id; id_ats = []; id_loc = floc s e }
55

56
57
58
59
60
  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)
61

62
63
  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 }
64
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
65

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

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
76
    sp_reads   = [];
77
    sp_writes  = [];
78
    sp_alias   = [];
79
    sp_variant = [];
80
81
    sp_checkrw = false;
    sp_diverge = false;
82
    sp_partial = false;
83
  }
84

85
86
87
88
  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;
89
    sp_reads   = s1.sp_reads @ s2.sp_reads;
90
    sp_writes  = s1.sp_writes @ s2.sp_writes;
91
    sp_alias   = s1.sp_alias @ s2.sp_alias;
92
    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
    sp_partial = s1.sp_partial || s2.sp_partial;
96
  }
97

Andrei Paskevich's avatar
Andrei Paskevich committed
98
99
100
  let break_id    = "'Break"
  let continue_id = "'Continue"
  let return_id   = "'Return"
101

102
103
  let apply_return pat sp =
    let apply = function
104
      | loc, [{pat_desc = Pvar {id_str = "result"; id_loc = l}}, f]
105
106
107
108
109
110
        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 }

111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
  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 }
133

Andrei Paskevich's avatar
Andrei Paskevich committed
134
135
136
137
138
139
  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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
    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
159
160
161
162
163
    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
164
165
    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
166
167
168
    let p = mk_t (Tquant (Dterm.DTexists, bl, [], join ql)) in
    [mk_t (Tattr (ATstr we_attr, p))]

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

172
173
174
  let error_loc loc = Loc.error ~loc Error

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
182
183
%}

184
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
185

186
%token <string> LIDENT CORE_LIDENT UIDENT CORE_UIDENT
187
%token <Number.integer_literal> INTEGER
188
%token <string> OP1 OP2 OP3 OP4 OPPREF
189
%token <Number.real_literal> REAL
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
190
%token <string> STRING
191
%token <string> ATTRIBUTE
192
%token <Loc.position> POSITION
193
%token <string> QUOTE_LIDENT
194
195
%token <string> RIGHTSQ_QUOTE (* ]'' *)
%token <string> RIGHTPAR_QUOTE (* )'spec *)
196
%token <string> RIGHTPAR_USCORE (* )_spec *)
197

198
(* keywords *)
199

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

206
(* program keywords *)
207

208
%token ABSTRACT ABSURD ALIAS ANY ASSERT ASSUME AT BEGIN BREAK CHECK
Andrei Paskevich's avatar
Andrei Paskevich committed
209
%token CONTINUE DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
210
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD PARTIAL
211
212
%token PRIVATE PURE RAISE RAISES READS REC REQUIRES
%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES
213

214
(* symbols *)
215

Andrei Paskevich's avatar
Andrei Paskevich committed
216
%token AND ARROW
217
%token BAR
218
%token COLON COMMA
219
%token DOT DOTDOT EQUAL LT GT LTGT MINUS
220
%token LEFTPAR LEFTSQ
221
%token LARROW LRARROW OR
222
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
223
%token UNDERSCORE
224
225
226

%token EOF

227
(* program symbols *)
228

229
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
230

231
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
232

233
234
%nonassoc below_SEMI
%nonassoc SEMICOLON
235
%nonassoc LET VAL EXCEPTION
236
%nonassoc prec_no_else
237
%nonassoc DOT ELSE RETURN
Andrei Paskevich's avatar
Andrei Paskevich committed
238
%nonassoc prec_no_spec
239
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES ALIAS DIVERGES VARIANT
240
241
242
243
%nonassoc below_LARROW
%nonassoc LARROW
%nonassoc below_COMMA
%nonassoc COMMA
244
%nonassoc AS
245
%nonassoc GHOST
Andrei Paskevich's avatar
Andrei Paskevich committed
246
%nonassoc prec_attr
247
%nonassoc COLON (* weaker than -> because of t: a -> b *)
248
%right ARROW LRARROW BY SO
249
250
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
251
%nonassoc NOT
252
%right EQUAL LTGT LT GT OP1
253
%nonassoc AT OLD
254
%left OP2 MINUS
255
%left OP3
256
%left OP4
257
%nonassoc prec_prefix_op
258
%nonassoc INTEGER REAL (* stronger than MINUS *)
259
260
%nonassoc LEFTSQ
%nonassoc OPPREF
261

262
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
263

Guillaume Melquiond's avatar
Guillaume Melquiond committed
264
%start <Pmodule.pmodule Wstdlib.Mstr.t> mlw_file
265
%start <Ptree.term> term_eof
266
267
%start <Ptree.qualid> qualid_eof
%start <Ptree.qualid list> qualid_comma_list_eof
268
%start <Ptree.term list> term_comma_list_eof
269
%start <Ptree.ident list> ident_comma_list_eof
270

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
271
272
%%

273
274
275
276
277
(* parsing of a single term *)

term_eof:
| term EOF { $1 }

278
(* Modules and scopes *)
279

280
mlw_file:
281
282
283
284
285
| mlw_module* EOF
    { Typing.close_file () }
| module_decl+ EOF
    { let loc = floc $startpos($2) $endpos($2) in
      Typing.close_module loc; Typing.close_file () }
286

287
mlw_module:
288
289
| module_head module_decl* END
    { Typing.close_module (floc $startpos($3) $endpos($3)) }
290

291
module_head:
Andrei Paskevich's avatar
Andrei Paskevich committed
292
293
| THEORY attrs(uident_nq)  { Typing.open_module $2 }
| MODULE attrs(uident_nq)  { Typing.open_module $2 }
294

Andrei Paskevich's avatar
Andrei Paskevich committed
295
296
scope_head:
| SCOPE boption(IMPORT) uident
297
    { Typing.open_scope (floc $startpos $endpos) $3; $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
298

299
module_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
300
| scope_head module_decl* END
301
    { Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 }
302
303
| IMPORT uqualid
    { Typing.import_scope (floc $startpos $endpos) $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
304
305
306
| d = pure_decl | d = prog_decl | d = meta_decl
    { Typing.add_decl (floc $startpos $endpos) d }
| use_clone { () }
307

308
(* Use and clone *)
309

310
use_clone:
Andrei Paskevich's avatar
Andrei Paskevich committed
311
312
313
314
| 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)) }
315
| USE boption(IMPORT) m_as_list = comma_list1(use_as)
Andrei Paskevich's avatar
Andrei Paskevich committed
316
    { let loc = floc $startpos $endpos in
317
318
      let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in
      if $2 && not exists_as then Warning.emit ~loc
319
        "the keyword `import' is redundant here and can be omitted";
320
321
322
323
324
      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
325
326
| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst
    { let loc = floc $startpos $endpos in
327
328
      if $2 && $4 = None then Warning.emit ~loc
        "the keyword `import' is redundant here and can be omitted";
329
      let import = $2 || $4 = None in
330
      Typing.open_scope loc (use_as $3 $4);
Andrei Paskevich's avatar
Andrei Paskevich committed
331
      Typing.add_decl loc (Dclone ($3, $5));
332
      Typing.close_scope loc ~import }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
333

334
335
336
use_as:
| n = tqualid q = option(preceded(AS, uident)) { (n, q) }

337
clone_subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
338
339
340
341
| (* epsilon *)                         { [] }
| WITH comma_list1(single_clone_subst)  { $2 }

single_clone_subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
342
| TYPE qualid ty_var* EQUAL ty  { CStsym  ($2,$3,$5) }
343
| TYPE qualid                   { CStsym  ($2, [], PTtyapp ($2, [])) }
Andrei Paskevich's avatar
Andrei Paskevich committed
344
| CONSTANT  qualid EQUAL qualid { CSfsym  ($2,$4) }
345
| CONSTANT  qualid              { CSfsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
346
| FUNCTION  qualid EQUAL qualid { CSfsym  ($2,$4) }
347
| FUNCTION  qualid              { CSfsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
348
| PREDICATE qualid EQUAL qualid { CSpsym  ($2,$4) }
349
| PREDICATE qualid              { CSpsym  ($2,$2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
350
| VAL       qualid EQUAL qualid { CSvsym  ($2,$4) }
351
| VAL       qualid              { CSvsym  ($2,$2) }
352
353
| EXCEPTION qualid EQUAL qualid { CSxsym  ($2,$4) }
| EXCEPTION qualid              { CSxsym  ($2,$2) }
354
| AXIOM     qualid              { CSaxiom ($2) }
Andrei Paskevich's avatar
Andrei Paskevich committed
355
356
| LEMMA     qualid              { CSlemma ($2) }
| GOAL      qualid              { CSgoal  ($2) }
357
358
359
| AXIOM     DOT                 { CSprop  (Decl.Paxiom) }
| LEMMA     DOT                 { CSprop  (Decl.Plemma) }
| GOAL      DOT                 { CSprop  (Decl.Pgoal) }
360

Andrei Paskevich's avatar
Andrei Paskevich committed
361
(* Meta declarations *)
362

Andrei Paskevich's avatar
Andrei Paskevich committed
363
364
meta_decl:
| META sident comma_list1(meta_arg)  { Dmeta ($2, $3) }
365
366

meta_arg:
367
368
369
370
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
371
372
373
| AXIOM     qualid  { Max $2 }
| LEMMA     qualid  { Mlm $2 }
| GOAL      qualid  { Mgl $2 }
374
| STRING            { Mstr $1 }
375
| INTEGER           { Mint (Number.to_small_integer $1) }
376

Andrei Paskevich's avatar
Andrei Paskevich committed
377
378
379
380
381
382
383
384
385
(* 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
386
387
388
| 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
389

390
(* Type declarations *)
391
392

type_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
393
| attrs(lident_nq) ty_var* typedefn invariant* type_witness
394
  { let (vis, mut), def = $3 in
395
    { td_ident = $1; td_params = $2;
396
      td_vis = vis; td_mut = mut;
397
      td_inv = $4; td_wit = $5; td_def = def;
398
      td_loc = floc $startpos $endpos } }
399

400
401
402
403
type_witness:
| (* epsilon *)                           { [] }
| BY LEFTBRC field_list1(expr) RIGHTBRC   { $3 }

404
ty_var:
Andrei Paskevich's avatar
Andrei Paskevich committed
405
| attrs(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
406
407

typedefn:
408
| (* epsilon *)
409
    { (Abstract, false), TDrecord [] }
410
411
| EQUAL vis_mut bar_list1(type_case)
    { $2, TDalgebraic $3 }
412
| EQUAL vis_mut LEFTBRC loption(semicolon_list1(type_field)) RIGHTBRC
413
414
415
    { $2, TDrecord $4 }
| EQUAL vis_mut ty
    { $2, TDalias $3 }
Clément Fumex's avatar
Clément Fumex committed
416
(* FIXME: allow negative bounds *)
417
| EQUAL LT RANGE int_constant int_constant GT
418
    { (Public, false), TDrange ($4, $5) }
Clément Fumex's avatar
Clément Fumex committed
419
| EQUAL LT FLOAT INTEGER INTEGER GT
420
    { (Public, false),
421
422
423
      TDfloat (Number.to_small_integer $4, Number.to_small_integer $5) }

int_constant:
424
425
| INTEGER       { Number.compute_int_literal $1 }
| MINUS INTEGER { BigInt.minus (Number.compute_int_literal $2) }
426
427
428
429
430
431
432

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

abstract:
435
436
| PRIVATE           { Private }
| ABSTRACT          { Abstract }
437

438
type_field:
Andrei Paskevich's avatar
Andrei Paskevich committed
439
| attrs(lident_nq) cast
Andrei Paskevich's avatar
Andrei Paskevich committed
440
441
  { { f_ident = $1; f_mutable = false; f_ghost = false;
      f_pty = $2; f_loc = floc $startpos $endpos } }
Andrei Paskevich's avatar
Andrei Paskevich committed
442
| field_modifiers attrs(lident_nq) cast
443
444
  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
      f_pty = $3; f_loc = floc $startpos $endpos } }
445

446
447
448
449
450
451
field_modifiers:
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

452
type_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
453
| attrs(uident_nq) params { floc $startpos $endpos, $1, $2 }
454

455
(* Logic declarations *)
456

457
constant_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
458
459
| attrs(lident_rich) cast preceded(EQUAL,term)?
  { { ld_ident = add_model_trace_attr $1;
460
      ld_params = []; ld_type = Some $2;
461
      ld_def = $3; ld_loc = floc $startpos $endpos } }
462

463
function_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
464
| attrs(lident_rich) params cast preceded(EQUAL,term)?
465
466
  { { 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
467

468
predicate_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
469
| attrs(lident_rich) params preceded(EQUAL,term)?
470
471
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
472

473
with_logic_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
474
| WITH attrs(lident_rich) params cast? preceded(EQUAL,term)?
475
476
  { { 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
477

478
(* Inductive declarations *)
479
480

inductive_decl:
Andrei Paskevich's avatar
Andrei Paskevich committed
481
| attrs(lident_rich) params ind_defn
482
483
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
484

485
486
487
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
488

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

492
(* Type expressions *)
493

494
495
496
497
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
498

499
500
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
501
| quote_lident                      { PTtyvar $1 }
502
503
504
505
| uqualid DOT ty_block              { PTscope ($1, $3) }
| ty_block                          { $1 }

ty_block:
506
507
508
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
509
| LEFTBRC ty RIGHTBRC               { PTpure $2 }
510

511
512
cast:
| COLON ty  { $2 }
513

514
(* Parameters and binders *)
515

516
517
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
518
519
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
520
521
   names, whose type must be inferred. *)

522
params:  param*  { List.concat $1 }
523

524
binders: binder+ { List.concat $1 }
525
526
527

param:
| anon_binder
528
    { error_param (floc $startpos $endpos) }
529
530
| lident_nq attr+
    { error_param (floc $startpos $endpos) }
531
532
533
534
| ty_arg
    { [floc $startpos $endpos, None, false, $1] }
| LEFTPAR GHOST ty RIGHTPAR
    { [floc $startpos $endpos, None, true, $3] }
535
| LEFTPAR binder_vars_rest RIGHTPAR
536
    { match $2 with [l,_] -> error_param l
537
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
538
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
539
    { match $3 with [l,_] -> error_param l
540
541
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
542
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
543
| LEFTPAR GHOST binder_vars cast RIGHTPAR
544
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
545

546
547
binder:
| anon_binder
548
    { let l,i = $1 in [l, i, false, None] }
549
550
| lident_nq attr+
    { [floc $startpos $endpos, Some (add_attr $1 $2), false, None] }
551
552
553
554
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
555
          [floc $startpos $endpos, Some id, false, None]
556
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
557
558
559
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
560
561
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
562
| LEFTPAR binder_vars_rest RIGHTPAR
563
    { match $2 with [l,i] -> [l, i, false, None]
564
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
565
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
566
    { match $3 with [l,i] -> [l, i, true, None]
567
568
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
569
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
570
| LEFTPAR GHOST binder_vars cast RIGHTPAR
571
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
572

573
574
575
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
576

577
binder_vars_rest:
578
| binder_vars_head attr+ binder_var*
579
580
    { List.rev_append (match $1 with
        | (l, Some id) :: bl ->
581
582
583
            let l2 = floc $startpos($2) $endpos($2) in
            (Loc.join l l2, Some (add_attr id $2)) :: bl
        | _ -> assert false) $3 }
584
| binder_vars_head anon_binder binder_var*
585
    { List.rev_append $1 ($2 :: $3) }
586
| anon_binder binder_var*
587
    { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
588

589
binder_vars_head:
590
| ty {
591
592
    let of_id id = id.id_loc, Some id in
    let push acc = function
593
      | PTtyapp (Qident id, []) -> of_id id :: acc
594
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
595
    match $1 with
596
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
597
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
598

599
binder_var:
Andrei Paskevich's avatar
Andrei Paskevich committed
600
| attrs(lident_nq)  { floc $startpos $endpos, Some $1 }
Clément Fumex's avatar
Clément Fumex committed
601
| anon_binder       { $1 }
602
603

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

606
607
608
609
(* Logical terms *)

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

610
611
612
613
term:
| single_term %prec below_COMMA   { $1 }
| single_term COMMA term_
    { mk_term (Ttuple ($1::$3)) $startpos $endpos }
614
615

term_:
616
617
618
619
620
621
| single_term %prec below_COMMA   { [$1] }
| single_term COMMA term_         { $1::$3 }

single_term: t = mk_term(single_term_) { t }

single_term_:
622
623
| term_arg_
    { match $1 with (* break the infix relation chain *)
Andrei Paskevich's avatar
Andrei Paskevich committed
624
625
626
      | Tinfix (l,o,r) -> Tinnfix (l,o,r)
      | Tbinop (l,o,r) -> Tbinnop (l,o,r)
      | d -> d }
627
| NOT single_term
Andrei Paskevich's avatar
Andrei Paskevich committed
628
    { Tnot $2 }
629
| OLD single_term
Andrei Paskevich's avatar
Andrei Paskevich committed
630
    { Tat ($2, mk_id Dexpr.old_label $startpos($1) $endpos($1)) }
631
| single_term AT uident
632
    { Tat ($1, $3) }
633
| prefix_op single_term %prec prec_prefix_op
634
    { Tidapp (Qident $1, [$2]) }
635
| MINUS INTEGER
636
    { Tconst (Number.ConstInt (mk_int_const true $2)) }
637
| MINUS REAL
638
    { Tconst (Number.ConstReal (mk_real_const true $2)) }
639
| l = single_term ; o = bin_op ; r = single_term
640
    { Tbinop (l, o, r) }
641
| l = single_term ; o = infix_op_1 ; r = single_term
642
    { Tinfix (l, o, r) }
643
| l = single_term ; o = infix_op_234 ; r = single_term
644
    { Tidapp (Qident o, [l; r]) }
645
| term_arg located(term_arg)+
646
647
648
649
650
    { 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
651
    { let re_pat pat d = { pat with pat_desc = d } in
652
653
      let cast t ty = { t with term_desc = Tcast (t,ty) } in
      let rec unfold d p = match p.pat_desc with
654
        | Pparen p | Pscope (_,p) -> unfold d p
655
656
657
658
659
660
        | 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 }
661
| LET attrs(lident_op_nq) EQUAL term IN term
662
    { Tlet ($2, $4, $6) }
Andrei Paskevich's avatar
Andrei Paskevich committed
663
| LET attrs(lident_nq) mk_term(lam_defn) IN term
664
    { Tlet ($2, $3, $5) }
665
| LET attrs(lident_op_nq) mk_term(lam_defn) IN term
666
    { Tlet ($2, $3, $5) }
667
| MATCH term WITH match_cases(term) END
668
    { Tcase ($2, $4) }
669
| quant comma_list1(quant_vars) triggers DOT term
Andrei Paskevich's avatar
Andrei Paskevich committed
670
    { let l = List.map add_model_attrs (List.concat $2) in
671
      Tquant ($1, l, $3, $5) }
672
| FUN binders ARROW term
Andrei Paskevich's avatar
Andrei Paskevich committed
673
    { Tquant (Dterm.DTlambda, $2, [], $4) }
674
675
| EPSILON
    { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
Andrei Paskevich's avatar
Andrei Paskevich committed
676
677
| attr single_term %prec prec_attr
    { Tattr ($1, $2) }
678
| single_term cast
679
680
    { Tcast ($1, $2) }

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

684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
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 }

700
term_block_:
701
| BEGIN term END                                    { $2.term_desc }
702
| LEFTPAR term RIGHTPAR                             { $2.term_desc }
703
| BEGIN END                                         { Ttuple [] }
704
705
706
| 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
707
708

term_sub_:
709
710
| term_block_                                       { $1 }
| uqualid DOT mk_term(term_block_)                  { Tscope ($1, $3) }
Andrei Paskevich's avatar
M.()    
Andrei Paskevich committed
711
| term_dot DOT lqualid_rich                         { Tidapp ($3,[$1]) }
712
713
714
715
716
717
718
719
720
721
| 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]) }
722

723
724
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
725

726
match_cases(X):
727
728
729
730
| cl = bar_list1(match_case(X)) { cl }

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

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

735
triggers:
736
737
| (* epsilon *)                                                         { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(single_term)) RIGHTSQ  { $2 }
738

739
%inline bin_op:
Andrei Paskevich's avatar
Andrei Paskevich committed
740
741
742
743
744
745
| ARROW   { Dterm.DTimplies }
| LRARROW { Dterm.DTiff }
| OR      { Dterm.DTor }
| BARBAR  { Dterm.DTor_asym }
| AND     { Dterm.DTand }
| AMPAMP  { Dterm.DTand_asym }
746
747
| BY      { Dterm.DTby }
| SO      { Dterm.DTso }
748

749
quant:
Andrei Paskevich's avatar
Andrei Paskevich committed
750
751
| FORALL  { Dterm.DTforall }
| EXISTS  { Dterm.DTexists }
752

753
numeral:
754
755
| INTEGER { Number.ConstInt (mk_int_const false $1) }
| REAL    { Number.ConstReal (mk_real_const false $1) }
756

757
(* Program declarations *)
758

Andrei Paskevich's avatar
Andrei Paskevich committed
759
prog_decl:
760
761
762
763
764
765
766
767
768
769
770
771
| VAL ghost kind attrs(lident_rich) mk_expr(val_defn)
    { Dlet (add_model_trace_attr $4, ghost $2, $3, apply_partial $2 $5) }
| LET ghost kind attrs(lident_rich) mk_expr(fun_defn)
    { Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
| LET ghost kind attrs(lident_rich) const_defn
    { Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
| 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) }
772
773

ghost: