diff --git a/src/mlw/compile.ml b/src/mlw/compile.ml index 4588a078e76b5af68dfcb0636cd3283b1bcd07ab..c31fccf31402dbf9fcef53772a8b6b493da18b23 100644 --- a/src/mlw/compile.ml +++ b/src/mlw/compile.ml @@ -256,11 +256,13 @@ module Translate = struct when isconstructor info rs && mask = MaskGhost -> ML.e_unit | Econst c -> Debug.dprintf debug_compile "compiling constant@."; + assert (mask = MaskVisible); let c = match c with Number.ConstInt c -> c | _ -> assert false in - ML.mk_expr (ML.Econst c) (ML.I e.e_ity) mask eff attrs + ML.e_const c (ML.I e.e_ity) mask eff attrs | Evar pv -> Debug.dprintf debug_compile "compiling variable %a@." print_pv pv; - ML.mk_expr (ML.Evar pv) (ML.I e.e_ity) mask eff attrs + assert (mask = MaskVisible); + ML.e_var pv (ML.I e.e_ity) mask eff attrs | Elet (LDvar (_, e1), e2) when e_ghost e1 -> expr info svar mask e2 | Elet (LDvar (_, e1), e2) when e_ghost e2 -> diff --git a/src/mlw/mltree.ml b/src/mlw/mltree.ml index 15fb20f20e47ffe73ade7fa26839522dd00ab3a0..3c5dc72a4ff0c7b54845b16486bffe6e3ce87c1f 100644 --- a/src/mlw/mltree.ml +++ b/src/mlw/mltree.ml @@ -299,6 +299,12 @@ let mk_its_defn its_name its_args its_private its_def = let e_unit = mk_expr enope (I Ity.ity_unit) MaskVisible Ity.eff_empty Sattr.empty +let e_const c = + mk_expr (Econst c) + +let e_var pv = + mk_expr (Evar pv) + let var_defn pv e = Lvar (pv, e)