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.3 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
32

%{

  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
		    
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
53
%}

/* Tokens */ 

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 */

Andrei Paskevich's avatar
Andrei Paskevich committed
62
63
64
65
66
%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 OR  
%token THEN THEORY TRUE TYPE USE WITH
67
68
69

/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
70
71
%token ARROW
%token BAR 
72
%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 STAR
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
Andrei Paskevich's avatar
Andrei Paskevich committed
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 STAR
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
113
%type <Ptree.logic_file> logic_file
%start logic_file
%%

logic_file:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114
115
| list1_theory EOF
   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116
117
118
119
120
121
122
123
124
125
126
| EOF 
   { [] }
;

list1_decl:
| decl 
   { [$1] }
| decl list1_decl 
   { $1 :: $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
127
128
129
130
131
132
133
list0_decl:
| /* epsilon */
   { [] }
| list1_decl 
   { $1 }
;

134
ident:
135
136
137
138
139
140
141
| uident { $1 }
| lident { $1 }
;

ident_rich:
| uident      { $1 }
| lident_rich { $1 }
142
143
;

144
lident:
145
| LIDENT
146
147
148
    { { id = $1; id_loc = loc () } }
;

149
150
lident_rich:
| lident
151
    { $1 }
152
153
154
155
| LEFTPAR lident_op RIGHTPAR 
    { { id = infix $2; id_loc = loc () } }
| LEFTPAR_STAR_RIGHTPAR
    { { id = infix "*"; id_loc = loc () } }
156
| LEFTPAR lident_op UNDERSCORE RIGHTPAR 
157
    { { id = prefix $2; id_loc = loc () } }
158
159
| LEFTPAR OPPREF RIGHTPAR 
    { { id = prefix $2; id_loc = loc () } }
160
161
;

162
lident_op:
163
| OP1   { $1 }
164
165
| OP2   { $1 }
| OP3   { $1 }
166
| STAR  { "*" }
167
| OP4   { $1 }
168
169
| EQUAL { "=" }
;
170

171
any_op:
172
| OP1   { $1 }
173
174
| OP2   { $1 }
| OP3   { $1 }
175
| STAR  { "*" }
176
| OP4   { $1 }
177
;
178

179
180
181
182
183
184
185
186
187
188
189
190
uident:
| UIDENT { { id = $1; id_loc = loc () } }
;

lqualid:
| lident             { Qident $1 }
| uqualid DOT lident { Qdot ($1, $3) }
;

uqualid:
| uident             { Qident $1 }
| uqualid DOT uident { Qdot ($1, $3) }
191
192
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193
194
195
any_qualid:
| ident                { Qident $1 }
| any_qualid DOT ident { Qdot ($1, $3) }
196
197
;

198
199
200
201
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }

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

206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
params:
| /* epsilon */                          { [] }
| LEFTPAR list1_param_sep_comma RIGHTPAR { $2 }
;

param:
| primitive_type              { None, $1 }
| lident COLON primitive_type { Some $1, $3 }
;

list1_param_sep_comma:
| param                             { [$1] }
| param COMMA list1_param_sep_comma { $1 :: $3 }
;

221
222
223
224
primitive_types:
| /* epsilon */                                   { [] }
| LEFTPAR list1_primitive_type_sep_comma RIGHTPAR { $2 }

225
226
227
228
229
230
231
232
233
234
235
logic_type_option:
| /* epsilon */        { None }
| COLON primitive_type { Some $2 }
;

logic_def_option:
| /* epsilon */ { None }
| EQUAL lexpr   { Some $2 }
;

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

list1_logic_decl:
242
243
| logic_decl                  %prec prec_decls { [$1] }
| logic_decl list1_logic_decl                  { $1 :: $2 }
244
245
246
;

type_decl:
247
248
| TYPE type_args lident typedefn
  { { td_loc = loc (); td_ident = $3; td_params = $2; td_def = $4 } }
249
250
251
;

list1_type_decl:
252
| type_decl                  %prec prec_decls { [$1] }
253
254
255
| type_decl list1_type_decl                   { $1 :: $2 }
;

256
inductive_decl:
257
| INDUCTIVE lident_rich primitive_types inddefn
258
259
260
261
262
263
264
265
  { { in_loc = loc (); in_ident = $2; in_params = $3; in_def = $4 } }

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

decl:
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
| 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
287
    { Namespace (loc (), true, Some $3, $4) }
288
| NAMESPACE IMPORT UNDERSCORE list0_decl END
289
    { Namespace (loc (), true, None, $4) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
290
291
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
292
293
294
295
296
297
298
299
list1_theory:
| theory 
   { [$1] }
| theory list1_theory 
   { $1 :: $2 }
;

theory:
300
| THEORY uident list0_decl END 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
301
   { { pt_loc = loc (); pt_name = $2; pt_decl = $3 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
302
303
;

304
305
306
307
type_args:
| /* epsilon */                                             { [] }
| type_var                                                  { [$1] }
| LEFTPAR type_var COMMA list1_type_var_sep_comma RIGHTPAR  { $2 :: $4 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
308
309
310
311
;

typedefn:
| /* epsilon */
312
313
314
    { TDabstract }
| EQUAL primitive_type
    { TDalias $2 }
315
316
317
| EQUAL typecases
    { TDalgebraic $2 }
| EQUAL BAR typecases
318
    { TDalgebraic $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
319
320
321
322
323
324
325
326
;

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

typecase:
327
| uident primitive_types { (loc_i 1,$1,$2) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
328
329
330
331
332
333
334
335
336
337
338
339
340
;

inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

344
simple_primitive_type:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
345
| type_var 
346
   { PPTtyvar $1 }
347
| lqualid
348
   { PPTtyapp ([], $1) }
349
| simple_primitive_type lqualid
350
   { PPTtyapp ([$1], $2) }
351
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR lqualid
352
   { PPTtyapp ($2 :: $4, $6) }
353
354
355
356
357
358
359
360
361
362
363
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

primitive_type:
| simple_primitive_type 
    { $1 }
| simple_primitive_type STAR list1_simple_primitive_type_sep_star 
   { PPTtuple ($1 :: $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
364
365
366
367
368
369
370
;

list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

371
372
373
374
375
list1_simple_primitive_type_sep_star:
| simple_primitive_type                                           { [$1] }
| simple_primitive_type STAR list1_simple_primitive_type_sep_star { $1 :: $3 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
376
377
378
379
380
381
382
383
384
385
386
lexpr:
| lexpr ARROW lexpr 
   { infix_pp $1 PPimplies $3 }
| lexpr LRARROW lexpr 
   { infix_pp $1 PPiff $3 }
| lexpr OR lexpr 
   { infix_pp $1 PPor $3 }
| lexpr AND lexpr 
   { infix_pp $1 PPand $3 }
| NOT lexpr 
   { prefix_pp PPnot $2 }
387
| lexpr EQUAL lexpr 
388
   { let id = { id = infix "="; id_loc = loc_i 2 } in
389
     mk_pp (PPinfix ($1, id, $3)) }
390
391
| lexpr OP1 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
392
     mk_pp (PPinfix ($1, id, $3)) }
393
394
| lexpr OP2 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
395
     mk_pp (PPinfix ($1, id, $3)) }
396
397
| lexpr OP3 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
398
     mk_pp (PPinfix ($1, id, $3)) }
399
400
401
| lexpr STAR lexpr 
   { let id = { id = infix "*"; id_loc = loc_i 2 } in
     mk_pp (PPinfix ($1, id, $3)) }
402
403
| lexpr OP4 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
404
     mk_pp (PPinfix ($1, id, $3)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
405
| any_op lexpr %prec prefix_op
406
407
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }
408
409
| qualid list1_lexpr_arg
   { mk_pp (PPapp ($1, $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
410
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
411
   { mk_pp (PPif ($2, $4, $6)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
412
| FORALL list1_uquant_sep_comma triggers DOT lexpr
413
   { mk_pp (PPquant (PPforall, $2, $3, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
414
| EXISTS list1_uquant_sep_comma triggers DOT lexpr
415
   { mk_pp (PPquant (PPexists, $2, $3, $5)) }
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
| STRING lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
| LET pattern EQUAL lexpr IN lexpr 
   { 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)) }
| lexpr COLON simple_primitive_type
   { mk_pp (PPcast ($1, $3)) }
| lexpr_arg 
   { $1 }
;

lexpr_arg:
| qualid
   { mk_pp (PPvar $1) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
435
| INTEGER
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
436
   { mk_pp (PPconst (Term.ConstInt $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
437
| FLOAT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
438
   { mk_pp (PPconst (Term.ConstReal $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
439
440
441
442
443
444
| TRUE
   { mk_pp PPtrue }
| FALSE
   { mk_pp PPfalse }    
| LEFTPAR lexpr RIGHTPAR
   { $2 }
445
446
447
448
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
449
450
451
452
453
454
455
| OPPREF lexpr_arg
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }

list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456

457
458
459
460
461
list1_uquant_sep_comma:
| uquant                              { [$1] }
| uquant COMMA list1_uquant_sep_comma { $1::$3 }

uquant:
462
| list1_lident COLON primitive_type { $1,$3 }
463

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
464
465
466
467
468
469
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
473
474
475
476
list1_pat_sep_comma:
| pattern                           { [$1] }
| pattern COMMA list1_pat_sep_comma { $1::$3 }

477
478
479
480
list1_pat_arg:
| pat_arg               { [$1] }
| pat_arg list1_pat_arg { $1::$2 }

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
481
pattern:
482
483
484
485
486
| pat_arg               { $1 }
| uqualid list1_pat_arg { mk_pat (PPpapp ($1, $2)) }
| pattern AS lident     { mk_pat (PPpas ($1,$3)) }

pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
487
488
489
| UNDERSCORE                                    { mk_pat (PPpwild) }
| lident                                        { mk_pat (PPpvar $1) }
| uqualid                                       { mk_pat (PPpapp ($1, [])) }
Andrei Paskevich's avatar
Andrei Paskevich committed
490
| LEFTPAR pattern RIGHTPAR                      { $2 }
491
492
493
| 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
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
;

triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;

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 }
;

type_var:
| QUOTE ident { $2 }
;

list1_type_var_sep_comma:
| type_var                                { [$1] }
| type_var COMMA list1_type_var_sep_comma { $1 :: $3 }
;

bar_:
| /* epsilon */ { () }
| BAR           { () }
;

529
530
531
list1_lident:
| lident              { [$1] }
| lident list1_lident { $1 :: $2 }
532
533
;

534
use:
535
| imp_exp tqualid              
536
    { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
537
| imp_exp tqualid AS uident
538
539
540
    { { 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
541
542
;

543
544
545
546
imp_exp:
| IMPORT        { Import }
| EXPORT        { Export }
| /* epsilon */ { Nothing }
547
548
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
549
clone_subst:
550
551
| /* epsilon */          { [] } 
| WITH list1_comma_subst { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
552
553
554
;

list1_comma_subst:
555
556
| subst                         { [$1] }
| subst COMMA list1_comma_subst { $1 :: $3 } 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
557
558
559
;

subst:
560
561
562
563
| TYPE  qualid EQUAL qualid { CStsym ($2, $4) }
| LOGIC qualid EQUAL qualid { CSlsym ($2, $4) }
| LEMMA qualid              { CSlemma $2 }
| GOAL  qualid              { CSgoal  $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
564
565
;