From 46381652adbece2d7ccfd57fae8b5ee2365fb374 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 6 Jan 2023 16:51:27 +0100
Subject: Fix some issues with the values given back by loop backward
 translations

---
 tests/fstar/misc/Loops.Clauses.Template.fst | 10 +++++
 tests/fstar/misc/Loops.Clauses.fst          | 10 +++++
 tests/fstar/misc/Loops.Funs.fst             | 67 +++++++++++++++++++++++++++++
 3 files changed, 87 insertions(+)

(limited to 'tests/fstar/misc')

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
 
-- 
cgit v1.2.3