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

%{
13
module Increment = struct
14
15
16
17
18
19
20
  let stack = Stack.create ()
  let open_file inc = Stack.push inc stack
  let close_file () = ignore (Stack.pop stack)
  let open_theory id = (Stack.top stack).Ptree.open_theory id
  let close_theory () = (Stack.top stack).Ptree.close_theory ()
  let open_module id = (Stack.top stack).Ptree.open_module id
  let close_module () = (Stack.top stack).Ptree.close_module ()
21
22
  let open_namespace n = (Stack.top stack).Ptree.open_namespace n
  let close_namespace l b = (Stack.top stack).Ptree.close_namespace l b
23
24
25
  let new_decl loc d = (Stack.top stack).Ptree.new_decl loc d
  let new_pdecl loc d = (Stack.top stack).Ptree.new_pdecl loc d
  let use_clone loc use = (Stack.top stack).Ptree.use_clone loc use
26
end
27

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28
29
  open Ptree

30
  let infix  s = "infix "  ^ s
31
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
32
  let mixfix s = "mixfix " ^ s
33

34
  let qualid_last = function Qident x | Qdot (_, x) -> x.id_str
Andrei Paskevich's avatar
Andrei Paskevich committed
35

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

38
  let model_label = Ident.create_label "model"
39
  let model_projected = Ident.create_label "model_projected"
40
41
42
43
44

  let is_model_label l =
    match l with
    | Lpos _ -> false
    | Lstr lab ->
45
46
      (lab = model_label) || (lab = model_projected)

47

48
  let model_lab_present labels =
49
50
51
52
53
54
55
56
57
58
59
    try
      ignore(List.find is_model_label labels);
      true
    with Not_found ->
      false

  let model_trace_regexp = Str.regexp "model_trace:"

  let is_model_trace_label l =
    match l with
    | Lpos _ -> false
60
    | Lstr lab ->
61
      try
62
	ignore(Str.search_forward model_trace_regexp lab.Ident.lab_string 0);
63
64
65
66
67
68
69
70
71
72
73
	true
      with Not_found -> false

  let model_trace_lab_present labels =
    try
      ignore(List.find is_model_trace_label labels);
      true
    with Not_found ->
      false

  let add_model_trace name labels =
74
    if (model_lab_present labels) && (not (model_trace_lab_present labels)) then
75
76
      (Lstr (Ident.create_label ("model_trace:" ^ name)))::labels
    else
77
      labels
78
79
80
81

  let add_lab id l =
    let l = add_model_trace id.id_str l in
    { id with id_lab = l }
82

83
  let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
84

85
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
86

87
88
  let get_op s e = Qident (mk_id (mixfix "[]") s e)
  let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
89
90
91
  let sub_op s e = Qident (mk_id (mixfix "[_.._]") s e)
  let above_op s e = Qident (mk_id (mixfix "[_..]") s e)
  let below_op s e = Qident (mk_id (mixfix "[.._]") s e)
92

93
94
  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 }
95
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
96

97
98
99
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
100
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
101
102
103
104
105
106
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
107
    sp_reads   = [];
108
109
    sp_writes  = [];
    sp_variant = [];
110
111
    sp_checkrw = false;
    sp_diverge = false;
112
  }
113

114
115
116
117
  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;
118
    sp_reads   = s1.sp_reads @ s2.sp_reads;
119
120
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
121
122
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
123
  }
124

125
(* dead code
126
  let add_init_mark e =
127
    let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
128
    { e with expr_desc = Emark (init, e) }
129
*)
130

131
  let small_integer i =
132
    try match i with
133
134
135
136
      | Number.IConstDec s -> int_of_string s
      | Number.IConstHex s -> int_of_string ("0x"^s)
      | Number.IConstOct s -> int_of_string ("0o"^s)
      | Number.IConstBin s -> int_of_string ("0b"^s)
137
    with Failure _ -> raise Error
138

139
140
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
141

142
143
144
145
146
  let error_loc loc = Loc.error ~loc Error

  let () = Exn_printer.register (fun fmt exn -> match exn with
    | Error -> Format.fprintf fmt "syntax error"
    | _ -> raise exn)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
147
148
%}

149
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
150

Clément Fumex's avatar
Clément Fumex committed
151
%token <string> LIDENT LIDENT_QUOTE UIDENT UIDENT_QUOTE
152
%token <Ptree.integer_constant> INTEGER
153
%token <string> OP1 OP2 OP3 OP4 OPPREF
Clément Fumex's avatar
Clément Fumex committed
154
%token <Ptree.real_constant> REAL
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155
%token <string> STRING
156
%token <Loc.position> POSITION
157
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
158

159
(* keywords *)
160

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

167
(* program keywords *)
168

169
170
171
172
173
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE
%token PRIVATE RAISE RAISES READS REC REQUIRES RETURNS
%token TO TRY VAL VARIANT WHILE WRITES
174

175
(* symbols *)
176

Andrei Paskevich's avatar
Andrei Paskevich committed
177
%token AND ARROW
178
%token BAR
179
%token COLON COMMA
Clément Fumex's avatar
Clément Fumex committed
180
%token DOT DOTDOT EQUAL LAMBDA LT GT LTGT
181
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
182
%token LARROW LRARROW OR
183
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
184
%token UNDERSCORE
185
186
187

%token EOF

188
(* program symbols *)
189

190
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
191

192
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193

194
%nonassoc IN
195
196
197
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
198
%nonassoc prec_no_else
199
%nonassoc DOT ELSE GHOST
200
%nonassoc prec_named
201
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
202

Andrei Paskevich's avatar
Andrei Paskevich committed
203
%right ARROW LRARROW
Martin Clochard's avatar
Martin Clochard committed
204
%right BY SO
205
206
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
207
%nonassoc NOT
Clément Fumex's avatar
Clément Fumex committed
208
%left EQUAL LTGT LT GT OP1
209
%nonassoc LARROW
210
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
211
%left OP2
212
%left OP3
213
%left OP4
214
%nonassoc prec_prefix_op
215
216
%nonassoc LEFTSQ
%nonassoc OPPREF
217

218
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
219

220
221
%start <Ptree.incremental -> unit> open_file
%start <unit> logic_file program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
222
223
%%

224
225
(* Theories, modules, namespaces *)

226
open_file:
227
(* Dummy token. Menhir does not accept epsilon. *)
228
| EOF { Increment.open_file }
229

Andrei Paskevich's avatar
Andrei Paskevich committed
230
logic_file:
231
| theory* EOF   { Increment.close_file () }
232

233
program_file:
234
| theory_or_module* EOF { Increment.close_file () }
235

236
theory:
237
| theory_head theory_decl* END  { Increment.close_theory () }
238

239
240
theory_or_module:
| theory                        { () }
241
| module_head module_decl* END  { Increment.close_module () }
242

243
theory_head:
Clément Fumex's avatar
Clément Fumex committed
244
| THEORY labels(uident_nq)  { Increment.open_theory $2 }
245

246
module_head:
Clément Fumex's avatar
Clément Fumex committed
247
| MODULE labels(uident_nq)  { Increment.open_module $2 }
248

249
theory_decl:
250
251
| decl            { Increment.new_decl  (floc $startpos $endpos) $1 }
| use_clone       { Increment.use_clone (floc $startpos $endpos) $1 }
252
| namespace_head theory_decl* END
253
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
254

255
module_decl:
256
257
258
| decl            { Increment.new_decl  (floc $startpos $endpos) $1 }
| pdecl           { Increment.new_pdecl (floc $startpos $endpos) $1 }
| use_clone       { Increment.use_clone (floc $startpos $endpos) $1 }
259
| namespace_head module_decl* END
260
    { Increment.close_namespace (floc $startpos($1) $endpos($1)) $1 }
261

262
namespace_head:
Clément Fumex's avatar
Clément Fumex committed
263
| NAMESPACE boption(IMPORT) uident_nq
264
   { Increment.open_namespace $3.id_str; $2 }
265

266
(* Use and clone *)
267

268
use_clone:
269
270
271
| USE use                                 { ($2, None) }
| CLONE use                               { ($2, Some []) }
| CLONE use WITH comma_list1(clone_subst) { ($2, Some $4) }
272

273
use:
274
| boption(IMPORT) tqualid
275
    { { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
276
277
| boption(IMPORT) tqualid AS uident
    { { use_theory = $2; use_import = Some ($1, $4.id_str) } }
278
279
| EXPORT tqualid
    { { use_theory = $2; use_import = None } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
280

281
clone_subst:
282
283
| NAMESPACE ns EQUAL ns         { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid ty_var* EQUAL ty  { CStsym  (floc $startpos $endpos, $2,$3,$5) }
284
285
286
287
288
289
| CONSTANT  qualid EQUAL qualid { CSfsym  (floc $startpos $endpos, $2,$4) }
| FUNCTION  qualid EQUAL qualid { CSfsym  (floc $startpos $endpos, $2,$4) }
| PREDICATE qualid EQUAL qualid { CSpsym  (floc $startpos $endpos, $2,$4) }
| VAL       qualid EQUAL qualid { CSvsym  (floc $startpos $endpos, $2,$4) }
| LEMMA     qualid              { CSlemma (floc $startpos $endpos, $2) }
| GOAL      qualid              { CSgoal  (floc $startpos $endpos, $2) }
290

291
292
293
ns:
| uqualid { Some $1 }
| DOT     { None }
294

295
296
297
298
299
300
301
302
303
304
(* Theory declarations *)

decl:
| TYPE with_list1(type_decl)                { Dtype $2 }
| TYPE late_invariant                       { Dtype [$2] }
| CONSTANT  constant_decl                   { Dlogic [$2] }
| FUNCTION  function_decl  with_logic_decl* { Dlogic ($2::$3) }
| PREDICATE predicate_decl with_logic_decl* { Dlogic ($2::$3) }
| INDUCTIVE   with_list1(inductive_decl)    { Dind (Decl.Ind, $2) }
| COINDUCTIVE with_list1(inductive_decl)    { Dind (Decl.Coind, $2) }
Clément Fumex's avatar
Clément Fumex committed
305
306
307
| AXIOM labels(ident_nq) COLON term         { Dprop (Decl.Paxiom, $2, $4) }
| LEMMA labels(ident_nq) COLON term         { Dprop (Decl.Plemma, $2, $4) }
| GOAL  labels(ident_nq) COLON term         { Dprop (Decl.Pgoal, $2, $4) }
308
| META sident comma_list1(meta_arg)         { Dmeta ($2, $3) }
309
310

meta_arg:
311
312
313
314
315
316
317
| TYPE      ty      { Mty $2 }
| CONSTANT  qualid  { Mfs $2 }
| FUNCTION  qualid  { Mfs $2 }
| PREDICATE qualid  { Mps $2 }
| PROP      qualid  { Mpr $2 }
| STRING            { Mstr $1 }
| INTEGER           { Mint (small_integer $1) }
318
319

(* Type declarations *)
320
321

type_decl:
Clément Fumex's avatar
Clément Fumex committed
322
| labels(lident_nq) ty_var* typedefn
323
  { let model, vis, def, inv = $3 in
324
    let vis = if model then Abstract else vis in
325
326
327
    { td_ident = $1; td_params = $2;
      td_model = model; td_vis = vis; td_def = def;
      td_inv = inv; td_loc = floc $startpos $endpos } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
328

329
late_invariant:
Clément Fumex's avatar
Clément Fumex committed
330
| labels(lident_nq) ty_var* invariant+
331
332
333
  { { td_ident = $1; td_params = $2;
      td_model = false; td_vis = Public; td_def = TDabstract;
      td_inv = $3; td_loc = floc $startpos $endpos } }
334

335
ty_var:
336
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
337
338

typedefn:
339
| (* epsilon *)
340
    { false, Public, TDabstract, [] }
341
| model abstract bar_list1(type_case) invariant*
342
    { $1, $2, TDalgebraic $3, $4 }
343
| model abstract LEFTBRC semicolon_list1(type_field) RIGHTBRC invariant*
344
    { $1, $2, TDrecord $4, $6 }
345
346
| model abstract ty invariant*
    { $1, $2, TDalias $3, $4 }
Clément Fumex's avatar
Clément Fumex committed
347
348
349
350
351
352
353
(* FIXME: allow negative bounds *)
| EQUAL LT RANGE INTEGER INTEGER GT
    { false, Public,
      TDrange (Number.compute_int $4, Number.compute_int $5), [] }
| EQUAL LT FLOAT INTEGER INTEGER GT
    { false, Public,
      TDfloat (small_integer $4, small_integer $5), [] }
354

355
356
357
358
359
model:
| EQUAL         { false }
| MODEL         { true }

abstract:
360
| (* epsilon *) { Public }
361
362
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
363

364
type_field:
Clément Fumex's avatar
Clément Fumex committed
365
| field_modifiers labels(lident_nq) cast
366
367
  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
      f_pty = $3; f_loc = floc $startpos $endpos } }
368

369
field_modifiers:
370
| (* epsilon *) { false, false }
371
372
373
374
375
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

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

379
(* Logic declarations *)
380

381
382
constant_decl:
| labels(lident_rich) cast preceded(EQUAL,term)?
383
384
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
385

386
387
function_decl:
| labels(lident_rich) params cast preceded(EQUAL,term)?
388
389
  { { 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
390

391
392
predicate_decl:
| labels(lident_rich) params preceded(EQUAL,term)?
393
394
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
395

396
with_logic_decl:
397
| WITH labels(lident_rich) params cast? preceded(EQUAL,term)?
398
399
  { { 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
400

401
(* Inductive declarations *)
402
403

inductive_decl:
404
| labels(lident_rich) params ind_defn
405
406
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
407

408
409
410
ind_defn:
| (* epsilon *)             { [] }
| EQUAL bar_list1(ind_case) { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
411

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

415
(* Type expressions *)
416

417
418
419
420
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
421

422
423
424
425
426
427
428
ty_arg:
| lqualid                           { PTtyapp ($1, []) }
| quote_lident                      { PTtyvar ($1, false) }
| opaque_quote_lident               { PTtyvar ($1, true) }
| LEFTPAR comma_list2(ty) RIGHTPAR  { PTtuple $2 }
| LEFTPAR RIGHTPAR                  { PTtuple [] }
| LEFTPAR ty RIGHTPAR               { PTparen $2 }
429

430
431
cast:
| COLON ty  { $2 }
432

433
(* Parameters and binders *)
434

435
436
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
437
438
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
439
440
   names, whose type must be inferred. *)

441
params:  param*  { List.concat $1 }
442

443
binders: binder+ { List.concat $1 }
444
445
446

param:
| anon_binder
447
448
449
450
451
452
453
454
    { error_param (floc $startpos $endpos) }
| ty_arg
    { [floc $startpos $endpos, None, false, $1] }
| LEFTPAR GHOST ty RIGHTPAR
    { [floc $startpos $endpos, None, true, $3] }
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident _, []) ->
455
456
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
457
| LEFTPAR binder_vars_rest RIGHTPAR
458
    { match $2 with [l,_] -> error_param l
459
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
460
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
461
    { match $3 with [l,_] -> error_param l
462
463
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
464
    { List.map (fun (l,i) -> l, i, false, $3) $2 }
465
| LEFTPAR GHOST binder_vars cast RIGHTPAR
466
    { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
467

468
469
binder:
| anon_binder
470
471
472
473
474
    { error_param (floc $startpos $endpos) }
| ty_arg
    { match $1 with
      | PTtyapp (Qident id, [])
      | PTparen (PTtyapp (Qident id, [])) ->
475
476
             [floc $startpos $endpos, Some id, false, None]
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
477
478
479
| LEFTPAR GHOST ty RIGHTPAR
    { match $3 with
      | PTtyapp (Qident id, []) ->
480
481
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
482
483
484
| ty_arg label label*
    { match $1 with
      | PTtyapp (Qident id, []) ->
485
486
487
             let id = add_lab id ($2::$3) in
             [floc $startpos $endpos, Some id, false, None]
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
488
| LEFTPAR binder_vars_rest RIGHTPAR
489
    { match $2 with [l,i] -> [l, i, false, None]
490
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
491
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
492
    { match $3 with [l,i] -> [l, i, true, None]
493
494
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
495
    { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
496
| LEFTPAR GHOST binder_vars cast RIGHTPAR
497
    { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
498

499
500
501
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
502

503
binder_vars_rest:
504
505
506
507
508
509
510
| binder_vars_head label label* binder_var*
    { List.rev_append (match $1 with
        | (l, Some id) :: bl ->
            let l3 = floc $startpos($3) $endpos($3) in
            (Loc.join l l3, Some (add_lab id ($2::$3))) :: bl
        | _ -> assert false) $4 }
| binder_vars_head anon_binder binder_var*
511
   { List.rev_append $1 ($2 :: $3) }
512
| anon_binder binder_var*
513
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
514

515
binder_vars_head:
516
| ty {
517
518
    let of_id id = id.id_loc, Some id in
    let push acc = function
519
      | PTtyapp (Qident id, []) -> of_id id :: acc
520
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
521
    match $1 with
522
      | PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
523
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
524

525
binder_var:
Clément Fumex's avatar
Clément Fumex committed
526
527
| labels(lident_nq) { floc $startpos $endpos, Some $1 }
| anon_binder       { $1 }
528
529

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

532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
(* Logical terms *)

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

term: t = mk_term(term_) { t }

term_:
| term_arg_
    { match $1 with (* break the infix relation chain *)
      | Tinfix (l,o,r) -> Tinnfix (l,o,r) | d -> d }
| NOT term
    { Tunop (Tnot, $2) }
| prefix_op term %prec prec_prefix_op
    { Tidapp (Qident $1, [$2]) }
| l = term ; o = bin_op ; r = term
    { Tbinop (l, o, r) }
| l = term ; o = infix_op ; r = term
    { Tinfix (l, o, r) }
| term_arg located(term_arg)+ (* FIXME/TODO: "term term_arg" *)
    { let join f (a,_,e) = mk_term (Tapply (f,a)) $startpos e in
      (List.fold_left join $1 $2).term_desc }
| IF term THEN term ELSE term
    { Tif ($2, $4, $6) }
| LET pattern EQUAL term IN term
    { match $2.pat_desc with
      | Pvar id -> Tlet (id, $4, $6)
      | Pwild -> Tlet (id_anonymous $2.pat_loc, $4, $6)
      | Ptuple [] -> Tlet (id_anonymous $2.pat_loc,
          { $4 with term_desc = Tcast ($4, PTtuple []) }, $6)
561
562
563
564
565
      | Pcast ({pat_desc = Pvar id}, ty) ->
          Tlet (id, { $4 with term_desc = Tcast ($4, ty) }, $6)
      | Pcast ({pat_desc = Pwild}, ty) ->
          let id = id_anonymous $2.pat_loc in
          Tlet (id, { $4 with term_desc = Tcast ($4, ty) }, $6)
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
      | _ -> Tmatch ($4, [$2, $6]) }
| MATCH term WITH match_cases(term) END
    { Tmatch ($2, $4) }
| MATCH comma_list2(term) WITH match_cases(term) END
    { Tmatch (mk_term (Ttuple $2) $startpos($2) $endpos($2), $4) }
| quant comma_list1(quant_vars) triggers DOT term
    { Tquant ($1, List.concat $2, $3, $5) }
| EPSILON
    { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
| label term %prec prec_named
    { Tnamed ($1, $2) }
| term cast
    { Tcast ($1, $2) }

term_arg: mk_term(term_arg_) { $1 }
term_dot: mk_term(term_dot_) { $1 }

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

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

term_sub_:
| term_dot DOT lqualid_rich                         { Tidapp ($3,[$1]) }
| LEFTPAR term RIGHTPAR                             { $2.term_desc }
| LEFTPAR RIGHTPAR                                  { Ttuple [] }
| LEFTPAR comma_list2(term) RIGHTPAR                { Ttuple $2 }
| LEFTBRC field_list1(term) RIGHTBRC                { Trecord $2 }
| LEFTBRC term_arg WITH field_list1(term) RIGHTBRC  { Tupdate ($2,$4) }
| term_arg LEFTSQ term RIGHTSQ
    { Tidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
| term_arg LEFTSQ term LARROW term RIGHTSQ
    { Tidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
608
609
610
611
612
613
| term_arg LEFTSQ term DOTDOT term RIGHTSQ
    { Tidapp (sub_op $startpos($2) $endpos($2), [$1;$3;$5]) }
| term_arg LEFTSQ term DOTDOT RIGHTSQ
    { Tidapp (above_op $startpos($2) $endpos($2), [$1;$3]) }
| term_arg LEFTSQ DOTDOT term RIGHTSQ
    { Tidapp (below_op $startpos($2) $endpos($2), [$1;$4]) }
614

615
616
field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
617

618
619
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
620

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

624
625
626
triggers:
| (* epsilon *)                                                 { [] }
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
627

628
629
630
631
632
633
634
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| BARBAR  { Tor_asym }
| AND     { Tand }
| AMPAMP  { Tand_asym }
Martin Clochard's avatar
Martin Clochard committed
635
636
| BY      { Tby }
| SO      { Tso }
637

638
639
640
641
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }
| LAMBDA  { Tlambda }
642

643
644
numeral:
| INTEGER { Number.ConstInt $1 }
Clément Fumex's avatar
Clément Fumex committed
645
| REAL    { Number.ConstReal $1 }
646

647
(* Program declarations *)
648

649
pdecl:
650
| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
651
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
652
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
653
| LET REC with_list1(rec_defn)                      { Drec $3 }
Clément Fumex's avatar
Clément Fumex committed
654
655
| EXCEPTION labels(uident_nq)                       { Dexn ($2, PTtuple []) }
| EXCEPTION labels(uident_nq) ty                    { Dexn ($2, $3) }
656

657
658
659
660
661
662
top_ghost:
| (* epsilon *) { Gnone  }
| GHOST         { Gghost }
| LEMMA         { Glemma }

(* Function declarations *)
663
664

type_v:
665
| arrow_type_v  { $1 }
666
| cast          { PTpure $1 }
667
668

arrow_type_v:
669
| param params tail_type_c  { PTfunc ($1 @ $2, $3) }
670
671

tail_type_c:
672
673
| single_spec spec arrow_type_v { $3, spec_union $1 $2 }
| COLON simple_type_c           { $2 }
674
675

simple_type_c:
676
677
678
| ty spec { PTpure $1, $2 }

(* Function definitions *)
679

680
rec_defn:
681
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
682
    { $2, $1, ($3, $4, $8, spec_union $5 $7) }
683

684
fun_defn:
685
| binders cast? spec EQUAL spec seq_expr { ($1, $2, $6, spec_union $3 $5) }
686

687
fun_expr:
688
689
| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }

690
691
692
693
694
695
696
697
(* Program expressions *)

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

seq_expr:
| expr %prec below_SEMI   { $1 }
| expr SEMICOLON          { $1 }
| expr SEMICOLON seq_expr { mk_expr (Esequence ($1, $3)) $startpos $endpos }
698

699
expr: e = mk_expr(expr_) { e }
700
701
702

expr_:
| expr_arg_
703
704
    { match $1 with (* break the infix relation chain *)
      | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
705
| NOT expr %prec prec_prefix_op
706
    { Enot $2 }
707
| prefix_op expr %prec prec_prefix_op
708
709
710
711
712
713
714
715
    { Eidapp (Qident $1, [$2]) }
| l = expr ; o = lazy_op ; r = expr
    { Elazy (l,o,r) }
| l = expr ; o = infix_op ; r = expr
    { Einfix (l,o,r) }
| expr_arg located(expr_arg)+ (* FIXME/TODO: "expr expr_arg" *)
    { let join f (a,_,e) = mk_expr (Eapply (f,a)) $startpos e in
      (List.fold_left join $1 $2).expr_desc }
716
| IF seq_expr THEN expr ELSE expr
717
    { Eif ($2, $4, $6) }
718
| IF seq_expr THEN expr %prec prec_no_else
719
720
721
722
723
724
725
    { Eif ($2, $4, mk_expr (Etuple []) $startpos $endpos) }
| expr LARROW expr
    { match $1.expr_desc with
      | Eidapp (q, [e1]) -> Eassign (e1, q, $3)
      | Eidapp (Qident id, [e1;e2]) when id.id_str = mixfix "[]" ->
          Eidapp (Qident {id with id_str = mixfix "[]<-"}, [e1;e2;$3])
      | _ -> raise Error }
726
| LET top_ghost pattern EQUAL seq_expr IN seq_expr
727
    { match $3.pat_desc with
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
      | Pvar id -> Elet (id, $2, $5, $7)
      | Pwild -> Elet (id_anonymous $3.pat_loc, $2, $5, $7)
      | Ptuple [] -> Elet (id_anonymous $3.pat_loc, $2,
          { $5 with expr_desc = Ecast ($5, PTtuple []) }, $7)
      | Pcast ({pat_desc = Pvar id}, ty) ->
          Elet (id, $2, { $5 with expr_desc = Ecast ($5, ty) }, $7)
      | Pcast ({pat_desc = Pwild}, ty) ->
          let id = id_anonymous $3.pat_loc in
          Elet (id, $2, { $5 with expr_desc = Ecast ($5, ty) }, $7)
      | _ ->
          let e = match $2 with
            | Glemma -> Loc.errorm ~loc:($3.pat_loc)
                "`let lemma' cannot be used with complex patterns"
            | Gghost -> { $5 with expr_desc = Eghost $5 }
            | Gnone -> $5 in
          Ematch (e, [$3, $7]) }
| LET top_ghost labels(lident_op_id) EQUAL seq_expr IN seq_expr
    { Elet ($3, $2, $5, $7) }
Clément Fumex's avatar
Clément Fumex committed
746
| LET top_ghost labels(lident_nq) fun_defn IN seq_expr
747
748
749
    { Efun ($3, $2, $4, $6) }
| LET top_ghost labels(lident_op_id) fun_defn IN seq_expr
    { Efun ($3, $2, $4, $6) }
750
| LET REC with_list1(rec_defn) IN seq_expr
751
    { Erec ($3, $5) }
752
| fun_expr
753
754
755
756
757
758
759
    { Elam $1 }
| VAL top_ghost labels(lident_rich) mk_expr(val_expr) IN seq_expr
    { Elet ($3, $2, $4, $6) }
| MATCH seq_expr WITH match_cases(seq_expr) END
    { Ematch ($2, $4) }
| MATCH comma_list2(expr) WITH match_cases(seq_expr) END
    { Ematch (mk_expr (Etuple $2) $startpos($2) $endpos($2), $4) }
760
| quote_uident COLON seq_expr
761
    { Emark ($1, $3) }
762
| LOOP loop_annotation seq_expr END
763
    { Eloop ($2, $3) }
764
| WHILE seq_expr DO loop_annotation seq_expr DONE
765
766
767
    { Ewhile ($2, $4, $5) }
| FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
    { Efor ($2, $4, $5, $6, $8, $9) }
768
| ABSURD
769
    { Eabsurd }
770
| RAISE uqualid
771
    { Eraise ($2, None) }
772
| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
773
774
775
    { Eraise ($3, Some $4) }
| TRY seq_expr WITH bar_list1(exn_handler) END
    { Etry ($2, $4) }
776
| ANY simple_type_c
777
    { Eany $2 }
778
| GHOST expr
779
    { Eghost $2 }
780
| ABSTRACT spec seq_expr END
781
782
783
    { Eabstract($3, $2) }
| assertion_kind LEFTBRC term RIGHTBRC
    { Eassert ($1, $3) }
784
| label expr %prec prec_named
785
786
787
    { Enamed ($1, $2) }
| expr cast
    { Ecast ($1, $2) }
788

789
790
expr_arg: e = mk_expr(expr_arg_) { e }
expr_dot: e = mk_expr(expr_dot_) { e }
791
792

expr_arg_:
793
794
795
796
797
798
799
800
801
802
803
| qualid                    { Eident $1 }
| numeral                   { Econst $1 }
| TRUE                      { Etrue }
| FALSE                     { Efalse }
| o = oppref ; a = expr_arg { Eidapp (Qident o, [a]) }
| expr_sub                  { $1 }

expr_dot_:
| lqualid                   { Eident $1 }
| o = oppref ; a = expr_dot { Eidapp (Qident o, [a]) }
| expr_sub                  { $1 }
804
805

expr_sub:
806
| expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
807
808
809
810
811
812
813
| BEGIN seq_expr END                                { $2.expr_desc }
| LEFTPAR seq_expr RIGHTPAR                         { $2.expr_desc }
| BEGIN END                                         { Etuple [] }
| LEFTPAR RIGHTPAR                                  { Etuple [] }
| LEFTPAR comma_list2(expr) RIGHTPAR                { Etuple $2 }
| LEFTBRC field_list1(expr) RIGHTBRC                { Erecord $2 }
| LEFTBRC expr_arg WITH field_list1(expr) RIGHTBRC  { Eupdate ($2, $4) }
814
| expr_arg LEFTSQ expr RIGHTSQ
815
    { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
816
| expr_arg LEFTSQ expr LARROW expr RIGHTSQ
817
    { Eidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
818
819
820
821
822
823
| expr_arg LEFTSQ expr DOTDOT expr RIGHTSQ
    { Eidapp (sub_op $startpos($2) $endpos($2), [$1;$3;$5]) }
| expr_arg LEFTSQ expr DOTDOT RIGHTSQ
    { Eidapp (above_op $startpos($2) $endpos($2), [$1;$3]) }
| expr_arg LEFTSQ DOTDOT expr RIGHTSQ
    { Eidapp (below_op $startpos($2) $endpos($2), [$1;$4]) }
824

825
826
827
828
829
830
831
loop_annotation:
| (* epsilon *)
    { { loop_invariant = []; loop_variant = [] } }
| invariant loop_annotation
    { let a = $2 in { a with loop_invariant = $1 :: a.loop_invariant } }
| variant loop_annotation
    { let a = $2 in { a with loop_variant = variant_union $1 a.loop_variant } }
832

833
834
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }