From af929939c44116cdfd5faa845273d0f032d761bf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 7 Jan 2023 17:21:27 +0100
Subject: Improve the order of the loop input parameters

---
 tests/fstar/misc/Loops.Clauses.Template.fst |  2 +-
 tests/fstar/misc/Loops.Clauses.fst          |  4 ++--
 tests/fstar/misc/Loops.Funs.fst             | 10 +++++-----
 3 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'tests/fstar/misc')

diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 1b141d64..8cdc6e2c 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -42,7 +42,7 @@ let get_elem_mut_decreases (x : usize) (ls : list_t usize) : nat = admit ()
 
 (** [loops::get_elem_shared]: decreases clause *)
 unfold
-let get_elem_shared_decreases (x : usize) (slots : vec (list_t usize))
+let get_elem_shared_decreases (slots : vec (list_t usize)) (x : usize)
   (ls : list_t usize) (ls0 : list_t usize) : nat =
   admit ()
 
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index 57849896..a03f0302 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -43,8 +43,8 @@ let get_elem_mut_decreases (x : usize) (ls : list_t usize) : list_t usize = ls
 
 (** [loops::get_elem_shared]: decreases clause *)
 unfold
-let get_elem_shared_decreases (x : usize) (v : vec (list_t usize))
-  (l : list_t usize) (ls : list_t usize) : list_t usize =
+let get_elem_shared_decreases (slots : vec (list_t usize)) (x : usize)
+  (ls : list_t usize) (ls0 : list_t usize) : list_t usize =
   ls
 
 (** [loops::list_nth_mut_loop_with_id]: decreases clause *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index ca918e35..e8fb89e9 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -222,13 +222,13 @@ let get_elem_mut_back
 
 (** [loops::get_elem_shared] *)
 let rec get_elem_shared_loop_fwd
-  (x : usize) (slots : vec (list_t usize)) (ls : list_t usize)
+  (slots : vec (list_t usize)) (x : usize) (ls : list_t usize)
   (ls0 : list_t usize) :
-  Tot (result usize) (decreases (get_elem_shared_decreases x slots ls ls0))
+  Tot (result usize) (decreases (get_elem_shared_decreases slots x ls ls0))
   =
-  begin match ls0 with
+  begin match ls with
   | ListCons y tl ->
-    if y = x then Return y else get_elem_shared_loop_fwd x slots ls tl
+    if y = x then Return y else get_elem_shared_loop_fwd slots x tl ls0
   | ListNil -> Fail Failure
   end
 
@@ -237,7 +237,7 @@ let get_elem_shared_fwd
   (slots : vec (list_t usize)) (x : usize) : result usize =
   begin match vec_index_fwd (list_t usize) slots 0 with
   | Fail e -> Fail e
-  | Return l -> get_elem_shared_loop_fwd x slots l l
+  | Return l -> get_elem_shared_loop_fwd slots x l l
   end
 
 (** [loops::id_mut] *)
-- 
cgit v1.2.3