Regenerate the files

4 files changed, 22 insertions, 36 deletions

diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index bb1b9a64..6672b523 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -22,9 +22,7 @@ let test_new_non_zero_u32
 (** [external::test_vec]:
     Source: 'src/external.rs', lines 17:0-17:17 *)
 let test_vec : result unit =
-  let v = alloc_vec_Vec_new u32 in
-  let* _ = alloc_vec_Vec_push u32 v 0 in
-  Return ()
+  let* _ = alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0 in Return ()
 
 (** Unit test for [external::test_vec] *)
 let _ = assert_norm (test_vec = Return ())
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 0fd0c1dc..ffcc32f3 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -220,10 +220,9 @@ let _ = assert_norm (test_list1 = Return ())
 (** [no_nested_borrows::test_box1]:
     Source: 'src/no_nested_borrows.rs', lines 208:0-208:18 *)
 let test_box1 : result unit =
-  let b = 0 in
-  let* (_, deref_mut_back) = alloc_boxed_Box_deref_mut i32 b in
-  let* b1 = deref_mut_back 1 in
-  let* x = alloc_boxed_Box_deref i32 b1 in
+  let* (_, deref_mut_back) = alloc_boxed_Box_deref_mut i32 0 in
+  let* b = deref_mut_back 1 in
+  let* x = alloc_boxed_Box_deref i32 b in
   if not (x = 1) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_box1] *)
@@ -263,8 +262,7 @@ let is_cons (t : Type0) (l : list_t t) : result bool =
 (** [no_nested_borrows::test_is_cons]:
     Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 *)
 let test_is_cons : result unit =
-  let l = List_Nil in
-  let* b = is_cons i32 (List_Cons 0 l) in
+  let* b = is_cons i32 (List_Cons 0 List_Nil) in
   if not b then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -281,8 +279,7 @@ let split_list (t : Type0) (l : list_t t) : result (t & (list_t t)) =
 (** [no_nested_borrows::test_split_list]:
     Source: 'src/no_nested_borrows.rs', lines 267:0-267:24 *)
 let test_split_list : result unit =
-  let l = List_Nil in
-  let* p = split_list i32 (List_Cons 0 l) in
+  let* p = split_list i32 (List_Cons 0 List_Nil) in
   let (hd, _) = p in
   if not (hd = 0) then Fail Failure else Return ()
 
@@ -388,26 +385,25 @@ let list_rev (t : Type0) (l : list_t t) : result (list_t t) =
 (** [no_nested_borrows::test_list_functions]:
     Source: 'src/no_nested_borrows.rs', lines 398:0-398:28 *)
 let test_list_functions : result unit =
-  let l = List_Nil in
-  let l1 = List_Cons 2 l in
-  let l2 = List_Cons 1 l1 in
-  let* i = list_length i32 (List_Cons 0 l2) in
+  let l = List_Cons 2 List_Nil in
+  let l1 = List_Cons 1 l in
+  let* i = list_length i32 (List_Cons 0 l1) in
   if not (i = 3)
   then Fail Failure
   else
-    let* i1 = list_nth_shared i32 (List_Cons 0 l2) 0 in
+    let* i1 = list_nth_shared i32 (List_Cons 0 l1) 0 in
     if not (i1 = 0)
     then Fail Failure
     else
-      let* i2 = list_nth_shared i32 (List_Cons 0 l2) 1 in
+      let* i2 = list_nth_shared i32 (List_Cons 0 l1) 1 in
       if not (i2 = 1)
       then Fail Failure
       else
-        let* i3 = list_nth_shared i32 (List_Cons 0 l2) 2 in
+        let* i3 = list_nth_shared i32 (List_Cons 0 l1) 2 in
         if not (i3 = 2)
         then Fail Failure
         else
-          let* (_, list_nth_mut_back) = list_nth_mut i32 (List_Cons 0 l2) 1 in
+          let* (_, list_nth_mut_back) = list_nth_mut i32 (List_Cons 0 l1) 1 in
           let* ls = list_nth_mut_back 3 in
           let* i4 = list_nth_shared i32 ls 0 in
           if not (i4 = 0)
@@ -448,9 +444,7 @@ let id_mut_pair3
   (t1 t2 : Type0) (x : t1) (y : t2) :
   result ((t1 & t2) & (t1 -> result t1) & (t2 -> result t2))
   =
-  let back_'a = fun ret -> Return ret in
-  let back_'b = fun ret -> Return ret in
-  Return ((x, y), back_'a, back_'b)
+  Return ((x, y), Return, Return)
 
 (** [no_nested_borrows::id_mut_pair4]:
     Source: 'src/no_nested_borrows.rs', lines 426:0-426:92 *)
@@ -458,10 +452,7 @@ let id_mut_pair4
   (t1 t2 : Type0) (p : (t1 & t2)) :
   result ((t1 & t2) & (t1 -> result t1) & (t2 -> result t2))
   =
-  let (x, x1) = p in
-  let back_'a = fun ret -> Return ret in
-  let back_'b = fun ret -> Return ret in
-  Return ((x, x1), back_'a, back_'b)
+  let (x, x1) = p in Return ((x, x1), Return, Return)
 
 (** [no_nested_borrows::StructWithTuple]
     Source: 'src/no_nested_borrows.rs', lines 433:0-433:34 *)
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index c6082929..cf4dc454 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -80,13 +80,12 @@ let rec sum (l : list_t i32) : result i32 =
 (** [paper::test_nth]:
     Source: 'src/paper.rs', lines 68:0-68:17 *)
 let test_nth : result unit =
-  let l = List_Nil in
-  let l1 = List_Cons 3 l in
-  let l2 = List_Cons 2 l1 in
-  let* (x, list_nth_mut_back) = list_nth_mut i32 (List_Cons 1 l2) 2 in
+  let l = List_Cons 3 List_Nil in
+  let l1 = List_Cons 2 l in
+  let* (x, list_nth_mut_back) = list_nth_mut i32 (List_Cons 1 l1) 2 in
   let* x1 = i32_add x 1 in
-  let* l3 = list_nth_mut_back x1 in
-  let* i = sum l3 in
+  let* l2 = list_nth_mut_back x1 in
+  let* i = sum l2 in
   if not (i = 7) then Fail Failure else Return ()
 
 (** Unit test for [paper::test_nth] *)
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index cbe7d6b8..b477802b 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -20,15 +20,13 @@ let rec get_list_at_x
   begin match ls with
   | List_Cons hd tl ->
     if hd = x
-    then
-      let back_'a = fun ret -> Return ret in Return (List_Cons hd tl, back_'a)
+    then Return (List_Cons hd tl, Return)
     else
       let* (l, get_list_at_x_back) = get_list_at_x tl x in
       let back_'a =
         fun ret ->
           let* tl1 = get_list_at_x_back ret in Return (List_Cons hd tl1) in
       Return (l, back_'a)
-  | List_Nil ->
-    let back_'a = fun ret -> Return ret in Return (List_Nil, back_'a)
+  | List_Nil -> Return (List_Nil, Return)
   end