Merge branch 'main' into son/clean-synthesis

1 files changed, 85 insertions, 87 deletions

diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 7e333b56..a5ba31bc 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -71,7 +71,7 @@ let test3 : result unit =
   let* x = get_max 4 3 in
   let* y = get_max 10 11 in
   let* z = u32_add x y in
-  if not (z = 15) then Fail Failure else Ok ()
+  if z = 15 then Ok () else Fail Failure
 
 (** Unit test for [no_nested_borrows::test3] *)
 let _ = assert_norm (test3 = Ok ())
@@ -79,7 +79,7 @@ let _ = assert_norm (test3 = Ok ())
 (** [no_nested_borrows::test_neg1]:
     Source: 'tests/src/no_nested_borrows.rs', lines 90:0-90:18 *)
 let test_neg1 : result unit =
-  let* y = i32_neg 3 in if not (y = -3) then Fail Failure else Ok ()
+  let* y = i32_neg 3 in if y = -3 then Ok () else Fail Failure
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
 let _ = assert_norm (test_neg1 = Ok ())
@@ -87,7 +87,7 @@ let _ = assert_norm (test_neg1 = Ok ())
 (** [no_nested_borrows::refs_test1]:
     Source: 'tests/src/no_nested_borrows.rs', lines 97:0-97:19 *)
 let refs_test1 : result unit =
-  if not (1 = 1) then Fail Failure else Ok ()
+  if 1 = 1 then Ok () else Fail Failure
 
 (** Unit test for [no_nested_borrows::refs_test1] *)
 let _ = assert_norm (refs_test1 = Ok ())
@@ -95,15 +95,12 @@ let _ = assert_norm (refs_test1 = Ok ())
 (** [no_nested_borrows::refs_test2]:
     Source: 'tests/src/no_nested_borrows.rs', lines 108:0-108:19 *)
 let refs_test2 : result unit =
-  if not (2 = 2)
-  then Fail Failure
-  else
-    if not (0 = 0)
-    then Fail Failure
-    else
-      if not (2 = 2)
-      then Fail Failure
-      else if not (2 = 2) then Fail Failure else Ok ()
+  if 2 = 2
+  then
+    if 0 = 0
+    then if 2 = 2 then if 2 = 2 then Ok () else Fail Failure else Fail Failure
+    else Fail Failure
+  else Fail Failure
 
 (** Unit test for [no_nested_borrows::refs_test2] *)
 let _ = assert_norm (refs_test2 = Ok ())
@@ -122,7 +119,7 @@ let test_box1 : result unit =
   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 Ok ()
+  if x = 1 then Ok () else Fail Failure
 
 (** Unit test for [no_nested_borrows::test_box1] *)
 let _ = assert_norm (test_box1 = Ok ())
@@ -145,7 +142,7 @@ let test_panic (b : bool) : result unit =
 (** [no_nested_borrows::test_copy_int]:
     Source: 'tests/src/no_nested_borrows.rs', lines 160:0-160:22 *)
 let test_copy_int : result unit =
-  let* y = copy_int 0 in if not (0 = y) then Fail Failure else Ok ()
+  let* y = copy_int 0 in if 0 = y then Ok () else Fail Failure
 
 (** Unit test for [no_nested_borrows::test_copy_int] *)
 let _ = assert_norm (test_copy_int = Ok ())
@@ -159,7 +156,7 @@ let is_cons (t : Type0) (l : list_t t) : result bool =
     Source: 'tests/src/no_nested_borrows.rs', lines 174:0-174:21 *)
 let test_is_cons : result unit =
   let* b = is_cons i32 (List_Cons 0 List_Nil) in
-  if not b then Fail Failure else Ok ()
+  if b then Ok () else Fail Failure
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
 let _ = assert_norm (test_is_cons = Ok ())
@@ -177,7 +174,7 @@ let split_list (t : Type0) (l : list_t t) : result (t & (list_t t)) =
 let test_split_list : result unit =
   let* p = split_list i32 (List_Cons 0 List_Nil) in
   let (hd, _) = p in
-  if not (hd = 0) then Fail Failure else Ok ()
+  if hd = 0 then Ok () else Fail Failure
 
 (** Unit test for [no_nested_borrows::test_split_list] *)
 let _ = assert_norm (test_split_list = Ok ())
@@ -195,13 +192,11 @@ let choose
 let choose_test : result unit =
   let* (z, choose_back) = choose i32 true 0 0 in
   let* z1 = i32_add z 1 in
-  if not (z1 = 1)
-  then Fail Failure
-  else
+  if z1 = 1
+  then
     let* (x, y) = choose_back z1 in
-    if not (x = 1)
-    then Fail Failure
-    else if not (y = 0) then Fail Failure else Ok ()
+    if x = 1 then if y = 0 then Ok () else Fail Failure else Fail Failure
+  else Fail Failure
 
 (** Unit test for [no_nested_borrows::choose_test] *)
 let _ = assert_norm (choose_test = Ok ())
@@ -211,20 +206,25 @@ let _ = assert_norm (choose_test = Ok ())
 let test_char : result char =
   Ok 'a'
 
+(** [no_nested_borrows::panic_mut_borrow]:
+    Source: 'tests/src/no_nested_borrows.rs', lines 220:0-220:36 *)
+let panic_mut_borrow (i : u32) : result u32 =
+  Fail Failure
+
 (** [no_nested_borrows::Tree]
-    Source: 'tests/src/no_nested_borrows.rs', lines 220:0-220:16 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 225:0-225:16 *)
 type tree_t (t : Type0) =
 | Tree_Leaf : t -> tree_t t
 | Tree_Node : t -> nodeElem_t t -> tree_t t -> tree_t t
 
 (** [no_nested_borrows::NodeElem]
-    Source: 'tests/src/no_nested_borrows.rs', lines 225:0-225:20 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 230:0-230:20 *)
 and nodeElem_t (t : Type0) =
 | NodeElem_Cons : tree_t t -> nodeElem_t t -> nodeElem_t t
 | NodeElem_Nil : nodeElem_t t
 
 (** [no_nested_borrows::list_length]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 260:0-260:48 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 265:0-265:48 *)
 let rec list_length (t : Type0) (l : list_t t) : result u32 =
   begin match l with
   | List_Cons _ l1 -> let* i = list_length t l1 in u32_add 1 i
@@ -232,7 +232,7 @@ let rec list_length (t : Type0) (l : list_t t) : result u32 =
   end
 
 (** [no_nested_borrows::list_nth_shared]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 268:0-268:62 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 273:0-273:62 *)
 let rec list_nth_shared (t : Type0) (l : list_t t) (i : u32) : result t =
   begin match l with
   | List_Cons x tl ->
@@ -241,7 +241,7 @@ let rec list_nth_shared (t : Type0) (l : list_t t) (i : u32) : result t =
   end
 
 (** [no_nested_borrows::list_nth_mut]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 284:0-284:67 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 289:0-289:67 *)
 let rec list_nth_mut
   (t : Type0) (l : list_t t) (i : u32) :
   result (t & (t -> result (list_t t)))
@@ -260,7 +260,7 @@ let rec list_nth_mut
   end
 
 (** [no_nested_borrows::list_rev_aux]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 300:0-300:63 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 305:0-305:63 *)
 let rec list_rev_aux
   (t : Type0) (li : list_t t) (lo : list_t t) : result (list_t t) =
   begin match li with
@@ -269,50 +269,50 @@ let rec list_rev_aux
   end
 
 (** [no_nested_borrows::list_rev]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 314:0-314:42 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:42 *)
 let list_rev (t : Type0) (l : list_t t) : result (list_t t) =
   let (li, _) = core_mem_replace (list_t t) l List_Nil in
   list_rev_aux t li List_Nil
 
 (** [no_nested_borrows::test_list_functions]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:28 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 324:0-324:28 *)
 let test_list_functions : result unit =
   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
+  if i = 3
+  then
     let* i1 = list_nth_shared i32 (List_Cons 0 l1) 0 in
-    if not (i1 = 0)
-    then Fail Failure
-    else
+    if i1 = 0
+    then
       let* i2 = list_nth_shared i32 (List_Cons 0 l1) 1 in
-      if not (i2 = 1)
-      then Fail Failure
-      else
+      if i2 = 1
+      then
         let* i3 = list_nth_shared i32 (List_Cons 0 l1) 2 in
-        if not (i3 = 2)
-        then Fail Failure
-        else
+        if i3 = 2
+        then
           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)
-          then Fail Failure
-          else
+          if i4 = 0
+          then
             let* i5 = list_nth_shared i32 ls 1 in
-            if not (i5 = 3)
-            then Fail Failure
-            else
+            if i5 = 3
+            then
               let* i6 = list_nth_shared i32 ls 2 in
-              if not (i6 = 2) then Fail Failure else Ok ()
+              if i6 = 2 then Ok () else Fail Failure
+            else Fail Failure
+          else Fail Failure
+        else Fail Failure
+      else Fail Failure
+    else Fail Failure
+  else Fail Failure
 
 (** Unit test for [no_nested_borrows::test_list_functions] *)
 let _ = assert_norm (test_list_functions = Ok ())
 
 (** [no_nested_borrows::id_mut_pair1]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 335:0-335:89 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 340:0-340:89 *)
 let id_mut_pair1
   (t1 t2 : Type0) (x : t1) (y : t2) :
   result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2)))
@@ -320,7 +320,7 @@ let id_mut_pair1
   Ok ((x, y), Ok)
 
 (** [no_nested_borrows::id_mut_pair2]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 339:0-339:88 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 344:0-344:88 *)
 let id_mut_pair2
   (t1 t2 : Type0) (p : (t1 & t2)) :
   result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2)))
@@ -328,7 +328,7 @@ let id_mut_pair2
   let (x, x1) = p in Ok ((x, x1), Ok)
 
 (** [no_nested_borrows::id_mut_pair3]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 343:0-343:93 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 348:0-348:93 *)
 let id_mut_pair3
   (t1 t2 : Type0) (x : t1) (y : t2) :
   result ((t1 & t2) & (t1 -> result t1) & (t2 -> result t2))
@@ -336,7 +336,7 @@ let id_mut_pair3
   Ok ((x, y), Ok, Ok)
 
 (** [no_nested_borrows::id_mut_pair4]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 347:0-347:92 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 352:0-352:92 *)
 let id_mut_pair4
   (t1 t2 : Type0) (p : (t1 & t2)) :
   result ((t1 & t2) & (t1 -> result t1) & (t2 -> result t2))
@@ -344,59 +344,57 @@ let id_mut_pair4
   let (x, x1) = p in Ok ((x, x1), Ok, Ok)
 
 (** [no_nested_borrows::StructWithTuple]
-    Source: 'tests/src/no_nested_borrows.rs', lines 354:0-354:34 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 359:0-359:34 *)
 type structWithTuple_t (t1 t2 : Type0) = { p : (t1 & t2); }
 
 (** [no_nested_borrows::new_tuple1]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 358:0-358:48 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 *)
 let new_tuple1 : result (structWithTuple_t u32 u32) =
   Ok { p = (1, 2) }
 
 (** [no_nested_borrows::new_tuple2]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 362:0-362:48 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 367:0-367:48 *)
 let new_tuple2 : result (structWithTuple_t i16 i16) =
   Ok { p = (1, 2) }
 
 (** [no_nested_borrows::new_tuple3]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 366:0-366:48 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:48 *)
 let new_tuple3 : result (structWithTuple_t u64 i64) =
   Ok { p = (1, 2) }
 
 (** [no_nested_borrows::StructWithPair]
-    Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:33 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 376:0-376:33 *)
 type structWithPair_t (t1 t2 : Type0) = { p : pair_t t1 t2; }
 
 (** [no_nested_borrows::new_pair1]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 375:0-375:46 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:46 *)
 let new_pair1 : result (structWithPair_t u32 u32) =
   Ok { p = { x = 1; y = 2 } }
 
 (** [no_nested_borrows::test_constants]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 383:0-383:23 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 388:0-388:23 *)
 let test_constants : result unit =
   let* swt = new_tuple1 in
   let (i, _) = swt.p in
-  if not (i = 1)
-  then Fail Failure
-  else
+  if i = 1
+  then
     let* swt1 = new_tuple2 in
     let (i1, _) = swt1.p in
-    if not (i1 = 1)
-    then Fail Failure
-    else
+    if i1 = 1
+    then
       let* swt2 = new_tuple3 in
       let (i2, _) = swt2.p in
-      if not (i2 = 1)
-      then Fail Failure
-      else
-        let* swp = new_pair1 in
-        if not (swp.p.x = 1) then Fail Failure else Ok ()
+      if i2 = 1
+      then let* swp = new_pair1 in if swp.p.x = 1 then Ok () else Fail Failure
+      else Fail Failure
+    else Fail Failure
+  else Fail Failure
 
 (** Unit test for [no_nested_borrows::test_constants] *)
 let _ = assert_norm (test_constants = Ok ())
 
 (** [no_nested_borrows::test_weird_borrows1]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 392:0-392:28 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 397:0-397:28 *)
 let test_weird_borrows1 : result unit =
   Ok ()
 
@@ -404,71 +402,71 @@ let test_weird_borrows1 : result unit =
 let _ = assert_norm (test_weird_borrows1 = Ok ())
 
 (** [no_nested_borrows::test_mem_replace]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 402:0-402:37 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 *)
 let test_mem_replace (px : u32) : result u32 =
   let (y, _) = core_mem_replace u32 px 1 in
-  if not (y = 0) then Fail Failure else Ok 2
+  if y = 0 then Ok 2 else Fail Failure
 
 (** [no_nested_borrows::test_shared_borrow_bool1]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 409:0-409:47 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 414:0-414:47 *)
 let test_shared_borrow_bool1 (b : bool) : result u32 =
   if b then Ok 0 else Ok 1
 
 (** [no_nested_borrows::test_shared_borrow_bool2]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 422:0-422:40 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 427:0-427:40 *)
 let test_shared_borrow_bool2 : result u32 =
   Ok 0
 
 (** [no_nested_borrows::test_shared_borrow_enum1]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 437:0-437:52 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 442:0-442:52 *)
 let test_shared_borrow_enum1 (l : list_t u32) : result u32 =
   begin match l with | List_Cons _ _ -> Ok 1 | List_Nil -> Ok 0 end
 
 (** [no_nested_borrows::test_shared_borrow_enum2]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 449:0-449:40 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 454:0-454:40 *)
 let test_shared_borrow_enum2 : result u32 =
   Ok 0
 
 (** [no_nested_borrows::incr]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 460:0-460:24 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 *)
 let incr (x : u32) : result u32 =
   u32_add x 1
 
 (** [no_nested_borrows::call_incr]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 464:0-464:35 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:35 *)
 let call_incr (x : u32) : result u32 =
   incr x
 
 (** [no_nested_borrows::read_then_incr]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:41 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 474:0-474:41 *)
 let read_then_incr (x : u32) : result (u32 & u32) =
   let* x1 = u32_add x 1 in Ok (x, x1)
 
 (** [no_nested_borrows::Tuple]
-    Source: 'tests/src/no_nested_borrows.rs', lines 475:0-475:24 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 *)
 type tuple_t (t1 t2 : Type0) = t1 * t2
 
 (** [no_nested_borrows::use_tuple_struct]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 477:0-477:48 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 *)
 let use_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) =
   let (_, i) = x in Ok (1, i)
 
 (** [no_nested_borrows::create_tuple_struct]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 481:0-481:61 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 *)
 let create_tuple_struct (x : u32) (y : u64) : result (tuple_t u32 u64) =
   Ok (x, y)
 
 (** [no_nested_borrows::IdType]
-    Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:20 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 *)
 type idType_t (t : Type0) = t
 
 (** [no_nested_borrows::use_id_type]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 488:0-488:40 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 *)
 let use_id_type (t : Type0) (x : idType_t t) : result t =
   Ok x
 
 (** [no_nested_borrows::create_id_type]:
-    Source: 'tests/src/no_nested_borrows.rs', lines 492:0-492:43 *)
+    Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 *)
 let create_id_type (t : Type0) (x : t) : result (idType_t t) =
   Ok x