compile.ml 9.94 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

module ML = struct

75 76 77
  open Expr
  open Pdecl

78
  type ty =
79
    | Tvar    of tvsymbol
80 81 82
    | Tapp    of ident * ty list
    | Ttuple  of ty list

83 84 85
  type is_ghost = bool

  type var = ident * ty * is_ghost
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105

  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 *)

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

108
  type expr = {
Mário Pereira's avatar
Mário Pereira committed
109 110 111
    e_node   : expr_node;
    e_ity    : ity;
    e_effect : effect;
112 113 114 115
  }

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

  type is_mutable = bool

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

141 142 143 144 145 146 147
  type its_defn = {
    its_name    : ident;
    its_args    : tvsymbol list;
    its_private : bool;
    its_def     : typedef option;
  }

148
  type decl = (* TODO add support for the extraction of ocaml modules *)
149 150
    | Dtype of its_defn list
    | Dlet  of is_rec * (rsymbol * var list * expr) list
151
        (* TODO add return type? *)
152
    | Dexn  of xsymbol * ty option
153

154
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
155 156
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

157
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
158 159 160 161
  let ml_let id e1 e2 =
    Elet (id, e1, e2)

  let tunit = Ttuple []
162

163 164 165 166 167
  let enope = Eblock []

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

168 169 170 171 172
  let mk_var id ty ghost = (id, ty, ghost)

  let mk_its_defn id args private_ def =
    { its_name = id; its_args = args; its_private = private_; its_def = def; }

173
end
Mário Pereira's avatar
Mário Pereira committed
174 175 176 177 178 179 180 181 182 183

(** 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
184 185 186 187
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
188
       ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
189 190 191 192 193 194 195 196
    | 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

197 198 199
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
  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
215 216
  (** programs *)

217 218 219
  (* individual types *)
  let rec ity t =
    match t.ity_node with
220 221
    | Ityvar (tvs, _) ->
       ML.Tvar tvs
222 223
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
       ML.Ttuple (List.map ity itl)
224 225 226 227
    | 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
228 229
  let pv_name pv = pv.pv_vs.vs_name

Mário Pereira's avatar
Mário Pereira committed
230
  let pvty pv =
231 232 233 234 235
    if pv.pv_ghost then
      ML.mk_var (pv_name pv) ML.tunit true
    else
      let (vs, vs_ty) = vsty pv.pv_vs in
      ML.mk_var vs vs_ty false
Mário Pereira's avatar
Mário Pereira committed
236

237 238 239 240
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
241 242 243 244
  (* function arguments *)
  let args = (* point-free *)
    List.map pvty

Mário Pereira's avatar
Mário Pereira committed
245
  (* expressions *)
246
  let rec expr info ({e_effect = eff} as e) =
247
    (* assert (not eff.eff_ghost); *)
Mário Pereira's avatar
Mário Pereira committed
248
    match e.e_node with
249 250 251
    | 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
252
    | Evar pvs ->
253
       ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
254
    | Elet (LDvar (pvs, e1), e2) ->
255
       let ml_let = ML.ml_let pvs (expr info e1) (expr info e2) in
256
       ML.mk_expr ml_let (ML.I e.e_ity) eff
257
    | Eexec ({c_node = Capp (rs, pvl)}, _) ->
258
       ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
259
    | Eabsurd ->
260
       ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
261
    | Ecase (e1, pl) ->
262 263
       let e1 = expr info e1 in
       let pl = List.map (ebranch info) pl in
264 265 266
       ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) eff
    | Eassert _ ->
       ML.mk_unit
267
    | Eif (e1, e2, e3) ->
268 269 270
       let e1 = expr info e1 in
       let e2 = expr info e2 in
       let e3 = expr info e3 in
271
       ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
272 273
    | Eghost eg ->
       expr info eg (* it keeps its ghost status *)
274 275
    | _ -> (* TODO *) assert false

276 277
  and ebranch info ({pp_pat = p}, e) =
    pat p, expr info e
278

279 280 281 282
  let its_args ts = ts.its_ts.ts_args
  let itd_name td = td.itd_its.its_ts.ts_name

  (* type declarations/definitions *)
283
  let tdef itd =
284
    let s = itd.itd_its in
285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
    let ddata_constructs = (* point-free *)
      List.map (fun ({rs_cty = rsc} as rs) ->
          rs.rs_name,
          let args = List.filter (fun x -> not x.pv_ghost) rsc.cty_args in
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
    let drecord_fields = (* point-free *)
      List.map (fun ({rs_cty = rsc} as rs) ->
          (List.exists (pv_equal (Opt.get rs.rs_field)) s.its_mfields),
          rs.rs_name,
          if rs_ghost rs then ML.tunit else ity rsc.cty_result)
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
300 301
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
302
         ML.mk_its_defn id args is_private None
303
      | None, cl, [] ->
304 305 306 307 308
         let cl = ddata_constructs cl in
         ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
      | None, _, pjl ->
         let pjl = drecord_fields pjl in
         ML.mk_its_defn id args is_private (Some (ML.Drecord pjl))
309
      | Some t, _, _ ->
310
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
311
    end
Mário Pereira's avatar
Mário Pereira committed
312 313

  (* program declarations *)
314
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
315 316 317
    match pd.pd_node with
    | PDlet (LDvar (_, _)) ->
       []
318 319
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
       [ML.Dlet (false, [rs, args cty.cty_args, expr info e])]
Mário Pereira's avatar
Mário Pereira committed
320 321 322 323 324 325
    | PDlet (LDsym ({rs_name = rsn}, {c_node = Capp _})) ->
       []
    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cpur _})) ->
       []
    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cany})) ->
       []
326 327 328 329
    | 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
330
           rs, args rs.rs_cty.cty_args, expr info e) rl in
331
       [ML.Dlet (true, rec_def)]
Mário Pereira's avatar
Mário Pereira committed
332 333
    | PDpure ->
       []
334
    | PDtype itl ->
335 336
       [ML.Dtype (List.map tdef itl)]
    | PDexn xs ->
337
       if ity_equal xs.xs_ity ity_unit then
338
         [ML.Dexn (xs, None)]
339
       else
340
         [ML.Dexn (xs, Some (ity xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
341 342

  (* unit module declarations *)
343
  let mdecl info = function
Mário Pereira's avatar
Mário Pereira committed
344
    | Udecl pd ->
345
       pdecl info pd
346
    |  _ -> (* TODO *) []
Mário Pereira's avatar
Mário Pereira committed
347 348

  (* modules *)
349 350
  let module_ info m =
    List.concat (List.map (mdecl info) m.mod_units)
Mário Pereira's avatar
Mário Pereira committed
351 352

end
Mário Pereira's avatar
Mário Pereira committed
353 354 355

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