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

48
  let rec get_decl_name = function
Mário Pereira's avatar
Mário Pereira committed
49 50
    | 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
    | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
    | Dlet (Lsym ({rs_name=id}, _, _, _))
Mário Pereira's avatar
Mário Pereira committed
53
    | Dlet (Lany ({rs_name=id}, _, _))
54
    | Dexn ({xs_name=id}, _) -> [id]
55
    | Dmodule (_, dl) -> List.concat (List.map get_decl_name dl)
Mário Pereira's avatar
Mário Pereira committed
56

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

Mário Pereira's avatar
Mário Pereira committed
66 67
  let rec iter_deps_ty f = function
    | Tvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
68
    | Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
Mário Pereira's avatar
Mário Pereira committed
69 70 71
    | 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
72 73
    | Ddata constrl ->
      List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
Mário Pereira's avatar
Mário Pereira committed
74
    | Drecord pjl -> List.iter (fun (_, _, ty) -> iter_deps_ty f ty) pjl
Mário Pereira's avatar
Mário Pereira committed
75 76 77 78 79
    | 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
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
  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
102
    | Econst _ | Evar _ | Eabsurd | Ehole -> ()
Mário Pereira's avatar
Mário Pereira committed
103 104
    | Eapp (rs, exprl) ->
      f rs.rs_name; List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
105 106 107
    | 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
108 109 110 111 112 113 114 115
    | 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
Mário Pereira's avatar
Mário Pereira committed
116 117 118 119
    | Elet (Lany (_, ty_result, args), e2) ->
      iter_deps_ty f ty_result;
      List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
      iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
    | 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
145 146 147 148 149
    | 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
150 151 152 153 154
    | 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
155
    | Eignore e -> iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
156

157
  let rec iter_deps f = function
Mário Pereira's avatar
Mário Pereira committed
158 159
    | Dtype its_dl ->
      List.iter (iter_deps_its_defn f) its_dl
Mário Pereira's avatar
Mário Pereira committed
160 161 162 163
    | Dlet (Lsym (_rs, ty_result, args, e)) ->
      iter_deps_ty f ty_result;
      iter_deps_args f args;
      iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
164 165 166
    | Dlet (Lany (_rs, ty_result, args)) ->
      iter_deps_ty f ty_result;
      iter_deps_args f args
Mário Pereira's avatar
Mário Pereira committed
167 168 169 170 171
    | 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
172 173 174
    | Dlet (Lvar (_, e)) -> iter_deps_expr f e
    | Dexn (_, None) -> ()
    | Dexn (_, Some ty) -> iter_deps_ty f ty
175
    | Dmodule (_, dl) -> List.iter (iter_deps f) dl
176

Mário Pereira's avatar
Mário Pereira committed
177 178
  let mk_expr e_node e_ity e_effect e_label =
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect; e_label = e_label; }
Mário Pereira's avatar
Mário Pereira committed
179

180
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
181
  let mk_let_var pv e1 e2 =
Mário Pereira's avatar
Mário Pereira committed
182
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
183 184

  let tunit = Ttuple []
185

Mário Pereira's avatar
Mário Pereira committed
186 187 188 189 190 191
  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
192

193 194 195
  let enope = Eblock []

  let mk_unit =
Mário Pereira's avatar
Mário Pereira committed
196
    mk_expr enope (I Ity.ity_unit) Ity.eff_empty Slab.empty
197

Mário Pereira's avatar
Mário Pereira committed
198
  let mk_hole =
Mário Pereira's avatar
Mário Pereira committed
199
    mk_expr Ehole (I Ity.ity_unit) Ity.eff_empty Slab.empty
Mário Pereira's avatar
Mário Pereira committed
200

201 202
  let mk_var id ty ghost = (id, ty, ghost)

203 204
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

205
  let mk_its_defn id args private_ def =
Mário Pereira's avatar
Mário Pereira committed
206 207
    { its_name    = id      ; its_args = args;
      its_private = private_; its_def  = def; }
208

Mário Pereira's avatar
Mário Pereira committed
209 210
  let mk_ignore e =
    if is_unit e.e_ity then e
Mário Pereira's avatar
Mário Pereira committed
211
    else mk_expr (Eignore e) ity_unit e.e_effect e.e_label
Mário Pereira's avatar
Mário Pereira committed
212

213 214
  let eseq e1 e2 =
    match e1.e_node, e2.e_node with
Mário Pereira's avatar
Mário Pereira committed
215
    | (Eblock [] | Ehole), e | e, (Eblock [] | Ehole) -> e
216 217 218 219 220
    | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
    | _, Eblock e2 -> Eblock (e1 :: e2)
    | Eblock e1, _ -> Eblock (e1 @ [e2])
    | _ -> Eblock [e1; e2]

221
end
Mário Pereira's avatar
Mário Pereira committed
222 223 224 225 226

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
227 228 229
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
230

Mário Pereira's avatar
Mário Pereira committed
231 232 233
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
234 235
  (* remove ghost components from tuple, using mask *)
  let visible_of_mask m sl = match m with
236
    | MaskGhost    -> assert false (* FIXME *)
Mário Pereira's avatar
Mário Pereira committed
237 238 239 240 241 242
    | MaskVisible  -> sl
    | MaskTuple ml ->
      let add_ity acc m ity = if mask_ghost m then acc else ity :: acc in
      if List.length sl < List.length ml then sl (* FIXME ? much likely... *)
      else List.fold_left2 add_ity [] ml sl

Mário Pereira's avatar
Mário Pereira committed
243 244 245 246
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
247
       Mltree.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
248
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
249
       Mltree.Ttuple (List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
250
    | Tyapp (ts, tyl) ->
251
       Mltree.Tapp (ts.ts_name, List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
252 253 254 255

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

Mário Pereira's avatar
Mário Pereira committed
256 257 258 259 260
  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
261

262
  let rec filter_out_ghost_rdef = function
Mário Pereira's avatar
Mário Pereira committed
263
    | [] -> []
264 265
    | { rec_sym = rs; rec_rsym = rrs } :: l when rs_ghost rs || rs_ghost rrs ->
      filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
266 267
    | rdef :: l ->
      rdef :: filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
268

Mário Pereira's avatar
Mário Pereira committed
269
  let rec pat m p = match p.pat_node with
270
    | Pwild ->
271
      Mltree.Pwild
272
    | Pvar vs when (restore_pv vs).pv_ghost ->
273
      Mltree.Pwild
274
    | Pvar vs ->
275
      Mltree.Pident vs.vs_name
276
    | Por (p1, p2) ->
Mário Pereira's avatar
Mário Pereira committed
277
      Mltree.Por (pat m p1, pat m p2)
278
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
Mário Pereira's avatar
Mário Pereira committed
279
      pat m p
280
    | Pas (p, vs) ->
Mário Pereira's avatar
Mário Pereira committed
281
      Mltree.Pas (pat m p, vs.vs_name)
282
    | Papp (ls, pl) when is_fs_tuple ls ->
Mário Pereira's avatar
Mário Pereira committed
283 284 285 286 287
      let pl = visible_of_mask m pl in
      begin match pl with
        | [] -> Mltree.Pwild
        | [p] -> pat m p
        | _ -> Mltree.Ptuple (List.map (pat m) pl) end
288
    | Papp (ls, pl) ->
289 290
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
291
      let mk acc pv pp = if not pv.pv_ghost then pat m pp :: acc else acc in
292
      let pat_pl = List.fold_left2 mk [] args pl in
293
      Mltree.Papp (ls, List.rev pat_pl)
294

Mário Pereira's avatar
Mário Pereira committed
295 296
  (** programs *)

297 298
  let pv_name pv = pv.pv_vs.vs_name

299
  (* individual types *)
Mário Pereira's avatar
Mário Pereira committed
300 301
  let mlty_of_ity mask t =
    let rec loop t = match t.ity_node with
302 303 304 305 306 307 308 309 310 311 312 313 314
      | _ when mask_ghost mask ->
        ML.tunit
      | Ityvar (tvs, _) ->
        Mltree.Tvar tvs
      | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
        let itl = List.rev (visible_of_mask mask itl) in
        Mltree.Ttuple (List.map loop itl)
      | Ityapp ({its_ts = ts}, itl, _) ->
        let itl = List.rev (visible_of_mask mask itl) in
        Mltree.Tapp (ts.ts_name, List.map loop itl)
      | Ityreg {reg_its = its; reg_args = args} ->
        let args = List.map loop args in
        Mltree.Tapp (its.its_ts.ts_name, args) in
Mário Pereira's avatar
Mário Pereira committed
315
    loop t
Mário Pereira's avatar
Mário Pereira committed
316

Mário Pereira's avatar
Mário Pereira committed
317
  let pvty pv =
Mário Pereira's avatar
Mário Pereira committed
318 319
    if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true
    else let (vs, vs_ty) = vsty pv.pv_vs in
320
      ML.mk_var vs vs_ty false
Mário Pereira's avatar
Mário Pereira committed
321

322 323 324
  (* let for_direction = function *)
  (*   | To -> Mltree.To *)
  (*   | DownTo -> Mltree.DownTo *)
325

Mário Pereira's avatar
Mário Pereira committed
326
  let isconstructor info rs =
327
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
328 329 330 331 332 333
    | 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
334 335 336 337
  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
338
    let pv_equal_field rs = pv_equal (fd_of_rs rs) in
Mário Pereira's avatar
Mário Pereira committed
339 340 341 342
    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
343

344
  let get_record_itd info rs =
345
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
346 347
    | Some {pd_node = PDtype itdl} ->
      let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
348
      let itd = match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
349
        | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365
        | 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
366

Mário Pereira's avatar
Mário Pereira committed
367
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
368 369
    (* FIXME : effects and types of the expression in this situation *)
    let args_f =
Mário Pereira's avatar
Mário Pereira committed
370 371
      let def pv =
        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
372 373
      filter_ghost_params pv_not_ghost def cty_app.cty_args in
    let args =
Mário Pereira's avatar
Mário Pereira committed
374 375
      let def pv =
        ML.mk_expr (Mltree.Evar pv) (Mltree.I pv.pv_ity) eff_empty Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
376 377 378 379 380
      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
381
    let eapp = ML.mk_expr (Mltree.Eapp (rsc, args)) (Mltree.C cty_app)
Mário Pereira's avatar
Mário Pereira committed
382
        cty_app.cty_effect Slab.empty in
383
    ML.mk_expr (Mltree.Efun (args_f, eapp)) (Mltree.C cty_app)
Mário Pereira's avatar
Mário Pereira committed
384
      cty_app.cty_effect Slab.empty
Mário Pereira's avatar
Mário Pereira committed
385

386 387 388 389 390 391
  (* 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
392 393 394 395
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
      if args = [] then [ML.mk_var_unit ()] else args
396

Mário Pereira's avatar
Mário Pereira committed
397 398
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
399
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
400 401 402 403 404 405 406
      | 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 =
Mário Pereira's avatar
Mário Pereira committed
407 408
    let def pv =
      ML.mk_expr (Mltree.Evar pv) (Mltree.I pv.pv_ity) eff_empty Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
409 410
    filter_params_cty pv_not_ghost def pvl cty_args

Mário Pereira's avatar
Mário Pereira committed
411
  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
412 413
    let i_expr, from_expr, to_expr =
      let int_ity = ML.ity_int in let eff_e = eff_empty in
Mário Pereira's avatar
Mário Pereira committed
414 415 416
      ML.mk_expr (Mltree.Evar i_pv)    int_ity eff_e Slab.empty,
      ML.mk_expr (Mltree.Evar from_pv) int_ity eff_e Slab.empty,
      ML.mk_expr (Mltree.Evar to_pv)   int_ity eff_e Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
417
    let for_rs    =
Mário Pereira's avatar
Mário Pereira committed
418
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
419
      let for_cty = create_cty [i_pv] [] [] Mxs.empty Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
420 421
      create_rsymbol for_id for_cty in
    let for_expr =
Mário Pereira's avatar
Mário Pereira committed
422 423 424
      let test =
        ML.mk_expr (Mltree.Eapp (op_b_rs, [i_expr; to_expr]))
          (Mltree.I ity_bool) eff_empty Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
425
      let next_expr =
426
        let one_const = Number.int_const_of_int 1 in
Mário Pereira's avatar
Mário Pereira committed
427
        let one_expr  =
Mário Pereira's avatar
Mário Pereira committed
428 429
          ML.mk_expr (Mltree.Econst one_const) ML.ity_int
            eff_empty Slab.empty in
430
        let i_op_one = Mltree.Eapp (op_a_rs, [i_expr; one_expr]) in
Mário Pereira's avatar
Mário Pereira committed
431 432 433 434
        ML.mk_expr i_op_one ML.ity_int eff_empty Slab.empty in
      let rec_call  =
        ML.mk_expr (Mltree.Eapp (for_rs, [next_expr])) ML.ity_unit
          eff Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
435
      let seq_expr =
Mário Pereira's avatar
Mário Pereira committed
436 437 438 439
        ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff Slab.empty in
      ML.mk_expr (Mltree.Eif (test, seq_expr, ML.mk_unit)) ML.ity_unit
        eff Slab.empty in
    let ty_int = mlty_of_ity MaskVisible ity_int in
Mário Pereira's avatar
Mário Pereira committed
440
    let for_call_expr = let for_call = Mltree.Eapp (for_rs, [from_expr]) in
Mário Pereira's avatar
Mário Pereira committed
441
      ML.mk_expr for_call ML.ity_unit eff Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
442
    let pv_name pv = pv.pv_vs.vs_name in
443
    let args = [ pv_name i_pv, ty_int, false ] in
Mário Pereira's avatar
Mário Pereira committed
444
    let for_rec_def = {
445 446 447
      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
448
    } in
449
    let for_let = Mltree.Elet (Mltree.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
450 451 452 453
    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 =
454
      let ns = (Opt.get info.Mltree.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
455 456 457 458 459
      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 =
460
      let ns = (Opt.get info.Mltree.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
461 462 463
      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

464
  (* exception ExtractionAny *)
Mário Pereira's avatar
Mário Pereira committed
465

466 467
  (* build the set of type variables from functions arguments *)
  let rec add_tvar acc = function
468 469
    | Mltree.Tvar tv -> Stv.add tv acc
    | Mltree.Tapp (_, tyl) | Mltree.Ttuple tyl ->
470 471
      List.fold_left add_tvar acc tyl

Mário Pereira's avatar
Mário Pereira committed
472
  (* expressions *)
Mário Pereira's avatar
Mário Pereira committed
473
  let rec expr info ({e_effect = eff; e_label = lbl} as e) =
Mário Pereira's avatar
Mário Pereira committed
474
    assert (not eff.eff_ghost);
Mário Pereira's avatar
Mário Pereira committed
475
    match e.e_node with
476
    | Econst c ->
Mário Pereira's avatar
Mário Pereira committed
477 478
      let c = match c with Number.ConstInt c -> c | _ -> assert false in
      ML.mk_expr (Mltree.Econst c) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
479
    | Evar pv ->
Mário Pereira's avatar
Mário Pereira committed
480
      ML.mk_expr (Mltree.Evar pv) (Mltree.I e.e_ity) eff lbl
481
    | Elet (LDvar (_, e1), e2) when e_ghost e1 ->
Mário Pereira's avatar
Mário Pereira committed
482
      expr info e2
483
    | Elet (LDvar (_, e1), e2) when e_ghost e2 ->
Mário Pereira's avatar
Mário Pereira committed
484
      ML.mk_expr (ML.eseq (expr info e1) ML.mk_unit) ML.ity_unit eff lbl
Mário Pereira's avatar
Mário Pereira committed
485 486 487 488
    | 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
Mário Pereira's avatar
Mário Pereira committed
489
        ML.mk_expr (ML.eseq e1 (expr info e2)) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
490 491
    | Elet (LDvar (pv, e1), e2) ->
      let ml_let = ML.mk_let_var pv (expr info e1) (expr info e2) in
Mário Pereira's avatar
Mário Pereira committed
492
      ML.mk_expr ml_let (Mltree.I e.e_ity) eff lbl
493 494
    | Elet (LDsym (rs, _), ein) when rs_ghost rs ->
      expr info ein
495
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
496
      let args = params cty.cty_args in
497 498
      let ef = expr info ef in
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
499
      let res = mlty_of_ity cty.cty_mask cty.cty_result in
500
      let ml_letrec = Mltree.Elet (Mltree.Lsym (rs, res, args, ef), ein) in
Mário Pereira's avatar
Mário Pereira committed
501
      ML.mk_expr ml_letrec (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
502 503
    | 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
504 505
      (* partial application of constructor *)
      let eta_app = mk_eta_expansion rs_app pvl cty in
Mário Pereira's avatar
Mário Pereira committed
506
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
507 508
      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
Mário Pereira's avatar
Mário Pereira committed
509
      let res = mlty_of_ity cty.cty_mask func in
510
      let ml_letrec = Mltree.Elet (Mltree.Lsym (rsf, res, [], eta_app), ein) in
Mário Pereira's avatar
Mário Pereira committed
511
      ML.mk_expr ml_letrec (Mltree.I e.e_ity) e.e_effect lbl
Mário Pereira's avatar
Mário Pereira committed
512
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
513
      (* partial application *)
Mário Pereira's avatar
Mário Pereira committed
514
      let pvl = app pvl rs_app.rs_cty.cty_args in
515
      let eapp =
Mário Pereira's avatar
Mário Pereira committed
516 517
        ML.mk_expr (Mltree.Eapp (rs_app, pvl)) (Mltree.C cty)
          cty.cty_effect Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
518
      let ein  = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
519
      let res  = mlty_of_ity cty.cty_mask cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
520
      let args = params cty.cty_args in
521
      let ml_letrec = Mltree.Elet (Mltree.Lsym (rsf, res, args, eapp), ein) in
Mário Pereira's avatar
Mário Pereira committed
522
      ML.mk_expr ml_letrec (Mltree.I e.e_ity) e.e_effect lbl
Mário Pereira's avatar
Mário Pereira committed
523
    | Elet (LDrec rdefl, ein) ->
524 525 526 527
      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}} ->
Mário Pereira's avatar
Mário Pereira committed
528
          let res  = mlty_of_ity rs1.rs_cty.cty_mask rs1.rs_cty.cty_result in
529 530 531
          let args = params cty.cty_args in
          let svar =
            let args' = List.map (fun (_, ty, _) -> ty) args in
532
            let svar  = List.fold_left add_tvar Stv.empty args' in
533 534
            add_tvar svar res in
          let ef = expr info ef in
535 536 537
          { Mltree.rec_sym  = rs1;  Mltree.rec_rsym = rs2;
            Mltree.rec_args = args; Mltree.rec_exp  = ef ;
            Mltree.rec_res  = res;  Mltree.rec_svar = svar; }
538 539
        | _ -> assert false in
      let rdefl = List.map def rdefl in
540
      if rdefl <> [] then
541
        let ml_letrec = Mltree.Elet (Mltree.Lrec rdefl, expr info ein) in
Mário Pereira's avatar
Mário Pereira committed
542
        ML.mk_expr ml_letrec (Mltree.I e.e_ity) e.e_effect lbl
543
      else expr info ein
544 545
    | Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs ->
      ML.mk_unit
546 547
    | Eexec ({c_node = Capp (rs, _)}, _) when is_empty_record info rs ->
      ML.mk_unit
548 549
    | Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
      ML.mk_unit
Mário Pereira's avatar
Mário Pereira committed
550
    | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
Mário Pereira's avatar
Mário Pereira committed
551 552
      when isconstructor info rs && cty.cty_args <> [] ->
      (* partial application of constructors *)
Mário Pereira's avatar
Mário Pereira committed
553
      mk_eta_expansion rs pvl cty
Mário Pereira's avatar
Mário Pereira committed
554
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
Mário Pereira's avatar
Mário Pereira committed
555
      let pvl = app pvl rs.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
556
      begin match pvl with
557
      | [pv_expr] when is_optimizable_record_rs info rs -> pv_expr
Mário Pereira's avatar
Mário Pereira committed
558
      | _ -> ML.mk_expr (Mltree.Eapp (rs, pvl)) (Mltree.I e.e_ity) eff lbl end
Mário Pereira's avatar
Mário Pereira committed
559 560 561
    | Eexec ({c_node = Cfun e; c_cty = {cty_args = []}}, _) ->
      (* abstract block *)
      expr info e
562
    | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
563
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
564
      ML.mk_expr (Mltree.Efun (args, expr info e)) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
565
    | Eexec ({c_node = Cany}, _) -> (* raise ExtractionAny *)
Mário Pereira's avatar
Mário Pereira committed
566
      ML.mk_hole
567
    | Eabsurd ->
Mário Pereira's avatar
Mário Pereira committed
568
      ML.mk_expr Mltree.Eabsurd (Mltree.I e.e_ity) eff lbl
569 570
    | Ecase (e1, _) when e_ghost e1 ->
      ML.mk_unit
571
    | Ecase (e1, pl) ->
Mário Pereira's avatar
Mário Pereira committed
572 573
      let e1 = expr info e1 in
      let pl = List.map (ebranch info) pl in
Mário Pereira's avatar
Mário Pereira committed
574
      ML.mk_expr (Mltree.Ematch (e1, pl)) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
575
    | Eassert _ -> ML.mk_unit
Mário Pereira's avatar
Mário Pereira committed
576 577 578
    | Eif (e1, e2, e3) when e_ghost e3 ->
      let e1 = expr info e1 in
      let e2 = expr info e2 in
Mário Pereira's avatar
Mário Pereira committed
579
      ML.mk_expr (Mltree.Eif (e1, e2, ML.mk_unit)) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
580 581 582
    | Eif (e1, e2, e3) when e_ghost e2 ->
      let e1 = expr info e1 in
      let e3 = expr info e3 in
Mário Pereira's avatar
Mário Pereira committed
583
      ML.mk_expr (Mltree.Eif (e1, ML.mk_unit, e3)) (Mltree.I e.e_ity) eff lbl
584
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
585 586 587
      let e1 = expr info e1 in
      let e2 = expr info e2 in
      let e3 = expr info e3 in
Mário Pereira's avatar
Mário Pereira committed
588
      ML.mk_expr (Mltree.Eif (e1, e2, e3)) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
589 590 591
    | Ewhile (e1, _, _, e2) ->
      let e1 = expr info e1 in
      let e2 = expr info e2 in
Mário Pereira's avatar
Mário Pereira committed
592
      ML.mk_expr (Mltree.Ewhile (e1, e2)) (Mltree.I e.e_ity) eff lbl
593
    | Efor (pv1, (pv2, To, pv3), _, _, efor) ->
Mário Pereira's avatar
Mário Pereira committed
594
      let efor = expr info efor in
Mário Pereira's avatar
Mário Pereira committed
595
      mk_for_to info pv1 pv2 pv3 efor eff lbl
596
    | Efor (pv1, (pv2, DownTo, pv3), _, _, efor) ->
Mário Pereira's avatar
Mário Pereira committed
597
      let efor = expr info efor in
Mário Pereira's avatar
Mário Pereira committed
598
      mk_for_downto info pv1 pv2 pv3 efor eff lbl
Mário Pereira's avatar
Mário Pereira committed
599
    | Eghost _ -> assert false
600
    | Eassign al ->
Mário Pereira's avatar
Mário Pereira committed
601
      ML.mk_expr (Mltree.Eassign al) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
602
    | Epure _ -> (* assert false (\*TODO*\) *) ML.mk_hole
603 604
    | Etry (etry, case, pvl_e_map) ->
      assert (not case); (* TODO *)
Mário Pereira's avatar
Mário Pereira committed
605 606 607 608
      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
Mário Pereira's avatar
Mário Pereira committed
609
      ML.mk_expr (Mltree.Etry (etry, bl)) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
610 611 612
    | Eraise (xs, ex) ->
      let ex =
        match expr info ex with
613
        | {Mltree.e_node = Mltree.Eblock []} -> None
Mário Pereira's avatar
Mário Pereira committed
614 615
        | e -> Some e
      in
Mário Pereira's avatar
Mário Pereira committed
616
      ML.mk_expr (Mltree.Eraise (xs, ex)) (Mltree.I e.e_ity) eff lbl
617 618 619
    | Eexn (xs, e1) ->
      let e1 = expr info e1 in
      let ty = if ity_equal xs.xs_ity ity_unit
Mário Pereira's avatar
Mário Pereira committed
620 621
        then None else Some (mlty_of_ity xs.xs_mask xs.xs_ity) in
      ML.mk_expr (Mltree.Eexn (xs, ty, e1)) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
622 623 624 625
    | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
    (*   assert false (\*TODO*\) *)
    | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
    (*   assert false (\*TODO*\) *)
626

Mário Pereira's avatar
Mário Pereira committed
627
  and ebranch info ({pp_pat = p; pp_mask = m}, e) =
628 629 630 631 632 633 634
    (* If the [case] expression is not ghost but there is (at least) one ghost
       branch, then it must be the case that this is an effectful [case],
       i.e., at least one of the non-ghost branches is effectful.  In extract
       code, the onlye sound meaning for this [case] expression is to keep for
       each branch the effectul sub-expression. This is similar to the case
       of a [let x = e1 in e2] where [x] is a ghost [pvsymbol] *)
    if e.e_effect.eff_ghost then (pat m p, ML.mk_unit)
Mário Pereira's avatar
Mário Pereira committed
635
    else (pat m p, expr info e)
636

637
  (* type declarations/definitions *)
Mário Pereira's avatar
Mário Pereira committed
638
  let tdef itd =
639
    let s = itd.itd_its in
640
    let ddata_constructs = (* point-free *)
Mário Pereira's avatar
Mário Pereira committed
641
      List.map (fun ({rs_cty = cty} as rs) ->
642
          rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
643
          let args = List.filter pv_not_ghost cty.cty_args in
644 645
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
646
    let drecord_fields ({rs_cty = cty} as rs) =
647
      (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields),
Mário Pereira's avatar
Mário Pereira committed
648
      rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
649
      mlty_of_ity cty.cty_mask cty.cty_result
650 651 652 653
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
654
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
655
      | NoDef, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
656
        ML.mk_its_defn id args is_private None
657
      | NoDef, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
658
        let cl = ddata_constructs cl in
659
        ML.mk_its_defn id args is_private (Some (Mltree.Ddata cl))
660
      | NoDef, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
661 662
        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
663
        begin match pjl with
664 665
          | [] -> ML.mk_its_defn id args is_private
                    (Some (Mltree.Dalias ML.tunit))
666
          | [_, _, ty_pj] when is_optimizable_record_itd itd ->
667 668
            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
669
        end
670
      | Alias t, _, _ ->
Mário Pereira's avatar
Mário Pereira committed
671 672
        ML.mk_its_defn id args is_private (* FIXME ? is this a good mask ? *)
          (Some (Mltree.Dalias (mlty_of_ity MaskVisible t)))
673 674
      | Range _, _, _ -> assert false (* TODO *)
      | Float _, _, _ -> assert false (* TODO *)
675
    end
Mário Pereira's avatar
Mário Pereira committed
676

677
  (* exception ExtractionVal of rsymbol *)
Mário Pereira's avatar
Mário Pereira committed
678

Mário Pereira's avatar
Mário Pereira committed
679 680 681 682
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
683 684 685
  let rec fun_expr_of_mask mask e =
    let open Mltree in
    let mk_e e_node = { e with e_node = e_node } in
686
    (* assert (mask <> MaskGhost); *)
Mário Pereira's avatar
Mário Pereira committed
687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715
    match e.e_node with
    | Econst _ | Evar _   | Efun _ | Eassign _ | Ewhile _
    | Efor   _ | Eraise _ | Eexn _ | Eabsurd   | Ehole    -> e
    | Eapp (rs, el) when is_rs_tuple rs ->
      begin match visible_of_mask mask el with
        | [] -> ML.mk_unit
        | [e] -> e
        | el -> mk_e (Eapp (rs, el)) end
    | Eapp _ -> e
    | Elet (let_def, ein) -> let ein = fun_expr_of_mask mask ein in
      mk_e (Elet (let_def, ein))
    | Eif (e1, e2, e3) ->
      let e2 = fun_expr_of_mask mask e2 in
      let e3 = fun_expr_of_mask mask e3 in
      mk_e (Eif (e1, e2, e3))
    | Ematch (e1, pel) ->
      let mk_pel (p, ee) = (p, fun_expr_of_mask mask ee) in
      mk_e (Ematch (e1, List.map mk_pel pel))
    | Eblock [] -> e
    | Eblock el -> let (e_block, e_last) = Lists.chop_last el in
      let e_last = fun_expr_of_mask mask e_last in
      mk_e (Eblock (e_block @ [e_last]))
    | Etry (e1, xspvel) ->
      let mk_xspvel (xs, pvl, ee) = (xs, pvl, fun_expr_of_mask mask ee) in
      mk_e (Etry (e1, List.map mk_xspvel xspvel))
    | Eignore ee ->
      let ee = fun_expr_of_mask mask ee in
      mk_e (Eignore ee)

716 717
  (* pids: identifiers from cloned modules without definitions *)
  let pdecl _pids info pd =
Mário Pereira's avatar
Mário Pereira committed
718
    match pd.pd_node with
719
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
720
      []
Mário Pereira's avatar
Mário Pereira committed
721 722 723 724
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cany})) ->
      let args = params cty.cty_args in
      let res = mlty_of_ity cty.cty_mask cty.cty_result in
      [Mltree.Dlet (Mltree.Lany (rs, res, args))]
Mário Pereira's avatar
Mário Pereira committed
725
      (* raise (ExtractionVal _rs) *)
Mário Pereira's avatar
Mário Pereira committed
726 727
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
      []
Mário Pereira's avatar
Mário Pereira committed
728
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e; c_cty = _c_cty})) ->
729
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
730 731 732 733 734
      (* let open Format in *)
      (* let pr_mask fmt = function *)
      (*   | MaskVisible -> fprintf fmt "Visible@." *)
      (*   | MaskTuple _ -> fprintf fmt "Tuple@." *)
      (*   | MaskGhost   -> fprintf fmt "Ghost@." in *)
Mário Pereira's avatar
Mário Pereira committed
735
      let res = mlty_of_ity cty.cty_mask cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
736
      (* eprintf "Mask of %s:%a@." rs.rs_name.id_string pr_mask c_cty.cty_mask; *)
Mário Pereira's avatar
Mário Pereira committed
737 738 739
      let e = expr info e in
      let e = fun_expr_of_mask cty.cty_mask e in
      [Mltree.Dlet (Mltree.Lsym (rs, res, args, e))]
740
    | PDlet (LDrec rl) ->
741
      let rl = filter_out_ghost_rdef rl in
Mário Pereira's avatar
Mário Pereira committed
742
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
743
        let e = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
744
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
745
        let res  = mlty_of_ity rs1.rs_cty.cty_mask rs1.rs_cty.cty_result in
746 747
        let svar =
          let args' = List.map (fun (_, ty, _) -> ty) args in
748
          let svar  = List.fold_left add_tvar Stv.empty args' in
749
          add_tvar svar res in
Mário Pereira's avatar
Mário Pereira committed
750
        let e = fun_expr_of_mask rs1.rs_cty.cty_mask (expr info e) in
751
        { Mltree.rec_sym  = rs1;  Mltree.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
752
          Mltree.rec_args = args; Mltree.rec_exp  = e;
753 754
          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
755
    | PDlet (LDsym _) | PDpure | PDlet (LDvar _) ->
756
      []
757
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
758
      let itsd = List.map tdef itl in
759
      [Mltree.Dtype itsd]
760
    | PDexn xs ->
761
      if ity_equal xs.xs_ity ity_unit then [Mltree.Dexn (xs, None)]
Mário Pereira's avatar
Mário Pereira committed
762
      else [Mltree.Dexn (xs, Some (mlty_of_ity xs.xs_mask xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
763

Mário Pereira's avatar
Mário Pereira committed
764
  let pdecl_m m pd =
765
    let info = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in
766
    pdecl Sid.empty info pd
Mário Pereira's avatar
Mário Pereira committed
767

768 769 770 771 772 773 774 775 776 777 778
  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
779
    | Uscope (_, l) -> List.for_all empty_munit l
780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798
    | 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

Mário Pereira's avatar
Mário Pereira committed
799 800 801 802
  (* unit module declarations *)
  let rec mdecl pids info = function
    | Udecl pd -> pdecl pids info pd
    | Uscope (_, ([Uuse _] | [Uclone _])) -> []
803 804