From 4f824528f5e0c0f898b20917c6c06821efb934da Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 27 Oct 2023 12:12:18 +0200 Subject: Regenerate some of the F* test files --- tests/fstar/misc/Loops.Funs.fst | 392 ++++++++++++++++++++-------------------- 1 file changed, 201 insertions(+), 191 deletions(-) (limited to 'tests/fstar/misc/Loops.Funs.fst') diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 9a80f415..0f755351 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -8,20 +8,20 @@ include Loops.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [loops::sum]: loop 0: forward function *) -let rec sum_loop_fwd +let rec sum_loop (max : u32) (i : u32) (s : u32) : Tot (result u32) (decreases (sum_loop_decreases max i s)) = if i < max - then let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop_fwd max i0 s0 + then let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop max i0 s0 else u32_mul s 2 (** [loops::sum]: forward function *) -let sum_fwd (max : u32) : result u32 = - sum_loop_fwd max 0 0 +let sum (max : u32) : result u32 = + sum_loop max 0 0 (** [loops::sum_with_mut_borrows]: loop 0: forward function *) -let rec sum_with_mut_borrows_loop_fwd +let rec sum_with_mut_borrows_loop (max : u32) (mi : u32) (ms : u32) : Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms)) = @@ -29,15 +29,15 @@ let rec sum_with_mut_borrows_loop_fwd then let* ms0 = u32_add ms mi in let* mi0 = u32_add mi 1 in - sum_with_mut_borrows_loop_fwd max mi0 ms0 + sum_with_mut_borrows_loop max mi0 ms0 else u32_mul ms 2 (** [loops::sum_with_mut_borrows]: forward function *) -let sum_with_mut_borrows_fwd (max : u32) : result u32 = - sum_with_mut_borrows_loop_fwd max 0 0 +let sum_with_mut_borrows (max : u32) : result u32 = + sum_with_mut_borrows_loop max 0 0 (** [loops::sum_with_shared_borrows]: loop 0: forward function *) -let rec sum_with_shared_borrows_loop_fwd +let rec sum_with_shared_borrows_loop (max : u32) (i : u32) (s : u32) : Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s)) = @@ -45,62 +45,64 @@ let rec sum_with_shared_borrows_loop_fwd then let* i0 = u32_add i 1 in let* s0 = u32_add s i0 in - sum_with_shared_borrows_loop_fwd max i0 s0 + sum_with_shared_borrows_loop max i0 s0 else u32_mul s 2 (** [loops::sum_with_shared_borrows]: forward function *) -let sum_with_shared_borrows_fwd (max : u32) : result u32 = - sum_with_shared_borrows_loop_fwd max 0 0 +let sum_with_shared_borrows (max : u32) : result u32 = + sum_with_shared_borrows_loop max 0 0 (** [loops::clear]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) -let rec clear_loop_fwd_back - (v : vec u32) (i : usize) : - Tot (result (vec u32)) (decreases (clear_loop_decreases v i)) +let rec clear_loop + (v : alloc_vec_Vec u32) (i : usize) : + Tot (result (alloc_vec_Vec u32)) (decreases (clear_loop_decreases v i)) = - let i0 = vec_len u32 v in + let i0 = alloc_vec_Vec_len u32 v in if i < i0 then let* i1 = usize_add i 1 in - let* v0 = vec_index_mut_back u32 v i 0 in - clear_loop_fwd_back v0 i1 + let* v0 = + alloc_vec_Vec_index_mut_back u32 usize + (core_slice_index_usize_coresliceindexSliceIndexInst u32) v i 0 in + clear_loop v0 i1 else Return v (** [loops::clear]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) -let clear_fwd_back (v : vec u32) : result (vec u32) = - clear_loop_fwd_back v 0 +let clear (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) = + clear_loop v 0 (** [loops::list_mem]: loop 0: forward function *) -let rec list_mem_loop_fwd +let rec list_mem_loop (x : u32) (ls : list_t u32) : Tot (result bool) (decreases (list_mem_loop_decreases x ls)) = begin match ls with - | ListCons y tl -> if y = x then Return true else list_mem_loop_fwd x tl - | ListNil -> Return false + | List_Cons y tl -> if y = x then Return true else list_mem_loop x tl + | List_Nil -> Return false end (** [loops::list_mem]: forward function *) -let list_mem_fwd (x : u32) (ls : list_t u32) : result bool = - list_mem_loop_fwd x ls +let list_mem (x : u32) (ls : list_t u32) : result bool = + list_mem_loop x ls (** [loops::list_nth_mut_loop]: loop 0: forward function *) -let rec list_nth_mut_loop_loop_fwd +let rec list_nth_mut_loop_loop (t : Type0) (ls : list_t t) (i : u32) : Tot (result t) (decreases (list_nth_mut_loop_loop_decreases t ls i)) = begin match ls with - | ListCons x tl -> + | List_Cons x tl -> if i = 0 then Return x - else let* i0 = u32_sub i 1 in list_nth_mut_loop_loop_fwd t tl i0 - | ListNil -> Fail Failure + else let* i0 = u32_sub i 1 in list_nth_mut_loop_loop t tl i0 + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_loop]: forward function *) -let list_nth_mut_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t = - list_nth_mut_loop_loop_fwd t ls i +let list_nth_mut_loop (t : Type0) (ls : list_t t) (i : u32) : result t = + list_nth_mut_loop_loop t ls i (** [loops::list_nth_mut_loop]: loop 0: backward function 0 *) let rec list_nth_mut_loop_loop_back @@ -108,14 +110,14 @@ let rec list_nth_mut_loop_loop_back Tot (result (list_t t)) (decreases (list_nth_mut_loop_loop_decreases t ls i)) = begin match ls with - | ListCons x tl -> + | List_Cons x tl -> if i = 0 - then Return (ListCons ret tl) + then Return (List_Cons ret tl) else let* i0 = u32_sub i 1 in let* tl0 = list_nth_mut_loop_loop_back t tl i0 ret in - Return (ListCons x tl0) - | ListNil -> Fail Failure + Return (List_Cons x tl0) + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_loop]: backward function 0 *) @@ -124,36 +126,40 @@ let list_nth_mut_loop_back list_nth_mut_loop_loop_back t ls i ret (** [loops::list_nth_shared_loop]: loop 0: forward function *) -let rec list_nth_shared_loop_loop_fwd +let rec list_nth_shared_loop_loop (t : Type0) (ls : list_t t) (i : u32) : Tot (result t) (decreases (list_nth_shared_loop_loop_decreases t ls i)) = begin match ls with - | ListCons x tl -> + | List_Cons x tl -> if i = 0 then Return x - else let* i0 = u32_sub i 1 in list_nth_shared_loop_loop_fwd t tl i0 - | ListNil -> Fail Failure + else let* i0 = u32_sub i 1 in list_nth_shared_loop_loop t tl i0 + | List_Nil -> Fail Failure end (** [loops::list_nth_shared_loop]: forward function *) -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 +let list_nth_shared_loop (t : Type0) (ls : list_t t) (i : u32) : result t = + list_nth_shared_loop_loop t ls i (** [loops::get_elem_mut]: loop 0: forward function *) -let rec get_elem_mut_loop_fwd +let rec get_elem_mut_loop (x : usize) (ls : list_t usize) : Tot (result usize) (decreases (get_elem_mut_loop_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 + | List_Cons y tl -> if y = x then Return y else get_elem_mut_loop x tl + | List_Nil -> Fail Failure end (** [loops::get_elem_mut]: forward function *) -let get_elem_mut_fwd (slots : vec (list_t usize)) (x : usize) : result usize = - let* l = vec_index_mut_fwd (list_t usize) slots 0 in - get_elem_mut_loop_fwd x l +let get_elem_mut + (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = + let* l = + alloc_vec_Vec_index_mut (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) + slots 0 in + get_elem_mut_loop x l (** [loops::get_elem_mut]: loop 0: backward function 0 *) let rec get_elem_mut_loop_back @@ -161,39 +167,48 @@ let rec get_elem_mut_loop_back Tot (result (list_t usize)) (decreases (get_elem_mut_loop_decreases x ls)) = begin match ls with - | ListCons y tl -> + | List_Cons y tl -> if y = x - then Return (ListCons ret tl) - else let* tl0 = get_elem_mut_loop_back x tl ret in Return (ListCons y tl0) - | ListNil -> Fail Failure + then Return (List_Cons ret tl) + else let* tl0 = get_elem_mut_loop_back x tl ret in Return (List_Cons y tl0) + | List_Nil -> Fail Failure end (** [loops::get_elem_mut]: backward function 0 *) let get_elem_mut_back - (slots : vec (list_t usize)) (x : usize) (ret : usize) : - result (vec (list_t usize)) + (slots : alloc_vec_Vec (list_t usize)) (x : usize) (ret : usize) : + result (alloc_vec_Vec (list_t usize)) = - let* l = vec_index_mut_fwd (list_t usize) slots 0 in + let* l = + alloc_vec_Vec_index_mut (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) + slots 0 in let* l0 = get_elem_mut_loop_back x l ret in - vec_index_mut_back (list_t usize) slots 0 l0 + alloc_vec_Vec_index_mut_back (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) slots + 0 l0 (** [loops::get_elem_shared]: loop 0: forward function *) -let rec get_elem_shared_loop_fwd +let rec get_elem_shared_loop (x : usize) (ls : list_t usize) : Tot (result usize) (decreases (get_elem_shared_loop_decreases x ls)) = begin match ls with - | ListCons y tl -> if y = x then Return y else get_elem_shared_loop_fwd x tl - | ListNil -> Fail Failure + | List_Cons y tl -> if y = x then Return y else get_elem_shared_loop x tl + | List_Nil -> Fail Failure end (** [loops::get_elem_shared]: forward function *) -let get_elem_shared_fwd - (slots : vec (list_t usize)) (x : usize) : result usize = - let* l = vec_index_fwd (list_t usize) slots 0 in get_elem_shared_loop_fwd x l +let get_elem_shared + (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = + let* l = + alloc_vec_Vec_index (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) + slots 0 in + get_elem_shared_loop x l (** [loops::id_mut]: forward function *) -let id_mut_fwd (t : Type0) (ls : list_t t) : result (list_t t) = +let id_mut (t : Type0) (ls : list_t t) : result (list_t t) = Return ls (** [loops::id_mut]: backward function 0 *) @@ -202,26 +217,26 @@ let id_mut_back Return ret (** [loops::id_shared]: forward function *) -let id_shared_fwd (t : Type0) (ls : list_t t) : result (list_t t) = +let id_shared (t : Type0) (ls : list_t t) : result (list_t t) = Return ls (** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *) -let rec list_nth_mut_loop_with_id_loop_fwd +let rec list_nth_mut_loop_with_id_loop (t : Type0) (i : u32) (ls : list_t t) : Tot (result t) (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls)) = begin match ls with - | ListCons x tl -> + | List_Cons x tl -> if i = 0 then Return x - else let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop_fwd t i0 tl - | ListNil -> Fail Failure + else let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop t i0 tl + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_loop_with_id]: forward function *) -let list_nth_mut_loop_with_id_fwd +let list_nth_mut_loop_with_id (t : Type0) (ls : list_t t) (i : u32) : result t = - let* ls0 = id_mut_fwd t ls in list_nth_mut_loop_with_id_loop_fwd t i ls0 + let* ls0 = id_mut t ls in list_nth_mut_loop_with_id_loop t i ls0 (** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *) let rec list_nth_mut_loop_with_id_loop_back @@ -230,66 +245,64 @@ let rec list_nth_mut_loop_with_id_loop_back (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls)) = begin match ls with - | ListCons x tl -> + | List_Cons x tl -> if i = 0 - then Return (ListCons ret tl) + then Return (List_Cons ret tl) else let* i0 = u32_sub i 1 in let* tl0 = list_nth_mut_loop_with_id_loop_back t i0 tl ret in - Return (ListCons x tl0) - | ListNil -> Fail Failure + Return (List_Cons x tl0) + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_loop_with_id]: backward function 0 *) let list_nth_mut_loop_with_id_back (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = - let* ls0 = id_mut_fwd t ls in + let* ls0 = id_mut t ls in let* l = list_nth_mut_loop_with_id_loop_back t i ls0 ret in id_mut_back t ls l (** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *) -let rec list_nth_shared_loop_with_id_loop_fwd +let rec list_nth_shared_loop_with_id_loop (t : Type0) (i : u32) (ls : list_t t) : Tot (result t) (decreases (list_nth_shared_loop_with_id_loop_decreases t i ls)) = begin match ls with - | ListCons x tl -> + | List_Cons x tl -> if i = 0 then Return x - else let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop_fwd t i0 tl - | ListNil -> Fail Failure + else let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop t i0 tl + | List_Nil -> Fail Failure end (** [loops::list_nth_shared_loop_with_id]: forward function *) -let list_nth_shared_loop_with_id_fwd +let list_nth_shared_loop_with_id (t : Type0) (ls : list_t t) (i : u32) : result t = - let* ls0 = id_shared_fwd t ls in - list_nth_shared_loop_with_id_loop_fwd t i ls0 + let* ls0 = id_shared t ls in list_nth_shared_loop_with_id_loop t i ls0 (** [loops::list_nth_mut_loop_pair]: loop 0: forward function *) -let rec list_nth_mut_loop_pair_loop_fwd +let rec list_nth_mut_loop_pair_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 then Return (x0, x1) - else - let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_loop_fwd t tl0 tl1 i0 - | ListNil -> Fail Failure + else let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_loop_pair]: forward function *) -let list_nth_mut_loop_pair_fwd +let list_nth_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = - list_nth_mut_loop_pair_loop_fwd t ls0 ls1 i + list_nth_mut_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *) let rec list_nth_mut_loop_pair_loop_back'a @@ -298,18 +311,18 @@ let rec list_nth_mut_loop_pair_loop_back'a (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 - then Return (ListCons ret tl0) + then Return (List_Cons ret tl0) else let* i0 = u32_sub i 1 in let* tl00 = list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret in - Return (ListCons x0 tl00) - | ListNil -> Fail Failure + Return (List_Cons x0 tl00) + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_loop_pair]: backward function 0 *) @@ -326,18 +339,18 @@ let rec list_nth_mut_loop_pair_loop_back'b (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 - then Return (ListCons ret tl1) + then Return (List_Cons ret tl1) else let* i0 = u32_sub i 1 in let* tl10 = list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret in - Return (ListCons x1 tl10) - | ListNil -> Fail Failure + Return (List_Cons x1 tl10) + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_loop_pair]: backward function 1 *) @@ -348,54 +361,51 @@ let list_nth_mut_loop_pair_back'b list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret (** [loops::list_nth_shared_loop_pair]: loop 0: forward function *) -let rec list_nth_shared_loop_pair_loop_fwd +let rec list_nth_shared_loop_pair_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) (decreases (list_nth_shared_loop_pair_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 then Return (x0, x1) - else - let* i0 = u32_sub i 1 in - list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0 - | ListNil -> Fail Failure + else let* i0 = u32_sub i 1 in list_nth_shared_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_shared_loop_pair]: forward function *) -let list_nth_shared_loop_pair_fwd +let list_nth_shared_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = - list_nth_shared_loop_pair_loop_fwd t ls0 ls1 i + list_nth_shared_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *) -let rec list_nth_mut_loop_pair_merge_loop_fwd +let rec list_nth_mut_loop_pair_merge_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 then Return (x0, x1) else - let* i0 = u32_sub i 1 in - list_nth_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 - | ListNil -> Fail Failure + let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_loop_pair_merge]: forward function *) -let list_nth_mut_loop_pair_merge_fwd +let list_nth_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = - list_nth_mut_loop_pair_merge_loop_fwd t ls0 ls1 i + list_nth_mut_loop_pair_merge_loop t ls0 ls1 i (** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *) let rec list_nth_mut_loop_pair_merge_loop_back @@ -404,19 +414,19 @@ let rec list_nth_mut_loop_pair_merge_loop_back (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 - then let (x, x2) = ret in Return (ListCons x tl0, ListCons x2 tl1) + then let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1) else let* i0 = u32_sub i 1 in let* (tl00, tl10) = list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in - Return (ListCons x0 tl00, ListCons x1 tl10) - | ListNil -> Fail Failure + Return (List_Cons x0 tl00, List_Cons x1 tl10) + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *) @@ -427,54 +437,54 @@ let list_nth_mut_loop_pair_merge_back list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret (** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *) -let rec list_nth_shared_loop_pair_merge_loop_fwd +let rec list_nth_shared_loop_pair_merge_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) (decreases (list_nth_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 then Return (x0, x1) else let* i0 = u32_sub i 1 in - list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 - | ListNil -> Fail Failure + list_nth_shared_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_shared_loop_pair_merge]: forward function *) -let list_nth_shared_loop_pair_merge_fwd +let list_nth_shared_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = - list_nth_shared_loop_pair_merge_loop_fwd t ls0 ls1 i + list_nth_shared_loop_pair_merge_loop t ls0 ls1 i (** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *) -let rec list_nth_mut_shared_loop_pair_loop_fwd +let rec list_nth_mut_shared_loop_pair_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 then Return (x0, x1) else let* i0 = u32_sub i 1 in - list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0 - | ListNil -> Fail Failure + list_nth_mut_shared_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_shared_loop_pair]: forward function *) -let list_nth_mut_shared_loop_pair_fwd +let list_nth_mut_shared_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = - list_nth_mut_shared_loop_pair_loop_fwd t ls0 ls1 i + list_nth_mut_shared_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *) let rec list_nth_mut_shared_loop_pair_loop_back @@ -483,18 +493,18 @@ let rec list_nth_mut_shared_loop_pair_loop_back (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 - then Return (ListCons ret tl0) + then Return (List_Cons ret tl0) else let* i0 = u32_sub i 1 in let* tl00 = list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret in - Return (ListCons x0 tl00) - | ListNil -> Fail Failure + Return (List_Cons x0 tl00) + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *) @@ -505,29 +515,29 @@ let list_nth_mut_shared_loop_pair_back list_nth_mut_shared_loop_pair_loop_back t ls0 ls1 i ret (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *) -let rec list_nth_mut_shared_loop_pair_merge_loop_fwd +let rec list_nth_mut_shared_loop_pair_merge_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 then Return (x0, x1) else let* i0 = u32_sub i 1 in - list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 - | ListNil -> Fail Failure + list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *) -let list_nth_mut_shared_loop_pair_merge_fwd +let list_nth_mut_shared_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = - list_nth_mut_shared_loop_pair_merge_loop_fwd t ls0 ls1 i + list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *) let rec list_nth_mut_shared_loop_pair_merge_loop_back @@ -536,19 +546,19 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 - then Return (ListCons ret tl0) + then Return (List_Cons ret tl0) else let* i0 = u32_sub i 1 in let* tl00 = list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret in - Return (ListCons x0 tl00) - | ListNil -> Fail Failure + Return (List_Cons x0 tl00) + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *) @@ -559,29 +569,29 @@ let list_nth_mut_shared_loop_pair_merge_back list_nth_mut_shared_loop_pair_merge_loop_back t ls0 ls1 i ret (** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *) -let rec list_nth_shared_mut_loop_pair_loop_fwd +let rec list_nth_shared_mut_loop_pair_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 then Return (x0, x1) else let* i0 = u32_sub i 1 in - list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0 - | ListNil -> Fail Failure + list_nth_shared_mut_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_shared_mut_loop_pair]: forward function *) -let list_nth_shared_mut_loop_pair_fwd +let list_nth_shared_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = - list_nth_shared_mut_loop_pair_loop_fwd t ls0 ls1 i + list_nth_shared_mut_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *) let rec list_nth_shared_mut_loop_pair_loop_back @@ -590,18 +600,18 @@ let rec list_nth_shared_mut_loop_pair_loop_back (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 - then Return (ListCons ret tl1) + then Return (List_Cons ret tl1) else let* i0 = u32_sub i 1 in let* tl10 = list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret in - Return (ListCons x1 tl10) - | ListNil -> Fail Failure + Return (List_Cons x1 tl10) + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *) @@ -612,29 +622,29 @@ let list_nth_shared_mut_loop_pair_back list_nth_shared_mut_loop_pair_loop_back t ls0 ls1 i ret (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *) -let rec list_nth_shared_mut_loop_pair_merge_loop_fwd +let rec list_nth_shared_mut_loop_pair_merge_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 then Return (x0, x1) else let* i0 = u32_sub i 1 in - list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 - | ListNil -> Fail Failure + list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *) -let list_nth_shared_mut_loop_pair_merge_fwd +let list_nth_shared_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = - list_nth_shared_mut_loop_pair_merge_loop_fwd t ls0 ls1 i + list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *) let rec list_nth_shared_mut_loop_pair_merge_loop_back @@ -643,19 +653,19 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) = begin match ls0 with - | ListCons x0 tl0 -> + | List_Cons x0 tl0 -> begin match ls1 with - | ListCons x1 tl1 -> + | List_Cons x1 tl1 -> if i = 0 - then Return (ListCons ret tl1) + then Return (List_Cons ret tl1) else let* i0 = u32_sub i 1 in let* tl10 = list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in - Return (ListCons x1 tl10) - | ListNil -> Fail Failure + Return (List_Cons x1 tl10) + | List_Nil -> Fail Failure end - | ListNil -> Fail Failure + | List_Nil -> Fail Failure end (** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *) -- cgit v1.2.3 From 5e92ae6b361f9221f5c5f9a39ab4c28a36597a77 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 11:40:59 +0100 Subject: Regenerate most of the test files --- tests/fstar/misc/Loops.Funs.fst | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) (limited to 'tests/fstar/misc/Loops.Funs.fst') diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 0f755351..4dd3a5dd 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -64,7 +64,7 @@ let rec clear_loop let* i1 = usize_add i 1 in let* v0 = alloc_vec_Vec_index_mut_back u32 usize - (core_slice_index_usize_coresliceindexSliceIndexInst u32) v i 0 in + (core_slice_index_SliceIndexUsizeSliceTInst u32) v i 0 in clear_loop v0 i1 else Return v @@ -157,8 +157,7 @@ let get_elem_mut (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = let* l = alloc_vec_Vec_index_mut (list_t usize) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) - slots 0 in + (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in get_elem_mut_loop x l (** [loops::get_elem_mut]: loop 0: backward function 0 *) @@ -181,12 +180,10 @@ let get_elem_mut_back = let* l = alloc_vec_Vec_index_mut (list_t usize) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) - slots 0 in + (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in let* l0 = get_elem_mut_loop_back x l ret in alloc_vec_Vec_index_mut_back (list_t usize) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) slots - 0 l0 + (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 l0 (** [loops::get_elem_shared]: loop 0: forward function *) let rec get_elem_shared_loop @@ -203,8 +200,7 @@ let get_elem_shared (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = let* l = alloc_vec_Vec_index (list_t usize) usize - (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) - slots 0 in + (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in get_elem_shared_loop x l (** [loops::id_mut]: forward function *) -- cgit v1.2.3 From 137cc7335e64fcb70c254e7fd2a6fa353fb43e61 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 14:57:38 +0100 Subject: Regenerate the files --- tests/fstar/misc/Loops.Funs.fst | 183 ++++++++++++++++++++++++++-------------- 1 file changed, 122 insertions(+), 61 deletions(-) (limited to 'tests/fstar/misc/Loops.Funs.fst') diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 4dd3a5dd..d2ac5561 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -7,7 +7,8 @@ include Loops.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [loops::sum]: loop 0: forward function *) +(** [loops::sum]: loop 0: forward function + Source: 'src/loops.rs', lines 4:0-14:1 *) let rec sum_loop (max : u32) (i : u32) (s : u32) : Tot (result u32) (decreases (sum_loop_decreases max i s)) @@ -16,11 +17,13 @@ let rec sum_loop then let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop max i0 s0 else u32_mul s 2 -(** [loops::sum]: forward function *) +(** [loops::sum]: forward function + Source: 'src/loops.rs', lines 4:0-4:27 *) let sum (max : u32) : result u32 = sum_loop max 0 0 -(** [loops::sum_with_mut_borrows]: loop 0: forward function *) +(** [loops::sum_with_mut_borrows]: loop 0: forward function + Source: 'src/loops.rs', lines 19:0-31:1 *) let rec sum_with_mut_borrows_loop (max : u32) (mi : u32) (ms : u32) : Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms)) @@ -32,11 +35,13 @@ let rec sum_with_mut_borrows_loop sum_with_mut_borrows_loop max mi0 ms0 else u32_mul ms 2 -(** [loops::sum_with_mut_borrows]: forward function *) +(** [loops::sum_with_mut_borrows]: forward function + Source: 'src/loops.rs', lines 19:0-19:44 *) let sum_with_mut_borrows (max : u32) : result u32 = sum_with_mut_borrows_loop max 0 0 -(** [loops::sum_with_shared_borrows]: loop 0: forward function *) +(** [loops::sum_with_shared_borrows]: loop 0: forward function + Source: 'src/loops.rs', lines 34:0-48:1 *) let rec sum_with_shared_borrows_loop (max : u32) (i : u32) (s : u32) : Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s)) @@ -48,12 +53,14 @@ let rec sum_with_shared_borrows_loop sum_with_shared_borrows_loop max i0 s0 else u32_mul s 2 -(** [loops::sum_with_shared_borrows]: forward function *) +(** [loops::sum_with_shared_borrows]: forward function + Source: 'src/loops.rs', lines 34:0-34:47 *) let sum_with_shared_borrows (max : u32) : result u32 = sum_with_shared_borrows_loop max 0 0 (** [loops::clear]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/loops.rs', lines 52:0-58:1 *) let rec clear_loop (v : alloc_vec_Vec u32) (i : usize) : Tot (result (alloc_vec_Vec u32)) (decreases (clear_loop_decreases v i)) @@ -69,11 +76,13 @@ let rec clear_loop else Return v (** [loops::clear]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/loops.rs', lines 52:0-52:30 *) let clear (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) = clear_loop v 0 -(** [loops::list_mem]: loop 0: forward function *) +(** [loops::list_mem]: loop 0: forward function + Source: 'src/loops.rs', lines 66:0-75:1 *) let rec list_mem_loop (x : u32) (ls : list_t u32) : Tot (result bool) (decreases (list_mem_loop_decreases x ls)) @@ -83,11 +92,13 @@ let rec list_mem_loop | List_Nil -> Return false end -(** [loops::list_mem]: forward function *) +(** [loops::list_mem]: forward function + Source: 'src/loops.rs', lines 66:0-66:52 *) let list_mem (x : u32) (ls : list_t u32) : result bool = list_mem_loop x ls -(** [loops::list_nth_mut_loop]: loop 0: forward function *) +(** [loops::list_nth_mut_loop]: loop 0: forward function + Source: 'src/loops.rs', lines 78:0-88:1 *) let rec list_nth_mut_loop_loop (t : Type0) (ls : list_t t) (i : u32) : Tot (result t) (decreases (list_nth_mut_loop_loop_decreases t ls i)) @@ -100,11 +111,13 @@ let rec list_nth_mut_loop_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_loop]: forward function *) +(** [loops::list_nth_mut_loop]: forward function + Source: 'src/loops.rs', lines 78:0-78:71 *) let list_nth_mut_loop (t : Type0) (ls : list_t t) (i : u32) : result t = list_nth_mut_loop_loop t ls i -(** [loops::list_nth_mut_loop]: loop 0: backward function 0 *) +(** [loops::list_nth_mut_loop]: loop 0: backward function 0 + Source: 'src/loops.rs', lines 78:0-88:1 *) 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_loop_decreases t ls i)) @@ -120,12 +133,14 @@ let rec list_nth_mut_loop_loop_back | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_loop]: backward function 0 *) +(** [loops::list_nth_mut_loop]: backward function 0 + Source: 'src/loops.rs', lines 78:0-78:71 *) let list_nth_mut_loop_back (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = list_nth_mut_loop_loop_back t ls i ret -(** [loops::list_nth_shared_loop]: loop 0: forward function *) +(** [loops::list_nth_shared_loop]: loop 0: forward function + Source: 'src/loops.rs', lines 91:0-101:1 *) let rec list_nth_shared_loop_loop (t : Type0) (ls : list_t t) (i : u32) : Tot (result t) (decreases (list_nth_shared_loop_loop_decreases t ls i)) @@ -138,11 +153,13 @@ let rec list_nth_shared_loop_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_shared_loop]: forward function *) +(** [loops::list_nth_shared_loop]: forward function + Source: 'src/loops.rs', lines 91:0-91:66 *) let list_nth_shared_loop (t : Type0) (ls : list_t t) (i : u32) : result t = list_nth_shared_loop_loop t ls i -(** [loops::get_elem_mut]: loop 0: forward function *) +(** [loops::get_elem_mut]: loop 0: forward function + Source: 'src/loops.rs', lines 103:0-117:1 *) let rec get_elem_mut_loop (x : usize) (ls : list_t usize) : Tot (result usize) (decreases (get_elem_mut_loop_decreases x ls)) @@ -152,7 +169,8 @@ let rec get_elem_mut_loop | List_Nil -> Fail Failure end -(** [loops::get_elem_mut]: forward function *) +(** [loops::get_elem_mut]: forward function + Source: 'src/loops.rs', lines 103:0-103:73 *) let get_elem_mut (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = let* l = @@ -160,7 +178,8 @@ let get_elem_mut (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in get_elem_mut_loop x l -(** [loops::get_elem_mut]: loop 0: backward function 0 *) +(** [loops::get_elem_mut]: loop 0: backward function 0 + Source: 'src/loops.rs', lines 103:0-117:1 *) let rec get_elem_mut_loop_back (x : usize) (ls : list_t usize) (ret : usize) : Tot (result (list_t usize)) (decreases (get_elem_mut_loop_decreases x ls)) @@ -173,7 +192,8 @@ let rec get_elem_mut_loop_back | List_Nil -> Fail Failure end -(** [loops::get_elem_mut]: backward function 0 *) +(** [loops::get_elem_mut]: backward function 0 + Source: 'src/loops.rs', lines 103:0-103:73 *) let get_elem_mut_back (slots : alloc_vec_Vec (list_t usize)) (x : usize) (ret : usize) : result (alloc_vec_Vec (list_t usize)) @@ -185,7 +205,8 @@ let get_elem_mut_back alloc_vec_Vec_index_mut_back (list_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 l0 -(** [loops::get_elem_shared]: loop 0: forward function *) +(** [loops::get_elem_shared]: loop 0: forward function + Source: 'src/loops.rs', lines 119:0-133:1 *) let rec get_elem_shared_loop (x : usize) (ls : list_t usize) : Tot (result usize) (decreases (get_elem_shared_loop_decreases x ls)) @@ -195,7 +216,8 @@ let rec get_elem_shared_loop | List_Nil -> Fail Failure end -(** [loops::get_elem_shared]: forward function *) +(** [loops::get_elem_shared]: forward function + Source: 'src/loops.rs', lines 119:0-119:68 *) let get_elem_shared (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = let* l = @@ -203,20 +225,24 @@ let get_elem_shared (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in get_elem_shared_loop x l -(** [loops::id_mut]: forward function *) +(** [loops::id_mut]: forward function + Source: 'src/loops.rs', lines 135:0-135:50 *) let id_mut (t : Type0) (ls : list_t t) : result (list_t t) = Return ls -(** [loops::id_mut]: backward function 0 *) +(** [loops::id_mut]: backward function 0 + Source: 'src/loops.rs', lines 135:0-135:50 *) let id_mut_back (t : Type0) (ls : list_t t) (ret : list_t t) : result (list_t t) = Return ret -(** [loops::id_shared]: forward function *) +(** [loops::id_shared]: forward function + Source: 'src/loops.rs', lines 139:0-139:45 *) let id_shared (t : Type0) (ls : list_t t) : result (list_t t) = Return ls -(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *) +(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function + Source: 'src/loops.rs', lines 144:0-155:1 *) let rec list_nth_mut_loop_with_id_loop (t : Type0) (i : u32) (ls : list_t t) : Tot (result t) (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls)) @@ -229,12 +255,14 @@ let rec list_nth_mut_loop_with_id_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_loop_with_id]: forward function *) +(** [loops::list_nth_mut_loop_with_id]: forward function + Source: 'src/loops.rs', lines 144:0-144:75 *) let list_nth_mut_loop_with_id (t : Type0) (ls : list_t t) (i : u32) : result t = let* ls0 = id_mut t ls in list_nth_mut_loop_with_id_loop t i ls0 -(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *) +(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 + Source: 'src/loops.rs', lines 144:0-155:1 *) let rec list_nth_mut_loop_with_id_loop_back (t : Type0) (i : u32) (ls : list_t t) (ret : t) : Tot (result (list_t t)) @@ -251,14 +279,16 @@ let rec list_nth_mut_loop_with_id_loop_back | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_loop_with_id]: backward function 0 *) +(** [loops::list_nth_mut_loop_with_id]: backward function 0 + Source: 'src/loops.rs', lines 144:0-144:75 *) let list_nth_mut_loop_with_id_back (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = let* ls0 = id_mut t ls in let* l = list_nth_mut_loop_with_id_loop_back t i ls0 ret in id_mut_back t ls l -(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *) +(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function + Source: 'src/loops.rs', lines 158:0-169:1 *) let rec list_nth_shared_loop_with_id_loop (t : Type0) (i : u32) (ls : list_t t) : Tot (result t) @@ -272,12 +302,14 @@ let rec list_nth_shared_loop_with_id_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_shared_loop_with_id]: forward function *) +(** [loops::list_nth_shared_loop_with_id]: forward function + Source: 'src/loops.rs', lines 158:0-158:70 *) let list_nth_shared_loop_with_id (t : Type0) (ls : list_t t) (i : u32) : result t = let* ls0 = id_shared t ls in list_nth_shared_loop_with_id_loop t i ls0 -(** [loops::list_nth_mut_loop_pair]: loop 0: forward function *) +(** [loops::list_nth_mut_loop_pair]: loop 0: forward function + Source: 'src/loops.rs', lines 174:0-195:1 *) let rec list_nth_mut_loop_pair_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) @@ -295,12 +327,14 @@ let rec list_nth_mut_loop_pair_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_loop_pair]: forward function *) +(** [loops::list_nth_mut_loop_pair]: forward function + Source: 'src/loops.rs', lines 174:0-178:27 *) let list_nth_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = list_nth_mut_loop_pair_loop t ls0 ls1 i -(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *) +(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 + Source: 'src/loops.rs', lines 174:0-195:1 *) let rec list_nth_mut_loop_pair_loop_back'a (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) @@ -321,14 +355,16 @@ let rec list_nth_mut_loop_pair_loop_back'a | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_loop_pair]: backward function 0 *) +(** [loops::list_nth_mut_loop_pair]: backward function 0 + Source: 'src/loops.rs', lines 174:0-178:27 *) let list_nth_mut_loop_pair_back'a (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : result (list_t t) = list_nth_mut_loop_pair_loop_back'a t ls0 ls1 i ret -(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 *) +(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 + Source: 'src/loops.rs', lines 174:0-195:1 *) let rec list_nth_mut_loop_pair_loop_back'b (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) @@ -349,14 +385,16 @@ let rec list_nth_mut_loop_pair_loop_back'b | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_loop_pair]: backward function 1 *) +(** [loops::list_nth_mut_loop_pair]: backward function 1 + Source: 'src/loops.rs', lines 174:0-178:27 *) let list_nth_mut_loop_pair_back'b (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : result (list_t t) = list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret -(** [loops::list_nth_shared_loop_pair]: loop 0: forward function *) +(** [loops::list_nth_shared_loop_pair]: loop 0: forward function + Source: 'src/loops.rs', lines 198:0-219:1 *) let rec list_nth_shared_loop_pair_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) @@ -374,12 +412,14 @@ let rec list_nth_shared_loop_pair_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_shared_loop_pair]: forward function *) +(** [loops::list_nth_shared_loop_pair]: forward function + Source: 'src/loops.rs', lines 198:0-202:19 *) let list_nth_shared_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = list_nth_shared_loop_pair_loop t ls0 ls1 i -(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *) +(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function + Source: 'src/loops.rs', lines 223:0-238:1 *) let rec list_nth_mut_loop_pair_merge_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) @@ -398,12 +438,14 @@ let rec list_nth_mut_loop_pair_merge_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_loop_pair_merge]: forward function *) +(** [loops::list_nth_mut_loop_pair_merge]: forward function + Source: 'src/loops.rs', lines 223:0-227:27 *) let list_nth_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = list_nth_mut_loop_pair_merge_loop t ls0 ls1 i -(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *) +(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 + Source: 'src/loops.rs', lines 223:0-238:1 *) let rec list_nth_mut_loop_pair_merge_loop_back (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) : Tot (result ((list_t t) & (list_t t))) @@ -425,14 +467,16 @@ let rec list_nth_mut_loop_pair_merge_loop_back | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *) +(** [loops::list_nth_mut_loop_pair_merge]: backward function 0 + Source: 'src/loops.rs', lines 223:0-227:27 *) let list_nth_mut_loop_pair_merge_back (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) : result ((list_t t) & (list_t t)) = list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret -(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *) +(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function + Source: 'src/loops.rs', lines 241:0-256:1 *) let rec list_nth_shared_loop_pair_merge_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) @@ -452,12 +496,14 @@ let rec list_nth_shared_loop_pair_merge_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_shared_loop_pair_merge]: forward function *) +(** [loops::list_nth_shared_loop_pair_merge]: forward function + Source: 'src/loops.rs', lines 241:0-245:19 *) let list_nth_shared_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = list_nth_shared_loop_pair_merge_loop t ls0 ls1 i -(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *) +(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function + Source: 'src/loops.rs', lines 259:0-274:1 *) let rec list_nth_mut_shared_loop_pair_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) @@ -477,12 +523,14 @@ let rec list_nth_mut_shared_loop_pair_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_shared_loop_pair]: forward function *) +(** [loops::list_nth_mut_shared_loop_pair]: forward function + Source: 'src/loops.rs', lines 259:0-263:23 *) let list_nth_mut_shared_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = list_nth_mut_shared_loop_pair_loop t ls0 ls1 i -(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *) +(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 + Source: 'src/loops.rs', lines 259:0-274:1 *) let rec list_nth_mut_shared_loop_pair_loop_back (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) @@ -503,14 +551,16 @@ let rec list_nth_mut_shared_loop_pair_loop_back | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *) +(** [loops::list_nth_mut_shared_loop_pair]: backward function 0 + Source: 'src/loops.rs', lines 259:0-263:23 *) let list_nth_mut_shared_loop_pair_back (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : result (list_t t) = list_nth_mut_shared_loop_pair_loop_back t ls0 ls1 i ret -(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *) +(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function + Source: 'src/loops.rs', lines 278:0-293:1 *) let rec list_nth_mut_shared_loop_pair_merge_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) @@ -530,12 +580,14 @@ let rec list_nth_mut_shared_loop_pair_merge_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *) +(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function + Source: 'src/loops.rs', lines 278:0-282:23 *) let list_nth_mut_shared_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i -(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *) +(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 + Source: 'src/loops.rs', lines 278:0-293:1 *) let rec list_nth_mut_shared_loop_pair_merge_loop_back (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) @@ -557,14 +609,16 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back | List_Nil -> Fail Failure end -(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *) +(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 + Source: 'src/loops.rs', lines 278:0-282:23 *) let list_nth_mut_shared_loop_pair_merge_back (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : result (list_t t) = list_nth_mut_shared_loop_pair_merge_loop_back t ls0 ls1 i ret -(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *) +(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function + Source: 'src/loops.rs', lines 297:0-312:1 *) let rec list_nth_shared_mut_loop_pair_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) @@ -584,12 +638,14 @@ let rec list_nth_shared_mut_loop_pair_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_shared_mut_loop_pair]: forward function *) +(** [loops::list_nth_shared_mut_loop_pair]: forward function + Source: 'src/loops.rs', lines 297:0-301:23 *) let list_nth_shared_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = list_nth_shared_mut_loop_pair_loop t ls0 ls1 i -(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *) +(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 + Source: 'src/loops.rs', lines 297:0-312:1 *) let rec list_nth_shared_mut_loop_pair_loop_back (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) @@ -610,14 +666,16 @@ let rec list_nth_shared_mut_loop_pair_loop_back | List_Nil -> Fail Failure end -(** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *) +(** [loops::list_nth_shared_mut_loop_pair]: backward function 1 + Source: 'src/loops.rs', lines 297:0-301:23 *) let list_nth_shared_mut_loop_pair_back (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : result (list_t t) = list_nth_shared_mut_loop_pair_loop_back t ls0 ls1 i ret -(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *) +(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function + Source: 'src/loops.rs', lines 316:0-331:1 *) let rec list_nth_shared_mut_loop_pair_merge_loop (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) @@ -637,12 +695,14 @@ let rec list_nth_shared_mut_loop_pair_merge_loop | List_Nil -> Fail Failure end -(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *) +(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function + Source: 'src/loops.rs', lines 316:0-320:23 *) let list_nth_shared_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i -(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *) +(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 + Source: 'src/loops.rs', lines 316:0-331:1 *) let rec list_nth_shared_mut_loop_pair_merge_loop_back (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) @@ -664,7 +724,8 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back | List_Nil -> Fail Failure end -(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *) +(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 + Source: 'src/loops.rs', lines 316:0-320:23 *) let list_nth_shared_mut_loop_pair_merge_back (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : result (list_t t) -- cgit v1.2.3