parser.mly 31.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11 12

%{
13
module Incremental = 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
32
  let mixfix s = "mixfix " ^ s
33

34
  let qualid_last = function Qident x | Qdot (_, x) -> x.id
35

36
  let floc s e = Loc.extract (s,e)
37

38
  let add_lab id l = { id with id_lab = l }
39

40
  let id_anonymous loc = { id = "_"; id_lab = []; id_loc = loc }
41

42
  let mk_id id s e = { id = id; id_lab = []; id_loc = floc s e }
43

44
  let mk_pat d s e = { pat_desc = d; pat_loc = floc s e }
45

46
  let mk_pp d s e = { pp_desc = d; pp_loc = floc s e }
47

48
  let mk_expr d s e = { expr_desc = d; expr_loc = floc s e }
49

50 51 52
  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
53
    | _, ({pp_loc = loc},_)::_ -> Loc.errorm ~loc
54 55 56 57 58 59
        "multiple `variant' clauses are not allowed"

  let empty_spec = {
    sp_pre     = [];
    sp_post    = [];
    sp_xpost   = [];
60
    sp_reads   = [];
61 62
    sp_writes  = [];
    sp_variant = [];
63 64
    sp_checkrw = false;
    sp_diverge = false;
65
  }
66

67 68 69 70
  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;
71
    sp_reads   = s1.sp_reads @ s2.sp_reads;
72 73
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
74 75
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
76
  }
77

78
(* dead code
79
  let add_init_mark e =
80
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
81
    { e with expr_desc = Emark (init, e) }
82
*)
83

84
  let small_integer i =
85
    try match i with
86 87 88 89
      | 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)
90
    with Failure _ -> raise Error
91

92 93
  let error_param loc =
    Loc.errorm ~loc "cannot determine the type of the parameter"
94

95 96 97 98 99
  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
100 101
%}

102
(* Tokens *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
103

104
%token <string> LIDENT UIDENT
105
%token <Ptree.integer_constant> INTEGER
106
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107 108
%token <Ptree.real_constant> FLOAT
%token <string> STRING
109
%token <Loc.position> POSITION
110
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
111

112
(* keywords *)
113

114
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
115 116 117
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
118
%token THEN THEORY TRUE TYPE USE WITH
119

120
(* program keywords *)
121

122 123 124 125 126
%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
127

128
(* symbols *)
129

Andrei Paskevich's avatar
Andrei Paskevich committed
130
%token AND ARROW
131
%token BAR
132
%token COLON COMMA
133
%token DOT EQUAL LAMBDA LTGT
134
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
135
%token LARROW LRARROW OR
136
%token RIGHTPAR RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
137
%token UNDERSCORE
138 139 140

%token EOF

141
(* program symbols *)
142

143
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
144

145
(* Precedences *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
146

147
%nonassoc IN
148 149 150
%nonassoc below_SEMI
%nonassoc SEMICOLON
%nonassoc LET VAL
151
%nonassoc prec_no_else
152
%nonassoc DOT ELSE GHOST
153
%nonassoc prec_named
154
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155

Andrei Paskevich's avatar
Andrei Paskevich committed
156
%right ARROW LRARROW
157 158
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
159
%nonassoc NOT
160
%left EQUAL LTGT OP1
161
%nonassoc LARROW
162
%nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
163
%left OP2
164
%left OP3
165
%left OP4
166
%nonassoc prec_prefix_op
167 168
%nonassoc LEFTSQ
%nonassoc OPPREF
169

170
(* Entry points *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
171

172 173
%start <Ptree.incremental -> unit> open_file
%start <unit> logic_file program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174 175
%%

176
open_file:
177
| (* epsilon *) { Incremental.open_file }
178

179
logic_file:
180
| theory* EOF   { Incremental.close_file () }
181

182 183
theory:
| theory_head theory_decl* END  { Incremental.close_theory () }
184

185
theory_head:
186
| THEORY labels(uident)  { Incremental.open_theory $2 }
187

188 189 190 191 192
theory_decl:
| decl            { Incremental.new_decl  (floc $startpos $endpos) $1 }
| use_clone       { Incremental.use_clone (floc $startpos $endpos) $1 }
| namespace_head theory_decl* END
    { Incremental.close_namespace (floc $startpos($1) $endpos($1)) $1 }
193

194
namespace_head:
195 196
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
197 198

namespace_import:
199
| (* epsilon *)  { false }
200 201
| IMPORT         { true }

202
(* Declaration *)
203

204
decl:
205 206 207 208 209 210 211 212 213 214
| TYPE with_list1(type_decl)                      { TypeDecl $2 }
| TYPE late_invariant                             { TypeDecl [$2] }
| CONSTANT logic_decl_constant                    { LogicDecl [$2] }
| FUNCTION logic_decl_function with_logic_decl*   { LogicDecl ($2::$3) }
| PREDICATE logic_decl_predicate with_logic_decl* { LogicDecl ($2::$3) }
| inductive with_list1(inductive_decl)            { IndDecl ($1, $2) }
| AXIOM labels(ident) COLON lexpr                 { PropDecl (Kaxiom, $2, $4) }
| LEMMA labels(ident) COLON lexpr                 { PropDecl (Klemma, $2, $4) }
| GOAL labels(ident) COLON lexpr                  { PropDecl (Kgoal, $2, $4) }
| META sident comma_list1(meta_arg)               { Meta ($2, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
215

216 217 218 219
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }

220
(* Use and clone *)
221

222
use_clone:
223 224
| USE use               { ($2, None) }
| CLONE use clone_subst { ($2, Some $3) }
225

226
use:
227 228 229 230 231 232
| opt_import tqualid
    { { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
| opt_import tqualid AS uident
    { { use_theory = $2; use_import = Some ($1, $4.id) } }
| EXPORT tqualid
    { { use_theory = $2; use_import = None } }
233

234
opt_import:
235
| (* epsilon *) { false }
236
| IMPORT        { true  }
237 238

clone_subst:
239 240
| (* epsilon *)                               { [] }
| WITH comma_list1(subst)  { $2 }
241 242

subst:
243 244 245 246 247 248 249 250 251
| NAMESPACE ns     EQUAL ns     { CSns    (floc $startpos $endpos, $2,$4) }
| TYPE qualid type_arg* EQUAL primitive_type
                                { CStsym  (floc $startpos $endpos, $2,$3,$5) }
| 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) }
252

253 254 255
ns:
| uqualid { Some $1 }
| DOT     { None }
256

257
(* Meta args *)
258 259

meta_arg:
260 261 262 263 264 265 266 267 268
| TYPE primitive_type { PMAty  $2 }
| CONSTANT  qualid    { PMAfs  $2 }
| FUNCTION  qualid    { PMAfs  $2 }
| PREDICATE qualid    { PMAps  $2 }
| PROP      qualid    { PMApr  $2 }
| STRING              { PMAstr $1 }
| INTEGER             { PMAint (small_integer $1) }

(* Type declarations *)
269 270

type_decl:
271 272
| labels(lident) type_arg* typedefn
  { let model, vis, def, inv = $3 in
273
    let vis = if model then Abstract else vis in
274 275 276
    { td_ident = $1; td_params = $2;
      td_model = model; td_vis = vis; td_def = def;
      td_inv = inv; td_loc = floc $startpos $endpos } }
277

278
late_invariant:
279 280 281 282
| labels(lident) type_arg* invariant+
  { { td_ident = $1; td_params = $2;
      td_model = false; td_vis = Public; td_def = TDabstract;
      td_inv = $3; td_loc = floc $startpos $endpos } }
283

284 285
type_arg:
| labels(quote_lident) { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
286 287

typedefn:
288
| (* epsilon *)
289
    { false, Public, TDabstract, [] }
290
| equal_model visibility bar_list1(typecase) invariant*
291
    { $1, $2, TDalgebraic $3, $4 }
292
| equal_model visibility BAR bar_list1(typecase) invariant*
293
    { $1, $2, TDalgebraic $4, $5 }
294 295 296
| equal_model visibility LEFTBRC record_fields RIGHTBRC invariant*
    { $1, $2, TDrecord $4, $6 }
(* abstract/private is not allowed for alias type *)
297
| equal_model visibility primitive_type
298 299
    { if $2 <> Public then
        Loc.error ~loc:(floc $startpos($2) $endpos($2)) Error;
300
      $1, Public, TDalias $3, [] }
301 302

visibility:
303
| (* epsilon *) { Public }
304 305
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
306 307

equal_model:
308 309
| EQUAL         { false }
| MODEL         { true }
310

311 312 313
record_fields:
| record_field SEMICOLON?               { [$1] }
| record_field SEMICOLON record_fields  { $1 :: $3 }
314

315
field_modifiers:
316
| (* epsilon *) { false, false }
317 318 319 320 321
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }

322
record_field:
323 324 325
| field_modifiers labels(lident) cast
  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
      f_pty = $3; f_loc = floc $startpos $endpos } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
326 327

typecase:
328
| labels(uident) params { floc $startpos $endpos, $1, $2 }
329

330
(* Logic declarations *)
331

332
logic_decl_constant:
333 334 335
| labels(lident_rich) cast preceded(EQUAL,lexpr)?
  { { ld_ident = $1; ld_params = []; ld_type = Some $2;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
336

Andrei Paskevich's avatar
Andrei Paskevich committed
337
logic_decl_function:
338 339 340
| labels(lident_rich) params cast preceded(EQUAL,lexpr)?
  { { 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
341 342

logic_decl_predicate:
343 344 345
| labels(lident_rich) params preceded(EQUAL,lexpr)?
  { { ld_ident = $1; ld_params = $2; ld_type = None;
      ld_def = $3; ld_loc = floc $startpos $endpos } }
346

347 348 349 350
with_logic_decl:
| WITH labels(lident_rich) params cast? preceded(EQUAL,lexpr)?
  { { 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
351

352
(* Inductive declarations *)
353 354

inductive_decl:
355 356 357
| labels(lident_rich) params inddefn
  { { in_ident = $1; in_params = $2;
      in_def = $3; in_loc = floc $startpos $endpos } }
358

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
359
inddefn:
360 361
| (* epsilon *)                 { [] }
| EQUAL BAR? bar_list1(indcase) { $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
362 363

indcase:
364
| labels(ident) COLON lexpr { floc $startpos $endpos, $1, $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
365

366
(* Type expressions *)
367 368

primitive_type:
369
| primitive_type_arg                  { $1 }
370
| lqualid primitive_type_arg+         { PPTtyapp ($1, $2) }
371
| primitive_type ARROW primitive_type { PPTarrow ($1, $3) }
372 373

primitive_type_arg:
374 375 376 377 378 379 380 381
| lqualid                                       { PPTtyapp ($1, []) }
| quote_lident                                  { PPTtyvar ($1, false) }
| opaque_quote_lident                           { PPTtyvar ($1, true) }
| LEFTPAR comma_list2(primitive_type) RIGHTPAR  { PPTtuple $2 }
| LEFTPAR RIGHTPAR                              { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR               { PPTparen $2 }

(* Logic expressions *)
382

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
383
lexpr:
384 385 386 387 388 389
| mk_pp(lexpr_) { $1 }

lexpr_:
| lexpr_arg_
   { match $1 with (* break the infix relation chain *)
     | PPinfix (l,o,r) -> PPinnfix (l,o,r) | d -> d }
390
| lexpr ARROW lexpr
391
   { PPbinop ($1, PPimplies, $3) }
392
| lexpr LRARROW lexpr
393
   { PPbinop ($1, PPiff, $3) }
394
| lexpr OR lexpr
395
   { PPbinop ($1, PPor, $3) }
396
| lexpr BARBAR lexpr
397
   { PPbinop ($1, PPor_asym, $3) }
398
| lexpr AND lexpr
399
   { PPbinop ($1, PPand, $3) }
400
| lexpr AMPAMP lexpr
401
   { PPbinop ($1, PPand_asym, $3) }
402
| NOT lexpr
403 404 405
   { PPunop (PPnot, $2) }
| l = lexpr ; o = infix_op ; r = lexpr
   { PPinfix (l, o, r) }
406
| prefix_op lexpr %prec prec_prefix_op
407 408 409 410
   { PPidapp (Qident $1, [$2]) }
| lexpr_arg lexpr_arg_loc+ (* FIXME/TODO: "lexpr lexpr_arg" *)
   { let join f (e,a) = mk_pp (PPapply (f,a)) $startpos e in
     (List.fold_left join $1 $2).pp_desc }
411
| IF lexpr THEN lexpr ELSE lexpr
412 413 414
   { PPif ($2, $4, $6) }
| quant comma_list1(quant_vars) triggers DOT lexpr
   { PPquant ($1, List.concat $2, $3, $5) }
415
| label lexpr %prec prec_named
416
   { PPnamed ($1, $2) }
417
| LET pattern EQUAL lexpr IN lexpr
418
   { match $2.pat_desc with
419 420 421 422 423 424 425 426 427 428 429 430 431 432
     | PPpvar id -> PPlet (id, $4, $6)
     | PPpwild -> PPlet (id_anonymous $2.pat_loc, $4, $6)
     | PPptuple [] -> PPlet (id_anonymous $2.pat_loc,
          { $4 with pp_desc = PPcast ($4, PPTtuple []) }, $6)
     | _ -> PPmatch ($4, [$2, $6]) }
| MATCH lexpr WITH BAR? bar_list1(match_case) END
   { PPmatch ($2, $5) }
| MATCH comma_list2(lexpr) WITH BAR? bar_list1(match_case) END
   { PPmatch (mk_pp (PPtuple $2) $startpos($2) $endpos($2), $5) }
| lexpr cast
   { PPcast ($1, $2) }

lexpr_arg_loc:
| lexpr_arg { $endpos, $1 }
433

434
constant:
435 436
| INTEGER   { Number.ConstInt $1 }
| FLOAT     { Number.ConstReal $1 }
437

438
lexpr_arg:
439 440 441 442 443 444 445 446 447 448
| mk_pp(lexpr_arg_) { $1 }

lexpr_arg_:
| qualid                              { PPident $1 }
| constant                            { PPconst $1 }
| TRUE                                { PPtrue }
| FALSE                               { PPfalse }
| quote_uident                        { PPident (Qident $1) }
| o = oppref ; a = lexpr_arg          { PPidapp (Qident o, [a]) }
| lexpr_sub                           { $1 }
449 450

lexpr_dot:
451 452 453
| lqualid                             { PPident $1 }
| o = oppref ; a = mk_pp(lexpr_dot)   { PPidapp (Qident o, [a]) }
| lexpr_sub                           { $1 }
454 455

lexpr_sub:
456 457 458 459 460 461
| mk_pp(lexpr_dot) DOT lqualid_rich                   { PPidapp ($3,[$1]) }
| LEFTPAR lexpr RIGHTPAR                              { $2.pp_desc }
| LEFTPAR RIGHTPAR                                    { PPtuple [] }
| LEFTPAR comma_list2(lexpr) RIGHTPAR                 { PPtuple $2 }
| LEFTBRC field_list1(lexpr) RIGHTBRC                 { PPrecord $2 }
| LEFTBRC lexpr_arg WITH field_list1(lexpr) RIGHTBRC  { PPupdate ($2,$4) }
462
| lexpr_arg LEFTSQ lexpr RIGHTSQ
463 464
   { let id = mk_id (mixfix "[]") $startpos($2) $endpos($2) in
     PPidapp (Qident id, [$1;$3]) }
465
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
466 467
   { let id = mk_id (mixfix "[<-]") $startpos($2) $endpos($2) in
     PPidapp (Qident id, [$1;$3;$5]) }
468

Andrei Paskevich's avatar
Andrei Paskevich committed
469 470 471 472
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
473 474
| EPSILON { Loc.errorm ~loc:(floc $startpos $endpos)
    "epsilon terms are currently not supported in WhyML" }
Andrei Paskevich's avatar
Andrei Paskevich committed
475

476 477
match_case:
| pattern ARROW lexpr   { $1, $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
478

479 480
mk_pp(X):
| d = X   { mk_pp d $startpos $endpos }
481

482
(* Triggers *)
483

484 485 486
triggers:
| (* epsilon *)                      { [] }
| LEFTSQ bar_list1(trigger) RIGHTSQ  { $2 }
487

488 489
trigger:
| comma_list1(lexpr) { $1 }
490

491
(* Patterns *)
492

493 494
pattern:
| mk_pat(pattern_)  { $1 }
495

496 497 498
pattern_:
| pat_conj                      { $1 }
| mk_pat(pat_conj) BAR pattern  { PPpor ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
499

500 501 502
pat_conj:
| pat_uni                       { $1 }
| comma_list2(mk_pat(pat_uni))  { PPptuple $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
503

504 505 506 507
pat_uni:
| pat_arg_                          { $1 }
| uqualid pat_arg+                  { PPpapp ($1,$2) }
| mk_pat(pat_uni) AS labels(lident) { PPpas ($1,$3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
508

509 510
pat_arg:
| mk_pat(pat_arg_)  { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
511

512 513 514 515 516 517 518
pat_arg_:
| UNDERSCORE                            { PPpwild }
| labels(lident)                        { PPpvar $1 }
| uqualid                               { PPpapp ($1,[]) }
| LEFTPAR RIGHTPAR                      { PPptuple [] }
| LEFTPAR pattern_ RIGHTPAR             { $2 }
| LEFTBRC field_list1(pattern) RIGHTBRC { PPprec $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
519

520 521
mk_pat(X):
| X { mk_pat $1 $startpos $endpos }
522

523
(* Binders *)
524

525 526
(* [param] and [binder] below must have the same grammar
   and raise [Error] in the same cases. Interpretaion of
527 528
   single-standing untyped [Qident]'s is different: [param]
   treats them as type expressions, [binder], as parameter
529 530 531 532 533 534 535
   names, whose type must be inferred. *)

params:
| param*  { List.concat $1 }

binders:
| binder+ { List.concat $1 }
536 537 538

param:
| anon_binder
539
   { error_param (floc $startpos $endpos) }
540
| primitive_type_arg
541
   { [floc $startpos $endpos, None, false, $1] }
542
| LEFTPAR GHOST primitive_type RIGHTPAR
543 544
   { [floc $startpos $endpos, None, true, $3] }
| primitive_type_arg label label*
545
   { match $1 with
546 547 548
      | PPTtyapp (Qident _, []) ->
             error_param (floc $startpos $endpos)
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
549
| LEFTPAR binder_vars_rest RIGHTPAR
550 551
   { match $2 with [l,_] -> error_param l
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
552
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
553 554 555 556 557 558
   { match $3 with [l,_] -> error_param l
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
   { List.map (fun (l,i) -> l, i, false, $3) $2 }
| LEFTPAR GHOST binder_vars cast RIGHTPAR
   { List.map (fun (l,i) -> l, i, true, $4) $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
559

560 561
binder:
| anon_binder
562
   { error_param (floc $startpos $endpos) }
563 564 565 566
| primitive_type_arg
   { match $1 with
      | PPTtyapp (Qident id, [])
      | PPTparen (PPTtyapp (Qident id, [])) ->
567 568
             [floc $startpos $endpos, Some id, false, None]
      | _ -> [floc $startpos $endpos, None, false, Some $1] }
569 570 571
| LEFTPAR GHOST primitive_type RIGHTPAR
   { match $3 with
      | PPTtyapp (Qident id, []) ->
572 573 574
             [floc $startpos $endpos, Some id, true, None]
      | _ -> [floc $startpos $endpos, None, true, Some $3] }
| primitive_type_arg label label*
575 576
   { match $1 with
      | PPTtyapp (Qident id, []) ->
577 578 579
             let id = add_lab id ($2::$3) in
             [floc $startpos $endpos, Some id, false, None]
      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
580 581
| LEFTPAR binder_vars_rest RIGHTPAR
   { match $2 with [l,i] -> [l, i, false, None]
582
      | _ -> error_loc (floc $startpos($3) $endpos($3)) }
583 584
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
   { match $3 with [l,i] -> [l, i, true, None]
585 586 587 588 589
      | _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
   { List.map (fun (l,i) -> l, i, false, Some $3) $2 }
| LEFTPAR GHOST binder_vars cast RIGHTPAR
   { List.map (fun (l,i) -> l, i, true, Some $4) $3 }
590

591 592 593
binder_vars:
| binder_vars_head  { List.rev $1 }
| binder_vars_rest  { $1 }
594

595
binder_vars_rest:
596
| binder_vars_head label label* quant_var*
597 598
   { List.rev_append (match $1 with
      | (l, Some id) :: bl ->
599 600
          let l3 = floc $startpos($3) $endpos($3) in
          (Loc.join l l3, Some (add_lab id ($2::$3))) :: bl
601
      | _ -> assert false) $4 }
602
| binder_vars_head anon_binder quant_var*
603
   { List.rev_append $1 ($2 :: $3) }
604
| anon_binder quant_var*
605
   { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
606

607 608 609 610 611
binder_vars_head:
| primitive_type {
    let of_id id = id.id_loc, Some id in
    let push acc = function
      | PPTtyapp (Qident id, []) -> of_id id :: acc
612
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
613 614
    match $1 with
      | PPTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
615
      | _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
616 617

quant_vars:
618
| quant_var+ cast? {
619 620 621
    List.map (function
      | loc, None -> Loc.errorm ~loc "anonymous binders are not allowed here"
      | _, Some i -> i, $2) $1 }
622

623 624 625
quant_var:
| labels(lident)  { floc $startpos $endpos, Some $1 }
| anon_binder     { $1 }
626 627

anon_binder:
628 629 630 631
| UNDERSCORE      { floc $startpos $endpos, None }

labels(X):
| X label*  { add_lab $1 $2 }
632

633
(* Idents *)
634 635 636 637

ident:
| uident { $1 }
| lident { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
638

639
uident:
640
| UIDENT          { mk_id $1 $startpos $endpos }
641 642

lident:
643 644
| LIDENT          { mk_id $1 $startpos $endpos }
| lident_keyword  { mk_id $1 $startpos $endpos }
645 646 647 648

lident_keyword:
| MODEL           { "model" }

649
quote_uident:
650
| QUOTE_UIDENT    { mk_id ("'" ^ $1) $startpos $endpos }
651 652

quote_lident:
653
| QUOTE_LIDENT    { mk_id $1 $startpos $endpos }
654 655

opaque_quote_lident:
656
| OPAQUE_QUOTE_LIDENT { mk_id $1 $startpos $endpos }
657

658
(* Idents + symbolic operations' names *)
659

660 661 662
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
663

664
lident_rich:
665 666 667 668
| lident        { $1 }
| lident_op_id  { $1 }

lident_op_id:
669 670
| LEFTPAR lident_op RIGHTPAR  { mk_id $2 $startpos $endpos }
| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") $startpos $endpos }
671

672
lident_op:
673 674 675 676 677 678 679 680 681
| op_symbol               { infix $1 }
| op_symbol UNDERSCORE    { prefix $1 }
| EQUAL                   { infix "=" }
| OPPREF                  { prefix $1 }
| LEFTSQ RIGHTSQ          { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ   { mixfix "[<-]" }
| LEFTSQ RIGHTSQ LARROW   { mixfix "[]<-" }

op_symbol:
682 683 684 685 686
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }

687 688 689 690 691 692 693 694 695 696 697 698 699 700 701
%inline oppref:
| o = OPPREF { mk_id (prefix o)  $startpos $endpos }

prefix_op:
| op_symbol { mk_id (prefix $1)  $startpos $endpos }

%inline infix_op:
| o = OP1   { mk_id (infix o)    $startpos $endpos }
| o = OP2   { mk_id (infix o)    $startpos $endpos }
| o = OP3   { mk_id (infix o)    $startpos $endpos }
| o = OP4   { mk_id (infix o)    $startpos $endpos }
| EQUAL     { mk_id (infix "=")  $startpos $endpos }
| LTGT      { mk_id (infix "<>") $startpos $endpos }

(* Qualified idents *)
702

703 704 705
qualid:
| ident_rich              { Qident $1 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }
706

707 708 709
lqualid_rich:
| lident_rich             { Qident $1 }
| uqualid DOT lident_rich { Qdot ($1, $3) }
710 711

lqualid:
712 713
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
714

715 716 717
uqualid:
| uident              { Qident $1 }
| uqualid DOT uident  { Qdot ($1, $3) }
718

719
(* Theory/Module names *)
720

721 722 723 724
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }

725
any_qualid:
726 727 728 729 730
| sident                { Qident $1 }
| any_qualid DOT sident { Qdot ($1, $3) }

sident:
| ident   { $1 }
731
| STRING  { mk_id $1 $startpos $endpos }
732

733
label:
Andrei Paskevich's avatar
Andrei Paskevich committed
734
| STRING    { Lstr (Ident.create_label $1) }
735
| POSITION  { Lpos $1 }
736

737
(****************************************************************************)
738 739

program_file:
740
| theory_or_module* EOF { Incremental.close_file () }
741

742 743 744
theory_or_module:
| theory_head theory_decl* END  { Incremental.close_theory () }
| module_head module_decl* END  { Incremental.close_module () }
745

746
module_head:
747
| MODULE labels(uident)  { Incremental.open_module $2 }
748

749 750 751 752 753 754
module_decl:
| decl            { Incremental.new_decl  (floc $startpos $endpos) $1 }
| pdecl           { Incremental.new_pdecl (floc $startpos $endpos) $1 }
| use_clone       { Incremental.use_clone (floc $startpos $endpos) $1 }
| namespace_head module_decl* END
    { Incremental.close_namespace (floc $startpos($1) $endpos($1)) $1 }
755

756
pdecl:
757 758 759 760 761 762 763 764
| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
| LET REC with_list1(rec_defn)                      { Drec $3 }
| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
| EXCEPTION labels(uident)                          { Dexn ($2, PPTtuple []) }
| EXCEPTION labels(uident) primitive_type           { Dexn ($2, $3) }

(*
765 766 767
type_c:
| spec arrow_type_v { $2, $1 }
| simple_type_c     { $1 }
768
*)
769 770

type_v:
771 772
| arrow_type_v  { $1 }
| cast          { Tpure $1 }
773 774

arrow_type_v:
775
| param params tail_type_c  { Tarrow ($1 @ $2, $3) }
776 777 778 779 780 781 782

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

simple_type_c:
| primitive_type spec { Tpure $1, $2 }
783

784
rec_defn:
785 786
| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
   { $2, $1, ($3, $4, $8, spec_union $5 $7) }
787

788
fun_defn:
789
| binders cast? spec EQUAL spec seq_expr { ($1, $2, $6, spec_union $3 $5) }
790

791
fun_expr:
792 793 794
| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }

(* Expressions *)
795 796

expr:
797 798 799 800 801 802
| mk_expr(expr_)  { $1 }

expr_:
| expr_arg_
   { match $1 with (* break the infix relation chain *)
     | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d }
803
| expr LARROW expr
804
   { match $1.expr_desc with
805
     | Eidapp (q, [e1]) -> Eassign (e1, q, $3)
806
     | Eidapp (Qident id, [e1;e2]) when id.id = mixfix "[]" ->
807 808 809 810
         Eidapp (Qident {id with id = mixfix "[]<-"}, [e1;e2;$3])
     | _ -> raise Error }
| l = expr ; o = infix_op ; r = expr
   { Einfix (l,o,r) }
811
| NOT expr %prec prec_prefix_op
812
   { Enot $2 }
813
| prefix_op expr %prec prec_prefix_op
814 815 816 817
   { Eidapp (Qident $1, [$2]) }
| expr_arg expr_arg_loc+ (* FIXME/TODO: "expr expr_arg" *)
   { let join f (e,a) = mk_expr (Eapply (f,a)) $startpos e in
     (List.fold_left join $1 $2).expr_desc }
818
| IF seq_expr THEN expr ELSE expr
819
   { Eif ($2, $4, $6) }
820
| IF seq_expr THEN expr %prec prec_no_else
821 822
   { Eif ($2, $4, mk_expr (Etuple []) $startpos $endpos) }
(*
823
| expr SEMICOLON expr
824 825
   { Esequence ($1, $3) }
*)
826
| assertion_kind LEFTBRC lexpr RIGHTBRC
827
   { Eassert ($1, $3) }
828
| expr AMPAMP expr
829
   { Elazy (LazyAnd, $1, $3) }
830
| expr BARBAR expr
831
   { Elazy (LazyOr, $1, $3) }
832
| LET pattern EQUAL seq_expr IN seq_expr
833
   { match $2.pat_desc with
834 835 836 837 838
     | PPpvar id -> Elet (id, Gnone, $4, $6)
     | PPpwild -> Elet (id_anonymous $2.pat_loc, Gnone, $4, $6)
     | PPptuple [] -> Elet (id_anonymous $2.pat_loc, Gnone,
          { $4 with expr_desc = Ecast ($4, PPTtuple []) }, $6)
     | _ -> Ematch ($4, [$2, $6]) }
839
| LET GHOST pat_arg EQUAL seq_expr IN seq_expr
840
   { match $3.pat_desc with
841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863
     | PPpvar id -> Elet (id, Gghost, $5, $7)
     | PPpwild -> Elet (id_anonymous $3.pat_loc, Gghost, $5, $7)
     | PPptuple [] -> Elet (id_anonymous $3.pat_loc, Gghost,
          { $5 with expr_desc = Ecast ($5, PPTtuple []) }, $7)
     | _ -> Ematch ({ $5 with expr_desc = Eghost $5 }, [$3, $7]) }
| LET labels(lident) fun_defn IN seq_expr
   { Efun ($2, Gnone, $3, $5) }
| LET labels(lident_op_id) fun_defn IN seq_expr
   { Efun ($2, Gnone, $3, $5) }
| LET GHOST labels(lident) fun_defn IN seq_expr
   { Efun ($3, Gghost, $4, $6) }
| LET GHOST labels(lident_op_id) fun_defn IN seq_expr
   { Efun ($3, Gghost, $4, $6) }
| LET labels(lident_op_id) EQUAL seq_expr IN seq_expr
   { Elet ($2, Gnone, $4, $6) }
| LET GHOST labels(lident_op_id) EQUAL seq_expr IN seq_expr
   { Elet ($3, Gghost, $5, $7) }
| LET LEMMA labels(lident_rich) EQUAL seq_expr IN seq_expr
   { Elet ($3, Glemma, $5, $7) }
| LET LEMMA labels(lident_rich) fun_defn IN seq_expr
   { Efun ($3, Glemma, $4, $6) }
| LET REC with_list1(rec_defn) IN seq_expr
   { Erec ($3, $5) }
864
| fun_expr
865 866 867 868 869 870 871 872 873
   { Elam $1 }
| VAL top_ghost labels(lident_rich) val_expr IN seq_expr
   { Elet ($3, $2, $4, $6) }
| MATCH seq_expr WITH BAR? bar_list1(program_match_case) END
   { Ematch ($2, $5) }
| MATCH comma_list2(expr) WITH BAR? bar_list1(program_match_case) END
   { Ematch (mk_expr (Etuple $2) $startpos($2) $endpos($2), $5) }
| quote_uident COLON seq_expr
   { Emark ($1, $3) }
874
| LOOP loop_annotation seq_expr END
875
   { Eloop ($2, $3) }
876
| WHILE seq_expr DO loop_annotation seq_expr DONE
877
   { Ewhile ($2, $4, $5) }
878
| FOR lident EQUAL seq_expr for_direction seq_expr
879 880
  DO invariant* seq_expr DONE
   { Efor ($2, $4, $5, $6, $8, $9) }
881
| ABSURD