Regenerate the files

1 files changed, 42 insertions, 194 deletions

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