compile.ml 35.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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 49 50 51 52 53
    | Dtype itdefl ->
        let add_id = function
          | Some (Ddata l)   -> List.map (fun (idc,    _) -> idc) l
          | Some (Drecord l) -> List.map (fun (_, idp, _) -> idp) l
          | _ -> [] in
        let add_td_ids {its_name = id; its_def = def} = id :: (add_id def) in
        List.flatten (List.map add_td_ids itdefl)
Mário Pereira's avatar
Mário Pereira committed
54
    | Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
55 56
    | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
    | Dlet (Lsym ({rs_name=id}, _, _, _))
Mário Pereira's avatar
Mário Pereira committed
57
    | Dlet (Lany ({rs_name=id}, _, _))
58
    | Dexn ({xs_name=id}, _) -> [id]
59
    | Dmodule (_, dl) -> List.concat (List.map get_decl_name dl)
Mário Pereira's avatar
Mário Pereira committed
60

61
  let rec add_known_decl decl k_map id =
Mário Pereira's avatar
Mário Pereira committed
62
    match decl with
63
    | Dmodule (_, dl) ->
64 65 66 67
        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
68
    | _ -> Mid.add id decl k_map
Mário Pereira's avatar
Mário Pereira committed
69

Mário Pereira's avatar
Mário Pereira committed
70 71
  let rec iter_deps_ty f = function
    | Tvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
72
    | Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
Mário Pereira's avatar
Mário Pereira committed
73 74 75
    | 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
76
    | Ddata constrl ->
77
        List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
Mário Pereira's avatar
Mário Pereira committed
78
    | Drecord pjl -> List.iter (fun (_, _, ty) -> iter_deps_ty f ty) pjl
Mário Pereira's avatar
Mário Pereira committed
79
    | Dalias ty -> iter_deps_ty f ty
80
    | Drange _ | Dfloat _ -> ()
Mário Pereira's avatar
Mário Pereira committed
81 82 83 84

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

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

Mário Pereira's avatar
Mário Pereira committed
182
  let mk_expr e_node e_ity e_effect e_label =
Mário Pereira's avatar
Mário Pereira committed
183
    { e_node; e_ity; e_effect; e_label; }
Mário Pereira's avatar
Mário Pereira committed
184

Mário Pereira's avatar
Mário Pereira committed
185
  let tunit = Ttuple []
186

Mário Pereira's avatar
Mário Pereira committed
187 188 189 190 191
  let ity_unit = I Ity.ity_unit

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

193 194
  let enope = Eblock []

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

198 199
  let mk_var id ty ghost = (id, ty, ghost)

200 201
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

202
  let mk_its_defn id args private_ def =
Mário Pereira's avatar
Mário Pereira committed
203 204
    { its_name    = id      ; its_args = args;
      its_private = private_; its_def  = def; }
205

206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223
  (* 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
224
    if is_unit e.e_ity then e
Mário Pereira's avatar
Mário Pereira committed
225
    else mk_expr (Eignore e) ity_unit e.e_effect e.e_label
Mário Pereira's avatar
Mário Pereira committed
226

227
  let e_if e1 e2 e3 =
Mário Pereira's avatar
Mário Pereira committed
228
    mk_expr (Mltree.Eif (e1, e2, e3)) e2.e_ity
229 230 231 232

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

233 234 235
  let e_for pv1 pv2 dir pv3 e1 =
    mk_expr (Mltree.Efor (pv1, pv2, dir, pv3, e1)) ity_unit

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

239 240 241
  let e_assign al ity eff lbl =
    if al = [] then e_unit else mk_expr (Mltree.Eassign al) ity eff lbl

242 243 244 245 246 247 248 249 250 251 252
  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
253

254
end
Mário Pereira's avatar
Mário Pereira committed
255 256 257 258 259

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
260 261 262
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
263

Mário Pereira's avatar
Mário Pereira committed
264 265 266
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
267 268 269 270 271
  (* remove ghost components from tuple, using mask *)
  let visible_of_mask m sl = match m with
    | MaskGhost    -> assert false (* FIXME ? *)
    | MaskVisible  -> sl
    | MaskTuple ml ->
272 273 274
        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
275

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

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

Mário Pereira's avatar
Mário Pereira committed
289 290 291
  let rec filter_ghost_params p def = function
    | [] -> []
    | pv :: l ->
292 293
        if p pv then def pv :: (filter_ghost_params p def l)
        else filter_ghost_params p def l
294

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

Mário Pereira's avatar
Mário Pereira committed
302
  let rec pat m p = match p.pat_node with
303
    | Pwild ->
304
        Mltree.Pwild
305
    | Pvar vs when (restore_pv vs).pv_ghost ->
306
        Mltree.Pwild
307
    | Pvar vs ->
308
        Mltree.Pvar vs
309
    | Por (p1, p2) ->
310
        Mltree.Por (pat m p1, pat m p2)
311
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
312
        pat m p
313
    | Pas (p, vs) ->
314
        Mltree.Pas (pat m p, vs)
315
    | Papp (ls, pl) when is_fs_tuple ls ->
316 317 318 319 320
        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
321
    | Papp (ls, pl) ->
322 323 324 325 326
        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)
327

Mário Pereira's avatar
Mário Pereira committed
328 329
  (** programs *)

330 331
  let pv_name pv = pv.pv_vs.vs_name

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

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

353 354 355
  let for_direction = function
    | To -> Mltree.To
    | DownTo -> Mltree.DownTo
356

Mário Pereira's avatar
Mário Pereira committed
357
  let isconstructor info rs =
358
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
359
    | Some {pd_node = PDtype its} ->
360 361 362
        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
363 364
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
365 366 367 368
  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
369
    let pv_equal_field rs = pv_equal (fd_of_rs rs) in
Mário Pereira's avatar
Mário Pereira committed
370 371 372 373
    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
374

375
  let get_record_itd info rs =
376
    match Mid.find_opt rs.rs_name info.Mltree.from_km with
Mário Pereira's avatar
Mário Pereira committed
377
    | Some {pd_node = PDtype itdl} ->
378 379 380 381 382
        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
383 384 385 386 387 388 389 390 391 392 393 394 395 396
    | _ -> 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
397

Mário Pereira's avatar
Mário Pereira committed
398
  let mk_eta_expansion rs pvl ({cty_args = ca; cty_effect = ce} as c) =
Mário Pereira's avatar
Mário Pereira committed
399 400
    (* FIXME : effects and types of the expression in this situation *)
    let args_f =
Mário Pereira's avatar
Mário Pereira committed
401 402 403
      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
404
    let args =
Mário Pereira's avatar
Mário Pereira committed
405 406
      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
407
      let args = filter_ghost_params pv_not_ghost def pvl in
Mário Pereira's avatar
Mário Pereira committed
408 409 410
      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
411

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

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

  let app pvl cty_args =
Mário Pereira's avatar
Mário Pereira committed
432 433
    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
434 435
    filter_params_cty pv_not_ghost def pvl cty_args

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

442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477
  let rec fun_expr_of_mask mask e =
    let open Mltree in
    let mk_e e_node = { e with e_node = e_node } in
    match e.e_node with
    | Econst _ | Evar _   | Efun _ | Eassign _ | Ewhile _
    | Efor   _ | Eraise _ | Eexn _ | Eabsurd   | Ehole when mask = MaskGhost ->
        ML.e_unit
    | 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.e_unit
          | [e] -> e
          | el -> mk_e (Eapp (rs, el)) end
    | Eapp _ when mask = MaskGhost -> (* FIXME ? *)
        ML.e_unit
    | 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)
478

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

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

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

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

679 680
  (* pids: identifiers from cloned modules without definitions *)
  let pdecl _pids info pd =
Mário Pereira's avatar
Mário Pereira committed
681
    match pd.pd_node with
682 683 684 685 686 687 688 689
    | PDlet (LDvar (_, e)) when e_ghost e ->
        []
    | PDlet (LDvar (pv, e)) when pv.pv_ghost ->
        if eff_pure e.e_effect then []
        else let unit_ = create_pvsymbol (id_fresh "()") ity_unit in
          [Mltree.Dlet (Mltree.Lvar (unit_, expr info Stv.empty e))]
    | PDlet (LDvar (pv, e)) ->
        [Mltree.Dlet (Mltree.Lvar (pv, expr info Stv.empty e))]
690
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
691
        []
Mário Pereira's avatar
Mário Pereira committed
692
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cany})) ->
693 694 695
        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))]
696 697 698 699
    | 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, []))]
700
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
701 702
        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
703 704 705 706 707
        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
708 709
        let e = fun_expr_of_mask cty.cty_mask e in
        [Mltree.Dlet (Mltree.Lsym (rs, res, args, e))]
710
    | PDlet (LDrec rl) ->
711 712 713 714 715 716 717 718 719
        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
720
          let e = fun_expr_of_mask rs1.rs_cty.cty_mask (expr info svar e) in
721 722 723 724
          { 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))]
725
    | PDlet (LDsym _) | PDpure ->
726
        []
727
    | PDtype itl ->
728 729
        let itsd = List.map tdef itl in
        [Mltree.Dtype itsd]
730
    | PDexn xs ->
731 732
        if ity_equal xs.xs_ity ity_unit || xs.xs_mask = MaskGhost then
          [Mltree.Dexn (xs, None)]
733
        else [Mltree.Dexn (xs, Some (mlty_of_ity xs.xs_mask xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
734

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

739 740 741 742 743 744 745 746 747 748 749
  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
750
    | Uscope (_, l) -> List.for_all empty_munit l
751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769
    | 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
770 771 772 773
  (* unit module declarations *)
  let rec mdecl pids info = function
    | Udecl pd -> pdecl pids info pd
    | Uscope (_, ([Uuse _] | [Uclone _])) -> []
774
    | Uscope (s, dl) -> let dl = List.concat (List.map (mdecl pids info) dl) in
775
        [Mltree.Dmodule (s, dl)]
Mário Pereira's avatar
Mário Pereira committed
776
    | Uuse _ | Uclone _ | Umeta _ -> []
777 778 779 780

  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
781
  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
782
  let module_ m =
783
    let from = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in
784 785 786
    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
787
    let add_decl known_map decl = let idl = ML.get_decl_name decl in
Mário Pereira's avatar
Mário Pereira committed
788
      List.fold_left (ML.add_known_decl decl) known_map idl in