diff --git a/modules/python.mlw b/modules/python.mlw
index 512007363661b39a7d0c79ac125162df4407c9f3..a171e300b0343058055e18d0e529e4c57ac14938 100644
--- a/modules/python.mlw
+++ b/modules/python.mlw
@@ -30,4 +30,9 @@ module Python
ensures { S.length !result = u - l }
ensures { forall i. l <= i < u -> result[i] = i }
+ (* TODO: specify division and modulus according to
+ https://docs.python.org/3/reference/expressions.html *)
+ function div int int : int
+ function mod int int : int
+
end
diff --git a/plugins/python/py_ast.ml b/plugins/python/py_ast.ml
index 75b63efa5404cc7bae3099479613afd38423a823..7da0690120165cb10a09f1f1451334b145b0be30 100644
--- a/plugins/python/py_ast.ml
+++ b/plugins/python/py_ast.ml
@@ -50,10 +50,10 @@ and stmt_desc =
| Sassign of ident * expr
| Sprint of expr
| Swhile of expr * Ptree.loop_annotation * block
- | Sfor of ident * expr * block
+ | Sfor of ident * expr * Ptree.loop_annotation * block
| Seval of expr
| Sset of expr * expr * expr (* e1[e2] = e3 *)
- | Sassert of Ptree.term
+ | Sassert of Ptree.assertion_kind * Ptree.term
and block = stmt list
diff --git a/plugins/python/py_lexer.mll b/plugins/python/py_lexer.mll
index 63d2afceaf4e5549b7f8c59d2f84ffbb4d43d4eb..da0fb6ede563f8c01eef0cbc6e7ff0ac04ed5234 100644
--- a/plugins/python/py_lexer.mll
+++ b/plugins/python/py_lexer.mll
@@ -16,6 +16,10 @@
exception Lexing_error of string
+ let () = Why3.Exn_printer.register (fun fmt exn -> match exn with
+ | Lexing_error s -> Format.fprintf fmt "syntax error: %s" s
+ | _ -> raise exn)
+
let id_or_kwd =
let h = Hashtbl.create 32 in
List.iter (fun (s, tok) -> Hashtbl.add h s tok)
@@ -67,12 +71,15 @@ rule next_tokens = parse
| "##" space* "invariant" space+ { [INVARIANT] }
| "##" space* "variant" space+ { [VARIANT] }
| "##" space* "assert" space+ { [ASSERT] }
+ | "##" space* "assume" space+ { [ASSUME] }
+ | "##" space* "check" space+ { [CHECK] }
+ | "##" { raise (Lexing_error "expecting an annotation") }
| ident as id
{ [id_or_kwd id] }
| '+' { [PLUS] }
| '-' { [MINUS] }
| '*' { [TIMES] }
- | '/' { [DIV] }
+ | "//" { [DIV] }
| '%' { [MOD] }
| '=' { [EQUAL] }
| "==" { [CMP Beq] }
diff --git a/plugins/python/py_main.ml b/plugins/python/py_main.ml
index c4f49af8dd619a44a86ee3bb3c1c0718c9a12c0b..87b72c96008e3490ef8c4a704b3085f4517a1ff9 100644
--- a/plugins/python/py_main.ml
+++ b/plugins/python/py_main.ml
@@ -80,8 +80,8 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
| Py_ast.Badd -> Eidapp (infix ~loc "+", [e1; e2])
| Py_ast.Bsub -> Eidapp (infix ~loc "-", [e1; e2])
| Py_ast.Bmul -> Eidapp (infix ~loc "*", [e1; e2])
- | Py_ast.Bdiv -> assert false (*TODO*)
- | Py_ast.Bmod -> assert false (*TODO*)
+ | Py_ast.Bdiv -> Eidapp (Qident (mk_id ~loc "div"), [e1; e2])
+ | Py_ast.Bmod -> Eidapp (Qident (mk_id ~loc "mod"), [e1; e2])
| Py_ast.Beq -> Eidapp (infix ~loc "=", [e1; e2])
| Py_ast.Bneq -> Eidapp (infix ~loc "<>", [e1; e2])
| Py_ast.Blt -> Eidapp (infix ~loc "<", [e1; e2])
@@ -120,13 +120,13 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
mk_expr ~loc (Einfix (x, mk_id ~loc "infix :=", e))
else
block env ~loc [s]
- | Py_ast.Sfor (_id, _e, _s) ->
+ | Py_ast.Sfor (_id, _e, _a, _s) ->
assert false (*TODO*)
| Py_ast.Sset (e1, e2, e3) ->
mk_expr ~loc (Eidapp (mixfix ~loc "[]<-",
[expr env e1; expr env e2; expr env e3]))
- | Py_ast.Sassert t ->
- mk_expr ~loc (Eassert (Aassert, deref env t))
+ | Py_ast.Sassert (k, t) ->
+ mk_expr ~loc (Eassert (k, deref env t))
and block env ?(loc=Loc.dummy_position) = function
| [] ->
diff --git a/plugins/python/py_parser.mly b/plugins/python/py_parser.mly
index 5ce06cd596cea0bca2aae9742d7352d5f4c84447..67ef15971f9d2cd9212e310c76d79d09d3889b87 100644
--- a/plugins/python/py_parser.mly
+++ b/plugins/python/py_parser.mly
@@ -14,6 +14,10 @@
open Ptree
open Py_ast
+ let () = Why3.Exn_printer.register (fun fmt exn -> match exn with
+ | Error -> Format.fprintf fmt "syntax error"
+ | _ -> raise exn)
+
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 }
@@ -46,7 +50,7 @@
%token LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ COMMA EQUAL COLON BEGIN END NEWLINE
%token PLUS MINUS TIMES DIV MOD
(* annotations *)
-%token INVARIANT VARIANT ASSERT
+%token INVARIANT VARIANT ASSUME ASSERT CHECK
%token ARROW LRARROW FORALL EXISTS DOT THEN LET
(* precedences *)
@@ -145,14 +149,18 @@ stmt_desc:
{ Sif (c, s, []) }
| IF c = expr COLON s1 = suite ELSE COLON s2 = suite
{ Sif (c, s1, s2) }
-| 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, l) }
-| FOR x = ident IN e = expr COLON s = suite
- { Sfor (x, e, s) }
+| 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
+ { let a, l = b in Sfor (x, e, a, l) }
;
+loop_body:
+| s = simple_stmt NEWLINE
+ { empty_annotation, [s] }
+| NEWLINE BEGIN a=loop_annotation l=nonempty_list(stmt) END
+ { a, l }
+
loop_annotation:
| (* epsilon *)
{ empty_annotation }
@@ -178,12 +186,17 @@ simple_stmt_desc:
{ Sset (e1, e2, e3) }
| PRINT e = expr
{ Sprint e }
-| ASSERT t = term
- { Sassert t }
+| k=assertion_kind t = term
+ { Sassert (k, t) }
| e = expr
{ Seval e }
;
+assertion_kind:
+| ASSERT { Aassert }
+| ASSUME { Aassume }
+| CHECK { Acheck }
+
ident:
id = IDENT { mk_id id $startpos $endpos }
;
diff --git a/plugins/python/test.py b/plugins/python/test.py
index a01f29b6b2f94d5cabdf32acee24a0931fde2f90..3386b225bf9a96ada6badbc63b9a72f6a4da3eac 100644
--- a/plugins/python/test.py
+++ b/plugins/python/test.py
@@ -9,6 +9,8 @@ while b < 100:
b = a+b
## assert b >= 1
a = b-a
+
+# lists
l = range(0, 10)
## assert forall i. 0 <= i < 10 -> l[i] >= 0
l[2] = 42
@@ -21,6 +23,15 @@ while i < 10:
l[i] = 0
i = i+1
+# arithmetic
+# Python's division is *Euclidean* division
+q = -4 // 3
+## assert q == -2
+r = -4 % 3
+## assert r == 2
+## assert 4 // -3 == -2
+## assert 4 % -3 == -2
+
# Local Variables:
# compile-command: "make -C ../.. && why3 ide test.py"
# End: