parser.mly 15.8 KB
Newer Older
1 2
/**************************************************************************/
/*                                                                        */
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
/*  Copyright (C) 2010-                                                   */
/*    Francois Bobot                                                      */
/*    Jean-Christophe Filliatre                                           */
/*    Johannes Kanig                                                      */
/*    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 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
  open Theory

  let env_ref  = ref []
  let lenv_ref = ref []
  let uc_ref   = ref []

  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

  let inside_env env rule lexer lexbuf =
    ref_push env_ref env;
      ref_push lenv_ref Mnm.empty;
    let res = rule lexer lexbuf in
      ref_drop lenv_ref;
    ref_drop env_ref;
    res

  let inside_uc env lenv uc rule lexer lexbuf =
    ref_push env_ref env;
      ref_push lenv_ref lenv;
        ref_push uc_ref uc;
    let res = rule lexer lexbuf in
        ref_drop uc_ref;
      ref_drop lenv_ref;
    ref_drop env_ref;
    res
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52 53 54 55 56 57 58 59 60 61 62

  open Ptree
  open Parsing

  let loc () = (symbol_start_pos (), symbol_end_pos ())
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
  let mk_pp d = mk_ppl (loc ()) d
  let mk_pp_i i d = mk_ppl (loc_i i) d
63

Andrei Paskevich's avatar
Andrei Paskevich committed
64 65
  let mk_pat p = { pat_loc = loc (); pat_desc = p }

66
  let infix_ppl loc a i b = mk_ppl loc (PPbinop (a, i, b))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
67 68
  let infix_pp a i b = infix_ppl (loc ()) a i b

69
  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
70 71
  let prefix_pp p a = prefix_ppl (loc ()) p a

72 73 74
  let infix s = "infix " ^ s
  let prefix s = "prefix " ^ s

75 76 77 78 79
  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
      | _ -> raise exn
    )
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
80 81
%}

82
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83

84
%token <string> LIDENT UIDENT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85
%token <string> INTEGER
86
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87 88
%token <Ptree.real_constant> FLOAT
%token <string> STRING
89 90 91

/* keywords */

92 93 94
%token AND AS AXIOM CLONE
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
95
%token LET LOGIC MATCH META NAMESPACE NOT PROP OR
Andrei Paskevich's avatar
Andrei Paskevich committed
96
%token THEN THEORY TRUE TYPE USE WITH
97 98 99

/* symbols */

100
%token ARROW ASYM_AND ASYM_OR
101 102
%token BAR
%token COLON COMMA
103
%token DOT EQUAL LTGT
104
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
105
%token LRARROW
Andrei Paskevich's avatar
Andrei Paskevich committed
106
%token QUOTE
107
%token RIGHTPAR RIGHTSQ
108 109 110 111
%token UNDERSCORE

%token EOF

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
112 113
/* Precedences */

114
%nonassoc DOT ELSE IN
115
%nonassoc prec_named
116
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
117 118

%right ARROW LRARROW
119 120
%right OR ASYM_OR
%right AND ASYM_AND
Andrei Paskevich's avatar
Andrei Paskevich committed
121
%nonassoc NOT
122
%left EQUAL LTGT OP1
123
%left OP2
124
%left OP3
125
%left OP4
Andrei Paskevich's avatar
Andrei Paskevich committed
126
%nonassoc prefix_op
127

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
128 129
/* Entry points */

130 131 132 133 134 135
%type <Ptree.lexpr> lexpr_eof
%start lexpr_eof
%type <Theory.theory_uc> list0_decl_eof
%start list0_decl_eof
%type <Theory.theory Theory.Mnm.t> logic_file_eof
%start logic_file_eof
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
136 137
%%

138 139 140 141 142 143 144 145 146 147 148 149 150
logic_file_eof:
| list0_theory EOF  { ref_get lenv_ref }
;

list0_decl_eof:
| list0_decl EOF  { ref_get uc_ref }
;

lexpr_eof:
| lexpr EOF  { $1 }
;

/* File, theory, namespace */
151

152 153 154
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
155 156
;

157 158 159 160 161
theory_head:
| THEORY uident
   { let id = $2 in
     let name = Ident.id_user id.id id.id_loc in
     ref_push uc_ref (create_theory name); id }
162 163
;

164
theory:
165 166 167
| theory_head list0_decl END
   { let uc = ref_pop uc_ref in
     ref_set lenv_ref (Typing.close_theory (ref_get lenv_ref) $1 uc) }
168 169
;

170
list0_decl:
171 172 173 174 175 176 177 178 179 180
| /* epsilon */        { () }
| new_decl list0_decl  { () }
;

new_decl:
| decl
   { 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) $1) }
| namespace_head namespace_import namespace_name list0_decl END
   { ref_set uc_ref (Typing.close_namespace (loc ()) $2 $3 (ref_get uc_ref)) }
181 182
;

183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
namespace_head:
| NAMESPACE
   { ref_set uc_ref (open_namespace (ref_get uc_ref)) }
;

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

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

/* Declaration */

200
decl:
201 202 203 204 205 206
| TYPE list1_type_decl
    { TypeDecl $2 }
| LOGIC list1_logic_decl
    { LogicDecl $2 }
| INDUCTIVE list1_inductive_decl
    { IndDecl $2 }
207 208 209 210 211 212 213 214 215 216
| AXIOM uident COLON lexpr
    { PropDecl (loc (), Kaxiom, $2, $4) }
| LEMMA uident COLON lexpr
    { PropDecl (loc (), Klemma, $2, $4) }
| GOAL uident COLON lexpr
    { PropDecl (loc (), Kgoal, $2, $4) }
| USE use
    { UseClone (loc (), $2, None) }
| CLONE use clone_subst
    { UseClone (loc (), $2, Some $3) }
217 218
| META ident list1_meta_arg_sep_comma
    { Meta (loc (), $2, $3) }
219 220
| META STRING list1_meta_arg_sep_comma
    { Meta (loc (), { id = $2; id_loc = loc_i 2 }, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
221 222
;

223 224 225 226 227 228 229 230 231
/* 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 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
232 233
;

234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256
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:
| TYPE  qualid EQUAL qualid { CStsym ($2, $4) }
| LOGIC qualid EQUAL qualid { CSlsym ($2, $4) }
| LEMMA qualid              { CSlemma $2 }
| GOAL  qualid              { CSgoal  $2 }
;

257 258 259 260 261 262 263 264 265 266 267 268 269 270 271
/* Meta args */

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

meta_arg:
| TYPE  qualid { PMAts  $2 }
| LOGIC qualid { PMAls  $2 }
| PROP  qualid { PMApr  $2 }
| STRING       { PMAstr $1 }
| INTEGER      { PMAint $1 }
;

272 273 274
/* Type declarations */

list1_type_decl:
275 276
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
277 278 279
;

type_decl:
280 281
| lident type_args typedefn
  { { td_loc = loc (); td_ident = $1; td_params = $2; td_def = $3 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282 283
;

284
type_args:
285 286
| /* epsilon */      { [] }
| type_var type_args { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
287 288 289
;

typedefn:
290 291 292 293
| /* epsilon */           { TDabstract }
| EQUAL primitive_type    { TDalias $2 }
| EQUAL typecases         { TDalgebraic $2 }
| EQUAL BAR typecases     { TDalgebraic $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
294 295 296 297 298 299 300 301
;

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

typecase:
302 303 304 305 306 307
| uident params   { (loc_i 1,$1,$2) }
;

/* Logic declarations */

list1_logic_decl:
308 309
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
310 311 312
;

logic_decl:
313 314 315
| lident_rich params logic_type_option logic_def_option
  { { ld_loc = loc (); ld_ident = $1; ld_params = $2;
      ld_type = $3; ld_def = $4; } }
316 317 318 319 320 321 322 323 324 325
;

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
326 327
;

328 329 330
/* Inductive declarations */

list1_inductive_decl:
331 332
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
333 334 335
;

inductive_decl:
336 337
| lident_rich params inddefn
  { { in_loc = loc (); in_ident = $1; in_params = $2; in_def = $3 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
338
;
339

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
340 341 342 343 344 345 346 347 348 349 350
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

indcase:
Andrei Paskevich's avatar
Andrei Paskevich committed
351
| uident COLON lexpr { (loc (),$1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
352 353
;

354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377
/* Type expressions */

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

primitive_type_non_lident:
| primitive_type_arg_non_lident  { $1 }
| lq_uident primitive_type_args  { PPTtyapp ($2, $1) }
;

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

primitive_type_arg:
| lq_lident                      { PPTtyapp ([], $1) }
| primitive_type_arg_non_lident  { $1 }
;

primitive_type_arg_non_lident:
| lq_uident
378
   { PPTtyapp ([], $1) }
379 380 381 382
| type_var
   { PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
383 384 385 386 387 388
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
389 390 391 392 393
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

394 395
type_var:
| QUOTE ident { $2 }
396 397
;

398 399
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
400
lexpr:
401
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
402
   { infix_pp $1 PPimplies $3 }
403
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
404
   { infix_pp $1 PPiff $3 }
405
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
406
   { infix_pp $1 PPor $3 }
407
| lexpr ASYM_OR lexpr
MARCHE Claude's avatar
MARCHE Claude committed
408
   { let label = Ident.label "asym_split" in
409
     mk_pp (PPnamed (label, infix_pp $1 PPor $3)) }
410
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
411
   { infix_pp $1 PPand $3 }
412
| lexpr ASYM_AND lexpr
MARCHE Claude's avatar
MARCHE Claude committed
413
   { let label = Ident.label "asym_split" in
414
     mk_pp (PPnamed (label, infix_pp $1 PPand $3)) }
415
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
416
   { prefix_pp PPnot $2 }
417
| lexpr EQUAL lexpr
418
   { let id = { id = infix "="; id_loc = loc_i 2 } in
419
     mk_pp (PPinfix ($1, id, $3)) }
420 421 422
| lexpr LTGT lexpr
   { let id = { id = infix "="; id_loc = loc_i 2 } in
     prefix_pp PPnot (mk_pp (PPinfix ($1, id, $3))) }
423
| lexpr OP1 lexpr
424
   { let id = { id = infix $2; id_loc = loc_i 2 } in
425
     mk_pp (PPinfix ($1, id, $3)) }
426
| lexpr OP2 lexpr
427
   { let id = { id = infix $2; id_loc = loc_i 2 } in
428
     mk_pp (PPinfix ($1, id, $3)) }
429
| lexpr OP3 lexpr
430
   { let id = { id = infix $2; id_loc = loc_i 2 } in
431
     mk_pp (PPinfix ($1, id, $3)) }
432
| lexpr OP4 lexpr
433
   { let id = { id = infix $2; id_loc = loc_i 2 } in
434
     mk_pp (PPinfix ($1, id, $3)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
435
| any_op lexpr %prec prefix_op
436 437
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }
438 439
| qualid list1_lexpr_arg
   { mk_pp (PPapp ($1, $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
440
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
441
   { mk_pp (PPif ($2, $4, $6)) }
442
| FORALL list1_param_var_sep_comma triggers DOT lexpr
443
   { mk_pp (PPquant (PPforall, $2, $3, $5)) }
444
| EXISTS list1_param_var_sep_comma triggers DOT lexpr
445
   { mk_pp (PPquant (PPexists, $2, $3, $5)) }
446
| STRING lexpr %prec prec_named
MARCHE Claude's avatar
MARCHE Claude committed
447
   { mk_pp (PPnamed (Ident.label ~loc:(loc ()) $1, $2)) }
448
| LET pattern EQUAL lexpr IN lexpr
449 450
   { match $2.pat_desc with
       | PPpvar id -> mk_pp (PPlet (id, $4, $6))
Andrei Paskevich's avatar
Andrei Paskevich committed
451 452
       | _ -> mk_pp (PPmatch ($4, [$2, $6])) }
| MATCH lexpr WITH bar_ match_cases END
453
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
454 455
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
   { mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
456 457
| EPSILON lident COLON primitive_type DOT lexpr
   { mk_pp (PPeps ($2, $4, $6)) }
458
| lexpr COLON primitive_type
459
   { mk_pp (PPcast ($1, $3)) }
460
| lexpr_arg
461 462 463
   { $1 }
;

464 465 466
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
467
;
468

469 470 471
lexpr_arg:
| qualid
   { mk_pp (PPvar $1) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
472
| INTEGER
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
473
   { mk_pp (PPconst (Term.ConstInt $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
474
| FLOAT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
475
   { mk_pp (PPconst (Term.ConstReal $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
476 477 478
| TRUE
   { mk_pp PPtrue }
| FALSE
479
   { mk_pp PPfalse }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
480 481
| LEFTPAR lexpr RIGHTPAR
   { $2 }
482 483 484 485
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
486 487 488
| OPPREF lexpr_arg
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }
Andrei Paskevich's avatar
Andrei Paskevich committed
489
;
490

491
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
492

493 494 495 496
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
497

498 499 500 501 502 503 504 505 506 507 508 509 510 511 512
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 */
513

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
514 515 516 517 518 519
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
520
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
521 522 523
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542
| 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:
| pat_arg                { $1 }
| uqualid list1_pat_arg  { mk_pat (PPpapp ($1, $2)) }
| pat_uni AS lident      { mk_pat (PPpas ($1, $3)) }
;
543

544
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
545 546 547
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
548

549
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
550 551 552 553 554
| UNDERSCORE                { mk_pat (PPpwild) }
| lident                    { mk_pat (PPpvar $1) }
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
555 556
;

557
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
558

559 560 561
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
562 563
;

564 565 566 567 568 569 570 571 572 573 574 575 576
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
577 578
;

579 580 581 582 583 584 585 586
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
587 588
;

589 590 591 592
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
593 594
;

595 596 597
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
598 599
;

600 601 602
param_var:
| list1_lident COLON primitive_type
   { List.map (fun id -> (Some id, $3)) $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
603 604
;

605
list1_lident:
606 607
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
608 609
;

610 611 612 613 614
/* Idents */

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

617 618 619
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
620 621
;

622 623 624 625 626 627 628 629 630 631 632
lident_rich:
| lident
    { $1 }
| LEFTPAR lident_op RIGHTPAR
    { { id = infix $2; id_loc = loc () } }
| LEFTPAR_STAR_RIGHTPAR
    { { id = infix "*"; id_loc = loc () } }
| LEFTPAR lident_op UNDERSCORE RIGHTPAR
    { { id = prefix $2; id_loc = loc () } }
| LEFTPAR OPPREF RIGHTPAR
    { { id = prefix $2; id_loc = loc () } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
633 634
;

635 636
lident:
| LIDENT  { { id = $1; id_loc = loc () } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
637 638
;

639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683
lident_op:
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
| EQUAL { "=" }
;

any_op:
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

uident:
| UIDENT { { id = $1; id_loc = loc () } }
;

lq_lident:
| lident             { Qident $1 }
;

lq_uident:
| uqualid DOT lident { Qdot ($1, $3) }
;

lqualid:
| lq_lident { $1 }
| lq_uident { $1 }
;

uqualid:
| uident             { Qident $1 }
| uqualid DOT uident { Qdot ($1, $3) }
;

any_qualid:
| ident                { Qident $1 }
| any_qualid DOT ident { Qdot ($1, $3) }
;

tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
684
;
685 686 687 688

qualid:
| ident_rich             { Qident $1 }
| uqualid DOT ident_rich { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
689
;
690 691 692 693 694 695

/* Misc */

bar_:
| /* epsilon */ { () }
| BAR           { () }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
696 697
;