From 7e79a2adde6a75e33973a1cd559f85a47551b18a Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 11 Jul 2018 12:59:59 +0100
Subject: Partially revert change to add_vec_int et al

On second thought, this change should not really make a difference; the CHERI
test suite still passes without it.  Moreover, using unsigned conversion of the
vector argument leads to more convenient lemmas for the provers.
---
 src/gen_lib/sail2_operators_bitlists.lem | 26 +++++++++++++-------------
 src/gen_lib/sail2_operators_mwords.lem   | 26 +++++++++++++-------------
 2 files changed, 26 insertions(+), 26 deletions(-)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index b9a2fa86..186e0a09 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -145,19 +145,19 @@ let subs_vec  = arith_op_bv integerMinus true
 let mult_vec  = arith_op_double_bl integerMult false
 let mults_vec = arith_op_double_bl integerMult true
 
-val add_vec_int      : list bitU -> integer -> list bitU
-val sub_vec_int      : list bitU -> integer -> list bitU
-val mult_vec_int     : list bitU -> integer -> list bitU
-let add_vec_int  l r = arith_op_bv_int integerAdd true l r
-let sub_vec_int  l r = arith_op_bv_int integerMinus true l r
-let mult_vec_int l r = arith_op_double_bl integerMult true l (of_int (length l) r)
-
-val add_int_vec      : integer -> list bitU -> list bitU
-val sub_int_vec      : integer -> list bitU -> list bitU
-val mult_int_vec     : integer -> list bitU -> list bitU
-let add_int_vec  l r = arith_op_int_bv integerAdd true l r
-let sub_int_vec  l r = arith_op_int_bv integerMinus true l r
-let mult_int_vec l r = arith_op_double_bl integerMult true (of_int (length r) l) r
+val add_vec_int       : list bitU -> integer -> list bitU
+val sub_vec_int       : list bitU -> integer -> list bitU
+val mult_vec_int      : list bitU -> integer -> list bitU
+let add_vec_int   l r = arith_op_bv_int integerAdd false l r
+let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
+let mult_vec_int  l r = arith_op_double_bl integerMult false l (of_int (length l) r)
+
+val add_int_vec       : integer -> list bitU -> list bitU
+val sub_int_vec       : integer -> list bitU -> list bitU
+val mult_int_vec      : integer -> list bitU -> list bitU
+let add_int_vec   l r = arith_op_int_bv integerAdd false l r
+let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
+let mult_int_vec  l r = arith_op_double_bl integerMult false (of_int (length r) l) r
 
 val add_vec_bit      : list bitU -> bitU -> list bitU
 val adds_vec_bit     : list bitU -> bitU -> list bitU
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index c0b7f2d1..a7fb7c50 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -142,19 +142,19 @@ let subs_vec  l r = arith_op_bv integerMinus true  l r
 let mult_vec  l r = arith_op_bv integerMult  false (zeroExtend l : mword 'b) (zeroExtend r : mword 'b)
 let mults_vec l r = arith_op_bv integerMult  true  (signExtend l : mword 'b) (signExtend r : mword 'b)
 
-val add_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-val sub_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
-let add_vec_int  l r = arith_op_bv_int integerAdd   true  l r
-let sub_vec_int  l r = arith_op_bv_int integerMinus true  l r
-let mult_vec_int l r = arith_op_bv_int integerMult  true  (signExtend l : mword 'b) r
-
-val add_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
-val sub_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
-val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
-let add_int_vec  l r = arith_op_int_bv integerAdd   true  l r
-let sub_int_vec  l r = arith_op_int_bv integerMinus true  l r
-let mult_int_vec l r = arith_op_int_bv integerMult  true  l (signExtend r : mword 'b)
+val add_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val sub_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val mult_vec_int  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let add_vec_int   l r = arith_op_bv_int integerAdd   false l r
+let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
+let mult_vec_int  l r = arith_op_bv_int integerMult  false (zeroExtend l : mword 'b) r
+
+val add_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val sub_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val mult_int_vec  : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+let add_int_vec   l r = arith_op_int_bv integerAdd   false l r
+let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
+let mult_int_vec  l r = arith_op_int_bv integerMult  false l (zeroExtend r : mword 'b)
 
 val add_vec_bool  : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
 val adds_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
-- 
cgit v1.2.3