summaryrefslogtreecommitdiff
path: root/tests/fstar/misc
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/fstar/misc/External.Funs.fst4
-rw-r--r--tests/fstar/misc/Loops.Clauses.Template.fst3
-rw-r--r--tests/fstar/misc/Loops.Funs.fst59
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst7
-rw-r--r--tests/fstar/misc/Paper.fst2
5 files changed, 28 insertions, 47 deletions
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 6672b523..3ba20022 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -33,8 +33,8 @@ let custom_swap
(t : Type0) (x : t) (y : t) (st : state) :
result (state & (t & (t -> state -> result (state & (t & t)))))
=
- let* (st1, (x1, x2)) = core_mem_swap t x y st in
- let back_'a = fun ret st2 -> Return (st2, (ret, x2)) in
+ let* (st1, (x1, y1)) = core_mem_swap t x y st in
+ let back_'a = fun ret st2 -> Return (st2, (ret, y1)) in
Return (st1, (x1, back_'a))
(** [external::test_custom_swap]:
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index c8ed16f4..e43f8170 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -13,8 +13,7 @@ unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
(** [loops::sum_with_mut_borrows]: decreases clause
Source: 'src/loops.rs', lines 19:0-31:1 *)
unfold
-let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat
- =
+let sum_with_mut_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
admit ()
(** [loops::sum_with_shared_borrows]: decreases clause
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]:
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index c71f8dbb..db63eb0d 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -425,8 +425,7 @@ let id_mut_pair1
(t1 t2 : Type0) (x : t1) (y : t2) :
result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2)))
=
- let back_'a = fun ret -> let (x1, x2) = ret in Return (x1, x2) in
- Return ((x, y), back_'a)
+ Return ((x, y), Return)
(** [no_nested_borrows::id_mut_pair2]:
Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 *)
@@ -434,9 +433,7 @@ let id_mut_pair2
(t1 t2 : Type0) (p : (t1 & t2)) :
result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2)))
=
- let (x, x1) = p in
- let back_'a = fun ret -> let (x2, x3) = ret in Return (x2, x3) in
- Return ((x, x1), back_'a)
+ let (x, x1) = p in Return ((x, x1), Return)
(** [no_nested_borrows::id_mut_pair3]:
Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 *)
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index cf4dc454..ddc5e7a8 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -13,7 +13,7 @@ let ref_incr (x : i32) : result i32 =
(** [paper::test_incr]:
Source: 'src/paper.rs', lines 8:0-8:18 *)
let test_incr : result unit =
- let* i = ref_incr 0 in if not (i = 1) then Fail Failure else Return ()
+ let* x = ref_incr 0 in if not (x = 1) then Fail Failure else Return ()
(** Unit test for [paper::test_incr] *)
let _ = assert_norm (test_incr = Return ())
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 22:36:52 +0000