python: logical annotations

.gitignore

@@ -217,6 +217,7 @@ pvsbin/
 /plugins/python/py_parser.ml
 /plugins/python/py_parser.mli
 /plugins/python/test/
+/plugins/python/py_parser.conflicts
 
 # /drivers
 /drivers/coq-realizations.aux

plugins/python/py_ast.ml

@@ -54,6 +54,7 @@ and stmt_desc =
   | Sfor of ident * expr * stmt
   | Seval of expr
   | Sset of expr * expr * expr (* e1[e2] = e3 *)
+  | Sassert of Ptree.term
 
 and def = ident * ident list * stmt
 

plugins/python/py_lexer.mll

@@ -36,10 +36,20 @@
   let string_buffer = Buffer.create 1024
 
   let stack = ref [0]  (* indentation stack *)
+
   let rec unindent n = match !stack with
     | m :: _ when m = n -> []
     | m :: st when m > n -> stack := st; END :: unindent n
     | _ -> raise (Lexing_error "bad indentation")
+
+  let update_stack n =
+    match !stack with
+    | m :: _ when m < n ->
+      stack := n :: !stack;
+      [NEWLINE; BEGIN]
+    | _ ->
+      NEWLINE :: unindent n
+
 }
 
 let letter = ['a'-'z' 'A'-'Z']
@@ -47,22 +57,17 @@ let digit = ['0'-'9']
 let ident = letter (letter | digit | '_')*
 let integer = ['0'-'9']+
 let space = ' ' | '\t'
-let comment = "#" [^'\n']*
+let comment = "#" [^'#''\n'] [^'\n']*
 
 rule next_tokens = parse
-  | '\n'
-      { newline lexbuf;
-	let n = indentation lexbuf in
-	match !stack with
-	  | m :: _ when m < n ->
-	      stack := n :: !stack;
-	      [NEWLINE; BEGIN]
-	  | _ ->
-	      NEWLINE :: unindent n
-      }
+  | '\n'    { newline lexbuf; update_stack (indentation lexbuf) }
   | (space | comment)+
-      { next_tokens lexbuf }
-  | ident as id { [id_or_kwd id] }
+            { next_tokens lexbuf }
+  | "##" space* "invariant" space+ { [INVARIANT] }
+  | "##" space* "variant"   space+ { [VARIANT] }
+  | "##" space* "assert"    space+ { [ASSERT] }
+  | ident as id
+            { [id_or_kwd id] }
   | '+'     { [PLUS] }
   | '-'     { [MINUS] }
   | '*'     { [TIMES] }
@@ -81,14 +86,19 @@ rule next_tokens = parse
   | ']'     { [RSQ] }
   | ','     { [COMMA] }
   | ':'     { [COLON] }
+  (* logic symbols *)
+  | "->"    { [ARROW] }
+  | "->"    { [LRARROW] }
   | integer as s
             { [INTEGER s] }
   | '"'     { [STRING (string lexbuf)] }
   | eof     { [EOF] }
   | _ as c  { raise (Lexing_error ("illegal character: " ^ String.make 1 c)) }
 
+(* count the indentation, i.e. the number of space characters from bol *)
 and indentation = parse
   | (space | comment)* '\n'
+      (* skip empty lines *)
       { newline lexbuf; indentation lexbuf }
   | space* as s
       { String.length s }

plugins/python/py_main.ml

@@ -14,7 +14,7 @@ open Mlw_module
 open Ptree
 open Stdlib
 
-let debug = Debug.register_flag "mini-python"
+let debug = Debug.register_flag "python"
   ~desc:"mini-python plugin debug flag"
 
 let mk_id ?(loc=Loc.dummy_position) name =
@@ -22,6 +22,8 @@ let mk_id ?(loc=Loc.dummy_position) name =
 
 let mk_expr ?(loc=Loc.dummy_position) d =
   { expr_desc = d; expr_loc = loc }
+let mk_term ?(loc=Loc.dummy_position) d =
+  { term_desc = d; term_loc = loc }
 let mk_unit ~loc =
   mk_expr ~loc (Etuple [])
 
@@ -37,12 +39,24 @@ let empty_spec = {
 }
 
 type env = {
-  vars: unit Hstr.t;
+  vars: ident Hstr.t;
 }
 
 let infix  ~loc s = Qident (mk_id ~loc ("infix "  ^ s))
 let prefix ~loc s = Qident (mk_id ~loc ("prefix " ^ s))
 
+(* dereference all variables from the environment *)
+let deref env t =
+  let deref _ ({id_loc=loc} as id) t =
+    let tid = mk_term ~loc (Tident (Qident id)) in
+    let tid = mk_term ~loc (Tidapp (prefix ~loc "!", [tid])) in
+    mk_term ~loc:t.term_loc (Tlet (id, tid, t)) in
+  Hstr.fold deref env.vars t
+
+let loop_annotation env a =
+  { loop_invariant = List.map (deref env) a.loop_invariant;
+    loop_variant   = List.map (fun (t, o) -> deref env t, o) a.loop_variant }
+
 let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
   | Py_ast.Enone ->
     mk_unit ~loc
@@ -78,11 +92,11 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
     mk_expr ~loc (Eidapp (prefix ~loc "-", [expr env e]))
   | Py_ast.Eunop (Py_ast.Unot, e) ->
     mk_expr ~loc (Eidapp (Qident (mk_id ~loc "not"), [expr env e]))
-  | Py_ast.Ecall (id, el) ->
+  | Py_ast.Ecall (_id, _el) ->
     assert false (*TODO*)
-  | Py_ast.Elist el ->
+  | Py_ast.Elist _el ->
     assert false
-  | Py_ast.Eget (e1, e2) ->
+  | Py_ast.Eget (_e1, _e2) ->
     assert false (*TODO*)
 
 let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
@@ -96,8 +110,8 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
   | Py_ast.Sif (e, s1, s2) ->
     mk_expr ~loc (Eif (expr env e, stmt env s1, stmt env s2))
   | Py_ast.Swhile (e, ann, s) ->
-    mk_expr ~loc (Ewhile (expr env e, ann, stmt env s))
-  | Py_ast.Sreturn e ->
+    mk_expr ~loc (Ewhile (expr env e, loop_annotation env ann, stmt env s))
+  | Py_ast.Sreturn _e ->
     assert false (*TODO*)
   | Py_ast.Sassign (id, e) ->
     let e = expr env e in
@@ -106,10 +120,12 @@ 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, _s) ->
     assert false (*TODO*)
-  | Py_ast.Sset (e1, e2, e3) ->
+  | Py_ast.Sset (_e1, _e2, _e3) ->
     assert false (*TODO*)
+  | Py_ast.Sassert t ->
+    mk_expr ~loc (Eassert (Aassert, deref env t))
 
 and block env loc = function
   | [] ->
@@ -117,7 +133,7 @@ and block env loc = function
   | { Py_ast.stmt_loc = loc; stmt_desc = Py_ast.Sassign (id, e) } :: sl
     when not (Hstr.mem env.vars id.id_str) ->
     let e = expr env e in (* check e *before* adding id to environment *)
-    Hstr.add env.vars id.id_str ();
+    Hstr.add env.vars id.id_str id;
     let e1 = mk_expr ~loc (Eidapp (Qident (mk_id ~loc "ref"), [e])) in
     mk_expr ~loc (Elet (id, Gnone, e1, block env loc sl))
   | { Py_ast.stmt_loc = loc } as s :: sl ->

plugins/python/py_parser.mly

@@ -29,6 +29,10 @@
   let empty_annotation =
     { loop_invariant = []; loop_variant = [] }
 
+  let infix  s = "infix "  ^ s
+  let prefix s = "prefix " ^ s
+  let mixfix s = "mixfix " ^ s
+
 %}
 
 %token <string> INTEGER
@@ -41,12 +45,14 @@
 %token PLUS MINUS TIMES DIV MOD
 
 /* annotations */
-%token INVARIANT VARIANT
+%token INVARIANT VARIANT ASSERT
+%token ARROW LRARROW
 
+%right ARROW LRARROW
 %left OR
 %left AND
 %nonassoc NOT
-%nonassoc CMP
+%left CMP
 %left PLUS MINUS
 %left TIMES DIV MOD
 %nonassoc unary_minus
@@ -153,10 +159,10 @@ loop_annotation:
     { let a = $2 in { a with loop_variant = variant_union $1 a.loop_variant } }
 
 invariant:
-| INVARIANT i=term { i }
+| INVARIANT i=term NEWLINE { i }
 
 variant:
-| VARIANT l=comma_list1(term) { List.map (fun t -> t, None) l }
+| VARIANT l=comma_list1(term) NEWLINE { List.map (fun t -> t, None) l }
 
 simple_stmt: located(simple_stmt_desc) { $1 };
 
@@ -169,6 +175,8 @@ simple_stmt_desc:
     { Sset (e1, e2, e3) }
 | PRINT e = expr
     { Sprint e }
+| ASSERT t = term
+    { Sassert t }
 | e = expr
     { Seval e }
 ;
@@ -184,10 +192,48 @@ mk_term(X): d = X { mk_term d $startpos $endpos }
 term: t = mk_term(term_) { t }
 
 term_:
+| 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) }
+| 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]) }
+
+(* term_arg: mk_term(term_arg_) { $1 } *)
+
+term_arg_:
 | ident       { Tident (Qident $1) }
 | INTEGER     { Tconst (Number.ConstInt ((Number.int_const_dec $1))) }
 | TRUE        { Ttrue }
 | FALSE       { Tfalse }
 
+%inline bin_op:
+| ARROW   { Timplies }
+| LRARROW { Tiff }
+| OR      { Tor }
+| AND     { Tand }
+
+%inline infix_op:
+| PLUS   { mk_id (infix "+") $startpos $endpos }
+| MINUS  { mk_id (infix "-") $startpos $endpos }
+| TIMES  { mk_id (infix "*") $startpos $endpos }
+| c=CMP  { let op = match c with
+          | Beq -> "="
+          | Bneq -> "<>"
+          | Blt  -> "<"
+          | Ble  -> "<="
+          | Bgt  -> ">"
+          | Bge  -> ">=" in
+           mk_id (infix op) $startpos $endpos }
+
+%inline div_mod_op:
+| DIV  { mk_id "div" $startpos $endpos }
+| MOD  { mk_id "mod" $startpos $endpos }
+
 comma_list1(X):
 | separated_nonempty_list(COMMA, X) { $1 }

plugins/python/test.py

@@ -2,8 +2,12 @@
 a = 0
 b = 1
 while b < 100:
+  ## invariant b >= a >= 0
+  ## invariant b >= 1
+  ## variant 200 - b - a
   print(a)
   b = a+b
+  ## assert b >= 1
   a = b-a
 
 # Local Variables: