Commit b494a842 authored by Mário Pereira's avatar Mário Pereira

Code extraction (wip)

Inlining of variables binded to unit
parent a80ea117
......@@ -367,9 +367,10 @@ module Translate = struct
ML.mk_expr (ML.eseq (expr info e1) ML.mk_unit) (ML.I e.e_ity) eff
| Elet (LDvar (pvs, e1), e2) when is_underscore pvs ->
ML.mk_expr (ML.eseq (expr info e1) (expr info e2)) (ML.I e.e_ity) eff
| Elet (LDvar (pvs, e1), e2) when e_ghost e1 ->
let ml_let = ML.ml_let_var pvs ML.mk_unit (expr info e2) in
ML.mk_expr ml_let (ML.I e.e_ity) eff
| Elet (LDvar (_pvs, e1), e2) when e_ghost e1 ->
(* let ml_let = ML.ml_let_var pvs ML.mk_unit (expr info e2) in *)
expr info e2
(* ML.mk_expr ml_let (ML.I e.e_ity) eff *)
| Elet (LDvar (pvs, e1), e2) ->
let ml_let = ML.ml_let_var pvs (expr info e1) (expr info e2) in
ML.mk_expr ml_let (ML.I e.e_ity) eff
......@@ -568,10 +569,13 @@ module Transform = struct
match e.e_node with
| 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 = Econst _} as e1)), e2)
| Elet (Lvar (pv, ({e_node = Eblock []} as e1)), e2) ->
add_subst pv e1 e2
| Elet (Lvar (pv, ({e_node = Eapp (rs, [])} as e1)), e2)
when Translate.isconstructor info rs ->
(* only optimize constructors with no argument *)
(* as it is a Lvar the constructor is not completely applied *)
add_subst pv e1 e2
| Elet (ld, e) ->
mk (Elet (let_def info subst ld, expr info subst e))
......
......@@ -272,7 +272,7 @@ module Print = struct
fprintf fmt "@[<hov 2>let %a =@ %a@]"
(print_lident info) (pv_name pv) (print_expr info) e;
| Lsym (rs, args, ef) ->
fprintf fmt "@[<hov 2>let %a %a@ =@ @[%a@]@]"
fprintf fmt "@[<hov 2>let %a@ @[%a@]@ =@ @[%a@]@]"
(print_lident info) rs.rs_name
(print_list space (print_vs_arg info)) args
(print_expr info) ef;
......@@ -416,13 +416,13 @@ module Print = struct
forget_tvs ();
fprintf fmt "@\n@\n"
| Dtype dl ->
print_list newline (print_type_decl info) fmt dl;
fprintf fmt "@\n@\n"
print_list newline (print_type_decl info) fmt dl;
fprintf fmt "@\n@\n"
| Dexn (xs, None) ->
fprintf fmt "exception %a@\n@\n" print_ident xs.xs_name
| Dexn (xs, Some t) ->
fprintf fmt "@[<hov 2>exception %a of %a@]@\n@\n"
print_ident xs.xs_name (print_ty ~paren:true info) t
fprintf fmt "@[<hov 2>exception %a of %a@]@\n@\n"
print_ident xs.xs_name (print_ty ~paren:true info) t
end
let extract_module pargs ?old fmt ({mod_theory = th} as m) =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment