From 32c017a6c326c4861ca6f548a9648cfb25af14e5 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Fri, 7 Nov 2014 13:16:48 +0000
Subject: Put back old num_to_bits temporarily; add in a num_to_bits_correct
 that treats the last argument as a big num

---
 src/lem_interp/interp_inter_imp.lem | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'src')

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 3c076eae..1227a4a8 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -44,6 +44,20 @@ let intern_value v = match v with
 end
 
 let num_to_bits size kind num =
+  match kind with
+    | Bitv -> Bitvector (match (Interp_lib.to_vec_inc 
+				  (Interp.V_tuple([Interp.V_lit(L_aux (L_num size) Interp_ast.Unknown);
+						   Interp.V_lit(L_aux (L_num (integerFromNat num)) Interp_ast.Unknown)]))) with
+	| Interp.V_vector _ _ bits -> from_bits bits end) true 0
+    | Bytev -> 
+      Bytevector (match (Interp_lib.to_vec_inc 
+			   (Interp.V_tuple([Interp.V_lit(L_aux (L_num size) Interp_ast.Unknown);
+					    Interp.V_lit(L_aux (L_num (integerFromNat num)) Interp_ast.Unknown)]))) with
+	| Interp.V_vector _ _ bits -> (to_bytes (from_bits bits)) end)
+end
+
+
+let num_to_bits_correct size kind num =
   match kind with
     | Bitv -> Bitvector (match (Interp_lib.to_vec_inc 
 				  (Interp.V_tuple([Interp.V_lit(L_aux (L_num (integerFromNat size)) Interp_ast.Unknown);
-- 
cgit v1.2.3