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 15.8 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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
  open Theory

  let env_ref  = ref []
  let lenv_ref = ref []
  let uc_ref   = ref []

  let ref_get  ref = List.hd !ref
  let ref_tail ref = List.tl !ref
  let ref_drop ref = ref := ref_tail ref
  let ref_pop  ref = let v = ref_get ref in ref_drop ref; v

  let ref_push ref v = ref := v :: !ref
  let ref_set  ref v = ref := v :: ref_tail ref

  let inside_env env rule lexer lexbuf =
    ref_push env_ref env;
      ref_push lenv_ref Mnm.empty;
    let res = rule lexer lexbuf in
      ref_drop lenv_ref;
    ref_drop env_ref;
    res

  let inside_uc env lenv uc rule lexer lexbuf =
    ref_push env_ref env;
      ref_push lenv_ref lenv;
        ref_push uc_ref uc;
    let res = rule lexer lexbuf in
        ref_drop uc_ref;
      ref_drop lenv_ref;
    ref_drop env_ref;
    res
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52
53
54
55
56
57
58
59
60
61
62

  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
63

Andrei Paskevich's avatar
Andrei Paskevich committed
64
65
  let mk_pat p = { pat_loc = loc (); pat_desc = p }

66
  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
67
68
  let infix_pp a i b = infix_ppl (loc ()) a i b

69
  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
70
71
  let prefix_pp p a = prefix_ppl (loc ()) p a

72
73
74
  let infix s = "infix " ^ s
  let prefix s = "prefix " ^ s

75
76
77
78
79
  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
80
81
%}

82
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
83

84
%token <string> LIDENT UIDENT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85
%token <string> INTEGER
86
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87
88
%token <Ptree.real_constant> FLOAT
%token <string> STRING
89
90
91

/* keywords */

92
93
%token AND AS AXIOM CLONE
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
Andrei Paskevich's avatar
Andrei Paskevich committed
94
%token GOAL IF IMPORT IN INDUCTIVE LAMBDA LEMMA
95
%token LET LOGIC MATCH META NAMESPACE NOT PROP OR
Andrei Paskevich's avatar
Andrei Paskevich committed
96
%token THEN THEORY TRUE TYPE USE WITH
97
98
99

/* symbols */

100
%token ARROW ASYM_AND ASYM_OR
101
102
%token BAR
%token COLON COMMA
103
%token DOT EQUAL LTGT
104
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
105
%token LRARROW
Andrei Paskevich's avatar
Andrei Paskevich committed
106
%token QUOTE
107
%token RIGHTPAR RIGHTSQ
108
109
110
111
%token UNDERSCORE

%token EOF

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
112
113
/* Precedences */

114
%nonassoc DOT ELSE IN
115
%nonassoc prec_named
116
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
117
118

%right ARROW LRARROW
119
120
%right OR ASYM_OR
%right AND ASYM_AND
Andrei Paskevich's avatar
Andrei Paskevich committed
121
%nonassoc NOT
122
%left EQUAL LTGT OP1
123
%left OP2
124
%left OP3
125
%left OP4
Andrei Paskevich's avatar
Andrei Paskevich committed
126
%nonassoc prefix_op
127

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
128
129
/* Entry points */

130
131
132
133
134
135
%type <Ptree.lexpr> lexpr_eof
%start lexpr_eof
%type <Theory.theory_uc> list0_decl_eof
%start list0_decl_eof
%type <Theory.theory Theory.Mnm.t> logic_file_eof
%start logic_file_eof
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
136
137
%%

138
139
140
141
142
143
144
145
146
147
148
149
150
logic_file_eof:
| list0_theory EOF  { ref_get lenv_ref }
;

list0_decl_eof:
| list0_decl EOF  { ref_get uc_ref }
;

lexpr_eof:
| lexpr EOF  { $1 }
;

/* File, theory, namespace */
151

152
153
154
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
155
156
;

157
158
159
160
161
theory_head:
| THEORY uident
   { let id = $2 in
     let name = Ident.id_user id.id id.id_loc in
     ref_push uc_ref (create_theory name); id }
162
163
;

164
theory:
165
166
167
| theory_head list0_decl END
   { let uc = ref_pop uc_ref in
     ref_set lenv_ref (Typing.close_theory (ref_get lenv_ref) $1 uc) }
168
169
;

170
list0_decl:
171
172
173
174
175
176
177
178
179
180
| /* epsilon */        { () }
| new_decl list0_decl  { () }
;

new_decl:
| decl
   { let env = ref_get env_ref in let lenv = ref_get lenv_ref in
     ref_set uc_ref (Typing.add_decl env lenv (ref_get uc_ref) $1) }
| namespace_head namespace_import namespace_name list0_decl END
   { ref_set uc_ref (Typing.close_namespace (loc ()) $2 $3 (ref_get uc_ref)) }
181
182
;

183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
namespace_head:
| NAMESPACE
   { ref_set uc_ref (open_namespace (ref_get uc_ref)) }
;

namespace_import:
| /* epsilon */  { false }
| IMPORT         { true }
;

namespace_name:
| uident      { Some $1 }
| UNDERSCORE  { None }
;

/* Declaration */

200
decl:
201
202
203
204
205
206
| TYPE list1_type_decl
    { TypeDecl $2 }
| LOGIC list1_logic_decl
    { LogicDecl $2 }
| INDUCTIVE list1_inductive_decl
    { IndDecl $2 }
207
208
209
210
211
212
213
214
215
216
| 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) }
217
218
| META ident list1_meta_arg_sep_comma
    { Meta (loc (), $2, $3) }
219
220
| 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
221
222
;

223
224
225
226
227
228
229
230
231
/* 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
232
233
;

234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
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 }
;

257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
/* 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 }
;

272
273
274
/* Type declarations */

list1_type_decl:
275
276
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
277
278
279
;

type_decl:
280
281
| lident type_args typedefn
  { { td_loc = loc (); td_ident = $1; td_params = $2; td_def = $3 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282
283
;

284
type_args:
285
286
| /* epsilon */      { [] }
| type_var type_args { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
287
288
289
;

typedefn:
290
291
292
293
| /* 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
294
295
296
297
298
299
300
301
;

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

typecase:
302
303
304
305
306
307
| uident params   { (loc_i 1,$1,$2) }
;

/* Logic declarations */

list1_logic_decl:
308
309
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
310
311
312
;

logic_decl:
313
314
315
| lident_rich params logic_type_option logic_def_option
  { { ld_loc = loc (); ld_ident = $1; ld_params = $2;
      ld_type = $3; ld_def = $4; } }
316
317
318
319
320
321
322
323
324
325
;

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
326
327
;

328
329
330
/* Inductive declarations */

list1_inductive_decl:
331
332
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
333
334
335
;

inductive_decl:
336
337
| lident_rich params inddefn
  { { in_loc = loc (); in_ident = $1; in_params = $2; in_def = $3 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
338
;
339

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
340
341
342
343
344
345
346
347
348
349
350
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
/* 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
378
   { PPTtyapp ([], $1) }
379
380
381
382
| type_var
   { PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
383
384
385
386
387
388
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
389
390
391
392
393
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

394
395
type_var:
| QUOTE ident { $2 }
396
397
;

398
399
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
400
lexpr:
401
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
402
   { infix_pp $1 PPimplies $3 }
403
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
404
   { infix_pp $1 PPiff $3 }
405
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
406
   { infix_pp $1 PPor $3 }
407
| lexpr ASYM_OR lexpr
MARCHE Claude's avatar
MARCHE Claude committed
408
   { let label = Ident.label "asym_split" in
409
     mk_pp (PPnamed (label, infix_pp $1 PPor $3)) }
410
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
411
   { infix_pp $1 PPand $3 }
412
| lexpr ASYM_AND lexpr
MARCHE Claude's avatar
MARCHE Claude committed
413
   { let label = Ident.label "asym_split" in
414
     mk_pp (PPnamed (label, infix_pp $1 PPand $3)) }
415
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
416
   { prefix_pp PPnot $2 }
417
| lexpr EQUAL lexpr
418
   { let id = { id = infix "="; id_loc = loc_i 2 } in
419
     mk_pp (PPinfix ($1, id, $3)) }
420
421
422
| lexpr LTGT lexpr
   { let id = { id = infix "="; id_loc = loc_i 2 } in
     prefix_pp PPnot (mk_pp (PPinfix ($1, id, $3))) }
423
| lexpr OP1 lexpr
424
   { let id = { id = infix $2; id_loc = loc_i 2 } in
425
     mk_pp (PPinfix ($1, id, $3)) }
426
| lexpr OP2 lexpr
427
   { let id = { id = infix $2; id_loc = loc_i 2 } in
428
     mk_pp (PPinfix ($1, id, $3)) }
429
| lexpr OP3 lexpr
430
   { let id = { id = infix $2; id_loc = loc_i 2 } in
431
     mk_pp (PPinfix ($1, id, $3)) }
432
| lexpr OP4 lexpr
433
   { let id = { id = infix $2; id_loc = loc_i 2 } in
434
     mk_pp (PPinfix ($1, id, $3)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
435
| any_op lexpr %prec prefix_op
436
437
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }
438
439
| qualid list1_lexpr_arg
   { mk_pp (PPapp ($1, $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
440
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
441
   { mk_pp (PPif ($2, $4, $6)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
442
443
| quant list1_param_var_sep_comma triggers DOT lexpr
   { mk_pp (PPquant ($1, $2, $3, $5)) }
444
| STRING lexpr %prec prec_named
MARCHE Claude's avatar
MARCHE Claude committed
445
   { mk_pp (PPnamed (Ident.label ~loc:(loc ()) $1, $2)) }
446
| LET pattern EQUAL lexpr IN lexpr
447
448
   { match $2.pat_desc with
       | PPpvar id -> mk_pp (PPlet (id, $4, $6))
Andrei Paskevich's avatar
Andrei Paskevich committed
449
450
       | _ -> mk_pp (PPmatch ($4, [$2, $6])) }
| MATCH lexpr WITH bar_ match_cases END
451
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
452
453
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
   { mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
454
455
| EPSILON lident COLON primitive_type DOT lexpr
   { mk_pp (PPeps ($2, $4, $6)) }
456
| lexpr COLON primitive_type
457
   { mk_pp (PPcast ($1, $3)) }
458
| lexpr_arg
459
460
461
   { $1 }
;

462
463
464
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
465
;
466

467
468
469
lexpr_arg:
| qualid
   { mk_pp (PPvar $1) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
470
| INTEGER
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
471
   { mk_pp (PPconst (Term.ConstInt $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
472
| FLOAT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
473
   { mk_pp (PPconst (Term.ConstReal $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
474
475
476
| TRUE
   { mk_pp PPtrue }
| FALSE
477
   { mk_pp PPfalse }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
478
479
| LEFTPAR lexpr RIGHTPAR
   { $2 }
480
481
482
483
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
484
485
486
| OPPREF lexpr_arg
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }
Andrei Paskevich's avatar
Andrei Paskevich committed
487
;
488

Andrei Paskevich's avatar
Andrei Paskevich committed
489
490
491
492
493
494
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

495
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
496

497
498
499
500
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
501

502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
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 */
517

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
518
519
520
521
522
523
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
524
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
525
526
527
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
| pat_conj              { $1 }
| pat_conj BAR pattern  { mk_pat (PPpor ($1, $3)) }
;

pat_conj:
| pat_uni                      { $1 }
| pat_uni COMMA list1_pat_uni  { mk_pat (PPptuple ($1::$3)) }
;

list1_pat_uni:
| pat_uni                      { [$1] }
| pat_uni COMMA list1_pat_uni  { $1::$3 }
;

pat_uni:
| pat_arg                { $1 }
| uqualid list1_pat_arg  { mk_pat (PPpapp ($1, $2)) }
| pat_uni AS lident      { mk_pat (PPpas ($1, $3)) }
;
547

548
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
549
550
551
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
552

553
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
554
555
556
557
558
| UNDERSCORE                { mk_pat (PPpwild) }
| lident                    { mk_pat (PPpvar $1) }
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
559
560
;

561
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
562

563
564
565
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
566
567
;

568
569
570
571
572
573
574
575
576
577
578
579
580
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
581
582
;

583
584
585
586
587
588
589
590
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
591
592
;

593
594
595
596
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
597
598
;

599
600
601
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
602
603
;

604
605
606
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
607
608
;

609
list1_lident:
610
611
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
612
613
;

614
615
616
617
618
/* Idents */

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

621
622
623
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
624
625
;

626
627
628
629
630
631
632
633
634
635
636
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
637
638
;

639
640
lident:
| LIDENT  { { id = $1; id_loc = loc () } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
641
642
;

643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
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) }
Andrei Paskevich's avatar
Andrei Paskevich committed
688
;
689
690
691
692

qualid:
| ident_rich             { Qident $1 }
| uqualid DOT ident_rich { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
693
;
694
695
696
697
698
699

/* Misc */

bar_:
| /* epsilon */ { () }
| BAR           { () }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
700
701
;