A new plugin to read Python programs

for teaching purposes only
limited to a microscopic fragment of Python for the moment

.gitignore

@@ -212,6 +212,12 @@ pvsbin/
 /plugins/tptp/tptp_parser.conflicts
 /plugins/parser/dimacs.ml
 
+# /plugins/python/
+/plugins/python/py_lexer.ml
+/plugins/python/py_parser.ml
+/plugins/python/py_parser.mli
+/plugins/python/test/
+
 # /drivers
 /drivers/coq-realizations.aux
 /drivers/pvs-realizations.aux

.merlin.in

@@ -17,6 +17,7 @@ S plugins/parser
 S plugins/printer
 S plugins/transform
 S plugins/tptp
+S plugins/python
 
 B src/util
 B src/core
@@ -37,6 +38,7 @@ B plugins/parser
 B plugins/printer
 B plugins/transform
 B plugins/tptp
+B plugins/python
 B lib/why3
 
 PKG str unix num dynlink @ZIPLIB@ @LABLGTK2PKG@ @META_OCAMLGRAPH@

Makefile.in

@@ -374,20 +374,27 @@ endif
 
 PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
 		plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
+		plugins/python/py_lexer.ml \
+		plugins/python/py_parser.ml plugins/python/py_parser.mli \
 		plugins/parser/dimacs.ml \
 
 PLUG_PARSER = genequlin dimacs
 PLUG_PRINTER =
 PLUG_TRANSFORM =
 PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
+PLUG_PYTHON = py_ast py_parser py_lexer py_main
 
-PLUGINS = genequlin dimacs tptp
+PLUGINS = genequlin dimacs tptp python
 
 TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
+PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
 
 TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
 TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
 
+PYTHONCMO = $(addsuffix .cmo, $(PYTHONMODULES))
+PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))
+
 ifeq (@enable_hypothesis_selection@,yes)
 PLUG_TRANSFORM += hypothesis_selection
 PLUGINS += hypothesis_selection
@@ -401,13 +408,13 @@ endif
 PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
 	      $(addprefix plugins/printer/, $(PLUG_PRINTER)) \
 	      $(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
-	      $(TPTPMODULES)
+	      $(TPTPMODULES) $(PYTHONMODULES)
 
 PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
 PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
 PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
 
-PLUGDIRS = parser printer transform tptp
+PLUGDIRS = parser printer transform tptp python
 PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
 
 $(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
@@ -453,6 +460,14 @@ lib/plugins/tptp.cmo: $(TPTPCMO)
 	$(SHOW) 'Linking  $@'
 	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
 
+lib/plugins/python.cmxs: $(PYTHONCMX)
+	$(SHOW) 'Linking  $@'
+	$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
+
+lib/plugins/python.cmo: $(PYTHONCMO)
+	$(SHOW) 'Linking  $@'
+	$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
+
 # depend and clean targets
 
 ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"

plugins/python/README

+A plugin to verify programs written in a (microscopic) fragment of Python.

plugins/python/py_ast.ml

+
+(* Arbres de syntaxe abstraite de Mini-Python *)
+
+type ident = string
+
+type unop =
+  | Uneg (* -e *)
+  | Unot (* not e *)
+
+type binop =
+  | Badd | Bsub | Bmul | Bdiv | Bmod    (* + - * / % *)
+  | Beq | Bneq | Blt | Ble | Bgt | Bge  (* == != < <= > >= *)
+  | Band | Bor                          (* && || *)
+
+type constant =
+  | Cnone
+  | Cbool of bool
+  | Cstring of string
+  | Cint of int (* en Python les entiers sont en réalité de précision
+                   arbitraire; on simplifie ici *)
+
+type expr =
+  | Ecst of constant
+  | Eident of ident
+  | Ebinop of binop * expr * expr
+  | Eunop of unop * expr
+  | Ecall of ident * expr list
+  | Elist of expr list
+  | Eget of expr * expr (* e1[e2] *)
+
+and stmt =
+  | Sif of expr * stmt * stmt
+  | Sreturn of expr
+  | Sassign of ident * expr
+  | Sprint of expr
+  | Sblock of stmt list
+  | Sfor of ident * expr * stmt
+  | Seval of expr
+  | Sset of expr * expr * expr (* e1[e2] = e3 *)
+
+and def = ident * ident list * stmt
+
+and file = def list * stmt
+

plugins/python/py_lexer.mll

+
+{
+  open Lexing
+  open Py_ast
+  open Py_parser
+
+  exception Lexing_error of string
+
+  let id_or_kwd =
+    let h = Hashtbl.create 32 in
+    List.iter (fun (s, tok) -> Hashtbl.add h s tok)
+      ["def", DEF; "if", IF; "else", ELSE;
+       "return", RETURN; "print", PRINT;
+       "for", FOR; "in", IN;
+       "and", AND; "or", OR; "not", NOT;
+       "True", CST (Cbool true);
+       "False", CST (Cbool false);
+       "None", CST Cnone;];
+   fun s -> try Hashtbl.find h s with Not_found -> IDENT s
+
+  let newline lexbuf =
+    let pos = lexbuf.lex_curr_p in
+    lexbuf.lex_curr_p <-
+      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
+
+  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 letter = ['a'-'z' 'A'-'Z']
+let digit = ['0'-'9']
+let ident = letter (letter | digit | '_')*
+let integer = ['0'-'9']+
+let space = ' ' | '\t'
+let comment = "#" [^'\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
+      }
+  | (space | comment)+
+      { next_tokens lexbuf }
+  | ident as id { [id_or_kwd id] }
+  | '+'     { [PLUS] }
+  | '-'     { [MINUS] }
+  | '*'     { [TIMES] }
+  | '/'     { [DIV] }
+  | '%'     { [MOD] }
+  | '='     { [EQUAL] }
+  | "=="    { [CMP Beq] }
+  | "!="    { [CMP Bneq] }
+  | "<"     { [CMP Blt] }
+  | "<="    { [CMP Ble] }
+  | ">"     { [CMP Bgt] }
+  | ">="    { [CMP Bge] }
+  | '('     { [LP] }
+  | ')'     { [RP] }
+  | '['     { [LSQ] }
+  | ']'     { [RSQ] }
+  | ','     { [COMMA] }
+  | ':'     { [COLON] }
+  | integer as s
+            { try [CST (Cint (int_of_string s))]
+              with _ -> raise (Lexing_error ("constant too large: " ^ s)) }
+  | '"'     { [CST (Cstring (string lexbuf))] }
+  | eof     { [EOF] }
+  | _ as c  { raise (Lexing_error ("illegal character: " ^ String.make 1 c)) }
+
+and indentation = parse
+  | (space | comment)* '\n'
+      { newline lexbuf; indentation lexbuf }
+  | space* as s
+      { String.length s }
+
+and string = parse
+  | '"'
+      { let s = Buffer.contents string_buffer in
+	Buffer.reset string_buffer;
+	s }
+  | "\\n"
+      { Buffer.add_char string_buffer '\n';
+	string lexbuf }
+  | "\\\""
+      { Buffer.add_char string_buffer '"';
+	string lexbuf }
+  | _ as c
+      { Buffer.add_char string_buffer c;
+	string lexbuf }
+  | eof
+      { raise (Lexing_error "unterminated string") }
+
+{
+
+  let next_token =
+    let tokens = Queue.create () in (* prochains lexèmes à renvoyer *)
+    fun lb ->
+      if Queue.is_empty tokens then begin
+	let l = next_tokens lb in
+	List.iter (fun t -> Queue.add t tokens) l
+      end;
+      Queue.pop tokens
+}
+
+
+

plugins/python/py_main.ml

+
+open Why3
+open Mlw_module
+open Ptree
+open Stdlib
+
+let debug = Debug.register_flag "mini-python"
+  ~desc:"mini-python plugin debug flag"
+
+let read_channel env path file c =
+  let lb = Lexing.from_channel c in
+  Loc.set_file file lb;
+  let f = Loc.with_location (Py_parser.file Py_lexer.next_token) lb in
+  Debug.dprintf debug "%s parsed successfully.@." file;
+  let file = Filename.basename file in
+  let file = Filename.chop_extension file in
+  let name = String.capitalize_ascii file in
+  Debug.dprintf debug "building module %s.@." name;
+  let inc = Mlw_typing.open_file env path in
+  let id = { id_str = name; id_lab = []; id_loc = Loc.dummy_position } in
+  inc.open_module id;
+  (* Typing.add_decl id.id_loc *)
+  (*   (Duse (Qdot (Qident (mk_id "ocaml"), mk_id "OCaml") )); *)
+  (* Typing.close_scope id.id_loc ~import:true; *)
+  (*  List.iter (fun x -> add_decl (loc_of_decl x) x) f; *)
+  inc.close_module ();
+  let mm, _ as res = Mlw_typing.close_file () in
+  if path = [] && Debug.test_flag debug then begin
+    let add_m _ m modm = Ident.Mid.add m.mod_theory.Theory.th_name m modm in
+    let modm = Mstr.fold add_m mm Ident.Mid.empty in
+    let print_m _ m = Format.eprintf
+      "@[<hov 2>module %a@\n%a@]@\nend@\n@." Pretty.print_th m.mod_theory
+      (Pp.print_list Pp.newline2 Mlw_pretty.print_pdecl) m.mod_decls in
+    Ident.Mid.iter print_m modm
+  end;
+  res
+
+let () =
+  Env.register_format mlw_language "python" ["py"] read_channel
+    ~desc:"mini-Python format"

plugins/python/py_parser.mly

+
+%{
+  open Py_ast
+%}
+
+%token <Py_ast.constant> CST
+%token <Py_ast.binop> CMP
+%token <string> IDENT
+%token DEF IF ELSE RETURN PRINT FOR IN AND OR NOT
+%token EOF
+%token LP RP LSQ RSQ COMMA EQUAL COLON BEGIN END NEWLINE
+%token PLUS MINUS TIMES DIV MOD
+
+%left OR
+%left AND
+%nonassoc NOT
+%nonassoc CMP
+%left PLUS MINUS
+%left TIMES DIV MOD
+%nonassoc unary_minus
+%nonassoc LSQ
+
+%start file
+
+%type <Py_ast.file> file
+
+%%
+
+file:
+| NEWLINE? dl = list(def) b = list(stmt) EOF
+    { dl, Sblock b }
+;
+
+def:
+| DEF f = ident LP x = separated_list(COMMA, ident) RP
+  COLON s = suite
+    { f, x, s }
+;
+
+expr:
+| c = CST
+    { Ecst c }
+| id = ident
+    { Eident id }
+| e1 = expr LSQ e2 = expr RSQ
+    { 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) }
+| f = ident LP e = separated_list(COMMA, expr) RP
+    { Ecall (f, e) }
+| LSQ l = separated_list(COMMA, expr) RSQ
+    { Elist l }
+| LP e = expr RP
+    { e }
+;
+
+suite:
+| s = simple_stmt NEWLINE
+    { s }
+| NEWLINE BEGIN l = nonempty_list(stmt) END
+    { Sblock l }
+;
+
+stmt:
+| s = simple_stmt NEWLINE
+    { s }
+| IF c = expr COLON s = suite
+    { Sif (c, s, Sblock []) }
+| IF c = expr COLON s1 = suite ELSE COLON s2 = suite
+    { Sif (c, s1, s2) }
+| FOR x = ident IN e = expr COLON s = suite
+    { Sfor (x, e, s) }
+;
+
+simple_stmt:
+| RETURN e = expr
+    { Sreturn e }
+| id = ident EQUAL e = expr
+    { Sassign (id, e) }
+| e1 = expr LSQ e2 = expr RSQ EQUAL e3 = expr
+    { Sset (e1, e2, e3) }
+| PRINT e = expr
+    { Sprint e }
+| e = expr
+    { Seval e }
+;
+
+%inline binop:
+| PLUS  { Badd }
+| MINUS { Bsub }
+| TIMES { Bmul }
+| DIV   { Bdiv }
+| MOD   { Bmod }
+| c=CMP { c    }
+| AND   { Band }
+| OR    { Bor  }
+;
+
+ident:
+  id = IDENT { id }
+;
+
+

plugins/python/test.py

+
+
+# Local Variables:
+# compile-command: "make -C ../.. && why3 ide test.py"
+# End: