compile.ml 35.5 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
(*                                                                  *)
(*  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

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

46
  let rec get_decl_name = function
Mário Pereira's avatar
Mário Pereira committed
47 48
    | Dtype itdefl -> List.map (fun {its_name = id} -> id) itdefl
    | Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
49 50
    | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
    | Dlet (Lsym ({rs_name=id}, _, _, _))
Mário Pereira's avatar
Mário Pereira committed
51
    | Dlet (Lany ({rs_name=id}, _, _))
52
    | Dexn ({xs_name=id}, _) -> [id]
53
    | Dmodule (_, dl) -> List.concat (List.map get_decl_name dl)
Mário Pereira's avatar
Mário Pereira committed
54

55
  let rec add_known_decl decl k_map id =
Mário Pereira's avatar
Mário Pereira committed
56
    match decl with
57
    | Dmodule (_, dl) ->
58 59 60 61 62
      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
63

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

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

Mário Pereira's avatar
Mário Pereira committed
175 176
  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
177

Mário Pereira's avatar
Mário Pereira committed
178
  let tunit = Ttuple []
179

Mário Pereira's avatar
Mário Pereira committed
180 181 182 183 184 185
  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
186

187 188
  let enope = Eblock []

Mário Pereira's avatar
Mário Pereira committed
189
  let mk_hole =
Mário Pereira's avatar
Mário Pereira committed
190
    mk_expr Ehole (I Ity.ity_unit) Ity.eff_empty Slab.empty
Mário Pereira's avatar
Mário Pereira committed
191

192 193
  let mk_var id ty ghost = (id, ty, ghost)

194 195
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

196
  let mk_its_defn id args private_ def =
Mário Pereira's avatar
Mário Pereira committed
197 198
    { its_name    = id      ; its_args = args;
      its_private = private_; its_def  = def; }
199

200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
  (* smart constructors *)
  let e_unit =
    mk_expr enope (I Ity.ity_unit) Ity.eff_empty Slab.empty

  let var_defn pv e =
    Lvar (pv, e)

  let sym_defn f ty_res args e =
    Lsym (f, ty_res, args, e)

  let e_let ld e = mk_expr (Elet (ld, e))

  let e_app rs pvl =
    mk_expr (Mltree.Eapp (rs, pvl))

  let e_fun args e = mk_expr (Efun (args, e))

  let e_ignore e =
Mário Pereira's avatar
Mário Pereira committed
218
    if is_unit e.e_ity then e
Mário Pereira's avatar
Mário Pereira committed
219
    else mk_expr (Eignore e) ity_unit e.e_effect e.e_label
Mário Pereira's avatar
Mário Pereira committed
220

221
  let e_if e1 e2 e3 =
Mário Pereira's avatar
Mário Pereira committed
222
    mk_expr (Mltree.Eif (e1, e2, e3)) e2.e_ity
223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240

  let e_while e1 e2 =
    mk_expr (Mltree.Ewhile (e1, e2)) ity_unit

  let e_match e bl =
    mk_expr (Mltree.Ematch (e, bl))

  let e_absurd =
    mk_expr Eabsurd

  let e_seq e1 e2 =
    let e = match e1.e_node, e2.e_node with
      | (Eblock [] | Ehole), e | e, (Eblock [] | Ehole) -> e
      | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
      | _, Eblock e2 -> Eblock (e1 :: e2)
      | Eblock e1, _ -> Eblock (e1 @ [e2])
      | _ -> Eblock [e1; e2] in
    mk_expr e
241

242
end
Mário Pereira's avatar
Mário Pereira committed
243 244 245 246 247

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
248 249 250
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
251

Mário Pereira's avatar
Mário Pereira committed
252 253 254
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
255 256
  (* remove ghost components from tuple, using mask *)
  let visible_of_mask m sl = match m with
Mário Pereira's avatar
Mário Pereira committed
257
    | MaskGhost    -> assert false (* FIXME ? *)
Mário Pereira's avatar
Mário Pereira committed
258 259 260 261 262 263
    | 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
264 265 266 267
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
268
       Mltree.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
269
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
270
       Mltree.Ttuple (List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
271
    | Tyapp (ts, tyl) ->
272
       Mltree.Tapp (ts.ts_name, List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
273 274 275 276

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

Mário Pereira's avatar
Mário Pereira committed
277 278 279 280 281
  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
282

283
  let rec filter_out_ghost_rdef = function
Mário Pereira's avatar
Mário Pereira committed
284
    | [] -> []
285 286
    | { 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
287 288
    | rdef :: l ->
      rdef :: filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
289

Mário Pereira's avatar
Mário Pereira committed
290
  let rec pat m p = match p.pat_node with
291
    | Pwild ->
292
      Mltree.Pwild
293
    | Pvar vs when (restore_pv vs).pv_ghost ->
294
      Mltree.Pwild
295
    | Pvar vs ->
296
      Mltree.Pident vs.vs_name
297
    | Por (p1, p2) ->
Mário Pereira's avatar
Mário Pereira committed
298
      Mltree.Por (pat m p1, pat m p2)
299
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
Mário Pereira's avatar
Mário Pereira committed
300
      pat m p
301
    | Pas (p, vs) ->
Mário Pereira's avatar
Mário Pereira committed
302
      Mltree.Pas (pat m p, vs.vs_name)
303
    | Papp (ls, pl) when is_fs_tuple ls ->
Mário Pereira's avatar
Mário Pereira committed
304 305 306 307 308
      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
309
    | Papp (ls, pl) ->
310 311
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
312
      let mk acc pv pp = if not pv.pv_ghost then pat m pp :: acc else acc in
313
      let pat_pl = List.fold_left2 mk [] args pl in
314
      Mltree.Papp (ls, List.rev pat_pl)
315

Mário Pereira's avatar
Mário Pereira committed
316 317
  (** programs *)

318 319
  let pv_name pv = pv.pv_vs.vs_name

320
  (* individual types *)
Mário Pereira's avatar
Mário Pereira committed
321 322
  let mlty_of_ity mask t =
    let rec loop t = match t.ity_node with
323
    | _ when mask_equal mask MaskGhost -> ML.tunit
Mário Pereira's avatar
Mário Pereira committed
324 325 326 327 328 329 330 331 332 333
    | 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, _) ->
      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
334
    loop t
Mário Pereira's avatar
Mário Pereira committed
335

Mário Pereira's avatar
Mário Pereira committed
336
  let pvty pv =
Mário Pereira's avatar
Mário Pereira committed
337 338
    if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true
    else let (vs, vs_ty) = vsty pv.pv_vs in
339
      ML.mk_var vs vs_ty false
Mário Pereira's avatar
Mário Pereira committed
340

341 342 343
  (* let for_direction = function *)
  (*   | To -> Mltree.To *)
  (*   | DownTo -> Mltree.DownTo *)
344

Mário Pereira's avatar
Mário Pereira committed
345
  let isconstructor info rs =
346
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
347 348 349 350 351 352
    | 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
353 354 355 356
  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
357
    let pv_equal_field rs = pv_equal (fd_of_rs rs) in
Mário Pereira's avatar
Mário Pereira committed
358 359 360 361
    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
362

363
  let get_record_itd info rs =
364
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
365 366
    | Some {pd_node = PDtype itdl} ->
      let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
367
      let itd = match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
368
        | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384
        | 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
385

Mário Pereira's avatar
Mário Pereira committed
386
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
387 388
    (* FIXME : effects and types of the expression in this situation *)
    let args_f =
389 390
      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
391 392
      filter_ghost_params pv_not_ghost def cty_app.cty_args in
    let args =
393 394
      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
395
      let args = filter_ghost_params pv_not_ghost def pvl in
396
      let extra_args = List.map def cty_app.cty_args in args @ extra_args in
397
    let eapp = ML.mk_expr (Mltree.Eapp (rsc, args)) (Mltree.C cty_app)
Mário Pereira's avatar
Mário Pereira committed
398
        cty_app.cty_effect Slab.empty in
399
    ML.mk_expr (Mltree.Efun (args_f, eapp)) (Mltree.C cty_app)
Mário Pereira's avatar
Mário Pereira committed
400
      cty_app.cty_effect Slab.empty
Mário Pereira's avatar
Mário Pereira committed
401

402 403 404 405 406 407
  (* 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
408 409 410 411
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
      if args = [] then [ML.mk_var_unit ()] else args
412

Mário Pereira's avatar
Mário Pereira committed
413 414
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
415
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
416 417 418 419 420 421 422
      | 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
423 424
    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
425 426
    filter_params_cty pv_not_ghost def pvl cty_args

Mário Pereira's avatar
Mário Pereira committed
427
  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
428 429
    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
430 431 432
      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
433
    let for_rs    =
Mário Pereira's avatar
Mário Pereira committed
434
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
435
      let for_cty = create_cty [i_pv] [] [] Mxs.empty Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
436 437
      create_rsymbol for_id for_cty in
    let for_expr =
Mário Pereira's avatar
Mário Pereira committed
438 439 440
      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
441
      let next_expr =
442
        let one_const = Number.int_const_of_int 1 in
Mário Pereira's avatar
Mário Pereira committed
443
        let one_expr  =
Mário Pereira's avatar
Mário Pereira committed
444 445
          ML.mk_expr (Mltree.Econst one_const) ML.ity_int
            eff_empty Slab.empty in
446
        let i_op_one = Mltree.Eapp (op_a_rs, [i_expr; one_expr]) in
Mário Pereira's avatar
Mário Pereira committed
447 448 449 450
        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
451
      let seq_expr =
452 453
        ML.e_seq body_expr rec_call ML.ity_unit eff Slab.empty in
      ML.mk_expr (Mltree.Eif (test, seq_expr, ML.e_unit)) ML.ity_unit
Mário Pereira's avatar
Mário Pereira committed
454 455
        eff Slab.empty in
    let ty_int = mlty_of_ity MaskVisible ity_int in
Mário Pereira's avatar
Mário Pereira committed
456
    let for_call_expr = let for_call = Mltree.Eapp (for_rs, [from_expr]) in
Mário Pereira's avatar
Mário Pereira committed
457
      ML.mk_expr for_call ML.ity_unit eff Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
458
    let pv_name pv = pv.pv_vs.vs_name in
459
    let args = [ pv_name i_pv, ty_int, false ] in
Mário Pereira's avatar
Mário Pereira committed
460
    let for_rec_def = {
461 462 463
      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
464
    } in
465
    let for_let = Mltree.Elet (Mltree.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
466 467 468 469
    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 =
470
      let ns = (Opt.get info.Mltree.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
471 472 473 474 475
      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 =
476
      let ns = (Opt.get info.Mltree.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
477 478 479
      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

480
  (* exception ExtractionAny *)
Mário Pereira's avatar
Mário Pereira committed
481

482 483
  (* build the set of type variables from functions arguments *)
  let rec add_tvar acc = function
484 485
    | Mltree.Tvar tv -> Stv.add tv acc
    | Mltree.Tapp (_, tyl) | Mltree.Ttuple tyl ->
486 487
      List.fold_left add_tvar acc tyl

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

Mário Pereira's avatar
Mário Pereira committed
624
  and ebranch info ({pp_pat = p; pp_mask = m}, e) =
Mário Pereira's avatar
Mário Pereira committed
625 626 627
    (* 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 *)
628
    if e.e_effect.eff_ghost then (pat m p, ML.e_unit)
Mário Pereira's avatar
Mário Pereira committed
629
    else (pat m p, expr info e)
630

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

671
  (* exception ExtractionVal of rsymbol *)
Mário Pereira's avatar
Mário Pereira committed
672

Mário Pereira's avatar
Mário Pereira committed
673 674 675 676
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
677 678 679
  let rec fun_expr_of_mask mask e =
    let open Mltree in
    let mk_e e_node = { e with e_node = e_node } in
680
    (* assert (mask <> MaskGhost); *)
Mário Pereira's avatar
Mário Pereira committed
681 682 683 684 685
    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
686
        | [] -> ML.e_unit
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
        | [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)

710 711
  (* pids: identifiers from cloned modules without definitions *)
  let pdecl _pids info pd =
Mário Pereira's avatar
Mário Pereira committed
712
    match pd.pd_node with
713
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
714
      []
Mário Pereira's avatar
Mário Pereira committed
715 716 717 718
    | 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
719 720
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
      []
Mário Pereira's avatar
Mário Pereira committed
721
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
722
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
723 724 725 726
      let res = mlty_of_ity cty.cty_mask cty.cty_result in
      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))]
727
    | PDlet (LDrec rl) ->
728
      let rl = filter_out_ghost_rdef rl in
Mário Pereira's avatar
Mário Pereira committed
729
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
730
        let e = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
731
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
732
        let res  = mlty_of_ity rs1.rs_cty.cty_mask rs1.rs_cty.cty_result in
733 734
        let svar =
          let args' = List.map (fun (_, ty, _) -> ty) args in
735
          let svar  = List.fold_left add_tvar Stv.empty args' in
736
          add_tvar svar res in
Mário Pereira's avatar
Mário Pereira committed
737
        let e = fun_expr_of_mask rs1.rs_cty.cty_mask (expr info e) in
738
        { Mltree.rec_sym  = rs1;  Mltree.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
739
          Mltree.rec_args = args; Mltree.rec_exp  = e;
740 741
          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
742
    | PDlet (LDsym _) | PDpure | PDlet (LDvar _) ->
743
      []
744
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
745
      let itsd = List.map tdef itl in
746
      [Mltree.Dtype itsd]
747
    | PDexn xs ->
748
      if ity_equal xs.xs_ity ity_unit then [Mltree.Dexn (xs, None)]
Mário Pereira's avatar
Mário Pereira committed
749
      else [Mltree.Dexn (xs, Some (mlty_of_ity xs.xs_mask xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
750

Mário Pereira's avatar
Mário Pereira committed
751
  let pdecl_m m pd =
752
    let info = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in
753
    pdecl Sid.empty info pd
Mário Pereira's avatar
Mário Pereira committed
754

755 756 757 758 759 760 761 762 763 764 765
  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
766
    | Uscope (_, l) -> List.for_all empty_munit l
767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785
    | 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
786 787 788 789
  (* unit module declarations *)
  let rec mdecl pids info = function
    | Udecl pd -> pdecl pids info pd
    | Uscope (_, ([Uuse _] | [Uclone _])) -> []
790 791 792
    | Uscope (s, dl) ->
      let dl = List.concat (List.map (mdecl pids info) dl) in
      [Mltree.Dmodule (s, dl)]
Mário Pereira's avatar
Mário Pereira committed
793 794
    | Uuse _ | Uclone _ | Umeta _ -> []

795 796 797
  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
798
  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
799
  let module_ m =
800
    let from = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in
801 802 803
    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
804
    let add_decl known_map decl = let idl = ML.get_decl_name decl in
Mário Pereira's avatar
Mário Pereira committed
805
      List.fold_left (ML.add_known_decl decl) known_map idl in
806
    let mod_known = List.fold_left add_decl Mid.empty mod_decl in {
807 808
      Mltree.mod_from = from;
      Mltree.mod_decl = mod_decl;
809
      Mltree.mod_known = mod_known;
810 811 812 813 814 815 816 817 818
    }

  (* 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
819

Mário Pereira's avatar
Mário Pereira committed
820 821
end