parser.mly 14.2 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 49
  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
50 51
%}

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

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

/* keywords */

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

/* symbols */

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

%token EOF

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
82 83 84

/* Precedences */

Andrei Paskevich's avatar
Andrei Paskevich committed
85 86
%nonassoc prec_decls
%nonassoc LOGIC TYPE INDUCTIVE
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87

88
%nonassoc DOT ELSE IN
89
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90

Andrei Paskevich's avatar
Andrei Paskevich committed
91
%nonassoc prec_named
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
92
%right ARROW LRARROW
93 94
%right OR ASYM_OR
%right AND ASYM_AND
Andrei Paskevich's avatar
Andrei Paskevich committed
95
%nonassoc NOT
96
%left EQUAL OP1
97
%left OP2
98
%left OP3
99
%left OP4
Andrei Paskevich's avatar
Andrei Paskevich committed
100
%nonassoc prefix_op
101
%nonassoc OPPREF
102

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
103 104 105 106
/* Entry points */

%type <Ptree.lexpr> lexpr
%start lexpr
107 108
%type <Ptree.decl list> list0_decl
%start list0_decl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
109 110 111 112
%type <Ptree.logic_file> logic_file
%start logic_file
%%

113
/* File, theory, declaration */
114

115 116 117
logic_file:
| list1_theory EOF  { $1 }
| EOF               { [] }
118 119
;

120 121 122
list1_theory:
| theory                { [$1] }
| theory list1_theory   { $1 :: $2 }
123 124
;

125 126 127
theory:
| THEORY uident list0_decl END
   { { pt_loc = loc (); pt_name = $2; pt_decl = $3 } }
128 129
;

130 131 132
list0_decl:
| /* epsilon */    { [] }
| decl list0_decl  { $1 :: $2 }
133 134 135
;

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

166 167 168 169 170 171 172 173 174
/* 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
175 176
;

177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
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 }
;

200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
/* 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 }
;

215 216 217 218 219 220 221 222 223 224
/* Type declarations */

list1_type_decl:
| type_decl                  %prec prec_decls { [$1] }
| type_decl list1_type_decl                   { $1 :: $2 }
;

type_decl:
| TYPE lident type_args typedefn
  { { td_loc = loc (); td_ident = $2; td_params = $3; td_def = $4 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225 226
;

227
type_args:
228 229
| /* epsilon */      { [] }
| type_var type_args { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
230 231 232
;

typedefn:
233 234 235 236
| /* 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
237 238 239 240 241 242 243 244
;

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

typecase:
245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268
| uident params   { (loc_i 1,$1,$2) }
;

/* Logic declarations */

list1_logic_decl:
| logic_decl                  %prec prec_decls { [$1] }
| logic_decl list1_logic_decl                  { $1 :: $2 }
;

logic_decl:
| LOGIC lident_rich params logic_type_option logic_def_option
  { { ld_loc = loc (); ld_ident = $2; ld_params = $3;
      ld_type = $4; ld_def = $5; } }
;

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
269 270
;

271 272 273 274 275 276 277 278 279 280 281
/* Inductive declarations */

list1_inductive_decl:
| inductive_decl                      %prec prec_decls { [$1] }
| inductive_decl list1_inductive_decl                  { $1 :: $2 }
;

inductive_decl:
| INDUCTIVE lident_rich params inddefn
  { { in_loc = loc (); in_ident = $2; in_params = $3; in_def = $4 } }

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

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331 332 333 334 335
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

336 337
type_var:
| QUOTE ident { $2 }
338 339
;

340 341
/* Logic expressions */

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

399 400 401 402
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }

403 404 405
lexpr_arg:
| qualid
   { mk_pp (PPvar $1) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
406
| INTEGER
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
407
   { mk_pp (PPconst (Term.ConstInt $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
408
| FLOAT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
409
   { mk_pp (PPconst (Term.ConstReal $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410 411 412
| TRUE
   { mk_pp PPtrue }
| FALSE
413
   { mk_pp PPfalse }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
414 415
| LEFTPAR lexpr RIGHTPAR
   { $2 }
416 417 418 419
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
420 421 422 423
| OPPREF lexpr_arg
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }

424
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
425

426 427 428 429
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
430

431 432 433 434 435 436 437 438 439 440 441 442 443 444 445
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 */
446

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

match_case:
453
| list1_pat_sep_comma ARROW lexpr { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
454 455
;

Andrei Paskevich's avatar
Andrei Paskevich committed
456 457 458 459
list1_pat_sep_comma:
| pattern                           { [$1] }
| pattern COMMA list1_pat_sep_comma { $1::$3 }

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
460
pattern:
461 462 463 464
| pat_arg               { $1 }
| uqualid list1_pat_arg { mk_pat (PPpapp ($1, $2)) }
| pattern AS lident     { mk_pat (PPpas ($1,$3)) }

465 466 467 468
list1_pat_arg:
| pat_arg               { [$1] }
| pat_arg list1_pat_arg { $1::$2 }

469
pat_arg:
470 471 472 473 474 475 476 477 478 479 480 481
| UNDERSCORE
   { mk_pat (PPpwild) }
| lident
   { mk_pat (PPpvar $1) }
| uqualid
   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR pattern RIGHTPAR
   { $2 }
| LEFTPAR RIGHTPAR
   { mk_pat (PPptuple []) }
| LEFTPAR pattern COMMA list1_pat_sep_comma RIGHTPAR
   { mk_pat (PPptuple ($2 :: $4)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
482 483
;

484
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
485

486 487 488
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
489 490
;

491 492 493 494 495 496 497 498 499 500 501 502 503
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
504 505
;

506 507 508 509 510 511 512 513
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
514 515
;

516 517 518 519
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
520 521
;

522 523 524
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
525 526
;

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

532
list1_lident:
533 534
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
535 536
;

537 538 539 540 541
/* Idents */

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

544 545 546
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
547 548
;

549 550 551 552 553 554 555 556 557 558 559
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
560 561
;

562 563
lident:
| LIDENT  { { id = $1; id_loc = loc () } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
564 565
;

566 567 568 569 570 571 572 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 620
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) }

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

/* Misc */

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