From 975ddb208f18cb4ba46293dd788c46eb1ce43938 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:58:44 +0200
Subject: Regenerate the test files

---
 tests/fstar/misc/External.Funs.fst           |  4 +-
 tests/fstar/misc/External.FunsExternal.fsti  |  9 ++-
 tests/fstar/misc/External.TypesExternal.fsti |  3 +-
 tests/fstar/misc/Loops.Funs.fst              | 83 ++++++++++++++--------------
 tests/fstar/misc/NoNestedBorrows.fst         | 11 ++--
 tests/fstar/misc/Paper.fst                   | 11 ++--
 tests/fstar/misc/PoloniusList.fst            |  4 +-
 7 files changed, 63 insertions(+), 62 deletions(-)

(limited to 'tests/fstar/misc')

diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 3ba20022..78960404 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -34,8 +34,8 @@ let custom_swap
   result (state & (t & (t -> state -> result (state & (t & t)))))
   =
   let* (st1, (x1, y1)) = core_mem_swap t x y st in
-  let back_'a = fun ret st2 -> Return (st2, (ret, y1)) in
-  Return (st1, (x1, back_'a))
+  let back = fun ret st2 -> Return (st2, (ret, y1)) in
+  Return (st1, (x1, back))
 
 (** [external::test_custom_swap]:
     Source: 'src/external.rs', lines 29:0-29:59 *)
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index a412aea9..4c1c58b7 100644
--- a/tests/fstar/misc/External.FunsExternal.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -7,16 +7,19 @@ include External.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::mem::swap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+    Name pattern: core::mem::swap *)
 val core_mem_swap (t : Type0) : t -> t -> state -> result (state & (t & t))
 
 (** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+    Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
 val core_num_nonzero_NonZeroU32_new
   : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
 
 (** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
 val core_option_Option_unwrap
   (t : Type0) : option t -> state -> result (state & t)
 
diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti
index 4bfbe0c5..45174c7e 100644
--- a/tests/fstar/misc/External.TypesExternal.fsti
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -6,7 +6,8 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+    Name pattern: core::num::nonzero::NonZeroU32 *)
 val core_num_nonzero_NonZeroU32_t : Type0
 
 (** The state type used in the state-error monad *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 7c099da2..93683deb 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -289,18 +289,17 @@ let rec list_nth_mut_loop_pair_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl0) in
-        let back_'b = fun ret -> Return (List_Cons ret tl1) in
-        Return ((x0, x1), back_'a, back_'b)
+        let back'a = fun ret -> Return (List_Cons ret tl0) in
+        let back'b = fun ret -> Return (List_Cons ret tl1) in
+        Return ((x0, x1), back'a, back'b)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1
-          in
-        let back_'a1 =
-          fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
-        let back_'b1 =
-          fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
-        Return (p, back_'a1, back_'b1)
+        let* (p, back'a, back'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1 in
+        let back'a1 =
+          fun ret -> let* tl01 = back'a ret in Return (List_Cons x0 tl01) in
+        let back'b1 =
+          fun ret -> let* tl11 = back'b ret in Return (List_Cons x1 tl11) in
+        Return (p, back'a1, back'b1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -352,18 +351,18 @@ let rec list_nth_mut_loop_pair_merge_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a =
+        let back =
           fun ret ->
             let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1) in
-        Return ((x0, x1), back_'a)
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
-        let back_'a1 =
+        let* (p, back) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
+        let back1 =
           fun ret ->
-            let* (tl01, tl11) = back_'a ret in
+            let* (tl01, tl11) = back ret in
             Return (List_Cons x0 tl01, List_Cons x1 tl11) in
-        Return (p, back_'a1)
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -417,14 +416,14 @@ let rec list_nth_mut_shared_loop_pair_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl0) in
-        Return ((x0, x1), back_'a)
+        let back = fun ret -> Return (List_Cons ret tl0) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
-        let back_'a1 =
-          fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
-        Return (p, back_'a1)
+        let* (p, back) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
+        let back1 =
+          fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -451,15 +450,15 @@ let rec list_nth_mut_shared_loop_pair_merge_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl0) in
-        Return ((x0, x1), back_'a)
+        let back = fun ret -> Return (List_Cons ret tl0) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) =
-          list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1 in
-        let back_'a1 =
-          fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
-        Return (p, back_'a1)
+        let* (p, back) = list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1
+          in
+        let back1 =
+          fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -486,14 +485,14 @@ let rec list_nth_shared_mut_loop_pair_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'b = fun ret -> Return (List_Cons ret tl1) in
-        Return ((x0, x1), back_'b)
+        let back = fun ret -> Return (List_Cons ret tl1) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
-        let back_'b1 =
-          fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
-        Return (p, back_'b1)
+        let* (p, back) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
+        let back1 =
+          fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -520,15 +519,15 @@ let rec list_nth_shared_mut_loop_pair_merge_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl1) in
-        Return ((x0, x1), back_'a)
+        let back = fun ret -> Return (List_Cons ret tl1) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) =
-          list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1 in
-        let back_'a1 =
-          fun ret -> let* tl11 = back_'a ret in Return (List_Cons x1 tl11) in
-        Return (p, back_'a1)
+        let* (p, back) = list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1
+          in
+        let back1 =
+          fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index db63eb0d..1a93beaa 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -291,8 +291,8 @@ let _ = assert_norm (test_split_list = Return ())
 let choose
   (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
   if b
-  then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
-  else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+  then let back = fun ret -> Return (ret, y) in Return (x, back)
+  else let back = fun ret -> Return (x, ret) in Return (y, back)
 
 (** [no_nested_borrows::choose_test]:
     Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 *)
@@ -355,15 +355,14 @@ let rec list_nth_mut
   begin match l with
   | List_Cons x tl ->
     if i = 0
-    then
-      let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a)
+    then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
     else
       let* i1 = u32_sub i 1 in
       let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in
-      let back_'a =
+      let back =
         fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1)
         in
-      Return (x1, back_'a)
+      Return (x1, back)
   | List_Nil -> Fail Failure
   end
 
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index ddc5e7a8..c2f47ad1 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -23,8 +23,8 @@ let _ = assert_norm (test_incr = Return ())
 let choose
   (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
   if b
-  then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
-  else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+  then let back = fun ret -> Return (ret, y) in Return (x, back)
+  else let back = fun ret -> Return (x, ret) in Return (y, back)
 
 (** [paper::test_choose]:
     Source: 'src/paper.rs', lines 23:0-23:20 *)
@@ -57,15 +57,14 @@ let rec list_nth_mut
   begin match l with
   | List_Cons x tl ->
     if i = 0
-    then
-      let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a)
+    then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
     else
       let* i1 = u32_sub i 1 in
       let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in
-      let back_'a =
+      let back =
         fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1)
         in
-      Return (x1, back_'a)
+      Return (x1, back)
   | List_Nil -> Fail Failure
   end
 
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index b477802b..4203247e 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -23,10 +23,10 @@ let rec get_list_at_x
     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 =
+      let back =
         fun ret ->
           let* tl1 = get_list_at_x_back ret in Return (List_Cons hd tl1) in
-      Return (l, back_'a)
+      Return (l, back)
   | List_Nil -> Return (List_Nil, Return)
   end
 
-- 
cgit v1.2.3