5 files changed, 33 insertions, 24 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 857a81a3..d35653c9 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -841,9 +841,12 @@ let interp mode (IState interp_state context) =
     | (o,_) -> o
 end 
 
-val state_to_outcome_s : forall 'v. interp_mode -> instruction_state -> Sail_impl_base.outcome_s instruction_state unit
-val outcome_to_outcome : interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome instruction_state unit
-let rec outcome_to_outcome mode = function
+val state_to_outcome_s : (instruction_state -> unit -> (string * string)) -> interp_mode -> instruction_state -> Sail_impl_base.outcome_s unit
+val outcome_to_outcome : (instruction_state -> unit -> (string * string)) -> interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome unit
+
+let rec outcome_to_outcome pp_instruction_state mode = 
+  let state_to_outcome_s = state_to_outcome_s pp_instruction_state in
+  function
   | Interp_interface.Read_mem rk addr size _ k ->
      Sail_impl_base.Read_mem (rk,addr,size) (fun v -> state_to_outcome_s mode (k v))
   | Interp_interface.Write_mem rk addr size _ mv _ k ->
@@ -876,16 +879,15 @@ let rec outcome_to_outcome mode = function
      failwith ("Interpreter error: " ^ message)
 end
 
-and state_to_outcome_s mode state = 
+and state_to_outcome_s pp_instruction_state mode state = 
   let next_outcome' = interp mode state in
-  let next_outcome = outcome_to_outcome mode next_outcome' in
-  (next_outcome, Just state)
-
+  let next_outcome = outcome_to_outcome pp_instruction_state mode next_outcome' in
+  (next_outcome, Just (pp_instruction_state state))
 
-let initial_outcome_s_of_instruction context mode instruction =
+val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit
+let initial_outcome_s_of_instruction pp_instruction_state context mode instruction =
   let state = instruction_to_istate context instruction in
-  let initial_outcome' = interp mode state in
-  (outcome_to_outcome mode initial_outcome',Just state)
+  state_to_outcome_s pp_instruction_state mode state
 
 
 (*Update slice potentially here*)
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index ea3ba154..b4a6c92b 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -202,5 +202,5 @@ val instruction_analysis :
   -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind)
 
 
-val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state unit
+val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit
 
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index ee67c2c7..760b0a35 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -3,7 +3,7 @@ open Interp_ast ;;
 open Sail_impl_base ;;
 open Interp_utilities ;;
 open Interp_interface ;;
-open Interp_inter_imp ;;
+
 
 open Nat_big_num ;;
 
@@ -498,3 +498,6 @@ let print_stack printer is = printer (instruction_stack_to_string is)
 let print_continuation printer (IState(stack,_)) = 
   let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env true e
 let print_instruction printer instr = printer (instruction_to_string instr)
+
+let pp_instruction_state state () =
+  (instruction_stack_to_string state,local_variables_to_string state)
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index 9eb89324..f629a307 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -71,3 +71,5 @@ val logfile_address_to_string : address -> string
 
 val byte_list_to_string : byte list -> string
 val bit_lifted_to_string : bit_lifted -> string
+
+val pp_instruction_state : instruction_state -> unit -> (string * string)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index e932282c..e29b3391 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -1,5 +1,5 @@
 open import Pervasives_extra
-open import Interp_ast (* only because the instruction type refers to base effect *)
+open import Interp_ast (* this can go away *)
             
 (* maybe isn't a member of type Ord - this should be in the Lem standard library*)
 instance forall 'a. Ord 'a => (Ord (maybe 'a))
@@ -415,30 +415,32 @@ they just have particular nias (and will be IK_simple *)
   | IK_simple
 
 (* the address_lifted types should go away here and be replaced by address *)
-type outcome 's 'a =
+type outcome 'a =
   (* Request to read memory, value is location to read, integer is size to read,
      followed by registers that were used in computing that size *)
-  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> outcome_s 's 'a)
+  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> outcome_s 'a)
   (* Tell the system a write is imminent, at address lifted, of size nat *)
-  | Write_ea of (write_kind * address_lifted * nat) * outcome_s 's 'a
+  | Write_ea of (write_kind * address_lifted * nat) * outcome_s 'a
   (* Request to write memory at last signalled address. Memory value should be 8
      times the size given in ea signal *)
-  | Write_memv of memory_value * (bool -> outcome_s 's 'a)
+  | Write_memv of memory_value * (bool -> outcome_s 'a)
   (* Request a memory barrier *)
-  | Barrier of barrier_kind * outcome_s 's 'a
+  | Barrier of barrier_kind * outcome_s 'a
   (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of outcome_s 's 'a
+  | Footprint of outcome_s 'a
   (* Request to read register, will track dependency when mode.track_values *)
-  | Read_reg of reg_name * (register_value -> outcome_s 's 'a)
+  | Read_reg of reg_name * (register_value -> outcome_s 'a)
   (* Request to write register *)
-  | Write_reg of (reg_name * register_value) * (outcome_s 's 'a)
-  | Escape of maybe string * maybe (outcome_s 's unit)
+  | Write_reg of (reg_name * register_value) * (outcome_s 'a)
+  | Escape of maybe string * maybe (outcome_s unit)
   (*Result of a failed assert with possible error message to report*)
   | Fail of maybe string
-  | Internal of (maybe string * maybe (unit -> string)) * outcome_s 's 'a
+  | Internal of (maybe string * maybe (unit -> string)) * outcome_s 'a
   | Done of 'a
   | Error of string
- and outcome_s 's 'a = outcome 's 'a * maybe 's
+ and outcome_s 'a = outcome 'a * maybe (unit -> (string * string))
+(* first string : output of instruction_stack_to_string
+   second string: output of local_variables_to_string *)
 
 let ~{ocaml} read_kindCompare rk1 rk2 =
   match (rk1, rk2) with