1 files changed, 20 insertions, 3 deletions

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index ce9cac1d..8db772c8 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -421,11 +421,17 @@ type barriers = list (string * barrier_kind)
 type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name))
 type memory_read = MR of read_kind * memory_parameter_transformer
 type memory_reads  = list (string * memory_read)
+type memory_write_ea = MEA of write_kind * memory_parameter_transformer
+type memory_write_eas = list (string * memory_write_ea)
 type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state))
 and memory_writes = list (string * memory_write)
+and memory_write_val = MV of maybe (instruction_state -> bool -> instruction_state)
+and memory_write_vals = list (string * memory_write_val)
 
 (* Definition information needed to run an instruction *)
-and context = Context of Interp.top_level * direction * memory_reads * memory_writes * barriers * external_functions
+and context =
+    Context of Interp.top_level * direction * 
+	memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * external_functions
 
 (* An instruction in flight *)
 and instruction_state = IState of interpreter_state * context
@@ -437,6 +443,10 @@ type outcome =
 | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) *  (memory_value -> instruction_state)
 (* Request to write memory, first value and dependent registers is location, second is the value to write *)
 | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state)
+(* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
+| Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * instruction_state
+(* Request to write memory at last signaled address. Memory value should be 8* the size given in ea signal *)
+| Write_memv of memory_value * maybe (list reg_name) * (bool -> instruction_state)
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
 (* Tell the system to dynamically recalculate dependency footprint *)
@@ -457,12 +467,14 @@ type outcome =
 type event = 
 | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
 | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
+| E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name)
+| E_write_memv of memory_value * maybe (list reg_name)
 | E_barrier of barrier_kind
 | E_footprint 
 | E_read_reg of reg_name
 | E_write_reg of reg_name * register_value
 | E_escape
-| E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*)
+| E_error of string 
 
 (* more explicit type classes to work around the occurrences of big_int in reg_name ::no longer necessary?*)
 
@@ -742,6 +754,9 @@ let ~{ocaml} eventCompare e1 e2 =
      compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
   | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> 
     compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
+  | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) ->
+    compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2))
+  | (E_write_memv mv1 tr1, E_write_memv mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
   | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2
   | (E_read_reg r1, E_read_reg r2) -> compare r1 r2
   | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2)
@@ -749,6 +764,8 @@ let ~{ocaml} eventCompare e1 e2 =
   | (E_escape,E_escape) -> EQ
   | (E_read_mem _ _ _ _, _) -> LT
   | (E_write_mem _ _ _ _ _ _, _) -> LT
+  | (E_write_ea _ _ _ _, _) -> LT
+  | (E_write_memv _ _, _) -> LT
   | (E_barrier _, _) -> LT
   | (E_read_reg _, _) -> LT
   | (E_write_reg _ _, _) -> LT
@@ -779,7 +796,7 @@ instance (SetType event)
 end
 
 (* Functions to build up the initial state for interpretation *)
-val build_context : specification -> memory_reads -> memory_writes -> barriers -> external_functions -> context 
+val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context 
 val initial_instruction_state : context -> string -> list register_value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)