summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-10-24 17:48:02 +0200
committerSon Ho2023-10-24 17:48:02 +0200
commita1f3bbb50d44d7ba881b32b8b05b1474276c9a4d (patch)
tree41d21dae4d7e74614b002fe832dd081ac53a2ea6 /backends
parent6eebc66e34561bc6985b5866d49c8314a6fbaee9 (diff)
parentc3c7ca132b0dc0c4ea9205876932decda63baca1 (diff)
Merge branch 'son_traits' into son_traits_types
Diffstat (limited to '')
-rw-r--r--backends/fstar/Primitives.fst23
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;