compile.ml 32 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Mário Pereira's avatar
Mário Pereira committed
4
(*  Copyright 2010-2017   --   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 25 26
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

(*
  - extract file f.mlw into OCaml file f.ml, with sub-modules

  - "use (im|ex)port" -> "open"
    but OCaml's open is not transitive, so requires some extra work
    to figure out all the opens

  - if a WhyML module M is extracted to something that is a signature,
    then extract "module type B_sig = ..." (as well as "module B = ...")
*)

(** Abstract syntax of ML *)

open Ident
open Ity
Mário Pereira's avatar
Mário Pereira committed
27
open Ty
Mário Pereira's avatar
Mário Pereira committed
28
open Term
29

Mário Pereira's avatar
Mário Pereira committed
30 31 32 33 34 35 36 37
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
38
  let fname = match fname, path with
Mário Pereira's avatar
Mário Pereira committed
39 40 41 42 43
    | None, "why3"::_ -> "why3"
    | None, _   -> String.concat "__" path
    | Some f, _ -> clean_name f in
  fname ^ "__" ^ t

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

Mário Pereira's avatar
Mário Pereira committed
48 49 50
  let get_decl_name = function
    | Dtype itdefl -> List.map (fun {its_name = id} -> id) itdefl
    | Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
51 52 53
    | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
    | Dlet (Lsym ({rs_name=id}, _, _, _))
    | Dexn ({xs_name=id}, _) -> [id]
54
    | Dclone _ -> [] (* FIXME? *)
Mário Pereira's avatar
Mário Pereira committed
55 56

  let add_known_decl decl k_map id =
Mário Pereira's avatar
Mário Pereira committed
57 58
    Mid.add id decl k_map

Mário Pereira's avatar
Mário Pereira committed
59 60
  let rec iter_deps_ty f = function
    | Tvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
61
    | Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
Mário Pereira's avatar
Mário Pereira committed
62 63 64
    | Ttuple ty_l -> List.iter (iter_deps_ty f) ty_l

  let iter_deps_typedef f = function
Mário Pereira's avatar
Mário Pereira committed
65 66
    | Ddata constrl ->
      List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
Mário Pereira's avatar
Mário Pereira committed
67
    | Drecord pjl -> List.iter (fun (_, _, ty) -> iter_deps_ty f ty) pjl
Mário Pereira's avatar
Mário Pereira committed
68 69 70 71 72
    | Dalias ty -> iter_deps_ty f ty

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

Mário Pereira's avatar
Mário Pereira committed
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
  let iter_deps_args f =
    List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg)

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

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

  and iter_deps_pat f = function
    | Pwild | Pident _ -> ()
    | Papp (ls, patl) ->
      f ls.ls_name;
      iter_deps_pat_list f patl
    | Ptuple patl -> iter_deps_pat_list f patl
    | Por (p1, p2) ->
      iter_deps_pat f p1;
      iter_deps_pat f p2
    | Pas (p, _) -> iter_deps_pat f p

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

146
  let rec iter_deps f = function
Mário Pereira's avatar
Mário Pereira committed
147 148
    | Dtype its_dl ->
      List.iter (iter_deps_its_defn f) its_dl
Mário Pereira's avatar
Mário Pereira committed
149 150 151 152 153 154 155 156 157
    | Dlet (Lsym (_rs, ty_result, args, e)) ->
      iter_deps_ty f ty_result;
      iter_deps_args f args;
      iter_deps_expr f e
    | Dlet (Lrec rdef) ->
      List.iter
        (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
           f rs.rs_name; iter_deps_args f args;
           iter_deps_expr f e; iter_deps_ty f res) rdef
Mário Pereira's avatar
Mário Pereira committed
158 159 160
    | Dlet (Lvar (_, e)) -> iter_deps_expr f e
    | Dexn (_, None) -> ()
    | Dexn (_, Some ty) -> iter_deps_ty f ty
161
    | Dclone (_, dl) -> List.iter (iter_deps f) dl
162

163
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
164 165
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

166
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
167
  let mk_let_var pv e1 e2 =
Mário Pereira's avatar
Mário Pereira committed
168
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
169 170

  let tunit = Ttuple []
171

Mário Pereira's avatar
Mário Pereira committed
172 173 174 175 176 177
  let ity_int  = I Ity.ity_int
  let ity_unit = I Ity.ity_unit

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

179 180 181 182 183
  let enope = Eblock []

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

Mário Pereira's avatar
Mário Pereira committed
184 185 186
  let mk_hole =
    mk_expr Ehole (I Ity.ity_unit) Ity.eff_empty

187 188
  let mk_var id ty ghost = (id, ty, ghost)

189 190
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

191
  let mk_its_defn id args private_ def =
Mário Pereira's avatar
Mário Pereira committed
192 193
    { its_name    = id      ; its_args = args;
      its_private = private_; its_def  = def; }
194

Mário Pereira's avatar
Mário Pereira committed
195 196 197 198
  let mk_ignore e =
    if is_unit e.e_ity then e
    else { e_node = Eignore e; e_effect = e.e_effect; e_ity = ity_unit }

199 200
  let eseq e1 e2 =
    match e1.e_node, e2.e_node with
Mário Pereira's avatar
Mário Pereira committed
201
    | (Eblock [] | Ehole), e | e, (Eblock [] | Ehole) -> e
202 203 204 205 206
    | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
    | _, Eblock e2 -> Eblock (e1 :: e2)
    | Eblock e1, _ -> Eblock (e1 @ [e2])
    | _ -> Eblock [e1; e2]

207
end
Mário Pereira's avatar
Mário Pereira committed
208 209 210 211 212

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
213 214 215
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
216

Mário Pereira's avatar
Mário Pereira committed
217 218 219
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
220 221 222 223
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
224
       Mltree.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
225
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
226
       Mltree.Ttuple (List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
227
    | Tyapp (ts, tyl) ->
228
       Mltree.Tapp (ts.ts_name, List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
229 230 231 232

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

Mário Pereira's avatar
Mário Pereira committed
233 234 235 236 237
  let rec filter_ghost_params p def = function
    | [] -> []
    | pv :: l ->
      if p pv then def pv :: (filter_ghost_params p def l)
      else filter_ghost_params p def l
238

239
  let rec filter_out_ghost_rdef = function
Mário Pereira's avatar
Mário Pereira committed
240 241
    | [] -> []
    | { rec_sym = rs; rec_rsym = rrs } :: l
242 243
      when rs_ghost rs || rs_ghost rrs -> filter_out_ghost_rdef l
    | rdef :: l -> rdef :: filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
244

245 246 247
  let rec pat p =
    match p.pat_node with
    | Pwild ->
248
      Mltree.Pwild
249
    | Pvar vs when (restore_pv vs).pv_ghost ->
250
      Mltree.Pwild
251
    | Pvar vs ->
252
      Mltree.Pident vs.vs_name
253
    | Por (p1, p2) ->
254
      Mltree.Por (pat p1, pat p2)
255 256
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
      pat p
257
    | Pas (p, vs) ->
258
      Mltree.Pas (pat p, vs.vs_name)
259
    | Papp (ls, pl) when is_fs_tuple ls ->
260
      Mltree.Ptuple (List.map pat pl)
261
    | Papp (ls, pl) ->
262 263
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
264 265
      let mk acc pv pp = if not pv.pv_ghost then pat pp :: acc else acc in
      let pat_pl = List.fold_left2 mk [] args pl in
266
      Mltree.Papp (ls, List.rev pat_pl)
267

Mário Pereira's avatar
Mário Pereira committed
268 269
  (** programs *)

270 271
  let pv_name pv = pv.pv_vs.vs_name

272 273 274
  (* individual types *)
  let rec ity t =
    match t.ity_node with
275
    | Ityvar (tvs, _) ->
276
      Mltree.Tvar tvs
277
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
278
      Mltree.Ttuple (List.map ity itl)
279
    | Ityapp ({its_ts = ts}, itl, _) ->
280
      Mltree.Tapp (ts.ts_name, List.map ity itl)
281 282
    | Ityreg {reg_its = its; reg_args = args} ->
      let args = List.map ity args in
283
      Mltree.Tapp (its.its_ts.ts_name, args)
Mário Pereira's avatar
Mário Pereira committed
284

Mário Pereira's avatar
Mário Pereira committed
285
  let pvty pv =
Mário Pereira's avatar
Mário Pereira committed
286 287
    if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true
    else let (vs, vs_ty) = vsty pv.pv_vs in
288
      ML.mk_var vs vs_ty false
Mário Pereira's avatar
Mário Pereira committed
289

290 291 292
  (* let for_direction = function *)
  (*   | To -> Mltree.To *)
  (*   | DownTo -> Mltree.DownTo *)
293

Mário Pereira's avatar
Mário Pereira committed
294
  let isconstructor info rs =
295
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
296 297 298 299 300 301
    | Some {pd_node = PDtype its} ->
      let is_constructor its =
        List.exists (rs_equal rs) its.itd_constructors in
      List.exists is_constructor its
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
302 303 304 305
  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
306
    let pv_equal_field rs = pv_equal (fd_of_rs rs) in
Mário Pereira's avatar
Mário Pereira committed
307 308 309 310
    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
311

312
  let get_record_itd info rs =
313
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
314 315
    | Some {pd_node = PDtype itdl} ->
      let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
316
      let itd = match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
317
        | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333
        | None -> List.find (fun itd -> f itd.itd_constructors) itdl in
      if itd.itd_fields = [] then None else Some itd
    | _ -> 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
334

Mário Pereira's avatar
Mário Pereira committed
335
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
336 337 338 339 340
    (* FIXME : effects and types of the expression in this situation *)
    let args_f =
      let def pv = pv_name pv, ity pv.pv_ity, pv.pv_ghost in
      filter_ghost_params pv_not_ghost def cty_app.cty_args in
    let args =
341
      let def pv = ML.mk_expr (Mltree.Evar pv) (Mltree.I pv.pv_ity) eff_empty in
Mário Pereira's avatar
Mário Pereira committed
342 343 344 345 346
      let args = filter_ghost_params pv_not_ghost def pvl in
      let extra_args =
        (* FIXME : ghost status in this extra arguments *)
        List.map def cty_app.cty_args in
      args @ extra_args in
347
    let eapp = ML.mk_expr (Mltree.Eapp (rsc, args)) (Mltree.C cty_app)
348 349 350
        cty_app.cty_effect in
    ML.mk_expr (Mltree.Efun (args_f, eapp)) (Mltree.C cty_app)
      cty_app.cty_effect
Mário Pereira's avatar
Mário Pereira committed
351

352 353 354 355 356 357
  (* 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

Mário Pereira's avatar
Mário Pereira committed
358 359 360 361
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
      if args = [] then [ML.mk_var_unit ()] else args
362

Mário Pereira's avatar
Mário Pereira committed
363 364
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
365
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
366 367 368 369 370 371 372
      | pv :: l1, arg :: l2 ->
        if p pv && p arg then def pv :: loop (l1, l2)
        else loop (l1, l2)
      | _ -> assert false
    in loop (pvl, cty_args)

  let app pvl cty_args =
373
    let def pv = ML.mk_expr (Mltree.Evar pv) (Mltree.I pv.pv_ity) eff_empty in
Mário Pereira's avatar
Mário Pereira committed
374 375
    filter_params_cty pv_not_ghost def pvl cty_args

Mário Pereira's avatar
Mário Pereira committed
376
  let mk_for op_b_rs op_a_rs i_pv from_pv to_pv body_expr eff =
Mário Pereira's avatar
Mário Pereira committed
377 378
    let i_expr, from_expr, to_expr =
      let int_ity = ML.ity_int in let eff_e = eff_empty in
379 380 381
      ML.mk_expr (Mltree.Evar i_pv)    int_ity eff_e,
      ML.mk_expr (Mltree.Evar from_pv) int_ity eff_e,
      ML.mk_expr (Mltree.Evar to_pv)   int_ity eff_e in
Mário Pereira's avatar
Mário Pereira committed
382
    let for_rs    =
Mário Pereira's avatar
Mário Pereira committed
383
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
384
      let for_cty = create_cty [i_pv] [] [] Mxs.empty
Mário Pereira's avatar
Mário Pereira committed
385
                               Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
386 387
      create_rsymbol for_id for_cty in
    let for_expr =
388 389
      let test = ML.mk_expr (Mltree.Eapp (op_b_rs, [i_expr; to_expr]))
                            (Mltree.I ity_bool) eff_empty in
Mário Pereira's avatar
Mário Pereira committed
390
      let next_expr =
391
        let one_const = Number.int_const_of_int 1 in
Mário Pereira's avatar
Mário Pereira committed
392
        let one_expr  =
393 394
          ML.mk_expr (Mltree.Econst one_const) ML.ity_int eff_empty in
        let i_op_one = Mltree.Eapp (op_a_rs, [i_expr; one_expr]) in
Mário Pereira's avatar
Mário Pereira committed
395
        ML.mk_expr i_op_one ML.ity_int eff_empty in
Mário Pereira's avatar
Mário Pereira committed
396
       let rec_call  =
397
        ML.mk_expr (Mltree.Eapp (for_rs, [next_expr]))
Mário Pereira's avatar
Mário Pereira committed
398
                    ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
399
      let seq_expr =
Mário Pereira's avatar
Mário Pereira committed
400
        ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff in
401
      ML.mk_expr (Mltree.Eif (test, seq_expr, ML.mk_unit)) ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
402
    let ty_int = ity ity_int in
Mário Pereira's avatar
Mário Pereira committed
403
    let for_call_expr   =
404
      let for_call      = Mltree.Eapp (for_rs, [from_expr]) in
Mário Pereira's avatar
Mário Pereira committed
405 406
      ML.mk_expr for_call ML.ity_unit eff in
    let pv_name pv = pv.pv_vs.vs_name in
407
    let args = [ pv_name i_pv, ty_int, false ] in
Mário Pereira's avatar
Mário Pereira committed
408
    let for_rec_def = {
409 410 411
      Mltree.rec_sym  = for_rs;   Mltree.rec_args = args;
      Mltree.rec_rsym = for_rs;   Mltree.rec_exp  = for_expr;
      Mltree.rec_res  = ML.tunit; Mltree.rec_svar = Stv.empty;
Mário Pereira's avatar
Mário Pereira committed
412
    } in
413
    let for_let = Mltree.Elet (Mltree.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
414 415 416 417
    ML.mk_expr for_let ML.ity_unit eff

  let mk_for_downto info i_pv from_pv to_pv body eff =
    let ge_rs, minus_rs =
418
      let ns = (Opt.get info.Mltree.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
419 420 421 422 423
      ns_find_rs ns ["Int"; "infix >="], ns_find_rs ns ["Int"; "infix -"] in
    mk_for ge_rs minus_rs i_pv from_pv to_pv body eff

  let mk_for_to info i_pv from_pv to_pv body eff =
    let le_rs, plus_rs =
424
      let ns = (Opt.get info.Mltree.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
425 426 427
      ns_find_rs ns ["Int"; "infix <="], ns_find_rs ns ["Int"; "infix +"] in
    mk_for le_rs plus_rs i_pv from_pv to_pv body eff

428
  (* exception ExtractionAny *)
Mário Pereira's avatar
Mário Pereira committed
429

430 431
  (* build the set of type variables from functions arguments *)
  let rec add_tvar acc = function
432 433
    | Mltree.Tvar tv -> Stv.add tv acc
    | Mltree.Tapp (_, tyl) | Mltree.Ttuple tyl ->
434 435
      List.fold_left add_tvar acc tyl

Mário Pereira's avatar
Mário Pereira committed
436
  (* expressions *)
437
  let rec expr info ({e_effect = eff} as e) =
Mário Pereira's avatar
Mário Pereira committed
438
    assert (not eff.eff_ghost);
Mário Pereira's avatar
Mário Pereira committed
439
    match e.e_node with
440
    | Econst c ->
441 442
      let c = match c with
          Number.ConstInt c -> c | _ -> assert false in
443
      ML.mk_expr (Mltree.Econst c) (Mltree.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
444
    | Evar pv ->
445
      ML.mk_expr (Mltree.Evar pv) (Mltree.I e.e_ity) eff
446
    | Elet (LDvar (_, e1), e2) when e_ghost e1 ->
Mário Pereira's avatar
Mário Pereira committed
447
      expr info e2
448 449
    | Elet (LDvar (_, e1), e2) when e_ghost e2 ->
      ML.mk_expr (ML.eseq (expr info e1) ML.mk_unit) ML.ity_unit eff
Mário Pereira's avatar
Mário Pereira committed
450 451 452 453
    | Elet (LDvar (pv, e1), e2)
      when pv.pv_ghost || not (Mpv.mem pv e2.e_effect.eff_reads) ->
      if eff_pure e1.e_effect then expr info e2
      else let e1 = ML.mk_ignore (expr info e1) in
454
        ML.mk_expr (ML.eseq e1 (expr info e2)) (Mltree.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
455 456
    | Elet (LDvar (pv, e1), e2) ->
      let ml_let = ML.mk_let_var pv (expr info e1) (expr info e2) in
457
      ML.mk_expr ml_let (Mltree.I e.e_ity) eff
458 459
    | Elet (LDsym (rs, _), ein) when rs_ghost rs ->
      expr info ein
460
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
461
      let args = params cty.cty_args in
462 463
      let ef = expr info ef in
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
464
      let res = ity cty.cty_result in
465 466
      let ml_letrec = Mltree.Elet (Mltree.Lsym (rs, res, args, ef), ein) in
      ML.mk_expr ml_letrec (Mltree.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
467 468
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein)
      when isconstructor info rs_app ->
Mário Pereira's avatar
Mário Pereira committed
469 470
      (* partial application of constructor *)
      let eta_app = mk_eta_expansion rs_app pvl cty in
Mário Pereira's avatar
Mário Pereira committed
471
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
472 473 474
      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 = ity func in
475 476
      let ml_letrec = Mltree.Elet (Mltree.Lsym (rsf, res, [], eta_app), ein) in
      ML.mk_expr ml_letrec (Mltree.I e.e_ity) e.e_effect
Mário Pereira's avatar
Mário Pereira committed
477
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
478
      (* partial application *)
Mário Pereira's avatar
Mário Pereira committed
479
      let pvl = app pvl rs_app.rs_cty.cty_args in
480
      let eapp =
481
        ML.mk_expr (Mltree.Eapp (rs_app, pvl)) (Mltree.C cty) cty.cty_effect in
Mário Pereira's avatar
Mário Pereira committed
482 483
      let ein  = expr info ein in
      let res  = ity cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
484
      let args = params cty.cty_args in
485 486
      let ml_letrec = Mltree.Elet (Mltree.Lsym (rsf, res, args, eapp), ein) in
      ML.mk_expr ml_letrec (Mltree.I e.e_ity) e.e_effect
Mário Pereira's avatar
Mário Pereira committed
487
    | Elet (LDrec rdefl, ein) ->
488 489 490 491
      let rdefl = filter_out_ghost_rdef rdefl in
      let def = function
        | {rec_sym = rs1; rec_rsym = rs2;
           rec_fun = {c_node = Cfun ef; c_cty = cty}} ->
492 493 494 495
          let res  = ity rs1.rs_cty.cty_result in
          let args = params cty.cty_args in
          let svar =
            let args' = List.map (fun (_, ty, _) -> ty) args in
496
            let svar  = List.fold_left add_tvar Stv.empty args' in
497 498
            add_tvar svar res in
          let ef = expr info ef in
499 500 501
          { Mltree.rec_sym  = rs1;  Mltree.rec_rsym = rs2;
            Mltree.rec_args = args; Mltree.rec_exp  = ef ;
            Mltree.rec_res  = res;  Mltree.rec_svar = svar; }
502 503
        | _ -> assert false in
      let rdefl = List.map def rdefl in
504
      if rdefl <> [] then
505 506
        let ml_letrec = Mltree.Elet (Mltree.Lrec rdefl, expr info ein) in
        ML.mk_expr ml_letrec (Mltree.I e.e_ity) e.e_effect
507
      else expr info ein
508 509
    | Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs ->
      ML.mk_unit
510 511
    | Eexec ({c_node = Capp (rs, _)}, _) when is_empty_record info rs ->
      ML.mk_unit
512 513
    | Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
      ML.mk_unit
Mário Pereira's avatar
Mário Pereira committed
514
    | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
Mário Pereira's avatar
Mário Pereira committed
515 516
      when isconstructor info rs && cty.cty_args <> [] ->
      (* partial application of constructors *)
Mário Pereira's avatar
Mário Pereira committed
517
      mk_eta_expansion rs pvl cty
Mário Pereira's avatar
Mário Pereira committed
518
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
Mário Pereira's avatar
Mário Pereira committed
519
      let pvl = app pvl rs.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
520
      begin match pvl with
521
      | [pv_expr] when is_optimizable_record_rs info rs -> pv_expr
522
      | _ -> ML.mk_expr (Mltree.Eapp (rs, pvl)) (Mltree.I e.e_ity) eff end
Mário Pereira's avatar
Mário Pereira committed
523 524 525
    | Eexec ({c_node = Cfun e; c_cty = {cty_args = []}}, _) ->
      (* abstract block *)
      expr info e
526
    | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
527
      let args = params cty.cty_args in
528
      ML.mk_expr (Mltree.Efun (args, expr info e)) (Mltree.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
529
    | Eexec ({c_node = Cany}, _) -> (* raise ExtractionAny *)
Mário Pereira's avatar
Mário Pereira committed
530
      ML.mk_hole
531
    | Eabsurd ->
532
      ML.mk_expr Mltree.Eabsurd (Mltree.I e.e_ity) eff
533 534
    | Ecase (e1, _) when e_ghost e1 ->
      ML.mk_unit
535
    | Ecase (e1, pl) ->
Mário Pereira's avatar
Mário Pereira committed
536 537
      let e1 = expr info e1 in
      let pl = List.map (ebranch info) pl in
538
      ML.mk_expr (Mltree.Ematch (e1, pl)) (Mltree.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
539
    | Eassert _ -> ML.mk_unit
Mário Pereira's avatar
Mário Pereira committed
540 541 542
    | Eif (e1, e2, e3) when e_ghost e3 ->
      let e1 = expr info e1 in
      let e2 = expr info e2 in
543
      ML.mk_expr (Mltree.Eif (e1, e2, ML.mk_unit)) (Mltree.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
544 545 546
    | Eif (e1, e2, e3) when e_ghost e2 ->
      let e1 = expr info e1 in
      let e3 = expr info e3 in
547
      ML.mk_expr (Mltree.Eif (e1, ML.mk_unit, e3)) (Mltree.I e.e_ity) eff
548
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
549 550 551
      let e1 = expr info e1 in
      let e2 = expr info e2 in
      let e3 = expr info e3 in
552
      ML.mk_expr (Mltree.Eif (e1, e2, e3)) (Mltree.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
553 554 555
    | Ewhile (e1, _, _, e2) ->
      let e1 = expr info e1 in
      let e2 = expr info e2 in
556
      ML.mk_expr (Mltree.Ewhile (e1, e2)) (Mltree.I e.e_ity) eff
557
    | Efor (pv1, (pv2, To, pv3), _, _, efor) ->
Mário Pereira's avatar
Mário Pereira committed
558
      let efor = expr info efor in
Mário Pereira's avatar
Mário Pereira committed
559
      mk_for_to info pv1 pv2 pv3 efor eff
560
    | Efor (pv1, (pv2, DownTo, pv3), _, _, efor) ->
Mário Pereira's avatar
Mário Pereira committed
561 562
      let efor = expr info efor in
      mk_for_downto info pv1 pv2 pv3 efor eff
Mário Pereira's avatar
Mário Pereira committed
563
    | Eghost _ -> assert false
564
    | Eassign al ->
565
      ML.mk_expr (Mltree.Eassign al) (Mltree.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
566
    | Epure _ -> (* assert false (\*TODO*\) *) ML.mk_hole
567 568
    | Etry (etry, case, pvl_e_map) ->
      assert (not case); (* TODO *)
Mário Pereira's avatar
Mário Pereira committed
569 570 571 572
      let etry = expr info etry in
      let bl   =
        let bl_map = Mxs.bindings pvl_e_map in
        List.map (fun (xs, (pvl, e)) -> xs, pvl, expr info e) bl_map in
573
      ML.mk_expr (Mltree.Etry (etry, bl)) (Mltree.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
574 575 576
    | Eraise (xs, ex) ->
      let ex =
        match expr info ex with
577
        | {Mltree.e_node = Mltree.Eblock []} -> None
Mário Pereira's avatar
Mário Pereira committed
578 579
        | e -> Some e
      in
580
      ML.mk_expr (Mltree.Eraise (xs, ex)) (Mltree.I e.e_ity) eff
581 582 583 584
    | Eexn (xs, e1) ->
      let e1 = expr info e1 in
      let ty = if ity_equal xs.xs_ity ity_unit
        then None else Some (ity xs.xs_ity) in
585
      ML.mk_expr (Mltree.Eexn (xs, ty, e1)) (Mltree.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
586 587 588 589
    | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
    (*   assert false (\*TODO*\) *)
    | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
    (*   assert false (\*TODO*\) *)
590

Mário Pereira's avatar
Mário Pereira committed
591 592
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
593

594
  (* type declarations/definitions *)
Mário Pereira's avatar
Mário Pereira committed
595
  let tdef itd =
596
    let s = itd.itd_its in
597 598 599
    let ddata_constructs = (* point-free *)
      List.map (fun ({rs_cty = rsc} as rs) ->
          rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
600
          let args = List.filter pv_not_ghost rsc.cty_args in
601 602
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
603
    let drecord_fields ({rs_cty = rsc} as rs) =
604
      (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields),
Mário Pereira's avatar
Mário Pereira committed
605 606
      rs.rs_name,
      ity rsc.cty_result
607 608 609 610
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
611
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
612
      | NoDef, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
613
        ML.mk_its_defn id args is_private None
614
      | NoDef, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
615
        let cl = ddata_constructs cl in
616
        ML.mk_its_defn id args is_private (Some (Mltree.Ddata cl))
617
      | NoDef, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
618 619
        let p e = not (rs_ghost e) in
        let pjl = filter_ghost_params p drecord_fields pjl in
Mário Pereira's avatar
Mário Pereira committed
620
        begin match pjl with
621 622
          | [] -> ML.mk_its_defn id args is_private
                    (Some (Mltree.Dalias ML.tunit))
623
          | [_, _, ty_pj] when is_optimizable_record_itd itd ->
624 625
            ML.mk_its_defn id args is_private (Some (Mltree.Dalias ty_pj))
          | pjl -> ML.mk_its_defn id args is_private (Some (Mltree.Drecord pjl))
Mário Pereira's avatar
Mário Pereira committed
626
        end
627
      | Alias t, _, _ ->
628
         ML.mk_its_defn id args is_private (Some (Mltree.Dalias (ity t)))
629 630
      | Range _, _, _ -> assert false (* TODO *)
      | Float _, _, _ -> assert false (* TODO *)
631
    end
Mário Pereira's avatar
Mário Pereira committed
632

633
  (* exception ExtractionVal of rsymbol *)
Mário Pereira's avatar
Mário Pereira committed
634

Mário Pereira's avatar
Mário Pereira committed
635 636 637 638
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

639 640
  (* pids: identifiers from cloned modules without definitions *)
  let pdecl _pids info pd =
Mário Pereira's avatar
Mário Pereira committed
641
    match pd.pd_node with
642
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
643
      []
Mário Pereira's avatar
Mário Pereira committed
644 645 646
    | PDlet (LDsym (_rs, {c_node = Cany})) ->
      []
      (* raise (ExtractionVal _rs) *)
Mário Pereira's avatar
Mário Pereira committed
647 648
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
      []
649
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
650
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
651
      let res  = ity cty.cty_result in
652
      [Mltree.Dlet (Mltree.Lsym (rs, res, args, expr info e))]
653
    | PDlet (LDrec rl) ->
654
      let rl = filter_out_ghost_rdef rl in
Mário Pereira's avatar
Mário Pereira committed
655
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
656
        let e = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
657
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
658
        let res  = ity rs1.rs_cty.cty_result in
659 660
        let svar =
          let args' = List.map (fun (_, ty, _) -> ty) args in
661
          let svar  = List.fold_left add_tvar Stv.empty args' in
662
          add_tvar svar res in
663 664 665 666
        { Mltree.rec_sym  = rs1;  Mltree.rec_rsym = rs2;
          Mltree.rec_args = args; Mltree.rec_exp  = expr info e;
          Mltree.rec_res  = res;  Mltree.rec_svar = svar; } in
      if rl = [] then [] else [Mltree.Dlet (Mltree.Lrec (List.map def rl))]
Mário Pereira's avatar
Mário Pereira committed
667
    | PDlet (LDsym _) | PDpure | PDlet (LDvar _) ->
668
      []
669
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
670
      let itsd = List.map tdef itl in
671
      [Mltree.Dtype itsd]
672
    | PDexn xs ->
673 674
      if ity_equal xs.xs_ity ity_unit then [Mltree.Dexn (xs, None)]
      else [Mltree.Dexn (xs, Some (ity xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
675

Mário Pereira's avatar
Mário Pereira committed
676
  let pdecl_m m pd =
677
    let info = { Mltree.from_mod = Some m; Mltree.from_km  = m.mod_known; } in
678
    pdecl Sid.empty info pd
Mário Pereira's avatar
Mário Pereira committed
679

Mário Pereira's avatar
Mário Pereira committed
680
  (* unit module declarations *)
681 682
  let rec mdecl pids info = function
    | Udecl pd -> pdecl pids info pd
683
    | Uscope (_, l) -> List.concat (List.map (mdecl pids info) l)
684
    | Uuse _ | Uclone _ | Umeta _ -> []
Mário Pereira's avatar
Mário Pereira committed
685

686 687 688 689 690 691 692 693 694 695 696
  let abstract_or_alias_type itd =
    itd.itd_fields = [] && itd.itd_constructors = []

  let empty_pdecl pd  = match pd.pd_node with
    | PDlet (LDsym (_, {c_node = Cfun _})) | PDlet (LDrec _) -> false
    | PDexn _ -> false (* FIXME? *)
    | PDtype itl -> List.for_all abstract_or_alias_type itl
    | _ -> true
  let rec empty_munit = function
    | Udecl pd -> empty_pdecl pd
    | Uclone mi -> List.for_all empty_munit mi.mi_mod.mod_units
697
    | Uscope (_, l) -> List.for_all empty_munit l
698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721
    | Uuse _ | Umeta _ -> true

  let is_empty_clone mi =
    Mts.is_empty mi.mi_ty &&
    Mts.is_empty mi.mi_ts &&
    Mls.is_empty mi.mi_ls &&
    Decl.Mpr.is_empty mi.mi_pr &&
    Decl.Mpr.is_empty mi.mi_pk &&
    Mvs.is_empty mi.mi_pv &&
    Mrs.is_empty mi.mi_rs &&
    Mxs.is_empty mi.mi_xs &&
    List.for_all empty_munit mi.mi_mod.mod_units

  let find_params dl =
    let add params = function
      | Uclone mi when is_empty_clone mi -> mi :: params
      | _ -> params in
    List.fold_left add [] dl

  let make_param from mi =
    let id = mi.mi_mod.mod_theory.Theory.th_name in
    Format.printf "param %s@." id.id_string;
    let dl =
      List.concat (List.map (mdecl Sid.empty from) mi.mi_mod.mod_units) in
722
    Mltree.Dclone (id, dl)
723 724 725 726

  let ids_of_params pids mi =
    Mid.fold (fun id _ pids -> Sid.add id pids) mi.mi_mod.mod_known pids

Mário Pereira's avatar
Mário Pereira committed
727
  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
728
  let module_ m =
729
    let from = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in
730 731 732 733
    let params = find_params m.mod_units in
    let pids = List.fold_left ids_of_params Sid.empty params in
    let mod_decl = List.concat (List.map (mdecl pids from) m.mod_units) in
    let mod_decl = List.map (make_param from) params @ mod_decl in
Mário Pereira's avatar
Mário Pereira committed
734 735 736
    let add known_map decl =
      let idl = ML.get_decl_name decl in
      List.fold_left (ML.add_known_decl decl) known_map idl in
737 738 739 740 741 742 743 744 745 746 747 748 749
    let mod_known = List.fold_left add Mid.empty mod_decl in {
      Mltree.mod_from = from;
      Mltree.mod_decl = mod_decl;
      Mltree.mod_known = mod_known
    }

  (* let () = Exn_printer.register (fun fmt e -> match e with *)
  (*   | ExtractionAny -> *)
  (*     Format.fprintf fmt "Cannot extract an undefined node" *)
  (*   | ExtractionVal rs -> *)
  (*     Format.fprintf fmt "Function %a cannot be extracted" *)
  (*       print_rs rs *)
  (*   | _ -> raise e) *)
Mário Pereira's avatar
Mário Pereira committed
750

Mário Pereira's avatar
Mário Pereira committed
751 752
end

753 754 755 756
(** Some transformations *)

module Transform = struct

757
  open Mltree
758

Mário Pereira's avatar
Mário Pereira committed
759
  let no_reads_writes_conflict spv spv_mreg =
760
    let is_not_write {pv_ity = ity} = match ity.ity_node with
Mário Pereira's avatar
Mário Pereira committed
761 762
        | Ityreg rho -> not (Mreg.mem rho spv_mreg)
        | _ -> true in
763
    Spv.for_all is_not_write spv
Mário Pereira's avatar
Mário Pereira committed
764

765
  (* type subst = expr Mpv.t *)
766

Mário Pereira's avatar
Mário Pereira committed
767 768 769 770 771
  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
772
  let rec expr info subst e =
Mário Pereira's avatar
Mário Pereira committed
773
    let mk e_node = { e with e_node = e_node } in
Mário Pereira's avatar
Mário Pereira committed
774
    let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
775
    match e.e_node with
Mário Pereira's avatar
Mário Pereira committed
776 777
    | 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
778
    | Elet (Lvar (pv, ({e_effect = eff1} as e1)), ({e_effect = eff2} as e2))
Mário Pereira's avatar
Mário Pereira committed
779
      when Slab.mem Expr.proxy_label pv.pv_vs.vs_name.id_label &&
Mário Pereira's avatar
Mário Pereira committed
780
           eff_pure eff1 &&
Mário Pereira's avatar
Mário Pereira committed
781
           no_reads_writes_conflict eff1.eff_reads eff2.eff_writes ->
Mário Pereira's avatar
Mário Pereira committed
782 783 784 785 786 787
      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
788
    | Elet (ld, e) ->
Mário Pereira's avatar
Mário Pereira committed
789 790 791
      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
792
    | Eapp (rs, el) ->
Mário Pereira's avatar
Mário Pereira committed
793 794
      let e_app, spv = mk_list_eb el (expr info subst) in
      mk (Eapp (rs, e_app)), spv
795
    | Efun (vl, e) ->
Mário Pereira's avatar
Mário Pereira committed
796 797 798 799 800 801 802 803
      (* 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
804
         restricted substitution. This keeps some proxy lets, preventing
Mário Pereira's avatar
Mário Pereira committed
805 806
         undiserable captures inside the [Efun] expression. *)
      let e, spv = expr info restrict_subst e in
Mário Pereira's avatar