py_parser.mly 8.8 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  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
  let () = Exn_printer.register (fun fmt exn -> match exn with
18 19 20
    | Error -> Format.fprintf fmt "syntax error"
    | _ -> raise exn)

21
  let floc s e = Loc.extract (s,e)
Andrei Paskevich's avatar
Andrei Paskevich committed
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 25
  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 }
26
  let mk_stmt loc d = Dstmt { stmt_desc = d; stmt_loc = loc }
27 28 29 30 31 32 33

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

34 35
  let get_op s e = Qident (mk_id (Ident.mixfix "[]") s e)
  let set_op s e = Qident (mk_id (Ident.mixfix "[<-]") s e)
36

37
  let empty_spec = {
38 39 40
    sp_pre     = [];    sp_post    = [];  sp_xpost  = [];
    sp_reads   = [];    sp_writes  = [];  sp_alias  = [];
    sp_variant = [];
41 42 43 44 45 46 47 48 49
    sp_checkrw = false; sp_diverge = false;
  }

  let spec_union s1 s2 = {
    sp_pre     = s1.sp_pre @ s2.sp_pre;
    sp_post    = s1.sp_post @ s2.sp_post;
    sp_xpost   = s1.sp_xpost @ s2.sp_xpost;
    sp_reads   = s1.sp_reads @ s2.sp_reads;
    sp_writes  = s1.sp_writes @ s2.sp_writes;
50
    sp_alias   = s1.sp_alias @ s2.sp_alias;
51 52 53 54 55
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
  }

56 57
%}

58 59
%token <string> INTEGER
%token <string> STRING
60 61
%token <Py_ast.binop> CMP
%token <string> IDENT
62
%token DEF IF ELSE ELIF RETURN WHILE FOR IN AND OR NOT NONE TRUE FALSE
63
%token FROM IMPORT BREAK
64
%token EOF
65
%token LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ COMMA EQUAL COLON BEGIN END NEWLINE
66
%token PLUS MINUS TIMES DIV MOD
67
(* annotations *)
68
%token INVARIANT VARIANT ASSUME ASSERT CHECK REQUIRES ENSURES LABEL
69
%token FUNCTION PREDICATE
70
%token ARROW LARROW LRARROW FORALL EXISTS DOT THEN LET
71 72

(* precedences *)
73

74 75
%nonassoc IN
%nonassoc DOT ELSE
76
%right ARROW LRARROW
77 78
%right OR
%right AND
79
%nonassoc NOT
80
%right CMP
81 82
%left PLUS MINUS
%left TIMES DIV MOD
83 84
%nonassoc unary_minus prec_prefix_op
%nonassoc LEFTSQ
85 86 87 88

%start file

%type <Py_ast.file> file
89
%type <Py_ast.decl> stmt
90 91 92 93

%%

file:
94 95 96 97
| NEWLINE* EOF
    { [] }
| NEWLINE? dl=nonempty_list(decl) NEWLINE? EOF
    { dl }
98 99
;

100 101 102 103 104 105
decl:
| import { $1 }
| def    { $1 }
| stmt   { $1 }
| func   { $1 }

106
import:
107 108 109 110 111 112 113 114
| FROM m=ident IMPORT l=separated_list(COMMA, ident) NEWLINE
  { Dimport (m, l) }

func:
| FUNCTION id=ident LEFTPAR l=separated_list(COMMA, ident) RIGHTPAR NEWLINE
  { Dlogic (true, id, l) }
| PREDICATE id=ident LEFTPAR l=separated_list(COMMA, ident) RIGHTPAR NEWLINE
  { Dlogic (false, id, l) }
115

116
def:
117
| DEF f = ident LEFTPAR x = separated_list(COMMA, ident) RIGHTPAR
118
  COLON NEWLINE BEGIN s=spec l=nonempty_list(stmt) END
119
    { Ddef (f, x, s, l) }
120 121
;

122 123 124 125 126 127 128 129 130
spec:
| (* epsilon *)     { empty_spec }
| single_spec spec  { spec_union $1 $2 }

single_spec:
| REQUIRES t=term NEWLINE
    { { empty_spec with sp_pre = [t] } }
| ENSURES e=ensures NEWLINE
    { { empty_spec with sp_post = [floc $startpos(e) $endpos(e), e] } }
131 132
| variant
    { { empty_spec with sp_variant = $1 } }
133 134 135 136

ensures:
| term
    { let id = mk_id "result" $startpos $endpos in
137
      [mk_pat (Pvar id) $startpos $endpos, $1] }
138

139
expr:
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
| 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 }
155 156
| id = ident
    { Eident id }
157
| e1 = expr LEFTSQ e2 = expr RIGHTSQ
158 159 160 161 162 163 164
    { 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) }
165 166 167 168
| e1 = expr TIMES e2 = expr
    { match e1.expr_desc with
      | Elist [e1] -> Emake (e1, e2)
      | _ -> Ebinop (Bmul, e1, e2) }
169
| f = ident LEFTPAR e = separated_list(COMMA, expr) RIGHTPAR
170
    { Ecall (f, e) }
171
| LEFTSQ l = separated_list(COMMA, expr) RIGHTSQ
172
    { Elist l }
173
| LEFTPAR e = expr RIGHTPAR
174 175 176 177 178 179 180 181 182 183 184 185 186 187 188
    { e.expr_desc }
;

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

located(X):
| X { mk_stmt (floc $startpos $endpos) $1 }
189 190
;

191
suite:
192
| s = simple_stmt NEWLINE
193
    { [s] }
194
| NEWLINE BEGIN l = nonempty_list(stmt) END
195
    { l }
196 197
;

198 199 200
stmt:
| located(stmt_desc)      { $1 }
| s = simple_stmt NEWLINE { s }
201 202

stmt_desc:
203
| IF c = expr COLON s1 = suite s2=else_branch
204
    { Sif (c, s1, s2) }
205
| WHILE e = expr COLON b=loop_body
206
    { let i, v, l = b in Swhile (e, i, v, l) }
207
| FOR x = ident IN e = expr COLON b=loop_body
208
    { let i, _, l = b in Sfor (x, e, i, l) }
209 210
;

211 212 213 214 215 216 217 218 219
else_branch:
| /* epsilon */
    { [] }
| ELSE COLON s2=suite
    { s2 }
| ELIF c=expr COLON s1=suite s2=else_branch
    { [mk_stmt (floc $startpos $endpos) (Sif (c, s1, s2))] }


220 221
loop_body:
| s = simple_stmt NEWLINE
222
  { [], [], [s] }
223
| NEWLINE BEGIN a=loop_annotation l=nonempty_list(stmt) END
224
  { fst a, snd a, l }
225

226 227
loop_annotation:
| (* epsilon *)
228
    { [], [] }
229
| invariant loop_annotation
230
    { let (i, v) = $2 in ($1::i, v) }
231
| variant loop_annotation
232
    { let (i, v) = $2 in (i, variant_union $1 v) }
233 234

invariant:
235
| INVARIANT i=term NEWLINE { i }
236 237

variant:
238
| VARIANT l=comma_list1(term) NEWLINE { List.map (fun t -> t, None) l }
239 240 241 242

simple_stmt: located(simple_stmt_desc) { $1 };

simple_stmt_desc:
243 244 245 246
| RETURN e = expr
    { Sreturn e }
| id = ident EQUAL e = expr
    { Sassign (id, e) }
247
| e1 = expr LEFTSQ e2 = expr RIGHTSQ EQUAL e3 = expr
248
    { Sset (e1, e2, e3) }
249 250
| k=assertion_kind t = term
    { Sassert (k, t) }
251 252
| e = expr
    { Seval e }
253 254
| BREAK
    { Sbreak }
255 256
| LABEL id=ident
    { Slabel id }
257 258
;

259
assertion_kind:
260 261 262
| ASSERT  { Expr.Assert }
| ASSUME  { Expr.Assume }
| CHECK   { Expr.Check }
263

264
ident:
265
  id = IDENT { mk_id id $startpos $endpos }
266 267
;

268 269 270 271 272 273 274
/* logic */

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

term: t = mk_term(term_) { t }

term_:
275 276
| term_arg_
    { match $1 with (* break the infix relation chain *)
277 278 279
      | Tinfix (l,o,r) -> Tinnfix (l,o,r)
      | Tbinop (l,o,r) -> Tbinnop (l,o,r)
      | d -> d }
280
| NOT term
281
    { Tnot $2 }
282 283
| o = prefix_op ; t = term %prec prec_prefix_op
    { Tidapp (Qident o, [t]) }
284 285
| l = term ; o = bin_op ; r = term
    { Tbinop (l, o, r) }
286
| l = term ; o = infix_op_1 ; r = term
287
    { Tinfix (l, o, r) }
288
| l = term ; o = infix_op_234 ; r = term
289
    { Tidapp (Qident o, [l; r]) }
290 291 292 293 294 295 296
| IF term THEN term ELSE term
    { Tif ($2, $4, $6) }
| LET id=ident EQUAL t1=term IN t2=term
    { Tlet (id, t1, t2) }
| q=quant l=comma_list1(ident) DOT t=term
    { let var id = id.id_loc, Some id, false, None in
      Tquant (q, List.map var l, [], t) }
297 298
| id=ident LEFTPAR l=separated_list(COMMA, term) RIGHTPAR
    { Tidapp (Qident id, l) }
299

300
quant:
301 302
| FORALL  { Dterm.DTforall }
| EXISTS  { Dterm.DTexists }
303 304

term_arg: mk_term(term_arg_) { $1 }
305 306

term_arg_:
307
| ident       { Tident (Qident $1) }
308
| INTEGER     { Tconst (Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec $1})) }
309
| NONE        { Ttuple [] }
310 311
| TRUE        { Ttrue }
| FALSE       { Tfalse }
312 313 314 315 316 317
| term_sub_                 { $1 }

term_sub_:
| LEFTPAR term RIGHTPAR                             { $2.term_desc }
| term_arg LEFTSQ term RIGHTSQ
    { Tidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
318 319
| term_arg LEFTSQ term LARROW term RIGHTSQ
    { Tidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
320

321
%inline bin_op:
322 323 324 325
| ARROW   { Dterm.DTimplies }
| LRARROW { Dterm.DTiff }
| OR      { Dterm.DTor }
| AND     { Dterm.DTand }
326

327
%inline infix_op_1:
328
| c=CMP  { let op = match c with
329
          | Beq  -> "="
330 331 332 333
          | Bneq -> "<>"
          | Blt  -> "<"
          | Ble  -> "<="
          | Bgt  -> ">"
334 335
          | Bge  -> ">="
          | Badd|Bsub|Bmul|Bdiv|Bmod|Band|Bor -> assert false in
336
           mk_id (Ident.infix op) $startpos $endpos }
337

338
%inline prefix_op:
339
| MINUS { mk_id (Ident.prefix "-")  $startpos $endpos }
340

341 342 343
%inline infix_op_234:
| DIV    { mk_id "div" $startpos $endpos }
| MOD    { mk_id "mod" $startpos $endpos }
344 345 346
| PLUS   { mk_id (Ident.infix "+") $startpos $endpos }
| MINUS  { mk_id (Ident.infix "-") $startpos $endpos }
| TIMES  { mk_id (Ident.infix "*") $startpos $endpos }
347

348 349
comma_list1(X):
| separated_nonempty_list(COMMA, X) { $1 }