py_main.ml 6.79 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14 15 16

open Why3
open Mlw_module
open Ptree
open Stdlib

17
let debug = Debug.register_flag "python"
18 19
  ~desc:"mini-python plugin debug flag"

20 21 22 23 24
let mk_id ?(loc=Loc.dummy_position) name =
  { id_str = name; id_lab = []; id_loc = loc }

let mk_expr ?(loc=Loc.dummy_position) d =
  { expr_desc = d; expr_loc = loc }
25 26
let mk_term ?(loc=Loc.dummy_position) d =
  { term_desc = d; term_loc = loc }
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
let mk_unit ~loc =
  mk_expr ~loc (Etuple [])

let empty_spec = {
  sp_pre     = [];
  sp_post    = [];
  sp_xpost   = [];
  sp_reads   = [];
  sp_writes  = [];
  sp_variant = [];
  sp_checkrw = false;
  sp_diverge = false;
}

type env = {
42
  vars: ident Hstr.t;
43 44 45 46
}

let infix  ~loc s = Qident (mk_id ~loc ("infix "  ^ s))
let prefix ~loc s = Qident (mk_id ~loc ("prefix " ^ s))
47
let mixfix ~loc s = Qident (mk_id ~loc ("mixfix " ^ s))
48

49 50 51 52 53 54 55 56 57 58 59 60
(* 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 }

61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
  | Py_ast.Enone ->
    mk_unit ~loc
  | Py_ast.Ebool b ->
    mk_expr ~loc (if b then Etrue else Efalse)
  | Py_ast.Eint s ->
    mk_expr ~loc (Econst (Number.ConstInt (Number.int_const_dec s)))
  | Py_ast.Estring _s ->
    assert false (*TODO*)
  | Py_ast.Eident id ->
    if not (Hstr.mem env.vars id.id_str) then
      Loc.errorm ~loc "unbound variable %s" id.id_str;
    mk_expr ~loc (Eidapp (prefix ~loc "!", [mk_expr ~loc (Eident (Qident id))]))
  | Py_ast.Ebinop (op, e1, e2) ->
    let e1 = expr env e1 in
    let e2 = expr env e2 in
    mk_expr ~loc (match op with
      | Py_ast.Band -> Elazy (e1, LazyAnd, e2)
      | Py_ast.Bor  -> Elazy (e1, LazyOr,  e2)
      | 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.Beq  -> Eidapp (infix ~loc "=", [e1; e2])
      | Py_ast.Bneq -> Eidapp (infix ~loc "<>", [e1; e2])
      | Py_ast.Blt  -> Eidapp (infix ~loc "<", [e1; e2])
      | Py_ast.Ble  -> Eidapp (infix ~loc "<=", [e1; e2])
      | Py_ast.Bgt  -> Eidapp (infix ~loc ">", [e1; e2])
      | Py_ast.Bge  -> Eidapp (infix ~loc ">=", [e1; e2])
    )
  | Py_ast.Eunop (Py_ast.Uneg, e) ->
    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]))
96 97
  | Py_ast.Ecall (id, el) ->
    mk_expr ~loc (Eidapp (Qident id, List.map (expr env) el))
98
  | Py_ast.Elist _el ->
99
    assert false
100 101
  | Py_ast.Eget (e1, e2) ->
    mk_expr ~loc (Eidapp (mixfix ~loc "[]", [expr env e1; expr env e2]))
102 103 104 105 106 107 108 109

let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
  match d with
  | Py_ast.Seval e ->
    expr env e
  | Py_ast.Sprint e ->
    mk_expr ~loc (Elet (mk_id ~loc "_", Gnone, expr env e, mk_unit ~loc))
  | Py_ast.Sif (e, s1, s2) ->
110
    mk_expr ~loc (Eif (expr env e, block env ~loc s1, block env ~loc s2))
111
  | Py_ast.Swhile (e, ann, s) ->
112 113
    mk_expr ~loc
      (Ewhile (expr env e, loop_annotation env ann, block env ~loc s))
114
  | Py_ast.Sreturn _e ->
115 116 117 118 119 120 121
    assert false (*TODO*)
  | Py_ast.Sassign (id, e) ->
    let e = expr env e in
    if Hstr.mem env.vars id.id_str then
      let x = let loc = id.id_loc in mk_expr ~loc (Eident (Qident id)) in
      mk_expr ~loc (Einfix (x, mk_id ~loc "infix :=", e))
    else
122
      block env ~loc [s]
123
  | Py_ast.Sfor (_id, _e, _s) ->
124
    assert false (*TODO*)
125
  | Py_ast.Sset (_e1, _e2, _e3) ->
126
    assert false (*TODO*)
127 128
  | Py_ast.Sassert t ->
    mk_expr ~loc (Eassert (Aassert, deref env t))
129

130
and block env ?(loc=Loc.dummy_position) = function
131 132 133 134 135
  | [] ->
    mk_unit ~loc
  | { 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 *)
136
    Hstr.add env.vars id.id_str id;
137
    let e1 = mk_expr ~loc (Eidapp (Qident (mk_id ~loc "ref"), [e])) in
138
    mk_expr ~loc (Elet (id, Gnone, e1, block env ~loc sl))
139
  | { Py_ast.stmt_loc = loc } as s :: sl ->
140 141 142
    let s = stmt env s in
    let sl = block env ~loc sl in
    mk_expr ~loc (Esequence (s, sl))
143 144 145 146

let translate inc (_dl, s) =
  let params = [Loc.dummy_position, None, false, Some (PTtuple [])] in
  let env = { vars = Hstr.create 32 } in
147
  let fd = (params, None, block env s, empty_spec) in
148 149 150
  let main = Dfun (mk_id "main", Gnone, fd) in
  inc.new_pdecl Loc.dummy_position main

151 152 153 154 155 156 157 158 159 160
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
161 162 163 164 165
  inc.open_module (mk_id name);
  let use_import (f, m) =
    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
166 167
  List.iter use_import
    ["int", "Int"; "ref", "Ref"; "python", "Python"];
168
  translate inc f;
169 170 171 172 173 174 175 176 177 178 179 180 181 182 183
  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"