summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/betree/Primitives.fst4
-rw-r--r--tests/hashmap/Primitives.fst4
-rw-r--r--tests/hashmap_on_disk/Primitives.fst4
-rw-r--r--tests/misc/NoNestedBorrows.fst4
-rw-r--r--tests/misc/Primitives.fst4
5 files changed, 20 insertions, 0 deletions
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
index 77cf59aa..f73c8c09 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/betree/Primitives.fst
@@ -145,6 +145,10 @@ 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)
+(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+ mk_scalar tgt_ty x
+
/// The scalar types
type isize : eqtype = scalar Isize
type i8 : eqtype = scalar I8
diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst
index 77cf59aa..f73c8c09 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/hashmap/Primitives.fst
@@ -145,6 +145,10 @@ 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)
+(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+ mk_scalar tgt_ty x
+
/// The scalar types
type isize : eqtype = scalar Isize
type i8 : eqtype = scalar I8
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index 77cf59aa..f73c8c09 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/Primitives.fst
@@ -145,6 +145,10 @@ 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)
+(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+ mk_scalar tgt_ty x
+
/// The scalar types
type isize : eqtype = scalar Isize
type i8 : eqtype = scalar I8
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index c83656bf..97688191 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -54,6 +54,10 @@ let div_test1_fwd (x : u32) : result u32 =
let rem_test_fwd (x : u32) (y : u32) : result u32 =
begin match u32_rem x y with | Fail -> Fail | Return i -> Return i end
+(** [no_nested_borrows::cast_test] *)
+let cast_test_fwd (x : u32) : result i32 =
+ begin match scalar_cast I32 x with | Fail -> Fail | Return i -> Return i end
+
(** [no_nested_borrows::test2] *)
let test2_fwd : result unit = Return ()
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
index 77cf59aa..f73c8c09 100644
--- a/tests/misc/Primitives.fst
+++ b/tests/misc/Primitives.fst
@@ -145,6 +145,10 @@ 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)
+(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+ mk_scalar tgt_ty x
+
/// The scalar types
type isize : eqtype = scalar Isize
type i8 : eqtype = scalar I8