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 13.1 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
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

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

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

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

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

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

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

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

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

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

159
lident_op:
160
| OP1   { $1 }
161
162
| OP2   { $1 }
| OP3   { $1 }
163
| STAR  { "*" }
164
| OP4   { $1 }
165
166
| EQUAL { "=" }
;
167

168
any_op:
169
| OP1   { $1 }
170
171
| OP2   { $1 }
| OP3   { $1 }
172
| STAR  { "*" }
173
| OP4   { $1 }
174
;
175

176
177
178
179
180
181
182
183
184
185
186
187
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) }
188
189
;

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

195
196
197
198
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }

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

203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
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 }
;

218
219
220
221
primitive_types:
| /* epsilon */                                   { [] }
| LEFTPAR list1_primitive_type_sep_comma RIGHTPAR { $2 }

222
223
224
225
226
227
228
229
230
231
232
logic_type_option:
| /* epsilon */        { None }
| COLON primitive_type { Some $2 }
;

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

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

list1_logic_decl:
239
240
| logic_decl                  %prec prec_decls { [$1] }
| logic_decl list1_logic_decl                  { $1 :: $2 }
241
242
243
;

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

list1_type_decl:
249
| type_decl                  %prec prec_decls { [$1] }
250
251
252
| type_decl list1_type_decl                   { $1 :: $2 }
;

253
inductive_decl:
254
| INDUCTIVE lident_rich primitive_types inddefn
255
256
257
258
259
260
261
262
  { { 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:
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
| 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
284
    { Namespace (loc (), true, Some $3, $4) }
285
| NAMESPACE IMPORT UNDERSCORE list0_decl END
286
    { Namespace (loc (), true, None, $4) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
287
288
;

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

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

301
302
303
304
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
305
306
307
308
;

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

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

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

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

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

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

341
simple_primitive_type:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
342
| type_var 
343
   { PPTtyvar $1 }
344
| lqualid
345
   { PPTtyapp ([], $1) }
346
| simple_primitive_type lqualid
347
   { PPTtyapp ([$1], $2) }
348
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR lqualid
349
   { PPTtyapp ($2 :: $4, $6) }
350
351
352
353
354
355
356
357
358
359
360
| 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
361
362
363
364
365
366
367
;

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

368
369
370
371
372
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
373
374
375
376
377
378
379
380
381
382
383
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 }
384
| lexpr EQUAL lexpr 
385
   { let id = { id = infix "="; id_loc = loc_i 2 } in
386
     mk_pp (PPinfix ($1, id, $3)) }
387
388
| lexpr OP1 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
389
     mk_pp (PPinfix ($1, id, $3)) }
390
391
| lexpr OP2 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
392
     mk_pp (PPinfix ($1, id, $3)) }
393
394
| lexpr OP3 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
395
     mk_pp (PPinfix ($1, id, $3)) }
396
397
398
| lexpr STAR lexpr 
   { let id = { id = infix "*"; id_loc = loc_i 2 } in
     mk_pp (PPinfix ($1, id, $3)) }
399
400
| lexpr OP4 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
401
     mk_pp (PPinfix ($1, id, $3)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
402
| any_op lexpr %prec prefix_op
403
404
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }
405
| qualid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
406
   { mk_pp (PPvar $1) }
407
| qualid LEFTPAR list1_lexpr_sep_comma RIGHTPAR
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
408
   { mk_pp (PPapp ($1, $3)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
409
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410
   { mk_pp (PPif ($2, $4, $6)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
411
| FORALL list1_uquant_sep_comma triggers DOT lexpr
412
   { mk_pp (PPquant (PPforall, $2, $3, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
413
| EXISTS list1_uquant_sep_comma triggers DOT lexpr
414
   { mk_pp (PPquant (PPexists, $2, $3, $5)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
415
| INTEGER
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
416
   { mk_pp (PPconst (Term.ConstInt $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
417
| FLOAT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
418
   { mk_pp (PPconst (Term.ConstReal $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
419
420
421
422
423
424
| TRUE
   { mk_pp PPtrue }
| FALSE
   { mk_pp PPfalse }    
| LEFTPAR lexpr RIGHTPAR
   { $2 }
425
426
427
428
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429
430
| STRING lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
431
432
433
434
| 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])) }
435
| MATCH list1_lexpr_sep_comma WITH bar_ match_cases END
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
436
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
437
438
| EPSILON lident COLON primitive_type DOT lexpr
   { mk_pp (PPeps ($2, $4, $6)) }
439
| lexpr COLON simple_primitive_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
440
   { mk_pp (PPcast ($1, $3)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
441
442
;

443
444
445
446
447
448
449
list1_uquant_sep_comma:
| uquant                              { [$1] }
| uquant COMMA list1_uquant_sep_comma { $1::$3 }

uquant:
| list1_lident_sep_comma COLON primitive_type { $1,$3 }

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:
456
| list1_pat_sep_comma ARROW lexpr { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
457
458
;

Andrei Paskevich's avatar
Andrei Paskevich committed
459
460
461
462
list1_pat_sep_comma:
| pattern                           { [$1] }
| pattern COMMA list1_pat_sep_comma { $1::$3 }

463
464
465
466
list1_pat_arg:
| pat_arg               { [$1] }
| pat_arg list1_pat_arg { $1::$2 }

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
467
pattern:
468
469
470
471
472
| 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
473
474
475
| UNDERSCORE                                    { mk_pat (PPpwild) }
| lident                                        { mk_pat (PPpvar $1) }
| uqualid                                       { mk_pat (PPpapp ($1, [])) }
Andrei Paskevich's avatar
Andrei Paskevich committed
476
| LEFTPAR pattern RIGHTPAR                      { $2 }
477
478
479
| 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
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
;

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           { () }
;

515
516
517
518
519
list1_lident_sep_comma:
| lident                              { [$1] }
| lident COMMA list1_lident_sep_comma { $1 :: $3 }
;

520
use:
521
| imp_exp tqualid              
522
    { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
523
| imp_exp tqualid AS uident
524
525
526
    { { 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
527
528
;

529
530
531
532
imp_exp:
| IMPORT        { Import }
| EXPORT        { Export }
| /* epsilon */ { Nothing }
533
534
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
535
clone_subst:
536
537
| /* epsilon */          { [] } 
| WITH list1_comma_subst { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
538
539
540
;

list1_comma_subst:
541
542
| subst                         { [$1] }
| subst COMMA list1_comma_subst { $1 :: $3 } 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
543
544
545
;

subst:
546
547
548
549
| 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
550
551
;