summaryrefslogtreecommitdiff
path: root/tests/fstar/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/misc')
-rw-r--r--tests/fstar/misc/Constants.fst48
-rw-r--r--tests/fstar/misc/External.Funs.fst12
-rw-r--r--tests/fstar/misc/Loops.Funs.fst16
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst53
-rw-r--r--tests/fstar/misc/Paper.fst15
-rw-r--r--tests/fstar/misc/PoloniusList.fst8
6 files changed, 32 insertions, 120 deletions
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index a0658206..9b90e9c7 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -22,12 +22,10 @@ let x2_body : result u32 = Return 3
let x2_c : u32 = eval_global x2_body
(** [constants::incr] *)
-let incr_fwd (n : u32) : result u32 =
- begin match u32_add n 1 with | Fail e -> Fail e | Return i -> Return i end
+let incr_fwd (n : u32) : result u32 = u32_add n 1
(** [constants::X3] *)
-let x3_body : result u32 =
- begin match incr_fwd 32 with | Fail e -> Fail e | Return i -> Return i end
+let x3_body : result u32 = incr_fwd 32
let x3_c : u32 = eval_global x3_body
(** [constants::mk_pair0] *)
@@ -41,19 +39,11 @@ let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
Return (Mkpair_t x y)
(** [constants::P0] *)
-let p0_body : result (u32 & u32) =
- begin match mk_pair0_fwd 0 1 with
- | Fail e -> Fail e
- | Return p -> Return p
- end
+let p0_body : result (u32 & u32) = mk_pair0_fwd 0 1
let p0_c : (u32 & u32) = eval_global p0_body
(** [constants::P1] *)
-let p1_body : result (pair_t u32 u32) =
- begin match mk_pair1_fwd 0 1 with
- | Fail e -> Fail e
- | Return p -> Return p
- end
+let p1_body : result (pair_t u32 u32) = mk_pair1_fwd 0 1
let p1_c : pair_t u32 u32 = eval_global p1_body
(** [constants::P2] *)
@@ -72,19 +62,14 @@ let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
Return (Mkwrap_t val0)
(** [constants::Y] *)
-let y_body : result (wrap_t i32) =
- begin match wrap_new_fwd i32 2 with
- | Fail e -> Fail e
- | Return w -> Return w
- end
+let y_body : result (wrap_t i32) = wrap_new_fwd i32 2
let y_c : wrap_t i32 = eval_global y_body
(** [constants::unwrap_y] *)
let unwrap_y_fwd : result i32 = Return y_c.wrap_val
(** [constants::YVAL] *)
-let yval_body : result i32 =
- begin match unwrap_y_fwd with | Fail e -> Fail e | Return i -> Return i end
+let yval_body : result i32 = unwrap_y_fwd
let yval_c : i32 = eval_global yval_body
(** [constants::get_z1::Z1] *)
@@ -95,8 +80,7 @@ let get_z1_z1_c : i32 = eval_global get_z1_z1_body
let get_z1_fwd : result i32 = Return get_z1_z1_c
(** [constants::add] *)
-let add_fwd (a : i32) (b : i32) : result i32 =
- begin match i32_add a b with | Fail e -> Fail e | Return i -> Return i end
+let add_fwd (a : i32) (b : i32) : result i32 = i32_add a b
(** [constants::Q1] *)
let q1_body : result i32 = Return 5
@@ -107,8 +91,7 @@ let q2_body : result i32 = Return q1_c
let q2_c : i32 = eval_global q2_body
(** [constants::Q3] *)
-let q3_body : result i32 =
- begin match add_fwd q2_c 3 with | Fail e -> Fail e | Return i -> Return i end
+let q3_body : result i32 = add_fwd q2_c 3
let q3_c : i32 = eval_global q3_body
(** [constants::get_z2] *)
@@ -118,11 +101,7 @@ let get_z2_fwd : result i32 =
| Return i ->
begin match add_fwd i q3_c with
| Fail e -> Fail e
- | Return i0 ->
- begin match add_fwd q1_c i0 with
- | Fail e -> Fail e
- | Return i1 -> Return i1
- end
+ | Return i0 -> add_fwd q1_c i0
end
end
@@ -131,8 +110,7 @@ let s1_body : result u32 = Return 6
let s1_c : u32 = eval_global s1_body
(** [constants::S2] *)
-let s2_body : result u32 =
- begin match incr_fwd s1_c with | Fail e -> Fail e | Return i -> Return i end
+let s2_body : result u32 = incr_fwd s1_c
let s2_c : u32 = eval_global s2_body
(** [constants::S3] *)
@@ -140,10 +118,6 @@ let s3_body : result (pair_t u32 u32) = Return p3_c
let s3_c : pair_t u32 u32 = eval_global s3_body
(** [constants::S4] *)
-let s4_body : result (pair_t u32 u32) =
- begin match mk_pair1_fwd 7 8 with
- | Fail e -> Fail e
- | Return p -> Return p
- end
+let s4_body : result (pair_t u32 u32) = mk_pair1_fwd 7 8
let s4_c : pair_t u32 u32 = eval_global s4_body
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index a57472d4..2529ec33 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -46,12 +46,7 @@ let test_new_non_zero_u32_fwd
begin match core_num_nonzero_non_zero_u32_new_fwd x st with
| Fail e -> Fail e
| Return (st0, opt) ->
- begin match
- core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
- with
- | Fail e -> Fail e
- | Return (st1, nzu) -> Return (st1, nzu)
- end
+ core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
end
(** [external::test_vec] *)
@@ -112,10 +107,7 @@ let test_custom_swap_back
(x : u32) (y : u32) (st : state) (st0 : state) :
result (state & (u32 & u32))
=
- begin match custom_swap_back u32 x y st 1 st0 with
- | Fail e -> Fail e
- | Return (st1, (x0, y0)) -> Return (st1, (x0, y0))
- end
+ custom_swap_back u32 x y st 1 st0
(** [external::test_swap_non_zero] *)
let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index f5339339..870a2159 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -19,21 +19,14 @@ let rec list_nth_mut_loop_loop0_fwd
else
begin match u32_sub i 1 with
| Fail e -> Fail e
- | Return i0 ->
- begin match list_nth_mut_loop_loop0_fwd t tl i0 with
- | Fail e -> Fail e
- | Return x0 -> Return x0
- end
+ | Return i0 -> list_nth_mut_loop_loop0_fwd t tl i0
end
| ListNil -> Fail Failure
end
(** [loops::list_nth_mut_loop] *)
let list_nth_mut_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
- begin match list_nth_mut_loop_loop0_fwd t ls i with
- | Fail e -> Fail e
- | Return x -> Return x
- end
+ list_nth_mut_loop_loop0_fwd t ls i
(** [loops::list_nth_mut_loop] *)
let rec list_nth_mut_loop_loop0_back
@@ -59,8 +52,5 @@ let rec list_nth_mut_loop_loop0_back
(** [loops::list_nth_mut_loop] *)
let list_nth_mut_loop_back
(t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
- begin match list_nth_mut_loop_loop0_back t ls i ret with
- | Fail e -> Fail e
- | Return l -> Return l
- end
+ list_nth_mut_loop_loop0_back t ls i ret
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 8424a7cc..f8c63798 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -31,35 +31,25 @@ type sum_t (t1 t2 : Type0) =
| SumRight : t2 -> sum_t t1 t2
(** [no_nested_borrows::neg_test] *)
-let neg_test_fwd (x : i32) : result i32 =
- begin match i32_neg x with | Fail e -> Fail e | Return i -> Return i end
+let neg_test_fwd (x : i32) : result i32 = i32_neg x
(** [no_nested_borrows::add_test] *)
-let add_test_fwd (x : u32) (y : u32) : result u32 =
- begin match u32_add x y with | Fail e -> Fail e | Return i -> Return i end
+let add_test_fwd (x : u32) (y : u32) : result u32 = u32_add x y
(** [no_nested_borrows::subs_test] *)
-let subs_test_fwd (x : u32) (y : u32) : result u32 =
- begin match u32_sub x y with | Fail e -> Fail e | Return i -> Return i end
+let subs_test_fwd (x : u32) (y : u32) : result u32 = u32_sub x y
(** [no_nested_borrows::div_test] *)
-let div_test_fwd (x : u32) (y : u32) : result u32 =
- begin match u32_div x y with | Fail e -> Fail e | Return i -> Return i end
+let div_test_fwd (x : u32) (y : u32) : result u32 = u32_div x y
(** [no_nested_borrows::div_test1] *)
-let div_test1_fwd (x : u32) : result u32 =
- begin match u32_div x 2 with | Fail e -> Fail e | Return i -> Return i end
+let div_test1_fwd (x : u32) : result u32 = u32_div x 2
(** [no_nested_borrows::rem_test] *)
-let rem_test_fwd (x : u32) (y : u32) : result u32 =
- begin match u32_rem x y with | Fail e -> Fail e | Return i -> Return i end
+let rem_test_fwd (x : u32) (y : u32) : result u32 = u32_rem x y
(** [no_nested_borrows::cast_test] *)
-let cast_test_fwd (x : u32) : result i32 =
- begin match scalar_cast U32 I32 x with
- | Fail e -> Fail e
- | Return i -> Return i
- end
+let cast_test_fwd (x : u32) : result i32 = scalar_cast U32 I32 x
(** [no_nested_borrows::test2] *)
let test2_fwd : result unit =
@@ -245,11 +235,7 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
| ListCons x l1 ->
begin match list_length_fwd t l1 with
| Fail e -> Fail e
- | Return i ->
- begin match u32_add 1 i with
- | Fail e -> Fail e
- | Return i0 -> Return i0
- end
+ | Return i -> u32_add 1 i
end
| ListNil -> Return 0
end
@@ -263,11 +249,7 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
else
begin match u32_sub i 1 with
| Fail e -> Fail e
- | Return i0 ->
- begin match list_nth_shared_fwd t tl i0 with
- | Fail e -> Fail e
- | Return x0 -> Return x0
- end
+ | Return i0 -> list_nth_shared_fwd t tl i0
end
| ListNil -> Fail Failure
end
@@ -281,11 +263,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
else
begin match u32_sub i 1 with
| Fail e -> Fail e
- | Return i0 ->
- begin match list_nth_mut_fwd t tl i0 with
- | Fail e -> Fail e
- | Return x0 -> Return x0
- end
+ | Return i0 -> list_nth_mut_fwd t tl i0
end
| ListNil -> Fail Failure
end
@@ -313,21 +291,14 @@ let rec list_nth_mut_back
let rec list_rev_aux_fwd
(t : Type0) (li : list_t t) (lo : list_t t) : result (list_t t) =
begin match li with
- | ListCons hd tl ->
- begin match list_rev_aux_fwd t tl (ListCons hd lo) with
- | Fail e -> Fail e
- | Return l -> Return l
- end
+ | ListCons hd tl -> list_rev_aux_fwd t tl (ListCons hd lo)
| ListNil -> Return lo
end
(** [no_nested_borrows::list_rev] *)
let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) =
let li = mem_replace_fwd (list_t t) l ListNil in
- begin match list_rev_aux_fwd t li ListNil with
- | Fail e -> Fail e
- | Return l0 -> Return l0
- end
+ list_rev_aux_fwd t li ListNil
(** [no_nested_borrows::test_list_functions] *)
let test_list_functions_fwd : result unit =
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 0f8604d1..199ceb63 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -6,8 +6,7 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [paper::ref_incr] *)
-let ref_incr_fwd_back (x : i32) : result i32 =
- begin match i32_add x 1 with | Fail e -> Fail e | Return x0 -> Return x0 end
+let ref_incr_fwd_back (x : i32) : result i32 = i32_add x 1
(** [paper::test_incr] *)
let test_incr_fwd : result unit =
@@ -66,11 +65,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
else
begin match u32_sub i 1 with
| Fail e -> Fail e
- | Return i0 ->
- begin match list_nth_mut_fwd t tl i0 with
- | Fail e -> Fail e
- | Return x0 -> Return x0
- end
+ | Return i0 -> list_nth_mut_fwd t tl i0
end
| ListNil -> Fail Failure
end
@@ -100,11 +95,7 @@ let rec sum_fwd (l : list_t i32) : result i32 =
| ListCons x tl ->
begin match sum_fwd tl with
| Fail e -> Fail e
- | Return i ->
- begin match i32_add x i with
- | Fail e -> Fail e
- | Return i0 -> Return i0
- end
+ | Return i -> i32_add x i
end
| ListNil -> Return 0
end
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 158a5fc7..12618dbb 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -14,13 +14,7 @@ type list_t (t : Type0) =
let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
begin match ls with
| ListCons hd tl ->
- if hd = x
- then Return (ListCons hd tl)
- else
- begin match get_list_at_x_fwd tl x with
- | Fail e -> Fail e
- | Return l -> Return l
- end
+ if hd = x then Return (ListCons hd tl) else get_list_at_x_fwd tl x
| ListNil -> Return ListNil
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 15:49:50 +0000