2 files changed, 50 insertions, 1 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 52e49999..e400ecec 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -506,7 +506,7 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
            (Interp.V_ctor (Id_aux (Id b) _) _ _ _) ->
             IK_barrier (match b with
                         | "Barrier_Sync" ->   Sync
-                        | "Barrier_Lwsync" -> LwSync
+                        | "Barrier_LwSync" -> LwSync
                         | "Barrier_Eieio" ->  Eieio
                         | "Barrier_Isync" ->  Isync
                         | "Barrier_DMB" ->    DMB
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 2850332e..bbff6a66 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -401,6 +401,17 @@ type read_kind =
   (* AArch64 reads *)
   | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
 
+instance (Show read_kind)
+  let show = function
+    | Read_plain -> "Read_plain"
+    | Read_tag -> "Read_tag"
+    | Read_reserve -> "Read_reserve"
+    | Read_acquire -> "Read_acquire"
+    | Read_exclusive_acquire -> "Read_exclusive_acquire"
+    | Read_stream -> "Read_stream"
+  end
+end
+
 type write_kind =
   (* common writes *)
     Write_plain
@@ -410,12 +421,40 @@ type write_kind =
   (* AArch64 writes *)
   | Write_release | Write_exclusive | Write_exclusive_release
 
+instance (Show write_kind)
+  let show = function
+    | Write_plain -> "Write_plain"
+    | Write_tag -> "Write_tag"
+    | Write_conditional -> "Write_conditional"
+    | Write_release -> "Write_release"
+    | Write_exclusive -> "Write_exclusive"
+    | Write_exclusive_release -> "Write_exclusive_release"
+  end
+end
+
 type barrier_kind =
   (* Power barriers *)
   Sync | LwSync | Eieio | Isync
   (* AArch64 barriers *)
   | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
 
+instance (Show barrier_kind)
+  let show = function
+    | Sync -> "Sync"
+    | LwSync -> "LwSync"
+    | Eieio -> "Eieio"
+    | Isync -> "Isync"
+    | DMB -> "DMB"
+    | DMB_ST -> "DMB_ST"
+    | DMB_LD -> "DMB_LD"
+    | DSB -> "DSB"
+    | DSB_ST -> "DSB_ST"
+    | DSB_LD -> "DSB_LD"
+    | ISB -> "ISB"
+  end
+end
+
+
 type instruction_kind = 
   | IK_barrier of barrier_kind 
   | IK_mem_read of read_kind 
@@ -427,6 +466,16 @@ they just have particular nias (and will be IK_simple *)
 (*  | IK_uncond_branch *)
   | IK_simple
 
+instance (Show instruction_kind)
+  let show = function
+    | IK_barrier bk -> "IK_barrier " ^ show bk
+    | IK_mem_read m -> "IK_mem_read " ^ show m
+    | IK_mem_write w -> "IK_mem_write " ^ show w
+    | IK_cond_branch -> "IK_cond_branch"
+    | IK_simple -> "IK_simple"
+  end
+end
+
 (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *)
 type external_functions = list (string * (Interp.value -> Interp.value))