py_parser.mly 8.79 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 18 19 20
  let () = Why3.Exn_printer.register (fun fmt exn -> match exn with
    | Error -> Format.fprintf fmt "syntax error"
    | _ -> raise exn)

21 22
  let floc s e = Loc.extract (s,e)
  let mk_id id s e = { id_str = id; id_lab = []; 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 34 35 36

  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 = [] }

37 38
  let get_op s e = Qident (mk_id (Ident.mixfix "[]") s e)
  let set_op s e = Qident (mk_id (Ident.mixfix "[<-]") s e)
39

40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
  let empty_spec = {
    sp_pre     = [];    sp_post    = [];  sp_xpost   = [];
    sp_reads   = [];    sp_writes  = [];  sp_variant = [];
    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;
    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;
  }

57 58
%}

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

(* precedences *)
74

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

%start file

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

%%

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

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

107
import:
108 109 110 111 112 113 114 115
| 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) }
116

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

123 124 125 126 127 128 129 130 131
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] } }
132 133
| variant
    { { empty_spec with sp_variant = $1 } }
134 135 136 137 138 139

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

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

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

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

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

212 213 214 215 216 217 218 219 220
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))] }


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

227 228 229 230 231 232 233 234 235
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:
236
| INVARIANT i=term NEWLINE { i }
237 238

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

simple_stmt: located(simple_stmt_desc) { $1 };

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

260 261 262 263 264
assertion_kind:
| ASSERT  { Aassert }
| ASSUME  { Aassume }
| CHECK   { Acheck }

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

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

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

term: t = mk_term(term_) { t }

term_:
276 277 278 279 280
| term_arg_
    { match $1 with (* break the infix relation chain *)
      | Tinfix (l,o,r) -> Tinnfix (l,o,r) | d -> d }
| NOT term
    { Tunop (Tnot, $2) }
281 282
| o = prefix_op ; t = term %prec prec_prefix_op
    { Tidapp (Qident o, [t]) }
283 284 285 286 287 288
| l = term ; o = bin_op ; r = term
    { Tbinop (l, o, r) }
| l = term ; o = infix_op ; r = term
    { Tinfix (l, o, r) }
| l = term ; o = div_mod_op ; r = term
    { Tidapp (Qident o, [l; r]) }
289 290 291 292 293 294 295
| 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) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
296 297
| id=ident LEFTPAR l=separated_list(COMMA, term) RIGHTPAR
    { Tidapp (Qident id, l) }
298

299 300 301 302 303
quant:
| FORALL  { Tforall }
| EXISTS  { Texists }

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

term_arg_:
306
| ident       { Tident (Qident $1) }
307
| INTEGER     { Tconst (Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec $1})) }
308
| NONE        { Ttuple [] }
309 310
| TRUE        { Ttrue }
| FALSE       { Tfalse }
311 312 313 314 315 316
| 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]) }
317 318
| term_arg LEFTSQ term LARROW term RIGHTSQ
    { Tidapp (set_op $startpos($2) $endpos($2), [$1;$3;$5]) }
319

320 321 322 323 324 325 326
%inline bin_op:
| ARROW   { Timplies }
| LRARROW { Tiff }
| OR      { Tor }
| AND     { Tand }

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

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

343 344 345 346
%inline div_mod_op:
| DIV  { mk_id "div" $startpos $endpos }
| MOD  { mk_id "mod" $startpos $endpos }

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