From 64646f5a7105b4530d2f3d04ebc7d570d18c26f4 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 31 Jan 2018 15:38:21 +0000
Subject: Export arithmetic shift right from Lem library

---
 src/gen_lib/sail_operators.lem          |  1 +
 src/gen_lib/sail_operators_bitlists.lem | 18 ++++++++++--------
 src/gen_lib/sail_operators_mwords.lem   | 18 ++++++++++--------
 3 files changed, 21 insertions(+), 16 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3