Merge pull request #123 from AeneasVerif/son/clean

Cleanup the code in preparation of the nested loops

1 files changed, 55 insertions, 65 deletions

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index ae529cf8..f396f16f 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -83,7 +83,7 @@ Fixpoint sum_array_loop
       s1 <- u32_add s i1;
       i2 <- usize_add i 1%usize;
       sum_array_loop N n1 a i2 s1)
-    else Return s
+    else Ok s
   end
 .
 
@@ -110,7 +110,7 @@ Fixpoint clear_loop
       i2 <- usize_add i 1%usize;
       v1 <- index_mut_back 0%u32;
       clear_loop n1 v1 i2)
-    else Return v
+    else Ok v
   end
 .
 
@@ -138,8 +138,8 @@ Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     match ls with
-    | List_Cons y tl => if y s= x then Return true else list_mem_loop n1 x tl
-    | List_Nil => Return false
+    | List_Cons y tl => if y s= x then Ok true else list_mem_loop n1 x tl
+    | List_Nil => Ok false
     end
   end
 .
@@ -162,16 +162,13 @@ Fixpoint list_nth_mut_loop_loop
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
-      then
-        let back := fun (ret : T) => Return (List_Cons ret tl) in
-        Return (x, back)
+      then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back)
       else (
         i1 <- u32_sub i 1%u32;
         p <- list_nth_mut_loop_loop T n1 tl i1;
         let (t, back) := p in
-        let back1 := fun (ret : T) => tl1 <- back ret; Return (List_Cons x tl1)
-          in
-        Return (t, back1))
+        let back1 := fun (ret : T) => tl1 <- back ret; Ok (List_Cons x tl1) in
+        Ok (t, back1))
     | List_Nil => Fail_ Failure
     end
   end
@@ -196,7 +193,7 @@ Fixpoint list_nth_shared_loop_loop
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
-      then Return x
+      then Ok x
       else (i1 <- u32_sub i 1%u32; list_nth_shared_loop_loop T n1 tl i1)
     | List_Nil => Fail_ Failure
     end
@@ -223,14 +220,13 @@ Fixpoint get_elem_mut_loop
     | List_Cons y tl =>
       if y s= x
       then
-        let back := fun (ret : usize) => Return (List_Cons ret tl) in
-        Return (y, back)
+        let back := fun (ret : usize) => Ok (List_Cons ret tl) in Ok (y, back)
       else (
         p <- get_elem_mut_loop n1 x tl;
         let (i, back) := p in
-        let back1 :=
-          fun (ret : usize) => tl1 <- back ret; Return (List_Cons y tl1) in
-        Return (i, back1))
+        let back1 := fun (ret : usize) => tl1 <- back ret; Ok (List_Cons y tl1)
+          in
+        Ok (i, back1))
     | List_Nil => Fail_ Failure
     end
   end
@@ -249,7 +245,7 @@ Definition get_elem_mut
   p1 <- get_elem_mut_loop n x ls;
   let (i, back) := p1 in
   let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in
-  Return (i, back1)
+  Ok (i, back1)
 .
 
 (** [loops::get_elem_shared]: loop 0:
@@ -260,8 +256,7 @@ Fixpoint get_elem_shared_loop
   | O => Fail_ OutOfFuel
   | S n1 =>
     match ls with
-    | List_Cons y tl =>
-      if y s= x then Return y else get_elem_shared_loop n1 x tl
+    | List_Cons y tl => if y s= x then Ok y else get_elem_shared_loop n1 x tl
     | List_Nil => Fail_ Failure
     end
   end
@@ -285,14 +280,13 @@ Definition id_mut
   (T : Type) (ls : List_t T) :
   result ((List_t T) * (List_t T -> result (List_t T)))
   :=
-  Return (ls, Return)
+  Ok (ls, Ok)
 .
 
 (** [loops::id_shared]:
     Source: 'src/loops.rs', lines 149:0-149:45 *)
 Definition id_shared (T : Type) (ls : List_t T) : result (List_t T) :=
-  Return ls
-.
+  Ok ls.
 
 (** [loops::list_nth_mut_loop_with_id]: loop 0:
     Source: 'src/loops.rs', lines 154:0-165:1 *)
@@ -306,16 +300,13 @@ Fixpoint list_nth_mut_loop_with_id_loop
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
-      then
-        let back := fun (ret : T) => Return (List_Cons ret tl) in
-        Return (x, back)
+      then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back)
       else (
         i1 <- u32_sub i 1%u32;
         p <- list_nth_mut_loop_with_id_loop T n1 i1 tl;
         let (t, back) := p in
-        let back1 := fun (ret : T) => tl1 <- back ret; Return (List_Cons x tl1)
-          in
-        Return (t, back1))
+        let back1 := fun (ret : T) => tl1 <- back ret; Ok (List_Cons x tl1) in
+        Ok (t, back1))
     | List_Nil => Fail_ Failure
     end
   end
@@ -332,7 +323,7 @@ Definition list_nth_mut_loop_with_id
   p1 <- list_nth_mut_loop_with_id_loop T n i ls1;
   let (t, back) := p1 in
   let back1 := fun (ret : T) => l <- back ret; id_mut_back l in
-  Return (t, back1)
+  Ok (t, back1)
 .
 
 (** [loops::list_nth_shared_loop_with_id]: loop 0:
@@ -345,7 +336,7 @@ Fixpoint list_nth_shared_loop_with_id_loop
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
-      then Return x
+      then Ok x
       else (
         i1 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop T n1 i1 tl)
     | List_Nil => Fail_ Failure
@@ -375,18 +366,18 @@ Fixpoint list_nth_mut_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back'a := fun (ret : T) => Return (List_Cons ret tl0) in
-          let back'b := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back'a, back'b)
+          let back'a := fun (ret : T) => Ok (List_Cons ret tl0) in
+          let back'b := fun (ret : T) => Ok (List_Cons ret tl1) in
+          Ok ((x0, x1), back'a, back'b)
         else (
           i1 <- u32_sub i 1%u32;
           t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1;
           let '(p, back'a, back'b) := t in
           let back'a1 :=
-            fun (ret : T) => tl01 <- back'a ret; Return (List_Cons x0 tl01) in
+            fun (ret : T) => tl01 <- back'a ret; Ok (List_Cons x0 tl01) in
           let back'b1 :=
-            fun (ret : T) => tl11 <- back'b ret; Return (List_Cons x1 tl11) in
-          Return (p, back'a1, back'b1))
+            fun (ret : T) => tl11 <- back'b ret; Ok (List_Cons x1 tl11) in
+          Ok (p, back'a1, back'b1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -417,7 +408,7 @@ Fixpoint list_nth_shared_loop_pair_loop
       match ls1 with
       | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (x0, x1)
+        then Ok (x0, x1)
         else (
           i1 <- u32_sub i 1%u32; list_nth_shared_loop_pair_loop T n1 tl0 tl1 i1)
       | List_Nil => Fail_ Failure
@@ -453,9 +444,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
         then
           let back :=
             fun (ret : (T * T)) =>
-              let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1)
-            in
-          Return ((x0, x1), back)
+              let (t, t1) := ret in Ok (List_Cons t tl0, List_Cons t1 tl1) in
+          Ok ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
@@ -464,8 +454,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
             fun (ret : (T * T)) =>
               p2 <- back ret;
               let (tl01, tl11) := p2 in
-              Return (List_Cons x0 tl01, List_Cons x1 tl11) in
-          Return (p1, back1))
+              Ok (List_Cons x0 tl01, List_Cons x1 tl11) in
+          Ok (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -496,7 +486,7 @@ Fixpoint list_nth_shared_loop_pair_merge_loop
       match ls1 with
       | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (x0, x1)
+        then Ok (x0, x1)
         else (
           i1 <- u32_sub i 1%u32;
           list_nth_shared_loop_pair_merge_loop T n1 tl0 tl1 i1)
@@ -531,15 +521,15 @@ Fixpoint list_nth_mut_shared_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back := fun (ret : T) => Return (List_Cons ret tl0) in
-          Return ((x0, x1), back)
+          let back := fun (ret : T) => Ok (List_Cons ret tl0) in
+          Ok ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1;
           let (p1, back) := p in
           let back1 :=
-            fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
-          Return (p1, back1))
+            fun (ret : T) => tl01 <- back ret; Ok (List_Cons x0 tl01) in
+          Ok (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -571,15 +561,15 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back := fun (ret : T) => Return (List_Cons ret tl0) in
-          Return ((x0, x1), back)
+          let back := fun (ret : T) => Ok (List_Cons ret tl0) in
+          Ok ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1;
           let (p1, back) := p in
           let back1 :=
-            fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
-          Return (p1, back1))
+            fun (ret : T) => tl01 <- back ret; Ok (List_Cons x0 tl01) in
+          Ok (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -611,15 +601,15 @@ Fixpoint list_nth_shared_mut_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back)
+          let back := fun (ret : T) => Ok (List_Cons ret tl1) in
+          Ok ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1;
           let (p1, back) := p in
           let back1 :=
-            fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
-          Return (p1, back1))
+            fun (ret : T) => tl11 <- back ret; Ok (List_Cons x1 tl11) in
+          Ok (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -651,15 +641,15 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back)
+          let back := fun (ret : T) => Ok (List_Cons ret tl1) in
+          Ok ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
           let (p1, back) := p in
           let back1 :=
-            fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
-          Return (p1, back1))
+            fun (ret : T) => tl11 <- back ret; Ok (List_Cons x1 tl11) in
+          Ok (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -684,7 +674,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   | S n1 =>
     if i s> 0%u32
     then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1)
-    else Return tt
+    else Ok tt
   end
 .
 
@@ -692,7 +682,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
     Source: 'src/loops.rs', lines 345:0-345:56 *)
 Definition ignore_input_mut_borrow
   (n : nat) (_a : u32) (i : u32) : result u32 :=
-  _ <- ignore_input_mut_borrow_loop n i; Return _a
+  _ <- ignore_input_mut_borrow_loop n i; Ok _a
 .
 
 (** [loops::incr_ignore_input_mut_borrow]: loop 0:
@@ -703,7 +693,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   | S n1 =>
     if i s> 0%u32
     then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1)
-    else Return tt
+    else Ok tt
   end
 .
 
@@ -711,7 +701,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
     Source: 'src/loops.rs', lines 353:0-353:60 *)
 Definition incr_ignore_input_mut_borrow
   (n : nat) (a : u32) (i : u32) : result u32 :=
-  a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Return a1
+  a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Ok a1
 .
 
 (** [loops::ignore_input_shared_borrow]: loop 0:
@@ -722,7 +712,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
   | S n1 =>
     if i s> 0%u32
     then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1)
-    else Return tt
+    else Ok tt
   end
 .
 
@@ -730,7 +720,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
     Source: 'src/loops.rs', lines 362:0-362:59 *)
 Definition ignore_input_shared_borrow
   (n : nat) (_a : u32) (i : u32) : result u32 :=
-  _ <- ignore_input_shared_borrow_loop n i; Return _a
+  _ <- ignore_input_shared_borrow_loop n i; Ok _a
 .
 
 End Loops.