parser.mly 16.7 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
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

  let add_lab id l = { id with id_lab = l }

79 80 81 82 83 84 85 86 87
  let user_loc fname lnum bol cnum1 cnum2 =
    let pos = {
      Lexing.pos_fname = fname;
      Lexing.pos_lnum = lnum;
      Lexing.pos_bol = bol;
      Lexing.pos_cnum = cnum1 }
    in
    pos, { pos with Lexing.pos_cnum = cnum2 }

88 89 90 91 92
  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
93 94
%}

95
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96

97
%token <string> LIDENT UIDENT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
98
%token <string> INTEGER
99
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
100 101
%token <Ptree.real_constant> FLOAT
%token <string> STRING
102 103 104

/* keywords */

105 106
%token AND AS AXIOM CLONE
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
Andrei Paskevich's avatar
Andrei Paskevich committed
107
%token GOAL IF IMPORT IN INDUCTIVE LAMBDA LEMMA
108
%token LET LOGIC MATCH META NAMESPACE NOT PROP OR
Andrei Paskevich's avatar
Andrei Paskevich committed
109
%token THEN THEORY TRUE TYPE USE WITH
110 111 112

/* symbols */

113
%token ARROW ASYM_AND ASYM_OR
114
%token BACKQUOTE BAR
115
%token COLON COMMA
116
%token DOT EQUAL LTGT
117
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
118
%token LRARROW
Andrei Paskevich's avatar
Andrei Paskevich committed
119
%token QUOTE
120
%token RIGHTPAR RIGHTSQ
121 122 123 124
%token UNDERSCORE

%token EOF

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
125 126
/* Precedences */

127
%nonassoc DOT ELSE IN
128
%nonassoc prec_named
129
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
130 131

%right ARROW LRARROW
132 133
%right OR ASYM_OR
%right AND ASYM_AND
Andrei Paskevich's avatar
Andrei Paskevich committed
134
%nonassoc NOT
135
%left EQUAL LTGT OP1
136
%left OP2
137
%left OP3
138
%left OP4
Andrei Paskevich's avatar
Andrei Paskevich committed
139
%nonassoc prefix_op
140

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
141 142
/* Entry points */

143 144 145 146 147 148
%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
149 150
%%

151 152 153 154 155 156 157 158 159 160 161 162 163
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 */
164

165 166 167
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
168 169
;

170
theory_head:
171 172 173
| THEORY uident labels
   { let id = add_lab $2 $3 and labels = $3 in
     let name = Ident.id_user ~labels id.id id.id_loc in
174
     ref_push uc_ref (create_theory name); id }
175 176
;

177
theory:
178 179 180
| 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) }
181 182
;

183
list0_decl:
184 185 186 187 188 189 190 191 192 193
| /* 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)) }
194 195
;

196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212
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 */

213
decl:
214 215 216 217 218 219
| TYPE list1_type_decl
    { TypeDecl $2 }
| LOGIC list1_logic_decl
    { LogicDecl $2 }
| INDUCTIVE list1_inductive_decl
    { IndDecl $2 }
220 221 222 223 224 225 226 227 228 229
| 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) }
230 231
| META ident list1_meta_arg_sep_comma
    { Meta (loc (), $2, $3) }
232
| META STRING list1_meta_arg_sep_comma
233
    { Meta (loc (), mk_id $2 (loc_i 2), $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
234 235
;

236 237 238 239 240 241 242 243 244
/* 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
245 246
;

247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
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 }
;

270 271 272 273 274 275 276 277 278 279 280 281 282 283 284
/* 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 }
;

285 286 287
/* Type declarations */

list1_type_decl:
288 289
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
290 291 292
;

type_decl:
293 294 295
| lident labels type_args typedefn
  { { td_loc = loc (); td_ident = add_lab $1 $2;
      td_params = $3; td_def = $4 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
296 297
;

298
type_args:
299 300
| /* epsilon */             { [] }
| type_var labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
301 302 303
;

typedefn:
304 305 306 307
| /* 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
308 309 310 311 312 313 314 315
;

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

typecase:
316
| uident labels params   { (loc (), add_lab $1 $2, $3) }
317 318 319 320 321
;

/* Logic declarations */

list1_logic_decl:
322 323
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
324 325 326
;

logic_decl:
327 328 329
| lident_rich labels params logic_type_option logic_def_option
  { { ld_loc = loc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = $4; ld_def = $5 } }
330 331 332 333 334 335 336 337 338 339
;

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
340 341
;

342 343 344
/* Inductive declarations */

list1_inductive_decl:
345 346
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
347 348 349
;

inductive_decl:
350 351 352
| lident_rich labels params inddefn
  { { in_loc = loc (); in_ident = add_lab $1 $2;
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
353
;
354

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
355 356 357 358 359 360 361 362 363 364 365
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

indcase:
366
| uident labels COLON lexpr { (loc (), add_lab $1 $2, $4) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
367 368
;

369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392
/* 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
393
   { PPTtyapp ([], $1) }
394 395 396 397
| type_var
   { PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
398 399 400 401 402 403
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
404 405 406 407 408
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

409 410
type_var:
| QUOTE ident { $2 }
411 412
;

413 414
/* Logic expressions */

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

468 469 470
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
471
;
472

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

Andrei Paskevich's avatar
Andrei Paskevich committed
494 495 496 497 498 499
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
;

500
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
501

502 503 504 505
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
506

507 508 509 510 511 512 513 514 515 516 517 518 519 520 521
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 */
522

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
523 524 525 526 527 528
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
529
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
530 531 532
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
533 534 535 536 537 538 539 540 541 542 543 544 545 546 547
| 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:
548 549 550
| pat_arg                   { $1 }
| uqualid list1_pat_arg     { mk_pat (PPpapp ($1, $2)) }
| pat_uni AS lident labels  { mk_pat (PPpas ($1, add_lab $3 $4)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
551
;
552

553
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
554 555 556
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
557

558
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
559
| UNDERSCORE                { mk_pat (PPpwild) }
560
| lident labels             { mk_pat (PPpvar (add_lab $1 $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
561 562 563
| 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
564 565
;

566
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
567

568 569 570
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
571 572
;

573 574 575 576 577 578 579 580 581 582 583 584 585
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
586 587
;

588 589 590 591 592 593 594 595
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
596 597
;

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

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

609 610 611
param_var:
| list1_lident COLON primitive_type
   { List.map (fun id -> (Some id, $3)) $1 }
612 613 614 615 616 617
| list1_lident label labels list0_lident_labels COLON primitive_type
   { let l = match List.rev $1 with
       | i :: l -> add_lab i ($2 :: $3) :: l
       | [] -> assert false
     in
     List.map (fun id -> (Some id, $6)) (List.rev_append l $4) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
618 619
;

620
list1_lident:
621 622
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
623 624
;

625 626 627 628 629
list0_lident_labels:
| /* epsilon */                      { [] }
| lident labels list0_lident_labels  { add_lab $1 $2 :: $3 }
;

630 631 632 633 634
/* Idents */

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

637 638 639
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
640 641
;

642 643 644 645
lident_rich:
| lident
    { $1 }
| LEFTPAR lident_op RIGHTPAR
646
    { mk_id (infix $2) (loc ()) }
647
| LEFTPAR_STAR_RIGHTPAR
648
    { mk_id (infix "*") (loc ()) }
649
| LEFTPAR lident_op UNDERSCORE RIGHTPAR
650
    { mk_id (prefix $2) (loc ()) }
651
| LEFTPAR OPPREF RIGHTPAR
652
    { mk_id (prefix $2) (loc ()) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
653 654
;

655
lident:
656
| LIDENT { mk_id $1 (loc ()) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
657 658
;

659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674
lident_op:
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
| EQUAL { "=" }
;

any_op:
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

uident:
675
| UIDENT { mk_id $1 (loc ()) }
676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703
;

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
704
;
705 706 707 708

qualid:
| ident_rich             { Qident $1 }
| uqualid DOT ident_rich { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
709
;
710 711 712

/* Misc */

713 714 715 716 717 718 719 720 721 722
label:
| STRING
   { Ident.label $1 }
| STRING BACKQUOTE INTEGER BACKQUOTE INTEGER
         BACKQUOTE INTEGER BACKQUOTE INTEGER BACKQUOTE STRING
   { let loc = user_loc $11 (int_of_string $3) (int_of_string $5)
                            (int_of_string $7) (int_of_string $9) in
     Ident.label ~loc $1 }
;

723 724 725 726 727
labels:
| /* epsilon */ { [] }
| label labels  { $1 :: $2 }
;

728 729 730
bar_:
| /* epsilon */ { () }
| BAR           { () }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
731 732
;