compile.ml 31.4 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
Mário Pereira's avatar
Mário Pereira committed
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

MARCHE Claude's avatar
MARCHE Claude committed
237 238 239 240 241 242 243
  let new_svar args res svar =
    let new_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
    Stv.diff new_svar svar

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

461
  and ebranch info svar mask ({pp_pat = p; pp_mask = m}, e) =
Mário Pereira's avatar
Mário Pereira committed
462 463 464
    (* 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 *)
465
    if e.e_effect.eff_ghost then (pat m p, ML.e_unit)
466
    else (pat m p, expr info svar mask e)
467

468
  (* type declarations/definitions *)
Mário Pereira's avatar
Mário Pereira committed
469
  let tdef itd =
470
    let s = itd.itd_its in
471
    let ddata_constructs = (* point-free *)
Mário Pereira's avatar
Mário Pereira committed
472
      List.map (fun ({rs_cty = cty} as rs) ->
473 474
        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
475
    let drecord_fields ({rs_cty = cty} as rs) =
476
      (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields,
Mário Pereira's avatar
Mário Pereira committed
477
      rs.rs_name,
478
      mlty_of_ity cty.cty_mask cty.cty_result) in
479 480 481
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
482
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
483
      | NoDef, [], [] ->
484
          ML.mk_its_defn id args is_private None
485
      | NoDef, cl, [] ->
486
          let cl = ddata_constructs cl in
487
          ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
488
      | NoDef, _, pjl ->
489 490 491
          let p e = not (rs_ghost e) in
          let pjl = filter_ghost_params p drecord_fields pjl in
          begin match pjl with
492 493
            | [] ->
                ML.mk_its_defn id args is_private (Some (ML.Dalias ML.tunit))
494
            | [_, _, ty_pj] when is_optimizable_record_itd itd ->
495
                ML.mk_its_defn id args is_private (Some (ML.Dalias ty_pj))
496
            | pjl ->
497
                ML.mk_its_defn id args is_private (Some (ML.Drecord pjl)) end
498
      | Alias t, _, _ ->
499
          ML.mk_its_defn id args is_private (* FIXME ? is this a good mask ? *)
500
            (Some (ML.Dalias (mlty_of_ity MaskVisible t)))
501 502
      | Range r, [], [] ->
          assert (args = []); (* a range type is not polymorphic *)
503
          ML.mk_its_defn id [] is_private (Some (ML.Drange r))
504
      | Float ff, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
505
          assert (args = []); (* a float type is not polymorphic *)
506
          ML.mk_its_defn id [] is_private (Some (ML.Dfloat ff))
507 508
      | (Range _ | Float _), _, _ ->
          assert false (* cannot have constructors or fields *)
509
    end
Mário Pereira's avatar
Mário Pereira committed
510

Mário Pereira's avatar
Mário Pereira committed
511 512 513 514
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

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

Mário Pereira's avatar
Mário Pereira committed
594
  let pdecl_m m pd =
595
    let info = { ML.from_mod = Some m; ML.from_km = m.mod_known; } in
596
    pdecl info pd
597

Mário Pereira's avatar
Mário Pereira committed
598
  (* unit module declarations *)
599 600
  let rec mdecl info = function
    | Udecl pd -> pdecl info pd
Mário Pereira's avatar
Mário Pereira committed
601
    | Uscope (_, ([Uuse _] | [Uclone _])) -> []
602
    | Uscope (s, dl) -> let dl = List.concat (List.map (mdecl info) dl) in
603
        [ML.Dmodule (s, dl)]
Mário Pereira's avatar
Mário Pereira committed
604
    | Uuse _ | Uclone _ | Umeta _ -> []
605

Mário Pereira's avatar
Mário Pereira committed
606
  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
607
  let module_ m =
608
    let from = { ML.from_mod = Some m; ML.from_km = m.mod_known; } in
609
    let mod_decl = List.concat (List.map (mdecl from) m.mod_units) in
610
    let add_decl known_map decl = let idl = ML.get_decl_name decl in
Mário Pereira's avatar
Mário Pereira committed
611
      List.fold_left (ML.add_known_decl decl) known_map idl in
612
    let mod_known = List.fold_left add_decl Mid.empty mod_decl in {
613 614 615
      ML.mod_from = from;
      ML.mod_decl = mod_decl;
      ML.mod_known = mod_known;
616 617
    }

Mário Pereira's avatar
Mário Pereira committed
618 619
end

620 621 622 623
(** Some transformations *)

module Transform = struct

624
  open Mltree
625

626 627 628
  let no_effect_conflict spv eff =
    Spv.is_empty (pvs_affected eff.eff_writes spv) &&
    Spv.is_empty (pvs_affected eff.eff_resets spv)
Mário Pereira's avatar
Mário Pereira committed
629

630 631
  let rec can_inline ({e_effect = eff1} as e1) ({e_effect = eff2} as e2) =
    match e2.e_node with
632
    | Evar _ | Econst _ | Eapp _ | Eassign [_] -> true
633
    | Elet (Lvar (_, {e_effect = eff1'}), e2') ->
634
       no_effect_conflict eff1.eff_reads eff1'
635
       && can_inline e1 e2'
636
    | _ -> no_effect_conflict eff1.eff_reads eff2
637

Mário Pereira's avatar
Mário Pereira committed
638 639 640 641 642
  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
643
  let rec expr info subst e =
Mário Pereira's avatar
Mário Pereira committed
644
    let mk e_node = { e with e_node = e_node } in
Mário Pereira's avatar
Mário Pereira committed
645
    let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
646
    match e.e_node with
Mário Pereira's avatar
Mário Pereira committed
647 648
    | Evar pv -> begin try Mpv.find pv subst, Spv.singleton pv
        with Not_found -> e, Spv.empty end
649
    | Elet (Lvar (pv, ({e_effect = eff1} as e1)), e2)
DAILLER Sylvain's avatar
DAILLER Sylvain committed
650
      when Sattr.mem proxy_attr pv.pv_vs.vs_name.id_attrs &&
Mário Pereira's avatar
Mário Pereira committed
651
           eff_pure eff1 &&
652
           can_inline e1 e2 ->
653 654 655 656 657 658
        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
659
    | Elet (ld, e) ->
660 661 662
        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
663
    | Eapp (rs, el) ->
664 665
        let e_app, spv = mk_list_eb el (expr info subst) in
        mk (Eapp (rs, e_app)), spv
666
    | Efun (vl, e) ->
667 668 669 670 671 672 673 674 675 676 677 678
        (* 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
679
    | Eif (e1, e2, e3) ->
680 681 682 683
        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
684
    | Eexn (xs, ty, e1) ->
685 686
        let e1, s1 = expr info subst e1 in
        mk (Eexn (xs, ty, e1)), s1
687
    | Ematch (e, bl, xl) ->
688 689
        let e, spv = expr info subst e in
        let e_bl, spv_bl = mk_list_eb bl (branch info subst) in
690 691 692 693 694 695 696 697
        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
*)
698
    | Eblock el ->
699 700
        let e_app, spv = mk_list_eb el (expr info subst) in
        mk (Eblock e_app), spv
701
    | Ewhile (e1, e2) ->
702 703 704
        let e1, s1 = expr info subst e1 in
        let e2, s2 = expr info subst e2 in
        mk (Ewhile (e1, e2)), Spv.union s1 s2
705
    | Efor (x, pv1, dir, pv2, e) ->
706
        let e, spv = expr info subst e in
707
        mk (Efor (x, pv1, dir, pv2, e)), spv
Mário Pereira's avatar
Mário Pereira committed
708 709
    | Eraise (exn, None) -> mk (Eraise (exn, None)), Spv.empty
    | Eraise (exn, Some e) ->
710 711
        let e, spv = expr info subst e in
        mk (Eraise (exn, Some e)), spv
712 713 714 715 716 717 718 719
    | Eassign al ->
       let al, s =
         List.fold_left
           (fun (accl, spv) (pv,rs,e) ->
             let e, s = expr info subst e in
             ((pv, rs, e)::accl, Spv.union spv s))
           ([], Spv.empty) al in
       mk (Eassign (List.rev al)), s
720
    | Econst _ | Eabsurd -> e, Spv.empty
Mário Pereira's avatar
Mário Pereira committed
721
    | Eignore e ->
722 723
        let e, spv = expr info subst e in
        mk (Eignore e), spv
724

Mário Pereira's avatar
Mário Pereira committed
725 726 727 728
  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
729

Mário Pereira's avatar
Mário Pereira committed
730
  and let_def info subst = function
731
    | Lvar (pv, e) ->
732 733 734
        assert (not (Mpv.mem pv subst)); (* no capture *)
        let e, spv = expr info subst e in
        Lvar (pv, e), spv
MARCHE Claude's avatar
MARCHE Claude committed
735
    | Lsym (rs, svar, res, args, e) ->
736
        let e, spv = expr info subst e in
MARCHE Claude's avatar
MARCHE Claude committed
737
        Lsym (rs, svar, res, args, e), spv
Mário Pereira's avatar
Mário Pereira committed
738
    | Lany _ as lany -> lany, Mpv.empty
Mário Pereira's avatar
Mário Pereira committed
739
    | Lrec rl ->
740 741
        let rdef, spv = mk_list_eb rl (rdef info subst) in
        Lrec rdef, spv
742

Mário Pereira's avatar
Mário Pereira committed
743
  and rdef info subst r =
Mário Pereira's avatar
Mário Pereira committed
744 745
    let rec_exp, spv = expr info subst r.rec_exp in
    { r with rec_exp = rec_exp }, spv
746

747
  let rec pdecl info = function
748
    | Dtype _ | Dexn _ | Dval _ as d -> d
749
    | Dmodule (id, dl) ->
750
        let dl = List.map (pdecl info) dl in Dmodule (id, dl)
Mário Pereira's avatar
Mário Pereira committed
751
    | Dlet def ->
752 753
        (* for top-level symbols we can forget the set of inlined variables *)
        let e, _ = let_def info Mpv.empty def in Dlet e
754

755 756
  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
757
    let add known_map decl =
758 759
      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
760
    let mod_known = List.fold_left add Mid.empty mod_decl in
761
    { m with mod_decl = mod_decl; mod_known = mod_known }
762 763

end