diff options
| author | Peter Sewell | 2014-10-30 19:15:31 +0000 |
|---|---|---|
| committer | Peter Sewell | 2014-10-30 19:20:27 +0000 |
| commit | 15953e5a5277faeb49959ea498ffa10253d74751 (patch) | |
| tree | 500240f0092f225a31929107fb428ca6682b8999 /src/lem_interp/interp_interface.lem | |
| parent | 74cc06dbe36e411133d392c846a9aff4b0a7df14 (diff) | |
use proper equality on register name type
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 17 |
1 files changed, 17 insertions, 0 deletions
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 *) |
