4 files changed, 160 insertions, 0 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 29f312bf..22c2fd19 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -184,6 +184,79 @@ Definition list_nth_shared_loop_fwd
   list_nth_shared_loop_loop_fwd T n ls i
 .
 
+(** [loops::get_elem_mut] *)
+Fixpoint get_elem_mut_loop_fwd
+  (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_mut_loop_fwd n0 x tl
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::get_elem_mut] *)
+Definition get_elem_mut_fwd
+  (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize :=
+  l <- vec_index_mut_fwd (List_t usize) slots (0%usize);
+  get_elem_mut_loop_fwd n x l
+.
+
+(** [loops::get_elem_mut] *)
+Fixpoint get_elem_mut_loop_back
+  (n : nat) (x : usize) (ls : List_t usize) (ret : usize) :
+  result (List_t usize)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons y tl =>
+      if y s= x
+      then Return (ListCons ret tl)
+      else (l <- get_elem_mut_loop_back n0 x tl ret; Return (ListCons y l))
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::get_elem_mut] *)
+Definition get_elem_mut_back
+  (n : nat) (slots : vec (List_t usize)) (x : usize) (ret : usize) :
+  result (vec (List_t usize))
+  :=
+  l <- vec_index_mut_fwd (List_t usize) slots (0%usize);
+  l0 <- get_elem_mut_loop_back n x l ret;
+  vec_index_mut_back (List_t usize) slots (0%usize) l0
+.
+
+(** [loops::get_elem_shared] *)
+Fixpoint get_elem_shared_loop_fwd
+  (n : nat) (x : usize) (v : vec (List_t usize)) (l : List_t 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 x v l tl
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::get_elem_shared] *)
+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 x slots l l
+.
+
 (** [loops::id_mut] *)
 Definition id_mut_fwd (T : Type) (ls : List_t T) : result (List_t T) :=
   Return ls
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 98d0a8ad..3d475d20 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -36,6 +36,16 @@ let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat
   =
   admit ()
 
+(** [loops::get_elem_mut]: decreases clause *)
+unfold
+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) (v : vec (list_t usize))
+  (l : list_t usize) (ls : list_t usize) : nat =
+  admit ()
+
 (** [loops::list_nth_mut_loop_with_id]: decreases clause *)
 unfold
 let list_nth_mut_loop_with_id_decreases (t : Type0) (i : u32) (ls : list_t t) :
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index e673d4ff..57849896 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -37,6 +37,16 @@ unfold
 let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : list_t t =
   ls
 
+(** [loops::get_elem_mut]: decreases clause *)
+unfold
+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 =
+  ls
+
 (** [loops::list_nth_mut_loop_with_id]: decreases clause *)
 unfold
 let list_nth_mut_loop_with_id_decreases (t : Type0) (i : u32) (ls : list_t t) :
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index c0aca975..b7dcd045 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -172,6 +172,73 @@ let rec list_nth_shared_loop_loop_fwd
 let list_nth_shared_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
   list_nth_shared_loop_loop_fwd t ls i
 
+(** [loops::get_elem_mut] *)
+let rec get_elem_mut_loop_fwd
+  (x : usize) (ls : list_t usize) :
+  Tot (result usize) (decreases (get_elem_mut_decreases x ls))
+  =
+  begin match ls with
+  | ListCons y tl -> if y = x then Return y else get_elem_mut_loop_fwd x tl
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::get_elem_mut] *)
+let get_elem_mut_fwd (slots : vec (list_t usize)) (x : usize) : result usize =
+  begin match vec_index_mut_fwd (list_t usize) slots 0 with
+  | Fail e -> Fail e
+  | Return l -> get_elem_mut_loop_fwd x l
+  end
+
+(** [loops::get_elem_mut] *)
+let rec get_elem_mut_loop_back
+  (x : usize) (ls : list_t usize) (ret : usize) :
+  Tot (result (list_t usize)) (decreases (get_elem_mut_decreases x ls))
+  =
+  begin match ls with
+  | ListCons y tl ->
+    if y = x
+    then Return (ListCons ret tl)
+    else
+      begin match get_elem_mut_loop_back x tl ret with
+      | Fail e -> Fail e
+      | Return l -> Return (ListCons y l)
+      end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::get_elem_mut] *)
+let get_elem_mut_back
+  (slots : vec (list_t usize)) (x : usize) (ret : usize) :
+  result (vec (list_t usize))
+  =
+  begin match vec_index_mut_fwd (list_t usize) slots 0 with
+  | Fail e -> Fail e
+  | Return l ->
+    begin match get_elem_mut_loop_back x l ret with
+    | Fail e -> Fail e
+    | Return l0 -> vec_index_mut_back (list_t usize) slots 0 l0
+    end
+  end
+
+(** [loops::get_elem_shared] *)
+let rec get_elem_shared_loop_fwd
+  (x : usize) (v : vec (list_t usize)) (l : list_t usize) (ls : list_t usize) :
+  Tot (result usize) (decreases (get_elem_shared_decreases x v l ls))
+  =
+  begin match ls with
+  | ListCons y tl ->
+    if y = x then Return y else get_elem_shared_loop_fwd x v l tl
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::get_elem_shared] *)
+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
+  end
+
 (** [loops::id_mut] *)
 let id_mut_fwd (t : Type0) (ls : list_t t) : result (list_t t) = Return ls