Regenerate the test files and add the fstar-split tests

1 files changed, 15 insertions, 15 deletions

diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 188b22d8..cbe7d6b8 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -11,24 +11,24 @@ type list_t (t : Type0) =
 | List_Cons : t -> list_t t -> list_t t
 | List_Nil : list_t t
 
-(** [polonius_list::get_list_at_x]: forward function
+(** [polonius_list::get_list_at_x]:
     Source: 'src/polonius_list.rs', lines 13:0-13:76 *)
-let rec get_list_at_x (ls : list_t u32) (x : u32) : result (list_t u32) =
-  begin match ls with
-  | List_Cons hd tl ->
-    if hd = x then Return (List_Cons hd tl) else get_list_at_x tl x
-  | List_Nil -> Return List_Nil
-  end
-
-(** [polonius_list::get_list_at_x]: backward function 0
-    Source: 'src/polonius_list.rs', lines 13:0-13:76 *)
-let rec get_list_at_x_back
-  (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
+let rec get_list_at_x
+  (ls : list_t u32) (x : u32) :
+  result ((list_t u32) & (list_t u32 -> result (list_t u32)))
+  =
   begin match ls with
   | List_Cons hd tl ->
     if hd = x
-    then Return ret
-    else let* tl0 = get_list_at_x_back tl x ret in Return (List_Cons hd tl0)
-  | List_Nil -> Return ret
+    then
+      let back_'a = fun ret -> Return ret in Return (List_Cons hd tl, back_'a)
+    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)
   end