From 558c5423c71fc725e3da91196c0b2a3cf994f42a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mpereira@lri.fr>
Date: Fri, 21 Sep 2018 19:07:45 +0200
Subject: [PATCH] Extraction: minor
---
src/mlw/compile.ml | 6 ++++--
src/mlw/mltree.ml | 6 ++++++
2 files changed, 10 insertions(+), 2 deletions(-)
diff --git a/src/mlw/compile.ml b/src/mlw/compile.ml
index 4588a078e..c31fccf31 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 15fb20f20..3c5dc72a4 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)
--
GitLab