diff options
| author | Son Ho | 2023-10-24 17:48:02 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-24 17:48:02 +0200 |
| commit | a1f3bbb50d44d7ba881b32b8b05b1474276c9a4d (patch) | |
| tree | 41d21dae4d7e74614b002fe832dd081ac53a2ea6 /backends | |
| parent | 6eebc66e34561bc6985b5866d49c8314a6fbaee9 (diff) | |
| parent | c3c7ca132b0dc0c4ea9205876932decda63baca1 (diff) | |
Merge branch 'son_traits' into son_traits_types
Diffstat (limited to '')
| -rw-r--r-- | backends/fstar/Primitives.fst | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index e9391834..7d0845ed 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -100,6 +100,11 @@ type scalar_ty = | U64 | U128 +let is_unsigned = function +| Isize | I8 | I16 | I32 | I64 | I128 -> false +| Usize | U8 | U16 | U32 | U64 | U128 -> true + + let scalar_min (ty : scalar_ty) : int = match ty with | Isize -> isize_min @@ -162,6 +167,15 @@ let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = mk_scalar ty (x * y) +let scalar_lxor (#ty : scalar_ty { is_unsigned ty && ty <> Usize }) + (x : scalar ty) (y : scalar ty) : scalar ty = + match ty with + | U8 -> FStar.UInt.logxor #8 x y + | U16 -> FStar.UInt.logxor #16 x y + | U32 -> FStar.UInt.logxor #32 x y + | U64 -> FStar.UInt.logxor #64 x y + | U128 -> FStar.UInt.logxor #128 x y + (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = @@ -258,7 +272,7 @@ let u32_add = scalar_add #U32 let u64_add = scalar_add #U64 let u128_add = scalar_add #U128 -/// Substraction +/// Subtraction let isize_sub = scalar_sub #Isize let i8_sub = scalar_sub #I8 let i16_sub = scalar_sub #I16 @@ -286,6 +300,13 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +/// Logical operators, defined for unsigned types only, so far +let u8_xor = scalar_lxor #U8 +let u16_xor = scalar_lxor #U16 +let u32_xor = scalar_lxor #U32 +let u64_xor = scalar_lxor #U64 +let u128_xor = scalar_lxor #U128 + (*** Range *) type range (a : Type0) = { start : a; |