diff options
Diffstat (limited to 'tests/fstar/misc/Loops.Funs.fst')
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 59 |
1 files changed, 22 insertions, 37 deletions
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 5f24fe7a..7c099da2 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -25,15 +25,15 @@ let sum (max : u32) : result u32 = (** [loops::sum_with_mut_borrows]: loop 0: 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)) + (max : u32) (i : u32) (s : u32) : + Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max i s)) = - if mi < max + if i < max then - let* ms1 = u32_add ms mi in - let* mi1 = u32_add mi 1 in - sum_with_mut_borrows_loop max mi1 ms1 - else u32_mul ms 2 + let* ms = u32_add s i in + let* mi = u32_add i 1 in + sum_with_mut_borrows_loop max mi ms + else u32_mul s 2 (** [loops::sum_with_mut_borrows]: Source: 'src/loops.rs', lines 19:0-19:44 *) @@ -140,7 +140,7 @@ let list_nth_mut_loop (t : Type0) (ls : list_t t) (i : u32) : result (t & (t -> result (list_t t))) = - let* (x, back) = list_nth_mut_loop_loop t ls i in Return (x, back) + list_nth_mut_loop_loop t ls i (** [loops::list_nth_shared_loop]: loop 0: Source: 'src/loops.rs', lines 101:0-111:1 *) @@ -185,11 +185,11 @@ let get_elem_mut (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result (usize & (usize -> result (alloc_vec_Vec (list_t usize)))) = - let* (l, index_mut_back) = + let* (ls, index_mut_back) = alloc_vec_Vec_index_mut (list_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in - let* (i, back) = get_elem_mut_loop x l in - let back1 = fun ret -> let* l1 = back ret in index_mut_back l1 in + let* (i, back) = get_elem_mut_loop x ls in + let back1 = fun ret -> let* l = back ret in index_mut_back l in Return (i, back1) (** [loops::get_elem_shared]: loop 0: @@ -207,10 +207,10 @@ let rec get_elem_shared_loop Source: 'src/loops.rs', lines 129:0-129:68 *) let get_elem_shared (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = - let* l = + let* ls = alloc_vec_Vec_index (list_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in - get_elem_shared_loop x l + get_elem_shared_loop x ls (** [loops::id_mut]: Source: 'src/loops.rs', lines 145:0-145:50 *) @@ -312,8 +312,7 @@ let list_nth_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t))) = - let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t ls0 ls1 i in - Return (p, back_'a, back_'b) + list_nth_mut_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_shared_loop_pair]: loop 0: Source: 'src/loops.rs', lines 208:0-229:1 *) @@ -376,8 +375,7 @@ let list_nth_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t)))) = - let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_mut_loop_pair_merge_loop t ls0 ls1 i (** [loops::list_nth_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 251:0-266:1 *) @@ -438,8 +436,7 @@ let list_nth_mut_shared_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_mut_shared_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 288:0-303:1 *) @@ -474,8 +471,7 @@ let list_nth_mut_shared_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'a) = list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i (** [loops::list_nth_shared_mut_loop_pair]: loop 0: Source: 'src/loops.rs', lines 307:0-322:1 *) @@ -509,8 +505,7 @@ let list_nth_shared_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t ls0 ls1 i in - Return (p, back_'b) + list_nth_shared_mut_loop_pair_loop t ls0 ls1 i (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 326:0-341:1 *) @@ -545,8 +540,7 @@ let list_nth_shared_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - let* (p, back_'a) = list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i in - Return (p, back_'a) + list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i (** [loops::ignore_input_mut_borrow]: loop 0: Source: 'src/loops.rs', lines 345:0-349:1 *) @@ -555,10 +549,7 @@ let rec ignore_input_mut_borrow_loop Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i)) = if i > 0 - then - let* i1 = u32_sub i 1 in - let* _ = ignore_input_mut_borrow_loop i1 in - Return () + then let* i1 = u32_sub i 1 in ignore_input_mut_borrow_loop i1 else Return () (** [loops::ignore_input_mut_borrow]: @@ -573,10 +564,7 @@ let rec incr_ignore_input_mut_borrow_loop Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i)) = if i > 0 - then - let* i1 = u32_sub i 1 in - let* _ = incr_ignore_input_mut_borrow_loop i1 in - Return () + then let* i1 = u32_sub i 1 in incr_ignore_input_mut_borrow_loop i1 else Return () (** [loops::incr_ignore_input_mut_borrow]: @@ -593,10 +581,7 @@ let rec ignore_input_shared_borrow_loop Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i)) = if i > 0 - then - let* i1 = u32_sub i 1 in - let* _ = ignore_input_shared_borrow_loop i1 in - Return () + then let* i1 = u32_sub i 1 in ignore_input_shared_borrow_loop i1 else Return () (** [loops::ignore_input_shared_borrow]: |