parser.mly 35.3 KB
Newer Older
1 2
/**************************************************************************/
/*                                                                        */
MARCHE Claude's avatar
MARCHE Claude committed
3
/*  Copyright (C) 2010-2012                                               */
4 5 6
/*    François Bobot                                                      */
/*    Jean-Christophe Filliâtre                                           */
/*    Claude Marché                                                       */
MARCHE Claude's avatar
MARCHE Claude committed
7
/*    Guillaume Melquiond                                                 */
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
8
/*    Andrei Paskevich                                                    */
9 10 11 12 13 14 15 16 17 18 19
/*                                                                        */
/*  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
20 21

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

  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

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

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

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

  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 =
61 62
    ref_set uc_ref (Typing.add_decl (ref_get uc_ref) d)

63
  let new_use_clone loc d =
64
    let env = ref_get env_ref in let lenv = ref_get lenv_ref in
65
    ref_set uc_ref (Typing.add_use_clone env lenv (ref_get uc_ref) loc d)
66

67
end
68

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
69 70 71 72
  open Ptree
  open Parsing

  let loc () = (symbol_start_pos (), symbol_end_pos ())
73 74
  let floc () = Loc.extract (loc ())

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
75
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
76
  let floc_i i = Loc.extract (loc_i i)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
77
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
78
  let floc_ij i j = Loc.extract (loc_ij i j)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
79 80

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
81 82
  let mk_pp d = mk_ppl (floc ()) d
  let mk_pp_i i d = mk_ppl (floc_i i) d
83

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

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

89
  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
90
  let prefix_pp p a = prefix_ppl (floc ()) p a
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91

92
  let infix  s = "infix "  ^ s
93
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
94
  let mixfix s = "mixfix " ^ s
95

96 97
  let quote id = { id with id = "'" ^ id.id }

98 99 100 101
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

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

Andrei Paskevich's avatar
Andrei Paskevich committed
102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
  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]))

118 119 120 121 122
  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
      | _ -> raise exn
    )
123

124 125
  let mk_expr d = { expr_loc = floc (); expr_desc = d }
  let mk_expr_i i d = { expr_loc = floc_i i; expr_desc = d }
126 127 128 129 130 131 132

  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
    | [] ->
133
        assert false
134
    | [a] ->
135
        Eapply (f, a)
136
    | a :: l ->
137 138
        let loc = Loc.join f.expr_loc a.expr_loc in
        mk_apply { expr_loc = loc; expr_desc = Eapply (f, a) } l
139 140 141 142 143 144 145

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

Andrei Paskevich's avatar
Andrei Paskevich committed
146 147
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
148 149
    mk_expr (mk_apply_id id [e1; e2])

Andrei Paskevich's avatar
Andrei Paskevich committed
150 151
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
152 153
    mk_expr (mk_apply_id id [e1; e2; e3])

154
  let mk_infix e1 op e2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
155
    let id = mk_id (infix op) (floc_i 2) in
156 157 158
    mk_expr (mk_apply_id id [e1; e2])

  let mk_prefix op e1 =
Andrei Paskevich's avatar
Andrei Paskevich committed
159
    let id = mk_id (prefix op) (floc_i 1) in
160 161
    mk_expr (mk_apply_id id [e1])

Andrei Paskevich's avatar
Andrei Paskevich committed
162 163
  let exit_exn () = Qident (mk_id "%Exit" (floc ()))
  let id_anonymous () = mk_id "_" (floc ())
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
164
  let ty_unit () = PPTtuple []
165

Andrei Paskevich's avatar
Andrei Paskevich committed
166
  let id_lt_nat () = Qident (mk_id "lt_nat" (floc ()))
167 168 169

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

170 171 172 173 174 175 176
  let effect_union e1 e2 =
    let { pe_reads = r1; pe_writes = w1; pe_raises = x1 } = e1 in
    let { pe_reads = r2; pe_writes = w2; pe_raises = x2 } = e2 in
    { pe_reads = r1 @ r2; pe_writes = w1 @ w2; pe_raises = x1 @ x2 }

  let effect_exprs ghost l = List.map (fun x -> (ghost, x)) l

177 178 179 180 181
  let type_c p ty ef q =
    { pc_result_type = ty;
      pc_effect      = ef;
      pc_pre         = p;
      pc_post        = q; }
182

183
  let add_init_mark e =
184
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
185
    { e with expr_desc = Emark (init, e) }
186

187 188 189 190 191 192 193 194 195
  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

196 197 198
  let qualid_last = function
    | Qident x | Qdot (_, x) -> x.id

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
199 200
%}

201
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
202

203
%token <string> LIDENT UIDENT
204
%token <Ptree.integer_constant> INTEGER
205
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
206 207
%token <Ptree.real_constant> FLOAT
%token <string> STRING
208
%token <Loc.position> POSITION
209 210 211

/* keywords */

212
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
213 214 215
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
Andrei Paskevich's avatar
Andrei Paskevich committed
216
%token THEN THEORY TRUE TYPE USE WITH
217

218 219
/* program keywords */

220 221
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO
%token EXCEPTION FOR
222
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE PRIVATE RAISE
Andrei Paskevich's avatar
Andrei Paskevich committed
223
%token RAISES READS REC TO TRY VAL VARIANT WHILE WRITES
224

225 226
/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
227
%token AND ARROW
228
%token BAR
229
%token COLON COMMA
230
%token DOT EQUAL FUNC LAMBDA LTGT
231
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTREC LEFTSQ
232
%token LARROW LRARROW
Andrei Paskevich's avatar
Andrei Paskevich committed
233
%token OR PRED QUOTE
234
%token RIGHTPAR RIGHTREC RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
235
%token UNDERSCORE
236 237 238

%token EOF

239 240
/* program symbols */

241
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
242

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
243 244
/* Precedences */

245
%nonassoc prec_mark
246 247 248 249 250 251 252 253 254
%nonassoc prec_post
%nonassoc BAR

%nonassoc prec_triple
%nonassoc prec_simple

%nonassoc IN
%right SEMICOLON
%nonassoc prec_no_else
255
%nonassoc DOT ELSE GHOST
256
%nonassoc prec_named
257
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
258

Andrei Paskevich's avatar
Andrei Paskevich committed
259
%right ARROW LRARROW
260 261
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
262
%nonassoc NOT
263
%left EQUAL LTGT OP1
264 265
%nonassoc LARROW
%nonassoc RIGHTSQ    /* stronger than <- for e1[e2 <- e3] */
266
%left OP2
267
%left OP3
268
%left OP4
269
%nonassoc prec_prefix_op
270
%left prec_app
271 272
%nonassoc LEFTSQ
%nonassoc OPPREF
273

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
274 275
/* Entry points */

Andrei Paskevich's avatar
Andrei Paskevich committed
276
%type <unit Env.library -> string list -> unit> pre_logic_file
277
%start pre_logic_file
278
%type <Theory.theory Util.Mstr.t> logic_file
Andrei Paskevich's avatar
Andrei Paskevich committed
279
%start logic_file
280 281
%type <Ptree.program_file> program_file
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282 283
%%

284 285 286 287
pre_logic_file:
| /* epsilon */  { Incremental.open_logic_file }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
288
logic_file:
289
| list0_theory EOF  { Incremental.close_logic_file () }
290 291 292
;

/* File, theory, namespace */
293

294 295 296
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
297 298
;

299
theory_head:
300
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
301 302
;

303
theory:
304
| theory_head list0_decl END  { Incremental.close_theory (floc_i 1) }
305 306
;

307
list0_decl:
308 309 310 311 312 313
| /* epsilon */        { () }
| new_decl list0_decl  { () }
;

new_decl:
| decl
314
   { Incremental.new_decl $1 }
315
| use_clone
316
   { Incremental.new_use_clone (floc ()) $1 }
317
| namespace_head namespace_import namespace_name list0_decl END
318
   { Incremental.close_namespace (floc_ij 1 3) $2 $3 }
319 320
;

321
namespace_head:
322
| NAMESPACE  { Incremental.open_namespace () }
323 324 325 326 327 328 329 330
;

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

namespace_name:
331
| uident      { Some $1.id }
332 333 334 335 336
| UNDERSCORE  { None }
;

/* Declaration */

337
decl:
338 339
| TYPE list1_type_decl
    { TypeDecl $2 }
340 341
| CONSTANT logic_decl_constant
    { LogicDecl [$2] }
Andrei Paskevich's avatar
Andrei Paskevich committed
342 343 344
| FUNCTION list1_logic_decl_function
    { LogicDecl $2 }
| PREDICATE list1_logic_decl_predicate
345
    { LogicDecl $2 }
346 347
| inductive list1_inductive_decl
    { IndDecl ($1, $2) }
348
| AXIOM ident labels COLON lexpr
349
    { PropDecl (floc (), Kaxiom, add_lab $2 $3, $5) }
350
| LEMMA ident labels COLON lexpr
351
    { PropDecl (floc (), Klemma, add_lab $2 $3, $5) }
352
| GOAL ident labels COLON lexpr
353
    { PropDecl (floc (), Kgoal, add_lab $2 $3, $5) }
354
| META sident list1_meta_arg_sep_comma
355
    { Meta (floc (), $2, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
356 357
;

358 359 360 361 362
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

363 364
/* Use and clone */

365 366
use_clone:
| USE use
367
    { ($2, None) }
368
| CLONE use clone_subst
369
    { ($2, Some $3) }
370 371
;

372 373
use:
| imp_exp tqualid
374
    { { use_theory = $2; use_as = Some (qualid_last $2); use_imp_exp = $1 } }
375
| imp_exp tqualid AS uident
376
    { { use_theory = $2; use_as = Some $4.id; use_imp_exp = $1 } }
377
| imp_exp tqualid AS UNDERSCORE
378
    { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
379 380
;

381
imp_exp:
382 383 384
| IMPORT        { Some true }
| EXPORT        { None }
| /* epsilon */ { Some false }
385 386 387 388 389 390 391 392 393 394 395 396 397
;

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

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

subst:
398 399 400 401 402 403 404
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
| TYPE      qualid EQUAL qualid { CStsym (floc (), $2, $4) }
| CONSTANT  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| FUNCTION  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }
| LEMMA     qualid              { CSlemma (floc (), $2) }
| GOAL      qualid              { CSgoal  (floc (), $2) }
405 406
;

407 408 409 410 411
ns:
| uqualid { Some $1 }
| DOT     { None }
;

412 413 414 415 416 417 418 419
/* 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
420
| TYPE      qualid { PMAts  $2 }
421 422
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
423 424
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
425
| INTEGER          { PMAint (small_integer $1) }
426 427
;

428 429 430
/* Type declarations */

list1_type_decl:
431 432
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
433 434 435
;

type_decl:
436
| lident labels type_args typedefn
437
  { let model, vis, def = $4 in
438
    let vis = if model then Abstract else vis in
439
    { td_loc = floc (); td_ident = add_lab $1 $2;
440
      td_params = $3; td_model = model; td_vis = vis; td_def = def } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
441 442
;

443
type_args:
444 445
| /* epsilon */             { [] }
| type_var labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
446 447 448
;

typedefn:
449 450 451 452 453 454 455 456 457 458 459 460 461 462
| /* epsilon */                         { false, Public, TDabstract }
| equal_model visibility typecases      { $1,    $2,     TDalgebraic $3 }
| equal_model visibility BAR typecases  { $1,    $2,     TDalgebraic $4 }
| equal_model visibility record_type    { $1,    $2,     TDrecord $3 }
/* abstract/private is not allowed for alias type */
| equal_model visibility primitive_type
    { if $2 <> Public then Loc.error ~loc:(floc_i 2) Parsing.Parse_error;
      $1, Public, TDalias $3 }
;

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
463 464 465 466 467
;

equal_model:
| EQUAL { false }
| MODEL { true }
468 469 470
;

record_type:
Andrei Paskevich's avatar
Andrei Paskevich committed
471
| LEFTREC list1_record_field opt_semicolon RIGHTREC { List.rev $2 }
472 473 474 475
;

list1_record_field:
| record_field                              { [$1] }
476
| list1_record_field SEMICOLON record_field { $3 :: $1 }
477 478
;

479 480 481 482 483 484 485 486
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

487
record_field:
488 489 490 491 492 493
| field_modifiers lident labels COLON primitive_type
   { { f_loc = floc ();
       f_ident = add_lab $2 $3;
       f_mutable = fst $1;
       f_ghost = snd $1;
       f_pty = $5 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
494 495 496 497 498 499 500 501
;

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

typecase:
502
| uident labels params   { (floc (), add_lab $1 $2, $3) }
503 504 505 506
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
507 508 509 510 511 512 513 514 515 516
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 }
;

517
list1_logic_decl:
518 519
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
520 521
;

522 523 524 525 526 527
logic_decl_constant:
| lident_rich labels COLON primitive_type logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = []; ld_type = Some $4; ld_def = $5 } }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
528 529 530 531 532 533 534 535 536 537 538 539
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 } }
;

540
logic_decl:
541
| lident_rich labels params logic_type_option logic_def_option
542
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
543
      ld_params = $3; ld_type = $4; ld_def = $5 } }
544 545 546 547 548 549 550 551 552 553
;

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
554 555
;

556 557 558
/* Inductive declarations */

list1_inductive_decl:
559 560
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
561 562 563
;

inductive_decl:
564
| lident_rich labels params inddefn
565
  { { in_loc = floc (); in_ident = add_lab $1 $2;
566
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
567
;
568

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
569 570 571 572 573 574 575 576 577 578 579
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

583 584 585 586 587 588 589 590
/* Type expressions */

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

primitive_type_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
591 592
| primitive_type_arg_non_lident           { $1 }
| uqualid DOT lident primitive_type_args  { PPTtyapp ($4, Qdot ($1, $3)) }
593 594 595 596 597 598 599 600
;

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

primitive_type_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
601
| lident                         { PPTtyapp ([], Qident $1) }
602 603 604 605
| primitive_type_arg_non_lident  { $1 }
;

primitive_type_arg_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
606 607
| uqualid DOT lident
   { PPTtyapp ([], Qdot ($1, $3)) }
608 609 610 611
| type_var
   { PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
612 613 614 615 616 617
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
618 619 620 621 622
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

623
type_var:
624
| QUOTE lident { $2 }
625 626
;

627 628
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
629
lexpr:
630
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
631
   { infix_pp $1 PPimplies $3 }
632
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
633
   { infix_pp $1 PPiff $3 }
634
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
635
   { infix_pp $1 PPor $3 }
636
| lexpr BARBAR lexpr
637
   { infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPor $3 }
638
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
639
   { infix_pp $1 PPand $3 }
640
| lexpr AMPAMP lexpr
641
   { infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPand $3 }
642
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
643
   { prefix_pp PPnot $2 }
644
| lexpr EQUAL lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
645
   { mk_l_infix $1 "=" $3 }
646
| lexpr LTGT lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
647
   { prefix_pp PPnot (mk_l_infix $1 "=" $3) }
648
| lexpr OP1 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
649
   { mk_l_infix $1 $2 $3 }
650
| lexpr OP2 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
651
   { mk_l_infix $1 $2 $3 }
652
| lexpr OP3 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
653
   { mk_l_infix $1 $2 $3 }
654
| lexpr OP4 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
655
   { mk_l_infix $1 $2 $3 }
656
| prefix_op lexpr %prec prec_prefix_op
Andrei Paskevich's avatar
Andrei Paskevich committed
657
   { mk_l_prefix $1 $2 }
658 659
| qualid list1_lexpr_arg
   { mk_pp (PPapp ($1, $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
660
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
661
   { mk_pp (PPif ($2, $4, $6)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
662 663
| quant list1_param_var_sep_comma triggers DOT lexpr
   { mk_pp (PPquant ($1, $2, $3, $5)) }
664 665
| label lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
666
| LET pattern EQUAL lexpr IN lexpr
667 668
   { match $2.pat_desc with
       | PPpvar id -> mk_pp (PPlet (id, $4, $6))
Andrei Paskevich's avatar
Andrei Paskevich committed
669 670
       | _ -> mk_pp (PPmatch ($4, [$2, $6])) }
| MATCH lexpr WITH bar_ match_cases END
671
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
672 673
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
   { mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
674 675
| EPSILON lident labels COLON primitive_type DOT lexpr
   { mk_pp (PPeps (add_lab $2 $3, $5, $7)) }
676
| lexpr COLON primitive_type
677
   { mk_pp (PPcast ($1, $3)) }
678
| lexpr_arg
679 680 681
   { $1 }
;

682 683 684 685 686 687 688 689 690
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

691 692 693
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
694
;
695

696
constant:
Andrei Paskevich's avatar
Andrei Paskevich committed
697 698
| INTEGER   { Term.ConstInt $1 }
| FLOAT     { Term.ConstReal $1 }
699 700
;

701
lexpr_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
702 703 704 705 706 707
| 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 }
708
| QUOTE uident      { mk_pp (PPvar (Qident (quote $2))) }
Andrei Paskevich's avatar
Andrei Paskevich committed
709 710 711
;

lexpr_dot:
Andrei Paskevich's avatar
Andrei Paskevich committed
712 713 714
| lqualid_copy      { mk_pp (PPvar $1) }
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
715 716 717
;

lexpr_sub:
718
| lexpr_dot DOT lqualid_rich
Andrei Paskevich's avatar
Andrei Paskevich committed
719
   { mk_pp (PPapp ($3, [$1])) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
720 721
| LEFTPAR lexpr RIGHTPAR
   { $2 }
722 723 724 725
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
726 727
| LEFTREC list1_field_value opt_semicolon RIGHTREC
   { mk_pp (PPrecord (List.rev $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
728 729
| LEFTREC lexpr_arg WITH list1_field_value opt_semicolon RIGHTREC
   { mk_pp (PPupdate ($2, List.rev $4)) }
730
| lexpr_arg LEFTSQ lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
731
   { mk_l_mixfix2 "[]" $1 $3 }
732
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
733
   { mk_l_mixfix3 "[<-]" $1 $3 $5 }
Andrei Paskevich's avatar
Andrei Paskevich committed
734
;
735

Andrei Paskevich's avatar
Andrei Paskevich committed
736 737 738 739
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
740 741
| FUNC    { PPfunc }
| PRED    { PPpred }
Andrei Paskevich's avatar
Andrei Paskevich committed
742 743
;

744
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
745

746 747 748 749
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
750

751 752 753 754 755 756 757 758 759 760 761 762 763 764 765
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 */
766

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
767 768 769 770 771 772
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
773
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
774 775 776
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
777 778 779 780 781 782 783 784 785 786 787 788 789 790 791
| 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:
792 793 794
| 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
795
;
796

797
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
798 799 800
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
801

802
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
803
| UNDERSCORE                { mk_pat (PPpwild) }
804
| lident labels             { mk_pat (PPpvar (add_lab $1 $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
805 806 807
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
808 809 810 811 812 813 814 815 816 817
| 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
818 819
;

820
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
821

822 823 824
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
825 826
;

827 828 829 830 831 832 833 834 835 836 837 838 839
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
840 841
;

842 843 844 845 846 847 848 849
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
850 851
;

852 853 854 855
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
856 857
;

858 859 860
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
861 862
;

863 864 865
param_var:
| list1_lident COLON primitive_type
   { List.map (fun id -> (Some id, $3)) $1 }
866 867 868 869 870 871
| 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
872 873
;

874
list1_lident:
875 876
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
877 878
;