Treat integer casts in a general manner

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