Regenerate the code

1 files changed, 72 insertions, 68 deletions

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index a0338557..c2cca26d 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -201,9 +201,9 @@ Definition betree_Leaf_split
   p1 <- betree_List_hd (u64 * u64) content1;
   let (pivot, _) := p1 in
   p2 <- betree_NodeIdCounter_fresh_id node_id_cnt;
-  let (id0, nic) := p2 in
-  p3 <- betree_NodeIdCounter_fresh_id nic;
-  let (id1, nic1) := p3 in
+  let (id0, node_id_cnt1) := p2 in
+  p3 <- betree_NodeIdCounter_fresh_id node_id_cnt1;
+  let (id1, node_id_cnt2) := p3 in
   p4 <- betree_store_leaf_node id0 content0 st;
   let (st1, _) := p4 in
   p5 <- betree_store_leaf_node id1 content1 st1;
@@ -218,7 +218,8 @@ Definition betree_Leaf_split
       betree_Leaf_id := id1;
       betree_Leaf_size := params.(betree_Params_split_size)
     |} in
-  Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, nic1))
+  Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2,
+    node_id_cnt2))
 .
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
@@ -286,22 +287,22 @@ Fixpoint betree_Node_apply_upserts
     if b
     then (
       p <- betree_List_pop_front (u64 * betree_Message_t) msgs;
-      let (msg, l) := p in
+      let (msg, msgs1) := p in
       let (_, m) := msg in
       match m with
       | Betree_Message_Insert _ => Fail_ Failure
       | Betree_Message_Delete => Fail_ Failure
       | Betree_Message_Upsert s =>
         v <- betree_upsert_update prev s;
-        betree_Node_apply_upserts n1 l (Some v) key st
+        betree_Node_apply_upserts n1 msgs1 (Some v) key st
       end)
     else (
       p <- core_option_Option_unwrap u64 prev st;
       let (st1, v) := p in
-      l <-
+      msgs1 <-
         betree_List_push_front (u64 * betree_Message_t) msgs (key,
           Betree_Message_Insert v);
-      Return (st1, (v, l)))
+      Return (st1, (v, msgs1)))
   end
 .
 
@@ -351,9 +352,9 @@ with betree_Node_lookup
         then (
           p3 <- betree_Internal_lookup_in_children n1 node key st1;
           let (st2, p4) := p3 in
-          let (o, i) := p4 in
+          let (o, node1) := p4 in
           _ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l);
-          Return (st2, (o, Betree_Node_Internal i)))
+          Return (st2, (o, Betree_Node_Internal node1)))
         else
           match msg with
           | Betree_Message_Insert v =>
@@ -369,23 +370,24 @@ with betree_Node_lookup
           | Betree_Message_Upsert ufs =>
             p3 <- betree_Internal_lookup_in_children n1 node key st1;
             let (st2, p4) := p3 in
-            let (v, i) := p4 in
+            let (v, node1) := p4 in
             p5 <-
               betree_Node_apply_upserts n1 (Betree_List_Cons (k,
                 Betree_Message_Upsert ufs) l) v key st2;
             let (st3, p6) := p5 in
-            let (v1, l1) := p6 in
-            msgs1 <- lookup_first_message_for_key_back l1;
-            p7 <- betree_store_internal_node i.(betree_Internal_id) msgs1 st3;
+            let (v1, pending1) := p6 in
+            msgs1 <- lookup_first_message_for_key_back pending1;
+            p7 <-
+              betree_store_internal_node node1.(betree_Internal_id) msgs1 st3;
             let (st4, _) := p7 in
-            Return (st4, (Some v1, Betree_Node_Internal i))
+            Return (st4, (Some v1, Betree_Node_Internal node1))
           end
       | Betree_List_Nil =>
         p2 <- betree_Internal_lookup_in_children n1 node key st1;
         let (st2, p3) := p2 in
-        let (o, i) := p3 in
+        let (o, node1) := p3 in
         _ <- lookup_first_message_for_key_back Betree_List_Nil;
-        Return (st2, (o, Betree_Node_Internal i))
+        Return (st2, (o, Betree_Node_Internal node1))
       end
     | Betree_Node_Leaf node =>
       p <- betree_load_leaf_node node.(betree_Leaf_id) st;
@@ -413,8 +415,8 @@ Fixpoint betree_Node_filter_messages_for_key
         p1 <-
           betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k,
             m) l);
-        let (_, l1) := p1 in
-        betree_Node_filter_messages_for_key n1 key l1)
+        let (_, msgs1) := p1 in
+        betree_Node_filter_messages_for_key n1 key msgs1)
       else Return (Betree_List_Cons (k, m) l)
     | Betree_List_Nil => Return Betree_List_Nil
     end
@@ -463,17 +465,17 @@ Definition betree_Node_apply_to_internal
   then
     match new_msg with
     | Betree_Message_Insert i =>
-      l <- betree_Node_filter_messages_for_key n key msgs1;
-      l1 <-
-        betree_List_push_front (u64 * betree_Message_t) l (key,
+      msgs2 <- betree_Node_filter_messages_for_key n key msgs1;
+      msgs3 <-
+        betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
           Betree_Message_Insert i);
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | Betree_Message_Delete =>
-      l <- betree_Node_filter_messages_for_key n key msgs1;
-      l1 <-
-        betree_List_push_front (u64 * betree_Message_t) l (key,
+      msgs2 <- betree_Node_filter_messages_for_key n key msgs1;
+      msgs3 <-
+        betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
           Betree_Message_Delete);
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | Betree_Message_Upsert s =>
       p1 <- betree_List_hd (u64 * betree_Message_t) msgs1;
       let (_, m) := p1 in
@@ -481,32 +483,33 @@ Definition betree_Node_apply_to_internal
       | Betree_Message_Insert prev =>
         v <- betree_upsert_update (Some prev) s;
         p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1;
-        let (_, l) := p2 in
-        l1 <-
-          betree_List_push_front (u64 * betree_Message_t) l (key,
+        let (_, msgs2) := p2 in
+        msgs3 <-
+          betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
             Betree_Message_Insert v);
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | Betree_Message_Delete =>
         p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1;
-        let (_, l) := p2 in
+        let (_, msgs2) := p2 in
         v <- betree_upsert_update None s;
-        l1 <-
-          betree_List_push_front (u64 * betree_Message_t) l (key,
+        msgs3 <-
+          betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
             Betree_Message_Insert v);
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | Betree_Message_Upsert _ =>
         p2 <- betree_Node_lookup_first_message_after_key n key msgs1;
         let (msgs2, lookup_first_message_after_key_back) := p2 in
-        l <-
+        msgs3 <-
           betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
             Betree_Message_Upsert s);
-        msgs3 <- lookup_first_message_after_key_back l;
-        lookup_first_message_for_key_back msgs3
+        msgs4 <- lookup_first_message_after_key_back msgs3;
+        lookup_first_message_for_key_back msgs4
       end
     end
   else (
-    l <- betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg);
-    lookup_first_message_for_key_back l)
+    msgs2 <-
+      betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg);
+    lookup_first_message_for_key_back msgs2)
 .
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
@@ -522,8 +525,8 @@ Fixpoint betree_Node_apply_messages_to_internal
     match new_msgs with
     | Betree_List_Cons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
-      l <- betree_Node_apply_to_internal n1 msgs i m;
-      betree_Node_apply_messages_to_internal n1 l new_msgs_tl
+      msgs1 <- betree_Node_apply_to_internal n1 msgs i m;
+      betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl
     | Betree_List_Nil => Return msgs
     end
   end
@@ -570,28 +573,28 @@ Definition betree_Node_apply_to_leaf
   if b
   then (
     p1 <- betree_List_pop_front (u64 * u64) bindings1;
-    let (hd, l) := p1 in
+    let (hd, bindings2) := p1 in
     match new_msg with
     | Betree_Message_Insert v =>
-      l1 <- betree_List_push_front (u64 * u64) l (key, v);
-      lookup_mut_in_bindings_back l1
-    | Betree_Message_Delete => lookup_mut_in_bindings_back l
+      bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v);
+      lookup_mut_in_bindings_back bindings3
+    | Betree_Message_Delete => lookup_mut_in_bindings_back bindings2
     | Betree_Message_Upsert s =>
       let (_, i) := hd in
       v <- betree_upsert_update (Some i) s;
-      l1 <- betree_List_push_front (u64 * u64) l (key, v);
-      lookup_mut_in_bindings_back l1
+      bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v);
+      lookup_mut_in_bindings_back bindings3
     end)
   else
     match new_msg with
     | Betree_Message_Insert v =>
-      l <- betree_List_push_front (u64 * u64) bindings1 (key, v);
-      lookup_mut_in_bindings_back l
+      bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v);
+      lookup_mut_in_bindings_back bindings2
     | Betree_Message_Delete => lookup_mut_in_bindings_back bindings1
     | Betree_Message_Upsert s =>
       v <- betree_upsert_update None s;
-      l <- betree_List_push_front (u64 * u64) bindings1 (key, v);
-      lookup_mut_in_bindings_back l
+      bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v);
+      lookup_mut_in_bindings_back bindings2
     end
 .
 
@@ -608,8 +611,8 @@ Fixpoint betree_Node_apply_messages_to_leaf
     match new_msgs with
     | Betree_List_Cons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
-      l <- betree_Node_apply_to_leaf n1 bindings i m;
-      betree_Node_apply_messages_to_leaf n1 l new_msgs_tl
+      bindings1 <- betree_Node_apply_to_leaf n1 bindings i m;
+      betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl
     | Betree_List_Nil => Return bindings
     end
   end
@@ -680,38 +683,39 @@ with betree_Node_apply_messages
     | Betree_Node_Internal node =>
       p <- betree_load_internal_node node.(betree_Internal_id) st;
       let (st1, content) := p in
-      l <- betree_Node_apply_messages_to_internal n1 content msgs;
-      num_msgs <- betree_List_len (u64 * betree_Message_t) n1 l;
+      content1 <- betree_Node_apply_messages_to_internal n1 content msgs;
+      num_msgs <- betree_List_len (u64 * betree_Message_t) n1 content1;
       if num_msgs s>= params.(betree_Params_min_flush_size)
       then (
-        p1 <- betree_Internal_flush n1 node params node_id_cnt l st1;
+        p1 <- betree_Internal_flush n1 node params node_id_cnt content1 st1;
         let (st2, p2) := p1 in
-        let (content1, p3) := p2 in
+        let (content2, p3) := p2 in
         let (node1, node_id_cnt1) := p3 in
         p4 <-
-          betree_store_internal_node node1.(betree_Internal_id) content1 st2;
+          betree_store_internal_node node1.(betree_Internal_id) content2 st2;
         let (st3, _) := p4 in
         Return (st3, (Betree_Node_Internal node1, node_id_cnt1)))
       else (
-        p1 <- betree_store_internal_node node.(betree_Internal_id) l st1;
+        p1 <-
+          betree_store_internal_node node.(betree_Internal_id) content1 st1;
         let (st2, _) := p1 in
         Return (st2, (Betree_Node_Internal node, node_id_cnt)))
     | Betree_Node_Leaf node =>
       p <- betree_load_leaf_node node.(betree_Leaf_id) st;
       let (st1, content) := p in
-      l <- betree_Node_apply_messages_to_leaf n1 content msgs;
-      len <- betree_List_len (u64 * u64) n1 l;
+      content1 <- betree_Node_apply_messages_to_leaf n1 content msgs;
+      len <- betree_List_len (u64 * u64) n1 content1;
       i <- u64_mul 2%u64 params.(betree_Params_split_size);
       if len s>= i
       then (
-        p1 <- betree_Leaf_split n1 node l params node_id_cnt st1;
+        p1 <- betree_Leaf_split n1 node content1 params node_id_cnt st1;
         let (st2, p2) := p1 in
-        let (new_node, nic) := p2 in
+        let (new_node, node_id_cnt1) := p2 in
         p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2;
         let (st3, _) := p3 in
-        Return (st3, (Betree_Node_Internal new_node, nic)))
+        Return (st3, (Betree_Node_Internal new_node, node_id_cnt1)))
       else (
-        p1 <- betree_store_leaf_node node.(betree_Leaf_id) l st1;
+        p1 <- betree_store_leaf_node node.(betree_Leaf_id) content1 st1;
         let (st2, _) := p1 in
         Return (st2, (Betree_Node_Leaf
           {| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len
@@ -744,7 +748,7 @@ Definition betree_BeTree_new
   :=
   node_id_cnt <- betree_NodeIdCounter_new;
   p <- betree_NodeIdCounter_fresh_id node_id_cnt;
-  let (id, nic) := p in
+  let (id, node_id_cnt1) := p in
   p1 <- betree_store_leaf_node id Betree_List_Nil st;
   let (st1, _) := p1 in
   Return (st1,
@@ -754,7 +758,7 @@ Definition betree_BeTree_new
           betree_Params_min_flush_size := min_flush_size;
           betree_Params_split_size := split_size
         |};
-      betree_BeTree_node_id_cnt := nic;
+      betree_BeTree_node_id_cnt := node_id_cnt1;
       betree_BeTree_root :=
         (Betree_Node_Leaf
           {| betree_Leaf_id := id; betree_Leaf_size := 0%u64 |})