Merge pull request #93 from AeneasVerif/son/examples

Add some examples and improve the shape of the generated code

12 files changed, 182 insertions, 199 deletions

diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 34d163b7..049d63cb 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -30,27 +30,25 @@ Definition array_to_mut_slice_
   (T : Type) (s : array T 32%usize) :
   result ((slice T) * (slice T -> result (array T 32%usize)))
   :=
-  p <- array_to_slice_mut T 32%usize s;
-  let (s1, to_slice_mut_back) := p in
-  Return (s1, to_slice_mut_back)
+  array_to_slice_mut T 32%usize s
 .
 
 (** [arrays::array_len]:
     Source: 'src/arrays.rs', lines 25:0-25:40 *)
 Definition array_len (T : Type) (s : array T 32%usize) : result usize :=
-  s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i
+  s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
 .
 
 (** [arrays::shared_array_len]:
     Source: 'src/arrays.rs', lines 29:0-29:48 *)
 Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize :=
-  s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i
+  s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
 .
 
 (** [arrays::shared_slice_len]:
     Source: 'src/arrays.rs', lines 33:0-33:44 *)
 Definition shared_slice_len (T : Type) (s : slice T) : result usize :=
-  let i := slice_len T s in Return i
+  Return (slice_len T s)
 .
 
 (** [arrays::index_array_shared]:
@@ -78,9 +76,7 @@ Definition index_mut_array
   (T : Type) (s : array T 32%usize) (i : usize) :
   result (T * (T -> result (array T 32%usize)))
   :=
-  p <- array_index_mut_usize T 32%usize s i;
-  let (t, index_mut_back) := p in
-  Return (t, index_mut_back)
+  array_index_mut_usize T 32%usize s i
 .
 
 (** [arrays::index_slice]:
@@ -95,9 +91,7 @@ Definition index_mut_slice
   (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T)))
   :=
-  p <- slice_index_mut_usize T s i;
-  let (t, index_mut_back) := p in
-  Return (t, index_mut_back)
+  slice_index_mut_usize T s i
 .
 
 (** [arrays::slice_subslice_shared_]:
@@ -136,9 +130,7 @@ Definition array_to_slice_mut_
   (x : array u32 32%usize) :
   result ((slice u32) * (slice u32 -> result (array u32 32%usize)))
   :=
-  p <- array_to_slice_mut u32 32%usize x;
-  let (s, to_slice_mut_back) := p in
-  Return (s, to_slice_mut_back)
+  array_to_slice_mut u32 32%usize x
 .
 
 (** [arrays::array_subslice_shared_]:
@@ -334,8 +326,8 @@ Definition update_mut_slice (x : slice u32) : result (slice u32) :=
 Definition update_all : result unit :=
   _ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
   _ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
-  a <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
-  p <- array_to_slice_mut u32 2%usize a;
+  x <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
+  p <- array_to_slice_mut u32 2%usize x;
   let (s, to_slice_mut_back) := p in
   s1 <- update_mut_slice s;
   _ <- to_slice_mut_back s1;
@@ -381,7 +373,7 @@ Definition take_array_t (a : array AB_t 2%usize) : result unit :=
 (** [arrays::non_copyable_array]:
     Source: 'src/arrays.rs', lines 229:0-229:27 *)
 Definition non_copyable_array : result unit :=
-  _ <- take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]); Return tt
+  take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ])
 .
 
 (** [arrays::sum]: loop 0:
@@ -548,8 +540,7 @@ Fixpoint iter_mut_slice_loop
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s< len
-    then (
-      i1 <- usize_add i 1%usize; _ <- iter_mut_slice_loop n1 len i1; Return tt)
+    then (i1 <- usize_add i 1%usize; iter_mut_slice_loop n1 len i1)
     else Return tt
   end
 .
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 3863a90f..c2cca26d 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -27,9 +27,7 @@ Definition betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) :
   result (state * unit)
   :=
-  p <- betree_utils_store_internal_node id content st;
-  let (st1, _) := p in
-  Return (st1, tt)
+  betree_utils_store_internal_node id content st
 .
 
 (** [betree_main::betree::load_leaf_node]:
@@ -45,9 +43,7 @@ Definition betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 * u64)) (st : state) :
   result (state * unit)
   :=
-  p <- betree_utils_store_leaf_node id content st;
-  let (st1, _) := p in
-  Return (st1, tt)
+  betree_utils_store_leaf_node id content st
 .
 
 (** [betree_main::betree::fresh_node_id]:
@@ -205,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;
@@ -222,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]:
@@ -290,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
 .
 
@@ -355,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 =>
@@ -373,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;
@@ -417,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
@@ -467,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
@@ -485,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]:
@@ -526,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
@@ -574,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
 .
 
@@ -612,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
@@ -684,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
@@ -748,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,
@@ -758,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 |})
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 13e4b9c1..b14bed66 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -3,8 +3,8 @@
 -arg -w
 -arg all
 
-BetreeMain_Types.v
 BetreeMain_TypesExternal_Template.v
+BetreeMain_Types.v
 Primitives.v
 BetreeMain_FunsExternal_Template.v
 BetreeMain_Funs.v
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index ec7ca29d..d5a6e535 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -34,8 +34,14 @@ Definition use_mul2_add1 (x : u32) (y : u32) : result u32 :=
 Definition incr (x : u32) : result u32 :=
   u32_add x 1%u32.
 
+(** [demo::use_incr]:
+    Source: 'src/demo.rs', lines 25:0-25:17 *)
+Definition use_incr : result unit :=
+  x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Return tt
+.
+
 (** [demo::CList]
-    Source: 'src/demo.rs', lines 27:0-27:17 *)
+    Source: 'src/demo.rs', lines 34:0-34:17 *)
 Inductive CList_t (T : Type) :=
 | CList_CCons : T -> CList_t T -> CList_t T
 | CList_CNil : CList_t T
@@ -45,7 +51,7 @@ Arguments CList_CCons { _ }.
 Arguments CList_CNil { _ }.
 
 (** [demo::list_nth]:
-    Source: 'src/demo.rs', lines 32:0-32:56 *)
+    Source: 'src/demo.rs', lines 39:0-39:56 *)
 Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
   match n with
   | O => Fail_ OutOfFuel
@@ -61,7 +67,7 @@ Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
 .
 
 (** [demo::list_nth_mut]:
-    Source: 'src/demo.rs', lines 47:0-47:68 *)
+    Source: 'src/demo.rs', lines 54:0-54:68 *)
 Fixpoint list_nth_mut
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -89,7 +95,7 @@ Fixpoint list_nth_mut
 .
 
 (** [demo::list_nth_mut1]: loop 0:
-    Source: 'src/demo.rs', lines 62:0-71:1 *)
+    Source: 'src/demo.rs', lines 69:0-78:1 *)
 Fixpoint list_nth_mut1_loop
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -116,16 +122,16 @@ Fixpoint list_nth_mut1_loop
 .
 
 (** [demo::list_nth_mut1]:
-    Source: 'src/demo.rs', lines 62:0-62:77 *)
+    Source: 'src/demo.rs', lines 69:0-69:77 *)
 Definition list_nth_mut1
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
   :=
-  p <- list_nth_mut1_loop T n l i; let (t, back_'a) := p in Return (t, back_'a)
+  list_nth_mut1_loop T n l i
 .
 
 (** [demo::i32_id]:
-    Source: 'src/demo.rs', lines 73:0-73:28 *)
+    Source: 'src/demo.rs', lines 80:0-80:28 *)
 Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -136,8 +142,30 @@ Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
   end
 .
 
+(** [demo::list_tail]:
+    Source: 'src/demo.rs', lines 88:0-88:64 *)
+Fixpoint list_tail
+  (T : Type) (n : nat) (l : CList_t T) :
+  result ((CList_t T) * (CList_t T -> result (CList_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons t tl =>
+      p <- list_tail T n1 tl;
+      let (c, list_tail_back) := p in
+      let back_'a :=
+        fun (ret : CList_t T) =>
+          tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in
+      Return (c, back_'a)
+    | CList_CNil => Return (CList_CNil, Return)
+    end
+  end
+.
+
 (** Trait declaration: [demo::Counter]
-    Source: 'src/demo.rs', lines 83:0-83:17 *)
+    Source: 'src/demo.rs', lines 97:0-97:17 *)
 Record Counter_t (Self : Type) := mkCounter_t {
   Counter_t_incr : Self -> result (usize * Self);
 }.
@@ -146,19 +174,19 @@ Arguments mkCounter_t { _ }.
 Arguments Counter_t_incr { _ }.
 
 (** [demo::{(demo::Counter for usize)}::incr]:
-    Source: 'src/demo.rs', lines 88:4-88:31 *)
+    Source: 'src/demo.rs', lines 102:4-102:31 *)
 Definition counterUsize_incr (self : usize) : result (usize * usize) :=
   self1 <- usize_add self 1%usize; Return (self, self1)
 .
 
 (** Trait implementation: [demo::{(demo::Counter for usize)}]
-    Source: 'src/demo.rs', lines 87:0-87:22 *)
+    Source: 'src/demo.rs', lines 101:0-101:22 *)
 Definition CounterUsize : Counter_t usize := {|
   Counter_t_incr := counterUsize_incr;
 |}.
 
 (** [demo::use_counter]:
-    Source: 'src/demo.rs', lines 95:0-95:59 *)
+    Source: 'src/demo.rs', lines 109:0-109:59 *)
 Definition use_counter
   (T : Type) (counterInst : Counter_t T) (cnt : T) : result (usize * T) :=
   counterInst.(Counter_t_incr) cnt
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 0478edbe..d709a8d5 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -26,9 +26,9 @@ Fixpoint hashMap_allocate_slots_loop
   | S n2 =>
     if n1 s> 0%usize
     then (
-      v <- alloc_vec_Vec_push (List_t T) slots List_Nil;
+      slots1 <- alloc_vec_Vec_push (List_t T) slots List_Nil;
       n3 <- usize_sub n1 1%usize;
-      hashMap_allocate_slots_loop T n2 v n3)
+      hashMap_allocate_slots_loop T n2 slots1 n3)
     else Return slots
   end
 .
@@ -190,8 +190,8 @@ Fixpoint hashMap_move_elements_from_list_loop
   | S n1 =>
     match ls with
     | List_Cons k v tl =>
-      hm <- hashMap_insert_no_resize T n1 ntable k v;
-      hashMap_move_elements_from_list_loop T n1 hm tl
+      ntable1 <- hashMap_insert_no_resize T n1 ntable k v;
+      hashMap_move_elements_from_list_loop T n1 ntable1 tl
     | List_Nil => Return ntable
     end
   end
@@ -224,12 +224,10 @@ Fixpoint hashMap_move_elements_loop
           (core_slice_index_SliceIndexUsizeSliceTInst (List_t T)) slots i;
       let (l, index_mut_back) := p in
       let (ls, l1) := core_mem_replace (List_t T) l List_Nil in
-      hm <- hashMap_move_elements_from_list T n1 ntable ls;
+      ntable1 <- hashMap_move_elements_from_list T n1 ntable ls;
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back l1;
-      back_'a <- hashMap_move_elements_loop T n1 hm slots1 i2;
-      let (hm1, v) := back_'a in
-      Return (hm1, v))
+      hashMap_move_elements_loop T n1 ntable1 slots1 i2)
     else Return (ntable, slots)
   end
 .
@@ -241,9 +239,7 @@ Definition hashMap_move_elements
   (slots : alloc_vec_Vec (List_t T)) (i : usize) :
   result ((HashMap_t T) * (alloc_vec_Vec (List_t T)))
   :=
-  back_'a <- hashMap_move_elements_loop T n ntable slots i;
-  let (hm, v) := back_'a in
-  Return (hm, v)
+  hashMap_move_elements_loop T n ntable slots i
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::try_resize]:
@@ -284,9 +280,11 @@ Definition hashMap_insert
   (T : Type) (n : nat) (self : HashMap_t T) (key : usize) (value : T) :
   result (HashMap_t T)
   :=
-  hm <- hashMap_insert_no_resize T n self key value;
-  i <- hashMap_len T hm;
-  if i s> hm.(hashMap_max_load) then hashMap_try_resize T n hm else Return hm
+  self1 <- hashMap_insert_no_resize T n self key value;
+  i <- hashMap_len T self1;
+  if i s> self1.(hashMap_max_load)
+  then hashMap_try_resize T n self1
+  else Return self1
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
@@ -398,9 +396,7 @@ Definition hashMap_get_mut_in_list
   (T : Type) (n : nat) (ls : List_t T) (key : usize) :
   result (T * (T -> result (List_t T)))
   :=
-  p <- hashMap_get_mut_in_list_loop T n ls key;
-  let (t, back_'a) := p in
-  Return (t, back_'a)
+  hashMap_get_mut_in_list_loop T n ls key
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::get_mut]:
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 6a7eeb2d..9fb3c482 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -29,9 +29,9 @@ Fixpoint hashmap_HashMap_allocate_slots_loop
   | S n2 =>
     if n1 s> 0%usize
     then (
-      v <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
+      slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
       n3 <- usize_sub n1 1%usize;
-      hashmap_HashMap_allocate_slots_loop T n2 v n3)
+      hashmap_HashMap_allocate_slots_loop T n2 slots1 n3)
     else Return slots
   end
 .
@@ -204,8 +204,8 @@ Fixpoint hashmap_HashMap_move_elements_from_list_loop
   | S n1 =>
     match ls with
     | Hashmap_List_Cons k v tl =>
-      hm <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
-      hashmap_HashMap_move_elements_from_list_loop T n1 hm tl
+      ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
+      hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl
     | Hashmap_List_Nil => Return ntable
     end
   end
@@ -239,12 +239,10 @@ Fixpoint hashmap_HashMap_move_elements_loop
           i;
       let (l, index_mut_back) := p in
       let (ls, l1) := core_mem_replace (hashmap_List_t T) l Hashmap_List_Nil in
-      hm <- hashmap_HashMap_move_elements_from_list T n1 ntable ls;
+      ntable1 <- hashmap_HashMap_move_elements_from_list T n1 ntable ls;
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back l1;
-      back_'a <- hashmap_HashMap_move_elements_loop T n1 hm slots1 i2;
-      let (hm1, v) := back_'a in
-      Return (hm1, v))
+      hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2)
     else Return (ntable, slots)
   end
 .
@@ -256,9 +254,7 @@ Definition hashmap_HashMap_move_elements
   (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) :
   result ((hashmap_HashMap_t T) * (alloc_vec_Vec (hashmap_List_t T)))
   :=
-  back_'a <- hashmap_HashMap_move_elements_loop T n ntable slots i;
-  let (hm, v) := back_'a in
-  Return (hm, v)
+  hashmap_HashMap_move_elements_loop T n ntable slots i
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
@@ -304,11 +300,11 @@ Definition hashmap_HashMap_insert
   (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) :
   result (hashmap_HashMap_t T)
   :=
-  hm <- hashmap_HashMap_insert_no_resize T n self key value;
-  i <- hashmap_HashMap_len T hm;
-  if i s> hm.(hashmap_HashMap_max_load)
-  then hashmap_HashMap_try_resize T n hm
-  else Return hm
+  self1 <- hashmap_HashMap_insert_no_resize T n self key value;
+  i <- hashmap_HashMap_len T self1;
+  if i s> self1.(hashmap_HashMap_max_load)
+  then hashmap_HashMap_try_resize T n self1
+  else Return self1
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
@@ -423,9 +419,7 @@ Definition hashmap_HashMap_get_mut_in_list
   (T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) :
   result (T * (T -> result (hashmap_List_t T)))
   :=
-  p <- hashmap_HashMap_get_mut_in_list_loop T n ls key;
-  let (t, back_'a) := p in
-  Return (t, back_'a)
+  hashmap_HashMap_get_mut_in_list_loop T n ls key
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
@@ -585,9 +579,7 @@ Definition insert_on_disk
   p <- hashmap_utils_deserialize st;
   let (st1, hm) := p in
   hm1 <- hashmap_HashMap_insert u64 n hm key value;
-  p1 <- hashmap_utils_serialize hm1 st1;
-  let (st2, _) := p1 in
-  Return (st2, tt)
+  hashmap_utils_serialize hm1 st1
 .
 
 (** [hashmap_main::main]:
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject
index 41945494..d73541d9 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -4,9 +4,9 @@
 -arg all
 
 HashmapMain_Types.v
+HashmapMain_FunsExternal_Template.v
 Primitives.v
 HashmapMain_Funs.v
 HashmapMain_TypesExternal.v
-HashmapMain_FunsExternal_Template.v
 HashmapMain_FunsExternal.v
 HashmapMain_TypesExternal_Template.v
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 91ea88c9..faf91fef 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -45,9 +45,9 @@ Definition custom_swap
   :=
   p <- core_mem_swap T x y st;
   let (st1, p1) := p in
-  let (t, t1) := p1 in
-  let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, t1)) in
-  Return (st1, (t, back_'a))
+  let (x1, y1) := p1 in
+  let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
+  Return (st1, (x1, back_'a))
 .
 
 (** [external::test_custom_swap]:
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index e235b60d..7c83a014 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -29,16 +29,16 @@ Definition sum (n : nat) (max : u32) : result u32 :=
 (** [loops::sum_with_mut_borrows]: loop 0:
     Source: 'src/loops.rs', lines 19:0-31:1 *)
 Fixpoint sum_with_mut_borrows_loop
-  (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
+  (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    if mi s< max
+    if i s< max
     then (
-      ms1 <- u32_add ms mi;
-      mi1 <- u32_add mi 1%u32;
-      sum_with_mut_borrows_loop n1 max mi1 ms1)
-    else u32_mul ms 2%u32
+      ms <- u32_add s i;
+      mi <- u32_add i 1%u32;
+      sum_with_mut_borrows_loop n1 max mi ms)
+    else u32_mul s 2%u32
   end
 .
 
@@ -183,7 +183,7 @@ Definition list_nth_mut_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) :
   result (T * (T -> result (List_t T)))
   :=
-  p <- list_nth_mut_loop_loop T n ls i; let (t, back) := p in Return (t, back)
+  list_nth_mut_loop_loop T n ls i
 .
 
 (** [loops::list_nth_shared_loop]: loop 0:
@@ -245,10 +245,10 @@ Definition get_elem_mut
   p <-
     alloc_vec_Vec_index_mut (List_t usize) usize
       (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
-  let (l, index_mut_back) := p in
-  p1 <- get_elem_mut_loop n x l;
+  let (ls, index_mut_back) := p in
+  p1 <- get_elem_mut_loop n x ls;
   let (i, back) := p1 in
-  let back1 := fun (ret : usize) => l1 <- back ret; index_mut_back l1 in
+  let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in
   Return (i, back1)
 .
 
@@ -273,10 +273,10 @@ Definition get_elem_shared
   (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
   result usize
   :=
-  l <-
+  ls <-
     alloc_vec_Vec_index (List_t usize) usize
       (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
-  get_elem_shared_loop n x l
+  get_elem_shared_loop n x ls
 .
 
 (** [loops::id_mut]:
@@ -400,9 +400,7 @@ Definition list_nth_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
   :=
-  t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i;
-  let '(p, back_'a, back_'b) := t in
-  Return (p, back_'a, back_'b)
+  list_nth_mut_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_loop_pair]: loop 0:
@@ -481,9 +479,7 @@ Definition list_nth_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
   :=
-  p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_loop_pair_merge]: loop 0:
@@ -557,9 +553,7 @@ Definition list_nth_mut_shared_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
@@ -599,9 +593,7 @@ Definition list_nth_mut_shared_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0:
@@ -641,9 +633,7 @@ Definition list_nth_shared_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i;
-  let (p1, back_'b) := p in
-  Return (p1, back_'b)
+  list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
@@ -683,9 +673,7 @@ Definition list_nth_shared_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::ignore_input_mut_borrow]: loop 0:
@@ -695,8 +683,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s> 0%u32
-    then (
-      i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt)
+    then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1)
     else Return tt
   end
 .
@@ -715,10 +702,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s> 0%u32
-    then (
-      i1 <- u32_sub i 1%u32;
-      _ <- incr_ignore_input_mut_borrow_loop n1 i1;
-      Return tt)
+    then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1)
     else Return tt
   end
 .
@@ -737,10 +721,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s> 0%u32
-    then (
-      i1 <- u32_sub i 1%u32;
-      _ <- ignore_input_shared_borrow_loop n1 i1;
-      Return tt)
+    then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1)
     else Return tt
   end
 .
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 73c4ee58..76dc4cf6 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -475,9 +475,7 @@ Definition id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
   :=
-  let back_'a := fun (ret : (T1 * T2)) => let (t, t1) := ret in Return (t, t1)
-    in
-  Return ((x, y), back_'a)
+  Return ((x, y), Return)
 .
 
 (** [no_nested_borrows::id_mut_pair2]:
@@ -486,10 +484,7 @@ Definition id_mut_pair2
   (T1 T2 : Type) (p : (T1 * T2)) :
   result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
   :=
-  let (t, t1) := p in
-  let back_'a :=
-    fun (ret : (T1 * T2)) => let (t2, t3) := ret in Return (t2, t3) in
-  Return ((t, t1), back_'a)
+  let (t, t1) := p in Return ((t, t1), Return)
 .
 
 (** [no_nested_borrows::id_mut_pair3]:
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 769cf34c..ad77fa2a 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 :=
 (** [paper::test_incr]:
     Source: 'src/paper.rs', lines 8:0-8:18 *)
 Definition test_incr : result unit :=
-  i <- ref_incr 0%i32; if negb (i s= 1%i32) then Fail_ Failure else Return tt
+  x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt
 .
 
 (** Unit test for [paper::test_incr] *)
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 869cdb4d..308de4f4 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,6 +3,7 @@
 -arg -w
 -arg all
 
+External_FunsExternal_Template.v
 Loops.v
 External_Types.v
 Primitives.v
@@ -10,9 +11,8 @@ External_Funs.v
 External_TypesExternal.v
 Constants.v
 PoloniusList.v
-Paper.v
 NoNestedBorrows.v
 External_FunsExternal.v
 Bitwise.v
 External_TypesExternal_Template.v
-External_FunsExternal_Template.v
+Paper.v