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
;