make outcome_s contain the instruction state pretty print rather than the instruction state, factor out interpreter/shallow embedding value conversion

1 files changed, 14 insertions, 12 deletions

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