diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 133 | ||||
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 37 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 42 | ||||
| -rw-r--r-- | tests/coq/misc/Constants.v | 32 | ||||
| -rw-r--r-- | tests/coq/misc/External_Funs.v | 9 | ||||
| -rw-r--r-- | tests/coq/misc/Loops.v | 9 | ||||
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 38 | ||||
| -rw-r--r-- | tests/coq/misc/Paper.v | 8 | ||||
| -rw-r--r-- | tests/coq/misc/PoloniusList.v | 4 | ||||
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 236 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 239 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 86 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 83 | ||||
| -rw-r--r-- | tests/fstar/misc/Constants.fst | 48 | ||||
| -rw-r--r-- | tests/fstar/misc/External.Funs.fst | 12 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 16 | ||||
| -rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 53 | ||||
| -rw-r--r-- | tests/fstar/misc/Paper.fst | 15 | ||||
| -rw-r--r-- | tests/fstar/misc/PoloniusList.fst | 8 |
19 files changed, 245 insertions, 863 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index ddcff646..004db30e 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -15,9 +15,7 @@ Definition betree_load_internal_node_fwd (id : u64) (st : state) : result (state * (Betree_list_t (u64 * Betree_message_t))) := - p <- betree_utils_load_internal_node_fwd id st; - let (st0, l) := p in - Return (st0, l) + betree_utils_load_internal_node_fwd id st . (** [betree_main::betree::store_internal_node] *) @@ -33,9 +31,7 @@ Definition betree_store_internal_node_fwd (** [betree_main::betree::load_leaf_node] *) Definition betree_load_leaf_node_fwd (id : u64) (st : state) : result (state * (Betree_list_t (u64 * u64))) := - p <- betree_utils_load_leaf_node_fwd id st; - let (st0, l) := p in - Return (st0, l) + betree_utils_load_leaf_node_fwd id st . (** [betree_main::betree::store_leaf_node] *) @@ -55,7 +51,7 @@ Definition betree_fresh_node_id_fwd (counter : u64) : result u64 := (** [betree_main::betree::fresh_node_id] *) Definition betree_fresh_node_id_back (counter : u64) : result u64 := - counter0 <- u64_add counter 1%u64; Return counter0 + u64_add counter 1%u64 . (** [betree_main::betree::NodeIdCounter::{0}::new] *) @@ -97,11 +93,9 @@ Definition betree_upsert_update_fwd match st with | BetreeUpsertFunStateAdd v => margin <- u64_sub core_num_u64_max_c prev0; - if margin s>= v - then (i <- u64_add prev0 v; Return i) - else Return core_num_u64_max_c + if margin s>= v then u64_add prev0 v else Return core_num_u64_max_c | BetreeUpsertFunStateSub v => - if prev0 s>= v then (i <- u64_sub prev0 v; Return i) else Return (0%u64) + if prev0 s>= v then u64_sub prev0 v else Return (0%u64) end end . @@ -113,8 +107,7 @@ Fixpoint betree_list_len_fwd | O => Fail_ OutOfFuel | S n0 => match self with - | BetreeListCons t tl => - i <- betree_list_len_fwd T n0 tl; i0 <- u64_add 1%u64 i; Return i0 + | BetreeListCons t tl => i <- betree_list_len_fwd T n0 tl; u64_add 1%u64 i | BetreeListNil => Return (0%u64) end end @@ -258,8 +251,7 @@ Definition betree_leaf_split_back let (st0, _) := p1 in p2 <- betree_store_leaf_node_fwd id1 content1 st0; let (_, _) := p2 in - node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0; - Return node_id_cnt1 + betree_node_id_counter_fresh_id_back node_id_cnt0 . (** [betree_main::betree::Node::{5}::lookup_in_bindings] *) @@ -278,7 +270,7 @@ Fixpoint betree_node_lookup_in_bindings_fwd else if i s> key then Return None - else (opt <- betree_node_lookup_in_bindings_fwd n0 key tl; Return opt) + else betree_node_lookup_in_bindings_fwd n0 key tl | BetreeListNil => Return None end end @@ -297,9 +289,7 @@ Fixpoint betree_node_lookup_first_message_for_key_fwd let (i, m) := x in if i s>= key then Return (BetreeListCons (i, m) next_msgs) - else ( - l <- betree_node_lookup_first_message_for_key_fwd n0 key next_msgs; - Return l) + else betree_node_lookup_first_message_for_key_fwd n0 key next_msgs | BetreeListNil => Return BetreeListNil end end @@ -348,9 +338,7 @@ Fixpoint betree_node_apply_upserts_fwd | BetreeMessageUpsert s => v <- betree_upsert_update_fwd prev s; msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs; - p <- betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st; - let (st0, i) := p in - Return (st0, i) + betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st end) else ( p <- core_option_option_unwrap_fwd u64 prev st; @@ -383,16 +371,13 @@ Fixpoint betree_node_apply_upserts_back | BetreeMessageUpsert s => v <- betree_upsert_update_fwd prev s; msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs; - msgs1 <- betree_node_apply_upserts_back n0 msgs0 (Some v) key st; - Return msgs1 + betree_node_apply_upserts_back n0 msgs0 (Some v) key st end) else ( p <- core_option_option_unwrap_fwd u64 prev st; let (_, v) := p in - msgs0 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, - BetreeMessageInsert v); - Return msgs0) + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, + BetreeMessageInsert v)) end . @@ -556,14 +541,8 @@ with betree_internal_lookup_in_children_fwd | O => Fail_ OutOfFuel | S n0 => if key s< self.(Betree_internal_pivot) - then ( - p <- betree_node_lookup_fwd n0 self.(Betree_internal_left) key st; - let (st0, opt) := p in - Return (st0, opt)) - else ( - p <- betree_node_lookup_fwd n0 self.(Betree_internal_right) key st; - let (st0, opt) := p in - Return (st0, opt)) + then betree_node_lookup_fwd n0 self.(Betree_internal_left) key st + else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st end (** [betree_main::betree::Internal::{4}::lookup_in_children] *) @@ -599,7 +578,7 @@ Fixpoint betree_node_lookup_mut_in_bindings_fwd let (i, i0) := hd in if i s>= key then Return (BetreeListCons (i, i0) tl) - else (l <- betree_node_lookup_mut_in_bindings_fwd n0 key tl; Return l) + else betree_node_lookup_mut_in_bindings_fwd n0 key tl | BetreeListNil => Return BetreeListNil end end @@ -643,43 +622,31 @@ Definition betree_node_apply_to_leaf_fwd_back bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; bindings2 <- betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); - bindings3 <- - betree_node_lookup_mut_in_bindings_back n key bindings bindings2; - Return bindings3 + betree_node_lookup_mut_in_bindings_back n key bindings bindings2 | BetreeMessageDelete => bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; - bindings2 <- - betree_node_lookup_mut_in_bindings_back n key bindings bindings1; - Return bindings2 + betree_node_lookup_mut_in_bindings_back n key bindings bindings1 | BetreeMessageUpsert s => let (_, i) := hd in v <- betree_upsert_update_fwd (Some i) s; bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; bindings2 <- betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); - bindings3 <- - betree_node_lookup_mut_in_bindings_back n key bindings bindings2; - Return bindings3 + betree_node_lookup_mut_in_bindings_back n key bindings bindings2 end) else match new_msg with | BetreeMessageInsert v => bindings1 <- betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); - bindings2 <- - betree_node_lookup_mut_in_bindings_back n key bindings bindings1; - Return bindings2 + betree_node_lookup_mut_in_bindings_back n key bindings bindings1 | BetreeMessageDelete => - bindings1 <- - betree_node_lookup_mut_in_bindings_back n key bindings bindings0; - Return bindings1 + betree_node_lookup_mut_in_bindings_back n key bindings bindings0 | BetreeMessageUpsert s => v <- betree_upsert_update_fwd None s; bindings1 <- betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); - bindings2 <- - betree_node_lookup_mut_in_bindings_back n key bindings bindings1; - Return bindings2 + betree_node_lookup_mut_in_bindings_back n key bindings bindings1 end . @@ -696,9 +663,7 @@ Fixpoint betree_node_apply_messages_to_leaf_fwd_back | BetreeListCons new_msg new_msgs_tl => let (i, m) := new_msg in bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m; - bindings1 <- - betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl; - Return bindings1 + betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl | BetreeListNil => Return bindings end end @@ -720,8 +685,7 @@ Fixpoint betree_node_filter_messages_for_key_fwd_back msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) (BetreeListCons (k, m) l); - msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; - Return msgs1) + betree_node_filter_messages_for_key_fwd_back n0 key msgs0) else Return (BetreeListCons (k, m) l) | BetreeListNil => Return BetreeListNil end @@ -740,9 +704,7 @@ Fixpoint betree_node_lookup_first_message_after_key_fwd | BetreeListCons p next_msgs => let (k, m) := p in if k s= key - then ( - l <- betree_node_lookup_first_message_after_key_fwd n0 key next_msgs; - Return l) + then betree_node_lookup_first_message_after_key_fwd n0 key next_msgs else Return (BetreeListCons (k, m) next_msgs) | BetreeListNil => Return BetreeListNil end @@ -788,15 +750,13 @@ Definition betree_node_apply_to_internal_fwd_back msgs2 <- betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, BetreeMessageInsert i); - msgs3 <- betree_node_lookup_first_message_for_key_back n key msgs msgs2; - Return msgs3 + betree_node_lookup_first_message_for_key_back n key msgs msgs2 | BetreeMessageDelete => msgs1 <- betree_node_filter_messages_for_key_fwd_back n key msgs0; msgs2 <- betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, BetreeMessageDelete); - msgs3 <- betree_node_lookup_first_message_for_key_back n key msgs msgs2; - Return msgs3 + betree_node_lookup_first_message_for_key_back n key msgs msgs2 | BetreeMessageUpsert s => p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0; let (_, m) := p in @@ -807,18 +767,14 @@ Definition betree_node_apply_to_internal_fwd_back msgs2 <- betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, BetreeMessageInsert v); - msgs3 <- - betree_node_lookup_first_message_for_key_back n key msgs msgs2; - Return msgs3 + betree_node_lookup_first_message_for_key_back n key msgs msgs2 | BetreeMessageDelete => v <- betree_upsert_update_fwd None s; msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; msgs2 <- betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, BetreeMessageInsert v); - msgs3 <- - betree_node_lookup_first_message_for_key_back n key msgs msgs2; - Return msgs3 + betree_node_lookup_first_message_for_key_back n key msgs msgs2 | BetreeMessageUpsert ufs => msgs1 <- betree_node_lookup_first_message_after_key_fwd n key msgs0; msgs2 <- @@ -826,17 +782,14 @@ Definition betree_node_apply_to_internal_fwd_back BetreeMessageUpsert s); msgs3 <- betree_node_lookup_first_message_after_key_back n key msgs0 msgs2; - msgs4 <- - betree_node_lookup_first_message_for_key_back n key msgs msgs3; - Return msgs4 + betree_node_lookup_first_message_for_key_back n key msgs msgs3 end end else ( msgs1 <- betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key, new_msg); - msgs2 <- betree_node_lookup_first_message_for_key_back n key msgs msgs1; - Return msgs2) + betree_node_lookup_first_message_for_key_back n key msgs msgs1) . (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) @@ -852,9 +805,7 @@ Fixpoint betree_node_apply_messages_to_internal_fwd_back | BetreeListCons new_msg new_msgs_tl => let (i, m) := new_msg in msgs0 <- betree_node_apply_to_internal_fwd_back n0 msgs i m; - msgs1 <- - betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl; - Return msgs1 + betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl | BetreeListNil => Return msgs end end @@ -1101,11 +1052,8 @@ Definition betree_node_apply_back result (Betree_node_t * Betree_node_id_counter_t) := let l := BetreeListNil in - p <- - betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons - (key, new_msg) l) st; - let (self0, node_id_cnt0) := p in - Return (self0, node_id_cnt0) + betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons + (key, new_msg) l) st . (** [betree_main::betree::BeTree::{6}::new] *) @@ -1169,8 +1117,7 @@ Definition betree_be_tree_insert_back (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : result Betree_be_tree_t := - self0 <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st; - Return self0 + betree_be_tree_apply_back n self key (BetreeMessageInsert value) st . (** [betree_main::betree::BeTree::{6}::delete] *) @@ -1190,8 +1137,7 @@ Definition betree_be_tree_delete_back (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : result Betree_be_tree_t := - self0 <- betree_be_tree_apply_back n self key BetreeMessageDelete st; - Return self0 + betree_be_tree_apply_back n self key BetreeMessageDelete st . (** [betree_main::betree::BeTree::{6}::upsert] *) @@ -1213,8 +1159,7 @@ Definition betree_be_tree_upsert_back (upd : Betree_upsert_fun_state_t) (st : state) : result Betree_be_tree_t := - self0 <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st; - Return self0 + betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st . (** [betree_main::betree::BeTree::{6}::lookup] *) @@ -1222,9 +1167,7 @@ Definition betree_be_tree_lookup_fwd (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : result (state * (option u64)) := - p <- betree_node_lookup_fwd n self.(Betree_be_tree_root) key st; - let (st0, opt) := p in - Return (st0, opt) + betree_node_lookup_fwd n self.(Betree_be_tree_root) key st . (** [betree_main::betree::BeTree::{6}::lookup] *) diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 17456d81..1ff3e576 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -24,8 +24,7 @@ Fixpoint hash_map_allocate_slots_fwd else ( slots0 <- vec_push_back (List_t T) slots ListNil; i <- usize_sub n0 1%usize; - v <- hash_map_allocate_slots_fwd T n1 slots0 i; - Return v) + hash_map_allocate_slots_fwd T n1 slots0 i) end . @@ -45,8 +44,7 @@ Definition hash_map_new_with_capacity_fwd (** [hashmap::HashMap::{0}::new] *) Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) := - hm <- hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize); - Return hm + hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize) . (** [hashmap::HashMap::{0}::clear_slots] *) @@ -62,8 +60,7 @@ Fixpoint hash_map_clear_slots_fwd_back then ( slots0 <- vec_index_mut_back (List_t T) slots i ListNil; i1 <- usize_add i 1%usize; - slots1 <- hash_map_clear_slots_fwd_back T n0 slots0 i1; - Return slots1) + hash_map_clear_slots_fwd_back T n0 slots0 i1) else Return slots end . @@ -93,7 +90,7 @@ Fixpoint hash_map_insert_in_list_fwd | ListCons ckey cvalue ls0 => if ckey s= key then Return false - else (b <- hash_map_insert_in_list_fwd T n0 key value ls0; Return b) + else hash_map_insert_in_list_fwd T n0 key value ls0 | ListNil => Return true end end @@ -158,8 +155,7 @@ Fixpoint hash_map_move_elements_from_list_fwd_back match ls with | ListCons k v tl => ntable0 <- hash_map_insert_no_resize_fwd_back T n0 ntable k v; - ntable1 <- hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl; - Return ntable1 + hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl | ListNil => Return ntable end end @@ -183,9 +179,7 @@ Fixpoint hash_map_move_elements_fwd_back let l0 := mem_replace_back (List_t T) l ListNil in slots0 <- vec_index_mut_back (List_t T) slots i l0; i1 <- usize_add i 1%usize; - p <- hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1; - let (ntable1, slots1) := p in - Return (ntable1, slots1)) + hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1) else Return (ntable, slots) end . @@ -221,7 +215,7 @@ Definition hash_map_insert_fwd_back self0 <- hash_map_insert_no_resize_fwd_back T n self key value; i <- hash_map_len_fwd T self0; if i s> self0.(Hash_map_max_load) - then (self1 <- hash_map_try_resize_fwd_back T n self0; Return self1) + then hash_map_try_resize_fwd_back T n self0 else Return self0 . @@ -235,7 +229,7 @@ Fixpoint hash_map_contains_key_in_list_fwd | ListCons ckey t ls0 => if ckey s= key then Return true - else (b <- hash_map_contains_key_in_list_fwd T n0 key ls0; Return b) + else hash_map_contains_key_in_list_fwd T n0 key ls0 | ListNil => Return false end end @@ -248,8 +242,7 @@ Definition hash_map_contains_key_fwd let i := vec_len (List_t T) self.(Hash_map_slots) in hash_mod <- usize_rem hash i; l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod; - b <- hash_map_contains_key_in_list_fwd T n key l; - Return b + hash_map_contains_key_in_list_fwd T n key l . (** [hashmap::HashMap::{0}::get_in_list] *) @@ -262,7 +255,7 @@ Fixpoint hash_map_get_in_list_fwd | ListCons ckey cvalue ls0 => if ckey s= key then Return cvalue - else (t <- hash_map_get_in_list_fwd T n0 key ls0; Return t) + else hash_map_get_in_list_fwd T n0 key ls0 | ListNil => Fail_ Failure end end @@ -275,8 +268,7 @@ Definition hash_map_get_fwd let i := vec_len (List_t T) self.(Hash_map_slots) in hash_mod <- usize_rem hash i; l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod; - t <- hash_map_get_in_list_fwd T n key l; - Return t + hash_map_get_in_list_fwd T n key l . (** [hashmap::HashMap::{0}::get_mut_in_list] *) @@ -289,7 +281,7 @@ Fixpoint hash_map_get_mut_in_list_fwd | ListCons ckey cvalue ls0 => if ckey s= key then Return cvalue - else (t <- hash_map_get_mut_in_list_fwd T n0 key ls0; Return t) + else hash_map_get_mut_in_list_fwd T n0 key ls0 | ListNil => Fail_ Failure end end @@ -322,8 +314,7 @@ Definition hash_map_get_mut_fwd let i := vec_len (List_t T) self.(Hash_map_slots) in hash_mod <- usize_rem hash i; l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; - t <- hash_map_get_mut_in_list_fwd T n key l; - Return t + hash_map_get_mut_in_list_fwd T n key l . (** [hashmap::HashMap::{0}::get_mut] *) @@ -356,7 +347,7 @@ Fixpoint hash_map_remove_from_list_fwd | ListCons i cvalue tl0 => Return (Some cvalue) | ListNil => Fail_ Failure end - else (opt <- hash_map_remove_from_list_fwd T n0 key tl; Return opt) + else hash_map_remove_from_list_fwd T n0 key tl | ListNil => Return None end end diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 295ec489..3eaaec8a 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -26,8 +26,7 @@ Fixpoint hashmap_hash_map_allocate_slots_fwd else ( slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil; i <- usize_sub n0 1%usize; - v <- hashmap_hash_map_allocate_slots_fwd T n1 slots0 i; - Return v) + hashmap_hash_map_allocate_slots_fwd T n1 slots0 i) end . @@ -48,9 +47,7 @@ Definition hashmap_hash_map_new_with_capacity_fwd (** [hashmap_main::hashmap::HashMap::{0}::new] *) Definition hashmap_hash_map_new_fwd (T : Type) (n : nat) : result (Hashmap_hash_map_t T) := - hm <- - hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize); - Return hm + hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize) . (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) @@ -66,8 +63,7 @@ Fixpoint hashmap_hash_map_clear_slots_fwd_back then ( slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil; i1 <- usize_add i 1%usize; - slots1 <- hashmap_hash_map_clear_slots_fwd_back T n0 slots0 i1; - Return slots1) + hashmap_hash_map_clear_slots_fwd_back T n0 slots0 i1) else Return slots end . @@ -102,8 +98,7 @@ Fixpoint hashmap_hash_map_insert_in_list_fwd | HashmapListCons ckey cvalue ls0 => if ckey s= key then Return false - else ( - b <- hashmap_hash_map_insert_in_list_fwd T n0 key value ls0; Return b) + else hashmap_hash_map_insert_in_list_fwd T n0 key value ls0 | HashmapListNil => Return true end end @@ -177,9 +172,7 @@ Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back match ls with | HashmapListCons k v tl => ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 ntable k v; - ntable1 <- - hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl; - Return ntable1 + hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl | HashmapListNil => Return ntable end end @@ -204,9 +197,7 @@ Fixpoint hashmap_hash_map_move_elements_fwd_back let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0; i1 <- usize_add i 1%usize; - p <- hashmap_hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1; - let (ntable1, slots1) := p in - Return (ntable1, slots1)) + hashmap_hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1) else Return (ntable, slots) end . @@ -245,7 +236,7 @@ Definition hashmap_hash_map_insert_fwd_back self0 <- hashmap_hash_map_insert_no_resize_fwd_back T n self key value; i <- hashmap_hash_map_len_fwd T self0; if i s> self0.(Hashmap_hash_map_max_load) - then (self1 <- hashmap_hash_map_try_resize_fwd_back T n self0; Return self1) + then hashmap_hash_map_try_resize_fwd_back T n self0 else Return self0 . @@ -259,8 +250,7 @@ Fixpoint hashmap_hash_map_contains_key_in_list_fwd | HashmapListCons ckey t ls0 => if ckey s= key then Return true - else ( - b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key ls0; Return b) + else hashmap_hash_map_contains_key_in_list_fwd T n0 key ls0 | HashmapListNil => Return false end end @@ -275,8 +265,7 @@ Definition hashmap_hash_map_contains_key_fwd let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in hash_mod <- usize_rem hash i; l <- vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; - b <- hashmap_hash_map_contains_key_in_list_fwd T n key l; - Return b + hashmap_hash_map_contains_key_in_list_fwd T n key l . (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) @@ -289,7 +278,7 @@ Fixpoint hashmap_hash_map_get_in_list_fwd | HashmapListCons ckey cvalue ls0 => if ckey s= key then Return cvalue - else (t <- hashmap_hash_map_get_in_list_fwd T n0 key ls0; Return t) + else hashmap_hash_map_get_in_list_fwd T n0 key ls0 | HashmapListNil => Fail_ Failure end end @@ -304,8 +293,7 @@ Definition hashmap_hash_map_get_fwd let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in hash_mod <- usize_rem hash i; l <- vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; - t <- hashmap_hash_map_get_in_list_fwd T n key l; - Return t + hashmap_hash_map_get_in_list_fwd T n key l . (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) @@ -318,7 +306,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_fwd | HashmapListCons ckey cvalue ls0 => if ckey s= key then Return cvalue - else (t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key ls0; Return t) + else hashmap_hash_map_get_mut_in_list_fwd T n0 key ls0 | HashmapListNil => Fail_ Failure end end @@ -354,8 +342,7 @@ Definition hashmap_hash_map_get_mut_fwd hash_mod <- usize_rem hash i; l <- vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; - t <- hashmap_hash_map_get_mut_in_list_fwd T n key l; - Return t + hashmap_hash_map_get_mut_in_list_fwd T n key l . (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) @@ -395,8 +382,7 @@ Fixpoint hashmap_hash_map_remove_from_list_fwd | HashmapListCons i cvalue tl0 => Return (Some cvalue) | HashmapListNil => Fail_ Failure end - else ( - opt <- hashmap_hash_map_remove_from_list_fwd T n0 key tl; Return opt) + else hashmap_hash_map_remove_from_list_fwd T n0 key tl | HashmapListNil => Return None end end diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index 7d3e5a34..acc15a13 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -23,10 +23,10 @@ Definition x2_body : result u32 := Return (3%u32). Definition x2_c : u32 := x2_body%global. (** [constants::incr] *) -Definition incr_fwd (n : u32) : result u32 := i <- u32_add n 1%u32; Return i. +Definition incr_fwd (n : u32) : result u32 := u32_add n 1%u32. (** [constants::X3] *) -Definition x3_body : result u32 := i <- incr_fwd (32%u32); Return i. +Definition x3_body : result u32 := incr_fwd (32%u32). Definition x3_c : u32 := x3_body%global. (** [constants::mk_pair0] *) @@ -47,15 +47,11 @@ Definition mk_pair1_fwd (x : u32) (y : u32) : result (Pair_t u32 u32) := . (** [constants::P0] *) -Definition p0_body : result (u32 * u32) := - p <- mk_pair0_fwd (0%u32) (1%u32); Return p -. +Definition p0_body : result (u32 * u32) := mk_pair0_fwd (0%u32) (1%u32). Definition p0_c : (u32 * u32) := p0_body%global. (** [constants::P1] *) -Definition p1_body : result (Pair_t u32 u32) := - p <- mk_pair1_fwd (0%u32) (1%u32); Return p -. +Definition p1_body : result (Pair_t u32 u32) := mk_pair1_fwd (0%u32) (1%u32). Definition p1_c : Pair_t u32 u32 := p1_body%global. (** [constants::P2] *) @@ -80,16 +76,14 @@ Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) := . (** [constants::Y] *) -Definition y_body : result (Wrap_t i32) := - w <- wrap_new_fwd i32 (2%i32); Return w -. +Definition y_body : result (Wrap_t i32) := wrap_new_fwd i32 (2%i32). Definition y_c : Wrap_t i32 := y_body%global. (** [constants::unwrap_y] *) Definition unwrap_y_fwd : result i32 := Return y_c.(Wrap_val). (** [constants::YVAL] *) -Definition yval_body : result i32 := i <- unwrap_y_fwd; Return i. +Definition yval_body : result i32 := unwrap_y_fwd. Definition yval_c : i32 := yval_body%global. (** [constants::get_z1::Z1] *) @@ -100,9 +94,7 @@ Definition get_z1_z1_c : i32 := get_z1_z1_body%global. Definition get_z1_fwd : result i32 := Return get_z1_z1_c. (** [constants::add] *) -Definition add_fwd (a : i32) (b : i32) : result i32 := - i <- i32_add a b; Return i -. +Definition add_fwd (a : i32) (b : i32) : result i32 := i32_add a b. (** [constants::Q1] *) Definition q1_body : result i32 := Return (5%i32). @@ -113,12 +105,12 @@ Definition q2_body : result i32 := Return q1_c. Definition q2_c : i32 := q2_body%global. (** [constants::Q3] *) -Definition q3_body : result i32 := i <- add_fwd q2_c (3%i32); Return i. +Definition q3_body : result i32 := add_fwd q2_c (3%i32). Definition q3_c : i32 := q3_body%global. (** [constants::get_z2] *) Definition get_z2_fwd : result i32 := - i <- get_z1_fwd; i0 <- add_fwd i q3_c; i1 <- add_fwd q1_c i0; Return i1 + i <- get_z1_fwd; i0 <- add_fwd i q3_c; add_fwd q1_c i0 . (** [constants::S1] *) @@ -126,7 +118,7 @@ Definition s1_body : result u32 := Return (6%u32). Definition s1_c : u32 := s1_body%global. (** [constants::S2] *) -Definition s2_body : result u32 := i <- incr_fwd s1_c; Return i. +Definition s2_body : result u32 := incr_fwd s1_c. Definition s2_c : u32 := s2_body%global. (** [constants::S3] *) @@ -134,9 +126,7 @@ Definition s3_body : result (Pair_t u32 u32) := Return p3_c. Definition s3_c : Pair_t u32 u32 := s3_body%global. (** [constants::S4] *) -Definition s4_body : result (Pair_t u32 u32) := - p <- mk_pair1_fwd (7%u32) (8%u32); Return p -. +Definition s4_body : result (Pair_t u32 u32) := mk_pair1_fwd (7%u32) (8%u32). Definition s4_c : Pair_t u32 u32 := s4_body%global. End Constants . diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index 3ddc1cf3..90390c1b 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -41,9 +41,7 @@ Definition test_new_non_zero_u32_fwd (x : u32) (st : state) : result (state * Core_num_nonzero_non_zero_u32_t) := p <- core_num_nonzero_non_zero_u32_new_fwd x st; let (st0, opt) := p in - p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0; - let (st1, nzu) := p0 in - Return (st1, nzu) + core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0 . (** [external::test_vec] *) @@ -94,10 +92,7 @@ Definition test_custom_swap_back (x : u32) (y : u32) (st : state) (st0 : state) : result (state * (u32 * u32)) := - p <- custom_swap_back u32 x y st (1%u32) st0; - let (st1, p0) := p in - let (x0, y0) := p0 in - Return (st1, (x0, y0)) + custom_swap_back u32 x y st (1%u32) st0 . (** [external::test_swap_non_zero] *) diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 48de76c2..b3f27546 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -25,10 +25,7 @@ Fixpoint list_nth_mut_loop_loop0_fwd | ListCons x tl => if i s= 0%u32 then Return x - else ( - i0 <- u32_sub i 1%u32; - t <- list_nth_mut_loop_loop0_fwd T n0 tl i0; - Return t) + else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop0_fwd T n0 tl i0) | ListNil => Fail_ Failure end end @@ -37,7 +34,7 @@ Fixpoint list_nth_mut_loop_loop0_fwd (** [loops::list_nth_mut_loop] *) Definition list_nth_mut_loop_fwd (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := - t <- list_nth_mut_loop_loop0_fwd T n ls i; Return t + list_nth_mut_loop_loop0_fwd T n ls i . (** [loops::list_nth_mut_loop] *) @@ -66,7 +63,7 @@ Definition list_nth_mut_loop_back (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) : result (List_t T) := - l <- list_nth_mut_loop_loop0_back T n ls i ret; Return l + list_nth_mut_loop_loop0_back T n ls i ret . End Loops . diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index a5f6126b..e91cf81a 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -46,37 +46,25 @@ Arguments SumLeft {T1} {T2} _. Arguments SumRight {T1} {T2} _. (** [no_nested_borrows::neg_test] *) -Definition neg_test_fwd (x : i32) : result i32 := i <- i32_neg x; Return i. +Definition neg_test_fwd (x : i32) : result i32 := i32_neg x. (** [no_nested_borrows::add_test] *) -Definition add_test_fwd (x : u32) (y : u32) : result u32 := - i <- u32_add x y; Return i -. +Definition add_test_fwd (x : u32) (y : u32) : result u32 := u32_add x y. (** [no_nested_borrows::subs_test] *) -Definition subs_test_fwd (x : u32) (y : u32) : result u32 := - i <- u32_sub x y; Return i -. +Definition subs_test_fwd (x : u32) (y : u32) : result u32 := u32_sub x y. (** [no_nested_borrows::div_test] *) -Definition div_test_fwd (x : u32) (y : u32) : result u32 := - i <- u32_div x y; Return i -. +Definition div_test_fwd (x : u32) (y : u32) : result u32 := u32_div x y. (** [no_nested_borrows::div_test1] *) -Definition div_test1_fwd (x : u32) : result u32 := - i <- u32_div x 2%u32; Return i -. +Definition div_test1_fwd (x : u32) : result u32 := u32_div x 2%u32. (** [no_nested_borrows::rem_test] *) -Definition rem_test_fwd (x : u32) (y : u32) : result u32 := - i <- u32_rem x y; Return i -. +Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y. (** [no_nested_borrows::cast_test] *) -Definition cast_test_fwd (x : u32) : result i32 := - i <- scalar_cast U32 I32 x; Return i -. +Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x. (** [no_nested_borrows::test2] *) Definition test2_fwd : result unit := @@ -261,8 +249,7 @@ Arguments TreeNode {T} _ _ _. (** [no_nested_borrows::list_length] *) Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 := match l with - | ListCons t l1 => - i <- list_length_fwd T l1; i0 <- u32_add 1%u32 i; Return i0 + | ListCons t l1 => i <- list_length_fwd T l1; u32_add 1%u32 i | ListNil => Return (0%u32) end . @@ -273,7 +260,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T := | ListCons x tl => if i s= 0%u32 then Return x - else (i0 <- u32_sub i 1%u32; t <- list_nth_shared_fwd T tl i0; Return t) + else (i0 <- u32_sub i 1%u32; list_nth_shared_fwd T tl i0) | ListNil => Fail_ Failure end . @@ -284,7 +271,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := | ListCons x tl => if i s= 0%u32 then Return x - else (i0 <- u32_sub i 1%u32; t <- list_nth_mut_fwd T tl i0; Return t) + else (i0 <- u32_sub i 1%u32; list_nth_mut_fwd T tl i0) | ListNil => Fail_ Failure end . @@ -308,7 +295,7 @@ Fixpoint list_nth_mut_back Fixpoint list_rev_aux_fwd (T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) := match li with - | ListCons hd tl => l <- list_rev_aux_fwd T tl (ListCons hd lo); Return l + | ListCons hd tl => list_rev_aux_fwd T tl (ListCons hd lo) | ListNil => Return lo end . @@ -316,8 +303,7 @@ Fixpoint list_rev_aux_fwd (** [no_nested_borrows::list_rev] *) Definition list_rev_fwd_back (T : Type) (l : List_t T) : result (List_t T) := let li := mem_replace_fwd (List_t T) l ListNil in - l0 <- list_rev_aux_fwd T li ListNil; - Return l0 + list_rev_aux_fwd T li ListNil . (** [no_nested_borrows::test_list_functions] *) diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 616eed37..cb4486c6 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -7,9 +7,7 @@ Local Open Scope Primitives_scope. Module Paper. (** [paper::ref_incr] *) -Definition ref_incr_fwd_back (x : i32) : result i32 := - x0 <- i32_add x 1%i32; Return x0 -. +Definition ref_incr_fwd_back (x : i32) : result i32 := i32_add x 1%i32. (** [paper::test_incr] *) Definition test_incr_fwd : result unit := @@ -63,7 +61,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := | ListCons x tl => if i s= 0%u32 then Return x - else (i0 <- u32_sub i 1%u32; t <- list_nth_mut_fwd T tl i0; Return t) + else (i0 <- u32_sub i 1%u32; list_nth_mut_fwd T tl i0) | ListNil => Fail_ Failure end . @@ -86,7 +84,7 @@ Fixpoint list_nth_mut_back (** [paper::sum] *) Fixpoint sum_fwd (l : List_t i32) : result i32 := match l with - | ListCons x tl => i <- sum_fwd tl; i0 <- i32_add x i; Return i0 + | ListCons x tl => i <- sum_fwd tl; i32_add x i | ListNil => Return (0%i32) end . diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v index a45c77c5..bd6df02e 100644 --- a/tests/coq/misc/PoloniusList.v +++ b/tests/coq/misc/PoloniusList.v @@ -19,9 +19,7 @@ Arguments ListNil {T}. Fixpoint get_list_at_x_fwd (ls : List_t u32) (x : u32) : result (List_t u32) := match ls with | ListCons hd tl => - if hd s= x - then Return (ListCons hd tl) - else (l <- get_list_at_x_fwd tl x; Return l) + if hd s= x then Return (ListCons hd tl) else get_list_at_x_fwd tl x | ListNil => Return ListNil end . diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index f4ba7927..628eb2c3 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -13,10 +13,7 @@ let betree_load_internal_node_fwd (id : u64) (st : state) : result (state & (betree_list_t (u64 & betree_message_t))) = - begin match betree_utils_load_internal_node_fwd id st with - | Fail e -> Fail e - | Return (st0, l) -> Return (st0, l) - end + betree_utils_load_internal_node_fwd id st (** [betree_main::betree::store_internal_node] *) let betree_store_internal_node_fwd @@ -31,10 +28,7 @@ let betree_store_internal_node_fwd (** [betree_main::betree::load_leaf_node] *) let betree_load_leaf_node_fwd (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) = - begin match betree_utils_load_leaf_node_fwd id st with - | Fail e -> Fail e - | Return (st0, l) -> Return (st0, l) - end + betree_utils_load_leaf_node_fwd id st (** [betree_main::betree::store_leaf_node] *) let betree_store_leaf_node_fwd @@ -54,11 +48,7 @@ let betree_fresh_node_id_fwd (counter : u64) : result u64 = end (** [betree_main::betree::fresh_node_id] *) -let betree_fresh_node_id_back (counter : u64) : result u64 = - begin match u64_add counter 1 with - | Fail e -> Fail e - | Return counter0 -> Return counter0 - end +let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1 (** [betree_main::betree::NodeIdCounter::{0}::new] *) let betree_node_id_counter_new_fwd : result betree_node_id_counter_t = @@ -99,22 +89,10 @@ let betree_upsert_update_fwd begin match u64_sub core_num_u64_max_c prev0 with | Fail e -> Fail e | Return margin -> - if margin >= v - then - begin match u64_add prev0 v with - | Fail e -> Fail e - | Return i -> Return i - end - else Return core_num_u64_max_c + if margin >= v then u64_add prev0 v else Return core_num_u64_max_c end | BetreeUpsertFunStateSub v -> - if prev0 >= v - then - begin match u64_sub prev0 v with - | Fail e -> Fail e - | Return i -> Return i - end - else Return 0 + if prev0 >= v then u64_sub prev0 v else Return 0 end end @@ -127,11 +105,7 @@ let rec betree_list_len_fwd | BetreeListCons x tl -> begin match betree_list_len_fwd t tl with | Fail e -> Fail e - | Return i -> - begin match u64_add 1 i with - | Fail e -> Fail e - | Return i0 -> Return i0 - end + | Return i -> u64_add 1 i end | BetreeListNil -> Return 0 end @@ -299,11 +273,7 @@ let betree_leaf_split_back begin match betree_store_leaf_node_fwd id1 content1 st0 with | Fail e -> Fail e | Return (_, _) -> - begin match betree_node_id_counter_fresh_id_back node_id_cnt0 - with - | Fail e -> Fail e - | Return node_id_cnt1 -> Return node_id_cnt1 - end + betree_node_id_counter_fresh_id_back node_id_cnt0 end end end @@ -326,11 +296,7 @@ let rec betree_node_lookup_in_bindings_fwd else if i > key then Return None - else - begin match betree_node_lookup_in_bindings_fwd key tl with - | Fail e -> Fail e - | Return opt -> Return opt - end + else betree_node_lookup_in_bindings_fwd key tl | BetreeListNil -> Return None end @@ -345,12 +311,7 @@ let rec betree_node_lookup_first_message_for_key_fwd let (i, m) = x in if i >= key then Return (BetreeListCons (i, m) next_msgs) - else - begin match betree_node_lookup_first_message_for_key_fwd key next_msgs - with - | Fail e -> Fail e - | Return l -> Return l - end + else betree_node_lookup_first_message_for_key_fwd key next_msgs | BetreeListNil -> Return BetreeListNil end @@ -402,11 +363,7 @@ let rec betree_node_apply_upserts_fwd betree_list_pop_front_back (u64 & betree_message_t) msgs with | Fail e -> Fail e | Return msgs0 -> - begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st - with - | Fail e -> Fail e - | Return (st0, i) -> Return (st0, i) - end + betree_node_apply_upserts_fwd msgs0 (Some v) key st end end end @@ -451,11 +408,7 @@ let rec betree_node_apply_upserts_back betree_list_pop_front_back (u64 & betree_message_t) msgs with | Fail e -> Fail e | Return msgs0 -> - begin match betree_node_apply_upserts_back msgs0 (Some v) key st - with - | Fail e -> Fail e - | Return msgs1 -> Return msgs1 - end + betree_node_apply_upserts_back msgs0 (Some v) key st end end end @@ -464,12 +417,8 @@ let rec betree_node_apply_upserts_back begin match core_option_option_unwrap_fwd u64 prev st with | Fail e -> Fail e | Return (_, v) -> - begin match - betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, - BetreeMessageInsert v) with - | Fail e -> Fail e - | Return msgs0 -> Return msgs0 - end + betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, + BetreeMessageInsert v) end end @@ -695,16 +644,8 @@ and betree_internal_lookup_in_children_fwd (decreases (betree_internal_lookup_in_children_decreases self key st)) = if key < self.betree_internal_pivot - then - begin match betree_node_lookup_fwd self.betree_internal_left key st with - | Fail e -> Fail e - | Return (st0, opt) -> Return (st0, opt) - end - else - begin match betree_node_lookup_fwd self.betree_internal_right key st with - | Fail e -> Fail e - | Return (st0, opt) -> Return (st0, opt) - end + then betree_node_lookup_fwd self.betree_internal_left key st + else betree_node_lookup_fwd self.betree_internal_right key st (** [betree_main::betree::Internal::{4}::lookup_in_children] *) and betree_internal_lookup_in_children_back @@ -739,11 +680,7 @@ let rec betree_node_lookup_mut_in_bindings_fwd let (i, i0) = hd in if i >= key then Return (BetreeListCons (i, i0) tl) - else - begin match betree_node_lookup_mut_in_bindings_fwd key tl with - | Fail e -> Fail e - | Return l -> Return l - end + else betree_node_lookup_mut_in_bindings_fwd key tl | BetreeListNil -> Return BetreeListNil end @@ -794,24 +731,14 @@ let betree_node_apply_to_leaf_fwd_back with | Fail e -> Fail e | Return bindings2 -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings - bindings2 with - | Fail e -> Fail e - | Return bindings3 -> Return bindings3 - end + betree_node_lookup_mut_in_bindings_back key bindings bindings2 end end | BetreeMessageDelete -> begin match betree_list_pop_front_back (u64 & u64) bindings0 with | Fail e -> Fail e | Return bindings1 -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - with - | Fail e -> Fail e - | Return bindings2 -> Return bindings2 - end + betree_node_lookup_mut_in_bindings_back key bindings bindings1 end | BetreeMessageUpsert s -> let (_, i) = hd in @@ -826,12 +753,8 @@ let betree_node_apply_to_leaf_fwd_back v) with | Fail e -> Fail e | Return bindings2 -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings - bindings2 with - | Fail e -> Fail e - | Return bindings3 -> Return bindings3 - end + betree_node_lookup_mut_in_bindings_back key bindings + bindings2 end end end @@ -844,19 +767,10 @@ let betree_node_apply_to_leaf_fwd_back betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with | Fail e -> Fail e | Return bindings1 -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - with - | Fail e -> Fail e - | Return bindings2 -> Return bindings2 - end + betree_node_lookup_mut_in_bindings_back key bindings bindings1 end | BetreeMessageDelete -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings bindings0 with - | Fail e -> Fail e - | Return bindings1 -> Return bindings1 - end + betree_node_lookup_mut_in_bindings_back key bindings bindings0 | BetreeMessageUpsert s -> begin match betree_upsert_update_fwd None s with | Fail e -> Fail e @@ -866,12 +780,7 @@ let betree_node_apply_to_leaf_fwd_back with | Fail e -> Fail e | Return bindings1 -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - with - | Fail e -> Fail e - | Return bindings2 -> Return bindings2 - end + betree_node_lookup_mut_in_bindings_back key bindings bindings1 end end end @@ -891,11 +800,7 @@ let rec betree_node_apply_messages_to_leaf_fwd_back begin match betree_node_apply_to_leaf_fwd_back bindings i m with | Fail e -> Fail e | Return bindings0 -> - begin match - betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with - | Fail e -> Fail e - | Return bindings1 -> Return bindings1 - end + betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl end | BetreeListNil -> Return bindings end @@ -915,11 +820,7 @@ let rec betree_node_filter_messages_for_key_fwd_back betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k, m) l) with | Fail e -> Fail e - | Return msgs0 -> - begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with - | Fail e -> Fail e - | Return msgs1 -> Return msgs1 - end + | Return msgs0 -> betree_node_filter_messages_for_key_fwd_back key msgs0 end else Return (BetreeListCons (k, m) l) | BetreeListNil -> Return BetreeListNil @@ -935,12 +836,7 @@ let rec betree_node_lookup_first_message_after_key_fwd | BetreeListCons p next_msgs -> let (k, m) = p in if k = key - then - begin match betree_node_lookup_first_message_after_key_fwd key next_msgs - with - | Fail e -> Fail e - | Return l -> Return l - end + then betree_node_lookup_first_message_after_key_fwd key next_msgs else Return (BetreeListCons (k, m) next_msgs) | BetreeListNil -> Return BetreeListNil end @@ -991,12 +887,7 @@ let betree_node_apply_to_internal_fwd_back (key, BetreeMessageInsert i) with | Fail e -> Fail e | Return msgs2 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs msgs2 - with - | Fail e -> Fail e - | Return msgs3 -> Return msgs3 - end + betree_node_lookup_first_message_for_key_back key msgs msgs2 end end | BetreeMessageDelete -> @@ -1009,12 +900,7 @@ let betree_node_apply_to_internal_fwd_back (key, BetreeMessageDelete) with | Fail e -> Fail e | Return msgs2 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs msgs2 - with - | Fail e -> Fail e - | Return msgs3 -> Return msgs3 - end + betree_node_lookup_first_message_for_key_back key msgs msgs2 end end | BetreeMessageUpsert s -> @@ -1037,12 +923,8 @@ let betree_node_apply_to_internal_fwd_back msgs1 (key, BetreeMessageInsert v) with | Fail e -> Fail e | Return msgs2 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - msgs2 with - | Fail e -> Fail e - | Return msgs3 -> Return msgs3 - end + betree_node_lookup_first_message_for_key_back key msgs + msgs2 end end end @@ -1060,12 +942,8 @@ let betree_node_apply_to_internal_fwd_back msgs1 (key, BetreeMessageInsert v) with | Fail e -> Fail e | Return msgs2 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - msgs2 with - | Fail e -> Fail e - | Return msgs3 -> Return msgs3 - end + betree_node_lookup_first_message_for_key_back key msgs + msgs2 end end end @@ -1084,12 +962,8 @@ let betree_node_apply_to_internal_fwd_back msgs2 with | Fail e -> Fail e | Return msgs3 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - msgs3 with - | Fail e -> Fail e - | Return msgs4 -> Return msgs4 - end + betree_node_lookup_first_message_for_key_back key msgs + msgs3 end end end @@ -1102,11 +976,7 @@ let betree_node_apply_to_internal_fwd_back new_msg) with | Fail e -> Fail e | Return msgs1 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs msgs1 with - | Fail e -> Fail e - | Return msgs2 -> Return msgs2 - end + betree_node_lookup_first_message_for_key_back key msgs msgs1 end end end @@ -1124,11 +994,7 @@ let rec betree_node_apply_messages_to_internal_fwd_back begin match betree_node_apply_to_internal_fwd_back msgs i m with | Fail e -> Fail e | Return msgs0 -> - begin match - betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with - | Fail e -> Fail e - | Return msgs1 -> Return msgs1 - end + betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl end | BetreeListNil -> Return msgs end @@ -1484,12 +1350,8 @@ let betree_node_apply_back result (betree_node_t & betree_node_id_counter_t) = let l = BetreeListNil in - begin match - betree_node_apply_messages_back self params node_id_cnt (BetreeListCons - (key, new_msg) l) st with - | Fail e -> Fail e - | Return (self0, node_id_cnt0) -> Return (self0, node_id_cnt0) - end + betree_node_apply_messages_back self params node_id_cnt (BetreeListCons (key, + new_msg) l) st (** [betree_main::betree::BeTree::{6}::new] *) let betree_be_tree_new_fwd @@ -1568,11 +1430,7 @@ let betree_be_tree_insert_back (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) : result betree_be_tree_t = - begin match betree_be_tree_apply_back self key (BetreeMessageInsert value) st - with - | Fail e -> Fail e - | Return self0 -> Return self0 - end + betree_be_tree_apply_back self key (BetreeMessageInsert value) st (** [betree_main::betree::BeTree::{6}::delete] *) let betree_be_tree_delete_fwd @@ -1591,10 +1449,7 @@ let betree_be_tree_delete_back (self : betree_be_tree_t) (key : u64) (st : state) : result betree_be_tree_t = - begin match betree_be_tree_apply_back self key BetreeMessageDelete st with - | Fail e -> Fail e - | Return self0 -> Return self0 - end + betree_be_tree_apply_back self key BetreeMessageDelete st (** [betree_main::betree::BeTree::{6}::upsert] *) let betree_be_tree_upsert_fwd @@ -1619,21 +1474,14 @@ let betree_be_tree_upsert_back (st : state) : result betree_be_tree_t = - begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st - with - | Fail e -> Fail e - | Return self0 -> Return self0 - end + betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st (** [betree_main::betree::BeTree::{6}::lookup] *) let betree_be_tree_lookup_fwd (self : betree_be_tree_t) (key : u64) (st : state) : result (state & (option u64)) = - begin match betree_node_lookup_fwd self.betree_be_tree_root key st with - | Fail e -> Fail e - | Return (st0, opt) -> Return (st0, opt) - end + betree_node_lookup_fwd self.betree_be_tree_root key st (** [betree_main::betree::BeTree::{6}::lookup] *) let betree_be_tree_lookup_back diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 1560624b..c06a6b9e 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -13,10 +13,7 @@ let betree_load_internal_node_fwd (id : u64) (st : state) : result (state & (betree_list_t (u64 & betree_message_t))) = - begin match betree_utils_load_internal_node_fwd id st with - | Fail e -> Fail e - | Return (st0, l) -> Return (st0, l) - end + betree_utils_load_internal_node_fwd id st (** [betree_main::betree::store_internal_node] *) let betree_store_internal_node_fwd @@ -31,10 +28,7 @@ let betree_store_internal_node_fwd (** [betree_main::betree::load_leaf_node] *) let betree_load_leaf_node_fwd (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) = - begin match betree_utils_load_leaf_node_fwd id st with - | Fail e -> Fail e - | Return (st0, l) -> Return (st0, l) - end + betree_utils_load_leaf_node_fwd id st (** [betree_main::betree::store_leaf_node] *) let betree_store_leaf_node_fwd @@ -54,11 +48,7 @@ let betree_fresh_node_id_fwd (counter : u64) : result u64 = end (** [betree_main::betree::fresh_node_id] *) -let betree_fresh_node_id_back (counter : u64) : result u64 = - begin match u64_add counter 1 with - | Fail e -> Fail e - | Return counter0 -> Return counter0 - end +let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1 (** [betree_main::betree::NodeIdCounter::{0}::new] *) let betree_node_id_counter_new_fwd : result betree_node_id_counter_t = @@ -99,22 +89,10 @@ let betree_upsert_update_fwd begin match u64_sub core_num_u64_max_c prev0 with | Fail e -> Fail e | Return margin -> - if margin >= v - then - begin match u64_add prev0 v with - | Fail e -> Fail e - | Return i -> Return i - end - else Return core_num_u64_max_c + if margin >= v then u64_add prev0 v else Return core_num_u64_max_c end | BetreeUpsertFunStateSub v -> - if prev0 >= v - then - begin match u64_sub prev0 v with - | Fail e -> Fail e - | Return i -> Return i - end - else Return 0 + if prev0 >= v then u64_sub prev0 v else Return 0 end end @@ -127,11 +105,7 @@ let rec betree_list_len_fwd | BetreeListCons x tl -> begin match betree_list_len_fwd t tl with | Fail e -> Fail e - | Return i -> - begin match u64_add 1 i with - | Fail e -> Fail e - | Return i0 -> Return i0 - end + | Return i -> u64_add 1 i end | BetreeListNil -> Return 0 end @@ -404,11 +378,7 @@ let rec betree_node_lookup_in_bindings_fwd else if i > key then Return None - else - begin match betree_node_lookup_in_bindings_fwd key tl with - | Fail e -> Fail e - | Return opt -> Return opt - end + else betree_node_lookup_in_bindings_fwd key tl | BetreeListNil -> Return None end @@ -423,12 +393,7 @@ let rec betree_node_lookup_first_message_for_key_fwd let (i, m) = x in if i >= key then Return (BetreeListCons (i, m) next_msgs) - else - begin match betree_node_lookup_first_message_for_key_fwd key next_msgs - with - | Fail e -> Fail e - | Return l -> Return l - end + else betree_node_lookup_first_message_for_key_fwd key next_msgs | BetreeListNil -> Return BetreeListNil end @@ -480,11 +445,7 @@ let rec betree_node_apply_upserts_fwd betree_list_pop_front_back (u64 & betree_message_t) msgs with | Fail e -> Fail e | Return msgs0 -> - begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st - with - | Fail e -> Fail e - | Return (st0, i) -> Return (st0, i) - end + betree_node_apply_upserts_fwd msgs0 (Some v) key st end end end @@ -529,11 +490,7 @@ let rec betree_node_apply_upserts_back betree_list_pop_front_back (u64 & betree_message_t) msgs with | Fail e -> Fail e | Return msgs0 -> - begin match - betree_node_apply_upserts_back msgs0 (Some v) key st st0 with - | Fail e -> Fail e - | Return (st1, msgs1) -> Return (st1, msgs1) - end + betree_node_apply_upserts_back msgs0 (Some v) key st st0 end end end @@ -776,16 +733,8 @@ and betree_internal_lookup_in_children_fwd (decreases (betree_internal_lookup_in_children_decreases self key st)) = if key < self.betree_internal_pivot - then - begin match betree_node_lookup_fwd self.betree_internal_left key st with - | Fail e -> Fail e - | Return (st0, opt) -> Return (st0, opt) - end - else - begin match betree_node_lookup_fwd self.betree_internal_right key st with - | Fail e -> Fail e - | Return (st0, opt) -> Return (st0, opt) - end + then betree_node_lookup_fwd self.betree_internal_left key st + else betree_node_lookup_fwd self.betree_internal_right key st (** [betree_main::betree::Internal::{4}::lookup_in_children] *) and betree_internal_lookup_in_children_back @@ -822,11 +771,7 @@ let rec betree_node_lookup_mut_in_bindings_fwd let (i, i0) = hd in if i >= key then Return (BetreeListCons (i, i0) tl) - else - begin match betree_node_lookup_mut_in_bindings_fwd key tl with - | Fail e -> Fail e - | Return l -> Return l - end + else betree_node_lookup_mut_in_bindings_fwd key tl | BetreeListNil -> Return BetreeListNil end @@ -877,24 +822,14 @@ let betree_node_apply_to_leaf_fwd_back with | Fail e -> Fail e | Return bindings2 -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings - bindings2 with - | Fail e -> Fail e - | Return bindings3 -> Return bindings3 - end + betree_node_lookup_mut_in_bindings_back key bindings bindings2 end end | BetreeMessageDelete -> begin match betree_list_pop_front_back (u64 & u64) bindings0 with | Fail e -> Fail e | Return bindings1 -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - with - | Fail e -> Fail e - | Return bindings2 -> Return bindings2 - end + betree_node_lookup_mut_in_bindings_back key bindings bindings1 end | BetreeMessageUpsert s -> let (_, i) = hd in @@ -909,12 +844,8 @@ let betree_node_apply_to_leaf_fwd_back v) with | Fail e -> Fail e | Return bindings2 -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings - bindings2 with - | Fail e -> Fail e - | Return bindings3 -> Return bindings3 - end + betree_node_lookup_mut_in_bindings_back key bindings + bindings2 end end end @@ -927,19 +858,10 @@ let betree_node_apply_to_leaf_fwd_back betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with | Fail e -> Fail e | Return bindings1 -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - with - | Fail e -> Fail e - | Return bindings2 -> Return bindings2 - end + betree_node_lookup_mut_in_bindings_back key bindings bindings1 end | BetreeMessageDelete -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings bindings0 with - | Fail e -> Fail e - | Return bindings1 -> Return bindings1 - end + betree_node_lookup_mut_in_bindings_back key bindings bindings0 | BetreeMessageUpsert s -> begin match betree_upsert_update_fwd None s with | Fail e -> Fail e @@ -949,12 +871,7 @@ let betree_node_apply_to_leaf_fwd_back with | Fail e -> Fail e | Return bindings1 -> - begin match - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - with - | Fail e -> Fail e - | Return bindings2 -> Return bindings2 - end + betree_node_lookup_mut_in_bindings_back key bindings bindings1 end end end @@ -974,11 +891,7 @@ let rec betree_node_apply_messages_to_leaf_fwd_back begin match betree_node_apply_to_leaf_fwd_back bindings i m with | Fail e -> Fail e | Return bindings0 -> - begin match - betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with - | Fail e -> Fail e - | Return bindings1 -> Return bindings1 - end + betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl end | BetreeListNil -> Return bindings end @@ -998,11 +911,7 @@ let rec betree_node_filter_messages_for_key_fwd_back betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k, m) l) with | Fail e -> Fail e - | Return msgs0 -> - begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with - | Fail e -> Fail e - | Return msgs1 -> Return msgs1 - end + | Return msgs0 -> betree_node_filter_messages_for_key_fwd_back key msgs0 end else Return (BetreeListCons (k, m) l) | BetreeListNil -> Return BetreeListNil @@ -1018,12 +927,7 @@ let rec betree_node_lookup_first_message_after_key_fwd | BetreeListCons p next_msgs -> let (k, m) = p in if k = key - then - begin match betree_node_lookup_first_message_after_key_fwd key next_msgs - with - | Fail e -> Fail e - | Return l -> Return l - end + then betree_node_lookup_first_message_after_key_fwd key next_msgs else Return (BetreeListCons (k, m) next_msgs) | BetreeListNil -> Return BetreeListNil end @@ -1074,12 +978,7 @@ let betree_node_apply_to_internal_fwd_back (key, BetreeMessageInsert i) with | Fail e -> Fail e | Return msgs2 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs msgs2 - with - | Fail e -> Fail e - | Return msgs3 -> Return msgs3 - end + betree_node_lookup_first_message_for_key_back key msgs msgs2 end end | BetreeMessageDelete -> @@ -1092,12 +991,7 @@ let betree_node_apply_to_internal_fwd_back (key, BetreeMessageDelete) with | Fail e -> Fail e | Return msgs2 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs msgs2 - with - | Fail e -> Fail e - | Return msgs3 -> Return msgs3 - end + betree_node_lookup_first_message_for_key_back key msgs msgs2 end end | BetreeMessageUpsert s -> @@ -1120,12 +1014,8 @@ let betree_node_apply_to_internal_fwd_back msgs1 (key, BetreeMessageInsert v) with | Fail e -> Fail e | Return msgs2 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - msgs2 with - | Fail e -> Fail e - | Return msgs3 -> Return msgs3 - end + betree_node_lookup_first_message_for_key_back key msgs + msgs2 end end end @@ -1143,12 +1033,8 @@ let betree_node_apply_to_internal_fwd_back msgs1 (key, BetreeMessageInsert v) with | Fail e -> Fail e | Return msgs2 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - msgs2 with - | Fail e -> Fail e - | Return msgs3 -> Return msgs3 - end + betree_node_lookup_first_message_for_key_back key msgs + msgs2 end end end @@ -1167,12 +1053,8 @@ let betree_node_apply_to_internal_fwd_back msgs2 with | Fail e -> Fail e | Return msgs3 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs - msgs3 with - | Fail e -> Fail e - | Return msgs4 -> Return msgs4 - end + betree_node_lookup_first_message_for_key_back key msgs + msgs3 end end end @@ -1185,11 +1067,7 @@ let betree_node_apply_to_internal_fwd_back new_msg) with | Fail e -> Fail e | Return msgs1 -> - begin match - betree_node_lookup_first_message_for_key_back key msgs msgs1 with - | Fail e -> Fail e - | Return msgs2 -> Return msgs2 - end + betree_node_lookup_first_message_for_key_back key msgs msgs1 end end end @@ -1207,11 +1085,7 @@ let rec betree_node_apply_messages_to_internal_fwd_back begin match betree_node_apply_to_internal_fwd_back msgs i m with | Fail e -> Fail e | Return msgs0 -> - begin match - betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with - | Fail e -> Fail e - | Return msgs1 -> Return msgs1 - end + betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl end | BetreeListNil -> Return msgs end @@ -1291,12 +1165,8 @@ let rec betree_node_apply_messages_fwd st1 with | Fail e -> Fail e | Return (st2, _) -> - begin match - betree_leaf_split_back0 node content0 params node_id_cnt - st0 st2 with - | Fail e -> Fail e - | Return (st3, ()) -> Return (st3, ()) - end + betree_leaf_split_back0 node content0 params node_id_cnt st0 + st2 end end else @@ -1457,12 +1327,8 @@ and betree_node_apply_messages_back1 content1 st3 with | Fail e -> Fail e | Return (_, _) -> - begin match - betree_internal_flush_back1 node params node_id_cnt - content0 st1 st0 with - | Fail e -> Fail e - | Return (st4, ()) -> Return (st4, ()) - end + betree_internal_flush_back1 node params node_id_cnt content0 + st1 st0 end end end @@ -1505,12 +1371,8 @@ and betree_node_apply_messages_back1 st1 st3 with | Fail e -> Fail e | Return (_, ()) -> - begin match - betree_leaf_split_back1 node content0 params node_id_cnt - st1 st0 with - | Fail e -> Fail e - | Return (st4, ()) -> Return (st4, ()) - end + betree_leaf_split_back1 node content0 params node_id_cnt + st1 st0 end end end @@ -1820,12 +1682,8 @@ let betree_node_apply_fwd (key, new_msg) l) st st0 with | Fail e -> Fail e | Return (st1, (_, _)) -> - begin match - betree_node_apply_messages_back1 self params node_id_cnt - (BetreeListCons (key, new_msg) l) st st1 with - | Fail e -> Fail e - | Return (st2, ()) -> Return (st2, ()) - end + betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons + (key, new_msg) l) st st1 end end @@ -1923,13 +1781,9 @@ let betree_be_tree_apply_fwd st0 with | Fail e -> Fail e | Return (st1, (_, _)) -> - begin match - betree_node_apply_back1 self.betree_be_tree_root - self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st - st1 with - | Fail e -> Fail e - | Return (st2, ()) -> Return (st2, ()) - end + betree_node_apply_back1 self.betree_be_tree_root + self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st + st1 end end @@ -2063,10 +1917,7 @@ let betree_be_tree_lookup_fwd (self : betree_be_tree_t) (key : u64) (st : state) : result (state & (option u64)) = - begin match betree_node_lookup_fwd self.betree_be_tree_root key st with - | Fail e -> Fail e - | Return (st0, opt) -> Return (st0, opt) - end + betree_node_lookup_fwd self.betree_be_tree_root key st (** [betree_main::betree::BeTree::{6}::lookup] *) let betree_be_tree_lookup_back diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index e3ae587f..59c4e125 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -24,11 +24,7 @@ let rec hash_map_allocate_slots_fwd | Return slots0 -> begin match usize_sub n 1 with | Fail e -> Fail e - | Return i -> - begin match hash_map_allocate_slots_fwd t slots0 i with - | Fail e -> Fail e - | Return v -> Return v - end + | Return i -> hash_map_allocate_slots_fwd t slots0 i end end @@ -55,10 +51,7 @@ let hash_map_new_with_capacity_fwd (** [hashmap::HashMap::{0}::new] *) let hash_map_new_fwd (t : Type0) : result (hash_map_t t) = - begin match hash_map_new_with_capacity_fwd t 32 4 5 with - | Fail e -> Fail e - | Return hm -> Return hm - end + hash_map_new_with_capacity_fwd t 32 4 5 (** [hashmap::HashMap::{0}::clear_slots] *) let rec hash_map_clear_slots_fwd_back @@ -74,11 +67,7 @@ let rec hash_map_clear_slots_fwd_back | Return slots0 -> begin match usize_add i 1 with | Fail e -> Fail e - | Return i1 -> - begin match hash_map_clear_slots_fwd_back t slots0 i1 with - | Fail e -> Fail e - | Return slots1 -> Return slots1 - end + | Return i1 -> hash_map_clear_slots_fwd_back t slots0 i1 end end else Return slots @@ -107,11 +96,7 @@ let rec hash_map_insert_in_list_fwd | ListCons ckey cvalue ls0 -> if ckey = key then Return false - else - begin match hash_map_insert_in_list_fwd t key value ls0 with - | Fail e -> Fail e - | Return b -> Return b - end + else hash_map_insert_in_list_fwd t key value ls0 | ListNil -> Return true end @@ -202,11 +187,7 @@ let rec hash_map_move_elements_from_list_fwd_back | ListCons k v tl -> begin match hash_map_insert_no_resize_fwd_back t ntable k v with | Fail e -> Fail e - | Return ntable0 -> - begin match hash_map_move_elements_from_list_fwd_back t ntable0 tl with - | Fail e -> Fail e - | Return ntable1 -> Return ntable1 - end + | Return ntable0 -> hash_map_move_elements_from_list_fwd_back t ntable0 tl end | ListNil -> Return ntable end @@ -233,12 +214,7 @@ let rec hash_map_move_elements_fwd_back | Return slots0 -> begin match usize_add i 1 with | Fail e -> Fail e - | Return i1 -> - begin match hash_map_move_elements_fwd_back t ntable0 slots0 i1 - with - | Fail e -> Fail e - | Return (ntable1, slots1) -> Return (ntable1, slots1) - end + | Return i1 -> hash_map_move_elements_fwd_back t ntable0 slots0 i1 end end end @@ -296,11 +272,7 @@ let hash_map_insert_fwd_back | Fail e -> Fail e | Return i -> if i > self0.hash_map_max_load - then - begin match hash_map_try_resize_fwd_back t self0 with - | Fail e -> Fail e - | Return self1 -> Return self1 - end + then hash_map_try_resize_fwd_back t self0 else Return self0 end end @@ -315,11 +287,7 @@ let rec hash_map_contains_key_in_list_fwd | ListCons ckey x ls0 -> if ckey = key then Return true - else - begin match hash_map_contains_key_in_list_fwd t key ls0 with - | Fail e -> Fail e - | Return b -> Return b - end + else hash_map_contains_key_in_list_fwd t key ls0 | ListNil -> Return false end @@ -335,11 +303,7 @@ let hash_map_contains_key_fwd | Return hash_mod -> begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with | Fail e -> Fail e - | Return l -> - begin match hash_map_contains_key_in_list_fwd t key l with - | Fail e -> Fail e - | Return b -> Return b - end + | Return l -> hash_map_contains_key_in_list_fwd t key l end end end @@ -351,13 +315,7 @@ let rec hash_map_get_in_list_fwd = begin match ls with | ListCons ckey cvalue ls0 -> - if ckey = key - then Return cvalue - else - begin match hash_map_get_in_list_fwd t key ls0 with - | Fail e -> Fail e - | Return x -> Return x - end + if ckey = key then Return cvalue else hash_map_get_in_list_fwd t key ls0 | ListNil -> Fail Failure end @@ -373,11 +331,7 @@ let hash_map_get_fwd | Return hash_mod -> begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with | Fail e -> Fail e - | Return l -> - begin match hash_map_get_in_list_fwd t key l with - | Fail e -> Fail e - | Return x -> Return x - end + | Return l -> hash_map_get_in_list_fwd t key l end end end @@ -391,11 +345,7 @@ let rec hash_map_get_mut_in_list_fwd | ListCons ckey cvalue ls0 -> if ckey = key then Return cvalue - else - begin match hash_map_get_mut_in_list_fwd t key ls0 with - | Fail e -> Fail e - | Return x -> Return x - end + else hash_map_get_mut_in_list_fwd t key ls0 | ListNil -> Fail Failure end @@ -430,11 +380,7 @@ let hash_map_get_mut_fwd begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with | Fail e -> Fail e - | Return l -> - begin match hash_map_get_mut_in_list_fwd t key l with - | Fail e -> Fail e - | Return x -> Return x - end + | Return l -> hash_map_get_mut_in_list_fwd t key l end end end @@ -485,11 +431,7 @@ let rec hash_map_remove_from_list_fwd | ListCons i cvalue tl0 -> Return (Some cvalue) | ListNil -> Fail Failure end - else - begin match hash_map_remove_from_list_fwd t key tl with - | Fail e -> Fail e - | Return opt -> Return opt - end + else hash_map_remove_from_list_fwd t key tl | ListNil -> Return None end diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index d6da4562..c4f2b039 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -25,11 +25,7 @@ let rec hashmap_hash_map_allocate_slots_fwd | Return slots0 -> begin match usize_sub n 1 with | Fail e -> Fail e - | Return i -> - begin match hashmap_hash_map_allocate_slots_fwd t slots0 i with - | Fail e -> Fail e - | Return v -> Return v - end + | Return i -> hashmap_hash_map_allocate_slots_fwd t slots0 i end end @@ -57,10 +53,7 @@ let hashmap_hash_map_new_with_capacity_fwd (** [hashmap_main::hashmap::HashMap::{0}::new] *) let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 with - | Fail e -> Fail e - | Return hm -> Return hm - end + hashmap_hash_map_new_with_capacity_fwd t 32 4 5 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) let rec hashmap_hash_map_clear_slots_fwd_back @@ -77,11 +70,7 @@ let rec hashmap_hash_map_clear_slots_fwd_back | Return slots0 -> begin match usize_add i 1 with | Fail e -> Fail e - | Return i1 -> - begin match hashmap_hash_map_clear_slots_fwd_back t slots0 i1 with - | Fail e -> Fail e - | Return slots1 -> Return slots1 - end + | Return i1 -> hashmap_hash_map_clear_slots_fwd_back t slots0 i1 end end else Return slots @@ -112,11 +101,7 @@ let rec hashmap_hash_map_insert_in_list_fwd | HashmapListCons ckey cvalue ls0 -> if ckey = key then Return false - else - begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 with - | Fail e -> Fail e - | Return b -> Return b - end + else hashmap_hash_map_insert_in_list_fwd t key value ls0 | HashmapListNil -> Return true end @@ -213,11 +198,7 @@ let rec hashmap_hash_map_move_elements_from_list_fwd_back begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with | Fail e -> Fail e | Return ntable0 -> - begin match - hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl with - | Fail e -> Fail e - | Return ntable1 -> Return ntable1 - end + hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl end | HashmapListNil -> Return ntable end @@ -247,11 +228,7 @@ let rec hashmap_hash_map_move_elements_fwd_back begin match usize_add i 1 with | Fail e -> Fail e | Return i1 -> - begin match - hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 with - | Fail e -> Fail e - | Return (ntable1, slots1) -> Return (ntable1, slots1) - end + hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 end end end @@ -310,11 +287,7 @@ let hashmap_hash_map_insert_fwd_back | Fail e -> Fail e | Return i -> if i > self0.hashmap_hash_map_max_load - then - begin match hashmap_hash_map_try_resize_fwd_back t self0 with - | Fail e -> Fail e - | Return self1 -> Return self1 - end + then hashmap_hash_map_try_resize_fwd_back t self0 else Return self0 end end @@ -329,11 +302,7 @@ let rec hashmap_hash_map_contains_key_in_list_fwd | HashmapListCons ckey x ls0 -> if ckey = key then Return true - else - begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 with - | Fail e -> Fail e - | Return b -> Return b - end + else hashmap_hash_map_contains_key_in_list_fwd t key ls0 | HashmapListNil -> Return false end @@ -351,11 +320,7 @@ let hashmap_hash_map_contains_key_fwd vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_contains_key_in_list_fwd t key l with - | Fail e -> Fail e - | Return b -> Return b - end + | Return l -> hashmap_hash_map_contains_key_in_list_fwd t key l end end end @@ -369,11 +334,7 @@ let rec hashmap_hash_map_get_in_list_fwd | HashmapListCons ckey cvalue ls0 -> if ckey = key then Return cvalue - else - begin match hashmap_hash_map_get_in_list_fwd t key ls0 with - | Fail e -> Fail e - | Return x -> Return x - end + else hashmap_hash_map_get_in_list_fwd t key ls0 | HashmapListNil -> Fail Failure end @@ -391,11 +352,7 @@ let hashmap_hash_map_get_fwd vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_get_in_list_fwd t key l with - | Fail e -> Fail e - | Return x -> Return x - end + | Return l -> hashmap_hash_map_get_in_list_fwd t key l end end end @@ -410,11 +367,7 @@ let rec hashmap_hash_map_get_mut_in_list_fwd | HashmapListCons ckey cvalue ls0 -> if ckey = key then Return cvalue - else - begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 with - | Fail e -> Fail e - | Return x -> Return x - end + else hashmap_hash_map_get_mut_in_list_fwd t key ls0 | HashmapListNil -> Fail Failure end @@ -450,11 +403,7 @@ let hashmap_hash_map_get_mut_fwd vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_get_mut_in_list_fwd t key l with - | Fail e -> Fail e - | Return x -> Return x - end + | Return l -> hashmap_hash_map_get_mut_in_list_fwd t key l end end end @@ -510,11 +459,7 @@ let rec hashmap_hash_map_remove_from_list_fwd | HashmapListCons i cvalue tl0 -> Return (Some cvalue) | HashmapListNil -> Fail Failure end - else - begin match hashmap_hash_map_remove_from_list_fwd t key tl with - | Fail e -> Fail e - | Return opt -> Return opt - end + else hashmap_hash_map_remove_from_list_fwd t key tl | HashmapListNil -> Return None end diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst index a0658206..9b90e9c7 100644 --- a/tests/fstar/misc/Constants.fst +++ b/tests/fstar/misc/Constants.fst @@ -22,12 +22,10 @@ let x2_body : result u32 = Return 3 let x2_c : u32 = eval_global x2_body (** [constants::incr] *) -let incr_fwd (n : u32) : result u32 = - begin match u32_add n 1 with | Fail e -> Fail e | Return i -> Return i end +let incr_fwd (n : u32) : result u32 = u32_add n 1 (** [constants::X3] *) -let x3_body : result u32 = - begin match incr_fwd 32 with | Fail e -> Fail e | Return i -> Return i end +let x3_body : result u32 = incr_fwd 32 let x3_c : u32 = eval_global x3_body (** [constants::mk_pair0] *) @@ -41,19 +39,11 @@ let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) = Return (Mkpair_t x y) (** [constants::P0] *) -let p0_body : result (u32 & u32) = - begin match mk_pair0_fwd 0 1 with - | Fail e -> Fail e - | Return p -> Return p - end +let p0_body : result (u32 & u32) = mk_pair0_fwd 0 1 let p0_c : (u32 & u32) = eval_global p0_body (** [constants::P1] *) -let p1_body : result (pair_t u32 u32) = - begin match mk_pair1_fwd 0 1 with - | Fail e -> Fail e - | Return p -> Return p - end +let p1_body : result (pair_t u32 u32) = mk_pair1_fwd 0 1 let p1_c : pair_t u32 u32 = eval_global p1_body (** [constants::P2] *) @@ -72,19 +62,14 @@ let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) = Return (Mkwrap_t val0) (** [constants::Y] *) -let y_body : result (wrap_t i32) = - begin match wrap_new_fwd i32 2 with - | Fail e -> Fail e - | Return w -> Return w - end +let y_body : result (wrap_t i32) = wrap_new_fwd i32 2 let y_c : wrap_t i32 = eval_global y_body (** [constants::unwrap_y] *) let unwrap_y_fwd : result i32 = Return y_c.wrap_val (** [constants::YVAL] *) -let yval_body : result i32 = - begin match unwrap_y_fwd with | Fail e -> Fail e | Return i -> Return i end +let yval_body : result i32 = unwrap_y_fwd let yval_c : i32 = eval_global yval_body (** [constants::get_z1::Z1] *) @@ -95,8 +80,7 @@ let get_z1_z1_c : i32 = eval_global get_z1_z1_body let get_z1_fwd : result i32 = Return get_z1_z1_c (** [constants::add] *) -let add_fwd (a : i32) (b : i32) : result i32 = - begin match i32_add a b with | Fail e -> Fail e | Return i -> Return i end +let add_fwd (a : i32) (b : i32) : result i32 = i32_add a b (** [constants::Q1] *) let q1_body : result i32 = Return 5 @@ -107,8 +91,7 @@ let q2_body : result i32 = Return q1_c let q2_c : i32 = eval_global q2_body (** [constants::Q3] *) -let q3_body : result i32 = - begin match add_fwd q2_c 3 with | Fail e -> Fail e | Return i -> Return i end +let q3_body : result i32 = add_fwd q2_c 3 let q3_c : i32 = eval_global q3_body (** [constants::get_z2] *) @@ -118,11 +101,7 @@ let get_z2_fwd : result i32 = | Return i -> begin match add_fwd i q3_c with | Fail e -> Fail e - | Return i0 -> - begin match add_fwd q1_c i0 with - | Fail e -> Fail e - | Return i1 -> Return i1 - end + | Return i0 -> add_fwd q1_c i0 end end @@ -131,8 +110,7 @@ let s1_body : result u32 = Return 6 let s1_c : u32 = eval_global s1_body (** [constants::S2] *) -let s2_body : result u32 = - begin match incr_fwd s1_c with | Fail e -> Fail e | Return i -> Return i end +let s2_body : result u32 = incr_fwd s1_c let s2_c : u32 = eval_global s2_body (** [constants::S3] *) @@ -140,10 +118,6 @@ let s3_body : result (pair_t u32 u32) = Return p3_c let s3_c : pair_t u32 u32 = eval_global s3_body (** [constants::S4] *) -let s4_body : result (pair_t u32 u32) = - begin match mk_pair1_fwd 7 8 with - | Fail e -> Fail e - | Return p -> Return p - end +let s4_body : result (pair_t u32 u32) = mk_pair1_fwd 7 8 let s4_c : pair_t u32 u32 = eval_global s4_body diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index a57472d4..2529ec33 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -46,12 +46,7 @@ let test_new_non_zero_u32_fwd begin match core_num_nonzero_non_zero_u32_new_fwd x st with | Fail e -> Fail e | Return (st0, opt) -> - begin match - core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0 - with - | Fail e -> Fail e - | Return (st1, nzu) -> Return (st1, nzu) - end + core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0 end (** [external::test_vec] *) @@ -112,10 +107,7 @@ let test_custom_swap_back (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 e -> Fail e - | Return (st1, (x0, y0)) -> Return (st1, (x0, y0)) - end + custom_swap_back u32 x y st 1 st0 (** [external::test_swap_non_zero] *) let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) = diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index f5339339..870a2159 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -19,21 +19,14 @@ let rec list_nth_mut_loop_loop0_fwd else begin match u32_sub i 1 with | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_loop_loop0_fwd t tl i0 with - | Fail e -> Fail e - | Return x0 -> Return x0 - end + | Return i0 -> list_nth_mut_loop_loop0_fwd t tl i0 end | ListNil -> Fail Failure end (** [loops::list_nth_mut_loop] *) let list_nth_mut_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t = - begin match list_nth_mut_loop_loop0_fwd t ls i with - | Fail e -> Fail e - | Return x -> Return x - end + list_nth_mut_loop_loop0_fwd t ls i (** [loops::list_nth_mut_loop] *) let rec list_nth_mut_loop_loop0_back @@ -59,8 +52,5 @@ let rec list_nth_mut_loop_loop0_back (** [loops::list_nth_mut_loop] *) let list_nth_mut_loop_back (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = - begin match list_nth_mut_loop_loop0_back t ls i ret with - | Fail e -> Fail e - | Return l -> Return l - end + list_nth_mut_loop_loop0_back t ls i ret diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index 8424a7cc..f8c63798 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -31,35 +31,25 @@ type sum_t (t1 t2 : Type0) = | SumRight : t2 -> sum_t t1 t2 (** [no_nested_borrows::neg_test] *) -let neg_test_fwd (x : i32) : result i32 = - begin match i32_neg x with | Fail e -> Fail e | Return i -> Return i end +let neg_test_fwd (x : i32) : result i32 = i32_neg x (** [no_nested_borrows::add_test] *) -let add_test_fwd (x : u32) (y : u32) : result u32 = - begin match u32_add x y with | Fail e -> Fail e | Return i -> Return i end +let add_test_fwd (x : u32) (y : u32) : result u32 = u32_add x y (** [no_nested_borrows::subs_test] *) -let subs_test_fwd (x : u32) (y : u32) : result u32 = - begin match u32_sub x y with | Fail e -> Fail e | Return i -> Return i end +let subs_test_fwd (x : u32) (y : u32) : result u32 = u32_sub x y (** [no_nested_borrows::div_test] *) -let div_test_fwd (x : u32) (y : u32) : result u32 = - begin match u32_div x y with | Fail e -> Fail e | Return i -> Return i end +let div_test_fwd (x : u32) (y : u32) : result u32 = u32_div x y (** [no_nested_borrows::div_test1] *) -let div_test1_fwd (x : u32) : result u32 = - begin match u32_div x 2 with | Fail e -> Fail e | Return i -> Return i end +let div_test1_fwd (x : u32) : result u32 = u32_div x 2 (** [no_nested_borrows::rem_test] *) -let rem_test_fwd (x : u32) (y : u32) : result u32 = - begin match u32_rem x y with | Fail e -> Fail e | Return i -> Return i end +let rem_test_fwd (x : u32) (y : u32) : result u32 = u32_rem x y (** [no_nested_borrows::cast_test] *) -let cast_test_fwd (x : u32) : result i32 = - begin match scalar_cast U32 I32 x with - | Fail e -> Fail e - | Return i -> Return i - end +let cast_test_fwd (x : u32) : result i32 = scalar_cast U32 I32 x (** [no_nested_borrows::test2] *) let test2_fwd : result unit = @@ -245,11 +235,7 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 = | ListCons x l1 -> begin match list_length_fwd t l1 with | Fail e -> Fail e - | Return i -> - begin match u32_add 1 i with - | Fail e -> Fail e - | Return i0 -> Return i0 - end + | Return i -> u32_add 1 i end | ListNil -> Return 0 end @@ -263,11 +249,7 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t = else begin match u32_sub i 1 with | Fail e -> Fail e - | Return i0 -> - begin match list_nth_shared_fwd t tl i0 with - | Fail e -> Fail e - | Return x0 -> Return x0 - end + | Return i0 -> list_nth_shared_fwd t tl i0 end | ListNil -> Fail Failure end @@ -281,11 +263,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = else begin match u32_sub i 1 with | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_fwd t tl i0 with - | Fail e -> Fail e - | Return x0 -> Return x0 - end + | Return i0 -> list_nth_mut_fwd t tl i0 end | ListNil -> Fail Failure end @@ -313,21 +291,14 @@ let rec list_nth_mut_back let rec list_rev_aux_fwd (t : Type0) (li : list_t t) (lo : list_t t) : result (list_t t) = begin match li with - | ListCons hd tl -> - begin match list_rev_aux_fwd t tl (ListCons hd lo) with - | Fail e -> Fail e - | Return l -> Return l - end + | ListCons hd tl -> list_rev_aux_fwd t tl (ListCons hd lo) | ListNil -> Return lo end (** [no_nested_borrows::list_rev] *) let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) = let li = mem_replace_fwd (list_t t) l ListNil in - begin match list_rev_aux_fwd t li ListNil with - | Fail e -> Fail e - | Return l0 -> Return l0 - end + list_rev_aux_fwd t li ListNil (** [no_nested_borrows::test_list_functions] *) let test_list_functions_fwd : result unit = diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst index 0f8604d1..199ceb63 100644 --- a/tests/fstar/misc/Paper.fst +++ b/tests/fstar/misc/Paper.fst @@ -6,8 +6,7 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [paper::ref_incr] *) -let ref_incr_fwd_back (x : i32) : result i32 = - begin match i32_add x 1 with | Fail e -> Fail e | Return x0 -> Return x0 end +let ref_incr_fwd_back (x : i32) : result i32 = i32_add x 1 (** [paper::test_incr] *) let test_incr_fwd : result unit = @@ -66,11 +65,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = else begin match u32_sub i 1 with | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_fwd t tl i0 with - | Fail e -> Fail e - | Return x0 -> Return x0 - end + | Return i0 -> list_nth_mut_fwd t tl i0 end | ListNil -> Fail Failure end @@ -100,11 +95,7 @@ let rec sum_fwd (l : list_t i32) : result i32 = | ListCons x tl -> begin match sum_fwd tl with | Fail e -> Fail e - | Return i -> - begin match i32_add x i with - | Fail e -> Fail e - | Return i0 -> Return i0 - end + | Return i -> i32_add x i end | ListNil -> Return 0 end diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst index 158a5fc7..12618dbb 100644 --- a/tests/fstar/misc/PoloniusList.fst +++ b/tests/fstar/misc/PoloniusList.fst @@ -14,13 +14,7 @@ type list_t (t : Type0) = let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) = begin match ls with | ListCons hd tl -> - if hd = x - then Return (ListCons hd tl) - else - begin match get_list_at_x_fwd tl x with - | Fail e -> Fail e - | Return l -> Return l - end + if hd = x then Return (ListCons hd tl) else get_list_at_x_fwd tl x | ListNil -> Return ListNil end |