py_main.ml 8.48 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
let mk_id ?(loc=Loc.dummy_position) name =
  { id_str = name; id_lab = []; id_loc = loc }

23 24 25 26
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))

27 28
let mk_expr ?(loc=Loc.dummy_position) d =
  { expr_desc = d; expr_loc = loc }
29 30
let mk_term ?(loc=Loc.dummy_position) d =
  { term_desc = d; term_loc = loc }
31 32
let mk_unit ~loc =
  mk_expr ~loc (Etuple [])
33 34 35 36 37 38 39 40 41 42
let mk_var ~loc id =
  mk_expr ~loc (Eident (Qident id))
let mk_ref ~loc e =
  mk_expr ~loc (Eidapp (Qident (mk_id ~loc "ref"), [e]))
let deref_id ~loc id =
  mk_expr ~loc (Eidapp (prefix ~loc "!", [mk_expr ~loc (Eident (Qident id))]))
let constant ~loc s =
  mk_expr ~loc (Econst (Number.ConstInt (Number.int_const_dec s)))
let len ~loc =
  Qident (mk_id ~loc "len")
43 44 45 46 47 48 49 50 51 52 53 54 55

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

type env = {
56 57
  vars: ident Mstr.t;
  for_index: int;
58 59
}

60 61 62 63 64 65 66 67 68 69 70 71
let empty_env =
  { vars = Mstr.empty;
    for_index = 0; }

let add_var env id =
  { env with vars = Mstr.add id.id_str id env.vars }

let for_vars ~loc env =
  let i = env.for_index in
  let env = { env with for_index = i + 1 } in
  let i = string_of_int env.for_index in
  mk_id ~loc ("for index " ^ i ), mk_id ~loc ("for list " ^ i), env
72

73 74 75 76 77 78
(* 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
79
  Mstr.fold deref env.vars t
80 81 82 83 84

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 }

85 86 87
let add_loop_invariant i a =
  { a with loop_invariant = i :: a.loop_invariant }

88 89 90 91 92 93
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 ->
94
    constant ~loc s
95 96 97
  | Py_ast.Estring _s ->
    assert false (*TODO*)
  | Py_ast.Eident id ->
98
    if not (Mstr.mem id.id_str env.vars) then
99
      Loc.errorm ~loc "unbound variable %s" id.id_str;
100
    deref_id ~loc id
101 102 103 104 105 106 107 108 109
  | 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])
110 111
      | Py_ast.Bdiv -> Eidapp (Qident (mk_id ~loc "div"), [e1; e2])
      | Py_ast.Bmod -> Eidapp (Qident (mk_id ~loc "mod"), [e1; e2])
112 113 114 115 116 117 118 119 120 121 122
      | 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]))
123 124
  | Py_ast.Ecall (id, el) ->
    mk_expr ~loc (Eidapp (Qident id, List.map (expr env) el))
125
  | Py_ast.Elist _el ->
126
    assert false
127 128
  | Py_ast.Eget (e1, e2) ->
    mk_expr ~loc (Eidapp (mixfix ~loc "[]", [expr env e1; expr env e2]))
129 130 131 132 133 134 135 136

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) ->
137
    mk_expr ~loc (Eif (expr env e, block env ~loc s1, block env ~loc s2))
138
  | Py_ast.Sreturn _e ->
139 140 141
    assert false (*TODO*)
  | Py_ast.Sassign (id, e) ->
    let e = expr env e in
142
    if Mstr.mem id.id_str env.vars then
143 144 145
      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
146
      block env ~loc [s]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
147 148 149
  | Py_ast.Sset (e1, e2, e3) ->
    mk_expr ~loc (Eidapp (mixfix ~loc "[]<-",
                          [expr env e1; expr env e2; expr env e3]))
150 151
  | Py_ast.Sassert (k, t) ->
    mk_expr ~loc (Eassert (k, deref env t))
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
  | Py_ast.Swhile (e, ann, s) ->
    mk_expr ~loc
      (Ewhile (expr env e, loop_annotation env ann, block env ~loc s))
  | Py_ast.Sfor (id, e, ann, body) ->
    (* for x in e: s
                             is translated to
       let l = e in
       let i = ref 0 in
       while !i < len(e) do
         invariant 0 <= !i (and user invariants)
         let x = l[!i] in
         s;
         i := !i + 1
       done
    *)
    let i, l, env = for_vars ~loc env in
    let e = expr env e in
    let env = add_var env id in
    mk_expr ~loc (Elet (l, Gnone, e, (* evaluate e only once *)
    mk_expr ~loc (Elet (i, Gnone, mk_ref ~loc (constant ~loc "0"),
    let lenl = mk_expr ~loc (Eidapp (len ~loc, [mk_var ~loc l])) in
    let test =
      mk_expr ~loc (Eidapp (infix ~loc "<", [deref_id ~loc i; lenl])) in
    mk_expr ~loc (Ewhile (test, loop_annotation env ann,
    let li = mk_expr ~loc
      (Eidapp (mixfix ~loc "[]", [mk_var ~loc l; deref_id ~loc i])) in
    mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc li,
    mk_expr ~loc (Esequence (block env body,
    mk_expr ~loc (Eidapp (Qident (mk_id ~loc "incr"), [mk_var ~loc i])))
    )))))))))
182

183
and block env ?(loc=Loc.dummy_position) = function
184 185 186
  | [] ->
    mk_unit ~loc
  | { Py_ast.stmt_loc = loc; stmt_desc = Py_ast.Sassign (id, e) } :: sl
187
    when not (Mstr.mem id.id_str env.vars) ->
188
    let e = expr env e in (* check e *before* adding id to environment *)
189 190
    let env = add_var env id in
    mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc e, block env ~loc sl))
191
  | { Py_ast.stmt_loc = loc } as s :: sl ->
192 193 194
    let s = stmt env s in
    let sl = block env ~loc sl in
    mk_expr ~loc (Esequence (s, sl))
195 196 197

let translate inc (_dl, s) =
  let params = [Loc.dummy_position, None, false, Some (PTtuple [])] in
198
  let env = empty_env in
199
  let fd = (params, None, block env s, empty_spec) in
200 201 202
  let main = Dfun (mk_id "main", Gnone, fd) in
  inc.new_pdecl Loc.dummy_position main

203 204 205 206 207 208 209 210 211 212
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
213 214 215 216 217
  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
218
  List.iter use_import
219
    ["int", "Int"; "ref", "Refint"; "python", "Python"];
220
  translate inc f;
221 222 223 224 225 226 227 228 229 230 231 232 233 234 235
  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"