3 files changed, 31 insertions, 6 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
+  
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 2115fa9f..a4581162 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -43,9 +43,9 @@ let lemnum default n = match n with
   | 32  -> "thirtytwo"
   | 35  -> "thirtyfive"
   | 39  -> "thirtynine"
-  | 40  -> "fourty"
-  | 47  -> "fourtyseven"
-  | 48  -> "fourtyeight"
+  | 40  -> "forty"
+  | 47  -> "fortyseven"
+  | 48  -> "fortyeight"
   | 55  -> "fiftyfive"
   | 56  -> "fiftysix"
   | 57  -> "fiftyseven"
diff --git a/src/process_file.ml b/src/process_file.ml
index 9586b6a6..b38ec0c5 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -183,9 +183,9 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
           Format.fprintf o "let thirtytwo  : integer = integerFromNat 32\n";
           Format.fprintf o "let thirtyfive : integer = integerFromNat 35\n";
           Format.fprintf o "let thirtynine : integer = integerFromNat 39\n";
-          Format.fprintf o "let fourty : integer = integerFromNat 40\n";
-          Format.fprintf o "let fourtyseven : integer = integerFromNat 47\n";
-          Format.fprintf o "let fourtyeight : integer = integerFromNat 48\n";
+          Format.fprintf o "let forty : integer = integerFromNat 40\n";
+          Format.fprintf o "let fortyseven : integer = integerFromNat 47\n";
+          Format.fprintf o "let fortyeight : integer = integerFromNat 48\n";
           Format.fprintf o "let fiftyfive  : integer = integerFromNat 55\n";
           Format.fprintf o "let fiftysix   : integer = integerFromNat 56\n";
           Format.fprintf o "let fiftyseven : integer = integerFromNat 57\n";