Merge pull request #123 from AeneasVerif/son/clean

Cleanup the code in preparation of the nested loops

1 files changed, 13 insertions, 14 deletions

diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index c2f47ad1..e6b4eb25 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -13,18 +13,18 @@ let ref_incr (x : i32) : result i32 =
 (** [paper::test_incr]:
     Source: 'src/paper.rs', lines 8:0-8:18 *)
 let test_incr : result unit =
-  let* x = ref_incr 0 in if not (x = 1) then Fail Failure else Return ()
+  let* x = ref_incr 0 in if not (x = 1) then Fail Failure else Ok ()
 
 (** Unit test for [paper::test_incr] *)
-let _ = assert_norm (test_incr = Return ())
+let _ = assert_norm (test_incr = Ok ())
 
 (** [paper::choose]:
     Source: 'src/paper.rs', lines 15:0-15:70 *)
 let choose
   (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
   if b
-  then let back = fun ret -> Return (ret, y) in Return (x, back)
-  else let back = fun ret -> Return (x, ret) in Return (y, back)
+  then let back = fun ret -> Ok (ret, y) in Ok (x, back)
+  else let back = fun ret -> Ok (x, ret) in Ok (y, back)
 
 (** [paper::test_choose]:
     Source: 'src/paper.rs', lines 23:0-23:20 *)
@@ -37,10 +37,10 @@ let test_choose : result unit =
     let* (x, y) = choose_back z1 in
     if not (x = 1)
     then Fail Failure
-    else if not (y = 0) then Fail Failure else Return ()
+    else if not (y = 0) then Fail Failure else Ok ()
 
 (** Unit test for [paper::test_choose] *)
-let _ = assert_norm (test_choose = Return ())
+let _ = assert_norm (test_choose = Ok ())
 
 (** [paper::List]
     Source: 'src/paper.rs', lines 35:0-35:16 *)
@@ -57,14 +57,13 @@ let rec list_nth_mut
   begin match l with
   | List_Cons x tl ->
     if i = 0
-    then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
+    then let back = fun ret -> Ok (List_Cons ret tl) in Ok (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 =
-        fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1)
-        in
-      Return (x1, back)
+        fun ret -> let* tl1 = list_nth_mut_back ret in Ok (List_Cons x tl1) in
+      Ok (x1, back)
   | List_Nil -> Fail Failure
   end
 
@@ -73,7 +72,7 @@ let rec list_nth_mut
 let rec sum (l : list_t i32) : result i32 =
   begin match l with
   | List_Cons x tl -> let* i = sum tl in i32_add x i
-  | List_Nil -> Return 0
+  | List_Nil -> Ok 0
   end
 
 (** [paper::test_nth]:
@@ -85,10 +84,10 @@ let test_nth : result unit =
   let* x1 = i32_add x 1 in
   let* l2 = list_nth_mut_back x1 in
   let* i = sum l2 in
-  if not (i = 7) then Fail Failure else Return ()
+  if not (i = 7) then Fail Failure else Ok ()
 
 (** Unit test for [paper::test_nth] *)
-let _ = assert_norm (test_nth = Return ())
+let _ = assert_norm (test_nth = Ok ())
 
 (** [paper::call_choose]:
     Source: 'src/paper.rs', lines 76:0-76:44 *)
@@ -97,5 +96,5 @@ let call_choose (p : (u32 & u32)) : result u32 =
   let* (pz, choose_back) = choose u32 true px py in
   let* pz1 = u32_add pz 1 in
   let* (px1, _) = choose_back pz1 in
-  Return px1
+  Ok px1