compile.ml 29.3 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 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
(********************************************************************)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

(*
  - option to extract into a single file

  - no more why3extract.cma
    use driver preludes instead

  - 2 drivers for nums and zarith

  - no delcaration at all for a module -> no file produced
    (e.g. ref.Ref)

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

  - drivers for val now may use %1, %2, etc. (though not mandatory)
    Capp f x y
      "..." -> "..." x y
      "...%1..." -> "...x..." y
      "..(*%1*)..." -> "...(*x*)..." y
      "..%1..%3.." -> (fun z -> "..x..z..")  (y ignored)

  - 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 = ...")

  - use a black list in printer to avoid clash with Pervasives symbols
    (e.g. ref, (!), etc.)

*)

47 48 49 50 51
(*
  Questions pour Jean-Christophe et Andreï :
    - est-ce qu'il y a des utilisations particulières du champ
      [itd_fields], vis-à-vis du champ [itd_constructors] ?

52 53 54
    - comme l'AST [expr] est déjà en forme normale-A, est-ce que ça
      fait du sense pour vous d'utiliser des applications de la forme
      [Eapp of ident * ident list] ?
55 56 57 58

    - faire un module Erasure, pour y concentrer tout ce qui
      appartient à l'éffacement du code fantôme ?

59 60
    - comment est-ce qu'il marche la [mask] d'un [prog_pattern] ?

61
 *)
62

63 64
(*
  TODO: réfléchir sur l'affectation parallèle
65 66 67
*)


68 69 70 71
(** Abstract syntax of ML *)

open Ident
open Ity
Mário Pereira's avatar
Mário Pereira committed
72
open Ty
Mário Pereira's avatar
Mário Pereira committed
73
open Term
74

Mário Pereira's avatar
Mário Pereira committed
75 76 77 78 79 80 81 82
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
83
  let fname = match fname, path with
Mário Pereira's avatar
Mário Pereira committed
84 85 86 87 88
    | None, "why3"::_ -> "why3"
    | None, _   -> String.concat "__" path
    | Some f, _ -> clean_name f in
  fname ^ "__" ^ t

89 90
module ML = struct

91 92
  open Expr

93
  type ty =
94
    | Tvar    of tvsymbol
95 96 97
    | Tapp    of ident * ty list
    | Ttuple  of ty list

98 99 100
  type is_ghost = bool

  type var = ident * ty * is_ghost
101

Mário Pereira's avatar
Mário Pereira committed
102 103
  type for_direction = To | DownTo

104 105 106
  type pat =
    | Pwild
    | Pident  of ident
Mário Pereira's avatar
Mário Pereira committed
107
    | Papp    of lsymbol * pat list
108 109 110 111 112 113 114 115
    | Ptuple  of pat list
    | Por     of pat * pat
    | Pas     of pat * ident

  type is_rec = bool

  type binop = Band | Bor | Beq

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

118
  type expr = {
Mário Pereira's avatar
Mário Pereira committed
119 120 121
    e_node   : expr_node;
    e_ity    : ity;
    e_effect : effect;
122
    (* TODO: add the set of free variables? *)
123 124 125 126
  }

  and expr_node =
    | Econst  of Number.integer_constant
127
    | Evar    of pvsymbol
128
    | Eapp    of rsymbol * expr list
129
    | Efun    of var list * expr
Mário Pereira's avatar
Mário Pereira committed
130
    | Elet    of let_def * expr
131
    | Eif     of expr * expr * expr
Mário Pereira's avatar
Mário Pereira committed
132
    (* | Ecast   of expr * ty *)
Mário Pereira's avatar
Mário Pereira committed
133
    | Eassign of (pvsymbol * rsymbol * pvsymbol) list
134 135 136
    | Ematch  of expr * (pat * expr) list
    | Eblock  of expr list
    | Ewhile  of expr * expr
Mário Pereira's avatar
Mário Pereira committed
137 138
    (* For loop for Why3's type int *)
    | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
Mário Pereira's avatar
Mário Pereira committed
139 140
    | Eraise  of xsymbol * expr option
    | Etry    of expr * (xsymbol * pvsymbol list * expr) list
141
    | Eabsurd
Mário Pereira's avatar
Mário Pereira committed
142
    | Ehole
143

Mário Pereira's avatar
Mário Pereira committed
144 145
  and let_def =
    | Lvar of pvsymbol * expr
Mário Pereira's avatar
Mário Pereira committed
146
    | Lsym of rsymbol * ty * var list * expr
Mário Pereira's avatar
Mário Pereira committed
147 148 149 150 151 152 153
    | 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
154
    rec_res  : ty;
Mário Pereira's avatar
Mário Pereira committed
155 156
  }

157 158 159 160 161 162 163
  type is_mutable = bool

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

164 165 166 167 168 169 170
  type its_defn = {
    its_name    : ident;
    its_args    : tvsymbol list;
    its_private : bool;
    its_def     : typedef option;
  }

171
  type decl = (* TODO add support for the extraction of ocaml modules *)
Mario Pereira's avatar
Mario Pereira committed
172
    | Dtype   of its_defn list
Mário Pereira's avatar
Mário Pereira committed
173
    | Dlet    of let_def
174
        (* TODO add return type? *)
Mario Pereira's avatar
Mario Pereira committed
175 176
    | Dexn    of xsymbol * ty option

Mário Pereira's avatar
Mário Pereira committed
177 178 179 180 181 182 183
  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
184 185 186 187 188 189 190 191
  let get_decl_name = function
    | Dtype itdefl -> List.map (fun {its_name = id} -> id) itdefl
    | Dlet (Lvar (pv, _)) -> [pv.pv_vs.vs_name]
    | Dlet (Lsym (rs, _, _, _)) -> [rs.rs_name]
    | Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
    | Dexn (xs, _) -> [xs.xs_name]

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

Mário Pereira's avatar
Mário Pereira committed
194 195
  let rec iter_deps_ty f = function
    | Tvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
196
    | Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
Mário Pereira's avatar
Mário Pereira committed
197 198 199
    | 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
200 201
    | Ddata constrl ->
      List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
Mário Pereira's avatar
Mário Pereira committed
202
    | Drecord pjl -> List.iter (fun (_, _, ty) -> iter_deps_ty f ty) pjl
Mário Pereira's avatar
Mário Pereira committed
203 204 205 206 207
    | 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
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
  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
230
    | Econst _ | Evar _ | Eabsurd | Ehole -> ()
Mário Pereira's avatar
Mário Pereira committed
231 232
    | Eapp (rs, exprl) ->
      f rs.rs_name; List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
233 234 235
    | 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
236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
    | 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
275
  let iter_deps f = function
Mário Pereira's avatar
Mário Pereira committed
276 277
    | Dtype its_dl ->
      List.iter (iter_deps_its_defn f) its_dl
Mário Pereira's avatar
Mário Pereira committed
278 279 280 281 282 283 284 285 286
    | 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
287 288 289
    | Dlet (Lvar (_, e)) -> iter_deps_expr f e
    | Dexn (_, None) -> ()
    | Dexn (_, Some ty) -> iter_deps_ty f ty
290

291
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
292 293
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

294
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
295
  let mk_let_var pv e1 e2 =
Mário Pereira's avatar
Mário Pereira committed
296
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
297 298

  let tunit = Ttuple []
299

Mário Pereira's avatar
Mário Pereira committed
300 301
  let ity_int  = I ity_int
  let ity_unit = I ity_unit
Mário Pereira's avatar
Mário Pereira committed
302

303 304 305 306 307
  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
308 309 310
  let mk_hole =
    mk_expr Ehole (I Ity.ity_unit) Ity.eff_empty

311 312
  let mk_var id ty ghost = (id, ty, ghost)

313 314
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

315
  let mk_its_defn id args private_ def =
Mário Pereira's avatar
Mário Pereira committed
316 317
    { its_name    = id      ; its_args = args;
      its_private = private_; its_def  = def; }
318

319 320
  let eseq e1 e2 =
    match e1.e_node, e2.e_node with
Mário Pereira's avatar
Mário Pereira committed
321
    | (Eblock [] | Ehole), e | e, (Eblock [] | Ehole) -> e
322 323 324 325 326
    | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
    | _, Eblock e2 -> Eblock (e1 :: e2)
    | Eblock e1, _ -> Eblock (e1 @ [e2])
    | _ -> Eblock [e1; e2]

327
end
Mário Pereira's avatar
Mário Pereira committed
328 329 330 331 332

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
333 334 335
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
336

Mário Pereira's avatar
Mário Pereira committed
337 338 339 340 341
  type info = {
    info_current_mo   : Pmodule.pmodule option;
    info_mo_known_map : Pdecl.known_map;
  }

Mário Pereira's avatar
Mário Pereira committed
342 343 344
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
345 346 347 348
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
349
       ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
350 351 352 353 354 355 356 357
    | 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

358 359 360
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

Mário Pereira's avatar
Mário Pereira committed
361 362 363 364 365
  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
366 367 368 369 370 371 372 373 374 375 376 377

  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
378 379 380 381 382 383
  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

384 385 386
  let rec pat p =
    match p.pat_node with
    | Pwild ->
387
      ML.Pwild
388
    | Pvar vs ->
389
      ML.Pident vs.vs_name
390
    | Por (p1, p2) ->
391
      ML.Por (pat p1, pat p2)
392
    | Pas (p, vs) ->
393
      ML.Pas (pat p, vs.vs_name)
394
    | Papp (ls, pl) when is_fs_tuple ls ->
395
      ML.Ptuple (List.map pat pl)
396
    | Papp (ls, pl) ->
397 398
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
399 400
      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
401
      in
Mário Pereira's avatar
Mário Pereira committed
402
      ML.Papp (ls, List.rev pat_pl)
403

Mário Pereira's avatar
Mário Pereira committed
404 405
  (** programs *)

406 407 408 409 410
  let pv_name pv = pv.pv_vs.vs_name

  let is_underscore pv =
    (pv_name pv).id_string = "_" && ity_equal pv.pv_ity ity_unit

411 412 413
  (* individual types *)
  let rec ity t =
    match t.ity_node with
414
    | Ityvar (tvs, _) ->
415
      ML.Tvar tvs
416
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
417
      ML.Ttuple (List.map ity itl)
418
    | Ityapp ({its_ts = ts}, itl, _) ->
419 420 421 422
      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
423

Mário Pereira's avatar
Mário Pereira committed
424
  let pvty pv =
425 426 427 428 429
    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
430

431 432 433 434
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
435 436 437 438 439 440 441 442
  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
443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470
  (* let get_record info rs = *)
  (*   match Mid.find_opt rs.rs_name info.info_mo_known_map with *)
  (*   | Some {pd_node = PDtype itdl} -> *)
  (*     let f itd = List.exists (rs_equal rs) itd.itd_fields in *)
  (*     let itd = List.find f itdl in *)
  (*     let is_private = itd.itd_its.its_private in *)

  (*   | _ -> true, [] *)

  let is_private_record info rs =
    match Mid.find_opt rs.rs_name info.info_mo_known_map with
    | Some {pd_node = PDtype itdl} ->
      let f itd = List.exists (rs_equal rs) itd.itd_fields in
      let itd = List.find f itdl in
      itd.itd_its.its_private
    | _ -> assert false (* rs is a field *)

  let get_record info rs =
    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
      let itd =
        try List.find (fun itd -> f itd.itd_constructors) itdl
        with Not_found -> List.find (fun itd -> f itd.itd_fields) itdl in
      let no_g e = not (rs_ghost e) in
      List.filter no_g itd.itd_fields, Some itd.itd_its.its_private
    | _ -> [], None

Mário Pereira's avatar
Mário Pereira committed
471
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
472 473 474 475 476
    (* 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 =
477
      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
478 479 480 481 482 483 484 485 486
      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

487 488 489 490 491 492
  (* 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
493 494 495 496
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
      if args = [] then [ML.mk_var_unit ()] else args
497

Mário Pereira's avatar
Mário Pereira committed
498 499
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
500
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
501 502 503 504 505 506 507 508 509 510
      | 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
511
  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
512 513 514 515 516 517
    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
518
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
519
      let for_cty = create_cty [i_pv] [] [] Mxs.empty
Mário Pereira's avatar
Mário Pereira committed
520
                               Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
521 522 523
      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
524 525
                            (ML.I ity_bool) eff_empty in
      let next_expr =
Mário Pereira's avatar
Mário Pereira committed
526
        let one_const = Number.int_const_dec "1" in
Mário Pereira's avatar
Mário Pereira committed
527
        let one_expr  =
Mário Pereira's avatar
Mário Pereira committed
528
          ML.mk_expr (ML.Econst one_const) ML.ity_int eff_empty in
Mário Pereira's avatar
Mário Pereira committed
529 530
        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
531
       let rec_call  =
Mário Pereira's avatar
Mário Pereira committed
532
        ML.mk_expr (ML.Eapp (for_rs, [next_expr]))
Mário Pereira's avatar
Mário Pereira committed
533
                    ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
534
      let seq_expr =
Mário Pereira's avatar
Mário Pereira committed
535
        ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
536 537
      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
538
    let for_call_expr   =
Mário Pereira's avatar
Mário Pereira committed
539
      let for_call      = ML.Eapp (for_rs, [from_expr]) in
Mário Pereira's avatar
Mário Pereira committed
540 541
      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
542
    let args = [ pv_name  i_pv, ty_int, false ] in
Mário Pereira's avatar
Mário Pereira committed
543
    let for_rec_def = {
Mário Pereira's avatar
Mário Pereira committed
544 545
      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
546
      ML.rec_res  = ML.tunit;
Mário Pereira's avatar
Mário Pereira committed
547
    } in
Mário Pereira's avatar
Mário Pereira committed
548
    let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
549 550 551 552 553 554 555 556 557 558 559 560 561 562
    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
563 564
  exception ExtractionAny

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

Mário Pereira's avatar
Mário Pereira committed
694 695
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
696

697 698 699 700
  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
701
  let tdef itd =
702
    let s = itd.itd_its in
703 704 705
    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
706
          let args = List.filter pv_not_ghost rsc.cty_args in
707 708
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
709
    let drecord_fields ({rs_cty = rsc} as rs) =
Mário Pereira's avatar
Mário Pereira committed
710 711 712
      (List.exists (pv_equal (Opt.get rs.rs_field)) s.its_mfields),
      rs.rs_name,
      ity rsc.cty_result
713 714 715 716
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
717 718
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
719
        ML.mk_its_defn id args is_private None
720
      | None, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
721 722
        let cl = ddata_constructs cl in
        ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
723
      | None, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
724 725
        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
726 727 728 729 730 731 732 733
        begin match pjl with
          | [] -> ML.mk_its_defn id args is_private None
          | [(is_mutable, _, ty_pj)]
            when not s.its_private && not is_mutable ->
            (* singleton public record with an imutable field *)
            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
734
      | Some t, _, _ ->
735
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
736
    end
Mário Pereira's avatar
Mário Pereira committed
737

Mário Pereira's avatar
Mário Pereira committed
738
  exception ExtractionVal of rsymbol
Mário Pereira's avatar
Mário Pereira committed
739

Mário Pereira's avatar
Mário Pereira committed
740 741 742 743
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
744
  (* program declarations *)
745
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
746
    match pd.pd_node with
747
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
748
      []
Mário Pereira's avatar
Mário Pereira committed
749 750 751
    | PDlet (LDsym (_rs, {c_node = Cany})) ->
      []
      (* raise (ExtractionVal _rs) *)
Mário Pereira's avatar
Mário Pereira committed
752 753
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
      []
754
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
755
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
756
      let res  = ity cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
757
      [ML.Dlet (ML.Lsym (rs, res, args, expr info e))]
758
    | PDlet (LDrec rl) ->
Mário Pereira's avatar
Mário Pereira committed
759
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
760
        let e = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
761
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
762
        let res  = ity rs1.rs_cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
763
        { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
764 765
          ML.rec_args = args; ML.rec_exp  = expr info e;
          ML.rec_res  = res } in
Mário Pereira's avatar
Mário Pereira committed
766
      let rec_def = filter_ghost_rdef def rl in
Mário Pereira's avatar
Mário Pereira committed
767 768
      [ML.Dlet (ML.Lrec rec_def)]
    | PDlet (LDsym _) | PDpure | PDlet (LDvar _) ->
769
      []
770
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
771
      let itsd = List.map tdef itl in
Mário Pereira's avatar
Mário Pereira committed
772
      [ML.Dtype itsd]
773
    | PDexn xs ->
Mário Pereira's avatar
Mário Pereira committed
774 775
      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
776

Mário Pereira's avatar
Mário Pereira committed
777 778 779 780 781 782
  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
783
  (* unit module declarations *)
784
  let mdecl info = function
Mário Pereira's avatar
Mário Pereira committed
785
    | Udecl pd -> pdecl info pd
786
    |  _ -> (* TODO *) []
Mário Pereira's avatar
Mário Pereira committed
787 788

  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
789 790 791 792
  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
793 794 795 796 797 798
    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
799

Mário Pereira's avatar
Mário Pereira committed
800 801 802 803 804 805 806 807
  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
808 809
end

810 811 812 813 814 815 816 817
(** Some transformations *)

module Transform = struct

  open ML

  type subst = expr Mpv.t

Mário Pereira's avatar
Mário Pereira committed
818
  let rec expr info subst e =
819
    let mk n = { e with e_node = n } in
Mário Pereira's avatar
Mário Pereira committed
820
    let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
821 822 823
    match e.e_node with
    | Evar pv ->
      (try Mpv.find pv subst with Not_found -> e)
Mário Pereira's avatar
Mário Pereira committed
824
    | Elet (Lvar (pv, ({e_node = Econst _ } as e1)), e2)
Mário Pereira's avatar
Mário Pereira committed
825
    | Elet (Lvar (pv, ({e_node = Eblock []} as e1)), e2) ->
Mário Pereira's avatar
Mário Pereira committed
826 827 828
      add_subst pv e1 e2
    | Elet (Lvar (pv, ({e_node = Eapp (rs, [])} as e1)), e2)
      when Translate.isconstructor info rs ->
Mário Pereira's avatar
Mário Pereira committed
829
      (* only optimize constructors with no argument *)
Mário Pereira's avatar
Mário Pereira committed
830
      (* because of Lvar we know the constructor is completely applied *)
Mário Pereira's avatar
Mário Pereira committed
831
      add_subst pv e1 e2
832
    | Elet (ld, e) ->
Mário Pereira's avatar
Mário Pereira committed
833
      mk (Elet (let_def info subst ld, expr info subst e))
834
    | Eapp (rs, el) ->
Mário Pereira's avatar
Mário Pereira committed
835
      mk (Eapp (rs, List.map (expr info subst) el))
836
    | Efun (vl, e) ->
Mário Pereira's avatar
Mário Pereira committed
837
      mk (Efun (vl, expr info subst e))
838
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
839
      mk (Eif (expr info subst e1, expr info subst e2, expr info subst e3))
Mário Pereira's avatar
Mário Pereira committed
840 841
    (* | Ecast (e, ty) -> *)
    (*   mk (Ecast (expr info subst e, ty)) *)
842
    | Ematch (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
843
      mk (Ematch (expr info subst e, List.map (branch info subst) bl))
844
    | Eblock el ->
Mário Pereira's avatar
Mário Pereira committed
845
      mk (Eblock (List.map (expr info subst) el))
846
    | Ewhile (e1, e2) ->
Mário Pereira's avatar
Mário Pereira committed
847
      mk (Ewhile (expr info subst e1, expr info subst e2))
848
    | Efor (x, pv1, dir, pv2, e) ->
Mário Pereira's avatar
Mário Pereira committed
849
      let e = mk (Efor (x, pv1, dir, pv2, expr info subst e)) in
850 851 852
      (* 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
853
      mk (Eraise (exn, Opt.map (expr info subst) eo))
854
    | Etry (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
855
      mk (Etry (expr info subst e, List.map (xbranch info subst) bl))
856 857 858
    | 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
859
    | Econst _ | Eabsurd | Ehole -> e
860 861 862 863 864 865 866

  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
867 868
  and branch info subst (pat, e) = pat, expr info subst e
  and xbranch info subst (exn, pat, e) = exn, pat, expr info subst e
869

Mário Pereira's avatar
Mário Pereira committed
870
  and let_def info subst = function
871 872
    | Lvar (pv, e) ->
      assert (not (Mpv.mem pv subst)); (* no capture *)
Mário Pereira's avatar
Mário Pereira committed
873
      Lvar (pv, expr info subst e)
Mário Pereira's avatar
Mário Pereira committed
874 875
    | Lsym (rs, res, args, e) ->
      Lsym (rs, res, args, expr info subst e)
Mário Pereira's avatar
Mário Pereira committed
876
    | Lrec rl -> Lrec (List.map (rdef info subst) rl)
877

Mário Pereira's avatar
Mário Pereira committed
878 879
  and rdef info subst r =
    { r with rec_exp = expr info subst r.rec_exp }
880

Mário Pereira's avatar
Mário Pereira committed
881
  let pdecl info = function
882
    | Dtype _ | Dexn _ as d -> d
Mário Pereira's avatar
Mário Pereira committed
883
    | Dlet def -> Dlet (let_def info Mpv.empty def)
884

Mário Pereira's avatar
Mário Pereira committed
885
  let module_ info m =
Mário Pereira's avatar
Mário Pereira committed
886 887 888 889 890 891
    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 }
892 893

end
Mário Pereira's avatar
Mário Pereira committed
894 895 896

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