Commit ced60b99 authored by Mário Pereira's avatar Mário Pereira
Browse files

Code extraction (wip)

Erasure of ghost code in statements sequence
parent 54bfdf27
...@@ -346,6 +346,8 @@ module Translate = struct ...@@ -346,6 +346,8 @@ module Translate = struct
ML.mk_expr (ML.Econst c) (ML.I e.e_ity) eff ML.mk_expr (ML.Econst c) (ML.I e.e_ity) eff
| Evar pvs -> | Evar pvs ->
ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff
| Elet (LDvar (pvs, e1), e2) when is_underscore pvs && e_ghost e2 ->
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 -> | 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 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 -> | Elet (LDvar (pvs, e1), e2) when e_ghost e1 ->
...@@ -523,13 +525,13 @@ end ...@@ -523,13 +525,13 @@ end
(** Erasure operations related to ghost code *) (** Erasure operations related to ghost code *)
module Erasure = struct (* module Erasure = struct *)
open ML (* open ML *)
end (* end *)
(* (*
* Local Variables: * Local Variables:
......
...@@ -419,6 +419,7 @@ let extract_module pargs ?old fmt ({mod_theory = th} as m) = ...@@ -419,6 +419,7 @@ let extract_module pargs ?old fmt ({mod_theory = th} as m) =
info_mo_known_map = m.mod_known; info_mo_known_map = m.mod_known;
info_fname = None; (* TODO *) info_fname = None; (* TODO *)
} in } in
fprintf fmt "(*@\n%a@\n*)" print_module m;
fprintf fmt fprintf fmt
"(* This file has been generated from Why3 module %a *)@\n@\n" "(* This file has been generated from Why3 module %a *)@\n@\n"
Print.print_module_name m; Print.print_module_name m;
......
Supports Markdown
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