parser.mly 32.3 KB
Newer Older
1 2
/**************************************************************************/
/*                                                                        */
3
/*  Copyright (C) 2010-2011                                               */
4 5 6
/*    François Bobot                                                      */
/*    Jean-Christophe Filliâtre                                           */
/*    Claude Marché                                                       */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
7
/*    Andrei Paskevich                                                    */
8 9 10 11 12 13 14 15 16 17 18
/*                                                                        */
/*  This software is free software; you can redistribute it and/or        */
/*  modify it under the terms of the GNU Library General Public           */
/*  License version 2.1, with the special exception on linking            */
/*  described in file LICENSE.                                            */
/*                                                                        */
/*  This software is distributed in the hope that it will be useful,      */
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  */
/*                                                                        */
/**************************************************************************/
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
19 20

%{
21
module Incremental = struct
22 23 24
  let env_ref  = ref []
  let lenv_ref = ref []
  let uc_ref   = ref []
25
  let path_ref = ref []
26 27 28 29 30 31 32 33 34

  let ref_get  ref = List.hd !ref
  let ref_tail ref = List.tl !ref
  let ref_drop ref = ref := ref_tail ref
  let ref_pop  ref = let v = ref_get ref in ref_drop ref; v

  let ref_push ref v = ref := v :: !ref
  let ref_set  ref v = ref := v :: ref_tail ref

35 36 37 38
  let open_logic_file env path =
    ref_push env_ref env;
    ref_push path_ref path;
    ref_push lenv_ref Util.Mstr.empty
39 40

  let close_logic_file () =
41 42 43
    ref_drop path_ref;
    ref_drop env_ref;
    ref_pop lenv_ref
44 45

  let open_theory id =
46 47
    let path = ref_get path_ref in
    ref_push uc_ref (Theory.create_theory ~path (Denv.create_user_id id))
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62

  let close_theory loc =
    let uc = ref_pop uc_ref in
    ref_set lenv_ref (Typing.close_theory loc (ref_get lenv_ref) uc)

  let open_namespace () =
    ref_set uc_ref (Theory.open_namespace (ref_get uc_ref))

  let close_namespace loc import name =
    ref_set uc_ref (Typing.close_namespace loc import name (ref_get uc_ref))

  let new_decl d =
    let env = ref_get env_ref in let lenv = ref_get lenv_ref in
    ref_set uc_ref (Typing.add_decl env lenv (ref_get uc_ref) d)
end
63

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
64 65 66 67
  open Ptree
  open Parsing

  let loc () = (symbol_start_pos (), symbol_end_pos ())
68 69
  let floc () = Loc.extract (loc ())

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
70
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
71
  let floc_i i = Loc.extract (loc_i i)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
72
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
73
  let floc_ij i j = Loc.extract (loc_ij i j)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
74 75

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
76 77
  let mk_pp d = mk_ppl (floc ()) d
  let mk_pp_i i d = mk_ppl (floc_i i) d
78

79
  let mk_pat p = { pat_loc = floc (); pat_desc = p }
Andrei Paskevich's avatar
Andrei Paskevich committed
80

81
  let infix_ppl loc a i b = mk_ppl loc (PPbinop (a, i, b))
82
  let infix_pp a i b = infix_ppl (floc ()) a i b
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83

84
  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
85
  let prefix_pp p a = prefix_ppl (floc ()) p a
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86

87
  let infix  s = "infix "  ^ s
88
  let prefix s = "prefix " ^ s
89
  let mixfix s = "mixfix " ^ s
90

91 92
  let quote id = { id with id = "'" ^ id.id }

93 94 95 96
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

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

97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
  let mk_l_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
    mk_pp (PPapp (Qident id, [e1]))

  let mk_l_infix e1 op e2 =
    let id = mk_id (infix op) (floc_i 2) in
    mk_pp (PPinfix (e1, id, e2))

  let mk_l_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
    mk_pp (PPapp (Qident id, [e1;e2]))

  let mk_l_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
    mk_pp (PPapp (Qident id, [e1;e2;e3]))

113 114 115 116 117
  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
      | _ -> raise exn
    )
118

119 120
  let mk_expr d = { expr_loc = floc (); expr_desc = d }
  let mk_expr_i i d = { expr_loc = floc_i i; expr_desc = d }
121 122 123 124 125 126 127

  let cast_body c ((p,e,q) as t) = match c with
    | None -> t
    | Some pt -> p, { e with expr_desc = Ecast (e, pt) }, q

  let rec mk_apply f = function
    | [] ->
128
        assert false
129
    | [a] ->
130
        Eapply (f, a)
131
    | a :: l ->
132 133
        let loc = Loc.join f.expr_loc a.expr_loc in
        mk_apply { expr_loc = loc; expr_desc = Eapply (f, a) } l
134 135 136 137 138 139 140

  let mk_apply_id id =
    let e =
      { expr_desc = Eident (Qident id); expr_loc = id.id_loc }
    in
    mk_apply e

141 142
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
143 144
    mk_expr (mk_apply_id id [e1; e2])

145 146
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
147 148
    mk_expr (mk_apply_id id [e1; e2; e3])

149
  let mk_infix e1 op e2 =
150
    let id = mk_id (infix op) (floc_i 2) in
151 152 153
    mk_expr (mk_apply_id id [e1; e2])

  let mk_prefix op e1 =
154
    let id = mk_id (prefix op) (floc_i 1) in
155 156
    mk_expr (mk_apply_id id [e1])

157 158
  let exit_exn () = Qident (mk_id "%Exit" (floc ()))
  let id_anonymous () = mk_id "_" (floc ())
159
  let ty_unit () = Tpure (PPTtuple [])
160

161
  let id_lt_nat () = Qident (mk_id "lt_nat" (floc ()))
162 163 164 165 166 167 168 169

  let empty_effect = { pe_reads = []; pe_writes = []; pe_raises = [] }

  let type_c p ty ef q =
    { pc_result_type = ty;
      pc_effect      = ef;
      pc_pre         = p;
      pc_post        = q; }
170

171
  let add_init_mark e =
172
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
173
    { e with expr_desc = Emark (init, e) }
174

175 176 177 178 179 180 181 182 183
  let small_integer i =
    try
      match i with
      | Term.IConstDecimal s -> int_of_string s
      | Term.IConstHexa    s -> int_of_string ("0x"^s)
      | Term.IConstOctal   s -> int_of_string ("0o"^s)
      | Term.IConstBinary  s -> int_of_string ("0b"^s)
    with Failure _ -> raise Parsing.Parse_error

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
184 185
%}

186
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
187

188
%token <string> LIDENT UIDENT
189
%token <Ptree.integer_constant> INTEGER
190
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
191 192
%token <Ptree.real_constant> FLOAT
%token <string> STRING
193
%token <Loc.position> POSITION
194 195 196

/* keywords */

Andrei Paskevich's avatar
Andrei Paskevich committed
197 198 199 200
%token AS AXIOM CLONE
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
201
%token THEN THEORY TRUE TYPE USE WITH
202

203 204
/* program keywords */

205 206
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO
%token EXCEPTION FOR
207
%token FUN INVARIANT LOOP MODEL MODULE MUTABLE RAISE
208
%token RAISES READS REC TO TRY VAL VARIANT WHILE WRITES
209

210 211
/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
212
%token AND ARROW
213
%token BAR
214
%token COLON COMMA
215
%token DOT EQUAL FUNC LAMBDA LTGT
216
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTREC LEFTSQ
217
%token LARROW LRARROW
Andrei Paskevich's avatar
Andrei Paskevich committed
218
%token OR PRED QUOTE
219
%token RIGHTPAR RIGHTREC RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
220
%token UNDERSCORE
221 222 223

%token EOF

224 225
/* program symbols */

226
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
227

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
228 229
/* Precedences */

230
%nonassoc prec_mark
231 232 233 234 235 236 237 238 239 240
%nonassoc prec_post
%nonassoc BAR

%nonassoc prec_triple
%nonassoc prec_simple

%nonassoc IN
%right SEMICOLON
%nonassoc prec_no_else
%nonassoc DOT ELSE
241
%nonassoc prec_named
242
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
243

Andrei Paskevich's avatar
Andrei Paskevich committed
244
%right ARROW LRARROW
245 246
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
247
%nonassoc NOT
248
%left EQUAL LTGT OP1
249 250
%nonassoc LARROW
%nonassoc RIGHTSQ    /* stronger than <- for e1[e2 <- e3] */
251
%left OP2
252
%left OP3
253
%left OP4
254
%nonassoc prec_prefix_op
255
%left prec_app
256 257
%nonassoc LEFTSQ
%nonassoc OPPREF
258

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
259 260
/* Entry points */

261
%type <Env.env -> string list -> unit> pre_logic_file
262
%start pre_logic_file
263
%type <Theory.theory Util.Mstr.t> logic_file
264
%start logic_file
265 266
%type <Ptree.program_file> program_file
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
267 268
%%

269 270 271 272
pre_logic_file:
| /* epsilon */  { Incremental.open_logic_file }
;

273
logic_file:
274
| list0_theory EOF  { Incremental.close_logic_file () }
275 276 277
;

/* File, theory, namespace */
278

279 280 281
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
282 283
;

284
theory_head:
285
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
286 287
;

288
theory:
289
| theory_head list0_decl END  { Incremental.close_theory (floc_i 1) }
290 291
;

292
list0_decl:
293 294 295 296 297 298
| /* epsilon */        { () }
| new_decl list0_decl  { () }
;

new_decl:
| decl
299
   { Incremental.new_decl $1 }
300
| namespace_head namespace_import namespace_name list0_decl END
301
   { Incremental.close_namespace (floc_i 3) $2 $3 }
302 303
;

304
namespace_head:
305
| NAMESPACE  { Incremental.open_namespace () }
306 307 308 309 310 311 312 313 314 315 316 317 318 319
;

namespace_import:
| /* epsilon */  { false }
| IMPORT         { true }
;

namespace_name:
| uident      { Some $1 }
| UNDERSCORE  { None }
;

/* Declaration */

320
decl:
321 322
| TYPE list1_type_decl
    { TypeDecl $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
323 324 325
| FUNCTION list1_logic_decl_function
    { LogicDecl $2 }
| PREDICATE list1_logic_decl_predicate
326 327 328
    { LogicDecl $2 }
| INDUCTIVE list1_inductive_decl
    { IndDecl $2 }
329
| AXIOM ident labels COLON lexpr
330
    { PropDecl (floc (), Kaxiom, add_lab $2 $3, $5) }
331
| LEMMA ident labels COLON lexpr
332
    { PropDecl (floc (), Klemma, add_lab $2 $3, $5) }
333
| GOAL ident labels COLON lexpr
334
    { PropDecl (floc (), Kgoal, add_lab $2 $3, $5) }
335
| USE use
336
    { UseClone (floc (), $2, None) }
337
| CLONE use clone_subst
338
    { UseClone (floc (), $2, Some $3) }
339
| META sident list1_meta_arg_sep_comma
340
    { Meta (floc (), $2, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
341 342
;

343 344 345 346 347 348 349 350 351
/* Use and clone */

use:
| imp_exp tqualid
    { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
| imp_exp tqualid AS uident
    { { use_theory = $2; use_as = Some (Some $4); use_imp_exp = $1 } }
| imp_exp tqualid AS UNDERSCORE
    { { use_theory = $2; use_as = Some None; use_imp_exp = $1 } }
352 353
;

354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370
imp_exp:
| IMPORT        { Import }
| EXPORT        { Export }
| /* epsilon */ { Nothing }
;

clone_subst:
| /* epsilon */          { [] }
| WITH list1_comma_subst { $2 }
;

list1_comma_subst:
| subst                         { [$1] }
| subst COMMA list1_comma_subst { $1 :: $3 }
;

subst:
Andrei Paskevich's avatar
Andrei Paskevich committed
371 372
| NAMESPACE ns     EQUAL ns     { CSns   ($2, $4) }
| TYPE      qualid EQUAL qualid { CStsym ($2, $4) }
373 374
| FUNCTION  qualid EQUAL qualid { CSfsym ($2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym ($2, $4) }
Andrei Paskevich's avatar
Andrei Paskevich committed
375 376
| LEMMA     qualid              { CSlemma $2 }
| GOAL      qualid              { CSgoal  $2 }
377 378
;

379 380 381 382 383
ns:
| uqualid { Some $1 }
| DOT     { None }
;

384 385 386 387 388 389 390 391
/* Meta args */

list1_meta_arg_sep_comma:
| meta_arg                                { [$1] }
| meta_arg COMMA list1_meta_arg_sep_comma { $1 :: $3 }
;

meta_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
392
| TYPE      qualid { PMAts  $2 }
393 394
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
395 396
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
397
| INTEGER          { PMAint (small_integer $1) }
398 399
;

400 401 402
/* Type declarations */

list1_type_decl:
403 404
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
405 406 407
;

type_decl:
408
| lident labels type_args typedefn
409 410 411
  { let model, def = $4 in
    { td_loc = floc (); td_ident = add_lab $1 $2;
      td_params = $3; td_model = model; td_def = def } }
412 413
;

414
type_args:
415 416
| /* epsilon */             { [] }
| type_var labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
417 418 419
;

typedefn:
420 421 422 423 424 425 426 427 428 429
| /* epsilon */                 { false, TDabstract }
| equal_model primitive_type    { $1, TDalias $2 }
| equal_model typecases         { $1, TDalgebraic $2 }
| equal_model BAR typecases     { $1, TDalgebraic $3 }
| equal_model record_type       { $1, TDrecord $2 }
;

equal_model:
| EQUAL { false }
| MODEL { true }
430 431 432
;

record_type:
Andrei Paskevich's avatar
Andrei Paskevich committed
433
| LEFTREC list1_record_field opt_semicolon RIGHTREC { List.rev $2 }
434 435 436 437
;

list1_record_field:
| record_field                              { [$1] }
438
| list1_record_field SEMICOLON record_field { $3 :: $1 }
439 440 441
;

record_field:
442
| opt_mutable lident labels COLON primitive_type
443
   { floc (), $1, add_lab $2 $3, $5 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
444 445 446 447 448 449 450 451
;

typecases:
| typecase                { [$1] }
| typecase BAR typecases  { $1::$3 }
;

typecase:
452
| uident labels params   { (floc (), add_lab $1 $2, $3) }
453 454 455 456
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
457 458 459 460 461 462 463 464 465 466
list1_logic_decl_function:
| logic_decl_function                        { [$1] }
| logic_decl_function WITH list1_logic_decl  { $1 :: $3 }
;

list1_logic_decl_predicate:
| logic_decl_predicate                        { [$1] }
| logic_decl_predicate WITH list1_logic_decl  { $1 :: $3 }
;

467
list1_logic_decl:
468 469
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
470 471
;

Andrei Paskevich's avatar
Andrei Paskevich committed
472 473 474 475 476 477 478 479 480 481 482 483
logic_decl_function:
| lident_rich labels params COLON primitive_type logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;

logic_decl_predicate:
| lident_rich labels params logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = None; ld_def = $4 } }
;

484
logic_decl:
485
| lident_rich labels params logic_type_option logic_def_option
486
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
487
      ld_params = $3; ld_type = $4; ld_def = $5 } }
488 489 490 491 492 493 494 495 496 497
;

logic_type_option:
| /* epsilon */        { None }
| COLON primitive_type { Some $2 }
;

logic_def_option:
| /* epsilon */ { None }
| EQUAL lexpr   { Some $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
498 499
;

500 501 502
/* Inductive declarations */

list1_inductive_decl:
503 504
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
505 506 507
;

inductive_decl:
508
| lident_rich labels params inddefn
509
  { { in_loc = floc (); in_ident = add_lab $1 $2;
510
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
511
;
512

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
513 514 515 516 517 518 519 520 521 522 523
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

indcases:
| indcase               { [$1] }
| indcase BAR indcases  { $1::$3 }
;

indcase:
524
| ident labels COLON lexpr { (floc (), add_lab $1 $2, $4) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
525 526
;

527 528 529 530 531 532 533 534
/* Type expressions */

primitive_type:
| primitive_type_arg           { $1 }
| lqualid primitive_type_args  { PPTtyapp ($2, $1) }
;

primitive_type_non_lident:
535 536
| primitive_type_arg_non_lident           { $1 }
| uqualid DOT lident primitive_type_args  { PPTtyapp ($4, Qdot ($1, $3)) }
537 538 539 540 541 542 543 544
;

primitive_type_args:
| primitive_type_arg                      { [$1] }
| primitive_type_arg primitive_type_args  { $1 :: $2 }
;

primitive_type_arg:
545
| lident                         { PPTtyapp ([], Qident $1) }
546 547 548 549
| primitive_type_arg_non_lident  { $1 }
;

primitive_type_arg_non_lident:
550 551
| uqualid DOT lident
   { PPTtyapp ([], Qdot ($1, $3)) }
552 553 554 555
| type_var
   { PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
556 557 558 559 560 561
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
562 563 564 565 566
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

567
type_var:
568
| QUOTE lident { $2 }
569 570
;

571 572
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
573
lexpr:
574
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
575
   { infix_pp $1 PPimplies $3 }
576
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
577
   { infix_pp $1 PPiff $3 }
578
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
579
   { infix_pp $1 PPor $3 }
580
| lexpr BARBAR lexpr
581
   { mk_pp (PPnamed (Lstr Term.asym_label, infix_pp $1 PPor $3)) }
582
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
583
   { infix_pp $1 PPand $3 }
584
| lexpr AMPAMP lexpr
585
   { mk_pp (PPnamed (Lstr Term.asym_label, infix_pp $1 PPand $3)) }
586
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
587
   { prefix_pp PPnot $2 }
588
| lexpr EQUAL lexpr
589
   { mk_l_infix $1 "=" $3 }
590
| lexpr LTGT lexpr
591
   { prefix_pp PPnot (mk_l_infix $1 "=" $3) }
592
| lexpr OP1 lexpr
593
   { mk_l_infix $1 $2 $3 }
594
| lexpr OP2 lexpr
595
   { mk_l_infix $1 $2 $3 }
596
| lexpr OP3 lexpr
597
   { mk_l_infix $1 $2 $3 }
598
| lexpr OP4 lexpr
599
   { mk_l_infix $1 $2 $3 }
600
| prefix_op lexpr %prec prec_prefix_op
601
   { mk_l_prefix $1 $2 }
602 603
| qualid list1_lexpr_arg
   { mk_pp (PPapp ($1, $2)) }
604
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
605
   { mk_pp (PPif ($2, $4, $6)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
606 607
| quant list1_param_var_sep_comma triggers DOT lexpr
   { mk_pp (PPquant ($1, $2, $3, $5)) }
608 609
| label lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
610
| LET pattern EQUAL lexpr IN lexpr
611 612
   { match $2.pat_desc with
       | PPpvar id -> mk_pp (PPlet (id, $4, $6))
Andrei Paskevich's avatar
Andrei Paskevich committed
613 614
       | _ -> mk_pp (PPmatch ($4, [$2, $6])) }
| MATCH lexpr WITH bar_ match_cases END
615
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
616 617
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
   { mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
618 619
| EPSILON lident labels COLON primitive_type DOT lexpr
   { mk_pp (PPeps (add_lab $2 $3, $5, $7)) }
620
| lexpr COLON primitive_type
621
   { mk_pp (PPcast ($1, $3)) }
622
| lexpr_arg
623 624 625
   { $1 }
;

626 627 628 629 630 631 632 633 634
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

field_value:
| lqualid EQUAL lexpr { $1, $3 }
;

635 636 637
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
638
;
639

640
constant:
641 642
| INTEGER   { Term.ConstInt $1 }
| FLOAT     { Term.ConstReal $1 }
643 644
;

645
lexpr_arg:
646 647 648 649 650 651
| qualid            { mk_pp (PPvar $1) }
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
652
| QUOTE uident      { mk_pp (PPvar (Qident (quote $2))) }
653 654 655
;

lexpr_dot:
656 657 658
| lqualid_copy      { mk_pp (PPvar $1) }
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
659 660 661
;

lexpr_sub:
662
| lexpr_dot DOT lqualid_rich
663
   { mk_pp (PPapp ($3, [$1])) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
664 665
| LEFTPAR lexpr RIGHTPAR
   { $2 }
666 667 668 669
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
670 671
| LEFTREC list1_field_value opt_semicolon RIGHTREC
   { mk_pp (PPrecord (List.rev $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
672 673
| LEFTREC lexpr_arg WITH list1_field_value opt_semicolon RIGHTREC
   { mk_pp (PPupdate ($2, List.rev $4)) }
674
| lexpr_arg LEFTSQ lexpr RIGHTSQ
675
   { mk_l_mixfix2 "[]" $1 $3 }
676
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
677
   { mk_l_mixfix3 "[<-]" $1 $3 $5 }
Andrei Paskevich's avatar
Andrei Paskevich committed
678
;
679

Andrei Paskevich's avatar
Andrei Paskevich committed
680 681 682 683
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
684 685
| FUNC    { PPfunc }
| PRED    { PPpred }
Andrei Paskevich's avatar
Andrei Paskevich committed
686 687
;

688
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
689

690 691 692 693
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
694

695 696 697 698 699 700 701 702 703 704 705 706 707 708 709
list1_trigger_sep_bar:
| trigger                           { [$1] }
| trigger BAR list1_trigger_sep_bar { $1 :: $3 }
;

trigger:
| list1_lexpr_sep_comma { $1 }
;

list1_lexpr_sep_comma:
| lexpr                             { [$1] }
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

/* Match expressions */
710

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
711 712 713 714 715 716
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
717
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
718 719 720
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
721 722 723 724 725 726 727 728 729 730 731 732 733 734 735
| pat_conj              { $1 }
| pat_conj BAR pattern  { mk_pat (PPpor ($1, $3)) }
;

pat_conj:
| pat_uni                      { $1 }
| pat_uni COMMA list1_pat_uni  { mk_pat (PPptuple ($1::$3)) }
;

list1_pat_uni:
| pat_uni                      { [$1] }
| pat_uni COMMA list1_pat_uni  { $1::$3 }
;

pat_uni:
736 737 738
| pat_arg                   { $1 }
| uqualid list1_pat_arg     { mk_pat (PPpapp ($1, $2)) }
| pat_uni AS lident labels  { mk_pat (PPpas ($1, add_lab $3 $4)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
739
;
740

741
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
742 743 744
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
745

746
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
747
| UNDERSCORE                { mk_pat (PPpwild) }
748
| lident labels             { mk_pat (PPpvar (add_lab $1 $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
749 750 751
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
752 753 754 755 756 757 758 759 760 761
| LEFTREC pfields RIGHTREC  { mk_pat (PPprec $2) }
;

pfields:
| pat_field opt_semicolon       { [$1] }
| pat_field SEMICOLON pfields   { $1::$3 }
;

pat_field:
| lqualid EQUAL pattern   { ($1, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
762 763
;

764
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
765

766 767 768
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
769 770
;

771 772 773 774 775 776 777 778 779 780 781 782 783
param:
| LEFTPAR param_var RIGHTPAR
   { $2 }
| LEFTPAR param_type RIGHTPAR
   { [None, $2] }
| LEFTPAR param_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { [None, PPTtuple ($2::$4)] }
| LEFTPAR RIGHTPAR
   { [None, PPTtuple []] }
| type_var
   { [None, PPTtyvar $1] }
| lqualid
   { [None, PPTtyapp ([], $1)] }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
784 785
;

786 787 788 789 790 791 792 793
param_type:
| lident param_type_cont
   { PPTtyapp ($2, Qident $1) }
| lident list1_lident param_type_cont
   { let id2ty i = PPTtyapp ([], Qident i) in
     PPTtyapp (List.map id2ty $2 @ $3, Qident $1) }
| primitive_type_non_lident
   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
794 795
;

796 797 798 799
param_type_cont:
| /* epsilon */                                      { [] }
| primitive_type_arg_non_lident                      { [$1] }
| primitive_type_arg_non_lident primitive_type_args  { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
800 801
;

802 803 804
list1_param_var_sep_comma:
| param_var                                  { $1 }
| param_var COMMA list1_param_var_sep_comma  { $1 @ $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
805 806
;

807 808 809
param_var:
| list1_lident COLON primitive_type
   { List.map (fun id -> (Some id, $3)) $1 }
810 811 812 813 814 815
| list1_lident label labels list0_lident_labels COLON primitive_type
   { let l = match List.rev $1 with
       | i :: l -> add_lab i ($2 :: $3) :: l
       | [] -> assert false
     in
     List.map (fun id -> (Some id, $6)) (List.rev_append l $4) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
816 817
;

818
list1_lident:
819 820
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
821 822
;

823 824 825 826 827
list0_lident_labels:
| /* epsilon */                      { [] }
| lident labels list0_lident_labels  { add_lab $1 $2 :: $3 }
;

828 829 830 831 832
/* Idents */

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

835 836 837 838 839 840 841 842 843 844 845 846 847 848 849
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

lident:
| LIDENT          { mk_id $1 (floc ()) }
| lident_keyword  { mk_id $1 (floc ()) }
;

lident_keyword:
| MODEL           { "model" }
;

/* Idents + symbolic operations' names */

850 851 852
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
853 854
;

855
lident_rich:
856 857 858
| lident                      { $1 }
| LEFTPAR lident_op RIGHTPAR  { mk_id $2 (floc ()) }
| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") (floc ()) }
859 860
;

861
lident_op:
862 863 864 865 866 867
| prefix_op             { infix $1 }
| prefix_op UNDERSCORE  { prefix $1 }
| EQUAL                 { infix "=" }
| OPPREF                { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
868 869
;

870
prefix_op:
871 872 873 874 875 876
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

877
/* Qualified idents */
878

879 880 881
qualid:
| ident_rich              { Qident $1 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }
882 883
;

884 885 886
lqualid_rich:
| lident_rich             { Qident $1 }
| uqualid DOT lident_rich { Qdot ($1, $3) }
887 888 889
;

lqualid:
890 891
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
892 893
;

894 895 896 897
/* copy of lqualid to avoid yacc conflicts */
lqualid_copy:
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
898 899
;

900 901 902
uqualid:
| uident              { Qident $1 }
| uqualid DOT uident  { Qdot ($1, $3) }
903 904
;

905 906
/* Theory/Module names */

907 908 909
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
910
;
911

912
any_qualid:
913 914 915 916 917 918 919
| sident                { Qident $1 }
| any_qualid DOT sident { Qdot ($1, $3) }
;

sident:
| ident   { $1 }
| STRING  { mk_id $1 (floc ()) }
Andrei Paskevich's avatar
Andrei Paskevich committed
920
;
921 922 923

/* Misc */

924
label:
925 926
| STRING    { Lstr $1 }
| POSITION  { Lpos $1 }
927 928
;

929 930 931 932 933
labels:
| /* epsilon */ { [] }
| label labels  { $1 :: $2 }
;

934 935 936
bar_:
| /* epsilon */ { () }
| BAR           { () }
937 938
;

939 940 941
/****************************************************************************/

program_file:
942
| list0_theory_or_module_ EOF { $1 }
943 944
;

945
list0_theory_or_module_:
946 947
| /* epsilon */
   { [] }
948
| list1_theory_or_module_
949 950 951
   { $1 }
;

952 953
list1_theory_or_module_:
| theory_or_module_
954
   { [$1] }
955
| theory_or_module_ list1_theory_or_module_
956 957 958
   { $1 :: $2 }
;

959 960
theory_or_module_:
| THEORY uident labels list0_full_decl END
961
   { Ptheory { pth_name = add_lab $2 $3; pth_decl = $4; } }
962
| MODULE uident labels list0_program_decl END
963
   { Pmodule { mod_name = add_lab $2 $3; mod_decl = $4; } }
964 965
;

966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981
list0_full_decl:
| /* epsilon */
   { [] }
| list1_full_decl
   { $1 }
;

list1_full_decl:
| full_decl
   { [$1] }
| full_decl list1_full_decl
   { $1 :: $2 }
;

full_decl:
| NAMESPACE namespace_import namespace_name list0_full_decl END
982
   { Dnamespace (floc_i 3, $3, $2, $4) }
983 984 985 986
| decl
   { Dlogic $1 }
;

987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003
list0_program_decl:
| /* epsilon */
   { [] }
| list1_program_decl
   { $1 }
;

list1_program_decl:
| program_decl
   { [$1] }
| program_decl list1_program_decl
   { $1 :: $2 }
;

program_decl:
| decl
    { Dlogic $1 }
1004
| LET lident_rich_pgm labels list1_type_v_binder opt_cast EQUAL triple
1005
    { Dlet (add_lab $2 $3, mk_expr_i 7 (Efun ($4, cast_body $5 $7))) }
1006
| LET lident_rich_pgm labels EQUAL FUN list1_type_v_binder ARROW triple
1007 1008 1009
    { Dlet (add_lab $2 $3, mk_expr_i 8 (Efun ($6, $8))) }
| LET REC list1_recfun_sep_and
    { Dletrec $3 }
1010
| VAL lident_rich_pgm labels COLON type_v
1011
    { Dparam (add_lab $2 $3, $5) }
1012
| VAL lident_rich_pgm labels list1_type_v_param COLON type_c
1013 1014
    { let tv = Tarrow ($4, $6) in
      Dparam (add_lab $2 $3, tv) }
1015 1016
| EXCEPTION uident labels
    { Dexn (add_lab $2 $3, None) }
1017
| EXCEPTION uident labels primitive_type
1018 1019 1020
    { Dexn (add_lab $2 $3, Some $4) }
| USE use_module
    { $2 }
1021
| NAMESPACE namespace_import namespace_name list0_program_decl END
1022
    { Dnamespace (floc_i 3, $3, $2, $4) }
1023 1024
;

1025 1026 1027 1028
lident_rich_pgm:
| lident_rich
    { $1 }
| LEFTPAR LEFTSQ RIGHTSQ LARROW RIGHTPAR
1029
    { mk_id (mixfix "[]<-") (floc ()) }
1030 1031 1032 1033 1034 1035 1036 1037 1038 1039
;

opt_mutable:
| /* epsilon */ { false }
| MUTABLE       { true  }
;

opt_semicolon:
| /* epsilon */ {}
| SEMICOLON     {}
1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054
;

use_module:
| imp_exp MODULE tqualid
    { Duse ($3, $1, None) }
| imp_exp MODULE tqualid AS uident
    { Duse ($3, $1, Some $5) }
;

list1_recfun_sep_and:
| recfun                           { [ $1 ] }
| recfun WITH list1_recfun_sep_and { $1 :: $3 }
;

recfun:
1055
| lident_rich_pgm labels list1_type_v_binder opt_cast opt_variant EQUAL triple
1056 1057 1058 1059
   { add_lab $1 $2, $3, $5, cast_body $4 $7 }
;

expr:
1060
| expr_arg %prec prec_simple
1061 1062 1063 1064
   { $1 }
| expr EQUAL expr
   { mk_infix $1 "=" $3 }
| expr LTGT expr
Andrei Paskevich's avatar
Andrei Paskevich committed
1065
   { mk_expr (Enot (mk_infix $1 "=" $3)) }
1066
| expr LARROW expr
1067
    { match $1.expr_desc with
1068 1069 1070
        | Eapply (e11, e12) -> begin match e11.expr_desc with
            | Eident x ->
                mk_expr (Eassign (e12, x, $3))
1071
            | Eapply ({ expr_desc = Eident (Qident x) }, e11)
Andrei Paskevich's avatar
Andrei Paskevich committed
1072
            when x.id = mixfix "[]" ->
1073 1074 1075 1076 1077 1078
                mk_mixfix3 "[]<-" e11 e12 $3
            | _ ->
                raise Parsing.Parse_error
          end
        | _ ->
            raise Parsing.Parse_error
1079
    }
1080 1081 1082 1083 1084 1085 1086 1087
| expr OP1 expr
   { mk_infix $1 $2 $3 }
| expr OP2 expr
   { mk_infix $1 $2 $3 }
| expr OP3 expr
   { mk_infix $1 $2 $3 }
| expr OP4 expr
   { mk_infix $1 $2 $3 }
1088
| NOT expr %prec prec_prefix_op
Andrei Paskevich's avatar
Andrei Paskevich committed
1089
   { mk_expr (Enot $2) }
1090
| prefix_op expr %prec prec_prefix_op