From b0454e54744eeedfe2e9e4c8c1dcb592020bb615 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 17 Dec 2022 14:40:10 +0100
Subject: Improve the loops' numbering

---
 tests/coq/misc/Loops.v          | 19 +++++++++----------
 tests/fstar/misc/Loops.Funs.fst | 18 +++++++++---------
 2 files changed, 18 insertions(+), 19 deletions(-)

(limited to 'tests')

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 72c47361..8d552b5b 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -7,20 +7,19 @@ Local Open Scope Primitives_scope.
 Module Loops.
 
 (** [loops::sum] *)
-Fixpoint sum_loop0_fwd
-  (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
+Fixpoint sum_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     if i s< max
-    then (s0 <- u32_add s i; i0 <- u32_add i 1%u32; sum_loop0_fwd n0 max i0 s0)
+    then (s0 <- u32_add s i; i0 <- u32_add i 1%u32; sum_loop_fwd n0 max i0 s0)
     else u32_mul s 2%u32
   end
 .
 
 (** [loops::sum] *)
 Definition sum_fwd (n : nat) (max : u32) : result u32 :=
-  sum_loop0_fwd n max (0%u32) (0%u32)
+  sum_loop_fwd n max (0%u32) (0%u32)
 .
 
 (** [loops::List] *)
@@ -33,7 +32,7 @@ Arguments ListCons {T} _ _.
 Arguments ListNil {T}.
 
 (** [loops::list_nth_mut_loop] *)
-Fixpoint list_nth_mut_loop_loop0_fwd
+Fixpoint list_nth_mut_loop_loop_fwd
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
   match n with
   | O => Fail_ OutOfFuel
@@ -42,7 +41,7 @@ Fixpoint list_nth_mut_loop_loop0_fwd
     | ListCons x tl =>
       if i s= 0%u32
       then Return x
-      else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop0_fwd T n0 tl i0)
+      else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop_fwd T n0 tl i0)
     | ListNil => Fail_ Failure
     end
   end
@@ -51,11 +50,11 @@ Fixpoint list_nth_mut_loop_loop0_fwd
 (** [loops::list_nth_mut_loop] *)
 Definition list_nth_mut_loop_fwd
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  list_nth_mut_loop_loop0_fwd T n ls i
+  list_nth_mut_loop_loop_fwd T n ls i
 .
 
 (** [loops::list_nth_mut_loop] *)
-Fixpoint list_nth_mut_loop_loop0_back
+Fixpoint list_nth_mut_loop_loop_back
   (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
@@ -68,7 +67,7 @@ Fixpoint list_nth_mut_loop_loop0_back
       then Return (ListCons ret tl)
       else (
         i0 <- u32_sub i 1%u32;
-        l <- list_nth_mut_loop_loop0_back T n0 tl i0 ret;
+        l <- list_nth_mut_loop_loop_back T n0 tl i0 ret;
         Return (ListCons x l))
     | ListNil => Fail_ Failure
     end
@@ -80,7 +79,7 @@ Definition list_nth_mut_loop_back
   (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
-  list_nth_mut_loop_loop0_back T n ls i ret
+  list_nth_mut_loop_loop_back T n ls i ret
 .
 
 End Loops .
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index a2ae2563..cf05b7f2 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -8,7 +8,7 @@ include Loops.Clauses
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [loops::sum] *)
-let rec sum_loop0_fwd
+let rec sum_loop_fwd
   (max : u32) (i : u32) (s : u32) :
   Tot (result u32) (decreases (sum_decreases max i s))
   =
@@ -19,16 +19,16 @@ let rec sum_loop0_fwd
     | Return s0 ->
       begin match u32_add i 1 with
       | Fail e -> Fail e
-      | Return i0 -> sum_loop0_fwd max i0 s0
+      | Return i0 -> sum_loop_fwd max i0 s0
       end
     end
   else u32_mul s 2
 
 (** [loops::sum] *)
-let sum_fwd (max : u32) : result u32 = sum_loop0_fwd max 0 0
+let sum_fwd (max : u32) : result u32 = sum_loop_fwd max 0 0
 
 (** [loops::list_nth_mut_loop] *)
-let rec list_nth_mut_loop_loop0_fwd
+let rec list_nth_mut_loop_loop_fwd
   (t : Type0) (ls : list_t t) (i : u32) :
   Tot (result t) (decreases (list_nth_mut_loop_decreases t ls i))
   =
@@ -39,17 +39,17 @@ let rec list_nth_mut_loop_loop0_fwd
     else
       begin match u32_sub i 1 with
       | Fail e -> Fail e
-      | Return i0 -> list_nth_mut_loop_loop0_fwd t tl i0
+      | Return i0 -> list_nth_mut_loop_loop_fwd t tl i0
       end
   | ListNil -> Fail Failure
   end
 
 (** [loops::list_nth_mut_loop] *)
 let list_nth_mut_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
-  list_nth_mut_loop_loop0_fwd t ls i
+  list_nth_mut_loop_loop_fwd t ls i
 
 (** [loops::list_nth_mut_loop] *)
-let rec list_nth_mut_loop_loop0_back
+let rec list_nth_mut_loop_loop_back
   (t : Type0) (ls : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t)) (decreases (list_nth_mut_loop_decreases t ls i))
   =
@@ -61,7 +61,7 @@ let rec list_nth_mut_loop_loop0_back
       begin match u32_sub i 1 with
       | Fail e -> Fail e
       | Return i0 ->
-        begin match list_nth_mut_loop_loop0_back t tl i0 ret with
+        begin match list_nth_mut_loop_loop_back t tl i0 ret with
         | Fail e -> Fail e
         | Return l -> Return (ListCons x l)
         end
@@ -72,5 +72,5 @@ let rec list_nth_mut_loop_loop0_back
 (** [loops::list_nth_mut_loop] *)
 let list_nth_mut_loop_back
   (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
-  list_nth_mut_loop_loop0_back t ls i ret
+  list_nth_mut_loop_loop_back t ls i ret
 
-- 
cgit v1.2.3