compile.ml 30.1 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
  module ML = Mltree

52 53
  let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)

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

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

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

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

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

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

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

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

Mário Pereira's avatar
Mário Pereira committed
122 123
  (** programs *)

124 125
  let pv_name pv = pv.pv_vs.vs_name

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

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

146
  let for_direction = function
147 148
    | To -> ML.To
    | DownTo -> ML.DownTo
149

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

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

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

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

208 209 210 211 212 213
  (* 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

214 215
  let params args = let args = filter_params args in
    if args = [] then [ML.mk_var_unit] else args
216

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

225
  let app pvl cty_args f_zero =
226
    let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) MaskVisible
Andrei Paskevich's avatar
Andrei Paskevich committed
227
      eff_empty Sattr.empty in
228 229
    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
230

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

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

439
  and ebranch info svar mask ({pp_pat = p; pp_mask = m}, e) =
Mário Pereira's avatar
Mário Pereira committed
440 441 442
    (* 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 *)
443
    if e.e_effect.eff_ghost then (pat m p, ML.e_unit)
444
    else (pat m p, expr info svar mask e)
445

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

Mário Pereira's avatar
Mário Pereira committed
489 490 491 492
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

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

Mário Pereira's avatar
Mário Pereira committed
575
  let pdecl_m m pd =
576
    let info = { ML.from_mod = Some m; ML.from_km = m.mod_known; } in
577
    pdecl info pd
578

579
  (* unit module declarations *)
580 581
  let rec mdecl info = function
    | Udecl pd -> pdecl info pd
582
    | Uscope (_, ([Uuse _] | [Uclone _])) -> []
583
    | Uscope (s, dl) -> let dl = List.concat (List.map (mdecl info) dl) in
584
        [ML.Dmodule (s, dl)]
585
    | Uuse _ | Uclone _ | Umeta _ -> []
586

Mário Pereira's avatar
Mário Pereira committed
587
  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
588
  let module_ m =
589
    let from = { ML.from_mod = Some m; ML.from_km = m.mod_known; } in
590
    let mod_decl = List.concat (List.map (mdecl from) m.mod_units) in
591
    let add_decl known_map decl = let idl = ML.get_decl_name decl in
Mário Pereira's avatar
Mário Pereira committed
592
      List.fold_left (ML.add_known_decl decl) known_map idl in
593
    let mod_known = List.fold_left add_decl Mid.empty mod_decl in {
594 595 596
      ML.mod_from = from;
      ML.mod_decl = mod_decl;
      ML.mod_known = mod_known;
597 598
    }

Mário Pereira's avatar
Mário Pereira committed
599 600
end

601 602 603 604
(** Some transformations *)

module Transform = struct

605
  open Mltree
606

Mário Pereira's avatar
Mário Pereira committed
607
  let no_reads_writes_conflict spv spv_mreg =
608
    let is_not_write {pv_ity = ity} = match ity.ity_node with
609 610
      | Ityreg rho -> not (Mreg.mem rho spv_mreg)
      | _ -> true in
611
    Spv.for_all is_not_write spv
Mário Pereira's avatar
Mário Pereira committed
612

Mário Pereira's avatar
Mário Pereira committed
613 614 615 616 617
  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
618
  let rec expr info subst e =
Mário Pereira's avatar
Mário Pereira committed
619
    let mk e_node = { e with e_node = e_node } in
Mário Pereira's avatar
Mário Pereira committed
620
    let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
621
    match e.e_node with
Mário Pereira's avatar
Mário Pereira committed
622 623
    | 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
624
    | Elet (Lvar (pv, ({e_effect = eff1} as e1)), ({e_effect = eff2} as e2))
Andrei Paskevich's avatar
Andrei Paskevich committed
625
      when Sattr.mem Expr.proxy_attr pv.pv_vs.vs_name.id_attrs &&
Mário Pereira's avatar
Mário Pereira committed
626
           eff_pure eff1 &&
Mário Pereira's avatar
Mário Pereira committed
627
           no_reads_writes_conflict eff1.eff_reads eff2.eff_writes ->
628 629 630 631 632 633
        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
634
    | Elet (ld, e) ->
635 636 637
        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
638
    | Eapp (rs, el) ->
639 640
        let e_app, spv = mk_list_eb el (expr info subst) in
        mk (Eapp (rs, e_app)), spv
641
    | Efun (vl, e) ->
642 643 644 645 646 647 648 649 650 651 652 653
        (* 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
654
    | Eif (e1, e2, e3) ->
655 656 657 658
        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
659
    | Eexn (xs, ty, e1) ->
660 661
        let e1, s1 = expr info subst e1 in
        mk (Eexn (xs, ty, e1)), s1
662
    | Ematch (e, bl, xl) ->
663 664
        let e, spv = expr info subst e in
        let e_bl, spv_bl = mk_list_eb bl (branch info subst) in
665 666 667 668 669 670 671 672
        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
*)
673
    | Eblock el ->
674 675
        let e_app, spv = mk_list_eb el (expr info subst) in
        mk (Eblock e_app), spv
676
    | Ewhile (e1, e2) ->
677 678 679
        let e1, s1 = expr info subst e1 in
        let e2, s2 = expr info subst e2 in
        mk (Ewhile (e1, e2)), Spv.union s1 s2
680
    | Efor (x, pv1, dir, pv2, e) ->
681
        let e, spv = expr info subst e in
682
        mk (Efor (x, pv1, dir, pv2, e)), spv
Mário Pereira's avatar
Mário Pereira committed
683 684
    | Eraise (exn, None) -> mk (Eraise (exn, None)), Spv.empty
    | Eraise (exn, Some e) ->
685 686
        let e, spv = expr info subst e in
        mk (Eraise (exn, Some e)), spv
Mário Pereira's avatar
Mário Pereira committed
687 688
    | Eassign _al ->
        e, Spv.empty
689
    | Econst _ | Eabsurd | Ehole | Eany _ -> e, Spv.empty
Mário Pereira's avatar
Mário Pereira committed
690
    | Eignore e ->
691 692
        let e, spv = expr info subst e in
        mk (Eignore e), spv
693

Mário Pereira's avatar
Mário Pereira committed
694 695 696 697
  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
698

Mário Pereira's avatar
Mário Pereira committed
699
  and let_def info subst = function
700
    | Lvar (pv, e) ->
701 702 703
        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
704
    | Lsym (rs, res, args, e) ->
705 706
        let e, spv = expr info subst e in
        Lsym (rs, res, args, e), spv
707
    | Lany _ as lany -> lany, Mpv.empty
Mário Pereira's avatar
Mário Pereira committed
708
    | Lrec rl ->
709 710
        let rdef, spv = mk_list_eb rl (rdef info subst) in
        Lrec rdef, spv
711

Mário Pereira's avatar
Mário Pereira committed
712
  and rdef info subst r =
Mário Pereira's avatar
Mário Pereira committed
713 714
    let rec_exp, spv = expr info subst r.rec_exp in
    { r with rec_exp = rec_exp }, spv
715

716
  let rec pdecl info = function
717 718
    | Dtype _ | Dexn _ as d -> d
    | Dmodule (id, dl) ->
719
        let dl = List.map (pdecl info) dl in Dmodule (id, dl)
Mário Pereira's avatar
Mário Pereira committed
720
    | Dlet def ->
721 722
        (* for top-level symbols we can forget the set of inlined variables *)
        let e, _ = let_def info Mpv.empty def in Dlet e
723

724 725
  let module_ m =
    let mod_decl = List.map (pdecl m.mod_from) m.mod_decl in
Mário Pereira's avatar
Mário Pereira committed
726
    let add known_map decl =
727 728
      let idl = Mltree.get_decl_name decl in
      List.fold_left (Mltree.add_known_decl decl) known_map idl in
Mário Pereira's avatar
Mário Pereira committed
729
    let mod_known = List.fold_left add Mid.empty mod_decl in
730
    { m with mod_decl = mod_decl; mod_known = mod_known }
731 732

end