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

Mário Pereira's avatar
Mário Pereira committed
42 43 44 45
(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
46 47 48
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
49

50 51 52 53 54
  module ML = Mltree

  let debug_compile =
    Debug.register_info_flag ~desc:"Compilation" "compile"

Mário Pereira's avatar
Mário Pereira committed
55 56 57
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
58
  (* remove ghost components from tuple, using mask *)
59
  (* TODO : completely remove this function *)
Mário Pereira's avatar
Mário Pereira committed
60 61 62 63
  let visible_of_mask m sl = match m with
    | MaskGhost    -> assert false (* FIXME ? *)
    | MaskVisible  -> sl
    | MaskTuple ml ->
64 65
        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... *)
66
        else List.rev (List.fold_left2 add_ity [] ml sl)
Mário Pereira's avatar
Mário Pereira committed
67

Mário Pereira's avatar
Mário Pereira committed
68 69 70 71
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
72
        ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
73
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
74
        ML.Ttuple (List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
75
    | Tyapp (ts, tyl) ->
76
        ML.Tapp (ts.ts_name, List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
77 78 79 80

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

Mário Pereira's avatar
Mário Pereira committed
81 82 83
  let rec filter_ghost_params p def = function
    | [] -> []
    | pv :: l ->
84 85
        if p pv then def pv :: (filter_ghost_params p def l)
        else filter_ghost_params p def l
86

87
  let rec filter_out_ghost_rdef = function
Mário Pereira's avatar
Mário Pereira committed
88
    | [] -> []
89
    | { rec_sym = rs; rec_rsym = rrs } :: l when rs_ghost rs || rs_ghost rrs ->
90
        filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
91
    | rdef :: l ->
92
        rdef :: filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
93

Mário Pereira's avatar
Mário Pereira committed
94
  let rec pat m p = match p.pat_node with
95
    | Pwild ->
96
        ML.Pwild
97
    | Pvar vs when (restore_pv vs).pv_ghost ->
98
        ML.Pwild
99
    | Pvar vs ->
100
        ML.Pvar vs
101
    | Por (p1, p2) ->
102
        ML.Por (pat m p1, pat m p2)
103
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
104
        pat m p
105
    | Pas (p, vs) ->
106
        ML.Pas (pat m p, vs)
107
    | Papp (ls, pl) when is_fs_tuple ls ->
108
        let pl = visible_of_mask m pl in
109
        begin match pl with
110
          | [] -> ML.Pwild
111
          | [p] -> pat m p
112
          | _ -> ML.Ptuple (List.map (pat m) pl) end
113
    | Papp (ls, pl) ->
114 115 116 117
        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
118
        ML.Papp (ls, List.rev pat_pl)
119

Mário Pereira's avatar
Mário Pereira committed
120 121
  (** programs *)

122 123
  let pv_name pv = pv.pv_vs.vs_name

124
  (* individual types *)
Mário Pereira's avatar
Mário Pereira committed
125 126
  let mlty_of_ity mask t =
    let rec loop t = match t.ity_node with
127
      | _ when mask_equal mask MaskGhost -> ML.tunit
128
      | Ityvar tvs ->
129
          ML.Tvar tvs
130
      | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
131
          let itl = visible_of_mask mask itl in
132
          ML.Ttuple (List.map loop itl)
133
      | Ityapp ({its_ts = ts}, itl, _) ->
134
          ML.Tapp (ts.ts_name, List.map loop itl)
135 136
      | Ityreg {reg_its = its; reg_args = args} ->
          let args = List.map loop args in
137
          ML.Tapp (its.its_ts.ts_name, args) in
Mário Pereira's avatar
Mário Pereira committed
138
    loop t
Mário Pereira's avatar
Mário Pereira committed
139

Mário Pereira's avatar
Mário Pereira committed
140
  let pvty pv =
Mário Pereira's avatar
Mário Pereira committed
141
    if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true
Mário Pereira's avatar
Mário Pereira committed
142
    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
143

144
  let for_direction = function
145 146
    | To -> ML.To
    | DownTo -> ML.DownTo
147

148
  let isconstructor info rs = (* TODO *)
149
    match Mid.find_opt rs.rs_name info.ML.from_km with
Mário Pereira's avatar
Mário Pereira committed
150
    | Some {pd_node = PDtype its} ->
151 152 153
        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
154 155
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
156 157 158 159
  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
160
    let pv_equal_field rs = pv_equal (fd_of_rs rs) in
Mário Pereira's avatar
Mário Pereira committed
161 162 163 164
    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
165

166
  let get_record_itd info rs =
167
    match Mid.find_opt rs.rs_name info.ML.from_km with
Mário Pereira's avatar
Mário Pereira committed
168
    | Some {pd_node = PDtype itdl} ->
169 170 171 172 173
        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
174 175 176 177 178 179 180 181 182 183 184 185 186 187
    | _ -> 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
188

Mário Pereira's avatar
Mário Pereira committed
189
  let mk_eta_expansion rs pvl ({cty_args = ca; cty_effect = ce} as c) =
Mário Pereira's avatar
Mário Pereira committed
190
    (* FIXME : effects and types of the expression in this situation *)
191
    let mv = MaskVisible in
Mário Pereira's avatar
Mário Pereira committed
192
    let args_f =
Mário Pereira's avatar
Mário Pereira committed
193
      let def pv =
194
        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
195
      filter_ghost_params pv_not_ghost def ca in
Mário Pereira's avatar
Mário Pereira committed
196
    let args =
197
      let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) mv
198
        eff_empty Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
199
      let args = filter_ghost_params pv_not_ghost def pvl in
Mário Pereira's avatar
Mário Pereira committed
200
      let extra_args = List.map def ca in args @ extra_args in
201
    let eapp = ML.mk_expr (ML.Eapp (rs, args)) (ML.C c) mv
202
      ce Slab.empty in
203
    ML.mk_expr (ML.Efun (args_f, eapp)) (ML.C c) mv ce Slab.empty
Mário Pereira's avatar
Mário Pereira committed
204

205 206 207 208 209 210
  (* 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

211 212
  let params args = let args = filter_params args in
    if args = [] then [ML.mk_var_unit] else args
213

Mário Pereira's avatar
Mário Pereira committed
214 215
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
216
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
217
      | pv :: l1, arg :: l2 ->
Mário Pereira's avatar
Mário Pereira committed
218
          if p pv && p arg then def pv :: loop (l1, l2) else loop (l1, l2)
Mário Pereira's avatar
Mário Pereira committed
219 220 221
      | _ -> assert false
    in loop (pvl, cty_args)

222
  let app pvl cty_args f_zero =
223
    let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) MaskVisible
224 225 226
      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
227

228 229
  (* build the set of type variables from functions arguments *)
  let rec add_tvar acc = function
230 231
    | ML.Tvar tv -> Stv.add tv acc
    | ML.Tapp (_, tyl) | ML.Ttuple tyl ->
232
        List.fold_left add_tvar acc tyl
233

Mário Pereira's avatar
Mário Pereira committed
234
  (* expressions *)
235
  let rec expr info svar mask ({e_effect = eff; e_label = lbl} as e) =
236
    assert (not (e_ghost e));
237
    assert (not (mask_spill e.e_mask mask));
Mário Pereira's avatar
Mário Pereira committed
238 239 240 241 242 243 244 245
    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
246
    match e.e_node with
247 248 249 250
    | Econst _ | Evar _ when mask = MaskGhost ->
        ML.e_unit
    | Eexec ({c_node = Cfun _; c_cty = {cty_args}}, _)
      when cty_args <> [] && mask = MaskGhost ->
251
        ML.e_unit
252 253 254 255
    | Eexec ({c_node = Capp (rs, _)}, _)
      when isconstructor info rs && mask = MaskGhost ->
        ML.e_unit
    | Econst c -> Debug.dprintf debug_compile "compiling constant@.";
256
        let c = match c with Number.ConstInt c -> c | _ -> assert false in
257
        ML.mk_expr (ML.Econst c) (ML.I e.e_ity) mask eff lbl
258
    | Evar pv ->
259
        Debug.dprintf debug_compile "compiling variable %a@." print_pv pv;
260
        ML.mk_expr (ML.Evar pv) (ML.I e.e_ity) mask eff lbl
261 262
    | Elet (LDvar (_, e1), e2) when e_ghost e1 ->
        expr info svar mask e2
263
    | Elet (LDvar (_, e1), e2) when e_ghost e2 ->
264
        (* sequences are transformed into [let o = e1 in e2] by A-normal form *)
265
        expr info svar MaskGhost e1
Mário Pereira's avatar
Mário Pereira committed
266 267
    | Elet (LDvar (pv, e1), e2)
      when pv.pv_ghost || not (Mpv.mem pv e2.e_effect.eff_reads) ->
268
        if eff_pure e1.e_effect then expr info svar mask e2
269
        else let e1 = ML.e_ignore (expr info svar MaskGhost e1) in
270
          ML.e_seq e1 (expr info svar mask e2) (ML.I e.e_ity) mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
271
    | Elet (LDvar (pv, e1), e2) ->
272 273
        Debug.dprintf debug_compile "compiling local definition of %s@."
          (pv_name pv).id_string;
274
        let ld = ML.var_defn pv (expr info svar MaskVisible e1) in
275
        ML.e_let ld (expr info svar mask e2) (ML.I e.e_ity) mask eff lbl
276 277
    | Elet (LDsym (rs, _), ein) when rs_ghost rs ->
        expr info svar mask ein
278
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
279 280
        Debug.dprintf debug_compile "compiling local function definition %s@."
          rs.rs_name.id_string;
281 282
        let args = params cty.cty_args in
        let res = mlty_of_ity cty.cty_mask cty.cty_result in
283
        let ld = ML.sym_defn rs res args (expr info svar cty.cty_mask ef) in
284
        ML.e_let ld (expr info svar mask ein) (ML.I e.e_ity) mask eff lbl
285
    | Elet (LDsym (rs, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein)
286
      when isconstructor info rs_app -> (* partial application of constructor *)
287 288 289 290 291
        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
292
        let ein = expr info svar mask ein in
293
        ML.e_let ld ein (ML.I e.e_ity) mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
294
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
295
        (* partial application *) (* FIXME -> zero arguments functions *)
296 297
        Debug.dprintf debug_compile "compiling partial application of %s@."
          rsf.rs_name.id_string;
298 299 300
        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
301
        let eapp = ML.e_app rs_app pvl (ML.C cty) cmk ceff Slab.empty in
302 303
        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
304
        let ein = expr info svar mask ein in
305
        ML.e_let ld ein (ML.I e.e_ity) mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
306
    | Elet (LDrec rdefl, ein) ->
307 308
        let rdefl = filter_out_ghost_rdef rdefl in
        let def = function
309 310
          | { rec_sym = rs1; rec_rsym = rs2;
              rec_fun = {c_node = Cfun ef; c_cty = cty} } ->
311 312
              let res = mlty_of_ity rs1.rs_cty.cty_mask rs1.rs_cty.cty_result in
              let args = params cty.cty_args in
313
              let new_svar =
314 315 316
                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
317
              let new_svar = Stv.diff svar new_svar in
318
              let ef = expr info (Stv.union svar new_svar) ef.e_mask ef in
319 320 321
              { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
                ML.rec_args = args; ML.rec_exp  = ef;
                ML.rec_res  = res;  ML.rec_svar = new_svar; }
322 323 324
          | _ -> assert false in
        let rdefl = List.map def rdefl in
        if rdefl <> [] then
325
          let ein = expr info svar mask ein in
326 327
          let ml_letrec = ML.Elet (ML.Lrec rdefl, ein) in
          ML.mk_expr ml_letrec (ML.I e.e_ity) mask e.e_effect lbl
328 329 330 331 332
        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
333
        let res_ity = ity_tuple (List.map (fun v -> v.pv_ity) pvl) in
334
        let pvl = ML.var_list_of_pv_list pvl in
335
        ML.e_app rs pvl (ML.I res_ity) mask eff lbl
336
    | Eexec ({c_node = Capp (rs, _)}, _) when is_empty_record info rs ->
Mário Pereira's avatar
Mário Pereira committed
337
        ML.e_unit
Mário Pereira's avatar
Mário Pereira committed
338
    | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
Mário Pereira's avatar
Mário Pereira committed
339
      when isconstructor info rs && cty.cty_args <> [] ->
340 341
        (* partial application of constructors *)
        mk_eta_expansion rs pvl cty
342
    | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _) ->
343 344
        Debug.dprintf debug_compile "compiling total application of %s@."
          rs.rs_name.id_string;
345
        Debug.dprintf debug_compile "cty_args: %d@." (List.length cty.cty_args);
346
        let add_unit = function [] -> [ML.e_unit] | args -> args in
347
        let id_f = fun x -> x in
348 349 350
        let f_zero = match rs.rs_logic with RLnone ->
          Debug.dprintf debug_compile "it is a RLnone@."; add_unit
                                          | _ -> id_f in
351
        let pvl = app pvl rs.rs_cty.cty_args f_zero in
352 353
        begin match pvl with
          | [pv_expr] when is_optimizable_record_rs info rs -> pv_expr
354
          | _ -> ML.e_app rs pvl (ML.I e.e_ity) mask eff lbl end
Mário Pereira's avatar
Mário Pereira committed
355
    | Eexec ({c_node = Cfun e; c_cty = {cty_args = []}}, _) ->
356
        (* abstract block *)
357
        Debug.dprintf debug_compile "compiling abstract block@.";
358
        expr info svar mask e
359
    | Eexec ({c_node = Cfun ef; c_cty = cty}, _) ->
360 361
        (* is it the case that every argument here is non-ghost ? *)
        Debug.dprintf debug_compile "compiling a lambda expression@.";
362
        let ef = expr info svar e.e_mask ef in
363
        ML.e_fun (params cty.cty_args) ef (ML.I e.e_ity) mask eff lbl
364
    | Eexec ({c_node = Cany}, _) ->
365
        ML.mk_hole
366
    | Eabsurd ->
367
        ML.e_absurd (ML.I e.e_ity) mask eff lbl
368 369
    | Eassert _ ->
        ML.e_unit
370
    | Eif (e1, e2, e3) when e_ghost e1 ->
371 372
        (* if [e1] is ghost but the entire [if-then-else] expression doesn't,
           it must be the case one of the branches is [Eabsurd] *)
373 374
        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
375
    | Eif (e1, e2, e3) when e_ghost e3 ->
376 377
        let e1 = expr info svar e1.e_mask e1 in
        let e2 = expr info svar mask e2 in
378
        ML.e_if e1 e2 ML.e_unit mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
379
    | Eif (e1, e2, e3) when e_ghost e2 ->
380 381
        let e1 = expr info svar e1.e_mask e1 in
        let e3 = expr info svar mask e3 in
382
        ML.e_if e1 ML.e_unit e3 mask eff lbl
383
    | Eif (e1, e2, e3) -> Debug.dprintf debug_compile "compiling if block@.";
384 385 386
        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
387
        ML.e_if e1 e2 e3 mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
388
    | Ewhile (e1, _, _, e2) ->
389
        Debug.dprintf debug_compile "compiling while block@.";
390 391
        let e1 = expr info svar e1.e_mask e1 in
        let e2 = expr info svar e2.e_mask e2 in
392
        ML.e_while e1 e2 mask eff lbl
393
    | Efor (pv1, (pv2, dir, pv3), _, _, efor) ->
394
        Debug.dprintf debug_compile "compiling for block@.";
395
        let dir = for_direction dir in
396
        let efor = expr info svar efor.e_mask efor in
397
        ML.e_for pv1 pv2 dir pv3 efor mask eff lbl
398 399
    | Eghost _ | Epure _ ->
        assert false
400
    | Eassign al ->
401 402
        let rm_ghost (_, rs, _) = not (rs_ghost rs) in
        let al = List.filter rm_ghost al in
403
        ML.e_assign al (ML.I e.e_ity) mask eff lbl
404
    | Ematch (e1, [], xl) when Mxs.is_empty xl ->
405
        expr info svar e1.e_mask e1
406
    | Ematch (e1, bl, xl) when e_ghost e1 ->
407 408 409 410 411
        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)
412
    | Ematch (e1, bl, xl) ->
413 414
        let e1 = expr info svar e1.e_mask e1 in
        let bl = List.map (ebranch info svar mask) bl in
415 416
        let mk_xl (xs, (pvl, e)) = let pvl = pv_list_of_mask pvl xs.xs_mask in
          (xs, pvl, expr info svar mask e) in
417
        let xl = List.map mk_xl (Mxs.bindings xl) in
418
        ML.e_match e1 bl xl (ML.I e.e_ity) mask eff lbl
419
    | Eraise (xs, ex) -> let ex = match expr info svar xs.xs_mask ex with
420
        | {ML.e_node = ML.Eblock []} -> None
421
        | e -> Some e in
422
        ML.mk_expr (ML.Eraise (xs, ex)) (ML.I e.e_ity) mask eff lbl
423
    | Eexn (xs, e1) ->
424
        if mask_ghost e1.e_mask then ML.mk_expr
425
          (ML.Eexn (xs, None, ML.e_unit)) (ML.I e.e_ity) mask eff lbl
426 427 428
        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
429
        ML.mk_expr (ML.Eexn (xs, ty, e1)) (ML.I e.e_ity) mask eff lbl
Mário Pereira's avatar
Mário Pereira committed
430 431
    | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
    | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
432

433
  and ebranch info svar mask ({pp_pat = p; pp_mask = m}, e) =
Mário Pereira's avatar
Mário Pereira committed
434 435 436
    (* 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 *)
437
    if e.e_effect.eff_ghost then (pat m p, ML.e_unit)
438
    else (pat m p, expr info svar mask e)
439

440
  (* type declarations/definitions *)
Mário Pereira's avatar
Mário Pereira committed
441
  let tdef itd =
442
    let s = itd.itd_its in
443
    let ddata_constructs = (* point-free *)
Mário Pereira's avatar
Mário Pereira committed
444
      List.map (fun ({rs_cty = cty} as rs) ->
445 446
        let args = List.filter pv_not_ghost cty.cty_args in
        (rs.rs_name, List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)) in
Mário Pereira's avatar
Mário Pereira committed
447
    let drecord_fields ({rs_cty = cty} as rs) =
448
      (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields,
Mário Pereira's avatar
Mário Pereira committed
449
      rs.rs_name,
450
      mlty_of_ity cty.cty_mask cty.cty_result) in
451 452 453
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
454
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
455
      | NoDef, [], [] ->
456
          ML.mk_its_defn id args is_private None
457
      | NoDef, cl, [] ->
458
          let cl = ddata_constructs cl in
459
          ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
460
      | NoDef, _, pjl ->
461 462 463
          let p e = not (rs_ghost e) in
          let pjl = filter_ghost_params p drecord_fields pjl in
          begin match pjl with
464 465
            | [] ->
                ML.mk_its_defn id args is_private (Some (ML.Dalias ML.tunit))
466
            | [_, _, ty_pj] when is_optimizable_record_itd itd ->
467
                ML.mk_its_defn id args is_private (Some (ML.Dalias ty_pj))
468
            | pjl ->
469
                ML.mk_its_defn id args is_private (Some (ML.Drecord pjl)) end
470
      | Alias t, _, _ ->
471
          ML.mk_its_defn id args is_private (* FIXME ? is this a good mask ? *)
472
            (Some (ML.Dalias (mlty_of_ity MaskVisible t)))
473 474
      | Range r, [], [] ->
          assert (args = []); (* a range type is not polymorphic *)
475
          ML.mk_its_defn id [] is_private (Some (ML.Drange r))
476
      | Float ff, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
477
          assert (args = []); (* a float type is not polymorphic *)
478
          ML.mk_its_defn id [] is_private (Some (ML.Dfloat ff))
479 480
      | (Range _ | Float _), _, _ ->
          assert false (* cannot have constructors or fields *)
481
    end
Mário Pereira's avatar
Mário Pereira committed
482

Mário Pereira's avatar
Mário Pereira committed
483 484 485 486
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

487
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
488
    match pd.pd_node with
489 490 491
    | PDlet (LDvar (_, e)) when e_ghost e ->
        []
    | PDlet (LDvar (pv, e)) when pv.pv_ghost ->
492 493
        Debug.dprintf debug_compile "compiling top-level ghost symbol %a@."
          print_pv pv;
494
        if eff_pure e.e_effect then []
495 496
        else let unit_ = pv (* create_pvsymbol (id_fresh "_") ity_unit *) in
          [ML.Dlet (ML.Lvar (unit_, expr info Stv.empty MaskGhost e))]
497
    | PDlet (LDvar (pv, e)) ->
498 499
        Debug.dprintf debug_compile "compiling top-level symbol %a@."
          print_pv pv;
500
        [ML.Dlet (ML.Lvar (pv, expr info Stv.empty e.e_mask e))]
501
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
502
        []
Mário Pereira's avatar
Mário Pereira committed
503
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cany})) ->
504 505
        let args = params cty.cty_args in
        let res = mlty_of_ity cty.cty_mask cty.cty_result in
506
        [ML.Dlet (ML.Lany (rs, res, args))]
507 508 509
    | 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
510
        [ML.Dlet (ML.Lany (rs, res, []))]
511
    | PDlet (LDsym ({rs_cty = cty; rs_logic} as rs, {c_node = Cfun e; c_cty}))
512 513 514 515 516 517
      when c_cty.cty_args = [] ->
        Debug.dprintf debug_compile "compiling zero-arguments function %a@."
          Expr.print_rs rs;
        Debug.dprintf debug_compile "rs_cty_eff:%b@. c_cty_eff:%b@."
          (cty_pure cty) (cty_pure c_cty);
        Debug.dprintf debug_compile "e_eff:%b@." (eff_pure e.e_effect);
518 519 520
        let args = match rs_logic with RLnone ->
          Debug.dprintf debug_compile "rlnone ici@."; [ML.mk_var_unit]
                                     | _ -> [] in
521 522 523 524 525 526 527
        let res = mlty_of_ity cty.cty_mask 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
        let e = expr info svar cty.cty_mask e in
        [ML.Dlet (ML.Lsym (rs, res, args, e))]
528
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
529
        Debug.dprintf debug_compile "compiling function %a@." Expr.print_rs rs;
530 531
        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
532 533 534 535
        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
536
        let e = expr info svar cty.cty_mask e in
537
        [ML.Dlet (ML.Lsym (rs, res, args, e))]
538
    | PDlet (LDrec rl) ->
539 540 541 542 543 544 545 546 547
        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
548
          let e = expr info svar rs1.rs_cty.cty_mask e in
549 550 551 552
          { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
            ML.rec_args = args; ML.rec_exp  = e;
            ML.rec_res  = res;  ML.rec_svar = svar; } in
        if rl = [] then [] else [ML.Dlet (ML.Lrec (List.map def rl))]
553
    | PDlet (LDsym _) | PDpure ->
554
        []
555
    | PDtype itl ->
556
        let itsd = List.map tdef itl in
557
        [ML.Dtype itsd]
558
    | PDexn xs ->
559
        if ity_equal xs.xs_ity ity_unit || xs.xs_mask = MaskGhost then
560 561
          [ML.Dexn (xs, None)]
        else [ML.Dexn (xs, Some (mlty_of_ity xs.xs_mask xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
562

Mário Pereira's avatar
Mário Pereira committed
563
  let pdecl_m m pd =
564
    let info = { ML.from_mod = Some m; ML.from_km = m.mod_known; } in
565
    pdecl info pd
566

Mário Pereira's avatar
Mário Pereira committed
567
  (* unit module declarations *)
568 569
  let rec mdecl info = function
    | Udecl pd -> pdecl info pd
Mário Pereira's avatar
Mário Pereira committed
570
    | Uscope (_, ([Uuse _] | [Uclone _])) -> []
571
    | Uscope (s, dl) -> let dl = List.concat (List.map (mdecl info) dl) in
572
        [ML.Dmodule (s, dl)]
Mário Pereira's avatar
Mário Pereira committed
573
    | Uuse _ | Uclone _ | Umeta _ -> []
574

Mário Pereira's avatar
Mário Pereira committed
575
  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
576
  let module_ m =
577
    let from = { ML.from_mod = Some m; ML.from_km = m.mod_known; } in
578
    let mod_decl = List.concat (List.map (mdecl from) m.mod_units) in
579
    let add_decl known_map decl = let idl = ML.get_decl_name decl in
Mário Pereira's avatar
Mário Pereira committed
580
      List.fold_left (ML.add_known_decl decl) known_map idl in
581
    let mod_known = List.fold_left add_decl Mid.empty mod_decl in {
582 583 584
      ML.mod_from = from;
      ML.mod_decl = mod_decl;
      ML.mod_known = mod_known;
585 586
    }

Mário Pereira's avatar
Mário Pereira committed
587 588
end

589 590 591 592
(** Some transformations *)

module Transform = struct

593
  open Mltree
594

Mário Pereira's avatar
Mário Pereira committed
595
  let no_reads_writes_conflict spv spv_mreg =
596
    let is_not_write {pv_ity = ity} = match ity.ity_node with
597 598
      | Ityreg rho -> not (Mreg.mem rho spv_mreg)
      | _ -> true in
599
    Spv.for_all is_not_write spv
Mário Pereira's avatar
Mário Pereira committed
600

Mário Pereira's avatar
Mário Pereira committed
601 602 603 604 605
  let mk_list_eb ebl f =
    let mk_acc e (e_acc, s_acc) =
      let e, s = f e in e::e_acc, Spv.union s s_acc in
    List.fold_right mk_acc ebl ([], Spv.empty)

Mário Pereira's avatar
Mário Pereira committed
606
  let rec expr info subst e =
Mário Pereira's avatar
Mário Pereira committed
607
    let mk e_node = { e with e_node = e_node } in
Mário Pereira's avatar
Mário Pereira committed
608
    let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
609
    match e.e_node with
Mário Pereira's avatar
Mário Pereira committed
610 611
    | Evar pv -> begin try Mpv.find pv subst, Spv.singleton pv
        with Not_found -> e, Spv.empty end
Mário Pereira's avatar
Mário Pereira committed
612
    | Elet (Lvar (pv, ({e_effect = eff1} as e1)), ({e_effect = eff2} as e2))
Mário Pereira's avatar
Mário Pereira committed
613
      when Slab.mem Expr.proxy_label pv.pv_vs.vs_name.id_label &&
Mário Pereira's avatar
Mário Pereira committed
614
           eff_pure eff1 &&
Mário Pereira's avatar
Mário Pereira committed
615
           no_reads_writes_conflict eff1.eff_reads eff2.eff_writes ->
616 617 618 619 620 621
        let e1, s1 = expr info subst e1 in
        let e2, s2 = add_subst pv e1 e2 in
        let s_union = Spv.union s1 s2 in
        if Spv.mem pv s2 then e2, s_union (* [pv] was substituted in [e2] *)
        else (* [pv] was not substituted in [e2], e.g [e2] is an [Efun] *)
          mk (Elet (Lvar (pv, e1), e2)), s_union
622
    | Elet (ld, e) ->
623 624 625
        let e, spv = expr info subst e in
        let e_let, spv_let = let_def info subst ld in
        mk (Elet (e_let, e)), Spv.union spv spv_let
626
    | Eapp (rs, el) ->
627 628
        let e_app, spv = mk_list_eb el (expr info subst) in
        mk (Eapp (rs, e_app)), spv
629
    | Efun (vl, e) ->
630 631 632 633 634 635 636 637 638 639 640 641
        (* For now, we accept to inline constants and constructors
           with zero arguments inside a [Efun]. *)
        let p _k e = match e.e_node with
          | Econst _ -> true
          | Eapp (rs, []) when Translate.isconstructor info rs -> true
          | _ -> false in
        let restrict_subst = Mpv.filter p subst in
        (* We begin the inlining of proxy variables in an [Efun] with a
           restricted substitution. This keeps some proxy lets, preventing
           undiserable captures inside the [Efun] expression. *)
        let e, spv = expr info restrict_subst e in
        mk (Efun (vl, e)), spv
642
    | Eif (e1, e2, e3) ->
643 644 645 646
        let e1, s1 = expr info subst e1 in
        let e2, s2 = expr info subst e2 in
        let e3, s3 = expr info subst e3 in
        mk (Eif (e1, e2, e3)), Spv.union (Spv.union s1 s2) s3
647
    | Eexn (xs, ty, e1) ->
648 649
        let e1, s1 = expr info subst e1 in
        mk (Eexn (xs, ty, e1)), s1
650
    | Ematch (e, bl, xl) ->
651 652
        let e, spv = expr info subst e in
        let e_bl, spv_bl = mk_list_eb bl (branch info subst) in
653 654 655 656 657 658 659 660
        let e_xl, spv_xl = mk_list_eb xl (xbranch info subst) in
        mk (Ematch (e, e_bl, e_xl)), Spv.union (Spv.union spv spv_bl) spv_xl
(*
    | Etry (e, case, bl) ->
        let e, spv = expr info subst e in
        let e_bl, spv_bl = mk_list_eb bl (xbranch info subst) in
        mk (Etry (e, case, e_bl)), Spv.union spv spv_bl
*)
661
    | Eblock el ->
662 663
        let e_app, spv = mk_list_eb el (expr info subst) in
        mk (Eblock e_app), spv
664
    | Ewhile (e1, e2) ->
665 666 667
        let e1, s1 = expr info subst e1 in
        let e2, s2 = expr info subst e2 in
        mk (Ewhile (e1, e2)), Spv.union s1 s2
668
    | Efor (x, pv1, dir, pv2, e) ->
669
        let e, spv = expr info subst e in
670
        mk (Efor (x, pv1, dir, pv2, e)), spv
Mário Pereira's avatar
Mário Pereira committed
671 672
    | Eraise (exn, None) -> mk (Eraise (exn, None)), Spv.empty
    | Eraise (exn, Some e) ->
673 674
        let e, spv = expr info subst e in
        mk (Eraise (exn, Some e)), spv
Mário Pereira's avatar
Mário Pereira committed
675 676
    | Eassign _al ->
        e, Spv.empty
Mário Pereira's avatar
Mário Pereira committed
677 678
    | Econst _ | Eabsurd | Ehole -> e, Spv.empty
    | Eignore e ->
679 680
        let e, spv = expr info subst e in
        mk (Eignore e), spv
681

Mário Pereira's avatar
Mário Pereira committed
682 683 684 685
  and branch info subst (pat, e) =
    let e, spv = expr info subst e in (pat, e), spv
  and xbranch info subst (exn, pvl, e) =
    let e, spv = expr info subst e in (exn, pvl, e), spv
686

Mário Pereira's avatar
Mário Pereira committed
687
  and let_def info subst = function
688
    | Lvar (pv, e) ->
689 690 691
        assert (not (Mpv.mem pv subst)); (* no capture *)
        let e, spv = expr info subst e in
        Lvar (pv, e), spv
Mário Pereira's avatar
Mário Pereira committed
692
    | Lsym (rs, res, args, e) ->