compile.ml 34.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Mário Pereira's avatar
Mário Pereira committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
(*                                                                  *)
(*  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 81 82 83
  }

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

Mário Pereira's avatar
Mário Pereira committed
102 103
  and let_def =
    | Lvar of pvsymbol * expr
Mário Pereira's avatar
Mário Pereira committed
104
    | Lsym of rsymbol * ty * var list * expr
Mário Pereira's avatar
Mário Pereira committed
105 106 107 108 109 110 111
    | 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
112
    rec_res  : ty;
113
    rec_svar : Stv.t; (* set of type variables *)
Mário Pereira's avatar
Mário Pereira committed
114 115
  }

116 117 118 119 120 121 122
  type is_mutable = bool

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

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

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

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

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

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

Mário Pereira's avatar
Mário Pereira committed
152 153 154
  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
155 156 157
    | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
    | Dlet (Lsym ({rs_name=id}, _, _, _))
    | Dexn ({xs_name=id}, _) -> [id]
158
    | Dclone _ -> [] (* FIXME? *)
Mário Pereira's avatar
Mário Pereira committed
159 160

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

Mário Pereira's avatar
Mário Pereira committed
163 164
  let rec iter_deps_ty f = function
    | Tvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
165
    | Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
Mário Pereira's avatar
Mário Pereira committed
166 167 168
    | 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
169 170
    | Ddata constrl ->
      List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
Mário Pereira's avatar
Mário Pereira committed
171
    | Drecord pjl -> List.iter (fun (_, _, ty) -> iter_deps_ty f ty) pjl
Mário Pereira's avatar
Mário Pereira committed
172 173 174 175 176
    | 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
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198
  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
199
    | Econst _ | Evar _ | Eabsurd | Ehole -> ()
Mário Pereira's avatar
Mário Pereira committed
200 201
    | Eapp (rs, exprl) ->
      f rs.rs_name; List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
202 203 204
    | 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
205 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
    | 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
238 239 240 241 242
    | Eexn (_xs, None, e) -> (* FIXME? How come we never do binding here? *)
      iter_deps_expr f e
    | Eexn (_xs, Some ty, e) -> (* FIXME? How come we never do binding here? *)
      iter_deps_ty f ty;
      iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
243 244 245 246 247
    | 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
248
    | Eignore e -> iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
249

250
  let rec iter_deps f = function
Mário Pereira's avatar
Mário Pereira committed
251 252
    | Dtype its_dl ->
      List.iter (iter_deps_its_defn f) its_dl
Mário Pereira's avatar
Mário Pereira committed
253 254 255 256 257 258 259 260 261
    | 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
262 263 264
    | Dlet (Lvar (_, e)) -> iter_deps_expr f e
    | Dexn (_, None) -> ()
    | Dexn (_, Some ty) -> iter_deps_ty f ty
265
    | Dclone (_, dl) -> List.iter (iter_deps f) dl
266

267
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
268 269
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

270
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
271
  let mk_let_var pv e1 e2 =
Mário Pereira's avatar
Mário Pereira committed
272
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
273 274

  let tunit = Ttuple []
275

Mário Pereira's avatar
Mário Pereira committed
276 277 278 279 280 281
  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
282

283 284 285 286 287
  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
288 289 290
  let mk_hole =
    mk_expr Ehole (I Ity.ity_unit) Ity.eff_empty

291 292
  let mk_var id ty ghost = (id, ty, ghost)

293 294
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

295
  let mk_its_defn id args private_ def =
Mário Pereira's avatar
Mário Pereira committed
296 297
    { its_name    = id      ; its_args = args;
      its_private = private_; its_def  = def; }
298

Mário Pereira's avatar
Mário Pereira committed
299 300 301 302
  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 }

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

311
end
Mário Pereira's avatar
Mário Pereira committed
312 313 314 315 316

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
317 318 319
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
320

Mário Pereira's avatar
Mário Pereira committed
321 322 323
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
324 325 326 327
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
328
       ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
329 330 331 332 333 334 335 336
    | 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

337 338 339
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

Mário Pereira's avatar
Mário Pereira committed
340 341 342 343 344
  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
345 346 347 348 349 350 351 352 353 354 355 356

  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)

357
  let rec filter_out_ghost_rdef = function
Mário Pereira's avatar
Mário Pereira committed
358 359
    | [] -> []
    | { rec_sym = rs; rec_rsym = rrs } :: l
360 361
      when rs_ghost rs || rs_ghost rrs -> filter_out_ghost_rdef l
    | rdef :: l -> rdef :: filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
362

363 364 365
  let rec pat p =
    match p.pat_node with
    | Pwild ->
366
      ML.Pwild
367 368
    | Pvar vs when (restore_pv vs).pv_ghost ->
      ML.Pwild
369
    | Pvar vs ->
370
      ML.Pident vs.vs_name
371
    | Por (p1, p2) ->
372
      ML.Por (pat p1, pat p2)
373 374
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
      pat p
375
    | Pas (p, vs) ->
376
      ML.Pas (pat p, vs.vs_name)
377
    | Papp (ls, pl) when is_fs_tuple ls ->
378
      ML.Ptuple (List.map pat pl)
379
    | Papp (ls, pl) ->
380 381
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
382 383
      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
384
      ML.Papp (ls, List.rev pat_pl)
385

Mário Pereira's avatar
Mário Pereira committed
386 387
  (** programs *)

388 389
  let pv_name pv = pv.pv_vs.vs_name

390 391 392
  (* individual types *)
  let rec ity t =
    match t.ity_node with
393
    | Ityvar (tvs, _) ->
394
      ML.Tvar tvs
395
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
396
      ML.Ttuple (List.map ity itl)
397
    | Ityapp ({its_ts = ts}, itl, _) ->
398 399 400 401
      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
402

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

408 409 410 411
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
412
  let isconstructor info rs =
413
    match Mid.find_opt rs.rs_name info.ML.from_km with
Mário Pereira's avatar
Mário Pereira committed
414 415 416 417 418 419
    | 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
420 421 422 423
  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
424
    let pv_equal_field rs = pv_equal (fd_of_rs rs) in
Mário Pereira's avatar
Mário Pereira committed
425 426 427 428
    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
429

430
  let get_record_itd info rs =
431
    match Mid.find_opt rs.rs_name info.ML.from_km with
Mário Pereira's avatar
Mário Pereira committed
432 433
    | Some {pd_node = PDtype itdl} ->
      let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
434
      let itd = match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
435
        | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
        | 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
452

Mário Pereira's avatar
Mário Pereira committed
453
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
454 455 456 457 458
    (* 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 =
459
      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
460 461 462 463 464 465 466 467 468
      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

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

Mário Pereira's avatar
Mário Pereira committed
480 481
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
482
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
483 484 485 486 487 488 489 490 491 492
      | 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
493
  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
494 495 496 497 498 499
    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
500
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
501
      let for_cty = create_cty [i_pv] [] [] Mxs.empty
Mário Pereira's avatar
Mário Pereira committed
502
                               Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
503 504 505
      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
506 507
                            (ML.I ity_bool) eff_empty in
      let next_expr =
Mário Pereira's avatar
Mário Pereira committed
508
        let one_const = Number.int_const_dec "1" in
Mário Pereira's avatar
Mário Pereira committed
509
        let one_expr  =
Mário Pereira's avatar
Mário Pereira committed
510
          ML.mk_expr (ML.Econst one_const) ML.ity_int eff_empty in
Mário Pereira's avatar
Mário Pereira committed
511 512
        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
513
       let rec_call  =
Mário Pereira's avatar
Mário Pereira committed
514
        ML.mk_expr (ML.Eapp (for_rs, [next_expr]))
Mário Pereira's avatar
Mário Pereira committed
515
                    ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
516
      let seq_expr =
Mário Pereira's avatar
Mário Pereira committed
517
        ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
518 519
      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
520
    let for_call_expr   =
Mário Pereira's avatar
Mário Pereira committed
521
      let for_call      = ML.Eapp (for_rs, [from_expr]) in
Mário Pereira's avatar
Mário Pereira committed
522 523
      ML.mk_expr for_call ML.ity_unit eff in
    let pv_name pv = pv.pv_vs.vs_name in
524
    let args = [ pv_name i_pv, ty_int, false ] in
Mário Pereira's avatar
Mário Pereira committed
525
    let for_rec_def = {
526 527
      ML.rec_sym  = for_rs;   ML.rec_args = args;
      ML.rec_rsym = for_rs;   ML.rec_exp  = for_expr;
528
      ML.rec_res  = ML.tunit; ML.rec_svar = Stv.empty;
Mário Pereira's avatar
Mário Pereira committed
529
    } in
Mário Pereira's avatar
Mário Pereira committed
530
    let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
531 532 533 534
    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 =
535
      let ns = (Opt.get info.ML.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
536 537 538 539 540
      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 =
541
      let ns = (Opt.get info.ML.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
542 543 544
      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
545 546
  exception ExtractionAny

547 548
  (* build the set of type variables from functions arguments *)
  let rec add_tvar acc = function
549
    | ML.Tvar tv -> Stv.add tv acc
550 551 552
    | ML.Tapp (_, tyl) | ML.Ttuple tyl ->
      List.fold_left add_tvar acc tyl

Mário Pereira's avatar
Mário Pereira committed
553
  (* expressions *)
554
  let rec expr info ({e_effect = eff} as e) =
Mário Pereira's avatar
Mário Pereira committed
555
    assert (not eff.eff_ghost);
Mário Pereira's avatar
Mário Pereira committed
556
    match e.e_node with
557
    | Econst c ->
Mário Pereira's avatar
Mário Pereira committed
558 559
      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
560 561
    | Evar pv ->
      ML.mk_expr (ML.Evar pv) (ML.I e.e_ity) eff
562
    | Elet (LDvar (_, e1), e2) when e_ghost e1 ->
Mário Pereira's avatar
Mário Pereira committed
563
      expr info e2
564 565
    | 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
566 567 568 569 570
    | 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
571 572
    | Elet (LDvar (pv, e1), e2) ->
      let ml_let = ML.mk_let_var pv (expr info e1) (expr info e2) in
573
      ML.mk_expr ml_let (ML.I e.e_ity) eff
574 575
    | Elet (LDsym (rs, _), ein) when rs_ghost rs ->
      expr info ein
576
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
577
      let args = params cty.cty_args in
578 579
      let ef = expr info ef in
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
580 581
      let res = ity cty.cty_result in
      let ml_letrec = ML.Elet (ML.Lsym (rs, res, args, ef), ein) in
582
      ML.mk_expr ml_letrec (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
583 584
    | 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
585 586
      (* partial application of constructor *)
      let eta_app = mk_eta_expansion rs_app pvl cty in
Mário Pereira's avatar
Mário Pereira committed
587
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
588 589 590
      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
591
      let ml_letrec = ML.Elet (ML.Lsym (rsf, res, [], eta_app), ein) in
Mário Pereira's avatar
Mário Pereira committed
592 593
      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) ->
594
      (* partial application *)
Mário Pereira's avatar
Mário Pereira committed
595
      let pvl = app pvl rs_app.rs_cty.cty_args in
596
      let eapp =
Mário Pereira's avatar
Mário Pereira committed
597
        ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
Mário Pereira's avatar
Mário Pereira committed
598 599
      let ein  = expr info ein in
      let res  = ity cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
600
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
601
      let ml_letrec = ML.Elet (ML.Lsym (rsf, res, args, eapp), ein) in
Mário Pereira's avatar
Mário Pereira committed
602 603
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
    | Elet (LDrec rdefl, ein) ->
604 605 606 607
      let rdefl = filter_out_ghost_rdef rdefl in
      let def = function
        | {rec_sym = rs1; rec_rsym = rs2;
           rec_fun = {c_node = Cfun ef; c_cty = cty}} ->
608 609 610 611
          let res  = ity rs1.rs_cty.cty_result in
          let args = params cty.cty_args in
          let svar =
            let args' = List.map (fun (_, ty, _) -> ty) args in
612
            let svar  = List.fold_left add_tvar Stv.empty args' in
613 614 615 616 617
            add_tvar svar res in
          let ef = expr info ef in
          { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
            ML.rec_args = args; ML.rec_exp  = ef ;
            ML.rec_res  = res;  ML.rec_svar = svar; }
618 619
        | _ -> assert false in
      let rdefl = List.map def rdefl in
620 621 622 623
      if rdefl <> [] then
        let ml_letrec = ML.Elet (ML.Lrec rdefl, expr info ein) in
        ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
      else expr info ein
624 625
    | Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs ->
      ML.mk_unit
626 627
    | Eexec ({c_node = Capp (rs, _)}, _) when is_empty_record info rs ->
      ML.mk_unit
628 629
    | Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
      ML.mk_unit
Mário Pereira's avatar
Mário Pereira committed
630
    | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
Mário Pereira's avatar
Mário Pereira committed
631 632
      when isconstructor info rs && cty.cty_args <> [] ->
      (* partial application of constructors *)
Mário Pereira's avatar
Mário Pereira committed
633
      mk_eta_expansion rs pvl cty
Mário Pereira's avatar
Mário Pereira committed
634
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
Mário Pereira's avatar
Mário Pereira committed
635
      let pvl = app pvl rs.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
636
      begin match pvl with
637
      | [pv_expr] when is_optimizable_record_rs info rs -> pv_expr
Mário Pereira's avatar
Mário Pereira committed
638 639 640 641
      | _ -> 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
642
    | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
643
      let args = params cty.cty_args in
644
      ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
645
    | Eexec ({c_node = Cany}, _) -> (* raise ExtractionAny *)
Mário Pereira's avatar
Mário Pereira committed
646
      ML.mk_hole
647
    | Eabsurd ->
648 649 650
      ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
    | Ecase (e1, _) when e_ghost e1 ->
      ML.mk_unit
651
    | Ecase (e1, pl) ->
Mário Pereira's avatar
Mário Pereira committed
652 653 654
      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
655
    | Eassert _ -> ML.mk_unit
Mário Pereira's avatar
Mário Pereira committed
656 657 658 659 660 661 662 663
    | Eif (e1, e2, e3) when e_ghost e3 ->
      let e1 = expr info e1 in
      let e2 = expr info e2 in
      ML.mk_expr (ML.Eif (e1, e2, ML.mk_unit)) (ML.I e.e_ity) eff
    | Eif (e1, e2, e3) when e_ghost e2 ->
      let e1 = expr info e1 in
      let e3 = expr info e3 in
      ML.mk_expr (ML.Eif (e1, ML.mk_unit, e3)) (ML.I e.e_ity) eff
664
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
665 666 667 668
      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
669 670 671 672
    | 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
673
    | Efor (pv1, (pv2, To, pv3), _, efor) ->
Mário Pereira's avatar
Mário Pereira committed
674
      let efor = expr info efor in
Mário Pereira's avatar
Mário Pereira committed
675 676 677 678
      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
679
    | Eghost _ -> assert false
680 681
    | Eassign al ->
      ML.mk_expr (ML.Eassign al) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
682
    | Epure _ -> (* assert false (\*TODO*\) *) ML.mk_hole
Mário Pereira's avatar
Mário Pereira committed
683 684 685 686 687 688
    | 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
689 690 691
    | Eraise (xs, ex) ->
      let ex =
        match expr info ex with
Mário Pereira's avatar
Mário Pereira committed
692
        | {ML.e_node = ML.Eblock []} -> None
Mário Pereira's avatar
Mário Pereira committed
693 694
        | e -> Some e
      in
Mário Pereira's avatar
Mário Pereira committed
695
      ML.mk_expr (ML.Eraise (xs, ex)) (ML.I e.e_ity) eff
696 697 698 699 700
    | Eexn (xs, e1) ->
      let e1 = expr info e1 in
      let ty = if ity_equal xs.xs_ity ity_unit
        then None else Some (ity xs.xs_ity) in
      ML.mk_expr (ML.Eexn (xs, ty, e1)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
701 702 703 704
    | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
    (*   assert false (\*TODO*\) *)
    | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
    (*   assert false (\*TODO*\) *)
705

Mário Pereira's avatar
Mário Pereira committed
706 707
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
708

709 710 711 712
  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
713
  let tdef itd =
714
    let s = itd.itd_its in
715 716 717
    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
718
          let args = List.filter pv_not_ghost rsc.cty_args in
719 720
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
721
    let drecord_fields ({rs_cty = rsc} as rs) =
722
      (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields),
Mário Pereira's avatar
Mário Pereira committed
723 724
      rs.rs_name,
      ity rsc.cty_result
725 726 727 728
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
729
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
730
      | NoDef, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
731
        ML.mk_its_defn id args is_private None
732
      | NoDef, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
733 734
        let cl = ddata_constructs cl in
        ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
735
      | NoDef, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
736 737
        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
738
        begin match pjl with
739 740
          | [] -> 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
741 742 743
            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
744
      | Alias t, _, _ ->
745
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
746 747
      | Range _, _, _ -> assert false (* TODO *)
      | Float _, _, _ -> assert false (* TODO *)
748
    end
Mário Pereira's avatar
Mário Pereira committed
749

Mário Pereira's avatar
Mário Pereira committed
750
  exception ExtractionVal of rsymbol
Mário Pereira's avatar
Mário Pereira committed
751

Mário Pereira's avatar
Mário Pereira committed
752 753 754 755
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

756 757
  (* pids: identifiers from cloned modules without definitions *)
  let pdecl _pids info pd =
Mário Pereira's avatar
Mário Pereira committed
758
    match pd.pd_node with
759
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
760
      []
Mário Pereira's avatar
Mário Pereira committed
761 762 763
    | PDlet (LDsym (_rs, {c_node = Cany})) ->
      []
      (* raise (ExtractionVal _rs) *)
Mário Pereira's avatar
Mário Pereira committed
764 765
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
      []
766
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
767
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
768
      let res  = ity cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
769
      [ML.Dlet (ML.Lsym (rs, res, args, expr info e))]
770
    | PDlet (LDrec rl) ->
771
      let rl = filter_out_ghost_rdef rl in
Mário Pereira's avatar
Mário Pereira committed
772
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
773
        let e = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
774
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
775
        let res  = ity rs1.rs_cty.cty_result in
776 777
        let svar =
          let args' = List.map (fun (_, ty, _) -> ty) args in
778
          let svar  = List.fold_left add_tvar Stv.empty args' in
779
          add_tvar svar res in
Mário Pereira's avatar
Mário Pereira committed
780
        { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
781
          ML.rec_args = args; ML.rec_exp  = expr info e;
782
          ML.rec_res  = res;  ML.rec_svar = svar; } in
783
      if rl = [] then [] else [ML.Dlet (ML.Lrec (List.map def rl))]
Mário Pereira's avatar
Mário Pereira committed
784
    | PDlet (LDsym _) | PDpure | PDlet (LDvar _) ->
785
      []
786
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
787
      let itsd = List.map tdef itl in
Mário Pereira's avatar
Mário Pereira committed
788
      [ML.Dtype itsd]
789
    | PDexn xs ->
Mário Pereira's avatar
Mário Pereira committed
790 791
      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
792

Mário Pereira's avatar
Mário Pereira committed
793
  let pdecl_m m pd =
794 795
    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
796

Mário Pereira's avatar
Mário Pereira committed
797
  (* unit module declarations *)
798 799
  let rec mdecl pids info = function
    | Udecl pd -> pdecl pids info pd
800
    | Uscope (_, l) -> List.concat (List.map (mdecl pids info) l)
801
    | Uuse _ | Uclone _ | Umeta _ -> []
Mário Pereira's avatar
Mário Pereira committed
802

803 804 805 806 807 808 809 810 811 812 813
  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
814
    | Uscope (_, l) -> List.for_all empty_munit l
815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843
    | 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
844
  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
845
  let module_ m =
846 847 848 849 850
    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
851 852 853 854
    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
855
    { ML.mod_from = from; ML.mod_decl = mod_decl; ML.mod_known = mod_known }
Mário Pereira's avatar
Mário Pereira committed
856

Mário Pereira's avatar
Mário Pereira committed
857 858 859 860 861 862 863 864
  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
865 866
end

867 868 869 870 871 872
(** Some transformations *)

module Transform = struct

  open ML

Mário Pereira's avatar
Mário Pereira committed
873
  let no_reads_writes_conflict spv spv_mreg =
874
    let is_not_write {pv_ity = ity} = match ity.ity_node with