From 15953e5a5277faeb49959ea498ffa10253d74751 Mon Sep 17 00:00:00 2001
From: Peter Sewell
Date: Thu, 30 Oct 2014 19:15:31 +0000
Subject: use proper equality on register name type

---
 src/lem_interp/interp_interface.lem | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'src/lem_interp/interp_interface.lem')

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 6561e588..dca329e9 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -29,12 +29,29 @@ type value =
 
 type slice = (integer * integer)
 
+
 type reg_name = 
 | Reg of string (*Name of the register, accessing the entire register*)
 | Reg_slice of string * slice (*Name of the register, accessing from the first to second integer of the slice*)
 | Reg_field of string * string * slice (*Name of the register, name of the field of the register accessed, the slice of the field*)
 | Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *)
 
+let reg_nameEqual r1 r2 = 
+  match (r1,r2) with
+  | (Reg s1, Reg s2) -> s1=s2
+  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> s1=s2 && sl1=sl2
+  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> s1=s2 && f1=f2 && sl1=sl2
+  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> s1=s2 && f1=f2 && sl1=sl2 && sl1'=sl2'
+  | _ -> false
+  end
+
+instance  (Eq reg_name)
+  let (=) = reg_nameEqual
+  let (<>) x y = not (reg_nameEqual x y)
+end
+
+
+
 type outcome =
 (* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values,
    integer is size to read, followed by registers that were used in computing that size *)
-- 
cgit v1.2.3