From 7ca25ab5c3e686eaca2716d003bfb04e742209ec Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 15 May 2022 22:35:23 +0200
Subject: Regenerate the F* files

---
 tests/misc/External.Funs.fst   |  3 +--
 tests/misc/NoNestedBorrows.fst | 49 ++++++++++++++++++++++--------------------
 tests/misc/Paper.fst           | 14 ++++++------
 tests/misc/Primitives.fst      |  2 +-
 4 files changed, 34 insertions(+), 34 deletions(-)

(limited to 'tests/misc')

diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index aafc0cf6..874b739c 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -109,8 +109,7 @@ let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
   | Return (st0, _) ->
     begin match swap_back u32 x 0 st with
     | Fail -> Fail
-    | Return (x0, _) ->
-      begin match x0 with | 0 -> Fail | _ -> Return (st0, x0) end
+    | Return (x0, _) -> if x0 = 0 then Fail else Return (st0, x0)
     end
   end
 
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index 97688191..35d32514 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -56,10 +56,14 @@ let rem_test_fwd (x : u32) (y : u32) : result u32 =
 
 (** [no_nested_borrows::cast_test] *)
 let cast_test_fwd (x : u32) : result i32 =
-  begin match scalar_cast I32 x with | Fail -> Fail | Return i -> Return i end
+  begin match scalar_cast U32 I32 x with
+  | Fail -> Fail
+  | Return i -> Return i
+  end
 
 (** [no_nested_borrows::test2] *)
-let test2_fwd : result unit = Return ()
+let test2_fwd : result unit =
+  begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end
 
 (** Unit test for [no_nested_borrows::test2] *)
 let _ = assert_norm (test2_fwd = Return ())
@@ -87,7 +91,11 @@ let test3_fwd : result unit =
 let _ = assert_norm (test3_fwd = Return ())
 
 (** [no_nested_borrows::test_neg1] *)
-let test_neg1_fwd : result unit = Return ()
+let test_neg1_fwd : result unit =
+  begin match i32_neg 3 with
+  | Fail -> Fail
+  | Return y -> if not (y = -3) then Fail else Return ()
+  end
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
 let _ = assert_norm (test_neg1_fwd = Return ())
@@ -222,27 +230,25 @@ and node_elem_t (t : Type0) =
 
 (** [no_nested_borrows::even] *)
 let rec even_fwd (x : u32) : result bool =
-  begin match x with
-  | 0 -> Return true
-  | _ ->
+  if x = 0
+  then Return true
+  else
     begin match u32_sub x 1 with
     | Fail -> Fail
     | Return i ->
       begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end
     end
-  end
 
 (** [no_nested_borrows::odd] *)
 and odd_fwd (x : u32) : result bool =
-  begin match x with
-  | 0 -> Return false
-  | _ ->
+  if x = 0
+  then Return false
+  else
     begin match u32_sub x 1 with
     | Fail -> Fail
     | Return i ->
       begin match even_fwd i with | Fail -> Fail | Return b -> Return b end
     end
-  end
 
 (** [no_nested_borrows::test_even_odd] *)
 let test_even_odd_fwd : result unit =
@@ -291,9 +297,9 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
 let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
   begin match l with
   | ListCons x tl ->
-    begin match i with
-    | 0 -> Return x
-    | _ ->
+    if i = 0
+    then Return x
+    else
       begin match u32_sub i 1 with
       | Fail -> Fail
       | Return i0 ->
@@ -302,7 +308,6 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
         | Return x0 -> Return x0
         end
       end
-    end
   | ListNil -> Fail
   end
 
@@ -310,9 +315,9 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
 let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
   begin match l with
   | ListCons x tl ->
-    begin match i with
-    | 0 -> Return x
-    | _ ->
+    if i = 0
+    then Return x
+    else
       begin match u32_sub i 1 with
       | Fail -> Fail
       | Return i0 ->
@@ -321,7 +326,6 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
         | Return x0 -> Return x0
         end
       end
-    end
   | ListNil -> Fail
   end
 
@@ -330,9 +334,9 @@ let rec list_nth_mut_back
   (t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
   begin match l with
   | ListCons x tl ->
-    begin match i with
-    | 0 -> Return (ListCons ret tl)
-    | _ ->
+    if i = 0
+    then Return (ListCons ret tl)
+    else
       begin match u32_sub i 1 with
       | Fail -> Fail
       | Return i0 ->
@@ -341,7 +345,6 @@ let rec list_nth_mut_back
         | Return tl0 -> Return (ListCons x tl0)
         end
       end
-    end
   | ListNil -> Fail
   end
 
diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
index d162519a..424889ef 100644
--- a/tests/misc/Paper.fst
+++ b/tests/misc/Paper.fst
@@ -59,9 +59,9 @@ type list_t (t : Type0) =
 let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
   begin match l with
   | ListCons x tl ->
-    begin match i with
-    | 0 -> Return x
-    | _ ->
+    if i = 0
+    then Return x
+    else
       begin match u32_sub i 1 with
       | Fail -> Fail
       | Return i0 ->
@@ -70,7 +70,6 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
         | Return x0 -> Return x0
         end
       end
-    end
   | ListNil -> Fail
   end
 
@@ -79,9 +78,9 @@ let rec list_nth_mut_back
   (t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
   begin match l with
   | ListCons x tl ->
-    begin match i with
-    | 0 -> Return (ListCons ret tl)
-    | _ ->
+    if i = 0
+    then Return (ListCons ret tl)
+    else
       begin match u32_sub i 1 with
       | Fail -> Fail
       | Return i0 ->
@@ -90,7 +89,6 @@ let rec list_nth_mut_back
         | Return tl0 -> Return (ListCons x tl0)
         end
       end
-    end
   | ListNil -> Fail
   end
 
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/misc/Primitives.fst
+++ b/tests/misc/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
 /// The scalar types
-- 
cgit v1.2.3