From 1302f2830905dc63f294aad00d78d03486e13d73 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 8 Jan 2023 09:42:33 +0100
Subject: Implement a pass to filter the unused input arguments in the loop
 functions

---
 tests/coq/misc/Loops.v | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

(limited to 'tests/coq/misc')

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 9d416bb0..ec77e4dd 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -235,16 +235,13 @@ Definition get_elem_mut_back
 
 (** [loops::get_elem_shared] *)
 Fixpoint get_elem_shared_loop_fwd
-  (n : nat) (slots : vec (List_t usize)) (x : usize) (ls : List_t usize)
-  (ls0 : List_t usize) :
-  result usize
-  :=
+  (n : nat) (x : usize) (ls : List_t usize) : result usize :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons y tl =>
-      if y s= x then Return y else get_elem_shared_loop_fwd n0 slots x tl ls0
+      if y s= x then Return y else get_elem_shared_loop_fwd n0 x tl
     | ListNil => Fail_ Failure
     end
   end
@@ -254,7 +251,7 @@ Fixpoint get_elem_shared_loop_fwd
 Definition get_elem_shared_fwd
   (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize :=
   l <- vec_index_fwd (List_t usize) slots (0%usize);
-  get_elem_shared_loop_fwd n slots x l l
+  get_elem_shared_loop_fwd n x l
 .
 
 (** [loops::id_mut] *)
@@ -329,17 +326,16 @@ Definition list_nth_mut_loop_with_id_back
 
 (** [loops::list_nth_shared_loop_with_id] *)
 Fixpoint list_nth_shared_loop_with_id_loop_fwd
-  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ls0 : List_t T) : result T :=
+  (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match ls0 with
+    match ls with
     | ListCons x tl =>
       if i s= 0%u32
       then Return x
       else (
-        i0 <- u32_sub i 1%u32;
-        list_nth_shared_loop_with_id_loop_fwd T n0 ls i0 tl)
+        i0 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop_fwd T n0 i0 tl)
     | ListNil => Fail_ Failure
     end
   end
@@ -348,7 +344,7 @@ Fixpoint list_nth_shared_loop_with_id_loop_fwd
 (** [loops::list_nth_shared_loop_with_id] *)
 Definition list_nth_shared_loop_with_id_fwd
   (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
-  ls0 <- id_shared_fwd T ls; list_nth_shared_loop_with_id_loop_fwd T n ls i ls0
+  ls0 <- id_shared_fwd T ls; list_nth_shared_loop_with_id_loop_fwd T n i ls0
 .
 
 (** [loops::list_nth_mut_loop_pair] *)
-- 
cgit v1.2.3