compile.ml 35.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
(*                                                                  *)
(*  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
        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
62
    | _ -> 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
    | Ddata constrl ->
71
        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
    | Dalias ty -> iter_deps_ty f ty
74
    | Drange _ | Dfloat _ -> ()
Mário Pereira's avatar
Mário Pereira committed
75 76 77 78

  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
79 80 81 82 83 84 85 86 87 88 89 90 91
  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) ->
92 93
        f ls.ls_name;
        iter_deps_pat_list f patl
Mário Pereira's avatar
Mário Pereira committed
94 95
    | Ptuple patl -> iter_deps_pat_list f patl
    | Por (p1, p2) ->
96 97
        iter_deps_pat f p1;
        iter_deps_pat f p2
Mário Pereira's avatar
Mário Pereira committed
98 99 100
    | 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
101
    | Econst _ | Evar _ | Eabsurd | Ehole -> ()
Mário Pereira's avatar
Mário Pereira committed
102
    | Eapp (rs, exprl) ->
103
        f rs.rs_name; List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
104
    | Efun (args, e) ->
105 106
        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
107
    | Elet (Lvar (_, e1), e2) ->
108 109
        iter_deps_expr f e1;
        iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
110
    | Elet (Lsym (_, ty_result, args, e1), e2) ->
111 112 113 114
        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
115
    | Elet (Lany (_, ty_result, args), e2) ->
116 117 118
        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
119
    | Elet ((Lrec rdef), e) ->
120 121 122 123 124
        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
Mário Pereira's avatar
Mário Pereira committed
125
    | Ematch (e, branchl) ->
126 127
        iter_deps_expr f e;
        List.iter (fun (p, e) -> iter_deps_pat f p; iter_deps_expr f e) branchl
Mário Pereira's avatar
Mário Pereira committed
128
    | Eif (e1, e2, e3) ->
129 130 131
        iter_deps_expr f e1;
        iter_deps_expr f e2;
        iter_deps_expr f e3
Mário Pereira's avatar
Mário Pereira committed
132
    | Eblock exprl ->
133
        List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
134
    | Ewhile (e1, e2) ->
135 136
        iter_deps_expr f e1;
        iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
137
    | Efor (_, _, _, _, e) ->
138
        iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
139
    | Eraise (xs, None) ->
140
        f xs.xs_name
Mário Pereira's avatar
Mário Pereira committed
141
    | Eraise (xs, Some e) ->
142 143
        f xs.xs_name;
        iter_deps_expr f e
144
    | Eexn (_xs, None, e) -> (* FIXME? How come we never do binding here? *)
145
        iter_deps_expr f e
146
    | Eexn (_xs, Some ty, e) -> (* FIXME? How come we never do binding here? *)
147 148
        iter_deps_ty f ty;
        iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
149
    | Etry (e, xbranchl) ->
150 151
        iter_deps_expr f e;
        List.iter (iter_deps_xbranch f) xbranchl
Mário Pereira's avatar
Mário Pereira committed
152
    | Eassign assingl ->
153
        List.iter (fun (_, rs, _) -> f rs.rs_name) assingl
Mário Pereira's avatar
Mário Pereira committed
154
    | Eignore e -> iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
155

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

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

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

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

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

227 228 229
  let e_for pv1 pv2 dir pv3 e1 =
    mk_expr (Mltree.Efor (pv1, pv2, dir, pv3, e1)) ity_unit

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

233 234 235 236 237
  let e_assign al ity eff lbl =
    let rm_ghost (_, rs, _) = not (rs_ghost rs) in
    let al = List.filter rm_ghost al in
    if al = [] then e_unit else mk_expr (Mltree.Eassign al) ity eff lbl

238 239 240 241 242 243 244 245 246 247 248
  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
249

250
end
Mário Pereira's avatar
Mário Pereira committed
251 252 253 254 255

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
256 257 258
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
259

Mário Pereira's avatar
Mário Pereira committed
260 261 262
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
263 264
  (* 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
265
    | MaskGhost    -> assert false (* FIXME ? *)
Mário Pereira's avatar
Mário Pereira committed
266 267
    | MaskVisible  -> sl
    | MaskTuple ml ->
268 269 270
        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
271

Mário Pereira's avatar
Mário Pereira committed
272 273 274 275
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
276
        Mltree.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
277
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
278
        Mltree.Ttuple (List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
279
    | Tyapp (ts, tyl) ->
280
        Mltree.Tapp (ts.ts_name, List.map type_ tyl)
Mário Pereira's avatar
Mário Pereira committed
281 282 283 284

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

Mário Pereira's avatar
Mário Pereira committed
285 286 287
  let rec filter_ghost_params p def = function
    | [] -> []
    | pv :: l ->
288 289
        if p pv then def pv :: (filter_ghost_params p def l)
        else filter_ghost_params p def l
290

291
  let rec filter_out_ghost_rdef = function
Mário Pereira's avatar
Mário Pereira committed
292
    | [] -> []
293
    | { rec_sym = rs; rec_rsym = rrs } :: l when rs_ghost rs || rs_ghost rrs ->
294
        filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
295
    | rdef :: l ->
296
        rdef :: filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
297

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

Mário Pereira's avatar
Mário Pereira committed
324 325
  (** programs *)

326 327
  let pv_name pv = pv.pv_vs.vs_name

328
  (* individual types *)
Mário Pereira's avatar
Mário Pereira committed
329 330
  let mlty_of_ity mask t =
    let rec loop t = match t.ity_node with
331
      | _ when mask_equal mask MaskGhost -> ML.tunit
332
      | Ityvar tvs ->
333 334
          Mltree.Tvar tvs
      | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
335
          let itl = visible_of_mask mask itl in
336 337 338 339 340 341
          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
342
    loop t
Mário Pereira's avatar
Mário Pereira committed
343

Mário Pereira's avatar
Mário Pereira committed
344
  let pvty pv =
Mário Pereira's avatar
Mário Pereira committed
345 346
    if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true
    else let (vs, vs_ty) = vsty pv.pv_vs in
347
      ML.mk_var vs vs_ty false
Mário Pereira's avatar
Mário Pereira committed
348

349 350 351
  let for_direction = function
    | To -> Mltree.To
    | DownTo -> Mltree.DownTo
352

Mário Pereira's avatar
Mário Pereira committed
353
  let isconstructor info rs =
354
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
355
    | Some {pd_node = PDtype its} ->
356 357 358
        let is_constructor its =
          List.exists (rs_equal rs) its.itd_constructors in
        List.exists is_constructor its
Mário Pereira's avatar
Mário Pereira committed
359 360
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
361 362 363 364
  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
365
    let pv_equal_field rs = pv_equal (fd_of_rs rs) in
Mário Pereira's avatar
Mário Pereira committed
366 367 368 369
    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
370

371
  let get_record_itd info rs =
372
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
373
    | Some {pd_node = PDtype itdl} ->
374 375 376 377 378
        let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
        let itd = match rs.rs_field with
          | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
          | None -> List.find (fun itd -> f itd.itd_constructors) itdl in
        if itd.itd_fields = [] then None else Some itd
379 380 381 382 383 384 385 386 387 388 389 390 391 392
    | _ -> 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
393

Mário Pereira's avatar
Mário Pereira committed
394
  let mk_eta_expansion rs pvl ({cty_args = ca; cty_effect = ce} as c) =
Mário Pereira's avatar
Mário Pereira committed
395 396
    (* FIXME : effects and types of the expression in this situation *)
    let args_f =
Mário Pereira's avatar
Mário Pereira committed
397 398 399
      let def pv =
        (pv_name pv, mlty_of_ity (mask_of_pv pv) pv.pv_ity, pv.pv_ghost) in
      filter_ghost_params pv_not_ghost def ca in
Mário Pereira's avatar
Mário Pereira committed
400
    let args =
Mário Pereira's avatar
Mário Pereira committed
401 402
      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
403
      let args = filter_ghost_params pv_not_ghost def pvl in
Mário Pereira's avatar
Mário Pereira committed
404 405 406
      let extra_args = List.map def ca in args @ extra_args in
    let eapp = ML.mk_expr (Mltree.Eapp (rs, args)) (Mltree.C c) ce Slab.empty in
    ML.mk_expr (Mltree.Efun (args_f, eapp)) (Mltree.C c) ce Slab.empty
Mário Pereira's avatar
Mário Pereira committed
407

408 409 410 411 412 413
  (* 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
414 415 416
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
417
        if args = [] then [ML.mk_var_unit ()] else args
418

Mário Pereira's avatar
Mário Pereira committed
419 420
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
421
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
422
      | pv :: l1, arg :: l2 ->
Mário Pereira's avatar
Mário Pereira committed
423
          if p pv && p arg then def pv :: loop (l1, l2) else loop (l1, l2)
Mário Pereira's avatar
Mário Pereira committed
424 425 426 427
      | _ -> assert false
    in loop (pvl, cty_args)

  let app pvl cty_args =
Mário Pereira's avatar
Mário Pereira committed
428 429
    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
430 431
    filter_params_cty pv_not_ghost def pvl cty_args

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

438 439 440 441 442 443 444 445 446 447 448 449
  let exp_of_mask e = function
    | MaskGhost   -> e_void
    | MaskVisible -> e
    (* | MaskTuple l -> match e with *)
    (*   | Capp (rs, pvl) -> assert (is_rs_tuple rs); *)
    (*       let rec add_exp acc pv = begin function *)
    (*         | MaskGhost   -> acc *)
    (*         | MaskVisible -> pv *)
    (*         | MaskTuple l ->  *)
    (*       end *)
      | _ -> assert false

Mário Pereira's avatar
Mário Pereira committed
450
  (* expressions *)
451
  let rec expr info svar ({e_effect = eff; e_label = lbl} as e) =
452
    assert (not (e_ghost e));
Mário Pereira's avatar
Mário Pereira committed
453
    match e.e_node with
454
    | Econst c ->
455 456
        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
457
    | Evar pv -> ML.mk_expr (Mltree.Evar pv) (Mltree.I e.e_ity) eff lbl
458
    | Elet (LDvar (_, e1), e2) when e_ghost e1 -> expr info svar e2
459
    | Elet (LDvar (_, e1), e2) when e_ghost e2 ->
460 461 462
        (* sequences are transformed into [let o = e1 in e2] by A-normal form *)
        (* FIXME? this is only the case when [e1] is effectful ? *)
        assert (ity_equal ity_unit e1.e_ity);
463
        expr info svar e1
Mário Pereira's avatar
Mário Pereira committed
464 465
    | Elet (LDvar (pv, e1), e2)
      when pv.pv_ghost || not (Mpv.mem pv e2.e_effect.eff_reads) ->
466 467 468
        if eff_pure e1.e_effect then expr info svar e2
        else let e1 = ML.e_ignore (expr info svar e1) in
          ML.e_seq e1 (expr info svar e2) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
469
    | Elet (LDvar (pv, e1), e2) ->
470 471 472
        let ld = ML.var_defn pv (expr info svar e1) in
        ML.e_let ld (expr info svar e2) (Mltree.I e.e_ity) eff lbl
    | Elet (LDsym (rs, _), ein) when rs_ghost rs -> expr info svar ein
473
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
474 475
        let args = params cty.cty_args in
        let res = mlty_of_ity cty.cty_mask cty.cty_result in
476 477
        let ld = ML.sym_defn rs res args (expr info svar ef) in
        ML.e_let ld (expr info svar ein) (Mltree.I e.e_ity) eff lbl
478
    | Elet (LDsym (rs, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein)
479
      when isconstructor info rs_app -> (* partial application of constructor *)
480 481 482 483 484
        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
        let res = mlty_of_ity cty.cty_mask func in
        let ld = ML.sym_defn rs res [] eta_app in
485
        ML.e_let ld (expr info svar ein) (Mltree.I e.e_ity) e.e_effect lbl
Mário Pereira's avatar
Mário Pereira committed
486
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
487 488 489 490 491 492
        (* partial application *)
        let pvl = app pvl rs_app.rs_cty.cty_args in
        let eff = cty.cty_effect in
        let eapp = ML.e_app rs_app pvl (Mltree.C cty) eff 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
493
        ML.e_let ld (expr info svar ein) (Mltree.I e.e_ity) e.e_effect lbl
Mário Pereira's avatar
Mário Pereira committed
494
    | Elet (LDrec rdefl, ein) ->
495 496
        let rdefl = filter_out_ghost_rdef rdefl in
        let def = function
497 498
          | { rec_sym = rs1; rec_rsym = rs2;
              rec_fun = {c_node = Cfun ef; c_cty = cty} } ->
499 500
              let res = mlty_of_ity rs1.rs_cty.cty_mask rs1.rs_cty.cty_result in
              let args = params cty.cty_args in
501
              let new_svar =
502 503 504
                let args' = List.map (fun (_, ty, _) -> ty) args in
                let svar  = List.fold_left add_tvar Stv.empty args' in
                add_tvar svar res in
505 506
              let new_svar = Stv.diff svar new_svar in
              let ef = expr info (Stv.union svar new_svar) ef in
507
              { Mltree.rec_sym  = rs1;  Mltree.rec_rsym = rs2;
508 509
                Mltree.rec_args = args; Mltree.rec_exp  = ef;
                Mltree.rec_res  = res;  Mltree.rec_svar = new_svar; }
510 511 512
          | _ -> assert false in
        let rdefl = List.map def rdefl in
        if rdefl <> [] then
513
          let ml_letrec = Mltree.Elet (Mltree.Lrec rdefl, expr info svar ein) in
514
          ML.mk_expr ml_letrec (Mltree.I e.e_ity) e.e_effect lbl
515
        else expr info svar ein
516 517 518
    | 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
519
    | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
Mário Pereira's avatar
Mário Pereira committed
520
      when isconstructor info rs && cty.cty_args <> [] ->
521 522
        (* partial application of constructors *)
        mk_eta_expansion rs pvl cty
Mário Pereira's avatar
Mário Pereira committed
523
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
524 525 526 527
        let pvl = app pvl rs.rs_cty.cty_args in
        begin match pvl with
          | [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
528
    | Eexec ({c_node = Cfun e; c_cty = {cty_args = []}}, _) ->
529
        (* abstract block *)
530
        expr info svar e
531
    | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
532 533
        ML.e_fun (params cty.cty_args) (expr info svar e)
                 (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
534
    | Eexec ({c_node = Cany}, _) -> (* raise ExtractionAny *)
535
        ML.mk_hole
536
    | Eabsurd -> ML.e_absurd (Mltree.I e.e_ity) eff lbl
537
    | Ecase (e1, bl) when e_ghost e1 ->
538 539
        (* if [e1] is ghost but the entire [match-with] expression doesn't,
           it must be the case the first branch is irrefutable *)
540
        (match bl with [] -> assert false | (_, e) :: _ -> expr info svar e)
541
    | Ecase (e1, pl) ->
542 543
        let pl = List.map (ebranch info svar) pl in
        ML.e_match (expr info svar e1) pl (Mltree.I e.e_ity) eff lbl
544
    | Eassert _ -> ML.e_unit
545
    | Eif (e1, e2, e3) when e_ghost e1 ->
546 547
        (* if [e1] is ghost but the entire [if-then-else] expression doesn't,
           it must be the case one of the branches is [Eabsurd] *)
548
        if e2.e_node = Eabsurd then expr info svar e3 else expr info svar e2
Mário Pereira's avatar
Mário Pereira committed
549
    | Eif (e1, e2, e3) when e_ghost e3 ->
550
        ML.e_if (expr info svar e1) (expr info svar e2) ML.e_unit eff lbl
Mário Pereira's avatar
Mário Pereira committed
551
    | Eif (e1, e2, e3) when e_ghost e2 ->
552
        ML.e_if (expr info svar e1) ML.e_unit (expr info svar e3) eff lbl
553
    | Eif (e1, e2, e3) ->
554 555 556 557
        let e1 = expr info svar e1 in
        let e2 = expr info svar e2 in
        let e3 = expr info svar e3 in
        ML.e_if e1 e2 e3 eff lbl
Mário Pereira's avatar
Mário Pereira committed
558
    | Ewhile (e1, _, _, e2) ->
559
        ML.e_while (expr info svar e1) (expr info svar e2) eff lbl
560 561
    | Efor (pv1, (pv2, dir, pv3), _, _, efor) ->
        let dir = for_direction dir in
562
        let efor = expr info svar efor in
563
        ML.e_for pv1 pv2 dir pv3 efor eff lbl
Mário Pereira's avatar
Mário Pereira committed
564
    | Eghost _ -> assert false
565
    | Eassign al ->
566
        ML.e_assign al (Mltree.I e.e_ity) eff lbl
567
    | Epure _ -> assert false
568
    | Etry (etry, case, pvl_e_map) ->
569
        assert (not case); (* TODO *)
570
        let etry = expr info svar etry in
571 572
        let bl   =
          let bl_map = Mxs.bindings pvl_e_map in
573
          List.map (fun (xs, (pvl, e)) -> xs, pvl, expr info svar e) bl_map in
574
        ML.mk_expr (Mltree.Etry (etry, bl)) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
575
    | Eraise (xs, ex) ->
576 577
        let ex = exp_of_mask ex xs.xs_mask in
        let ex = match expr info svar ex with
578
          | {Mltree.e_node = Mltree.Eblock []} -> None
579
          | e -> Some e in
580
        ML.mk_expr (Mltree.Eraise (xs, ex)) (Mltree.I e.e_ity) eff lbl
581
    | Eexn (xs, e1) ->
582 583 584 585 586
        if mask_ghost e1.e_mask then ML.mk_expr
            (Mltree.Eexn (xs, None, ML.e_unit)) (Mltree.I e.e_ity) eff lbl
        else let e1 = expr info svar e1 in
          let ty = if ity_equal xs.xs_ity ity_unit then None else
              Some (mlty_of_ity xs.xs_mask xs.xs_ity) in
587
        ML.mk_expr (Mltree.Eexn (xs, ty, e1)) (Mltree.I e.e_ity) eff lbl
Mário Pereira's avatar
Mário Pereira committed
588 589
    | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
    | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
590

591
  and ebranch info svar ({pp_pat = p; pp_mask = m}, e) =
Mário Pereira's avatar
Mário Pereira committed
592 593 594
    (* 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 *)
595
    if e.e_effect.eff_ghost then (pat m p, ML.e_unit)
596
    else (pat m p, expr info svar e)
597

598
  (* type declarations/definitions *)
Mário Pereira's avatar
Mário Pereira committed
599
  let tdef itd =
600
    let s = itd.itd_its in
601
    let ddata_constructs = (* point-free *)
Mário Pereira's avatar
Mário Pereira committed
602
      List.map (fun ({rs_cty = cty} as rs) ->
603
          rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
604
          let args = List.filter pv_not_ghost cty.cty_args in
605 606
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
607
    let drecord_fields ({rs_cty = cty} as rs) =
608
      (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields),
Mário Pereira's avatar
Mário Pereira committed
609
      rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
610
      mlty_of_ity cty.cty_mask cty.cty_result
611 612 613 614
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
615
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
616
      | NoDef, [], [] ->
617
          ML.mk_its_defn id args is_private None
618
      | NoDef, cl, [] ->
619 620
          let cl = ddata_constructs cl in
          ML.mk_its_defn id args is_private (Some (Mltree.Ddata cl))
621
      | NoDef, _, pjl ->
622 623 624 625 626 627 628 629 630 631
          let p e = not (rs_ghost e) in
          let pjl = filter_ghost_params p drecord_fields pjl in
          begin match pjl with
            | [] -> ML.mk_its_defn id args is_private
                      (Some (Mltree.Dalias ML.tunit))
            | [_, _, ty_pj] when is_optimizable_record_itd itd ->
                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))
          end
632
      | Alias t, _, _ ->
Mário Pereira's avatar
Mário Pereira committed
633
          ML.mk_its_defn id args is_private (* FIXME ? is this a good mask ? *)
634
            (Some (Mltree.Dalias (mlty_of_ity MaskVisible t)))
635 636 637 638
      | Range r, [], [] ->
          assert (args = []); (* a range type is not polymorphic *)
          ML.mk_its_defn id [] is_private (Some (Mltree.Drange r))
      | Float ff, [], [] ->
639
          assert (args = []); (* a range type is not polymorphic *)
640 641 642 643
          ML.mk_its_defn id [] is_private (Some (Mltree.Dfloat ff))
      | (Range _ | Float _), _, _ ->
          assert false (* cannot have constructors or fields *)

644
    end
Mário Pereira's avatar
Mário Pereira committed
645

646
  (* exception ExtractionVal of rsymbol *)
Mário Pereira's avatar
Mário Pereira committed
647

Mário Pereira's avatar
Mário Pereira committed
648 649 650 651
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
652 653 654
  let rec fun_expr_of_mask mask e =
    let open Mltree in
    let mk_e e_node = { e with e_node = e_node } in
655
    (* assert (mask <> MaskGhost); *)
Mário Pereira's avatar
Mário Pereira committed
656 657
    match e.e_node with
    | Econst _ | Evar _   | Efun _ | Eassign _ | Ewhile _
658 659 660
    | Efor   _ | Eraise _ | Eexn _ | Eabsurd   | Ehole when mask = MaskGhost ->
        ML.e_unit
    | Econst _ | Evar _   | Efun _ | Eassign _ | Ewhile _
Mário Pereira's avatar
Mário Pereira committed
661 662
    | Efor   _ | Eraise _ | Eexn _ | Eabsurd   | Ehole    -> e
    | Eapp (rs, el) when is_rs_tuple rs ->
663 664 665 666
        begin match visible_of_mask mask el with
          | [] -> ML.e_unit
          | [e] -> e
          | el -> mk_e (Eapp (rs, el)) end
Mário Pereira's avatar
Mário Pereira committed
667 668
    | Eapp _ -> e
    | Elet (let_def, ein) -> let ein = fun_expr_of_mask mask ein in
669
        mk_e (Elet (let_def, ein))
Mário Pereira's avatar
Mário Pereira committed
670
    | Eif (e1, e2, e3) ->
671 672 673
        let e2 = fun_expr_of_mask mask e2 in
        let e3 = fun_expr_of_mask mask e3 in
        mk_e (Eif (e1, e2, e3))
Mário Pereira's avatar
Mário Pereira committed
674
    | Ematch (e1, pel) ->
675 676
        let mk_pel (p, ee) = (p, fun_expr_of_mask mask ee) in
        mk_e (Ematch (e1, List.map mk_pel pel))
Mário Pereira's avatar
Mário Pereira committed
677 678
    | Eblock [] -> e
    | Eblock el -> let (e_block, e_last) = Lists.chop_last el in
679 680
        let e_last = fun_expr_of_mask mask e_last in
        mk_e (Eblock (e_block @ [e_last]))
Mário Pereira's avatar
Mário Pereira committed
681
    | Etry (e1, xspvel) ->
682 683
        let mk_xspvel (xs, pvl, ee) = (xs, pvl, fun_expr_of_mask mask ee) in
        mk_e (Etry (e1, List.map mk_xspvel xspvel))
Mário Pereira's avatar
Mário Pereira committed
684
    | Eignore ee ->
685 686
        let ee = fun_expr_of_mask mask ee in
        mk_e (Eignore ee)
Mário Pereira's avatar
Mário Pereira committed
687

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

Mário Pereira's avatar
Mário Pereira committed
736
  let pdecl_m m pd =
737
    let info = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in
738
    pdecl Sid.empty info pd
Mário Pereira's avatar
Mário Pereira committed
739

740 741 742 743 744 745 746 747 748 749 750
  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
751
    | Uscope (_, l) -> List.for_all empty_munit l
752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770
    | 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
771 772 773 774
  (* unit module declarations *)
  let rec mdecl pids info = function
    | Udecl pd -> pdecl pids info pd
    | Uscope (_, ([Uuse _] | [Uclone _])) -> []
775
    | Uscope (s, dl) ->