Merge branch 'sail2' into rmem_interpreter

1 files changed, 19 insertions, 1 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index 3a1b0927..eed257fb 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -50,7 +50,25 @@ val "prerr_int" : (string, int) -> unit
 
 // ***** Integer shifts *****
 
-val shl_int = "shl_int" : (int, int) -> int
+/*!
+A common idiom in asl is to take two bits of an opcode and convert in into a variable like
+```
+let elsize = shl_int(8, UInt(size))
+```
+THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}`
+*/
+val _shl8 = {c: "shl_mach_int", _: "shl_int"} :
+  forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> {'m, 'm in {8, 16, 32, 64}. int('m)}
+
+/*!
+Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}`
+*/
+val _shl32 = {c: "shl_mach_int", _: "shl_int"} :
+  forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)}
+
+val _shl_int = "shl_int" : (int, int) -> int
+
+overload shl_int = {_shl8, _shl32, _shl_int}
 
 val shr_int = "shr_int" : (int, int) -> int