summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_inter_imp.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
-rw-r--r--src/lem_interp/interp_inter_imp.lem8
1 files changed, 7 insertions, 1 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 3c076eae..cacbda62 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -54,7 +54,13 @@ let num_to_bits size kind num =
(Interp.V_tuple([Interp.V_lit(L_aux (L_num (integerFromNat size)) Interp_ast.Unknown);
Interp.V_lit(L_aux (L_num num) Interp_ast.Unknown)]))) with
| Interp.V_vector _ _ bits -> (to_bytes (from_bits bits)) end)
-end
+end
+
+let integer_of_byte_list bytes =
+ let intv = intern_value (Bytevector bytes) in
+ match Interp_lib.to_num false intv with
+ | Interp.V_lit (L_aux (L_num n) _) -> n
+ end
let extern_reg r slice = match (r,slice) with
| (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x