diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail2_operators_bitlists.lem | 38 | ||||
| -rw-r--r-- | src/gen_lib/sail2_operators_mwords.lem | 38 |
2 files changed, 26 insertions, 50 deletions
diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem index 0c833e90..b9a2fa86 100644 --- a/src/gen_lib/sail2_operators_bitlists.lem +++ b/src/gen_lib/sail2_operators_bitlists.lem @@ -145,31 +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 adds_vec_int : list bitU -> integer -> list bitU -val sub_vec_int : list bitU -> integer -> list bitU -val subs_vec_int : list bitU -> integer -> list bitU -val mult_vec_int : list bitU -> integer -> list bitU -val mults_vec_int : list bitU -> integer -> list bitU -let add_vec_int l r = arith_op_bv_int integerAdd false l r -let adds_vec_int l r = arith_op_bv_int integerAdd true l r -let sub_vec_int l r = arith_op_bv_int integerMinus false l r -let subs_vec_int l r = arith_op_bv_int integerMinus true l r -let mult_vec_int l r = arith_op_double_bl integerMult false l (of_int (length l) r) -let mults_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 adds_int_vec : integer -> list bitU -> list bitU -val sub_int_vec : integer -> list bitU -> list bitU -val subs_int_vec : integer -> list bitU -> list bitU -val mult_int_vec : integer -> list bitU -> list bitU -val mults_int_vec : integer -> list bitU -> list bitU -let add_int_vec l r = arith_op_int_bv integerAdd false l r -let adds_int_vec l r = arith_op_int_bv integerAdd true l r -let sub_int_vec l r = arith_op_int_bv integerMinus false l r -let subs_int_vec l r = arith_op_int_bv integerMinus true l r -let mult_int_vec l r = arith_op_double_bl integerMult false (of_int (length r) l) r -let mults_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 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_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 61048ac5..c0b7f2d1 100644 --- a/src/gen_lib/sail2_operators_mwords.lem +++ b/src/gen_lib/sail2_operators_mwords.lem @@ -142,31 +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 adds_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 subs_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 -val mults_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 adds_vec_int l r = arith_op_bv_int integerAdd true l r -let sub_vec_int l r = arith_op_bv_int integerMinus false l r -let subs_vec_int l r = arith_op_bv_int integerMinus true l r -let mult_vec_int l r = arith_op_bv_int integerMult false (zeroExtend l : mword 'b) r -let mults_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 adds_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 subs_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 -val mults_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 adds_int_vec l r = arith_op_int_bv integerAdd true l r -let sub_int_vec l r = arith_op_int_bv integerMinus false l r -let subs_int_vec l r = arith_op_int_bv integerMinus true l r -let mult_int_vec l r = arith_op_int_bv integerMult false l (zeroExtend r : mword 'b) -let mults_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 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_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a val adds_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a |