python: more term syntax

.gitignore

@@ -291,6 +291,7 @@ pvsbin/
 /modules/pqueue/
 /modules/mach/array/
 /modules/mach/int/
+/modules/python/
 
 # Try Why3
 /src/trywhy3/trywhy3.byte

modules/python.mlw

+
+module Python
+
+  use import int.Int
+  use import ref.Ref
+  use seq.Seq as S
+
+  type list 'a = ref (S.seq 'a)
+
+  function ([]) (l: list 'a) (i: int) : 'a =
+    S.([]) !l i
+
+  let ([]) (l: list 'a) (i: int) : 'a
+    requires { 0 <= i < S.length !l }
+    ensures  { result = l[i] }
+  = S.([]) !l i
+
+  val range (l u: int) : list int
+    requires { l <= u }
+    ensures  { forall i. l <= i < u -> result[i] = i }
+
+end

plugins/python/py_lexer.mll

@@ -23,9 +23,10 @@
        "return", RETURN; "print", PRINT; "while", WHILE;
        "for", FOR; "in", IN;
        "and", AND; "or", OR; "not", NOT;
-       "True", TRUE;
-       "False", FALSE;
-       "None", NONE;];
+       "True", TRUE; "False", FALSE; "None", NONE;
+       (* annotations *)
+       "forall", FORALL; "exists", EXISTS; "then", THEN; "let", LET;
+      ];
    fun s -> try Hashtbl.find h s with Not_found -> IDENT s
 
   let newline lexbuf =
@@ -80,15 +81,16 @@ rule next_tokens = parse
   | "<="    { [CMP Ble] }
   | ">"     { [CMP Bgt] }
   | ">="    { [CMP Bge] }
-  | '('     { [LP] }
-  | ')'     { [RP] }
-  | '['     { [LSQ] }
-  | ']'     { [RSQ] }
+  | '('     { [LEFTPAR] }
+  | ')'     { [RIGHTPAR] }
+  | '['     { [LEFTSQ] }
+  | ']'     { [RIGHTSQ] }
   | ','     { [COMMA] }
   | ':'     { [COLON] }
   (* logic symbols *)
   | "->"    { [ARROW] }
   | "->"    { [LRARROW] }
+  | "."     { [DOT] }
   | integer as s
             { [INTEGER s] }
   | '"'     { [STRING (string lexbuf)] }

plugins/python/py_main.ml

@@ -44,6 +44,7 @@ type env = {
 
 let infix  ~loc s = Qident (mk_id ~loc ("infix "  ^ s))
 let prefix ~loc s = Qident (mk_id ~loc ("prefix " ^ s))
+let mixfix ~loc s = Qident (mk_id ~loc ("mixfix " ^ s))
 
 (* dereference all variables from the environment *)
 let deref env t =
@@ -92,12 +93,12 @@ 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) ->
-    assert false (*TODO*)
+  | Py_ast.Ecall (id, el) ->
+    mk_expr ~loc (Eidapp (Qident id, List.map (expr env) el))
   | Py_ast.Elist _el ->
     assert false
-  | Py_ast.Eget (_e1, _e2) ->
-    assert false (*TODO*)
+  | Py_ast.Eget (e1, e2) ->
+    mk_expr ~loc (Eidapp (mixfix ~loc "[]", [expr env e1; expr env e2]))
 
 let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
   match d with
@@ -161,7 +162,8 @@ let read_channel env path file c =
     let q = Qdot (Qident (mk_id f), mk_id m) in
     let use = {use_theory = q; use_import = Some (true, m) }, None in
     inc.use_clone  Loc.dummy_position use in
-  List.iter use_import ["int", "Int"; "ref", "Ref"; "seq", "Seq"];
+  List.iter use_import
+    ["int", "Int"; "ref", "Ref"; "python", "Python"];
   translate inc f;
   inc.close_module ();
   let mm, _ as res = Mlw_typing.close_file () in

plugins/python/py_parser.mly

@@ -33,6 +33,8 @@
   let prefix s = "prefix " ^ s
   let mixfix s = "mixfix " ^ s
 
+  let get_op s e = Qident (mk_id (mixfix "[]") s e)
+
 %}
 
 %token <string> INTEGER
@@ -41,13 +43,16 @@
 %token <string> IDENT
 %token DEF IF ELSE RETURN PRINT WHILE FOR IN AND OR NOT NONE TRUE FALSE
 %token EOF
-%token LP RP LSQ RSQ COMMA EQUAL COLON BEGIN END NEWLINE
+%token LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ COMMA EQUAL COLON BEGIN END NEWLINE
 %token PLUS MINUS TIMES DIV MOD
-
-/* annotations */
+(* annotations *)
 %token INVARIANT VARIANT ASSERT
-%token ARROW LRARROW
+%token ARROW LRARROW FORALL EXISTS DOT THEN LET
+
+(* precedences *)
 
+%nonassoc IN
+%nonassoc DOT ELSE
 %right ARROW LRARROW
 %left OR
 %left AND
@@ -55,8 +60,8 @@
 %left CMP
 %left PLUS MINUS
 %left TIMES DIV MOD
-%nonassoc unary_minus
-%nonassoc LSQ
+%nonassoc unary_minus prec_prefix_op
+%nonassoc LEFTSQ
 
 %start file
 
@@ -70,7 +75,7 @@ file:
 ;
 
 def:
-| DEF f = ident LP x = separated_list(COMMA, ident) RP
+| DEF f = ident LEFTPAR x = separated_list(COMMA, ident) RIGHTPAR
   COLON s = suite
     { f, x, s }
 ;
@@ -93,7 +98,7 @@ expr_desc:
     { Estring s }
 | id = ident
     { Eident id }
-| e1 = expr LSQ e2 = expr RSQ
+| e1 = expr LEFTSQ e2 = expr RIGHTSQ
     { Eget (e1, e2) }
 | MINUS e1 = expr %prec unary_minus
     { Eunop (Uneg, e1) }
@@ -101,11 +106,11 @@ expr_desc:
     { Eunop (Unot, e1) }
 | e1 = expr o = binop e2 = expr
     { Ebinop (o, e1, e2) }
-| f = ident LP e = separated_list(COMMA, expr) RP
+| f = ident LEFTPAR e = separated_list(COMMA, expr) RIGHTPAR
     { Ecall (f, e) }
-| LSQ l = separated_list(COMMA, expr) RSQ
+| LEFTSQ l = separated_list(COMMA, expr) RIGHTSQ
     { Elist l }
-| LP e = expr RP
+| LEFTPAR e = expr RIGHTPAR
     { e.expr_desc }
 ;
 
@@ -171,7 +176,7 @@ simple_stmt_desc:
     { Sreturn e }
 | id = ident EQUAL e = expr
     { Sassign (id, e) }
-| e1 = expr LSQ e2 = expr RSQ EQUAL e3 = expr
+| e1 = expr LEFTSQ e2 = expr RIGHTSQ EQUAL e3 = expr
     { Sset (e1, e2, e3) }
 | PRINT e = expr
     { Sprint e }
@@ -197,20 +202,40 @@ term_:
       | Tinfix (l,o,r) -> Tinnfix (l,o,r) | d -> d }
 | NOT term
     { Tunop (Tnot, $2) }
+| prefix_op term %prec prec_prefix_op
+    { Tidapp (Qident $1, [$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]) }
+| 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) }
 
-(* term_arg: mk_term(term_arg_) { $1 } *)
+quant:
+| FORALL  { Tforall }
+| EXISTS  { Texists }
+
+term_arg: mk_term(term_arg_) { $1 }
 
 term_arg_:
 | ident       { Tident (Qident $1) }
 | INTEGER     { Tconst (Number.ConstInt ((Number.int_const_dec $1))) }
+| NONE        { Ttuple [] }
 | TRUE        { Ttrue }
 | FALSE       { Tfalse }
+| 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]) }
 
 %inline bin_op:
 | ARROW   { Timplies }
@@ -228,9 +253,13 @@ term_arg_:
           | Blt  -> "<"
           | Ble  -> "<="
           | Bgt  -> ">"
-          | Bge  -> ">=" in
+          | Bge  -> ">="
+          | Badd|Bsub|Bmul|Bdiv|Bmod|Band|Bor -> assert false in
            mk_id (infix op) $startpos $endpos }
 
+%inline prefix_op:
+| MINUS { mk_id (prefix "-")  $startpos $endpos }
+
 %inline div_mod_op:
 | DIV  { mk_id "div" $startpos $endpos }
 | MOD  { mk_id "mod" $startpos $endpos }

plugins/python/test.py

 
 a = 0
 b = 1
+l = range(0, 10)
+## assert forall i. 0 <= i < 10 -> l[i] >= 0
 while b < 100:
   ## invariant b >= a >= 0
   ## invariant b >= 1