compile.ml 13.4 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
    - comment est-ce qu'il marche la [mask] d'un [prog_pattern] ?

61
 *)
62

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


68 69 70 71
(** Abstract syntax of ML *)

open Ident
open Ity
Mário Pereira's avatar
Mário Pereira committed
72
open Ty
Mário Pereira's avatar
Mário Pereira committed
73
open Term
74
open Printer
75 76 77

module ML = struct

78 79
  open Expr

80
  type ty =
81
    | Tvar    of tvsymbol
82 83 84
    | Tapp    of ident * ty list
    | Ttuple  of ty list

85 86 87
  type is_ghost = bool

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

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

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

110
  type expr = {
Mário Pereira's avatar
Mário Pereira committed
111 112 113
    e_node   : expr_node;
    e_ity    : ity;
    e_effect : effect;
114
    (* TODO: add the set of free variables? *)
115 116 117 118
  }

  and expr_node =
    | Econst  of Number.integer_constant
119
    | Evar    of pvsymbol
120
    | Eapp    of rsymbol * expr list
121
    | Efun    of var list * expr
122 123
    | Elet    of pvsymbol * expr * expr
    | Eletrec of is_rec * (rsymbol * var list * expr) list * expr
124 125
    | Eif     of expr * expr * expr
    | Ecast   of expr * ty
126
    | Eassign of (rsymbol * pvsymbol) list
127 128 129 130 131 132
    | 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
133
    | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
134
    | Eraise  of exn * expr option
135
    | Etry    of expr * (exn * pvsymbol option * expr) list
136 137 138 139 140 141 142 143 144
    | Eabsurd

  type is_mutable = bool

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

145 146 147 148 149 150 151
  type its_defn = {
    its_name    : ident;
    its_args    : tvsymbol list;
    its_private : bool;
    its_def     : typedef option;
  }

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

158
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
159 160
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

161
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
162 163 164 165
  let ml_let id e1 e2 =
    Elet (id, e1, e2)

  let tunit = Ttuple []
166

167 168 169 170 171
  let enope = Eblock []

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

172 173 174 175 176
  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; }

177 178 179 180 181 182 183 184
  let eseq e1 e2 =
    match e1.e_node, e2.e_node with
    | Eblock [], e | e, Eblock [] -> e
    | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
    | _, Eblock e2 -> Eblock (e1 :: e2)
    | Eblock e1, _ -> Eblock (e1 @ [e2])
    | _ -> Eblock [e1; e2]

185
end
Mário Pereira's avatar
Mário Pereira committed
186

187 188 189 190 191 192 193 194 195 196
type info = {
  info_syn          : syntax_map;
  info_convert      : syntax_map;
  info_current_th   : Theory.theory;
  info_current_mo   : Pmodule.pmodule option;
  info_th_known_map : Decl.known_map;
  info_mo_known_map : Pdecl.known_map;
  info_fname        : string option;
}

Mário Pereira's avatar
Mário Pereira committed
197 198 199 200 201 202 203 204 205
(** 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
206 207 208 209
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
210
       ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
211 212 213 214 215 216 217 218
    | 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

219 220 221
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251
  let filter_ghost_params l =
    let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
    let p e = not e.pv_ghost in
    let rec filter_ghost_params_cps l k =
      match l with
      | [] -> k []
      | e :: r ->
        filter_ghost_params_cps r
          (fun fr -> k (if p e then (def e) :: fr else fr))
    in
    filter_ghost_params_cps l (fun x -> x)

  let filter2_ghost_params p def al l =
    let rec filter2_ghost_params_cps l k =
      match l with
      | []  -> k []
      | [e] -> k (if p e then [def e] else [al e])
      | e :: r ->
        filter2_ghost_params_cps r
          (fun fr -> k (if p e then (def e) :: fr else fr))
    in
    filter2_ghost_params_cps l (fun x -> x)

  let rec filter_ghost_params_pat = function
    | MaskVisible -> Format.printf "visible@\n"
    | MaskGhost   -> Format.printf "ghost@\n"
    | MaskTuple l ->
      Format.printf "list@\n";
      List.iter (filter_ghost_params_pat) l

252 253 254
  let rec pat p =
    match p.pat_node with
    | Pwild ->
255
      ML.Pwild
256
    | Pvar vs ->
257
      ML.Pident vs.vs_name
258
    | Por (p1, p2) ->
259
      ML.Por (pat p1, pat p2)
260
    | Pas (p, vs) ->
261
      ML.Pas (pat p, vs.vs_name)
262
    | Papp (ls, pl) when is_fs_tuple ls ->
263
      ML.Ptuple (List.map pat pl)
264
    | Papp (ls, pl) ->
265 266 267 268 269 270 271
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
      let pat_pl = List.fold_left2
          (fun acc pv pp -> if not pv.pv_ghost then (pat pp) :: acc else acc)
          [] args pl
      in
      ML.Papp (ls.ls_name, List.rev pat_pl)
272

Mário Pereira's avatar
Mário Pereira committed
273 274
  (** programs *)

275 276 277 278 279
  let pv_name pv = pv.pv_vs.vs_name

  let is_underscore pv =
    (pv_name pv).id_string = "_" && ity_equal pv.pv_ity ity_unit

280 281 282
  (* individual types *)
  let rec ity t =
    match t.ity_node with
283
    | Ityvar (tvs, _) ->
284
      ML.Tvar tvs
285
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
286
      ML.Ttuple (List.map ity itl)
287
    | Ityapp ({its_ts = ts}, itl, _) ->
288 289 290 291
      ML.Tapp (ts.ts_name, List.map ity itl)
    | Ityreg {reg_its = its; reg_args = args} ->
      let args = List.map ity args in
      ML.Tapp (its.its_ts.ts_name, args)
Mário Pereira's avatar
Mário Pereira committed
292

Mário Pereira's avatar
Mário Pereira committed
293
  let pvty pv =
294 295 296 297 298
    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
299

300 301 302 303
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
304 305 306 307
  (* function arguments *)
  let args = (* point-free *)
    List.map pvty

308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324
  let app info rs pvl =
    let isconstructor () =
      match Mid.find_opt rs.rs_name info.info_mo_known_map with
      | Some {pd_node = PDtype its} ->
        let is_constructor its =
          List.exists (rs_equal rs) its.itd_constructors in
        List.exists is_constructor its
      | _ -> false
    in
    match pvl with
    | pvl when isconstructor () -> filter_ghost_params pvl
    | pvl ->
      let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
      let al _ = ML.mk_unit in
      let p e = not e.pv_ghost in
      filter2_ghost_params p def al pvl

Mário Pereira's avatar
Mário Pereira committed
325
  (* expressions *)
326
  let rec expr info ({e_effect = eff} as e) =
327
    (* assert (not eff.eff_ghost); *)
Mário Pereira's avatar
Mário Pereira committed
328
    match e.e_node with
329 330 331
    | 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
332
    | Evar pvs ->
333 334 335 336 337 338
      ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff
    | Elet (LDvar (pvs, e1), e2) when is_underscore pvs ->
      ML.mk_expr (ML.eseq (expr info e1) (expr info e2)) (ML.I e.e_ity) eff
    | Elet (LDvar (pvs, e1), e2) when e_ghost e1 ->
      let ml_let = ML.ml_let pvs ML.mk_unit (expr info e2) in
       ML.mk_expr ml_let (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
339
    | Elet (LDvar (pvs, e1), e2) ->
340
       let ml_let = ML.ml_let pvs (expr info e1) (expr info e2) in
341
       ML.mk_expr ml_let (ML.I e.e_ity) eff
342 343 344 345
    | Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs ->
      ML.mk_unit
    | Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
      ML.mk_unit
346
    | Eexec ({c_node = Capp (rs, pvl)}, _) ->
347 348
      let pvl = app info rs pvl in
      ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
349
    | Eabsurd ->
350 351 352
      ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
    | Ecase (e1, _) when e_ghost e1 ->
      ML.mk_unit
353
    | Ecase (e1, pl) ->
354 355
       let e1 = expr info e1 in
       let pl = List.map (ebranch info) pl in
356 357 358
       ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) eff
    | Eassert _ ->
       ML.mk_unit
359
    | Eif (e1, e2, e3) ->
360 361 362
       let e1 = expr info e1 in
       let e2 = expr info e2 in
       let e3 = expr info e3 in
363
       ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
364
    | Eghost eg ->
365 366 367
      expr info eg (* it keeps its ghost status *)
    | Eassign [(_, rs, pv)] ->
      ML.mk_expr (ML.Eassign [(rs, pv)]) (ML.I e.e_ity) eff
368 369
    | _ -> (* TODO *) assert false

370 371
  and ebranch info ({pp_pat = p} as pp, e) =
    (filter_ghost_params_pat pp.pp_mask; pat p, expr info e)
372

373 374 375 376
  let its_args ts = ts.its_ts.ts_args
  let itd_name td = td.itd_its.its_ts.ts_name

  (* type declarations/definitions *)
377
  let tdef itd =
378
    let s = itd.itd_its in
379 380 381 382 383 384 385 386 387 388 389 390 391 392 393
    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
394 395
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
396
         ML.mk_its_defn id args is_private None
397
      | None, cl, [] ->
398 399 400 401 402
         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))
403
      | Some t, _, _ ->
404
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
405
    end
Mário Pereira's avatar
Mário Pereira committed
406 407

  (* program declarations *)
408
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
409
    match pd.pd_node with
410 411
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
      []
412
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
413 414 415 416 417 418
      let args_filter =
        let p (_, _, is_ghost) = not is_ghost in
        let def = fun x -> x in
        let al = fun x -> x in
        filter2_ghost_params p def al (args cty.cty_args) in
      [ML.Dlet (false, [rs, args_filter, expr info e])]
419
    | PDlet (LDrec rl) ->
420 421 422 423 424 425 426 427 428 429 430 431 432
      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
          let args_filter =
            let p (_, _, is_ghost) = not is_ghost in
            let def = fun x -> x in
            let al = fun x -> x in
            filter2_ghost_params p def al (args rs.rs_cty.cty_args) in
          rs, args_filter, expr info e) rl
      in
      [ML.Dlet (true, rec_def)]
    | PDlet (LDsym _)
    | PDlet (LDvar (_, _))
Mário Pereira's avatar
Mário Pereira committed
433
    | PDpure ->
434
      []
435
    | PDtype itl ->
436 437
       [ML.Dtype (List.map tdef itl)]
    | PDexn xs ->
438
       if ity_equal xs.xs_ity ity_unit then
439
         [ML.Dexn (xs, None)]
440
       else
441
         [ML.Dexn (xs, Some (ity xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
442 443

  (* unit module declarations *)
444
  let mdecl info = function
Mário Pereira's avatar
Mário Pereira committed
445
    | Udecl pd ->
446
       pdecl info pd
447
    |  _ -> (* TODO *) []
Mário Pereira's avatar
Mário Pereira committed
448 449

  (* modules *)
450 451
  let module_ info m =
    List.concat (List.map (mdecl info) m.mod_units)
Mário Pereira's avatar
Mário Pereira committed
452 453

end
Mário Pereira's avatar
Mário Pereira committed
454 455 456

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