diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/arrays/Arrays.Funs.fst | 17 | ||||
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 6 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 6 | ||||
| -rw-r--r-- | tests/fstar/demo/Demo.fst | 2 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 3 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 6 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 35 |
7 files changed, 24 insertions, 51 deletions
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst index cf0f4f8b..15c82e93 100644 --- a/tests/fstar/arrays/Arrays.Funs.fst +++ b/tests/fstar/arrays/Arrays.Funs.fst @@ -23,8 +23,7 @@ let array_to_mut_slice_ (t : Type0) (s : array t 32) : result ((slice t) & (slice t -> result (array t 32))) = - let* (s1, to_slice_mut_back) = array_to_slice_mut t 32 s in - Return (s1, to_slice_mut_back) + array_to_slice_mut t 32 s (** [arrays::array_len]: Source: 'src/arrays.rs', lines 25:0-25:40 *) @@ -62,8 +61,7 @@ let index_mut_array (t : Type0) (s : array t 32) (i : usize) : result (t & (t -> result (array t 32))) = - let* (x, index_mut_back) = array_index_mut_usize t 32 s i in - Return (x, index_mut_back) + array_index_mut_usize t 32 s i (** [arrays::index_slice]: Source: 'src/arrays.rs', lines 56:0-56:46 *) @@ -76,8 +74,7 @@ let index_mut_slice (t : Type0) (s : slice t) (i : usize) : result (t & (t -> result (slice t))) = - let* (x, index_mut_back) = slice_index_mut_usize t s i in - Return (x, index_mut_back) + slice_index_mut_usize t s i (** [arrays::slice_subslice_shared_]: Source: 'src/arrays.rs', lines 64:0-64:70 *) @@ -110,8 +107,7 @@ let array_to_slice_mut_ (x : array u32 32) : result ((slice u32) & (slice u32 -> result (array u32 32))) = - let* (s, to_slice_mut_back) = array_to_slice_mut u32 32 x in - Return (s, to_slice_mut_back) + array_to_slice_mut u32 32 x (** [arrays::array_subslice_shared_]: Source: 'src/arrays.rs', lines 80:0-80:74 *) @@ -308,7 +304,7 @@ let take_array_t (a : array aB_t 2) : result unit = (** [arrays::non_copyable_array]: Source: 'src/arrays.rs', lines 229:0-229:27 *) let non_copyable_array : result unit = - let* _ = take_array_t (mk_array aB_t 2 [ AB_A; AB_B ]) in Return () + take_array_t (mk_array aB_t 2 [ AB_A; AB_B ]) (** [arrays::sum]: loop 0: Source: 'src/arrays.rs', lines 242:0-250:1 *) @@ -444,8 +440,7 @@ let rec iter_mut_slice_loop Tot (result unit) (decreases (iter_mut_slice_loop_decreases len i)) = if i < len - then - let* i1 = usize_add i 1 in let* _ = iter_mut_slice_loop len i1 in Return () + then let* i1 = usize_add i 1 in iter_mut_slice_loop len i1 else Return () (** [arrays::iter_mut_slice]: diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index ec042fb3..74044961 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -22,8 +22,7 @@ let betree_store_internal_node (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : result (state & unit) = - let* (st1, _) = betree_utils_store_internal_node id content st in - Return (st1, ()) + betree_utils_store_internal_node id content st (** [betree_main::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 *) @@ -37,8 +36,7 @@ let betree_store_leaf_node (id : u64) (content : betree_List_t (u64 & u64)) (st : state) : result (state & unit) = - let* (st1, _) = betree_utils_store_leaf_node id content st in - Return (st1, ()) + betree_utils_store_leaf_node id content st (** [betree_main::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 *) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index ec042fb3..74044961 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -22,8 +22,7 @@ let betree_store_internal_node (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : result (state & unit) = - let* (st1, _) = betree_utils_store_internal_node id content st in - Return (st1, ()) + betree_utils_store_internal_node id content st (** [betree_main::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 *) @@ -37,8 +36,7 @@ let betree_store_leaf_node (id : u64) (content : betree_List_t (u64 & u64)) (st : state) : result (state & unit) = - let* (st1, _) = betree_utils_store_leaf_node id content st in - Return (st1, ()) + betree_utils_store_leaf_node id content st (** [betree_main::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 *) diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst index 5651b80f..4ad7cb65 100644 --- a/tests/fstar/demo/Demo.fst +++ b/tests/fstar/demo/Demo.fst @@ -109,7 +109,7 @@ let list_nth_mut1 (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result (t & (t -> result (cList_t t))) = - let* (x, back_'a) = list_nth_mut1_loop t n l i in Return (x, back_'a) + list_nth_mut1_loop t n l i (** [demo::i32_id]: Source: 'src/demo.rs', lines 80:0-80:28 *) diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 447f9b49..7ca8b9c1 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -308,8 +308,7 @@ let hashMap_get_mut_in_list (t : Type0) (ls : list_t t) (key : usize) : result (t & (t -> result (list_t t))) = - let* (x, back_'a) = hashMap_get_mut_in_list_loop t ls key in - Return (x, back_'a) + hashMap_get_mut_in_list_loop t ls key (** [hashmap::{hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 *) diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index b16dcada..9b5baaeb 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -324,8 +324,7 @@ let hashmap_HashMap_get_mut_in_list (t : Type0) (ls : hashmap_List_t t) (key : usize) : result (t & (t -> result (hashmap_List_t t))) = - let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t ls key in - Return (x, back_'a) + hashmap_HashMap_get_mut_in_list_loop t ls key (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 *) @@ -446,8 +445,7 @@ let insert_on_disk (key : usize) (value : u64) (st : state) : result (state & unit) = let* (st1, hm) = hashmap_utils_deserialize st in let* hm1 = hashmap_HashMap_insert u64 hm key value in - let* (st2, _) = hashmap_utils_serialize hm1 st1 in - Return (st2, ()) + hashmap_utils_serialize hm1 st1 (** [hashmap_main::main]: Source: 'src/hashmap_main.rs', lines 16:0-16:13 *) diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 5f24fe7a..c87f693b 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -140,7 +140,7 @@ let list_nth_mut_loop (t : Type0) (ls : list_t t) (i : u32) : result (t & (t -> result (list_t t))) = - let* (x, back) = list_nth_mut_loop_loop t ls i in Return (x, back) + list_nth_mut_loop_loop t ls i (** [loops::list_nth_shared_loop]: loop 0: Source: 'src/loops.rs', lines 101:0-111:1 *) @@ -312,8 +312,7 @@ let list_nth_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t))) = - let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t ls0 ls1 i in - Return (p, back_'a, back_'b) + list_nth_mut_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_shared_loop_pair]: loop 0: Source: 'src/loops.rs', lines 208:0-229:1 *) @@ -376,8 +375,7 @@ let list_nth_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t)))) = - let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_mut_loop_pair_merge_loop t ls0 ls1 i (** [loops::list_nth_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 251:0-266:1 *) @@ -438,8 +436,7 @@ let list_nth_mut_shared_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_mut_shared_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 288:0-303:1 *) @@ -474,8 +471,7 @@ let list_nth_mut_shared_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'a) = list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i (** [loops::list_nth_shared_mut_loop_pair]: loop 0: Source: 'src/loops.rs', lines 307:0-322:1 *) @@ -509,8 +505,7 @@ let list_nth_shared_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t ls0 ls1 i in - Return (p, back_'b) + list_nth_shared_mut_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 326:0-341:1 *) @@ -545,8 +540,7 @@ let list_nth_shared_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'a) = list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i (** [loops::ignore_input_mut_borrow]: loop 0: Source: 'src/loops.rs', lines 345:0-349:1 *) @@ -555,10 +549,7 @@ let rec ignore_input_mut_borrow_loop Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i)) = if i > 0 - then - let* i1 = u32_sub i 1 in - let* _ = ignore_input_mut_borrow_loop i1 in - Return () + then let* i1 = u32_sub i 1 in ignore_input_mut_borrow_loop i1 else Return () (** [loops::ignore_input_mut_borrow]: @@ -573,10 +564,7 @@ let rec incr_ignore_input_mut_borrow_loop Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i)) = if i > 0 - then - let* i1 = u32_sub i 1 in - let* _ = incr_ignore_input_mut_borrow_loop i1 in - Return () + then let* i1 = u32_sub i 1 in incr_ignore_input_mut_borrow_loop i1 else Return () (** [loops::incr_ignore_input_mut_borrow]: @@ -593,10 +581,7 @@ let rec ignore_input_shared_borrow_loop Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i)) = if i > 0 - then - let* i1 = u32_sub i 1 in - let* _ = ignore_input_shared_borrow_loop i1 in - Return () + then let* i1 = u32_sub i 1 in ignore_input_shared_borrow_loop i1 else Return () (** [loops::ignore_input_shared_borrow]: |