summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tests/misc/External.Funs.fst49
-rw-r--r--tests/misc/External.Opaque.fsti4
2 files changed, 46 insertions, 7 deletions
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index 57e9deee..21a389ca 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -15,14 +15,13 @@ let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
end
(** [external::swap] *)
-let swap_back
- (t : Type0) (x : t) (y : t) (st : state) : result (state & (t & t)) =
+let swap_back (t : Type0) (x : t) (y : t) (st : state) : result (t & t) =
begin match core_mem_swap_back0 t x y st with
| Fail -> Fail
- | Return (st0, x0) ->
- begin match core_mem_swap_back1 t x y st0 with
+ | Return x0 ->
+ begin match core_mem_swap_back1 t x y st with
| Fail -> Fail
- | Return (st1, y0) -> Return (st1, (x0, y0))
+ | Return y0 -> Return (x0, y0)
end
end
@@ -48,3 +47,43 @@ let test_vec_fwd (st : state) : result (state & unit) =
| Return _ -> Return (st, ())
end
+(** [external::custom_swap] *)
+let custom_swap_fwd
+ (t : Type0) (x : t) (y : t) (st : state) : result (state & t) =
+ begin match core_mem_swap_fwd t x y st with
+ | Fail -> Fail
+ | Return (st0, _) ->
+ begin match core_mem_swap_back0 t x y st with
+ | Fail -> Fail
+ | Return x0 -> Return (st0, x0)
+ end
+ end
+
+(** [external::custom_swap] *)
+let custom_swap_back
+ (t : Type0) (x : t) (y : t) (st : state) (ret : t) : result (t & t) =
+ begin match core_mem_swap_back0 t x y st with
+ | Fail -> Fail
+ | Return _ ->
+ begin match core_mem_swap_back1 t x y st with
+ | Fail -> Fail
+ | Return y0 -> Return (ret, y0)
+ end
+ end
+
+(** [external::test_custom_swap] *)
+let test_custom_swap_fwd
+ (x : u32) (y : u32) (st : state) : result (state & unit) =
+ begin match custom_swap_fwd u32 x y st with
+ | Fail -> Fail
+ | Return (st0, _) -> Return (st0, ())
+ end
+
+(** [external::test_custom_swap] *)
+let test_custom_swap_back
+ (x : u32) (y : u32) (st : state) : result (u32 & u32) =
+ begin match custom_swap_back u32 x y st 1 with
+ | Fail -> Fail
+ | Return (x0, y0) -> Return (x0, y0)
+ end
+
diff --git a/tests/misc/External.Opaque.fsti b/tests/misc/External.Opaque.fsti
index 59c90b6b..b13a46eb 100644
--- a/tests/misc/External.Opaque.fsti
+++ b/tests/misc/External.Opaque.fsti
@@ -10,10 +10,10 @@ include External.Types
val core_mem_swap_fwd (t : Type0) : t -> t -> state -> result (state & unit)
(** [core::mem::swap] *)
-val core_mem_swap_back0 (t : Type0) : t -> t -> state -> result (state & t)
+val core_mem_swap_back0 (t : Type0) : t -> t -> state -> result t
(** [core::mem::swap] *)
-val core_mem_swap_back1 (t : Type0) : t -> t -> state -> result (state & t)
+val core_mem_swap_back1 (t : Type0) : t -> t -> state -> result t
(** [core::num::nonzero::NonZeroU32::{14}::new] *)
val core_num_nonzero_non_zero_u32_14_new_fwd