parser.mly 11.9 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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
44
45
46
47
%}

/* Tokens */ 

48
%token <string> LIDENT UIDENT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
49
%token <string> INTEGER
50
%token <string> OP1 OP2 OP3 OP4
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
51
52
%token <Ptree.real_constant> FLOAT
%token <string> STRING
53
54
55

/* keywords */

Andrei Paskevich's avatar
Andrei Paskevich committed
56
57
58
59
60
%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
61
62
63

/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
64
65
%token ARROW
%token BAR 
66
%token COLON COMMA  
67
%token DOT EQUAL
68
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ 
69
%token LRARROW
Andrei Paskevich's avatar
Andrei Paskevich committed
70
%token QUOTE
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
71
%token RIGHTPAR RIGHTSQ 
72
73
74
75
%token UNDERSCORE

%token EOF

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76
77
78

/* Precedences */

Andrei Paskevich's avatar
Andrei Paskevich committed
79
80
%nonassoc prec_decls
%nonassoc LOGIC TYPE INDUCTIVE
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
81

82
%nonassoc DOT ELSE IN
Andrei Paskevich's avatar
Andrei Paskevich committed
83
%nonassoc COLON 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84

Andrei Paskevich's avatar
Andrei Paskevich committed
85
%nonassoc prec_named
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86
%right ARROW LRARROW
87
88
%right OR 
%right AND 
Andrei Paskevich's avatar
Andrei Paskevich committed
89
%nonassoc NOT
90
%left EQUAL OP1
91
92
%left OP2
%left OP3
93
%left OP4
Andrei Paskevich's avatar
Andrei Paskevich committed
94
%nonassoc prefix_op
95

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96
97
98
99
/* Entry points */

%type <Ptree.lexpr> lexpr
%start lexpr
100
101
%type <Ptree.decl list> list0_decl
%start list0_decl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
102
103
104
105
106
%type <Ptree.logic_file> logic_file
%start logic_file
%%

logic_file:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107
108
| list1_theory EOF
   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
109
110
111
112
113
114
115
116
117
118
119
| EOF 
   { [] }
;

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
120
121
122
123
124
125
126
list0_decl:
| /* epsilon */
   { [] }
| list1_decl 
   { $1 }
;

127
ident:
128
129
130
131
132
133
134
| uident { $1 }
| lident { $1 }
;

ident_rich:
| uident      { $1 }
| lident_rich { $1 }
135
136
;

137
lident:
138
| LIDENT
139
140
141
    { { id = $1; id_loc = loc () } }
;

142
143
lident_rich:
| lident
144
    { $1 }
145
146
147
148
| LEFTPAR lident_op RIGHTPAR 
    { { id = infix $2; id_loc = loc () } }
| LEFTPAR_STAR_RIGHTPAR
    { { id = infix "*"; id_loc = loc () } }
149
| LEFTPAR lident_op UNDERSCORE RIGHTPAR 
150
    { { id = prefix $2; id_loc = loc () } }
151
152
;

153
lident_op:
154
| OP1   { $1 }
155
156
| OP2   { $1 }
| OP3   { $1 }
157
| OP4   { $1 }
158
159
| EQUAL { "=" }
;
160

161
any_op:
162
| OP1   { $1 }
163
164
| OP2   { $1 }
| OP3   { $1 }
165
| OP4   { $1 }
166
;
167

168
169
170
171
172
173
174
175
176
177
178
179
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) }
180
181
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
182
183
184
any_qualid:
| ident                { Qident $1 }
| any_qualid DOT ident { Qdot ($1, $3) }
185
186
;

187
188
189
190
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }

191
qualid:
192
193
| ident_rich             { Qident $1 }
| uqualid DOT ident_rich { Qdot ($1, $3) }
194

195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
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 }
;

210
211
212
213
primitive_types:
| /* epsilon */                                   { [] }
| LEFTPAR list1_primitive_type_sep_comma RIGHTPAR { $2 }

214
215
216
217
218
219
220
221
222
223
224
logic_type_option:
| /* epsilon */        { None }
| COLON primitive_type { Some $2 }
;

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

logic_decl:
225
| LOGIC lident_rich params logic_type_option logic_def_option
226
227
  { { ld_loc = loc (); ld_ident = $2; ld_params = $3; 
      ld_type = $4; ld_def = $5; } }
228
229
230
;

list1_logic_decl:
231
232
| logic_decl                  %prec prec_decls { [$1] }
| logic_decl list1_logic_decl                  { $1 :: $2 }
233
234
235
;

type_decl:
236
237
| TYPE type_args lident typedefn
  { { td_loc = loc (); td_ident = $3; td_params = $2; td_def = $4 } }
238
239
240
;

list1_type_decl:
241
| type_decl                  %prec prec_decls { [$1] }
242
243
244
| type_decl list1_type_decl                   { $1 :: $2 }
;

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
281
282
283
284
285
286
287
288
list1_theory:
| theory 
   { [$1] }
| theory list1_theory 
   { $1 :: $2 }
;

theory:
289
| THEORY uident list0_decl END 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
290
   { { pt_loc = loc (); pt_name = $2; pt_decl = $3 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
291
292
;

293
294
295
296
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
297
298
299
300
;

typedefn:
| /* epsilon */
301
302
303
    { TDabstract }
| EQUAL primitive_type
    { TDalias $2 }
304
305
306
| EQUAL typecases
    { TDalgebraic $2 }
| EQUAL BAR typecases
307
    { TDalgebraic $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
308
309
310
311
312
313
314
315
;

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

typecase:
316
| uident primitive_types { (loc_i 1,$1,$2) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
317
318
319
320
321
322
323
324
325
326
327
328
329
;

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

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

indcase:
Andrei Paskevich's avatar
Andrei Paskevich committed
330
| uident COLON lexpr { (loc (),$1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331
332
333
334
;

primitive_type:
| type_var 
335
   { PPTtyvar $1 }
336
| lqualid
337
   { PPTtyapp ([], $1) }
338
| primitive_type lqualid
339
   { PPTtyapp ([$1], $2) }
340
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR lqualid
341
   { PPTtyapp ($2 :: $4, $6) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
;

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

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 }
360
| lexpr EQUAL lexpr 
361
   { let id = { id = infix "="; id_loc = loc_i 2 } in
362
     mk_pp (PPinfix ($1, id, $3)) }
363
364
| lexpr OP1 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
365
     mk_pp (PPinfix ($1, id, $3)) }
366
367
| lexpr OP2 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
368
     mk_pp (PPinfix ($1, id, $3)) }
369
370
| lexpr OP3 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
371
     mk_pp (PPinfix ($1, id, $3)) }
372
373
| lexpr OP4 lexpr 
   { let id = { id = infix $2; id_loc = loc_i 2 } in
374
     mk_pp (PPinfix ($1, id, $3)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
375
| any_op lexpr %prec prefix_op
376
377
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }
378
| qualid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
379
   { mk_pp (PPvar $1) }
380
| qualid LEFTPAR list1_lexpr_sep_comma RIGHTPAR
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
381
   { mk_pp (PPapp ($1, $3)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
382
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
383
   { mk_pp (PPif ($2, $4, $6)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
384
| FORALL list1_uquant_sep_comma triggers DOT lexpr
385
   { mk_pp (PPquant (PPforall, $2, $3, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
386
| EXISTS list1_uquant_sep_comma triggers DOT lexpr
387
   { mk_pp (PPquant (PPexists, $2, $3, $5)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
388
| INTEGER
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
389
   { mk_pp (PPconst (Term.ConstInt $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
390
| FLOAT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
391
   { mk_pp (PPconst (Term.ConstReal $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
392
393
394
395
396
397
| TRUE
   { mk_pp PPtrue }
| FALSE
   { mk_pp PPfalse }    
| LEFTPAR lexpr RIGHTPAR
   { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
398
399
| STRING lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
400
| LET lident EQUAL lexpr IN lexpr 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
401
   { mk_pp (PPlet ($2, $4, $6)) }
402
| MATCH list1_lexpr_sep_comma WITH bar_ match_cases END
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
403
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
404
405
| EPSILON lident COLON primitive_type DOT lexpr
   { mk_pp (PPeps ($2, $4, $6)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
406
407
| lexpr COLON primitive_type
   { mk_pp (PPcast ($1, $3)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
408
409
;

410
411
412
413
414
415
416
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
417
418
419
420
421
422
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
426
427
428
429
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
430
pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
431
432
433
434
435
| UNDERSCORE                                    { mk_pat (PPpwild) }
| lident                                        { mk_pat (PPpvar $1) }
| uqualid                                       { mk_pat (PPpapp ($1, [])) }
| uqualid LEFTPAR list1_pat_sep_comma RIGHTPAR  { mk_pat (PPpapp ($1, $3)) }
| pattern AS lident                             { mk_pat (PPpas ($1,$3)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
436
| LEFTPAR pattern RIGHTPAR                      { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
;

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

472
473
474
475
476
list1_lident_sep_comma:
| lident                              { [$1] }
| lident COMMA list1_lident_sep_comma { $1 :: $3 }
;

477
use:
478
| imp_exp tqualid              
479
    { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
480
| imp_exp tqualid AS uident
481
482
483
    { { 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
484
485
;

486
487
488
489
imp_exp:
| IMPORT        { Import }
| EXPORT        { Export }
| /* epsilon */ { Nothing }
490
491
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
492
clone_subst:
493
494
| /* epsilon */          { [] } 
| WITH list1_comma_subst { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
495
496
497
;

list1_comma_subst:
498
499
| subst                         { [$1] }
| subst COMMA list1_comma_subst { $1 :: $3 } 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
500
501
502
;

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