parser.mly 13.3 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 OPPREF
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
%nonassoc OPPREF
102

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

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

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

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

127 128 129 130 131 132 133
list0_decl:
| /* epsilon */
   { [] }
| list1_decl 
   { $1 }
;

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

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

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

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

162
lident_op:
163
| OP1   { $1 }
164 165
| OP2   { $1 }
| OP3   { $1 }
166
| STAR  { "*" }
167
| OP4   { $1 }
168 169
| EQUAL { "=" }
;
170

171
any_op:
172
| OP1   { $1 }
173 174
| OP2   { $1 }
| OP3   { $1 }
175
| STAR  { "*" }
176
| OP4   { $1 }
177
;
178

179 180 181 182 183 184 185 186 187 188 189 190
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) }
191 192
;

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

198 199 200 201
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }

202
qualid:
203 204
| ident_rich             { Qident $1 }
| uqualid DOT ident_rich { Qdot ($1, $3) }
205

206 207 208 209 210 211 212 213 214 215 216 217 218 219 220
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 }
;

221 222 223 224
primitive_types:
| /* epsilon */                                   { [] }
| LEFTPAR list1_primitive_type_sep_comma RIGHTPAR { $2 }

225 226 227 228 229 230 231 232 233 234 235
logic_type_option:
| /* epsilon */        { None }
| COLON primitive_type { Some $2 }
;

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

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

list1_logic_decl:
242 243
| logic_decl                  %prec prec_decls { [$1] }
| logic_decl list1_logic_decl                  { $1 :: $2 }
244 245 246
;

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

list1_type_decl:
252
| type_decl                  %prec prec_decls { [$1] }
253 254 255
| type_decl list1_type_decl                   { $1 :: $2 }
;

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

292 293 294 295 296 297 298 299
list1_theory:
| theory 
   { [$1] }
| theory list1_theory 
   { $1 :: $2 }
;

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

304 305 306 307
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
308 309 310 311
;

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

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

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

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

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

indcase:
341
| uident COLON lexpr { (loc (),$1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
342 343
;

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

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

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

lexpr_arg:
| qualid
   { mk_pp (PPvar $1) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
435
| INTEGER
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
436
   { mk_pp (PPconst (Term.ConstInt $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
437
| FLOAT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
438
   { mk_pp (PPconst (Term.ConstReal $1)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
439 440 441 442 443 444
| TRUE
   { mk_pp PPtrue }
| FALSE
   { mk_pp PPfalse }    
| LEFTPAR lexpr RIGHTPAR
   { $2 }
445 446 447 448
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
449 450 451 452 453 454 455
| OPPREF lexpr_arg
   { let id = { id = prefix $1; id_loc = loc_i 2 } in
     mk_pp (PPapp (Qident id, [$2])) }

list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456

457 458 459 460 461
list1_uquant_sep_comma:
| uquant                              { [$1] }
| uquant COMMA list1_uquant_sep_comma { $1::$3 }

uquant:
462
| list1_lident COLON primitive_type { $1,$3 }
463

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
464 465 466 467 468 469
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

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

Andrei Paskevich's avatar
Andrei Paskevich committed
473 474 475 476
list1_pat_sep_comma:
| pattern                           { [$1] }
| pattern COMMA list1_pat_sep_comma { $1::$3 }

477 478 479 480
list1_pat_arg:
| pat_arg               { [$1] }
| pat_arg list1_pat_arg { $1::$2 }

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
481
pattern:
482 483 484 485 486
| 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
487 488 489
| UNDERSCORE                                    { mk_pat (PPpwild) }
| lident                                        { mk_pat (PPpvar $1) }
| uqualid                                       { mk_pat (PPpapp ($1, [])) }
490
| LEFTPAR pattern RIGHTPAR                      { $2 }
491 492 493
| 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
494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528
;

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

529 530 531
list1_lident:
| lident              { [$1] }
| lident list1_lident { $1 :: $2 }
532 533
;

534
use:
535
| imp_exp tqualid              
536
    { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
537
| imp_exp tqualid AS uident
538 539 540
    { { 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
541 542
;

543 544 545 546
imp_exp:
| IMPORT        { Import }
| EXPORT        { Export }
| /* epsilon */ { Nothing }
547 548
;

549
clone_subst:
550 551
| /* epsilon */          { [] } 
| WITH list1_comma_subst { $2 }
552 553 554
;

list1_comma_subst:
555 556
| subst                         { [$1] }
| subst COMMA list1_comma_subst { $1 :: $3 } 
557 558 559
;

subst:
560 561 562 563
| TYPE  qualid EQUAL qualid { CStsym ($2, $4) }
| LOGIC qualid EQUAL qualid { CSlsym ($2, $4) }
| LEMMA qualid              { CSlemma $2 }
| GOAL  qualid              { CSgoal  $2 }
564 565
;