diff options
| author | Robert Norton | 2018-03-06 13:30:59 +0000 |
|---|---|---|
| committer | Robert Norton | 2018-03-06 13:30:59 +0000 |
| commit | 9c4b4f66347196cd0511d3a2f8d4f0056592ee6f (patch) | |
| tree | a5e3b5257f24acf9a6527b78be3a405f8142212b /mips_new_tc | |
| parent | 542093c381ec57a72b6e71c1fc452f5221082f02 (diff) | |
overload shift operators so they can be used with integer shifts in cheri128 definitions.
Diffstat (limited to 'mips_new_tc')
| -rw-r--r-- | mips_new_tc/prelude.sail | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/mips_new_tc/prelude.sail b/mips_new_tc/prelude.sail index bd6be289..ca13753c 100644 --- a/mips_new_tc/prelude.sail +++ b/mips_new_tc/prelude.sail @@ -111,9 +111,6 @@ val __raw_SetSlice_bits : forall 'n 'w. val __raw_GetSlice_bits : forall 'n 'w. (atom('n), atom('w), bits('n), int) -> bits('w) -val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) -val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) - val __SignExtendSlice = {lem: "exts_slice"} : forall 'm. (bits('m), int, int) -> bits('m) val __ZeroExtendSlice = {lem: "extz_slice"} : forall 'm. (bits('m), int, int) -> bits('m) @@ -358,8 +355,14 @@ infix 1 >> infix 1 << infix 1 >>_s -val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) -val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) +val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) +val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) + +val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) +val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) + +overload operator >> = {shift_bits_right, shiftr} +overload operator << = {shift_bits_left, shiftl} val operator >>_s = "shift_bits_right_arith" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) infix 7 *_s |