summaryrefslogtreecommitdiff
path: root/tests/misc
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/misc/External.Funs.fst3
-rw-r--r--tests/misc/NoNestedBorrows.fst49
-rw-r--r--tests/misc/Paper.fst14
-rw-r--r--tests/misc/Primitives.fst2
4 files changed, 34 insertions, 34 deletions
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index aafc0cf6..874b739c 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -109,8 +109,7 @@ let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
| Return (st0, _) ->
begin match swap_back u32 x 0 st with
| Fail -> Fail
- | Return (x0, _) ->
- begin match x0 with | 0 -> Fail | _ -> Return (st0, x0) end
+ | Return (x0, _) -> if x0 = 0 then Fail else Return (st0, x0)
end
end
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index 97688191..35d32514 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -56,10 +56,14 @@ let rem_test_fwd (x : u32) (y : u32) : result u32 =
(** [no_nested_borrows::cast_test] *)
let cast_test_fwd (x : u32) : result i32 =
- begin match scalar_cast I32 x with | Fail -> Fail | Return i -> Return i end
+ begin match scalar_cast U32 I32 x with
+ | Fail -> Fail
+ | Return i -> Return i
+ end
(** [no_nested_borrows::test2] *)
-let test2_fwd : result unit = Return ()
+let test2_fwd : result unit =
+ begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end
(** Unit test for [no_nested_borrows::test2] *)
let _ = assert_norm (test2_fwd = Return ())
@@ -87,7 +91,11 @@ let test3_fwd : result unit =
let _ = assert_norm (test3_fwd = Return ())
(** [no_nested_borrows::test_neg1] *)
-let test_neg1_fwd : result unit = Return ()
+let test_neg1_fwd : result unit =
+ begin match i32_neg 3 with
+ | Fail -> Fail
+ | Return y -> if not (y = -3) then Fail else Return ()
+ end
(** Unit test for [no_nested_borrows::test_neg1] *)
let _ = assert_norm (test_neg1_fwd = Return ())
@@ -222,27 +230,25 @@ and node_elem_t (t : Type0) =
(** [no_nested_borrows::even] *)
let rec even_fwd (x : u32) : result bool =
- begin match x with
- | 0 -> Return true
- | _ ->
+ if x = 0
+ then Return true
+ else
begin match u32_sub x 1 with
| Fail -> Fail
| Return i ->
begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end
end
- end
(** [no_nested_borrows::odd] *)
and odd_fwd (x : u32) : result bool =
- begin match x with
- | 0 -> Return false
- | _ ->
+ if x = 0
+ then Return false
+ else
begin match u32_sub x 1 with
| Fail -> Fail
| Return i ->
begin match even_fwd i with | Fail -> Fail | Return b -> Return b end
end
- end
(** [no_nested_borrows::test_even_odd] *)
let test_even_odd_fwd : result unit =
@@ -291,9 +297,9 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
begin match l with
| ListCons x tl ->
- begin match i with
- | 0 -> Return x
- | _ ->
+ if i = 0
+ then Return x
+ else
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
@@ -302,7 +308,6 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
| Return x0 -> Return x0
end
end
- end
| ListNil -> Fail
end
@@ -310,9 +315,9 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
begin match l with
| ListCons x tl ->
- begin match i with
- | 0 -> Return x
- | _ ->
+ if i = 0
+ then Return x
+ else
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
@@ -321,7 +326,6 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
| Return x0 -> Return x0
end
end
- end
| ListNil -> Fail
end
@@ -330,9 +334,9 @@ let rec list_nth_mut_back
(t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
begin match l with
| ListCons x tl ->
- begin match i with
- | 0 -> Return (ListCons ret tl)
- | _ ->
+ if i = 0
+ then Return (ListCons ret tl)
+ else
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
@@ -341,7 +345,6 @@ let rec list_nth_mut_back
| Return tl0 -> Return (ListCons x tl0)
end
end
- end
| ListNil -> Fail
end
diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
index d162519a..424889ef 100644
--- a/tests/misc/Paper.fst
+++ b/tests/misc/Paper.fst
@@ -59,9 +59,9 @@ type list_t (t : Type0) =
let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
begin match l with
| ListCons x tl ->
- begin match i with
- | 0 -> Return x
- | _ ->
+ if i = 0
+ then Return x
+ else
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
@@ -70,7 +70,6 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
| Return x0 -> Return x0
end
end
- end
| ListNil -> Fail
end
@@ -79,9 +78,9 @@ let rec list_nth_mut_back
(t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
begin match l with
| ListCons x tl ->
- begin match i with
- | 0 -> Return (ListCons ret tl)
- | _ ->
+ if i = 0
+ then Return (ListCons ret tl)
+ else
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
@@ -90,7 +89,6 @@ let rec list_nth_mut_back
| Return tl0 -> Return (ListCons x tl0)
end
end
- end
| ListNil -> Fail
end
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/misc/Primitives.fst
+++ b/tests/misc/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
/// The scalar types
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-26 20:24:19 +0000