plugins/python/py_parser.mly

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 %{
  13   open Why3
  14   open Ptree
  15   open Py_ast
  16
  17   let () = Exn_printer.register (fun fmt exn -> match exn with
  18     | Error -> Format.pp_print_string fmt "syntax error"
  19     | _ -> raise exn)
  20
  21   let floc s e = Loc.extract (s,e)
  22   let mk_id id s e = { id_str = id; id_ats = []; id_loc = floc s e }
  23   let mk_pat  d s e = { pat_desc  = d; pat_loc  = floc s e }
  24   let mk_term d s e = { term_desc = d; term_loc = floc s e }
  25   let mk_expr loc d = { expr_desc = d; expr_loc = loc }
  26   let mk_stmt loc d = Dstmt { stmt_desc = d; stmt_loc = loc }
  27   let mk_var id = mk_expr id.id_loc (Eident id)
  28
  29   let variant_union v1 v2 = match v1, v2 with
  30     | _, [] -> v1
  31     | [], _ -> v2
  32     | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
  33         "multiple `variant' clauses are not allowed"
  34
  35   let get_op s e = Qident (mk_id (Ident.op_get "") s e)
  36   let upd_op s e = Qident (mk_id (Ident.op_update "") s e)
  37
  38   let empty_spec = {
  39     sp_pre     = [];    sp_post    = [];  sp_xpost  = [];
  40     sp_reads   = [];    sp_writes  = [];  sp_alias  = [];
  41     sp_variant = [];
  42     sp_checkrw = false; sp_diverge = false; sp_partial = false;
  43   }
  44
  45   let spec_union s1 s2 = {
  46     sp_pre     = s1.sp_pre @ s2.sp_pre;
  47     sp_post    = s1.sp_post @ s2.sp_post;
  48     sp_xpost   = s1.sp_xpost @ s2.sp_xpost;
  49     sp_reads   = s1.sp_reads @ s2.sp_reads;
  50     sp_writes  = s1.sp_writes @ s2.sp_writes;
  51     sp_alias   = s1.sp_alias @ s2.sp_alias;
  52     sp_variant = variant_union s1.sp_variant s2.sp_variant;
  53     sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
  54     sp_diverge = s1.sp_diverge || s2.sp_diverge;
  55     sp_partial = s1.sp_partial || s2.sp_partial;
  56   }
  57
  58   let fresh_type_var =
  59     let r = ref 0 in
  60     fun loc -> incr r;
  61       PTtyvar { id_str = "a" ^ string_of_int !r; id_loc = loc; id_ats = [] }
  62
  63   let logic_type loc = function
  64   | None    -> fresh_type_var loc
  65   | Some ty -> ty
  66
  67   let logic_param loc (id, ty) = id, logic_type loc ty
  68
  69 %}
  70
  71 %token <string> INTEGER
  72 %token <string> STRING
  73 %token <Py_ast.binop> CMP
  74 %token <string> IDENT QIDENT TVAR
  75 %token DEF IF ELSE ELIF RETURN WHILE FOR IN AND OR NOT NONE TRUE FALSE PASS
  76 %token FROM IMPORT BREAK CONTINUE
  77 %token EOF
  78 %token LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ COMMA EQUAL COLON BEGIN END NEWLINE
  79        PLUSEQUAL MINUSEQUAL TIMESEQUAL DIVEQUAL MODEQUAL
  80        LEFTBR RIGHTBR
  81 %token PLUS MINUS TIMES DIV MOD
  82 (* annotations *)
  83 %token INVARIANT VARIANT ASSUME ASSERT CHECK REQUIRES ENSURES LABEL
  84 %token FUNCTION PREDICATE AXIOM LEMMA CONSTANT CALL
  85 %token ARROW LARROW LRARROW FORALL EXISTS DOT THEN LET OLD AT BY SO
  86
  87 (* precedences *)
  88
  89 %nonassoc IN
  90 %nonassoc DOT ELSE
  91 %right ARROW LRARROW BY SO
  92 %nonassoc IF
  93 %right OR
  94 %right AND
  95 %nonassoc NOT
  96 %right CMP
  97 %left PLUS MINUS
  98 %left TIMES DIV MOD
  99 %nonassoc unary_minus prec_prefix_op
 100 %nonassoc LEFTSQ
 101
 102 %start file
 103 (* Transformations entries *)
 104 %start <Why3.Ptree.term> term_eof
 105 %start <Why3.Ptree.term list> term_comma_list_eof
 106 %start <Why3.Ptree.ident list> ident_comma_list_eof
 107
 108 %type <Py_ast.file> file
 109 %type <Py_ast.decl> stmt
 110
 111 %%
 112
 113 file:
 114 | NEWLINE* EOF
 115     { [] }
 116 | NEWLINE? dl=nonempty_list(decl) NEWLINE? EOF
 117     { dl }
 118 ;
 119
 120 decl:
 121 | import { $1 }
 122 | def    { $1 }
 123 | stmt   { $1 }
 124 | func   { $1 }
 125 | prop   { $1 }
 126 | const  { $1 }
 127
 128 import:
 129 | FROM m=ident IMPORT l=separated_list(COMMA, ident) NEWLINE
 130   { Dimport (m, l) }
 131
 132 const:
 133 | CONSTANT NEWLINE id = ident EQUAL e = expr NEWLINE
 134   { Dconst (id,e) }
 135
 136 prop:
 137 | LEMMA id=ident COLON t=term NEWLINE
 138   { Dprop (Decl.Plemma, id, t) }
 139 | AXIOM id=ident COLON t=term NEWLINE
 140   { Dprop (Decl.Paxiom, id, t) }
 141
 142 func:
 143 | FUNCTION id=ident LEFTPAR l=separated_list(COMMA, param) RIGHTPAR
 144   ty=option(function_type) var = option(fp_variant) def=option(logic_body)
 145   NEWLINE
 146   { let loc = floc $startpos $endpos in
 147     Dlogic (id, List.map (logic_param loc) l, Some (logic_type loc ty),
 148             var, def) }
 149 | PREDICATE id=ident LEFTPAR l=separated_list(COMMA, param) RIGHTPAR
 150   var=option(fp_variant) def=option(logic_body) NEWLINE
 151   { let loc = floc $startpos $endpos in
 152     Dlogic (id, List.map (logic_param loc) l, None, var, def) }
 153
 154 fp_variant:
 155 | LEFTBR VARIANT v=term RIGHTBR { v }
 156
 157 logic_body:
 158 | EQUAL t=term
 159   { t }
 160
 161 param:
 162 | id=ident ty=option(param_type)
 163   { id, ty }
 164
 165 param_type:
 166 | COLON ty=typ
 167   { ty }
 168
 169 function_type:
 170 | ARROW ty=typ
 171   { ty }
 172
 173 /* Note: "list" is a legal type annotation in Python; we make it a
 174  * polymorphic type "list 'a" in WhyML  */
 175 typ:
 176 | id=type_var
 177   { PTtyvar id }
 178 | id=ident
 179   { if id.id_str = "list"
 180     then PTtyapp (Qident id, [fresh_type_var (floc $startpos $endpos)])
 181     else PTtyapp (Qident id, []) }
 182 | id=ident LEFTSQ tyl=separated_nonempty_list(COMMA, typ) RIGHTSQ
 183     {
 184       if id.id_str = "Tuple" then PTtuple tyl else PTtyapp (Qident id, tyl)
 185     }
 186
 187 def:
 188 | fct = as_funct
 189   DEF f = ident LEFTPAR x = separated_list(COMMA, param) RIGHTPAR
 190   ty=option(function_type) COLON NEWLINE BEGIN s=spec l=body END
 191     {
 192       if f.id_str = "range" then
 193         let loc = floc $startpos $endpos in
 194         Loc.errorm ~loc "micro Python does not allow shadowing 'range'"
 195       else if fct && ty = None then
 196         let loc = floc $startpos $endpos in
 197         Loc.errorm ~loc "a logical function should not return a unit type"
 198       else Ddef (f, x, ty, s, l ty s, fct)
 199     }
 200 ;
 201
 202 as_funct:
 203 | FUNCTION NEWLINE { true  }
 204 | (* epsilon *)    { false }
 205 ;
 206
 207 body:
 208 | nonempty_list(stmt)
 209   { fun _ _ -> $1 }
 210 | PASS NEWLINE
 211   { fun ty s -> [mk_stmt (floc $startpos $endpos) (Spass (ty, s))] }
 212
 213 spec:
 214 | (* epsilon *)     { empty_spec }
 215 | single_spec spec  { spec_union $1 $2 }
 216
 217 single_spec:
 218 | REQUIRES t=term NEWLINE
 219     { { empty_spec with sp_pre = [t] } }
 220 | ENSURES e=ensures NEWLINE
 221     { { empty_spec with sp_post = [floc $startpos(e) $endpos(e), e] } }
 222 | variant
 223     { { empty_spec with sp_variant = $1 } }
 224
 225 ensures:
 226 | term
 227     { let id = mk_id "result" $startpos $endpos in
 228       [mk_pat (Pvar id) $startpos $endpos, $1] }
 229 ;
 230
 231 expr_dot:
 232 | d = expr_dot_
 233    { mk_expr (floc $startpos $endpos) d }
 234 ;
 235
 236 expr_dot_:
 237 | id = ident
 238     { Eident id }
 239 | LEFTPAR e = expr RIGHTPAR
 240     { e.expr_desc }
 241 ;
 242
 243 expr:
 244 | d = expr_desc
 245    { mk_expr (floc $startpos $endpos) d }
 246 ;
 247
 248 /*
 249 expr_desc:
 250   e = expr_nt { e.expr_desc }
 251 | e1 = expr_nt COMMA el = separated_list(COMMA, expr_nt)
 252     { Etuple (e1::el) }
 253 ;
 254 */
 255 expr_desc:
 256   e = expr_nt_desc { e }
 257 | e = expr_nt COMMA el = separated_list(COMMA, expr_nt) { Etuple (e::el) }
 258 ;
 259
 260 expr_nt:
 261 | d = expr_nt_desc
 262    { mk_expr (floc $startpos $endpos) d }
 263 ;
 264
 265 expr_nt_desc:
 266 | NONE
 267     { Enone }
 268 | TRUE
 269     { Ebool true }
 270 | FALSE
 271     { Ebool false }
 272 | c = INTEGER
 273     { Eint c }
 274 | s = STRING
 275     { Estring s }
 276 | e1 = expr_nt LEFTSQ e2 = expr_nt RIGHTSQ
 277     { Eget (e1, e2) }
 278 | e1 = expr_nt LEFTSQ e2=option(expr_nt) COLON e3=option(expr_nt) RIGHTSQ
 279     {
 280       let f = mk_id "slice" $startpos $endpos in
 281       let none = mk_expr (floc $startpos $endpos) Enone in
 282       let e2, e3 = match e2, e3 with
 283         | None, None -> none, none
 284         | Some e, None -> e, none
 285         | None, Some e -> none, e
 286         | Some e, Some e' -> e, e'
 287       in
 288       Ecall(f,[e1;e2;e3])
 289     }
 290 | MINUS e1 = expr_nt %prec unary_minus
 291     { Eunop (Uneg, e1) }
 292 | NOT e1 = expr_nt
 293     { Eunop (Unot, e1) }
 294 | e1 = expr_nt o = binop e2 = expr_nt
 295     { Ebinop (o, e1, e2) }
 296 | e1 = expr_nt TIMES e2 = expr_nt
 297     { match e1.expr_desc with
 298       | Elist [e1] -> Emake (e1, e2)
 299       | _ -> Ebinop (Bmul, e1, e2) }
 300 | e=expr_dot DOT f=ident LEFTPAR el=separated_list(COMMA, expr_nt) RIGHTPAR
 301     {
 302       match f.id_str with
 303       | "pop" | "append" | "reverse" | "clear" | "copy" | "sort" ->
 304         Edot (e, f, el)
 305       | m -> let loc = floc $startpos $endpos in
 306              Loc.errorm ~loc "The method '%s' is not implemented" m
 307     }
 308 | f = ident LEFTPAR e = separated_list(COMMA, expr_nt) RIGHTPAR
 309     { Ecall (f, e) }
 310 | LEFTSQ l = separated_list(COMMA, expr_nt) RIGHTSQ
 311     { Elist l }
 312 | e1=expr_nt IF c=expr_nt ELSE e2=expr_nt
 313     { Econd(c,e1,e2) }
 314 | e=expr_dot_
 315     { e }
 316 ;
 317
 318 %inline binop:
 319 | PLUS  { Badd }
 320 | MINUS { Bsub }
 321 | DIV   { Bdiv }
 322 | MOD   { Bmod }
 323 | c=CMP { c    }
 324 | AND   { Band }
 325 | OR    { Bor  }
 326 ;
 327
 328 located(X):
 329 | X { mk_stmt (floc $startpos $endpos) $1 }
 330 ;
 331
 332 suite:
 333 | s = simple_stmt NEWLINE
 334     { [s] }
 335 | NEWLINE BEGIN l = nonempty_list(stmt) END
 336     { l }
 337 ;
 338
 339 stmt:
 340 | located(stmt_desc)      { $1 }
 341 | s = simple_stmt NEWLINE { s }
 342
 343 stmt_desc:
 344 | IF c = expr_nt COLON s1 = suite s2=else_branch
 345     { Sif (c, s1, s2) }
 346 | WHILE e = expr_nt COLON b=loop_body
 347     { let i, v, l = b in Swhile (e, i, v, l) }
 348 | FOR x = ident IN e = expr COLON b=loop_body
 349     { let i, _, l = b in Sfor (x, e, i, l) }
 350 ;
 351
 352 else_branch:
 353 | /* epsilon */
 354     { [] }
 355 | ELSE COLON s2=suite
 356     { s2 }
 357 | ELIF c=expr_nt COLON s1=suite s2=else_branch
 358     { [mk_stmt (floc $startpos $endpos) (Sif (c, s1, s2))] }
 359
 360
 361 loop_body:
 362 | s = simple_stmt NEWLINE
 363   { [], [], [s] }
 364 | NEWLINE BEGIN a=loop_annotation l=nonempty_list(stmt) END
 365   { fst a, snd a, l }
 366
 367 loop_annotation:
 368 | (* epsilon *)
 369     { [], [] }
 370 | invariant loop_annotation
 371     { let (i, v) = $2 in ($1::i, v) }
 372 | variant loop_annotation
 373     { let (i, v) = $2 in (i, variant_union $1 v) }
 374
 375 invariant:
 376 | INVARIANT i=term NEWLINE { i }
 377
 378 variant:
 379 | VARIANT l=comma_list1(term) NEWLINE { List.map (fun t -> t, None) l }
 380
 381 simple_stmt: located(simple_stmt_desc) { $1 };
 382
 383 simple_stmt_desc:
 384 | RETURN e = expr
 385     { Sreturn e }
 386 | lhs = expr EQUAL rhs = expr { Sassign (lhs, rhs) }
 387 | id=ident o=binop_equal e=expr_nt
 388     { let loc = floc $startpos $endpos in
 389       Sassign (mk_var id,
 390                mk_expr loc (Ebinop (o, mk_expr loc (Eident id), e))) }
 391 | e0 = expr_nt LEFTSQ e1 = expr_nt RIGHTSQ o=binop_equal e2 = expr
 392     {
 393       let loc = floc $startpos $endpos in
 394       let mk_expr_floc = mk_expr loc in
 395       let id = mk_id "'i" $startpos $endpos in
 396       let expr_id = mk_expr_floc (Eident id) in
 397       let a = mk_id "'a" $startpos $endpos in
 398       let expr_a = mk_expr_floc (Eident a) in
 399       let operation =
 400         mk_expr_floc (Ebinop (o, mk_expr_floc (Eget(expr_a, expr_id)), e2)) in
 401       let s1 =
 402         Dstmt ({ stmt_desc = Sassign (mk_var a, e0); stmt_loc = loc }) in
 403       let s2 =
 404         Dstmt ({ stmt_desc = Sassign (mk_var id, e1); stmt_loc = loc }) in
 405       let s3 =
 406         Dstmt ({ stmt_desc = Sset (expr_a, expr_id, operation);
 407                  stmt_loc = loc }) in
 408       Sblock [s1; s2; s3]
 409     }
 410 | k=assertion_kind t = term
 411     { Sassert (k, t) }
 412 | e = expr
 413     { Seval e }
 414 | CALL f = ident LEFTPAR e = separated_list(COMMA, term) RIGHTPAR
 415     { Scall_lemma (f, e) }
 416 | BREAK
 417     { Sbreak }
 418 | CONTINUE
 419     { Scontinue }
 420 | LABEL id=ident
 421     { Slabel id }
 422 ;
 423
 424 %inline binop_equal:
 425 | PLUSEQUAL  { Badd }
 426 | MINUSEQUAL { Bsub }
 427 | DIVEQUAL   { Bdiv }
 428 | TIMESEQUAL { Bmul }
 429 | MODEQUAL   { Bmod }
 430 ;
 431
 432 assertion_kind:
 433 | ASSERT  { Expr.Assert }
 434 | ASSUME  { Expr.Assume }
 435 | CHECK   { Expr.Check }
 436
 437 ident:
 438 | id = IDENT { mk_id id $startpos $endpos }
 439 ;
 440 quote_ident:
 441 | id = QIDENT { mk_id id $startpos $endpos }
 442 ;
 443 type_var:
 444 | id = TVAR { mk_id id $startpos $endpos }
 445 ;
 446
 447 /* logic */
 448
 449 mk_term(X): d = X { mk_term d $startpos $endpos }
 450
 451 term_tuple: t = mk_term(term_tuple_) { t }
 452
 453 term_tuple_:
 454 | t = term ; COMMA; lt=separated_list(COMMA, term)
 455     { Ttuple (t::lt) }
 456 | t = term_ { t }
 457
 458 term: t = mk_term(term_) { t }
 459
 460 term_:
 461 | term_arg_
 462     { match $1 with (* break the infix relation chain *)
 463       | Tinfix (l,o,r) -> Tinnfix (l,o,r)
 464       | Tbinop (l,o,r) -> Tbinnop (l,o,r)
 465       | d -> d }
 466 | NOT term
 467     { Tnot $2 }
 468 | OLD LEFTPAR t=term RIGHTPAR
 469     { Tat (t, mk_id Dexpr.old_label $startpos($1) $endpos($1)) }
 470 | AT LEFTPAR t=term COMMA l=ident RIGHTPAR
 471     { Tat (t, l) }
 472 | o = prefix_op ; t = term %prec prec_prefix_op
 473     { Tidapp (Qident o, [t]) }
 474 | l = term ; o = bin_op ; r = term
 475     { Tbinop (l, o, r) }
 476 | l = term ; o = infix_op_1 ; r = term
 477     { Tinfix (l, o, r) }
 478 | l = term ; o = infix_op_234 ; r = term
 479     { Tidapp (Qident o, [l; r]) }
 480 | IF term THEN term ELSE term
 481     { Tif ($2, $4, $6) }
 482 | LET id=ident EQUAL t1=term IN t2=term
 483     { Tlet (id, t1, t2) }
 484 | q=quant l=comma_list1(param) DOT t=term
 485     { let var (id, ty) = id.id_loc, Some id, false, ty in
 486       Tquant (q, List.map var l, [], t) }
 487 | id=ident LEFTPAR l=separated_list(COMMA, term) RIGHTPAR
 488     { Tidapp (Qident id, l) }
 489
 490 quant:
 491 | FORALL  { Dterm.DTforall }
 492 | EXISTS  { Dterm.DTexists }
 493
 494 term_arg: mk_term(term_arg_) { $1 }
 495
 496 term_arg_:
 497 | quote_ident { Tident (Qident $1) }
 498 | ident       { Tident (Qident $1) }
 499 | INTEGER     { Tconst (Constant.ConstInt Number.(int_literal ILitDec ~neg:false $1)) }
 500 | NONE        { Ttuple [] }
 501 | TRUE        { Ttrue }
 502 | FALSE       { Tfalse }
 503 | term_sub_                 { $1 }
 504
 505 term_sub_:
 506 | LEFTPAR term_tuple RIGHTPAR                             { $2.term_desc }
 507 | term_arg LEFTSQ term RIGHTSQ
 508     { Tidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
 509 | term_arg LEFTSQ term LARROW term RIGHTSQ
 510     { Tidapp (upd_op $startpos($2) $endpos($2), [$1;$3;$5]) }
 511 | e1 = term_arg LEFTSQ e2=option(term) COLON e3=option(term) RIGHTSQ
 512     {
 513       let slice = mk_id "slice" $startpos $endpos in
 514       let len = mk_id "len" $startpos $endpos in
 515       let z = Tconst (Constant.int_const_of_int 0) in
 516       let l = Tidapp(Qident len, [e1]) in
 517       let z = mk_term z $startpos $endpos in
 518       let l = mk_term l $startpos $endpos in
 519       let e2, e3 = match e2, e3 with
 520         | None, None -> z, l
 521         | Some e, None -> e, l
 522         | None, Some e -> z, e
 523         | Some e, Some e' -> e, e'
 524       in
 525       Tidapp(Qident slice,[e1;e2;e3])
 526     }
 527
 528 %inline bin_op:
 529 | ARROW   { Dterm.DTimplies }
 530 | LRARROW { Dterm.DTiff }
 531 | OR      { Dterm.DTor }
 532 | AND     { Dterm.DTand }
 533 | BY      { Dterm.DTby }
 534 | SO      { Dterm.DTso }
 535
 536 %inline infix_op_1:
 537 | c=CMP  { let op = match c with
 538           | Beq  -> "="
 539           | Bneq -> "<>"
 540           | Blt  -> "<"
 541           | Ble  -> "<="
 542           | Bgt  -> ">"
 543           | Bge  -> ">="
 544           | Badd|Bsub|Bmul|Bdiv|Bmod|Band|Bor -> assert false in
 545            mk_id (Ident.op_infix op) $startpos $endpos }
 546
 547 %inline prefix_op:
 548 | MINUS { mk_id (Ident.op_prefix "-")  $startpos $endpos }
 549
 550 %inline infix_op_234:
 551 | DIV    { mk_id (Ident.op_infix "//") $startpos $endpos }
 552 | MOD    { mk_id (Ident.op_infix "%") $startpos $endpos }
 553 | PLUS   { mk_id (Ident.op_infix "+") $startpos $endpos }
 554 | MINUS  { mk_id (Ident.op_infix "-") $startpos $endpos }
 555 | TIMES  { mk_id (Ident.op_infix "*") $startpos $endpos }
 556
 557 comma_list1(X):
 558 | separated_nonempty_list(COMMA, X) { $1 }
 559
 560 (* Parsing of a list of qualified identifiers for the ITP *)
 561
 562 (* parsing of a single term *)
 563
 564 term_eof:
 565 | term NEWLINE EOF { $1 }
 566
 567 ident_comma_list_eof:
 568 | comma_list1(ident) NEWLINE EOF { $1 }
 569
 570 term_comma_list_eof:
 571 | comma_list1(term) NEWLINE EOF { $1 }
 572 (* we use single_term to avoid conflict with tuples, that
 573    do not need parentheses *)