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

Mário Pereira's avatar
Mário Pereira committed
163 164
  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
165

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
  let enope = Eblock []

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

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

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
  let mk_ignore e =
    if is_unit e.e_ity then e
Mário Pereira's avatar
Mário Pereira committed
197
    else mk_expr (Eignore e) ity_unit e.e_effect e.e_label
Mário Pereira's avatar
Mário Pereira committed
198

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 224 225 226 227 228
  (* remove ghost components from tuple, using mask *)
  let visible_of_mask m sl = match m with
    | MaskGhost    -> assert false (* FIXME ? *)
    | 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
229 230 231 232
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
233
       Mltree.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
234
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
235
       Mltree.Ttuple (List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
236
    | Tyapp (ts, tyl) ->
237
       Mltree.Tapp (ts.ts_name, List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
238 239 240 241

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

Mário Pereira's avatar
Mário Pereira committed
242 243 244 245 246
  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
247

248
  let rec filter_out_ghost_rdef = function
Mário Pereira's avatar
Mário Pereira committed
249 250
    | [] -> []
    | { rec_sym = rs; rec_rsym = rrs } :: l
251 252
      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
253

Mário Pereira's avatar
Mário Pereira committed
254
  let rec pat m p = match p.pat_node with
255
    | Pwild ->
256
      Mltree.Pwild
257
    | Pvar vs when (restore_pv vs).pv_ghost ->
258
      Mltree.Pwild
259
    | Pvar vs ->
260
      Mltree.Pident vs.vs_name
261
    | Por (p1, p2) ->
Mário Pereira's avatar
Mário Pereira committed
262
      Mltree.Por (pat m p1, pat m p2)
263
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
Mário Pereira's avatar
Mário Pereira committed
264
      pat m p
265
    | Pas (p, vs) ->
Mário Pereira's avatar
Mário Pereira committed
266
      Mltree.Pas (pat m p, vs.vs_name)
267
    | Papp (ls, pl) when is_fs_tuple ls ->
Mário Pereira's avatar
Mário Pereira committed
268 269 270 271 272
      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
273
    | Papp (ls, pl) ->
274 275
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
276
      let mk acc pv pp = if not pv.pv_ghost then pat m pp :: acc else acc in
277
      let pat_pl = List.fold_left2 mk [] args pl in
278
      Mltree.Papp (ls, List.rev pat_pl)
279

Mário Pereira's avatar
Mário Pereira committed
280 281
  (** programs *)

282 283
  let pv_name pv = pv.pv_vs.vs_name

284
  (* individual types *)
Mário Pereira's avatar
Mário Pereira committed
285 286
  let mlty_of_ity mask t =
    let rec loop t = match t.ity_node with
287
    | Ityvar (tvs, _) ->
288
      Mltree.Tvar tvs
289
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
Mário Pereira's avatar
Mário Pereira committed
290 291
      let itl = List.rev (visible_of_mask mask itl) in
      Mltree.Ttuple (List.map loop itl)
292
    | Ityapp ({its_ts = ts}, itl, _) ->
Mário Pereira's avatar
Mário Pereira committed
293
      Mltree.Tapp (ts.ts_name, List.map loop itl)
294
    | Ityreg {reg_its = its; reg_args = args} ->
Mário Pereira's avatar
Mário Pereira committed
295 296 297
      let args = List.map loop args in
      Mltree.Tapp (its.its_ts.ts_name, args) in
    loop t
Mário Pereira's avatar
Mário Pereira committed
298

Mário Pereira's avatar
Mário Pereira committed
299
  let pvty pv =
Mário Pereira's avatar
Mário Pereira committed
300 301
    if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true
    else let (vs, vs_ty) = vsty pv.pv_vs in
302
      ML.mk_var vs vs_ty false
Mário Pereira's avatar
Mário Pereira committed
303

304 305 306
  (* let for_direction = function *)
  (*   | To -> Mltree.To *)
  (*   | DownTo -> Mltree.DownTo *)
307

Mário Pereira's avatar
Mário Pereira committed
308
  let isconstructor info rs =
309
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
310 311 312 313 314 315
    | 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
316 317 318 319
  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
320
    let pv_equal_field rs = pv_equal (fd_of_rs rs) in
Mário Pereira's avatar
Mário Pereira committed
321 322 323 324
    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
325

326
  let get_record_itd 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
    | Some {pd_node = PDtype itdl} ->
      let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
330
      let itd = match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
331
        | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347
        | 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
348

Mário Pereira's avatar
Mário Pereira committed
349
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
350 351
    (* FIXME : effects and types of the expression in this situation *)
    let args_f =
Mário Pereira's avatar
Mário Pereira committed
352 353
      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
354 355
      filter_ghost_params pv_not_ghost def cty_app.cty_args in
    let args =
Mário Pereira's avatar
Mário Pereira committed
356 357
      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
358 359 360 361 362
      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
363
    let eapp = ML.mk_expr (Mltree.Eapp (rsc, args)) (Mltree.C cty_app)
Mário Pereira's avatar
Mário Pereira committed
364
        cty_app.cty_effect Slab.empty in
365
    ML.mk_expr (Mltree.Efun (args_f, eapp)) (Mltree.C cty_app)
Mário Pereira's avatar
Mário Pereira committed
366
      cty_app.cty_effect Slab.empty
Mário Pereira's avatar
Mário Pereira committed
367

368 369 370 371 372 373
  (* 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
374 375 376 377
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
      if args = [] then [ML.mk_var_unit ()] else args
378

Mário Pereira's avatar
Mário Pereira committed
379 380
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
381
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
382 383 384 385 386 387 388
      | 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
389 390
    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
391 392
    filter_params_cty pv_not_ghost def pvl cty_args

Mário Pereira's avatar
Mário Pereira committed
393
  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
394 395
    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
396 397 398
      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
399
    let for_rs    =
Mário Pereira's avatar
Mário Pereira committed
400
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
401
      let for_cty = create_cty [i_pv] [] [] Mxs.empty Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
402 403
      create_rsymbol for_id for_cty in
    let for_expr =
Mário Pereira's avatar
Mário Pereira committed
404 405 406
      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
407
      let next_expr =
408
        let one_const = Number.int_const_of_int 1 in
Mário Pereira's avatar
Mário Pereira committed
409
        let one_expr  =
Mário Pereira's avatar
Mário Pereira committed
410 411
          ML.mk_expr (Mltree.Econst one_const) ML.ity_int
            eff_empty Slab.empty in
412
        let i_op_one = Mltree.Eapp (op_a_rs, [i_expr; one_expr]) in
Mário Pereira's avatar
Mário Pereira committed
413 414 415 416
        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
417
      let seq_expr =
Mário Pereira's avatar
Mário Pereira committed
418 419 420 421
        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
422
    let for_call_expr = let for_call = Mltree.Eapp (for_rs, [from_expr]) in
Mário Pereira's avatar
Mário Pereira committed
423
      ML.mk_expr for_call ML.ity_unit eff Slab.empty in
Mário Pereira's avatar
Mário Pereira committed
424
    let pv_name pv = pv.pv_vs.vs_name in
425
    let args = [ pv_name i_pv, ty_int, false ] in
Mário Pereira's avatar
Mário Pereira committed
426
    let for_rec_def = {
427 428 429
      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
430
    } in
431
    let for_let = Mltree.Elet (Mltree.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
432 433 434 435
    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 =
436
      let ns = (Opt.get info.Mltree.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
437 438 439 440 441
      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 =
442
      let ns = (Opt.get info.Mltree.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
443 444 445
      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

446
  (* exception ExtractionAny *)
Mário Pereira's avatar
Mário Pereira committed
447

448 449
  (* build the set of type variables from functions arguments *)
  let rec add_tvar acc = function
450 451
    | Mltree.Tvar tv -> Stv.add tv acc
    | Mltree.Tapp (_, tyl) | Mltree.Ttuple tyl ->
452 453
      List.fold_left add_tvar acc tyl

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

Mário Pereira's avatar
Mário Pereira committed
609 610
  and ebranch info ({pp_pat = p; pp_mask = m}, e) =
    (pat m p, expr info e)
611

612
  (* type declarations/definitions *)
Mário Pereira's avatar
Mário Pereira committed
613
  let tdef itd =
614
    let s = itd.itd_its in
615
    let ddata_constructs = (* point-free *)
Mário Pereira's avatar
Mário Pereira committed
616
      List.map (fun ({rs_cty = cty} as rs) ->
617
          rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
618
          let args = List.filter pv_not_ghost cty.cty_args in
619 620
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
621
    let drecord_fields ({rs_cty = cty} as rs) =
622
      (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields),
Mário Pereira's avatar
Mário Pereira committed
623
      rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
624
      mlty_of_ity cty.cty_mask cty.cty_result
625 626 627 628
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
629
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
630
      | NoDef, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
631
        ML.mk_its_defn id args is_private None
632
      | NoDef, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
633
        let cl = ddata_constructs cl in
634
        ML.mk_its_defn id args is_private (Some (Mltree.Ddata cl))
635
      | NoDef, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
636 637
        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
638
        begin match pjl with
639 640
          | [] -> ML.mk_its_defn id args is_private
                    (Some (Mltree.Dalias ML.tunit))
641
          | [_, _, ty_pj] when is_optimizable_record_itd itd ->
642 643
            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
644
        end
645
      | Alias t, _, _ ->
Mário Pereira's avatar
Mário Pereira committed
646 647
        ML.mk_its_defn id args is_private (* FIXME ? is this a good mask ? *)
          (Some (Mltree.Dalias (mlty_of_ity MaskVisible t)))
648 649
      | Range _, _, _ -> assert false (* TODO *)
      | Float _, _, _ -> assert false (* TODO *)
650
    end
Mário Pereira's avatar
Mário Pereira committed
651

652
  (* exception ExtractionVal of rsymbol *)
Mário Pereira's avatar
Mário Pereira committed
653

Mário Pereira's avatar
Mário Pereira committed
654 655 656 657
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690
  let rec fun_expr_of_mask mask e =
    let open Mltree in
    let mk_e e_node = { e with e_node = e_node } in
    assert (mask <> MaskGhost);
    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)

691 692
  (* pids: identifiers from cloned modules without definitions *)
  let pdecl _pids info pd =
Mário Pereira's avatar
Mário Pereira committed
693
    match pd.pd_node with
694
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
695
      []
Mário Pereira's avatar
Mário Pereira committed
696 697 698
    | PDlet (LDsym (_rs, {c_node = Cany})) ->
      []
      (* raise (ExtractionVal _rs) *)
Mário Pereira's avatar
Mário Pereira committed
699 700
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
      []
701
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
702
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
703 704 705 706
      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))]
707
    | PDlet (LDrec rl) ->
708
      let rl = filter_out_ghost_rdef rl in
Mário Pereira's avatar
Mário Pereira committed
709
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
710
        let e = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
711
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
712
        let res  = mlty_of_ity rs1.rs_cty.cty_mask rs1.rs_cty.cty_result in
713 714
        let svar =
          let args' = List.map (fun (_, ty, _) -> ty) args in
715
          let svar  = List.fold_left add_tvar Stv.empty args' in
716
          add_tvar svar res in
Mário Pereira's avatar
Mário Pereira committed
717
        let e = fun_expr_of_mask rs1.rs_cty.cty_mask (expr info e) in
718
        { Mltree.rec_sym  = rs1;  Mltree.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
719
          Mltree.rec_args = args; Mltree.rec_exp  = e;
720 721
          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
722
    | PDlet (LDsym _) | PDpure | PDlet (LDvar _) ->
723
      []
724
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
725
      let itsd = List.map tdef itl in
726
      [Mltree.Dtype itsd]
727
    | PDexn xs ->
728
      if ity_equal xs.xs_ity ity_unit then [Mltree.Dexn (xs, None)]
Mário Pereira's avatar
Mário Pereira committed
729
      else [Mltree.Dexn (xs, Some (mlty_of_ity xs.xs_mask xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
730

Mário Pereira's avatar
Mário Pereira committed
731
  let pdecl_m m pd =
732
    let info = { Mltree.from_mod = Some m; Mltree.from_km  = m.mod_known; } in
733
    pdecl Sid.empty info pd
Mário Pereira's avatar
Mário Pereira committed
734

Mário Pereira's avatar
Mário Pereira committed
735
  (* unit module declarations *)
736 737
  let rec mdecl pids info = function
    | Udecl pd -> pdecl pids info pd
738
    | Uscope (_, l) -> List.concat (List.map (mdecl pids info) l)
739
    | Uuse _ | Uclone _ | Umeta _ -> []
Mário Pereira's avatar
Mário Pereira committed
740

741 742 743 744 745 746 747 748 749 750 751
  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
752
    | Uscope (_, l) -> List.for_all empty_munit l
753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776
    | 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
777
    Mltree.Dclone (id, dl)
778 779 780 781

  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
782
  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
783
  let module_ m =
784
    let from = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in
785 786 787 788
    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
789 790 791
    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
792 793 794 795 796 797 798 799 800 801 802 803 804
    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
805

Mário Pereira's avatar
Mário Pereira committed
806 807
end

808 809 810 811
(** Some transformations *)