diff options
author | Son Ho | 2022-11-09 18:04:03 +0100 |
---|---|---|
committer | Son HO | 2022-11-10 11:35:30 +0100 |
commit | 8b6f8e5fb85bcd1b3257550270c4c857d4ee7f55 (patch) | |
tree | b0090425eb850af3b5c8dc1d4f6aa1eafe2c8e1a /tests/misc | |
parent | b970183881379ff676b232e47e353e924de8cfdd (diff) |
Implement the generation of stateful backward functions (controlled by an option)
Diffstat (limited to 'tests/misc')
-rw-r--r-- | tests/misc/External.Funs.fst | 61 | ||||
-rw-r--r-- | tests/misc/External.Opaque.fsti | 6 |
2 files changed, 42 insertions, 25 deletions
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst index 874b739c..68a0061e 100644 --- a/tests/misc/External.Funs.fst +++ b/tests/misc/External.Funs.fst @@ -12,24 +12,31 @@ let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) = 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 + begin match core_mem_swap_back0 t x y st st0 with | Fail -> Fail - | Return _ -> - begin match core_mem_swap_back1 t x y st with + | Return (st1, _) -> + begin match core_mem_swap_back1 t x y st st1 with | Fail -> Fail - | Return _ -> Return (st0, ()) + | Return (st2, _) -> Return (st2, ()) end end end (** [external::swap] *) -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 +let swap_back + (t : Type0) (x : t) (y : t) (st : state) (st0 : state) : + result (state & (t & t)) + = + begin match core_mem_swap_fwd t x y st with | Fail -> Fail - | Return x0 -> - begin match core_mem_swap_back1 t x y st with + | Return (st1, _) -> + begin match core_mem_swap_back0 t x y st st1 with | Fail -> Fail - | Return y0 -> Return (x0, y0) + | Return (st2, x0) -> + begin match core_mem_swap_back1 t x y st st2 with + | Fail -> Fail + | Return (_, y0) -> Return (st0, (x0, y0)) + end end end @@ -64,25 +71,31 @@ let custom_swap_fwd 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 + begin match core_mem_swap_back0 t x y st st0 with | Fail -> Fail - | Return x0 -> - begin match core_mem_swap_back1 t x y st with + | Return (st1, x0) -> + begin match core_mem_swap_back1 t x y st st1 with | Fail -> Fail - | Return _ -> Return (st0, x0) + | Return (st2, _) -> Return (st2, x0) end 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 + (t : Type0) (x : t) (y : t) (st : state) (ret : t) (st0 : state) : + result (state & (t & t)) + = + begin match core_mem_swap_fwd t x y st with | Fail -> Fail - | Return _ -> - begin match core_mem_swap_back1 t x y st with + | Return (st1, _) -> + begin match core_mem_swap_back0 t x y st st1 with | Fail -> Fail - | Return y0 -> Return (ret, y0) + | Return (st2, _) -> + begin match core_mem_swap_back1 t x y st st2 with + | Fail -> Fail + | Return (_, y0) -> Return (st0, (ret, y0)) + end end end @@ -96,10 +109,12 @@ let test_custom_swap_fwd (** [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 + (x : u32) (y : u32) (st : state) (st0 : state) : + result (state & (u32 & u32)) + = + begin match custom_swap_back u32 x y st 1 st0 with | Fail -> Fail - | Return (x0, y0) -> Return (x0, y0) + | Return (st1, (x0, y0)) -> Return (st1, (x0, y0)) end (** [external::test_swap_non_zero] *) @@ -107,9 +122,9 @@ let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) = begin match swap_fwd u32 x 0 st with | Fail -> Fail | Return (st0, _) -> - begin match swap_back u32 x 0 st with + begin match swap_back u32 x 0 st st0 with | Fail -> Fail - | Return (x0, _) -> if x0 = 0 then Fail else Return (st0, x0) + | Return (st1, (x0, _)) -> if x0 = 0 then Fail else Return (st1, x0) end end diff --git a/tests/misc/External.Opaque.fsti b/tests/misc/External.Opaque.fsti index 7c241c7c..7d86405a 100644 --- a/tests/misc/External.Opaque.fsti +++ b/tests/misc/External.Opaque.fsti @@ -10,10 +10,12 @@ 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 t +val core_mem_swap_back0 + (t : Type0) : t -> t -> state -> state -> result (state & t) (** [core::mem::swap] *) -val core_mem_swap_back1 (t : Type0) : t -> t -> state -> result t +val core_mem_swap_back1 + (t : Type0) : t -> t -> state -> state -> result (state & t) (** [core::num::nonzero::NonZeroU32::{14}::new] *) val core_num_nonzero_non_zero_u32_new_fwd |