From 40dc7ff0fefce917b1a1a4f2d04514644a3c84cc Mon Sep 17 00:00:00 2001
From: Peter Sewell
Date: Sun, 23 Nov 2014 00:59:21 +0000
Subject: fight with interface/impl mismatch. lose.

---
 src/lem_interp/interp_inter_imp.lem | 6 +++---
 src/lem_interp/interp_interface.lem | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index df47a75e..4cce629c 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -411,18 +411,18 @@ let decode_to_istate top_level orig_value =
 end
 
 
-let decode_to_instruction top_level value = 
+let decode_to_instruction (top_level:context) (value:opcode) : instruction_or_decode_error  = 
   match decode_to_istate top_level value with
   | Instr inst is -> IDE_instr inst
   | Decode_error de -> IDE_decode_error de
   end
 
 
-let instruction_to_istate top_level ((name, parms, _) as instr) = 
+let instruction_to_istate (top_level:context) (((name, parms, _) as instr):instruction) : instruction_state  = 
   let mode = make_mode true false in
   let get_value (name,typ,v) = 
     let (e,_) = 
-      Interp.to_exp mode Interp.eenv (intern_reg_value (opcode_to_regval v 0 D_increasing)) in e in
+      Interp.to_exp mode Interp.eenv (intern_reg_value ((* SUSPICIOUS?*) opcode_to_regval v 0 D_increasing)) in e in
 (*  (Instr instr*)
     (Interp.Thunk_frame
        (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 6a70990b..da086524 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -350,7 +350,7 @@ val decode_to_istate : context -> opcode -> i_state_or_error
 val decode_to_instruction : context -> opcode -> instruction_or_decode_error
 
 (*Function to generate the state to run from an instruction form; is always an Instr*)
-val instruction_to_istate : context -> instruction -> i_state_or_error
+val instruction_to_istate : context -> instruction -> instruction_state (*i_state_or_error*)
 
 (* Augment an address by the given value *)
 (*val add_to_address : value -> integer -> value
-- 
cgit v1.2.3