Regenerate the files

1 files changed, 38 insertions, 95 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] *)