diff options
| author | Thomas Bauereiss | 2018-01-31 15:38:21 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-01-31 15:38:21 +0000 |
| commit | 64646f5a7105b4530d2f3d04ebc7d570d18c26f4 (patch) | |
| tree | 8bf9893210b6ddefa3a3245439d648cddd6eeea4 /src | |
| parent | 15c9ff0ae2fd00e716d41d5f874679465e918a14 (diff) | |
Export arithmetic shift right from Lem library
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 1 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_bitlists.lem | 18 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 18 |
3 files changed, 21 insertions, 16 deletions
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index b84e659d..ada91bd0 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -170,6 +170,7 @@ let shift_op_bv op v n = let shiftl_bv = shift_op_bv LL_shift (*"<<"*) let shiftr_bv = shift_op_bv RR_shift (*">>"*) +let arith_shiftr_bv = shift_op_bv RR_shift_arith let rotl_bv = shift_op_bv LL_rot (*"<<<"*) let rotr_bv = shift_op_bv LL_rot (*">>>"*) diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem index af683780..374628a4 100644 --- a/src/gen_lib/sail_operators_bitlists.lem +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -128,14 +128,16 @@ let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed let sub_overflow_vec_bit = sub_overflow_bv_bit let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed -val shiftl : list bitU -> integer -> list bitU -val shiftr : list bitU -> integer -> list bitU -val rotl : list bitU -> integer -> list bitU -val rotr : list bitU -> integer -> list bitU -let shiftl = shiftl_bv -let shiftr = shiftr_bv -let rotl = rotl_bv -let rotr = rotr_bv +val shiftl : list bitU -> integer -> list bitU +val shiftr : list bitU -> integer -> list bitU +val arith_shiftr : list bitU -> integer -> list bitU +val rotl : list bitU -> integer -> list bitU +val rotr : list bitU -> integer -> list bitU +let shiftl = shiftl_bv +let shiftr = shiftr_bv +let arith_shiftr = arith_shiftr_bv +let rotl = rotl_bv +let rotr = rotr_bv val mod_vec : list bitU -> list bitU -> list bitU val quot_vec : list bitU -> list bitU -> list bitU diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 3762eb7f..7fa09b9b 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -128,14 +128,16 @@ let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed let sub_overflow_vec_bit = sub_overflow_bv_bit let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed -val shiftl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -val shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -val rotl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -val rotr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -let shiftl = shiftl_bv -let shiftr = shiftr_bv -let rotl = rotl_bv -let rotr = rotr_bv +val shiftl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a +val shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a +val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a +val rotl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a +val rotr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a +let shiftl = shiftl_bv +let shiftr = shiftr_bv +let arith_shiftr = arith_shiftr_bv +let rotl = rotl_bv +let rotr = rotr_bv val mod_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a val quot_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a |