parser.mly 14.4 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

%{

  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
32

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

35
  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
36 37
  let infix_pp a i b = infix_ppl (loc ()) a i b

38
  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
39 40
  let prefix_pp p a = prefix_ppl (loc ()) p a

41 42 43
  let infix s = "infix " ^ s
  let prefix s = "prefix " ^ s

44 45 46 47 48
  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
49 50
%}

51
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52

53
%token <string> LIDENT UIDENT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
54
%token <string> INTEGER
55
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
56 57
%token <Ptree.real_constant> FLOAT
%token <string> STRING
58 59 60

/* keywords */

61 62 63
%token AND AS AXIOM CLONE
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
64
%token LET LOGIC MATCH META NAMESPACE NOT PROP OR
Andrei Paskevich's avatar
Andrei Paskevich committed
65
%token THEN THEORY TRUE TYPE USE WITH
66 67 68

/* symbols */

69
%token ARROW ASYM_AND ASYM_OR
70 71
%token BAR
%token COLON COMMA
72
%token DOT EQUAL LTGT
73
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
74
%token LRARROW
Andrei Paskevich's avatar
Andrei Paskevich committed
75
%token QUOTE
76
%token RIGHTPAR RIGHTSQ
77 78 79 80
%token UNDERSCORE

%token EOF

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
81 82
/* Precedences */

83
%nonassoc DOT ELSE IN
84
%nonassoc prec_named
85
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86 87

%right ARROW LRARROW
88 89
%right OR ASYM_OR
%right AND ASYM_AND
Andrei Paskevich's avatar
Andrei Paskevich committed
90
%nonassoc NOT
91
%left EQUAL LTGT OP1
92
%left OP2
93
%left OP3
94
%left OP4
Andrei Paskevich's avatar
Andrei Paskevich committed
95
%nonassoc prefix_op
96
%nonassoc OPPREF
97

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
98 99 100 101
/* Entry points */

%type <Ptree.lexpr> lexpr
%start lexpr
102 103
%type <Ptree.decl list> list0_decl
%start list0_decl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104 105 106 107
%type <Ptree.logic_file> logic_file
%start logic_file
%%

108
/* File, theory, declaration */
109

110 111 112
logic_file:
| list1_theory EOF  { $1 }
| EOF               { [] }
113 114
;

115 116 117
list1_theory:
| theory                { [$1] }
| theory list1_theory   { $1 :: $2 }
118 119
;

120 121 122
theory:
| THEORY uident list0_decl END
   { { pt_loc = loc (); pt_name = $2; pt_decl = $3 } }
123 124
;

125 126 127
list0_decl:
| /* epsilon */    { [] }
| decl list0_decl  { $1 :: $2 }
128 129 130
;

decl:
131 132 133 134 135 136
| TYPE list1_type_decl
    { TypeDecl $2 }
| LOGIC list1_logic_decl
    { LogicDecl $2 }
| INDUCTIVE list1_inductive_decl
    { IndDecl $2 }
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
| 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) }
| NAMESPACE uident list0_decl END
    { Namespace (loc (), false, Some $2, $3) }
| NAMESPACE UNDERSCORE list0_decl END
    { Namespace (loc (), false, None, $3) }
| NAMESPACE IMPORT uident list0_decl END
152
    { Namespace (loc (), true, Some $3, $4) }
153
| NAMESPACE IMPORT UNDERSCORE list0_decl END
154
    { Namespace (loc (), true, None, $4) }
155 156
| META ident list1_meta_arg_sep_comma
    { Meta (loc (), $2, $3) }
157 158
| 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
159 160
;

161 162 163 164 165 166 167 168 169
/* 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
170 171
;

172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194
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 }
;

195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
/* 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 }
;

210 211 212
/* Type declarations */

list1_type_decl:
213 214
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
215 216 217
;

type_decl:
218 219
| 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
220 221
;

222
type_args:
223 224
| /* epsilon */      { [] }
| type_var type_args { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225 226 227
;

typedefn:
228 229 230 231
| /* 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
232 233 234 235 236 237 238 239
;

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

typecase:
240 241 242 243 244 245
| uident params   { (loc_i 1,$1,$2) }
;

/* Logic declarations */

list1_logic_decl:
246 247
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
248 249 250
;

logic_decl:
251 252 253
| lident_rich params logic_type_option logic_def_option
  { { ld_loc = loc (); ld_ident = $1; ld_params = $2;
      ld_type = $3; ld_def = $4; } }
254 255 256 257 258 259 260 261 262 263
;

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
264 265
;

266 267 268
/* Inductive declarations */

list1_inductive_decl:
269 270
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
271 272 273
;

inductive_decl:
274 275
| lident_rich params inddefn
  { { in_loc = loc (); in_ident = $1; in_params = $2; in_def = $3 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
276
;
277

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
278 279 280 281 282 283 284 285 286 287 288
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315
/* 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
316
   { PPTtyapp ([], $1) }
317 318 319 320
| type_var
   { PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
321 322 323 324 325 326
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
327 328 329 330 331
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

332 333
type_var:
| QUOTE ident { $2 }
334 335
;

336 337
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
338
lexpr:
339
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
340
   { infix_pp $1 PPimplies $3 }
341
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
342
   { infix_pp $1 PPiff $3 }
343
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
344
   { infix_pp $1 PPor $3 }
345 346
| lexpr ASYM_OR lexpr
   { mk_pp (PPnamed ("asym_split", infix_pp $1 PPor $3)) }
347
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
348
   { infix_pp $1 PPand $3 }
349 350
| lexpr ASYM_AND lexpr
   { mk_pp (PPnamed ("asym_split", infix_pp $1 PPand $3)) }
351
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
352
   { prefix_pp PPnot $2 }
353
| lexpr EQUAL lexpr
354
   { let id = { id = infix "="; id_loc = loc_i 2 } in
355
     mk_pp (PPinfix ($1, id, $3)) }
356 357 358
| lexpr LTGT lexpr
   { let id = { id = infix "="; id_loc = loc_i 2 } in
     prefix_pp PPnot (mk_pp (PPinfix ($1, id, $3))) }
359
| lexpr OP1 lexpr
360
   { let id = { id = infix $2; id_loc = loc_i 2 } in
361
     mk_pp (PPinfix ($1, id, $3)) }
362
| lexpr OP2 lexpr
363
   { let id = { id = infix $2; id_loc = loc_i 2 } in
364
     mk_pp (PPinfix ($1, id, $3)) }
365
| lexpr OP3 lexpr
366
   { let id = { id = infix $2; id_loc = loc_i 2 } in
367
     mk_pp (PPinfix ($1, id, $3)) }
368
| lexpr OP4 lexpr
369
   { let id = { id = infix $2; id_loc = loc_i 2 } in
370
     mk_pp (PPinfix ($1, id, $3)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
371
| any_op lexpr %prec prefix_op
372 373
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }
374 375
| qualid list1_lexpr_arg
   { mk_pp (PPapp ($1, $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
376
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
377
   { mk_pp (PPif ($2, $4, $6)) }
378
| FORALL list1_param_var_sep_comma triggers DOT lexpr
379
   { mk_pp (PPquant (PPforall, $2, $3, $5)) }
380
| EXISTS list1_param_var_sep_comma triggers DOT lexpr
381
   { mk_pp (PPquant (PPexists, $2, $3, $5)) }
382 383
| STRING lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
384
| LET pattern EQUAL lexpr IN lexpr
385 386
   { match $2.pat_desc with
       | PPpvar id -> mk_pp (PPlet (id, $4, $6))
Andrei Paskevich's avatar
Andrei Paskevich committed
387 388
       | _ -> mk_pp (PPmatch ($4, [$2, $6])) }
| MATCH lexpr WITH bar_ match_cases END
389
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
390 391
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
   { mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
392 393
| EPSILON lident COLON primitive_type DOT lexpr
   { mk_pp (PPeps ($2, $4, $6)) }
394
| lexpr COLON primitive_type
395
   { mk_pp (PPcast ($1, $3)) }
396
| lexpr_arg
397 398 399
   { $1 }
;

400 401 402
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
403
;
404

405 406 407
lexpr_arg:
| qualid
   { mk_pp (PPvar $1) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
408
| INTEGER
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
409
   { mk_pp (PPconst (Term.ConstInt $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410
| FLOAT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
411
   { mk_pp (PPconst (Term.ConstReal $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412 413 414
| TRUE
   { mk_pp PPtrue }
| FALSE
415
   { mk_pp PPfalse }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
416 417
| LEFTPAR lexpr RIGHTPAR
   { $2 }
418 419 420 421
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
422 423 424
| 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
425
;
426

427
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
428

429 430 431 432
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
433

434 435 436 437 438 439 440 441 442 443 444 445 446 447 448
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 */
449

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
450 451 452 453 454 455
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
456
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
457 458 459
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478
| 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)) }
;
479

480
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
481 482 483
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
484

485
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
486 487 488 489 490
| 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
491 492
;

493
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
494

495 496 497
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
498 499
;

500 501 502 503 504 505 506 507 508 509 510 511 512
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
513 514
;

515 516 517 518 519 520 521 522
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
523 524
;

525 526 527 528
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
529 530
;

531 532 533
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
534 535
;

536 537 538
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
539 540
;

541
list1_lident:
542 543
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
544 545
;

546 547 548 549 550
/* Idents */

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

553 554 555
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
556 557
;

558 559 560 561 562 563 564 565 566 567 568
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
569 570
;

571 572
lident:
| LIDENT  { { id = $1; id_loc = loc () } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
573 574
;

575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619
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
620
;
621 622 623 624

qualid:
| ident_rich             { Qident $1 }
| uqualid DOT ident_rich { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
625
;
626 627 628 629 630 631

/* Misc */

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