compile.ml 32 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

(*
  - suggest a command line to compile the extracted code
    (for instance in a comment)

  - extract file f.mlw into OCaml file f.ml, with sub-modules

  - "use (im|ex)port" -> "open"
    but OCaml's open is not transitive, so requires some extra work
    to figure out all the opens

  - if a WhyML module M is extracted to something that is a signature,
    then extract "module type B_sig = ..." (as well as "module B = ...")
*)

(** Abstract syntax of ML *)

open Ident
open Ity
Mário Pereira's avatar
Mário Pereira committed
30
open Ty
Mário Pereira's avatar
Mário Pereira committed
31
open Term
32

Mário Pereira's avatar
Mário Pereira committed
33 34 35 36 37 38 39 40
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
41
  let fname = match fname, path with
Mário Pereira's avatar
Mário Pereira committed
42 43 44 45 46
    | None, "why3"::_ -> "why3"
    | None, _   -> String.concat "__" path
    | Some f, _ -> clean_name f in
  fname ^ "__" ^ t

47 48
module ML = struct

49 50
  open Expr

51
  type ty =
52
    | Tvar    of tvsymbol
53 54 55
    | Tapp    of ident * ty list
    | Ttuple  of ty list

56 57 58
  type is_ghost = bool

  type var = ident * ty * is_ghost
59

Mário Pereira's avatar
Mário Pereira committed
60 61
  type for_direction = To | DownTo

62 63 64
  type pat =
    | Pwild
    | Pident  of ident
Mário Pereira's avatar
Mário Pereira committed
65
    | Papp    of lsymbol * pat list
66 67 68 69 70 71 72 73
    | Ptuple  of pat list
    | Por     of pat * pat
    | Pas     of pat * ident

  type is_rec = bool

  type binop = Band | Bor | Beq

74
  type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *)
75

76
  type expr = {
Mário Pereira's avatar
Mário Pereira committed
77 78 79
    e_node   : expr_node;
    e_ity    : ity;
    e_effect : effect;
80
    (* TODO: add the set of free variables? *)
81 82 83 84
  }

  and expr_node =
    | Econst  of Number.integer_constant
85
    | Evar    of pvsymbol
86
    | Eapp    of rsymbol * expr list
87
    | Efun    of var list * expr
Mário Pereira's avatar
Mário Pereira committed
88
    | Elet    of let_def * expr
89
    | Eif     of expr * expr * expr
Mário Pereira's avatar
Mário Pereira committed
90
    (* | Ecast   of expr * ty *)
Mário Pereira's avatar
Mário Pereira committed
91
    | Eassign of (pvsymbol * rsymbol * pvsymbol) list
92 93 94
    | Ematch  of expr * (pat * expr) list
    | Eblock  of expr list
    | Ewhile  of expr * expr
Mário Pereira's avatar
Mário Pereira committed
95 96
    (* For loop for Why3's type int *)
    | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
Mário Pereira's avatar
Mário Pereira committed
97 98
    | Eraise  of xsymbol * expr option
    | Etry    of expr * (xsymbol * pvsymbol list * expr) list
Mário Pereira's avatar
Mário Pereira committed
99
    | Eignore of expr
100
    | Eabsurd
Mário Pereira's avatar
Mário Pereira committed
101
    | Ehole
102
    (* | Eany *)
103

Mário Pereira's avatar
Mário Pereira committed
104 105
  and let_def =
    | Lvar of pvsymbol * expr
Mário Pereira's avatar
Mário Pereira committed
106
    | Lsym of rsymbol * ty * var list * expr
Mário Pereira's avatar
Mário Pereira committed
107 108 109 110 111 112 113
    | Lrec of rdef list

  and rdef = {
    rec_sym  : rsymbol; (* exported *)
    rec_rsym : rsymbol; (* internal *)
    rec_args : var list;
    rec_exp  : expr;
Mário Pereira's avatar
Mário Pereira committed
114
    rec_res  : ty;
Mário Pereira's avatar
Mário Pereira committed
115 116
  }

117 118 119 120 121 122 123
  type is_mutable = bool

  type typedef =
    | Ddata     of (ident * ty list) list
    | Drecord   of (is_mutable * ident * ty) list
    | Dalias    of ty

124 125 126 127 128 129 130
  type its_defn = {
    its_name    : ident;
    its_args    : tvsymbol list;
    its_private : bool;
    its_def     : typedef option;
  }

131
  type decl =
Mario Pereira's avatar
Mario Pereira committed
132
    | Dtype   of its_defn list
Mário Pereira's avatar
Mário Pereira committed
133
    | Dlet    of let_def
Mario Pereira's avatar
Mario Pereira committed
134
    | Dexn    of xsymbol * ty option
135 136 137 138
    | Dclone  of ident * decl list
(*
    | Dfunctor of ident * (ident * decl list) list * decl list
*)
Mario Pereira's avatar
Mario Pereira committed
139

Mário Pereira's avatar
Mário Pereira committed
140 141
  type known_map = decl Mid.t

142 143 144 145 146
  type from_module = {
    from_mod: Pmodule.pmodule option;
    from_km : Pdecl.known_map;
  }

Mário Pereira's avatar
Mário Pereira committed
147
  type pmodule = {
148
    mod_from  : from_module;
Mário Pereira's avatar
Mário Pereira committed
149 150 151 152
    mod_decl  : decl list;
    mod_known : known_map;
  }

Mário Pereira's avatar
Mário Pereira committed
153 154 155
  let get_decl_name = function
    | Dtype itdefl -> List.map (fun {its_name = id} -> id) itdefl
    | Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
156 157 158
    | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
    | Dlet (Lsym ({rs_name=id}, _, _, _))
    | Dexn ({xs_name=id}, _) -> [id]
159
    | Dclone _ -> [] (* FIXME? *)
Mário Pereira's avatar
Mário Pereira committed
160 161

  let add_known_decl decl k_map id =
Mário Pereira's avatar
Mário Pereira committed
162 163
    Mid.add id decl k_map

Mário Pereira's avatar
Mário Pereira committed
164 165
  let rec iter_deps_ty f = function
    | Tvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
166
    | Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
Mário Pereira's avatar
Mário Pereira committed
167 168 169
    | 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
170 171
    | Ddata constrl ->
      List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
Mário Pereira's avatar
Mário Pereira committed
172
    | Drecord pjl -> List.iter (fun (_, _, ty) -> iter_deps_ty f ty) pjl
Mário Pereira's avatar
Mário Pereira committed
173 174 175 176 177
    | 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
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
  let iter_deps_args f =
    List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg)

  let rec iter_deps_xbranch f (xs, _, e) =
    f xs.xs_name;
    iter_deps_expr f e

  and iter_deps_pat_list f patl =
    List.iter (iter_deps_pat f) patl

  and iter_deps_pat f = function
    | Pwild | Pident _ -> ()
    | Papp (ls, patl) ->
      f ls.ls_name;
      iter_deps_pat_list f patl
    | Ptuple patl -> iter_deps_pat_list f patl
    | Por (p1, p2) ->
      iter_deps_pat f p1;
      iter_deps_pat f p2
    | Pas (p, _) -> iter_deps_pat f p

  and iter_deps_expr f e = match e.e_node with
Mário Pereira's avatar
Mário Pereira committed
200
    | Econst _ | Evar _ | Eabsurd | Ehole -> ()
Mário Pereira's avatar
Mário Pereira committed
201 202
    | Eapp (rs, exprl) ->
      f rs.rs_name; List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
203 204 205
    | Efun (args, e) ->
      List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
      iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243
    | Elet (Lvar (_, e1), e2) ->
      iter_deps_expr f e1;
      iter_deps_expr f e2
    | Elet (Lsym (_, ty_result, args, e1), e2) ->
      iter_deps_ty f ty_result;
      List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
      iter_deps_expr f e1;
      iter_deps_expr f e2
    | Elet ((Lrec rdef), e) ->
      List.iter
        (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
           f rs.rs_name; iter_deps_args f args;
           iter_deps_expr f e; iter_deps_ty f res) rdef;
      iter_deps_expr f e
    | Ematch (e, branchl) ->
      iter_deps_expr f e;
      List.iter (fun (p, e) -> iter_deps_pat f p; iter_deps_expr f e) branchl
    | Eif (e1, e2, e3) ->
      iter_deps_expr f e1;
      iter_deps_expr f e2;
      iter_deps_expr f e3
    | Eblock exprl ->
      List.iter (iter_deps_expr f) exprl
    | Ewhile (e1, e2) ->
      iter_deps_expr f e1;
      iter_deps_expr f e2
    | Efor (_, _, _, _, e) ->
      iter_deps_expr f e
    | Eraise (xs, None) ->
      f xs.xs_name
    | Eraise (xs, Some e) ->
      f xs.xs_name;
      iter_deps_expr f e
    | Etry (e, xbranchl) ->
      iter_deps_expr f e;
      List.iter (iter_deps_xbranch f) xbranchl
    | Eassign assingl ->
      List.iter (fun (_, rs, _) -> f rs.rs_name) assingl
Mário Pereira's avatar
Mário Pereira committed
244
    | Eignore e -> iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
245

246
  let rec iter_deps f = function
Mário Pereira's avatar
Mário Pereira committed
247 248
    | Dtype its_dl ->
      List.iter (iter_deps_its_defn f) its_dl
Mário Pereira's avatar
Mário Pereira committed
249 250 251 252 253 254 255 256 257
    | Dlet (Lsym (_rs, ty_result, args, e)) ->
      iter_deps_ty f ty_result;
      iter_deps_args f args;
      iter_deps_expr f e
    | Dlet (Lrec rdef) ->
      List.iter
        (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
           f rs.rs_name; iter_deps_args f args;
           iter_deps_expr f e; iter_deps_ty f res) rdef
Mário Pereira's avatar
Mário Pereira committed
258 259 260
    | Dlet (Lvar (_, e)) -> iter_deps_expr f e
    | Dexn (_, None) -> ()
    | Dexn (_, Some ty) -> iter_deps_ty f ty
261
    | Dclone (_, dl) -> List.iter (iter_deps f) dl
262

263
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
264 265
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

266
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
267
  let mk_let_var pv e1 e2 =
Mário Pereira's avatar
Mário Pereira committed
268
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
269 270

  let tunit = Ttuple []
271

Mário Pereira's avatar
Mário Pereira committed
272 273 274 275 276 277
  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
278

279 280 281 282 283
  let enope = Eblock []

  let mk_unit =
    mk_expr enope (I Ity.ity_unit) Ity.eff_empty

Mário Pereira's avatar
Mário Pereira committed
284 285 286
  let mk_hole =
    mk_expr Ehole (I Ity.ity_unit) Ity.eff_empty

287 288
  let mk_var id ty ghost = (id, ty, ghost)

289 290
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

291
  let mk_its_defn id args private_ def =
Mário Pereira's avatar
Mário Pereira committed
292 293
    { its_name    = id      ; its_args = args;
      its_private = private_; its_def  = def; }
294

Mário Pereira's avatar
Mário Pereira committed
295 296 297 298
  let mk_ignore e =
    if is_unit e.e_ity then e
    else { e_node = Eignore e; e_effect = e.e_effect; e_ity = ity_unit }

299 300
  let eseq e1 e2 =
    match e1.e_node, e2.e_node with
Mário Pereira's avatar
Mário Pereira committed
301
    | (Eblock [] | Ehole), e | e, (Eblock [] | Ehole) -> e
302 303 304 305 306
    | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
    | _, Eblock e2 -> Eblock (e1 :: e2)
    | Eblock e1, _ -> Eblock (e1 @ [e2])
    | _ -> Eblock [e1; e2]

307
end
Mário Pereira's avatar
Mário Pereira committed
308 309 310 311 312

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
313 314 315
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
316

Mário Pereira's avatar
Mário Pereira committed
317 318 319
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
320 321 322 323
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
324
       ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
325 326 327 328 329 330 331 332
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
       ML.Ttuple (List.map type_ tyl)
    | Tyapp (ts, tyl) ->
       ML.Tapp (ts.ts_name, List.map type_ tyl)

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

333 334 335
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

Mário Pereira's avatar
Mário Pereira committed
336 337 338 339 340
  let rec filter_ghost_params p def = function
    | [] -> []
    | pv :: l ->
      if p pv then def pv :: (filter_ghost_params p def l)
      else filter_ghost_params p def l
341 342 343 344 345 346 347 348 349 350 351 352

  let filter2_ghost_params p def al l =
    let rec filter2_ghost_params_cps l k =
      match l with
      | []  -> k []
      | [e] -> k (if p e then [def e] else [al e])
      | e :: r ->
        filter2_ghost_params_cps r
          (fun fr -> k (if p e then (def e) :: fr else fr))
    in
    filter2_ghost_params_cps l (fun x -> x)

Mário Pereira's avatar
Mário Pereira committed
353 354 355 356 357 358
  let rec filter_ghost_rdef def = function
    | [] -> []
    | { rec_sym = rs; rec_rsym = rrs } :: l
      when rs_ghost rs || rs_ghost rrs -> filter_ghost_rdef def l
    | rdef :: l -> def rdef :: filter_ghost_rdef def l

359 360 361
  let rec pat p =
    match p.pat_node with
    | Pwild ->
362
      ML.Pwild
363 364
    | Pvar vs when (restore_pv vs).pv_ghost ->
      ML.Pwild
365
    | Pvar vs ->
366
      ML.Pident vs.vs_name
367
    | Por (p1, p2) ->
368
      ML.Por (pat p1, pat p2)
369 370
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
      pat p
371
    | Pas (p, vs) ->
372
      ML.Pas (pat p, vs.vs_name)
373
    | Papp (ls, pl) when is_fs_tuple ls ->
374
      ML.Ptuple (List.map pat pl)
375
    | Papp (ls, pl) ->
376 377
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
378 379
      let mk acc pv pp = if not pv.pv_ghost then pat pp :: acc else acc in
      let pat_pl = List.fold_left2 mk [] args pl in
Mário Pereira's avatar
Mário Pereira committed
380
      ML.Papp (ls, List.rev pat_pl)
381

Mário Pereira's avatar
Mário Pereira committed
382 383
  (** programs *)

384 385
  let pv_name pv = pv.pv_vs.vs_name

386 387 388
  (* individual types *)
  let rec ity t =
    match t.ity_node with
389
    | Ityvar (tvs, _) ->
390
      ML.Tvar tvs
391
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
392
      ML.Ttuple (List.map ity itl)
393
    | Ityapp ({its_ts = ts}, itl, _) ->
394 395 396 397
      ML.Tapp (ts.ts_name, List.map ity itl)
    | Ityreg {reg_its = its; reg_args = args} ->
      let args = List.map ity args in
      ML.Tapp (its.its_ts.ts_name, args)
Mário Pereira's avatar
Mário Pereira committed
398

Mário Pereira's avatar
Mário Pereira committed
399
  let pvty pv =
400 401 402 403 404
    if pv.pv_ghost then
      ML.mk_var (pv_name pv) ML.tunit true
    else
      let (vs, vs_ty) = vsty pv.pv_vs in
      ML.mk_var vs vs_ty false
Mário Pereira's avatar
Mário Pereira committed
405

406 407 408 409
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
410
  let isconstructor info rs =
411
    match Mid.find_opt rs.rs_name info.ML.from_km with
Mário Pereira's avatar
Mário Pereira committed
412 413 414 415 416 417
    | Some {pd_node = PDtype its} ->
      let is_constructor its =
        List.exists (rs_equal rs) its.itd_constructors in
      List.exists is_constructor its
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
418 419 420 421 422 423 424 425 426
  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
    let pv_equal_field rs = pv_equal (Opt.get rs.rs_field) in
    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
427

428
  let get_record_itd info rs =
429
    match Mid.find_opt rs.rs_name info.ML.from_km with
Mário Pereira's avatar
Mário Pereira committed
430 431
    | Some {pd_node = PDtype itdl} ->
      let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
432
      let itd = match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
433
        | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449
        | None -> List.find (fun itd -> f itd.itd_constructors) itdl in
      if itd.itd_fields = [] then None else Some itd
    | _ -> None

  let is_optimizable_record_itd itd =
    not itd.itd_its.its_private && is_singleton_imutable itd

  let is_optimizable_record_rs info rs =
    Opt.fold (fun _ -> is_optimizable_record_itd) false (get_record_itd info rs)

  let is_empty_record_itd itd =
    let is_ghost rs = rs_ghost rs in
    List.for_all is_ghost itd.itd_fields

  let is_empty_record info rs =
    Opt.fold (fun _ -> is_empty_record_itd) false (get_record_itd info rs)
Mário Pereira's avatar
Mário Pereira committed
450

Mário Pereira's avatar
Mário Pereira committed
451
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
452 453 454 455 456
    (* FIXME : effects and types of the expression in this situation *)
    let args_f =
      let def pv = pv_name pv, ity pv.pv_ity, pv.pv_ghost in
      filter_ghost_params pv_not_ghost def cty_app.cty_args in
    let args =
457
      let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
Mário Pereira's avatar
Mário Pereira committed
458 459 460 461 462 463 464 465 466
      let args = filter_ghost_params pv_not_ghost def pvl in
      let extra_args =
        (* FIXME : ghost status in this extra arguments *)
        List.map def cty_app.cty_args in
      args @ extra_args in
    let eapp =
      ML.mk_expr (ML.Eapp (rsc, args)) (ML.C cty_app) cty_app.cty_effect in
    ML.mk_expr (ML.Efun (args_f, eapp)) (ML.C cty_app) cty_app.cty_effect

467 468 469 470 471 472
  (* 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
473 474 475 476
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
      if args = [] then [ML.mk_var_unit ()] else args
477

Mário Pereira's avatar
Mário Pereira committed
478 479
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
480
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
481 482 483 484 485 486 487 488 489 490
      | pv :: l1, arg :: l2 ->
        if p pv && p arg then def pv :: loop (l1, l2)
        else loop (l1, l2)
      | _ -> assert false
    in loop (pvl, cty_args)

  let app pvl cty_args =
    let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
    filter_params_cty pv_not_ghost def pvl cty_args

Mário Pereira's avatar
Mário Pereira committed
491
  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
492 493 494 495 496 497
    let i_expr, from_expr, to_expr =
      let int_ity = ML.ity_int in let eff_e = eff_empty in
      ML.mk_expr (ML.Evar i_pv)     int_ity eff_e,
      ML.mk_expr (ML.Evar from_pv)  int_ity eff_e,
      ML.mk_expr (ML.Evar to_pv)    int_ity eff_e in
    let for_rs    =
Mário Pereira's avatar
Mário Pereira committed
498
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
499
      let for_cty = create_cty [i_pv] [] [] Mxs.empty
Mário Pereira's avatar
Mário Pereira committed
500
                               Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
501 502 503
      create_rsymbol for_id for_cty in
    let for_expr =
      let test = ML.mk_expr (ML.Eapp (op_b_rs, [i_expr; to_expr]))
Mário Pereira's avatar
Mário Pereira committed
504 505
                            (ML.I ity_bool) eff_empty in
      let next_expr =
Mário Pereira's avatar
Mário Pereira committed
506
        let one_const = Number.int_const_dec "1" in
Mário Pereira's avatar
Mário Pereira committed
507
        let one_expr  =
Mário Pereira's avatar
Mário Pereira committed
508
          ML.mk_expr (ML.Econst one_const) ML.ity_int eff_empty in
Mário Pereira's avatar
Mário Pereira committed
509 510
        let i_op_one = ML.Eapp (op_a_rs, [i_expr; one_expr]) in
        ML.mk_expr i_op_one ML.ity_int eff_empty in
Mário Pereira's avatar
Mário Pereira committed
511
       let rec_call  =
Mário Pereira's avatar
Mário Pereira committed
512
        ML.mk_expr (ML.Eapp (for_rs, [next_expr]))
Mário Pereira's avatar
Mário Pereira committed
513
                    ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
514
      let seq_expr =
Mário Pereira's avatar
Mário Pereira committed
515
        ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
516 517
      ML.mk_expr (ML.Eif (test, seq_expr, ML.mk_unit)) ML.ity_unit eff in
    let ty_int = ity ity_int in
Mário Pereira's avatar
Mário Pereira committed
518
    let for_call_expr   =
Mário Pereira's avatar
Mário Pereira committed
519
      let for_call      = ML.Eapp (for_rs, [from_expr]) in
Mário Pereira's avatar
Mário Pereira committed
520 521
      ML.mk_expr for_call ML.ity_unit eff in
    let pv_name pv = pv.pv_vs.vs_name in
Mário Pereira's avatar
Mário Pereira committed
522
    let args = [ pv_name  i_pv, ty_int, false ] in
Mário Pereira's avatar
Mário Pereira committed
523
    let for_rec_def = {
Mário Pereira's avatar
Mário Pereira committed
524 525
      ML.rec_sym  = for_rs; ML.rec_args = args;
      ML.rec_rsym = for_rs; ML.rec_exp  = for_expr;
Mário Pereira's avatar
Mário Pereira committed
526
      ML.rec_res  = ML.tunit;
Mário Pereira's avatar
Mário Pereira committed
527
    } in
Mário Pereira's avatar
Mário Pereira committed
528
    let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
529 530 531 532
    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 =
533
      let ns = (Opt.get info.ML.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
534 535 536 537 538
      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 =
539
      let ns = (Opt.get info.ML.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
540 541 542
      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

Mário Pereira's avatar
Mário Pereira committed
543 544
  exception ExtractionAny

Mário Pereira's avatar
Mário Pereira committed
545
  (* expressions *)
546
  let rec expr info ({e_effect = eff} as e) =
Mário Pereira's avatar
Mário Pereira committed
547
    assert (not eff.eff_ghost);
Mário Pereira's avatar
Mário Pereira committed
548
    match e.e_node with
549
    | Econst c ->
Mário Pereira's avatar
Mário Pereira committed
550 551
      let c = match c with Number.ConstInt c -> c | _ -> assert false in
      ML.mk_expr (ML.Econst c) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
552 553
    | Evar pv ->
      ML.mk_expr (ML.Evar pv) (ML.I e.e_ity) eff
554
    | Elet (LDvar (_, e1), e2) when e_ghost e1 ->
Mário Pereira's avatar
Mário Pereira committed
555
      expr info e2
556 557
    | Elet (LDvar (_, e1), e2) when e_ghost e2 ->
      ML.mk_expr (ML.eseq (expr info e1) ML.mk_unit) ML.ity_unit eff
Mário Pereira's avatar
Mário Pereira committed
558 559 560 561 562
    | Elet (LDvar (pv, e1), e2)
      when pv.pv_ghost || not (Mpv.mem pv e2.e_effect.eff_reads) ->
      if eff_pure e1.e_effect then expr info e2
      else let e1 = ML.mk_ignore (expr info e1) in
        ML.mk_expr (ML.eseq e1 (expr info e2)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
563 564
    | Elet (LDvar (pv, e1), e2) ->
      let ml_let = ML.mk_let_var pv (expr info e1) (expr info e2) in
565 566
      ML.mk_expr ml_let (ML.I e.e_ity) eff
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
567
      let args = params cty.cty_args in
568 569
      let ef = expr info ef in
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
570 571
      let res = ity cty.cty_result in
      let ml_letrec = ML.Elet (ML.Lsym (rs, res, args, ef), ein) in
572
      ML.mk_expr ml_letrec (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
573 574
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein)
      when isconstructor info rs_app ->
Mário Pereira's avatar
Mário Pereira committed
575 576
      (* partial application of constructor *)
      let eta_app = mk_eta_expansion rs_app pvl cty in
Mário Pereira's avatar
Mário Pereira committed
577
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
578 579 580
      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 = ity func in
Mário Pereira's avatar
Mário Pereira committed
581
      let ml_letrec = ML.Elet (ML.Lsym (rsf, res, [], eta_app), ein) in
Mário Pereira's avatar
Mário Pereira committed
582 583
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
584
      (* partial application *)
Mário Pereira's avatar
Mário Pereira committed
585
      let pvl = app pvl rs_app.rs_cty.cty_args in
586
      let eapp =
Mário Pereira's avatar
Mário Pereira committed
587
        ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
Mário Pereira's avatar
Mário Pereira committed
588 589
      let ein  = expr info ein in
      let res  = ity cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
590
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
591
      let ml_letrec = ML.Elet (ML.Lsym (rsf, res, args, eapp), ein) in
Mário Pereira's avatar
Mário Pereira committed
592 593 594 595
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
    | Elet (LDrec rdefl, ein) ->
      let ein = expr info ein in
      let rdefl =
Mário Pereira's avatar
Mário Pereira committed
596
        List.map (fun rdef -> match rdef with
Mário Pereira's avatar
Mário Pereira committed
597 598
          | {rec_sym = rs1; rec_rsym = rs2;
             rec_fun = {c_node = Cfun ef; c_cty = cty}} ->
Mário Pereira's avatar
Mário Pereira committed
599
            let res  = ity rs1.rs_cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
600 601
            let args = params cty.cty_args in let ef = expr info ef in
            { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
602
              ML.rec_args = args; ML.rec_exp  = ef ; ML.rec_res  = res }
Mário Pereira's avatar
Mário Pereira committed
603 604 605
          | _ -> assert false) rdefl
      in
      let ml_letrec = ML.Elet (ML.Lrec rdefl, ein) in
606
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
607 608
    | Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs ->
      ML.mk_unit
609 610
    | Eexec ({c_node = Capp (rs, _)}, _) when is_empty_record info rs ->
      ML.mk_unit
611 612
    | Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
      ML.mk_unit
Mário Pereira's avatar
Mário Pereira committed
613
    | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
Mário Pereira's avatar
Mário Pereira committed
614 615
      when isconstructor info rs && cty.cty_args <> [] ->
      (* partial application of constructors *)
Mário Pereira's avatar
Mário Pereira committed
616
      mk_eta_expansion rs pvl cty
Mário Pereira's avatar
Mário Pereira committed
617
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
Mário Pereira's avatar
Mário Pereira committed
618
      let pvl = app pvl rs.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
619
      begin match pvl with
620
      | [pv_expr] when is_optimizable_record_rs info rs -> pv_expr
Mário Pereira's avatar
Mário Pereira committed
621 622 623 624
      | _ -> ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff end
    | Eexec ({c_node = Cfun e; c_cty = {cty_args = []}}, _) ->
      (* abstract block *)
      expr info e
625
    | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
626
      let args = params cty.cty_args in
627
      ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
628
    | Eexec ({c_node = Cany}, _) -> (* raise ExtractionAny *)
Mário Pereira's avatar
Mário Pereira committed
629
      ML.mk_hole
630
    | Eabsurd ->
631 632 633
      ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
    | Ecase (e1, _) when e_ghost e1 ->
      ML.mk_unit
634
    | Ecase (e1, pl) ->
Mário Pereira's avatar
Mário Pereira committed
635 636 637
      let e1 = expr info e1 in
      let pl = List.map (ebranch info) pl in
      ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
638
    | Eassert _ -> ML.mk_unit
639
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
640 641 642 643
      let e1 = expr info e1 in
      let e2 = expr info e2 in
      let e3 = expr info e3 in
      ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
644 645 646 647
    | Ewhile (e1, _, _, e2) ->
      let e1 = expr info e1 in
      let e2 = expr info e2 in
      ML.mk_expr (ML.Ewhile (e1, e2)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
648
    | Efor (pv1, (pv2, To, pv3), _, efor) ->
Mário Pereira's avatar
Mário Pereira committed
649
      let efor = expr info efor in
Mário Pereira's avatar
Mário Pereira committed
650 651 652 653
      mk_for_to info pv1 pv2 pv3 efor eff
    | Efor (pv1, (pv2, DownTo, pv3), _, efor) ->
      let efor = expr info efor in
      mk_for_downto info pv1 pv2 pv3 efor eff
Mário Pereira's avatar
Mário Pereira committed
654
    | Eghost _ -> assert false
655 656
    | Eassign al ->
      ML.mk_expr (ML.Eassign al) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
657
    | Epure _ -> (* assert false (\*TODO*\) *) ML.mk_hole
Mário Pereira's avatar
Mário Pereira committed
658 659 660 661 662 663
    | Etry (etry, pvl_e_map) ->
      let etry = expr info etry in
      let bl   =
        let bl_map = Mxs.bindings pvl_e_map in
        List.map (fun (xs, (pvl, e)) -> xs, pvl, expr info e) bl_map in
      ML.mk_expr (ML.Etry (etry, bl)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
664 665 666
    | Eraise (xs, ex) ->
      let ex =
        match expr info ex with
Mário Pereira's avatar
Mário Pereira committed
667
        | {ML.e_node = ML.Eblock []} -> None
Mário Pereira's avatar
Mário Pereira committed
668 669
        | e -> Some e
      in
Mário Pereira's avatar
Mário Pereira committed
670
      ML.mk_expr (ML.Eraise (xs, ex)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
671 672 673 674
    | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
    (*   assert false (\*TODO*\) *)
    | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
    (*   assert false (\*TODO*\) *)
675

Mário Pereira's avatar
Mário Pereira committed
676 677
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
678

679 680 681 682
  let its_args ts = ts.its_ts.ts_args
  let itd_name td = td.itd_its.its_ts.ts_name

  (* type declarations/definitions *)
Mário Pereira's avatar
Mário Pereira committed
683
  let tdef itd =
684
    let s = itd.itd_its in
685 686 687
    let ddata_constructs = (* point-free *)
      List.map (fun ({rs_cty = rsc} as rs) ->
          rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
688
          let args = List.filter pv_not_ghost rsc.cty_args in
689 690
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
691
    let drecord_fields ({rs_cty = rsc} as rs) =
Mário Pereira's avatar
Mário Pereira committed
692 693 694
      (List.exists (pv_equal (Opt.get rs.rs_field)) s.its_mfields),
      rs.rs_name,
      ity rsc.cty_result
695 696 697 698
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
699 700
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
701
        ML.mk_its_defn id args is_private None
702
      | None, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
703 704
        let cl = ddata_constructs cl in
        ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
705
      | None, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
706 707
        let p e = not (rs_ghost e) in
        let pjl = filter_ghost_params p drecord_fields pjl in
Mário Pereira's avatar
Mário Pereira committed
708
        begin match pjl with
709 710
          | [] -> ML.mk_its_defn id args is_private (Some (ML.Dalias ML.tunit))
          | [_, _, ty_pj] when is_optimizable_record_itd itd ->
Mário Pereira's avatar
Mário Pereira committed
711 712 713
            ML.mk_its_defn id args is_private (Some (ML.Dalias ty_pj))
          | pjl -> ML.mk_its_defn id args is_private (Some (ML.Drecord pjl))
        end
714
      | Some t, _, _ ->
715
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
716
    end
Mário Pereira's avatar
Mário Pereira committed
717

Mário Pereira's avatar
Mário Pereira committed
718
  exception ExtractionVal of rsymbol
Mário Pereira's avatar
Mário Pereira committed
719

Mário Pereira's avatar
Mário Pereira committed
720 721 722 723
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

724 725
  (* pids: identifiers from cloned modules without definitions *)
  let pdecl _pids info pd =
Mário Pereira's avatar
Mário Pereira committed
726
    match pd.pd_node with
727
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
728
      []
Mário Pereira's avatar
Mário Pereira committed
729 730 731
    | PDlet (LDsym (_rs, {c_node = Cany})) ->
      []
      (* raise (ExtractionVal _rs) *)
Mário Pereira's avatar
Mário Pereira committed
732 733
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
      []
734
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
735
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
736
      let res  = ity cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
737
      [ML.Dlet (ML.Lsym (rs, res, args, expr info e))]
738
    | PDlet (LDrec rl) ->
Mário Pereira's avatar
Mário Pereira committed
739
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
740
        let e = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
741
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
742
        let res  = ity rs1.rs_cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
743
        { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
744 745
          ML.rec_args = args; ML.rec_exp  = expr info e;
          ML.rec_res  = res } in
Mário Pereira's avatar
Mário Pereira committed
746
      let rec_def = filter_ghost_rdef def rl in
Mário Pereira's avatar
Mário Pereira committed
747 748
      [ML.Dlet (ML.Lrec rec_def)]
    | PDlet (LDsym _) | PDpure | PDlet (LDvar _) ->
749
      []
750
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
751
      let itsd = List.map tdef itl in
Mário Pereira's avatar
Mário Pereira committed
752
      [ML.Dtype itsd]
753
    | PDexn xs ->
Mário Pereira's avatar
Mário Pereira committed
754 755
      if ity_equal xs.xs_ity ity_unit then [ML.Dexn (xs, None)]
      else [ML.Dexn (xs, Some (ity xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
756

Mário Pereira's avatar
Mário Pereira committed
757
  let pdecl_m m pd =
758 759
    let info = { ML.from_mod = Some m; ML.from_km  = m.mod_known; } in
    pdecl Sid.empty info pd
Mário Pereira's avatar
Mário Pereira committed
760

Mário Pereira's avatar
Mário Pereira committed
761
  (* unit module declarations *)
762 763 764
  let rec mdecl pids info = function
    | Udecl pd -> pdecl pids info pd
    | Uscope (_, _, l) -> List.concat (List.map (mdecl pids info) l)
765
    | Uuse _ | Uclone _ | Umeta _ -> []
Mário Pereira's avatar
Mário Pereira committed
766

767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807
  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
    | Uscope (_, _, l) -> List.for_all empty_munit l
    | Uuse _ | Umeta _ -> true

  let is_empty_clone mi =
    Mts.is_empty mi.mi_ty &&
    Mts.is_empty mi.mi_ts &&
    Mls.is_empty mi.mi_ls &&
    Decl.Mpr.is_empty mi.mi_pr &&
    Decl.Mpr.is_empty mi.mi_pk &&
    Mvs.is_empty mi.mi_pv &&
    Mrs.is_empty mi.mi_rs &&
    Mxs.is_empty mi.mi_xs &&
    List.for_all empty_munit mi.mi_mod.mod_units

  let find_params dl =
    let add params = function
      | Uclone mi when is_empty_clone mi -> mi :: params
      | _ -> params in
    List.fold_left add [] dl

  let make_param from mi =
    let id = mi.mi_mod.mod_theory.Theory.th_name in
    Format.printf "param %s@." id.id_string;
    let dl =
      List.concat (List.map (mdecl Sid.empty from) mi.mi_mod.mod_units) in
    ML.Dclone (id, dl)

  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
808
  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
809
  let module_ m =
810 811 812 813 814
    let from = { ML.from_mod = Some m; ML.from_km = m.mod_known; } in
    let params = find_params m.mod_units in
    let pids = List.fold_left ids_of_params Sid.empty params in
    let mod_decl = List.concat (List.map (mdecl pids from) m.mod_units) in
    let mod_decl = List.map (make_param from) params @ mod_decl in
Mário Pereira's avatar
Mário Pereira committed
815 816 817 818
    let add known_map decl =
      let idl = ML.get_decl_name decl in
      List.fold_left (ML.add_known_decl decl) known_map idl in
    let mod_known = List.fold_left add Mid.empty mod_decl in
819
    { ML.mod_from = from; ML.mod_decl = mod_decl; ML.mod_known = mod_known }
Mário Pereira's avatar
Mário Pereira committed
820

Mário Pereira's avatar
Mário Pereira committed
821 822 823 824 825 826 827 828
  let () = Exn_printer.register (fun fmt e -> match e with
    | ExtractionAny ->
      Format.fprintf fmt "Cannot extract an undefined node"
    | ExtractionVal rs ->
      Format.fprintf fmt "Function %a cannot be extracted"
        print_rs rs
    | _ -> raise e)

Mário Pereira's avatar
Mário Pereira committed
829 830
end

831 832 833 834 835 836
(** Some transformations *)

module Transform = struct

  open ML

Mário Pereira's avatar
Mário Pereira committed
837 838 839
  let conflict_reads_writes spv spv_mreg =
    Mreg.exists (fun _ v -> not (Spv.is_empty (Spv.diff v spv))) spv_mreg

840 841
  type subst = expr Mpv.t

Mário Pereira's avatar
Mário Pereira committed
842 843 844 845 846
  let mk_list_eb ebl f =
    let mk_acc e (e_acc, s_acc) =
      let e, s = f e in e::e_acc, Spv.union s s_acc in
    List.fold_right mk_acc ebl ([], Spv.empty)

Mário Pereira's avatar
Mário Pereira committed
847
  let rec expr info subst e =
Mário Pereira's avatar
Mário Pereira committed
848
    let mk e_node = { e with e_node = e_node } in
Mário Pereira's avatar
Mário Pereira committed
849
    let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
850
    match e.e_node with
Mário Pereira's avatar
Mário Pereira committed
851 852
    | Evar pv ->
      (try Mpv.find pv subst, Spv.singleton pv with Not_found -> e, Spv.empty)
Mário Pereira's avatar
Mário Pereira committed
853
    | Elet (Lvar (pv, ({e_effect = eff1} as e1)), ({e_effect = eff2} as e2))
Mário Pereira's avatar
Mário Pereira committed
854
      when Slab.mem Expr.proxy_label pv.pv_vs.vs_name.id_label &&
Mário Pereira's avatar
Mário Pereira committed
855 856
           eff_pure eff1 &&
           not (conflict_reads_writes eff1.eff_reads eff2.eff_writes) ->
Mário Pereira's avatar
Mário Pereira committed
857 858 859 860 861 862
      let e1, s1 = expr info subst e1 in
      let e2, s2 = add_subst pv e1 e2 in
      let s_union = Spv.union s1 s2 in
      if Spv.mem pv s2 then e2, s_union (* [pv] was substituted in [e2] *)
      else (* [pv] was not substituted in [e2], e.g [e2] is an [Efun] *)
        mk (Elet (Lvar (pv, e1), e2)), s_union
863
    | Elet (ld, e) ->
Mário Pereira's avatar
Mário Pereira committed
864 865 866
      let e, spv = expr info subst e in
      let e_let, spv_let = let_def info subst ld in
      mk (Elet (e_let, e)), Spv.union spv spv_let
867
    | Eapp (rs, el) ->
Mário Pereira's avatar
Mário Pereira committed
868 869
      let e_app, spv = mk_list_eb el (expr info subst) in
      mk (Eapp (rs, e_app)), spv
870
    | Efun (vl, e) ->
Mário Pereira's avatar
Mário Pereira committed
871 872 873 874 875
      (* We begin the inlining of proxy variables in an [Efun]
         with the empty substituion. This keeps A-normal lets,
         preventing undiserable capture of variables insinde. *)
      let e, spv = expr info Mpv.empty e in
      mk (Efun (vl, e)), spv
876
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
877 878 879 880
      let e1, s1 = expr info subst e1 in
      let e2, s2 = expr info subst e2 in
      let e3, s3 = expr info subst e3 in
      mk (Eif (e1, e2, e3)), Spv.union (Spv.union s1 s2) s3
881
    | Ematch (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
882 883 884
      let e, spv = expr info subst e in
      let e_bl, spv_bl = mk_list_eb bl (branch info subst) in
      mk (Ematch (e, e_bl)), Spv.union spv spv_bl
885
    | Eblock el ->
Mário Pereira's avatar
Mário Pereira committed
886 887
      let e_app, spv = mk_list_eb el (expr info subst) in
      mk (Eblock e_app), spv
888
    | Ewhile (e1, e2) ->