Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

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
;