py_parser.mly 4.51 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12

%{
13 14
  open Why3
  open Ptree
15
  open Py_ast
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31

  let floc s e = Loc.extract (s,e)
  let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
  let mk_term d s e = { term_desc = d; term_loc = floc s e }
  let mk_expr loc d = { expr_desc = d; expr_loc = loc }
  let mk_stmt loc d = { stmt_desc = d; stmt_loc = loc }

  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
        "multiple `variant' clauses are not allowed"

  let empty_annotation =
    { loop_invariant = []; loop_variant = [] }

32 33
%}

34 35
%token <string> INTEGER
%token <string> STRING
36 37
%token <Py_ast.binop> CMP
%token <string> IDENT
38
%token DEF IF ELSE RETURN PRINT WHILE FOR IN AND OR NOT NONE TRUE FALSE
39 40 41 42
%token EOF
%token LP RP LSQ RSQ COMMA EQUAL COLON BEGIN END NEWLINE
%token PLUS MINUS TIMES DIV MOD

43 44 45
/* annotations */
%token INVARIANT VARIANT

46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
%left OR
%left AND
%nonassoc NOT
%nonassoc CMP
%left PLUS MINUS
%left TIMES DIV MOD
%nonassoc unary_minus
%nonassoc LSQ

%start file

%type <Py_ast.file> file

%%

file:
| NEWLINE? dl = list(def) b = list(stmt) EOF
63
    { dl, { stmt_desc = Sblock b; stmt_loc = floc $startpos(b) $endpos(b) } }
64 65 66 67 68 69 70 71 72
;

def:
| DEF f = ident LP x = separated_list(COMMA, ident) RP
  COLON s = suite
    { f, x, s }
;

expr:
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
| d = expr_desc
   { mk_expr (floc $startpos $endpos) d }
;

expr_desc:
| NONE
    { Enone }
| TRUE
    { Ebool true }
| FALSE
    { Ebool false }
| c = INTEGER
    { Eint c }
| s = STRING
    { Estring s }
88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
| id = ident
    { Eident id }
| e1 = expr LSQ e2 = expr RSQ
    { Eget (e1, e2) }
| MINUS e1 = expr %prec unary_minus
    { Eunop (Uneg, e1) }
| NOT e1 = expr
    { Eunop (Unot, e1) }
| e1 = expr o = binop e2 = expr
    { Ebinop (o, e1, e2) }
| f = ident LP e = separated_list(COMMA, expr) RP
    { Ecall (f, e) }
| LSQ l = separated_list(COMMA, expr) RSQ
    { Elist l }
| LP e = expr RP
103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118
    { e.expr_desc }
;

%inline binop:
| PLUS  { Badd }
| MINUS { Bsub }
| TIMES { Bmul }
| DIV   { Bdiv }
| MOD   { Bmod }
| c=CMP { c    }
| AND   { Band }
| OR    { Bor  }
;

located(X):
| X { mk_stmt (floc $startpos $endpos) $1 }
119 120
;

121 122 123
suite: located(suite_desc) { $1 };

suite_desc:
124
| s = simple_stmt NEWLINE
125
    { s.stmt_desc }
126 127 128 129
| NEWLINE BEGIN l = nonempty_list(stmt) END
    { Sblock l }
;

130 131 132
stmt: located(stmt_desc) { $1 };

stmt_desc:
133
| s = simple_stmt NEWLINE
134
    { s.stmt_desc }
135
| IF c = expr COLON s = suite
136
    { Sif (c, s, mk_stmt (floc $startpos $endpos) (Sblock [])) }
137 138
| IF c = expr COLON s1 = suite ELSE COLON s2 = suite
    { Sif (c, s1, s2) }
139 140 141 142
| WHILE e = expr COLON s = simple_stmt NEWLINE
    { Swhile (e, empty_annotation, s) }
| WHILE e = expr COLON NEWLINE BEGIN a=loop_annotation l=nonempty_list(stmt) END
    { Swhile (e, a, mk_stmt (floc $startpos(l) $endpos(l)) (Sblock l)) }
143 144 145 146
| FOR x = ident IN e = expr COLON s = suite
    { Sfor (x, e, s) }
;

147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163
loop_annotation:
| (* epsilon *)
    { empty_annotation }
| invariant loop_annotation
    { let a = $2 in { a with loop_invariant = $1 :: a.loop_invariant } }
| variant loop_annotation
    { let a = $2 in { a with loop_variant = variant_union $1 a.loop_variant } }

invariant:
| INVARIANT i=term { i }

variant:
| VARIANT l=comma_list1(term) { List.map (fun t -> t, None) l }

simple_stmt: located(simple_stmt_desc) { $1 };

simple_stmt_desc:
164 165 166 167 168 169 170 171 172 173 174 175 176
| RETURN e = expr
    { Sreturn e }
| id = ident EQUAL e = expr
    { Sassign (id, e) }
| e1 = expr LSQ e2 = expr RSQ EQUAL e3 = expr
    { Sset (e1, e2, e3) }
| PRINT e = expr
    { Sprint e }
| e = expr
    { Seval e }
;

ident:
177
  id = IDENT { mk_id id $startpos $endpos }
178 179
;

180 181 182 183 184 185 186 187 188 189 190
/* logic */

mk_term(X): d = X { mk_term d $startpos $endpos }

term: t = mk_term(term_) { t }

term_:
| ident       { Tident (Qident $1) }
| INTEGER     { Tconst (Number.ConstInt ((Number.int_const_dec $1))) }
| TRUE        { Ttrue }
| FALSE       { Tfalse }
191

192 193
comma_list1(X):
| separated_nonempty_list(COMMA, X) { $1 }