MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

parser.mly 13.5 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
65
%token AND AS AXIOM CLONE
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET LOGIC MATCH NAMESPACE NOT PROP OR
Andrei Paskevich's avatar
Andrei Paskevich committed
66
%token THEN THEORY TRUE TYPE USE WITH
67
68
69

/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
70
%token ARROW
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
%right 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) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
160
161
;

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

173
174
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
200
201
202
203
204
205
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 }
;

/* 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
206
207
;

208
type_args:
209
210
| /* epsilon */      { [] }
| type_var type_args { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
211
212
213
;

typedefn:
214
215
216
217
| /* 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
218
219
220
221
222
223
224
225
;

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

typecase:
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
| 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
250
251
;

252
253
254
255
256
257
258
259
260
261
262
/* 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
263
264
265
266
267
268
269
270
271
272
273
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
/* 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
301
   { PPTtyapp ([], $1) }
302
303
304
305
| type_var
   { PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
306
307
308
309
310
311
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
312
313
314
315
316
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

317
318
type_var:
| QUOTE ident { $2 }
319
320
;

321
322
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
323
lexpr:
324
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
325
   { infix_pp $1 PPimplies $3 }
326
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
327
   { infix_pp $1 PPiff $3 }
328
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
329
   { infix_pp $1 PPor $3 }
330
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331
   { infix_pp $1 PPand $3 }
332
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
333
   { prefix_pp PPnot $2 }
334
| lexpr EQUAL lexpr
335
   { let id = { id = infix "="; id_loc = loc_i 2 } in
336
     mk_pp (PPinfix ($1, id, $3)) }
337
| lexpr OP1 lexpr
338
   { let id = { id = infix $2; id_loc = loc_i 2 } in
339
     mk_pp (PPinfix ($1, id, $3)) }
340
| lexpr OP2 lexpr
341
   { let id = { id = infix $2; id_loc = loc_i 2 } in
342
     mk_pp (PPinfix ($1, id, $3)) }
343
| lexpr OP3 lexpr
344
   { let id = { id = infix $2; id_loc = loc_i 2 } in
345
     mk_pp (PPinfix ($1, id, $3)) }
346
| lexpr OP4 lexpr
347
   { let id = { id = infix $2; id_loc = loc_i 2 } in
348
     mk_pp (PPinfix ($1, id, $3)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
349
| any_op lexpr %prec prefix_op
350
351
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }
352
353
| qualid list1_lexpr_arg
   { mk_pp (PPapp ($1, $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
354
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
355
   { mk_pp (PPif ($2, $4, $6)) }
356
| FORALL list1_param_var_sep_comma triggers DOT lexpr
357
   { mk_pp (PPquant (PPforall, $2, $3, $5)) }
358
| EXISTS list1_param_var_sep_comma triggers DOT lexpr
359
   { mk_pp (PPquant (PPexists, $2, $3, $5)) }
360
361
| STRING lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
362
| LET pattern EQUAL lexpr IN lexpr
363
364
365
366
367
368
369
   { 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)) }
370
| lexpr COLON primitive_type
371
   { mk_pp (PPcast ($1, $3)) }
372
| lexpr_arg
373
374
375
   { $1 }
;

376
377
378
379
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }

380
381
382
lexpr_arg:
| qualid
   { mk_pp (PPvar $1) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
383
| INTEGER
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
384
   { mk_pp (PPconst (Term.ConstInt $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
385
| FLOAT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
386
   { mk_pp (PPconst (Term.ConstReal $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
387
388
389
| TRUE
   { mk_pp PPtrue }
| FALSE
390
   { mk_pp PPfalse }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
391
392
| LEFTPAR lexpr RIGHTPAR
   { $2 }
393
394
395
396
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
397
398
399
400
| OPPREF lexpr_arg
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }

401
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
402

403
404
405
406
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
407

408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
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 */
423

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
424
425
426
427
428
429
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
433
434
435
436
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
437
pattern:
438
439
440
441
| pat_arg               { $1 }
| uqualid list1_pat_arg { mk_pat (PPpapp ($1, $2)) }
| pattern AS lident     { mk_pat (PPpas ($1,$3)) }

442
443
444
445
list1_pat_arg:
| pat_arg               { [$1] }
| pat_arg list1_pat_arg { $1::$2 }

446
pat_arg:
447
448
449
450
451
452
453
454
455
456
457
458
| 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
459
460
;

461
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
462

463
464
465
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
466
467
;

468
469
470
471
472
473
474
475
476
477
478
479
480
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
481
482
;

483
484
485
486
487
488
489
490
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
491
492
;

493
494
495
496
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
497
498
;

499
500
501
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
502
503
;

504
505
506
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
507
508
;

509
list1_lident:
510
511
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
512
513
;

514
515
516
517
518
/* Idents */

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

521
522
523
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
524
525
;

526
527
528
529
530
531
532
533
534
535
536
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
537
538
;

539
540
lident:
| LIDENT  { { id = $1; id_loc = loc () } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
541
542
;

543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
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
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
598
599
;