Adding support for extracting the information Christopher needs about an instruction

1 files changed, 25 insertions, 0 deletions

diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
new file mode 100644
index 00000000..6d8914c0
--- /dev/null
+++ b/src/lem_interp/instruction_extractor.lem
@@ -0,0 +1,25 @@
+open import Interp_ast
+import Interp
+
+type typ = 
+| Bit
+| Bitvector of maybe integer
+| Other
+
+type instruction = 
+|  Instr of string * list (string * typ) * list base_effect
+|  Skipped 
+
+val extract_instructions : string -> string -> defs tannot -> list instruction
+
+let extract_from_decode decoder = []
+
+let extract_effects instrs execute = instrs
+
+let extract_instructions decode_name execute_name defs = 
+  let (Just decoder) = Interp.find_function defs (Id_aux (Id decode_name) Unknown) in
+  let (Just executer) = Interp.find_function defs (Id_aux (Id execute_name) Unknown) in
+  let instr_no_effects = extract_from_decode decoder in
+  let instructions = extract_effects instr_no_effects executer in
+  instructions
+