compile.ml 28.7 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
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;
Mário Pereira's avatar
Mário Pereira committed
113 114
  }

115 116 117 118 119 120 121
  type is_mutable = bool

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

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

129
  type decl = (* TODO add support for the extraction of ocaml modules *)
Mario Pereira's avatar
Mario Pereira committed
130
    | Dtype   of its_defn list
Mário Pereira's avatar
Mário Pereira committed
131
    | Dlet    of let_def
132
        (* TODO add return type? *)
Mario Pereira's avatar
Mario Pereira committed
133 134
    | Dexn    of xsymbol * ty option

Mário Pereira's avatar
Mário Pereira committed
135 136 137 138 139 140 141
  type known_map = decl Mid.t

  type pmodule = {
    mod_decl  : decl list;
    mod_known : known_map;
  }

Mário Pereira's avatar
Mário Pereira committed
142 143 144
  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
145 146 147
    | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
    | Dlet (Lsym ({rs_name=id}, _, _, _))
    | Dexn ({xs_name=id}, _) -> [id]
Mário Pereira's avatar
Mário Pereira committed
148 149

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

Mário Pereira's avatar
Mário Pereira committed
152 153
  let rec iter_deps_ty f = function
    | Tvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
154
    | Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
Mário Pereira's avatar
Mário Pereira committed
155 156 157
    | 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
158 159
    | Ddata constrl ->
      List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
Mário Pereira's avatar
Mário Pereira committed
160
    | Drecord pjl -> List.iter (fun (_, _, ty) -> iter_deps_ty f ty) pjl
Mário Pereira's avatar
Mário Pereira committed
161 162 163 164 165
    | 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
166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187
  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
188
    | Econst _ | Evar _ | Eabsurd | Ehole -> ()
Mário Pereira's avatar
Mário Pereira committed
189 190
    | Eapp (rs, exprl) ->
      f rs.rs_name; List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
191 192 193
    | 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
194 195 196 197 198 199 200 201 202 203 204 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
    | 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
233
  let iter_deps f = function
Mário Pereira's avatar
Mário Pereira committed
234 235
    | Dtype its_dl ->
      List.iter (iter_deps_its_defn f) its_dl
Mário Pereira's avatar
Mário Pereira committed
236 237 238 239 240 241 242 243 244
    | 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
245 246 247
    | Dlet (Lvar (_, e)) -> iter_deps_expr f e
    | Dexn (_, None) -> ()
    | Dexn (_, Some ty) -> iter_deps_ty f ty
248

249
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
250 251
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

252
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
253
  let mk_let_var pv e1 e2 =
Mário Pereira's avatar
Mário Pereira committed
254
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
255 256

  let tunit = Ttuple []
257

Mário Pereira's avatar
Mário Pereira committed
258 259
  let ity_int  = I ity_int
  let ity_unit = I ity_unit
Mário Pereira's avatar
Mário Pereira committed
260

261 262 263 264 265
  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
266 267 268
  let mk_hole =
    mk_expr Ehole (I Ity.ity_unit) Ity.eff_empty

269 270
  let mk_var id ty ghost = (id, ty, ghost)

271 272
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

273
  let mk_its_defn id args private_ def =
Mário Pereira's avatar
Mário Pereira committed
274 275
    { its_name    = id      ; its_args = args;
      its_private = private_; its_def  = def; }
276

277 278
  let eseq e1 e2 =
    match e1.e_node, e2.e_node with
Mário Pereira's avatar
Mário Pereira committed
279
    | (Eblock [] | Ehole), e | e, (Eblock [] | Ehole) -> e
280 281 282 283 284
    | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
    | _, Eblock e2 -> Eblock (e1 :: e2)
    | Eblock e1, _ -> Eblock (e1 @ [e2])
    | _ -> Eblock [e1; e2]

285
end
Mário Pereira's avatar
Mário Pereira committed
286 287 288 289 290

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
291 292 293
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
294

Mário Pereira's avatar
Mário Pereira committed
295 296 297 298 299
  type info = {
    info_current_mo   : Pmodule.pmodule option;
    info_mo_known_map : Pdecl.known_map;
  }

Mário Pereira's avatar
Mário Pereira committed
300 301 302
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
303 304 305 306
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
307
       ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
308 309 310 311 312 313 314 315
    | 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

316 317 318
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

Mário Pereira's avatar
Mário Pereira committed
319 320 321 322 323
  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
324 325 326 327 328 329 330 331 332 333 334 335

  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
336 337 338 339 340 341
  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

342 343 344
  let rec pat p =
    match p.pat_node with
    | Pwild ->
345
      ML.Pwild
346 347
    | Pvar vs when (restore_pv vs).pv_ghost ->
      ML.Pwild
348
    | Pvar vs ->
349
      ML.Pident vs.vs_name
350
    | Por (p1, p2) ->
351
      ML.Por (pat p1, pat p2)
352 353
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
      pat p
354
    | Pas (p, vs) ->
355
      ML.Pas (pat p, vs.vs_name)
356
    | Papp (ls, pl) when is_fs_tuple ls ->
357
      ML.Ptuple (List.map pat pl)
358
    | Papp (ls, pl) ->
359 360
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
361 362
      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
363
      ML.Papp (ls, List.rev pat_pl)
364

Mário Pereira's avatar
Mário Pereira committed
365 366
  (** programs *)

367 368
  let pv_name pv = pv.pv_vs.vs_name

369 370 371
  (* individual types *)
  let rec ity t =
    match t.ity_node with
372
    | Ityvar (tvs, _) ->
373
      ML.Tvar tvs
374
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
375
      ML.Ttuple (List.map ity itl)
376
    | Ityapp ({its_ts = ts}, itl, _) ->
377 378 379 380
      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
381

Mário Pereira's avatar
Mário Pereira committed
382
  let pvty pv =
383 384 385 386 387
    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
388

389 390 391 392
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
393 394 395 396 397 398 399 400
  let isconstructor info rs =
    match Mid.find_opt rs.rs_name info.info_mo_known_map with
    | 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
401 402 403 404 405 406 407 408 409
  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
410

411
  let get_record_itd info rs =
Mário Pereira's avatar
Mário Pereira committed
412 413 414
    match Mid.find_opt rs.rs_name info.info_mo_known_map with
    | Some {pd_node = PDtype itdl} ->
      let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
415
      let itd = match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
416
        | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432
        | 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
433

Mário Pereira's avatar
Mário Pereira committed
434
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
435 436 437 438 439
    (* 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 =
440
      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
441 442 443 444 445 446 447 448 449
      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

450 451 452 453 454 455
  (* 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
456 457 458 459
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
      if args = [] then [ML.mk_var_unit ()] else args
460

Mário Pereira's avatar
Mário Pereira committed
461 462
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
463
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
464 465 466 467 468 469 470 471 472 473
      | 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
474
  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
475 476 477 478 479 480
    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
481
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
482
      let for_cty = create_cty [i_pv] [] [] Mxs.empty
Mário Pereira's avatar
Mário Pereira committed
483
                               Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
484 485 486
      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
487 488
                            (ML.I ity_bool) eff_empty in
      let next_expr =
Mário Pereira's avatar
Mário Pereira committed
489
        let one_const = Number.int_const_dec "1" in
Mário Pereira's avatar
Mário Pereira committed
490
        let one_expr  =
Mário Pereira's avatar
Mário Pereira committed
491
          ML.mk_expr (ML.Econst one_const) ML.ity_int eff_empty in
Mário Pereira's avatar
Mário Pereira committed
492 493
        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
494
       let rec_call  =
Mário Pereira's avatar
Mário Pereira committed
495
        ML.mk_expr (ML.Eapp (for_rs, [next_expr]))
Mário Pereira's avatar
Mário Pereira committed
496
                    ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
497
      let seq_expr =
Mário Pereira's avatar
Mário Pereira committed
498
        ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
499 500
      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
501
    let for_call_expr   =
Mário Pereira's avatar
Mário Pereira committed
502
      let for_call      = ML.Eapp (for_rs, [from_expr]) in
Mário Pereira's avatar
Mário Pereira committed
503 504
      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
505
    let args = [ pv_name  i_pv, ty_int, false ] in
Mário Pereira's avatar
Mário Pereira committed
506
    let for_rec_def = {
Mário Pereira's avatar
Mário Pereira committed
507 508
      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
509
      ML.rec_res  = ML.tunit;
Mário Pereira's avatar
Mário Pereira committed
510
    } in
Mário Pereira's avatar
Mário Pereira committed
511
    let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
512 513 514 515 516 517 518 519 520 521 522 523 524 525
    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 =
      let ns = (Opt.get info.info_current_mo).mod_export in
      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 =
      let ns = (Opt.get info.info_current_mo).mod_export in
      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
526 527
  exception ExtractionAny

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

Mário Pereira's avatar
Mário Pereira committed
657 658
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
659

660 661 662 663
  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
664
  let tdef itd =
665
    let s = itd.itd_its in
666 667 668
    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
669
          let args = List.filter pv_not_ghost rsc.cty_args in
670 671
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
672
    let drecord_fields ({rs_cty = rsc} as rs) =
Mário Pereira's avatar
Mário Pereira committed
673 674 675
      (List.exists (pv_equal (Opt.get rs.rs_field)) s.its_mfields),
      rs.rs_name,
      ity rsc.cty_result
676 677 678 679
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
680 681
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
682
        ML.mk_its_defn id args is_private None
683
      | None, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
684 685
        let cl = ddata_constructs cl in
        ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
686
      | None, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
687 688
        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
689
        begin match pjl with
690 691
          | [] -> 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
692 693 694
            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
695
      | Some t, _, _ ->
696
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
697
    end
Mário Pereira's avatar
Mário Pereira committed
698

Mário Pereira's avatar
Mário Pereira committed
699
  exception ExtractionVal of rsymbol
Mário Pereira's avatar
Mário Pereira committed
700

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

Mário Pereira's avatar
Mário Pereira committed
705
  (* program declarations *)
706
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
707
    match pd.pd_node with
708
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
709
      []
Mário Pereira's avatar
Mário Pereira committed
710 711 712
    | PDlet (LDsym (_rs, {c_node = Cany})) ->
      []
      (* raise (ExtractionVal _rs) *)
Mário Pereira's avatar
Mário Pereira committed
713 714
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
      []
715
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
716
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
717
      let res  = ity cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
718
      [ML.Dlet (ML.Lsym (rs, res, args, expr info e))]
719
    | PDlet (LDrec rl) ->
Mário Pereira's avatar
Mário Pereira committed
720
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
721
        let e = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
722
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
723
        let res  = ity rs1.rs_cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
724
        { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
725 726
          ML.rec_args = args; ML.rec_exp  = expr info e;
          ML.rec_res  = res } in
Mário Pereira's avatar
Mário Pereira committed
727
      let rec_def = filter_ghost_rdef def rl in
Mário Pereira's avatar
Mário Pereira committed
728 729
      [ML.Dlet (ML.Lrec rec_def)]
    | PDlet (LDsym _) | PDpure | PDlet (LDvar _) ->
730
      []
731
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
732
      let itsd = List.map tdef itl in
Mário Pereira's avatar
Mário Pereira committed
733
      [ML.Dtype itsd]
734
    | PDexn xs ->
Mário Pereira's avatar
Mário Pereira committed
735 736
      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
737

Mário Pereira's avatar
Mário Pereira committed
738 739 740 741 742 743
  let pdecl_m m pd =
    let info = {
      info_current_mo   = Some m;
      info_mo_known_map = m.mod_known; } in
    pdecl info pd

Mário Pereira's avatar
Mário Pereira committed
744
  (* unit module declarations *)
745
  let rec mdecl info = function
Mário Pereira's avatar
Mário Pereira committed
746
    | Udecl pd -> pdecl info pd
747 748
    | Uscope (_, _, l) -> List.concat (List.map (mdecl info) l)
    | Uuse _ | Uclone _ | Umeta _ -> []
Mário Pereira's avatar
Mário Pereira committed
749 750

  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
751 752 753 754
  let module_ m =
    let info = {
      info_current_mo   = Some m;
      info_mo_known_map = m.mod_known; } in
Mário Pereira's avatar
Mário Pereira committed
755 756 757 758 759 760
    let mod_decl = List.concat (List.map (mdecl info) m.mod_units) in
    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
    { ML.mod_decl = mod_decl; ML.mod_known = mod_known }, info
Mário Pereira's avatar
Mário Pereira committed
761

Mário Pereira's avatar
Mário Pereira committed
762 763 764 765 766 767 768 769
  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
770 771
end

772 773 774 775 776 777 778 779
(** Some transformations *)

module Transform = struct

  open ML

  type subst = expr Mpv.t

Mário Pereira's avatar
Mário Pereira committed
780
  let rec expr info subst e =
781
    let mk n = { e with e_node = n } in
Mário Pereira's avatar
Mário Pereira committed
782
    let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
783
    match e.e_node with
784 785 786 787 788 789 790 791 792 793 794
    | Evar pv -> (try Mpv.find pv subst with Not_found -> e)
    (* | Elet (Lvar (pv, ({e_node = Econst _ } as e1)), e2) *)
    (* | Elet (Lvar (pv, ({e_node = Eblock []} as e1)), e2) *)
    (*   when Slab.mem Expr.proxy_label pv.pv_vs.vs_name.id_label -> *)
    (*   add_subst pv e1 e2 *)
    (* | Elet (Lvar (pv, ({e_node = Eapp (rs, _)} as e1)), e2) *)
    (*   when Translate.isconstructor info rs && *)
    (*        Slab.mem Expr.proxy_label pv.pv_vs.vs_name.id_label -> *)
    (*   (\* because of Lvar we know the constructor is completely applied *\) *)
    (*   add_subst pv e1 e2 *)
    | Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
795 796
      when Slab.mem Expr.proxy_label pv.pv_vs.vs_name.id_label &&
           eff_pure e1.e_effect ->
797
      let e1 = expr info subst e1 in
Mário Pereira's avatar
Mário Pereira committed
798
      add_subst pv e1 e2
799
    | Elet (ld, e) ->
Mário Pereira's avatar
Mário Pereira committed
800
      mk (Elet (let_def info subst ld, expr info subst e))
801
    | Eapp (rs, el) ->
Mário Pereira's avatar
Mário Pereira committed
802
      mk (Eapp (rs, List.map (expr info subst) el))
803
    | Efun (vl, e) ->
Mário Pereira's avatar
Mário Pereira committed
804
      mk (Efun (vl, expr info subst e))
805
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
806
      mk (Eif (expr info subst e1, expr info subst e2, expr info subst e3))
807
    | Ematch (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
808
      mk (Ematch (expr info subst e, List.map (branch info subst) bl))
809
    | Eblock el ->
Mário Pereira's avatar
Mário Pereira committed
810
      mk (Eblock (List.map (expr info subst) el))
811
    | Ewhile (e1, e2) ->
Mário Pereira's avatar
Mário Pereira committed
812
      mk (Ewhile (expr info subst e1, expr info subst e2))
813
    | Efor (x, pv1, dir, pv2, e) ->
Mário Pereira's avatar
Mário Pereira committed
814
      let e = mk (Efor (x, pv1, dir, pv2, expr info subst e)) in
815 816 817
      (* be careful when pv1 and pv2 are in subst *)
      mk_let subst pv1 (mk_let subst pv2 e)
    | Eraise (exn, eo) ->
Mário Pereira's avatar
Mário Pereira committed
818
      mk (Eraise (exn, Opt.map (expr info subst) eo))
819
    | Etry (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
820
      mk (Etry (expr info subst e, List.map (xbranch info subst) bl))
821 822 823
    | Eassign al ->
      let assign e (_, _, pv) = mk_let subst pv e in
      List.fold_left assign e al
Mário Pereira's avatar
Mário Pereira committed
824
    | Econst _ | Eabsurd | Ehole -> e
825 826 827 828 829 830 831

  and mk_let subst pv e =
    try
      let e1 = Mpv.find pv subst in
      { e with e_node = Elet (Lvar (pv, e1), e) }
    with Not_found -> e

Mário Pereira's avatar
Mário Pereira committed
832 833
  and branch info subst (pat, e) = pat, expr info subst e
  and xbranch info subst (exn, pat, e) = exn, pat, expr info subst e
834

Mário Pereira's avatar
Mário Pereira committed
835
  and let_def info subst = function
836 837
    | Lvar (pv, e) ->
      assert (not (Mpv.mem pv subst)); (* no capture *)
Mário Pereira's avatar
Mário Pereira committed
838
      Lvar (pv, expr info subst e)
Mário Pereira's avatar
Mário Pereira committed
839 840
    | Lsym (rs, res, args, e) ->
      Lsym (rs, res, args, expr info subst e)
Mário Pereira's avatar
Mário Pereira committed
841
    | Lrec rl -> Lrec (List.map (rdef info subst) rl)
842

Mário Pereira's avatar
Mário Pereira committed
843 844
  and rdef info subst r =
    { r with rec_exp = expr info subst r.rec_exp }
845

Mário Pereira's avatar
Mário Pereira committed
846
  let pdecl info = function
847
    | Dtype _ | Dexn _ as d -> d
Mário Pereira's avatar
Mário Pereira committed
848
    | Dlet def -> Dlet (let_def info Mpv.empty def)
849

Mário Pereira's avatar
Mário Pereira committed
850
  let module_ info m =
Mário Pereira's avatar
Mário Pereira committed
851 852 853 854 855 856
    let mod_decl = List.map (pdecl info) m.mod_decl in
    let add known_map decl =
      let idl = 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
    { mod_decl = mod_decl; mod_known = mod_known }
857 858

end
Mário Pereira's avatar
Mário Pereira committed
859 860 861

(*
 * Local Variables:
862
 * compile-command: "make -C ../.. -j3 bin/why3extract.opt"
Mário Pereira's avatar
Mário Pereira committed
863 864
 * End:
 *)