summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_interface.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
-rw-r--r--src/lem_interp/interp_interface.lem3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index dca329e9..446c716c 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -99,6 +99,8 @@ Follows the form of the instruction in instruction_extractor, but populates the
*)
type instruction = (string * list (string * instr_parm_typ * value) * list base_effect)
+type v_kind = Bitv | Bytev
+
type decode_error =
| Unsupported_instruction_error of instruction
| Not_an_instruction_error of value
@@ -108,6 +110,7 @@ type i_state_or_error =
| Instr of instruction * instruction_state
| Decode_error of decode_error
+val num_to_bits : nat -> v_kind -> integer
(*Function to decode an instruction and build the state to run it*)
val decode_to_istate : context -> value -> i_state_or_error