parser.mly 13.1 KB
Newer Older
1 2
/**************************************************************************/
/*                                                                        */
Jean-Christophe Filliâtre's avatar
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 */

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

70 71
%token ARROW
%token BAR 
72
%token COLON COMMA  
73
%token DOT EQUAL
74
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ 
75
%token LRARROW
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 */

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
89
%nonassoc COLON 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90

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 
95
%nonassoc NOT
96
%left EQUAL OP1
97
%left OP2
98
%left OP3 STAR
99
%left OP4
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:
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 }
;

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
;

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 } }
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:
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)) }
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)) }
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)) }
411
| FORALL list1_uquant_sep_comma triggers DOT lexpr
412
   { mk_pp (PPquant (PPforall, $2, $3, $5)) }
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)) }
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, [])) }
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
;

535
clone_subst:
536 537
| /* epsilon */          { [] } 
| WITH list1_comma_subst { $2 }
538 539 540
;

list1_comma_subst:
541 542
| subst                         { [$1] }
| subst COMMA list1_comma_subst { $1 :: $3 } 
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 }
550 551
;