summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKathy Gray2014-11-07 12:51:10 +0000
committerKathy Gray2014-11-07 12:51:10 +0000
commit508f89568b9e3b58453e59e97bc5224e17a89f46 (patch)
tree46d73d6feff020eada0e8bfcbc2a7b8973279f68
parentdfe5abc0f401ed4ddee997df67299dd586628977 (diff)
Fix types in num_to_bits
-rw-r--r--src/lem_interp/interp_inter_imp.lem12
-rw-r--r--src/lem_interp/interp_interface.lem2
2 files changed, 7 insertions, 7 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 45f91601..3c076eae 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -45,14 +45,14 @@ 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
+ | Bitv -> Bitvector (match (Interp_lib.to_vec_inc
+ (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 -> 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
+ Bytevector (match (Interp_lib.to_vec_inc
+ (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
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 93194fe2..2422ccc5 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -230,7 +230,7 @@ type i_state_or_error =
| Instr of instruction * instruction_state
| Decode_error of decode_error
-val num_to_bits : nat -> v_kind -> integer
+val num_to_bits : nat -> v_kind -> integer -> value
(** proposed: *)
val nat_to_bytevector : nat -> list word8