python: support for randint

plugins/python/py_lexer.mll

@@ -28,6 +28,7 @@
        "for", FOR; "in", IN;
        "and", AND; "or", OR; "not", NOT;
        "True", TRUE; "False", FALSE; "None", NONE;
+       "from", FROM; "import", IMPORT;
        (* annotations *)
        "forall", FORALL; "exists", EXISTS; "then", THEN; "let", LET;
       ];

plugins/python/py_parser.mly

@@ -64,6 +64,7 @@
 %token <Py_ast.binop> CMP
 %token <string> IDENT
 %token DEF IF ELSE RETURN PRINT WHILE FOR IN AND OR NOT NONE TRUE FALSE
+%token FROM IMPORT
 %token EOF
 %token LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ COMMA EQUAL COLON BEGIN END NEWLINE
 %token PLUS MINUS TIMES DIV MOD
@@ -92,10 +93,14 @@
 %%
 
 file:
-| NEWLINE? dl = list(def) b = list(stmt) EOF
+| NEWLINE? import* dl=list(def) b=list(stmt) EOF
     { dl, b }
 ;
 
+import:
+| FROM m=ident IMPORT f=ident NEWLINE
+  { () (* FIXME: check legal imports *) }
+
 def:
 | DEF f = ident LEFTPAR x = separated_list(COMMA, ident) RIGHTPAR
   COLON NEWLINE BEGIN s=spec l=nonempty_list(stmt) END

plugins/python/test.py

 
+from random import randint
+
+i = randint(0, 10)
+#@ assert 0 <= i <= 10
+
 # def swap(a, i, j):
 #   #@ requires 0 <= i < len(a) and 0 <= j < len(a)
 #   t = a[i]