summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v133
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v37
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v42
-rw-r--r--tests/coq/misc/Constants.v32
-rw-r--r--tests/coq/misc/External_Funs.v9
-rw-r--r--tests/coq/misc/Loops.v9
-rw-r--r--tests/coq/misc/NoNestedBorrows.v38
-rw-r--r--tests/coq/misc/Paper.v8
-rw-r--r--tests/coq/misc/PoloniusList.v4
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst236
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst239
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst86
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst83
-rw-r--r--tests/fstar/misc/Constants.fst48
-rw-r--r--tests/fstar/misc/External.Funs.fst12
-rw-r--r--tests/fstar/misc/Loops.Funs.fst16
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst53
-rw-r--r--tests/fstar/misc/Paper.fst15
-rw-r--r--tests/fstar/misc/PoloniusList.fst8
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 13:43:54 +0000