From 9ba914479d792b673a90502fb55b0fa8a68202c7 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Thu, 11 Sep 2014 14:52:49 +0100
Subject: Adding support for extracting the information Christopher needs about
 an instruction

---
 src/lem_interp/instruction_extractor.lem | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 src/lem_interp/instruction_extractor.lem

(limited to 'src/lem_interp')

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
+  
-- 
cgit v1.2.3