compile.ml 37.4 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 74 75 76 77
    | Dalias ty -> iter_deps_ty f ty

  let iter_deps_its_defn f its_d =
    Opt.iter (iter_deps_typedef f) its_d.its_def

Mário Pereira's avatar
Mário Pereira committed
78 79 80 81 82 83 84 85 86 87 88 89 90
  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) ->
91 92
        f ls.ls_name;
        iter_deps_pat_list f patl
Mário Pereira's avatar
Mário Pereira committed
93 94
    | Ptuple patl -> iter_deps_pat_list f patl
    | Por (p1, p2) ->
95 96
        iter_deps_pat f p1;
        iter_deps_pat f p2
Mário Pereira's avatar
Mário Pereira committed
97 98 99
    | Pas (p, _) -> iter_deps_pat f p

  and iter_deps_expr f e = match e.e_node with
Mário Pereira's avatar
Mário Pereira committed
100
    | Econst _ | Evar _ | Eabsurd | Ehole -> ()
Mário Pereira's avatar
Mário Pereira committed
101
    | Eapp (rs, exprl) ->
102
        f rs.rs_name; List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
103
    | Efun (args, e) ->
104 105
        List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
        iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
106
    | Elet (Lvar (_, e1), e2) ->
107 108
        iter_deps_expr f e1;
        iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
109
    | Elet (Lsym (_, ty_result, args, e1), e2) ->
110 111 112 113
        iter_deps_ty f ty_result;
        List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
        iter_deps_expr f e1;
        iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
114
    | Elet (Lany (_, ty_result, args), e2) ->
115 116 117
        iter_deps_ty f ty_result;
        List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
        iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
118
    | Elet ((Lrec rdef), e) ->
119 120 121 122 123
        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
124
    | Ematch (e, branchl) ->
125 126
        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
127
    | Eif (e1, e2, e3) ->
128 129 130
        iter_deps_expr f e1;
        iter_deps_expr f e2;
        iter_deps_expr f e3
Mário Pereira's avatar
Mário Pereira committed
131
    | Eblock exprl ->
132
        List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
133
    | Ewhile (e1, e2) ->
134 135
        iter_deps_expr f e1;
        iter_deps_expr f e2
Mário Pereira's avatar
Mário Pereira committed
136
    | Efor (_, _, _, _, e) ->
137
        iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
138
    | Eraise (xs, None) ->
139
        f xs.xs_name
Mário Pereira's avatar
Mário Pereira committed
140
    | Eraise (xs, Some e) ->
141 142
        f xs.xs_name;
        iter_deps_expr f e
143
    | Eexn (_xs, None, e) -> (* FIXME? How come we never do binding here? *)
144
        iter_deps_expr f e
145
    | Eexn (_xs, Some ty, e) -> (* FIXME? How come we never do binding here? *)
146 147
        iter_deps_ty f ty;
        iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
148
    | Etry (e, xbranchl) ->
149 150
        iter_deps_expr f e;
        List.iter (iter_deps_xbranch f) xbranchl
Mário Pereira's avatar
Mário Pereira committed
151
    | Eassign assingl ->
152
        List.iter (fun (_, rs, _) -> f rs.rs_name) assingl
Mário Pereira's avatar
Mário Pereira committed
153
    | Eignore e -> iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
154

155
  let rec iter_deps f = function
Mário Pereira's avatar
Mário Pereira committed
156
    | Dtype its_dl ->
157
        List.iter (iter_deps_its_defn f) its_dl
Mário Pereira's avatar
Mário Pereira committed
158
    | Dlet (Lsym (_rs, ty_result, args, e)) ->
159 160 161
        iter_deps_ty f ty_result;
        iter_deps_args f args;
        iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
162
    | Dlet (Lany (_rs, ty_result, args)) ->
163 164
        iter_deps_ty f ty_result;
        iter_deps_args f args
Mário Pereira's avatar
Mário Pereira committed
165
    | Dlet (Lrec rdef) ->
166 167 168 169
        List.iter
          (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
             f rs.rs_name; iter_deps_args f args;
             iter_deps_expr f e; iter_deps_ty f res) rdef
Mário Pereira's avatar
Mário Pereira committed
170 171 172
    | Dlet (Lvar (_, e)) -> iter_deps_expr f e
    | Dexn (_, None) -> ()
    | Dexn (_, Some ty) -> iter_deps_ty f ty
173
    | Dmodule (_, dl) -> List.iter (iter_deps f) dl
174

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

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

Mário Pereira's avatar
Mário Pereira committed
180 181 182 183 184 185
  let ity_int  = I Ity.ity_int
  let ity_unit = I Ity.ity_unit

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

187 188
  let enope = Eblock []

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

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

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

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

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

  let var_defn pv e =
    Lvar (pv, e)

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

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

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

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

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

221
  let e_if e1 e2 e3 =
Mário Pereira's avatar
Mário Pereira committed
222
    mk_expr (Mltree.Eif (e1, e2, e3)) e2.e_ity
223 224 225 226 227 228 229

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

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

230 231 232 233 234
  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

235 236 237 238 239 240 241 242 243 244 245
  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
246

247
end
Mário Pereira's avatar
Mário Pereira committed
248 249 250 251 252

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
253 254 255
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
256

Mário Pereira's avatar
Mário Pereira committed
257 258 259
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

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

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

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

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

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

Mário Pereira's avatar
Mário Pereira committed
295
  let rec pat m p = match p.pat_node with
296
    | Pwild ->
297
        Mltree.Pwild
298
    | Pvar vs when (restore_pv vs).pv_ghost ->
299
        Mltree.Pwild
300
    | Pvar vs ->
301
        Mltree.Pident vs.vs_name
302
    | Por (p1, p2) ->
303
        Mltree.Por (pat m p1, pat m p2)
304
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
305
        pat m p
306
    | Pas (p, vs) ->
307
        Mltree.Pas (pat m p, vs.vs_name)
308
    | Papp (ls, pl) when is_fs_tuple ls ->
309 310 311 312 313
        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
314
    | Papp (ls, pl) ->
315 316 317 318 319
        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)
320

Mário Pereira's avatar
Mário Pereira committed
321 322
  (** programs *)

323 324
  let pv_name pv = pv.pv_vs.vs_name

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

341 342
  let ty_int = mlty_of_ity MaskVisible ity_int

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

348 349 350
  (* let for_direction = function *)
  (*   | To -> Mltree.To *)
  (*   | DownTo -> Mltree.DownTo *)
351

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

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

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

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

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

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

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

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

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

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

647
  and ebranch info svar ({pp_pat = p; pp_mask = m}, e) =
Mário Pereira's avatar
Mário Pereira committed
648 649 650
    (* 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 *)
651
    if e.e_effect.eff_ghost then (pat m p, ML.e_unit)
652
    else (pat m p, expr info svar e)
653

654
  (* type declarations/definitions *)
Mário Pereira's avatar
Mário Pereira committed
655
  let tdef itd =
656
    let s = itd.itd_its in
657
    let ddata_constructs = (* point-free *)
Mário Pereira's avatar
Mário Pereira committed
658
      List.map (fun ({rs_cty = cty} as rs) ->
659
          rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
660
          let args = List.filter pv_not_ghost cty.cty_args in
661 662
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
663
    let drecord_fields ({rs_cty = cty} as rs) =
664
      (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields),
Mário Pereira's avatar
Mário Pereira committed
665
      rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
666
      mlty_of_ity cty.cty_mask cty.cty_result
667 668 669 670
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
671
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
672
      | NoDef, [], [] ->
673
          ML.mk_its_defn id args is_private None
674
      | NoDef, cl, [] ->
675 676
          let cl = ddata_constructs cl in
          ML.mk_its_defn id args is_private (Some (Mltree.Ddata cl))
677
      | NoDef, _, pjl ->
678 679 680 681 682 683 684 685 686 687
          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
688
      | Alias t, _, _ ->
689
          ML.mk_its_defn id args is_private (* FIXME? is this a good mask? *)
690
            (Some (Mltree.Dalias (mlty_of_ity MaskVisible t)))
691 692 693 694
      | Range _, [], [] ->
          assert (args = []); (* a range type is not polymorphic *)
          ML.mk_its_defn id [] is_private (Some (Mltree.Dalias ty_int))
      | Range _, _, _ -> assert false (* a range type has no field/constructor *)
695
      | Float _, _, _ -> assert false (* TODO *)
696
    end
Mário Pereira's avatar
Mário Pereira committed
697

698
  (* exception ExtractionVal of rsymbol *)
Mário Pereira's avatar
Mário Pereira committed
699

Mário Pereira's avatar
Mário Pereira committed
700 701 702 703
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
704 705 706
  let rec fun_expr_of_mask mask e =
    let open Mltree in
    let mk_e e_node = { e with e_node = e_node } in
707
    (* assert (mask <> MaskGhost); *)
Mário Pereira's avatar
Mário Pereira committed
708 709 710 711
    match e.e_node with
    | Econst _ | Evar _   | Efun _ | Eassign _ | Ewhile _
    | Efor   _ | Eraise _ | Eexn _ | Eabsurd   | Ehole    -> e
    | Eapp (rs, el) when is_rs_tuple rs ->
712 713 714 715
        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
716 717
    | Eapp _ -> e
    | Elet (let_def, ein) -> let ein = fun_expr_of_mask mask ein in
718
        mk_e (Elet (let_def, ein))
Mário Pereira's avatar
Mário Pereira committed
719
    | Eif (e1, e2, e3) ->
720 721 722
        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
723
    | Ematch (e1, pel) ->
724 725
        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
726 727
    | Eblock [] -> e
    | Eblock el -> let (e_block, e_last) = Lists.chop_last el in
728 729
        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
730
    | Etry (e1, xspvel) ->
731 732
        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
733
    | Eignore ee ->
734 735
        let ee = fun_expr_of_mask mask ee in
        mk_e (Eignore ee)
Mário Pereira's avatar
Mário Pereira committed
736

737 738
  (* pids: identifiers from cloned modules without definitions *)
  let pdecl _pids info pd =
Mário Pereira's avatar
Mário Pereira committed
739
    match pd.pd_node with
740
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
741
        []
Mário Pereira's avatar
Mário Pereira committed
742
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cany})) ->
743 744 745
        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))]
746 747 748 749
    | 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
750
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
751 752
        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
753 754 755 756 757