compile.ml 34.6 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

(*
  - "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 = ...")
*)

(** Abstract syntax of ML *)

open Ident
open Ity
Mário Pereira's avatar
Mário Pereira committed
25
open Ty
Mário Pereira's avatar
Mário Pereira committed
26
open Term
27

Mário Pereira's avatar
Mário Pereira committed
28 29 30 31 32 33 34 35
let clean_name fname =
  (* TODO: replace with Filename.remove_extension
   * after migration to OCaml 4.04+ *)
  let remove_extension s =
    try Filename.chop_extension s with Invalid_argument _ -> s in
  let f = Filename.basename fname in (remove_extension f)

let module_name ?fname path t =
Mário Pereira's avatar
Mário Pereira committed
36
  let fname = match fname, path with
Mário Pereira's avatar
Mário Pereira committed
37 38 39 40 41
    | None, "why3"::_ -> "why3"
    | None, _   -> String.concat "__" path
    | Some f, _ -> clean_name f in
  fname ^ "__" ^ t

42
module ML = struct
43
  open Expr
44
  open Mltree
Mário Pereira's avatar
Mário Pereira committed
45

46
  let rec get_decl_name = function
Mário Pereira's avatar
Mário Pereira committed
47
    | Dtype itdefl ->
48
        let add_id = function (* add name of constructors and projections *)
Mário Pereira's avatar
Mário Pereira committed
49 50 51 52 53
          | Some (Ddata l)   -> List.map (fun (idc,    _) -> idc) l
          | Some (Drecord l) -> List.map (fun (_, idp, _) -> idp) l
          | _ -> [] in
        let add_td_ids {its_name = id; its_def = def} = id :: (add_id def) in
        List.flatten (List.map add_td_ids itdefl)
Mário Pereira's avatar
Mário Pereira committed
54
    | Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
55 56
    | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
    | Dlet (Lsym ({rs_name=id}, _, _, _))
Mário Pereira's avatar
Mário Pereira committed
57
    | Dlet (Lany ({rs_name=id}, _, _))
58
    | Dexn ({xs_name=id}, _) -> [id]
59
    | Dmodule (_, dl) -> List.concat (List.map get_decl_name dl)
Mário Pereira's avatar
Mário Pereira committed
60

61
  let rec add_known_decl decl k_map id =
Mário Pereira's avatar
Mário Pereira committed
62
    match decl with
63
    | Dmodule (_, dl) ->
64 65 66 67
        let add_decl k_map d =
          let idl = get_decl_name d in
          List.fold_left (add_known_decl d) k_map idl in
        List.fold_left add_decl k_map dl
68
    | _ -> Mid.add id decl k_map
Mário Pereira's avatar
Mário Pereira committed
69

Mário Pereira's avatar
Mário Pereira committed
70 71
  let rec iter_deps_ty f = function
    | Tvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
72
    | Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
Mário Pereira's avatar
Mário Pereira committed
73 74 75
    | Ttuple ty_l -> List.iter (iter_deps_ty f) ty_l

  let iter_deps_typedef f = function
Mário Pereira's avatar
Mário Pereira committed
76
    | Ddata constrl ->
77
        List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
Mário Pereira's avatar
Mário Pereira committed
78
    | Drecord pjl -> List.iter (fun (_, _, ty) -> iter_deps_ty f ty) pjl
Mário Pereira's avatar
Mário Pereira committed
79
    | Dalias ty -> iter_deps_ty f ty
80
    | Drange _ | Dfloat _ -> ()
Mário Pereira's avatar
Mário Pereira committed
81 82 83 84

  let iter_deps_its_defn f its_d =
    Opt.iter (iter_deps_typedef f) its_d.its_def

Mário Pereira's avatar
Mário Pereira committed
85 86 87 88 89 90 91 92 93 94 95
  let iter_deps_args f =
    List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg)

  let rec iter_deps_xbranch f (xs, _, e) =
    f xs.xs_name;
    iter_deps_expr f e

  and iter_deps_pat_list f patl =
    List.iter (iter_deps_pat f) patl

  and iter_deps_pat f = function
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
96
    | Pwild | Pvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
97
    | Papp (ls, patl) ->
98 99
        f ls.ls_name;
        iter_deps_pat_list f patl
Mário Pereira's avatar
Mário Pereira committed
100 101
    | Ptuple patl -> iter_deps_pat_list f patl
    | Por (p1, p2) ->
102 103
        iter_deps_pat f p1;
        iter_deps_pat f p2
Mário Pereira's avatar
Mário Pereira committed
104 105 106
    | Pas (p, _) -> iter_deps_pat f p

  and iter_deps_expr f e = match e.e_node with
Mário Pereira's avatar
Mário Pereira committed
107
    | Econst _ | Evar _ | Eabsurd | Ehole -> ()
Mário Pereira's avatar
Mário Pereira committed
108
    | Eapp (rs, exprl) ->
109
        f rs.rs_name; List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
110
    | Efun (args, e) ->
111 112
        List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
        iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
113
    | Elet (Lvar (_, e1), e2) ->
114 115
        iter_deps_expr f e1;
        iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
116
    | Elet (Lsym (_, ty_result, args, e1), e2) ->
117 118 119 120
        iter_deps_ty f ty_result;
        List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
        iter_deps_expr f e1;
        iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
121
    | Elet (Lany (_, ty_result, args), e2) ->
122 123 124
        iter_deps_ty f ty_result;
        List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
        iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
125
    | Elet ((Lrec rdef), e) ->
126 127 128 129 130
        List.iter
          (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
             f rs.rs_name; iter_deps_args f args;
             iter_deps_expr f e; iter_deps_ty f res) rdef;
        iter_deps_expr f e
131
    | Ematch (e, branchl, xl) ->
132
        iter_deps_expr f e;
133 134
        List.iter (fun (p, e) -> iter_deps_pat f p; iter_deps_expr f e) branchl;
        List.iter (iter_deps_xbranch f) xl
Mário Pereira's avatar
Mário Pereira committed
135
    | Eif (e1, e2, e3) ->
136 137 138
        iter_deps_expr f e1;
        iter_deps_expr f e2;
        iter_deps_expr f e3
Mário Pereira's avatar
Mário Pereira committed
139
    | Eblock exprl ->
140
        List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
141
    | Ewhile (e1, e2) ->
142 143
        iter_deps_expr f e1;
        iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
144
    | Efor (_, _, _, _, e) ->
145
        iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
146
    | Eraise (xs, None) ->
147
        f xs.xs_name
Mário Pereira's avatar
Mário Pereira committed
148
    | Eraise (xs, Some e) ->
149 150
        f xs.xs_name;
        iter_deps_expr f e
151
    | Eexn (_xs, None, e) -> (* FIXME? How come we never do binding here? *)
152
        iter_deps_expr f e
153
    | Eexn (_xs, Some ty, e) -> (* FIXME? How come we never do binding here? *)
154 155
        iter_deps_ty f ty;
        iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
156
    | Eassign assingl ->
157
        List.iter (fun (_, rs, _) -> f rs.rs_name) assingl
Mário Pereira's avatar
Mário Pereira committed
158
    | Eignore e -> iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
159

160
  let rec iter_deps f = function
Mário Pereira's avatar
Mário Pereira committed
161
    | Dtype its_dl ->
162
        List.iter (iter_deps_its_defn f) its_dl
Mário Pereira's avatar
Mário Pereira committed
163
    | Dlet (Lsym (_rs, ty_result, args, e)) ->
164 165 166
        iter_deps_ty f ty_result;
        iter_deps_args f args;
        iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
167
    | Dlet (Lany (_rs, ty_result, args)) ->
168 169
        iter_deps_ty f ty_result;
        iter_deps_args f args
Mário Pereira's avatar
Mário Pereira committed
170
    | Dlet (Lrec rdef) ->
171 172 173 174
        List.iter
          (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
             f rs.rs_name; iter_deps_args f args;
             iter_deps_expr f e; iter_deps_ty f res) rdef
Mário Pereira's avatar
Mário Pereira committed
175 176 177
    | Dlet (Lvar (_, e)) -> iter_deps_expr f e
    | Dexn (_, None) -> ()
    | Dexn (_, Some ty) -> iter_deps_ty f ty
178
    | Dmodule (_, dl) -> List.iter (iter_deps f) dl
179

180
  let ity_unit = I Ity.ity_unit
Mário Pereira's avatar
Mário Pereira committed
181

182 183 184 185 186 187 188 189 190 191
  let ity_of_mask ity mask =
    let mk_ty acc ty = function MaskGhost -> acc | _ -> ty :: acc in
    match ity, mask with
    | _, MaskGhost   -> ity_unit
    | _, MaskVisible -> ity
    | I ({ity_node = Ityapp ({its_ts = s}, tl, _)}), MaskTuple m
      when is_ts_tuple s && List.length tl = List.length m ->
        let tl = List.fold_left2 mk_ty [] tl m in
        I (ity_tuple tl)
    | _ -> ity (* FIXME ? *)
192

193 194 195 196
  let mk_expr e_node e_ity mask e_effect e_label =
    { e_node; e_ity = ity_of_mask e_ity mask; e_effect; e_label; }

  let tunit = Ttuple []
Mário Pereira's avatar
Mário Pereira committed
197 198 199 200

  let is_unit = function
    | I i -> ity_equal i Ity.ity_unit
    | _ -> false
Mário Pereira's avatar
Mário Pereira committed
201

202 203
  let enope = Eblock []

Mário Pereira's avatar
Mário Pereira committed
204
  let mk_hole =
205
    mk_expr Ehole (I Ity.ity_unit) MaskVisible Ity.eff_empty Slab.empty
Mário Pereira's avatar
Mário Pereira committed
206

207 208
  let mk_var id ty ghost = (id, ty, ghost)

209 210
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

211 212
  let mk_its_defn its_name its_args its_private its_def =
    { its_name; its_args; its_private; its_def; }
213

214 215
  (* smart constructors *)
  let e_unit =
216
    mk_expr enope (I Ity.ity_unit) MaskVisible Ity.eff_empty Slab.empty
217 218 219 220 221 222 223 224 225 226 227 228 229 230 231

  let var_defn pv e =
    Lvar (pv, e)

  let sym_defn f ty_res args e =
    Lsym (f, ty_res, args, e)

  let e_let ld e = mk_expr (Elet (ld, e))

  let e_app rs pvl =
    mk_expr (Mltree.Eapp (rs, pvl))

  let e_fun args e = mk_expr (Efun (args, e))

  let e_ignore e =
Mário Pereira's avatar
Mário Pereira committed
232
    if is_unit e.e_ity then e
233
    else mk_expr (Eignore e) ity_unit MaskVisible e.e_effect e.e_label
Mário Pereira's avatar
Mário Pereira committed
234

235
  let e_if e1 e2 e3 =
Mário Pereira's avatar
Mário Pereira committed
236
    mk_expr (Mltree.Eif (e1, e2, e3)) e2.e_ity
237 238 239 240

  let e_while e1 e2 =
    mk_expr (Mltree.Ewhile (e1, e2)) ity_unit

241 242 243
  let e_for pv1 pv2 dir pv3 e1 =
    mk_expr (Mltree.Efor (pv1, pv2, dir, pv3, e1)) ity_unit

244 245
  let e_match e bl xl =
    mk_expr (Mltree.Ematch (e, bl, xl))
246

247
(*
248 249 250 251
  let e_match_exn e bl eff_bl lbl_match xl =
    let ity = match bl with (_, d) :: _ -> d.e_ity | [] -> assert false in
    let e = e_match e bl ity eff_bl lbl_match in
    mk_expr (Mltree.Etry (e, true, xl))
252
*)
253

254 255
  let e_assign al ity mask eff lbl =
    if al = [] then e_unit else mk_expr (Mltree.Eassign al) ity mask eff lbl
256

257 258 259 260 261 262 263 264 265 266 267
  let e_absurd =
    mk_expr Eabsurd

  let e_seq e1 e2 =
    let e = match e1.e_node, e2.e_node with
      | (Eblock [] | Ehole), e | e, (Eblock [] | Ehole) -> e
      | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
      | _, Eblock e2 -> Eblock (e1 :: e2)
      | Eblock e1, _ -> Eblock (e1 @ [e2])
      | _ -> Eblock [e1; e2] in
    mk_expr e
268

269
  let var_list_of_pv_list pvl =
270 271
    let mk_var pv = mk_expr (Mltree.Evar pv) (Mltree.I pv.pv_ity)
      MaskVisible eff_empty Slab.empty in
272 273
    List.map mk_var pvl

274
end
Mário Pereira's avatar
Mário Pereira committed
275 276 277 278 279

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
280 281 282
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
283

Mário Pereira's avatar
Mário Pereira committed
284 285 286
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
287 288 289 290 291
  (* remove ghost components from tuple, using mask *)
  let visible_of_mask m sl = match m with
    | MaskGhost    -> assert false (* FIXME ? *)
    | MaskVisible  -> sl
    | MaskTuple ml ->
292 293 294
        let add_ity acc m ity = if mask_ghost m then acc else ity :: acc in
        if List.length sl < List.length ml then sl (* FIXME ? much likely... *)
        else List.fold_left2 add_ity [] ml sl
Mário Pereira's avatar
Mário Pereira committed
295

Mário Pereira's avatar
Mário Pereira committed
296 297 298 299
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
300
        Mltree.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
301
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
302
        Mltree.Ttuple (List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
303
    | Tyapp (ts, tyl) ->
304
        Mltree.Tapp (ts.ts_name, List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
305 306 307 308

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

Mário Pereira's avatar
Mário Pereira committed
309 310 311
  let rec filter_ghost_params p def = function
    | [] -> []
    | pv :: l ->
312 313
        if p pv then def pv :: (filter_ghost_params p def l)
        else filter_ghost_params p def l
314

315
  let rec filter_out_ghost_rdef = function
Mário Pereira's avatar
Mário Pereira committed
316
    | [] -> []
317
    | { rec_sym = rs; rec_rsym = rrs } :: l when rs_ghost rs || rs_ghost rrs ->
318
        filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
319
    | rdef :: l ->
320
        rdef :: filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
321

Mário Pereira's avatar
Mário Pereira committed
322
  let rec pat m p = match p.pat_node with
323
    | Pwild ->
324
        Mltree.Pwild
325
    | Pvar vs when (restore_pv vs).pv_ghost ->
326
        Mltree.Pwild
327
    | Pvar vs ->
328
        Mltree.Pvar vs
329
    | Por (p1, p2) ->
330
        Mltree.Por (pat m p1, pat m p2)
331
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
332
        pat m p
333
    | Pas (p, vs) ->
334
        Mltree.Pas (pat m p, vs)
335
    | Papp (ls, pl) when is_fs_tuple ls ->
336
        let pl = List.rev (visible_of_mask m pl) in
337 338 339 340
        begin match pl with
          | [] -> Mltree.Pwild
          | [p] -> pat m p
          | _ -> Mltree.Ptuple (List.map (pat m) pl) end
341
    | Papp (ls, pl) ->
342 343 344 345 346
        let rs = restore_rs ls in
        let args = rs.rs_cty.cty_args in
        let mk acc pv pp = if not pv.pv_ghost then pat m pp :: acc else acc in
        let pat_pl = List.fold_left2 mk [] args pl in
        Mltree.Papp (ls, List.rev pat_pl)
347

Mário Pereira's avatar
Mário Pereira committed
348 349
  (** programs *)

350 351
  let pv_name pv = pv.pv_vs.vs_name

352
  (* individual types *)
Mário Pereira's avatar
Mário Pereira committed
353 354
  let mlty_of_ity mask t =
    let rec loop t = match t.ity_node with
355
      | _ when mask_equal mask MaskGhost -> ML.tunit
356
      | Ityvar tvs ->
357 358
          Mltree.Tvar tvs
      | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
359
          let itl = visible_of_mask mask itl in
360 361 362 363 364 365
          Mltree.Ttuple (List.map loop itl)
      | Ityapp ({its_ts = ts}, itl, _) ->
          Mltree.Tapp (ts.ts_name, List.map loop itl)
      | Ityreg {reg_its = its; reg_args = args} ->
          let args = List.map loop args in
          Mltree.Tapp (its.its_ts.ts_name, args) in
Mário Pereira's avatar
Mário Pereira committed
366
    loop t
Mário Pereira's avatar
Mário Pereira committed
367

Mário Pereira's avatar
Mário Pereira committed
368
  let pvty pv =
Mário Pereira's avatar
Mário Pereira committed
369
    if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true
Mário Pereira's avatar
Mário Pereira committed
370
    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
371

372 373 374
  let for_direction = function
    | To -> Mltree.To
    | DownTo -> Mltree.DownTo
375

376
  let isconstructor info rs = (* TODO *)
377
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
378
    | Some {pd_node = PDtype its} ->
379 380 381
        let is_constructor its =
          List.exists (rs_equal rs) its.itd_constructors in
        List.exists is_constructor its
Mário Pereira's avatar
Mário Pereira committed
382 383
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
384 385 386 387
  let is_singleton_imutable itd =
    let not_g e = not (rs_ghost e) in
    let pjl = itd.itd_fields in
    let mfields = itd.itd_its.its_mfields in
388
    let pv_equal_field rs = pv_equal (fd_of_rs rs) in
Mário Pereira's avatar
Mário Pereira committed
389 390 391 392
    let get_mutable rs = List.exists (pv_equal_field rs) mfields in
    match filter_ghost_params not_g get_mutable pjl with
    | [is_mutable] -> not is_mutable
    | _ -> false
Mário Pereira's avatar
Mário Pereira committed
393

394
  let get_record_itd info rs =
395
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
396
    | Some {pd_node = PDtype itdl} ->
397 398 399 400 401
        let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
        let itd = match rs.rs_field with
          | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
          | None -> List.find (fun itd -> f itd.itd_constructors) itdl in
        if itd.itd_fields = [] then None else Some itd
402 403 404 405 406 407 408 409 410 411 412 413 414 415
    | _ -> None

  let is_optimizable_record_itd itd =
    not itd.itd_its.its_private && is_singleton_imutable itd

  let is_optimizable_record_rs info rs =
    Opt.fold (fun _ -> is_optimizable_record_itd) false (get_record_itd info rs)

  let is_empty_record_itd itd =
    let is_ghost rs = rs_ghost rs in
    List.for_all is_ghost itd.itd_fields

  let is_empty_record info rs =
    Opt.fold (fun _ -> is_empty_record_itd) false (get_record_itd info rs)
Mário Pereira's avatar
Mário Pereira committed
416

Mário Pereira's avatar
Mário Pereira committed
417
  let mk_eta_expansion rs pvl ({cty_args = ca; cty_effect = ce} as c) =
Mário Pereira's avatar
Mário Pereira committed
418
    (* FIXME : effects and types of the expression in this situation *)
419
    let mv = MaskVisible in
Mário Pereira's avatar
Mário Pereira committed
420
    let args_f =
Mário Pereira's avatar
Mário Pereira committed
421
      let def pv =
422
        pv_name pv, mlty_of_ity (mask_of_pv pv) pv.pv_ity, pv.pv_ghost in
Mário Pereira's avatar
Mário Pereira committed
423
      filter_ghost_params pv_not_ghost def ca in
Mário Pereira's avatar
Mário Pereira committed
424
    let args =
425 426
      let def pv = ML.mk_expr (Mltree.Evar pv) (Mltree.I pv.pv_ity) mv
        eff_empty Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
427
      let args = filter_ghost_params pv_not_ghost def pvl in
Mário Pereira's avatar
Mário Pereira committed
428
      let extra_args = List.map def ca in args @ extra_args in
429 430 431
    let eapp = ML.mk_expr (Mltree.Eapp (rs, args)) (Mltree.C c) mv
      ce Slab.empty in
    ML.mk_expr (Mltree.Efun (args_f, eapp)) (Mltree.C c) mv ce Slab.empty
Mário Pereira's avatar
Mário Pereira committed
432

433 434 435 436 437 438
  (* function arguments *)
  let filter_params args =
    let args = List.map pvty args in
    let p (_, _, is_ghost) = not is_ghost in
    List.filter p args

439 440 441
  let params args =
    let args = filter_params args in
    if args = [] then [ML.mk_var_unit ()] else args
442

Mário Pereira's avatar
Mário Pereira committed
443 444
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
445
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
446
      | pv :: l1, arg :: l2 ->
Mário Pereira's avatar
Mário Pereira committed
447
          if p pv && p arg then def pv :: loop (l1, l2) else loop (l1, l2)
Mário Pereira's avatar
Mário Pereira committed
448 449 450
      | _ -> assert false
    in loop (pvl, cty_args)

451 452 453 454 455
  let app pvl cty_args f_zero =
    let def pv = ML.mk_expr (Mltree.Evar pv) (Mltree.I pv.pv_ity) MaskVisible
      eff_empty Slab.empty in
    let args = filter_params_cty pv_not_ghost def pvl cty_args in
    f_zero args
Mário Pereira's avatar
Mário Pereira committed
456

457 458
  (* build the set of type variables from functions arguments *)
  let rec add_tvar acc = function
459 460
    | Mltree.Tvar tv -> Stv.add tv acc
    | Mltree.Tapp (_, tyl) | Mltree.Ttuple tyl ->
461
        List.fold_left add_tvar acc tyl
462

Mário Pereira's avatar
Mário Pereira committed
463
  (* expressions *)
464
  let rec expr info svar mask ({e_effect = eff; e_label = lbl} as e) =
465
    assert (not (e_ghost e));
466
    assert (not (mask_spill e.e_mask mask));
Mário Pereira's avatar
Mário Pereira committed
467 468 469 470 471 472 473 474
    let pv_list_of_mask pvl mask =
      let mk_pv_of_mask acc pv = function MaskGhost -> acc | _ -> pv :: acc in
      match mask with
      | MaskGhost   -> []
      | MaskVisible -> pvl
      | MaskTuple m -> assert (List.length m = List.length pvl);
          let pvl = List.fold_left2 mk_pv_of_mask [] pvl m in
          List.rev pvl in
Mário Pereira's avatar
Mário Pereira committed
475
    match e.e_node with
476 477
    | Econst _ | Evar _ | Eexec ({c_node = Cfun _}, _) (* FIXME *)
      when mask = MaskGhost ->
478
        ML.e_unit
479
    | Econst c ->
480
        let c = match c with Number.ConstInt c -> c | _ -> assert false in
481 482 483 484 485
        ML.mk_expr (Mltree.Econst c) (Mltree.I e.e_ity) mask eff lbl
    | Evar pv ->
        ML.mk_expr (Mltree.Evar pv) (Mltree.I e.e_ity) mask eff lbl
    | Elet (LDvar (_, e1), e2) when e_ghost e1 ->
        expr info svar mask e2
486
    | Elet (LDvar (_, e1), e2) when e_ghost e2 ->
487
        (* sequences are transformed into [let o = e1 in e2] by A-normal form *)
488
        expr info svar MaskGhost e1
Mário Pereira's avatar
Mário Pereira committed
489 490
    | Elet (LDvar (pv, e1), e2)
      when pv.pv_ghost || not (Mpv.mem pv e2.e_effect.eff_reads) ->
491
        if eff_pure e1.e_effect then expr info svar mask e2
492 493
        else let e1 = expr info svar MaskGhost e1 in
          ML.e_seq e1 (expr info svar mask e2) (Mltree.I e.e_ity) mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
494
    | Elet (LDvar (pv, e1), e2) ->
495 496
        let ld = ML.var_defn pv (expr info svar MaskVisible e1) in
        ML.e_let ld (expr info svar mask e2) (Mltree.I e.e_ity) mask eff lbl
497 498
    | Elet (LDsym (rs, _), ein) when rs_ghost rs ->
        expr info svar mask ein
499
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
500 501
        let args = params cty.cty_args in
        let res = mlty_of_ity cty.cty_mask cty.cty_result in
502 503
        let ld = ML.sym_defn rs res args (expr info svar cty.cty_mask ef) in
        ML.e_let ld (expr info svar mask ein) (Mltree.I e.e_ity) mask eff lbl
504
    | Elet (LDsym (rs, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein)
505
      when isconstructor info rs_app -> (* partial application of constructor *)
506 507 508 509 510
        let eta_app = mk_eta_expansion rs_app pvl cty in
        let mk_func pv f = ity_func pv.pv_ity f in
        let func = List.fold_right mk_func cty.cty_args cty.cty_result in
        let res = mlty_of_ity cty.cty_mask func in
        let ld = ML.sym_defn rs res [] eta_app in
511 512
        let ein = expr info svar mask ein in
        ML.e_let ld ein (Mltree.I e.e_ity) mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
513
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
514 515 516 517 518
        (* partial application *) (* FIXME -> zero arguments functions *)
        let cmk = cty.cty_mask in
        let ceff = cty.cty_effect in
        let pvl = app pvl rs_app.rs_cty.cty_args (fun x -> x) in
        let eapp = ML.e_app rs_app pvl (Mltree.C cty) cmk ceff Slab.empty in
519 520
        let res = mlty_of_ity cty.cty_mask cty.cty_result in
        let ld = ML.sym_defn rsf res (params cty.cty_args) eapp in
521 522
        let ein = expr info svar mask ein in
        ML.e_let ld ein (Mltree.I e.e_ity) mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
523
    | Elet (LDrec rdefl, ein) ->
524 525
        let rdefl = filter_out_ghost_rdef rdefl in
        let def = function
526 527
          | { rec_sym = rs1; rec_rsym = rs2;
              rec_fun = {c_node = Cfun ef; c_cty = cty} } ->
528 529
              let res = mlty_of_ity rs1.rs_cty.cty_mask rs1.rs_cty.cty_result in
              let args = params cty.cty_args in
530
              let new_svar =
531 532 533
                let args' = List.map (fun (_, ty, _) -> ty) args in
                let svar  = List.fold_left add_tvar Stv.empty args' in
                add_tvar svar res in
534
              let new_svar = Stv.diff svar new_svar in
535
              let ef = expr info (Stv.union svar new_svar) ef.e_mask ef in
536
              { Mltree.rec_sym  = rs1;  Mltree.rec_rsym = rs2;
537 538
                Mltree.rec_args = args; Mltree.rec_exp  = ef;
                Mltree.rec_res  = res;  Mltree.rec_svar = new_svar; }
539 540 541
          | _ -> assert false in
        let rdefl = List.map def rdefl in
        if rdefl <> [] then
542 543
          let ein = expr info svar mask ein in
          let ml_letrec = Mltree.Elet (Mltree.Lrec rdefl, ein) in
544
          ML.mk_expr ml_letrec (Mltree.I e.e_ity) mask e.e_effect lbl
545 546 547 548 549
        else expr info svar mask ein
    | Eexec ({c_node = Capp (rs, [])}, _)  when is_rs_tuple rs ->
        ML.e_unit
    | Eexec ({c_node = Capp (rs, pvl)}, _) when is_rs_tuple rs ->
        let pvl = pv_list_of_mask pvl mask in
Mário Pereira's avatar
Mário Pereira committed
550
        let res_ity = ity_tuple (List.map (fun v -> v.pv_ity) pvl) in
551
        let pvl = ML.var_list_of_pv_list pvl in
552 553
        ML.e_app rs pvl (Mltree.I res_ity) mask eff lbl
    | Eexec ({c_node = Capp (rs, _)}, _) when is_empty_record info rs ->
Mário Pereira's avatar
Mário Pereira committed
554
        ML.e_unit
Mário Pereira's avatar
Mário Pereira committed
555
    | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
Mário Pereira's avatar
Mário Pereira committed
556
      when isconstructor info rs && cty.cty_args <> [] ->
557 558
        (* partial application of constructors *)
        mk_eta_expansion rs pvl cty
Mário Pereira's avatar
Mário Pereira committed
559
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
560 561 562
        let add_unit = function [] -> [ML.e_unit] | args -> args in
        let f_zero = if isconstructor info rs then fun x -> x else add_unit in
        let pvl = app pvl rs.rs_cty.cty_args f_zero in
563 564
        begin match pvl with
          | [pv_expr] when is_optimizable_record_rs info rs -> pv_expr
565
          | _ -> ML.e_app rs pvl (Mltree.I e.e_ity) mask eff lbl end
Mário Pereira's avatar
Mário Pereira committed
566
    | Eexec ({c_node = Cfun e; c_cty = {cty_args = []}}, _) ->
567
        (* abstract block *)
568
        expr info svar e.e_mask e
569 570 571
    | Eexec ({c_node = Cfun ef; c_cty = cty}, _) ->
        let ef = expr info svar e.e_mask ef in
        ML.e_fun (params cty.cty_args) ef (Mltree.I e.e_ity) mask eff lbl
572
    | Eexec ({c_node = Cany}, _) ->
573
        ML.mk_hole
574
    | Eabsurd ->
575
        ML.e_absurd (Mltree.I e.e_ity) mask eff lbl
576 577
    | Eassert _ ->
        ML.e_unit
578
    | Eif (e1, e2, e3) when e_ghost e1 ->
579 580
        (* if [e1] is ghost but the entire [if-then-else] expression doesn't,
           it must be the case one of the branches is [Eabsurd] *)
581 582
        if e2.e_node = Eabsurd then expr info svar mask e3
        else expr info svar mask e2
Mário Pereira's avatar
Mário Pereira committed
583
    | Eif (e1, e2, e3) when e_ghost e3 ->
584 585
        let e1 = expr info svar e1.e_mask e1 in
        let e2 = expr info svar mask e2 in
586
        ML.e_if e1 e2 ML.e_unit mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
587
    | Eif (e1, e2, e3) when e_ghost e2 ->
588 589
        let e1 = expr info svar e1.e_mask e1 in
        let e3 = expr info svar mask e3 in
590
        ML.e_if e1 ML.e_unit e3 mask eff lbl
591
    | Eif (e1, e2, e3) ->
592 593 594
        let e1 = expr info svar e1.e_mask e1 in
        let e2 = expr info svar mask e2 in
        let e3 = expr info svar mask e3 in
595
        ML.e_if e1 e2 e3 mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
596
    | Ewhile (e1, _, _, e2) ->
597 598
        let e1 = expr info svar e1.e_mask e1 in
        let e2 = expr info svar e2.e_mask e2 in
599
        ML.e_while e1 e2 mask eff lbl
600 601
    | Efor (pv1, (pv2, dir, pv3), _, _, efor) ->
        let dir = for_direction dir in
602
        let efor = expr info svar efor.e_mask efor in
603
        ML.e_for pv1 pv2 dir pv3 efor mask eff lbl
604 605
    | Eghost _ | Epure _ ->
        assert false
606
    | Eassign al ->
607 608
        let rm_ghost (_, rs, _) = not (rs_ghost rs) in
        let al = List.filter rm_ghost al in
609
        ML.e_assign al (Mltree.I e.e_ity) mask eff lbl
610
    | Ematch (e1, [], xl) when Mxs.is_empty xl ->
611
        expr info svar e1.e_mask e1
612
    | Ematch (e1, bl, xl) when e_ghost e1 ->
613 614 615 616 617
        assert (Mxs.is_empty xl); (* Expr ensures this for the time being *)
        (* if [e1] is ghost but the entire [match-with] expression isn't,
           it must be the case the first non-absurd branch is irrefutable *)
        (match bl with (* FIXME: skip absurd branches *)
         | [] -> assert false | (_, e) :: _ -> expr info svar e.e_mask e)
618
    | Ematch (e1, bl, xl) ->
619 620 621
        let e1 = expr info svar e1.e_mask e1 in
        let bl = List.map (ebranch info svar mask) bl in
        (* NOTE: why no pv_list_of_mask here? *)
622
        let mk_xl (xs, (pvl, e)) = xs, pvl, expr info svar mask e in
623
        let xl = List.map mk_xl (Mxs.bindings xl) in
624
        ML.e_match e1 bl xl (Mltree.I e.e_ity) mask eff lbl
625 626 627
    | Eraise (xs, ex) -> let ex = match expr info svar xs.xs_mask ex with
        | {Mltree.e_node = Mltree.Eblock []} -> None
        | e -> Some e in
628
        ML.mk_expr (Mltree.Eraise (xs, ex)) (Mltree.I e.e_ity) mask eff lbl
629
    | Eexn (xs, e1) ->
630
        if mask_ghost e1.e_mask then ML.mk_expr
631
          (Mltree.Eexn (xs, None, ML.e_unit)) (Mltree.I e.e_ity) mask eff lbl
632 633 634
        else let e1 = expr info svar xs.xs_mask e1 in
          let ty = if ity_equal xs.xs_ity ity_unit then None
            else Some (mlty_of_ity xs.xs_mask xs.xs_ity) in
635
        ML.mk_expr (Mltree.Eexn (xs, ty, e1)) (Mltree.I e.e_ity) mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
636 637
    | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
    | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
638

639
  and ebranch info svar mask ({pp_pat = p; pp_mask = m}, e) =
Mário Pereira's avatar
Mário Pereira committed
640 641 642
    (* if the [case] expression is not ghost but there is (at least) one ghost
       branch, then it must be the case that all the branches return [unit]
       and at least one of the non-ghost branches is effectful *)
643
    if e.e_effect.eff_ghost then (pat m p, ML.e_unit)
644
    else (pat m p, expr info svar mask e)
645

646
  (* type declarations/definitions *)
Mário Pereira's avatar
Mário Pereira committed
647
  let tdef itd =
648
    let s = itd.itd_its in
649
    let ddata_constructs = (* point-free *)
Mário Pereira's avatar
Mário Pereira committed
650
      List.map (fun ({rs_cty = cty} as rs) ->
651
          rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
652
          let args = List.filter pv_not_ghost cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
653
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args) in
Mário Pereira's avatar
Mário Pereira committed
654
    let drecord_fields ({rs_cty = cty} as rs) =
655
      (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields),
Mário Pereira's avatar
Mário Pereira committed
656
      rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
657
      mlty_of_ity cty.cty_mask cty.cty_result in
658 659 660
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
661
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
662
      | NoDef, [], [] ->
663
          ML.mk_its_defn id args is_private None
664
      | NoDef, cl, [] ->
665 666
          let cl = ddata_constructs cl in
          ML.mk_its_defn id args is_private (Some (Mltree.Ddata cl))
667
      | NoDef, _, pjl ->
668 669 670 671 672 673 674 675 676 677
          let p e = not (rs_ghost e) in
          let pjl = filter_ghost_params p drecord_fields pjl in
          begin match pjl with
            | [] -> ML.mk_its_defn id args is_private
                      (Some (Mltree.Dalias ML.tunit))
            | [_, _, ty_pj] when is_optimizable_record_itd itd ->
                ML.mk_its_defn id args is_private (Some (Mltree.Dalias ty_pj))
            | pjl ->
                ML.mk_its_defn id args is_private (Some (Mltree.Drecord pjl))
          end
678
      | Alias t, _, _ ->
679 680
          ML.mk_its_defn id args is_private (* FIXME ? is this a good mask ? *)
            (Some (Mltree.Dalias (mlty_of_ity MaskVisible t)))
681 682 683 684
      | Range r, [], [] ->
          assert (args = []); (* a range type is not polymorphic *)
          ML.mk_its_defn id [] is_private (Some (Mltree.Drange r))
      | Float ff, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
685
          assert (args = []); (* a float type is not polymorphic *)
686 687 688
          ML.mk_its_defn id [] is_private (Some (Mltree.Dfloat ff))
      | (Range _ | Float _), _, _ ->
          assert false (* cannot have constructors or fields *)
689
    end
Mário Pereira's avatar
Mário Pereira committed
690

Mário Pereira's avatar
Mário Pereira committed
691 692 693 694
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

695
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
696
    match pd.pd_node with
697 698 699 700 701
    | PDlet (LDvar (_, e)) when e_ghost e ->
        []
    | PDlet (LDvar (pv, e)) when pv.pv_ghost ->
        if eff_pure e.e_effect then []
        else let unit_ = create_pvsymbol (id_fresh "()") ity_unit in
702
          [Mltree.Dlet (Mltree.Lvar (unit_, expr info Stv.empty e.e_mask e))]
703
    | PDlet (LDvar (pv, e)) ->
704
        [Mltree.Dlet (Mltree.Lvar (pv, expr info Stv.empty e.e_mask e))]
705
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
706
        []
Mário Pereira's avatar
Mário Pereira committed
707
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cany})) ->
708 709 710
        let args = params cty.cty_args in
        let res = mlty_of_ity cty.cty_mask cty.cty_result in
        [Mltree.Dlet (Mltree.Lany (rs, res, args))]
711 712 713 714
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e}))
      when is_val e.e_node -> (* zero argument functions *)
        let res = mlty_of_ity cty.cty_mask cty.cty_result in
        [Mltree.Dlet (Mltree.Lany (rs, res, []))]
715
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
716 717
        let args = params cty.cty_args in
        let res = mlty_of_ity cty.cty_mask cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
718 719 720 721
        let svar =
          let args' = List.map (fun (_, ty, _) -> ty) args in
          let svar  = List.fold_left add_tvar Stv.empty args' in
          add_tvar svar res in
722
        let e = expr info svar cty.cty_mask e in
723
        [Mltree.Dlet (Mltree.Lsym (rs, res, args, e))]
724
    | PDlet (LDrec rl) ->
725 726 727 728 729 730 731 732 733
        let rl = filter_out_ghost_rdef rl in
        let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
          let e = match e.c_node with Cfun e -> e | _ -> assert false in
          let args = params rs1.rs_cty.cty_args in
          let res  = mlty_of_ity rs1.rs_cty.cty_mask rs1.rs_cty.cty_result in
          let svar =
            let args' = List.map (fun (_, ty, _) -> ty) args in
            let svar  = List.fold_left add_tvar Stv.empty args' in
            add_tvar svar res in
734
          let e = expr info svar rs1.rs_cty.cty_mask e in
735 736 737 738
          { Mltree.rec_sym  = rs1;  Mltree.rec_rsym = rs2;
            Mltree.rec_args = args; Mltree.rec_exp  = e;
            Mltree.rec_res  = res;  Mltree.rec_svar = svar; } in
        if rl = [] then [] else [Mltree.Dlet (Mltree.Lrec (List.map def rl))]
739
    | PDlet (LDsym _) | PDpure ->
740
        []
741
    | PDtype itl ->
742 743
        let itsd = List.map tdef itl in
        [Mltree.Dtype itsd]
744
    | PDexn xs ->
745 746
        if ity_equal xs.xs_ity ity_unit || xs.xs_mask = MaskGhost then
          [Mltree.Dexn (xs, None)]
747
        else [Mltree.Dexn (xs, Some (mlty_of_ity xs.xs_mask xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
748

Mário Pereira's avatar
Mário Pereira committed
749
  let pdecl_m m pd =
750