compile.ml 9.66 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
(********************************************************************)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

(*
  - option to extract into a single file

  - no more why3extract.cma
    use driver preludes instead

  - 2 drivers for nums and zarith

  - no delcaration at all for a module -> no file produced
    (e.g. ref.Ref)

  - suggest a command line to compile the extracted code
    (for instance in a comment)

  - drivers for val now may use %1, %2, etc. (though not mandatory)
    Capp f x y
      "..." -> "..." x y
      "...%1..." -> "...x..." y
      "..(*%1*)..." -> "...(*x*)..." y
      "..%1..%3.." -> (fun z -> "..x..z..")  (y ignored)

  - extract file f.mlw into OCaml file f.ml, with sub-modules

  - "use (im|ex)port" -> "open"
    but OCaml's open is not transitive, so requires some extra work
    to figure out all the opens

  - if a WhyML module M is extracted to something that is a signature,
    then extract "module type B_sig = ..." (as well as "module B = ...")

  - use a black list in printer to avoid clash with Pervasives symbols
    (e.g. ref, (!), etc.)

*)

47 48 49 50 51
(*
  Questions pour Jean-Christophe et Andreï :
    - est-ce qu'il y a des utilisations particulières du champ
      [itd_fields], vis-à-vis du champ [itd_constructors] ?

52 53 54
    - comme l'AST [expr] est déjà en forme normale-A, est-ce que ça
      fait du sense pour vous d'utiliser des applications de la forme
      [Eapp of ident * ident list] ?
55 56 57 58

    - faire un module Erasure, pour y concentrer tout ce qui
      appartient à l'éffacement du code fantôme ?

59
 *)
60

61 62
(*
  TODO: réfléchir sur l'affectation parallèle
63 64 65
*)


66 67 68 69
(** Abstract syntax of ML *)

open Ident
open Ity
Mário Pereira's avatar
Mário Pereira committed
70
open Ty
Mário Pereira's avatar
Mário Pereira committed
71
open Term
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100

module ML = struct

  type ty =
    | Tvar    of ident
    | Tapp    of ident * ty list
    | Ttuple  of ty list

  type var = ident * ty

  type pat =
    | Pwild
    | Pident  of ident
    | Papp    of ident * pat list
    | Ptuple  of pat list
    | Precord of (ident * pat) list
    | Por     of pat * pat
    | Pas     of pat * ident

  type is_rec = bool

  type binop = Band | Bor | Beq

  type for_direction = To | DownTo

  type exn =
    | Xident  of ident
    | Xexit             (* Pervasives.Exit *)

101
  type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *)
102

103
  type expr = {
Mário Pereira's avatar
Mário Pereira committed
104 105 106
    e_node   : expr_node;
    e_ity    : ity;
    e_effect : effect;
107 108 109 110 111
  }

  and expr_node =
    | Econst  of Number.integer_constant
    | Eident  of ident
112
    | Eapp    of ident * ident list
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
    | Efun    of var list * expr
    | Elet    of ident * expr * expr
    | Eletrec of is_rec * (ident * var list * expr) list * expr
    | Eif     of expr * expr * expr
    | Ecast   of expr * ty
    | Etuple  of expr list (* at least 2 expressions *)
    | Econstr of ident * expr list
    | Ematch  of expr * (pat * expr) list
    | Ebinop  of expr * binop * expr
    | Enot    of expr
    | Eblock  of expr list
    | Ewhile  of expr * expr
    | Efor    of ident * ident * for_direction * ident * expr
    | Eraise  of exn * expr option
    | Etry    of expr * (exn * ident option * expr) list
    | Eabsurd

  type is_mutable = bool

  type typedef =
    | Dabstract
    | Ddata     of (ident * ty list) list
    | Drecord   of (is_mutable * ident * ty) list
    | Dalias    of ty

  type decl = (* TODO add support for the extraction of ocaml modules *)
    | Dtype of (ident * ident list * typedef) list
    | Dlet  of is_rec * (ident * var list * expr) list
        (* TODO add return type? *)
    | Dexn  of ident * ty option

144
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
145 146
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

147
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
148 149 150 151
  let ml_let id e1 e2 =
    Elet (id, e1, e2)

  let tunit = Ttuple []
152

153 154 155 156 157
  let enope = Eblock []

  let mk_unit =
    mk_expr enope (I Ity.ity_unit) Ity.eff_empty

158
end
Mário Pereira's avatar
Mário Pereira committed
159 160 161 162 163 164 165 166 167 168

(** Translation from Mlw to ML *)

module Translate = struct

  open Expr    (* Mlw expressions *)

  open Pmodule (* for the type of modules *)
  open Pdecl   (* for the type of program declarations *)

Mário Pereira's avatar
Mário Pereira committed
169 170 171 172 173 174 175 176 177 178 179 180 181
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
       ML.Tvar tvs.tv_name
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
       ML.Ttuple (List.map type_ tyl)
    | Tyapp (ts, tyl) ->
       ML.Tapp (ts.ts_name, List.map type_ tyl)

  let vsty vs =
    vs.vs_name, type_ vs.vs_ty

182 183 184
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
  let rec pat p =
    match p.pat_node with
    | Pwild ->
       ML.Pwild
    | Pvar vs ->
       ML.Pident vs.vs_name
    | Por (p1, p2) ->
       ML.Por (pat p1, pat p2)
    | Pas (p, vs) ->
       ML.Pas (pat p, vs.vs_name)
    | Papp (ls, pl) when is_fs_tuple ls ->
       ML.Ptuple (List.map pat pl)
    | Papp (ls, pl) ->
       ML.Papp (ls.ls_name, List.map pat pl)

Mário Pereira's avatar
Mário Pereira committed
200 201
  (** programs *)

202 203 204 205 206
  (* individual types *)
  let rec ity t =
    match t.ity_node with
    | Ityvar ({tv_name = tv}, _) ->
       ML.Tvar tv
207 208
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
       ML.Ttuple (List.map ity itl)
209 210 211 212
    | Ityapp ({its_ts = ts}, itl, _) ->
       ML.Tapp (ts.ts_name, List.map ity itl)
    | _ -> (* TODO *) assert false

Mário Pereira's avatar
Mário Pereira committed
213 214
  let pv_name pv = pv.pv_vs.vs_name

Mário Pereira's avatar
Mário Pereira committed
215 216 217 218
  let pvty pv =
    if pv.pv_ghost then (pv_name pv, ML.tunit)
    else vsty pv.pv_vs

219 220 221 222
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
223 224 225 226
  (* function arguments *)
  let args = (* point-free *)
    List.map pvty

Mário Pereira's avatar
Mário Pereira committed
227
  (* expressions *)
228
  let rec expr info ({e_effect = eff} as e) =
229
    (* assert (not eff.eff_ghost); *)
Mário Pereira's avatar
Mário Pereira committed
230
    match e.e_node with
231 232 233
    | Econst c ->
       let c = match c with Number.ConstInt c -> c | _ -> assert false in
       ML.mk_expr (ML.Econst c) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
234 235
    | Evar pvs ->
       let pv_id = pv_name pvs in
236
       ML.mk_expr (ML.Eident pv_id) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
237
    | Elet (LDvar (pvs, e1), e2) ->
238
       let ml_let = ML.ml_let (pv_name pvs) (expr info e1) (expr info e2) in
239
       ML.mk_expr ml_let (ML.I e.e_ity) eff
240
    | Eexec ({c_node = Capp (rs, pvl)}, _) ->
241 242
      let rs_id = rs.rs_name in
      let pv_id = List.map pv_name pvl in
243
       ML.mk_expr (ML.Eapp (rs_id, pv_id)) (ML.I e.e_ity) eff
244
    | Eabsurd ->
245
       ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
246
    | Ecase (e1, pl) ->
247 248
       let e1 = expr info e1 in
       let pl = List.map (ebranch info) pl in
249 250 251
       ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) eff
    | Eassert _ ->
       ML.mk_unit
252
    | Eif (e1, e2, e3) ->
253 254 255
       let e1 = expr info e1 in
       let e2 = expr info e2 in
       let e3 = expr info e3 in
256
       ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
257 258
    | Eghost eg ->
       expr info eg (* it keeps its ghost status *)
259 260
    | _ -> (* TODO *) assert false

261 262
  and ebranch info ({pp_pat = p}, e) =
    pat p, expr info e
263

264 265 266
  let its_args ts = ts.its_ts.ts_args
  let itd_name td = td.itd_its.its_ts.ts_name

267 268 269 270 271 272
  let drecord_fields {itd_its = its; itd_fields = fl} =
    List.map (fun ({rs_cty = rsc} as rs) ->
      (List.exists (pv_equal (Opt.get rs.rs_field)) its.its_mfields),
      rs.rs_name,
      if rs_ghost rs then ML.tunit else ity rsc.cty_result) fl

273 274
  let ddata_constructs = (* point-free *)
    List.map (fun ({rs_cty = rsc} as rs) ->
275
      rs.rs_name, List.map (fun {pv_vs = pv} -> type_ pv.vs_ty) rsc.cty_args)
276 277

  (* type declarations/definitions *)
278
  let tdef itd =
279 280 281
    let s = itd.itd_its in
    let id = itd_name itd in
    let args = its_args s in
282 283
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
284
         ML.Dtype [id, type_args args, ML.Dabstract]
285
      | None, cl, [] ->
286
         ML.Dtype [id, type_args args, ML.Ddata (ddata_constructs cl)]
287 288 289
      | None, _, _ ->
         ML.Dtype [id, type_args args, ML.Drecord (drecord_fields itd)]
      | Some t, _, _ ->
290 291
         ML.Dtype [id, type_args args, ML.Dalias (ity t)]
    end
Mário Pereira's avatar
Mário Pereira committed
292 293

  (* program declarations *)
294
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
295 296 297
    match pd.pd_node with
    | PDlet (LDvar (_, _)) ->
       []
Mário Pereira's avatar
Mário Pereira committed
298
    | PDlet (LDsym ({rs_name = rsn; rs_cty = cty}, {c_node = Cfun e})) ->
299
       [ML.Dlet (false, [rsn, args cty.cty_args, expr info e])]
Mário Pereira's avatar
Mário Pereira committed
300 301 302 303 304 305 306 307 308
    | PDlet (LDsym ({rs_name = rsn}, {c_node = Capp _})) ->
       Format.printf "LDsym Capp--> %s@." rsn.id_string;
       []
    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cpur _})) ->
       Format.printf "LDsym Cpur--> %s@." rsn.id_string;
       []
    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cany})) ->
       Format.printf "LDsym Cany--> %s@." rsn.id_string;
       []
309 310 311 312
    | PDlet (LDrec rl) ->
       let rec_def =
         List.map (fun {rec_fun = e; rec_rsym = rs} ->
           let e = match e.c_node with Cfun e -> e | _ -> assert false in
313
           rs.rs_name, args rs.rs_cty.cty_args, expr info e) rl in
314
       [ML.Dlet (true, rec_def)]
Mário Pereira's avatar
Mário Pereira committed
315 316
    | PDpure ->
       []
317
    | PDtype itl ->
318
       List.map tdef itl
319 320 321 322 323
    | PDexn ({xs_name = xsn} as xs) ->
       if ity_equal xs.xs_ity ity_unit then
         [ML.Dexn (xsn, None)]
       else
         [ML.Dexn (xsn, Some (ity xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
324 325

  (* unit module declarations *)
326
  let mdecl info = function
Mário Pereira's avatar
Mário Pereira committed
327
    | Udecl pd ->
328
       pdecl info pd
329
    |  _ -> (* TODO *) []
Mário Pereira's avatar
Mário Pereira committed
330 331

  (* modules *)
332 333
  let module_ info m =
    List.concat (List.map (mdecl info) m.mod_units)
Mário Pereira's avatar
Mário Pereira committed
334 335

end
Mário Pereira's avatar
Mário Pereira committed
336 337 338

(*
 * Local Variables:
339
 * compile-command: "make -C ../.. -j3 bin/why3extract.opt"
Mário Pereira's avatar
Mário Pereira committed
340 341
 * End:
 *)