From 5a96e28b8706ed945ccbb569881ca1888cd73ace Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 14 Nov 2022 11:58:31 +0100
Subject: Regenerate the files and fix the proofs
---
tests/fstar/misc/Constants.fst | 38 ++++++---
tests/fstar/misc/External.Funs.fst | 41 ++++-----
tests/fstar/misc/NoNestedBorrows.fst | 155 +++++++++++++++++++----------------
tests/fstar/misc/Paper.fst | 53 ++++++------
tests/fstar/misc/PoloniusList.fst | 4 +-
tests/fstar/misc/Primitives.fst | 32 ++++----
6 files changed, 180 insertions(+), 143 deletions(-)
(limited to 'tests/fstar/misc')
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index 884d1778..a0658206 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -23,11 +23,11 @@ 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 -> Fail | Return i -> Return i end
+ begin match u32_add n 1 with | Fail e -> Fail e | Return i -> Return i end
(** [constants::X3] *)
let x3_body : result u32 =
- begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end
+ begin match incr_fwd 32 with | Fail e -> Fail e | Return i -> Return i end
let x3_c : u32 = eval_global x3_body
(** [constants::mk_pair0] *)
@@ -42,12 +42,18 @@ let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
(** [constants::P0] *)
let p0_body : result (u32 & u32) =
- begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+ begin match mk_pair0_fwd 0 1 with
+ | Fail e -> Fail e
+ | Return p -> Return p
+ end
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 -> Fail | Return p -> Return p end
+ begin match mk_pair1_fwd 0 1 with
+ | Fail e -> Fail e
+ | Return p -> Return p
+ end
let p1_c : pair_t u32 u32 = eval_global p1_body
(** [constants::P2] *)
@@ -67,7 +73,10 @@ let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
(** [constants::Y] *)
let y_body : result (wrap_t i32) =
- begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end
+ begin match wrap_new_fwd i32 2 with
+ | Fail e -> Fail e
+ | Return w -> Return w
+ end
let y_c : wrap_t i32 = eval_global y_body
(** [constants::unwrap_y] *)
@@ -75,7 +84,7 @@ 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 -> Fail | Return i -> Return i end
+ begin match unwrap_y_fwd with | Fail e -> Fail e | Return i -> Return i end
let yval_c : i32 = eval_global yval_body
(** [constants::get_z1::Z1] *)
@@ -87,7 +96,7 @@ 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 -> Fail | Return i -> Return i end
+ begin match i32_add a b with | Fail e -> Fail e | Return i -> Return i end
(** [constants::Q1] *)
let q1_body : result i32 = Return 5
@@ -99,19 +108,19 @@ let q2_c : i32 = eval_global q2_body
(** [constants::Q3] *)
let q3_body : result i32 =
- begin match add_fwd q2_c 3 with | Fail -> Fail | Return i -> Return i end
+ begin match add_fwd q2_c 3 with | Fail e -> Fail e | Return i -> Return i end
let q3_c : i32 = eval_global q3_body
(** [constants::get_z2] *)
let get_z2_fwd : result i32 =
begin match get_z1_fwd with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
begin match add_fwd i q3_c with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
begin match add_fwd q1_c i0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i1 -> Return i1
end
end
@@ -123,7 +132,7 @@ let s1_c : u32 = eval_global s1_body
(** [constants::S2] *)
let s2_body : result u32 =
- begin match incr_fwd s1_c with | Fail -> Fail | Return i -> Return i end
+ begin match incr_fwd s1_c with | Fail e -> Fail e | Return i -> Return i end
let s2_c : u32 = eval_global s2_body
(** [constants::S3] *)
@@ -132,6 +141,9 @@ 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 -> Fail | Return p -> Return p end
+ begin match mk_pair1_fwd 7 8 with
+ | Fail e -> Fail e
+ | Return p -> Return p
+ end
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 68a0061e..a57472d4 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -10,13 +10,13 @@ include External.Opaque
(** [external::swap] *)
let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
begin match core_mem_swap_fwd t x y st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match core_mem_swap_back0 t x y st st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, _) ->
begin match core_mem_swap_back1 t x y st st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st2, _) -> Return (st2, ())
end
end
@@ -28,13 +28,13 @@ let swap_back
result (state & (t & t))
=
begin match core_mem_swap_fwd t x y st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, _) ->
begin match core_mem_swap_back0 t x y st st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st2, x0) ->
begin match core_mem_swap_back1 t x y st st2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, y0) -> Return (st0, (x0, y0))
end
end
@@ -44,12 +44,12 @@ let swap_back
let test_new_non_zero_u32_fwd
(x : u32) (st : state) : result (state & core_num_nonzero_non_zero_u32_t) =
begin match core_num_nonzero_non_zero_u32_new_fwd x st with
- | Fail -> Fail
+ | 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 -> Fail
+ | Fail e -> Fail e
| Return (st1, nzu) -> Return (st1, nzu)
end
end
@@ -58,7 +58,7 @@ let test_new_non_zero_u32_fwd
let test_vec_fwd : result unit =
let v = vec_new u32 in
begin match vec_push_back u32 v 0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return _ -> Return ()
end
@@ -69,13 +69,13 @@ let _ = assert_norm (test_vec_fwd = Return ())
let custom_swap_fwd
(t : Type0) (x : t) (y : t) (st : state) : result (state & t) =
begin match core_mem_swap_fwd t x y st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match core_mem_swap_back0 t x y st st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, x0) ->
begin match core_mem_swap_back1 t x y st st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st2, _) -> Return (st2, x0)
end
end
@@ -87,13 +87,13 @@ let custom_swap_back
result (state & (t & t))
=
begin match core_mem_swap_fwd t x y st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, _) ->
begin match core_mem_swap_back0 t x y st st1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st2, _) ->
begin match core_mem_swap_back1 t x y st st2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (_, y0) -> Return (st0, (ret, y0))
end
end
@@ -103,7 +103,7 @@ let custom_swap_back
let test_custom_swap_fwd
(x : u32) (y : u32) (st : state) : result (state & unit) =
begin match custom_swap_fwd u32 x y st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) -> Return (st0, ())
end
@@ -113,18 +113,19 @@ let test_custom_swap_back
result (state & (u32 & u32))
=
begin match custom_swap_back u32 x y st 1 st0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st1, (x0, y0)) -> Return (st1, (x0, y0))
end
(** [external::test_swap_non_zero] *)
let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
begin match swap_fwd u32 x 0 st with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (st0, _) ->
begin match swap_back u32 x 0 st st0 with
- | Fail -> Fail
- | Return (st1, (x0, _)) -> if x0 = 0 then Fail else Return (st1, x0)
+ | Fail e -> Fail e
+ | Return (st1, (x0, _)) ->
+ if x0 = 0 then Fail Failure else Return (st1, x0)
end
end
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 36dea95b..8424a7cc 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -32,38 +32,38 @@ type sum_t (t1 t2 : Type0) =
(** [no_nested_borrows::neg_test] *)
let neg_test_fwd (x : i32) : result i32 =
- begin match i32_neg x with | Fail -> Fail | Return i -> Return i end
+ begin match i32_neg x with | Fail e -> Fail e | Return i -> Return i end
(** [no_nested_borrows::add_test] *)
let add_test_fwd (x : u32) (y : u32) : result u32 =
- begin match u32_add x y with | Fail -> Fail | Return i -> Return i end
+ begin match u32_add x y with | Fail e -> Fail e | Return i -> Return i end
(** [no_nested_borrows::subs_test] *)
let subs_test_fwd (x : u32) (y : u32) : result u32 =
- begin match u32_sub x y with | Fail -> Fail | Return i -> Return i end
+ begin match u32_sub x y with | Fail e -> Fail e | Return i -> Return i end
(** [no_nested_borrows::div_test] *)
let div_test_fwd (x : u32) (y : u32) : result u32 =
- begin match u32_div x y with | Fail -> Fail | Return i -> Return i end
+ begin match u32_div x y with | Fail e -> Fail e | Return i -> Return i end
(** [no_nested_borrows::div_test1] *)
let div_test1_fwd (x : u32) : result u32 =
- begin match u32_div x 2 with | Fail -> Fail | Return i -> Return i end
+ begin match u32_div x 2 with | Fail e -> Fail e | Return i -> Return i end
(** [no_nested_borrows::rem_test] *)
let rem_test_fwd (x : u32) (y : u32) : result u32 =
- begin match u32_rem x y with | Fail -> Fail | Return i -> Return i end
+ begin match u32_rem x y with | Fail e -> Fail e | Return i -> Return i end
(** [no_nested_borrows::cast_test] *)
let cast_test_fwd (x : u32) : result i32 =
begin match scalar_cast U32 I32 x with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i -> Return i
end
(** [no_nested_borrows::test2] *)
let test2_fwd : result unit =
- begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end
+ begin match u32_add 23 44 with | Fail e -> Fail e | Return _ -> Return () end
(** Unit test for [no_nested_borrows::test2] *)
let _ = assert_norm (test2_fwd = Return ())
@@ -75,14 +75,14 @@ let get_max_fwd (x : u32) (y : u32) : result u32 =
(** [no_nested_borrows::test3] *)
let test3_fwd : result unit =
begin match get_max_fwd 4 3 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x ->
begin match get_max_fwd 10 11 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return y ->
begin match u32_add x y with
- | Fail -> Fail
- | Return z -> if not (z = 15) then Fail else Return ()
+ | Fail e -> Fail e
+ | Return z -> if not (z = 15) then Fail Failure else Return ()
end
end
end
@@ -93,15 +93,16 @@ let _ = assert_norm (test3_fwd = Return ())
(** [no_nested_borrows::test_neg1] *)
let test_neg1_fwd : result unit =
begin match i32_neg 3 with
- | Fail -> Fail
- | Return y -> if not (y = -3) then Fail else Return ()
+ | Fail e -> Fail e
+ | Return y -> if not (y = -3) then Fail Failure else Return ()
end
(** Unit test for [no_nested_borrows::test_neg1] *)
let _ = assert_norm (test_neg1_fwd = Return ())
(** [no_nested_borrows::refs_test1] *)
-let refs_test1_fwd : result unit = if not (1 = 1) then Fail else Return ()
+let refs_test1_fwd : result unit =
+ if not (1 = 1) then Fail Failure else Return ()
(** Unit test for [no_nested_borrows::refs_test1] *)
let _ = assert_norm (refs_test1_fwd = Return ())
@@ -109,11 +110,14 @@ let _ = assert_norm (refs_test1_fwd = Return ())
(** [no_nested_borrows::refs_test2] *)
let refs_test2_fwd : result unit =
if not (2 = 2)
- then Fail
+ then Fail Failure
else
if not (0 = 0)
- then Fail
- else if not (2 = 2) then Fail else if not (2 = 2) then Fail else Return ()
+ then Fail Failure
+ else
+ if not (2 = 2)
+ then Fail Failure
+ else if not (2 = 2) then Fail Failure else Return ()
(** Unit test for [no_nested_borrows::refs_test2] *)
let _ = assert_norm (refs_test2_fwd = Return ())
@@ -126,7 +130,7 @@ let _ = assert_norm (test_list1_fwd = Return ())
(** [no_nested_borrows::test_box1] *)
let test_box1_fwd : result unit =
- let b = 1 in let x = b in if not (x = 1) then Fail else Return ()
+ let b = 1 in let x = b in if not (x = 1) then Fail Failure else Return ()
(** Unit test for [no_nested_borrows::test_box1] *)
let _ = assert_norm (test_box1_fwd = Return ())
@@ -136,16 +140,17 @@ let copy_int_fwd (x : i32) : result i32 = Return x
(** [no_nested_borrows::test_unreachable] *)
let test_unreachable_fwd (b : bool) : result unit =
- if b then Fail else Return ()
+ if b then Fail Failure else Return ()
(** [no_nested_borrows::test_panic] *)
-let test_panic_fwd (b : bool) : result unit = if b then Fail else Return ()
+let test_panic_fwd (b : bool) : result unit =
+ if b then Fail Failure else Return ()
(** [no_nested_borrows::test_copy_int] *)
let test_copy_int_fwd : result unit =
begin match copy_int_fwd 0 with
- | Fail -> Fail
- | Return y -> if not (0 = y) then Fail else Return ()
+ | Fail e -> Fail e
+ | Return y -> if not (0 = y) then Fail Failure else Return ()
end
(** Unit test for [no_nested_borrows::test_copy_int] *)
@@ -162,8 +167,8 @@ let is_cons_fwd (t : Type0) (l : list_t t) : result bool =
let test_is_cons_fwd : result unit =
let l = ListNil in
begin match is_cons_fwd i32 (ListCons 0 l) with
- | Fail -> Fail
- | Return b -> if not b then Fail else Return ()
+ | Fail e -> Fail e
+ | Return b -> if not b then Fail Failure else Return ()
end
(** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -171,14 +176,18 @@ let _ = assert_norm (test_is_cons_fwd = Return ())
(** [no_nested_borrows::split_list] *)
let split_list_fwd (t : Type0) (l : list_t t) : result (t & (list_t t)) =
- begin match l with | ListCons hd tl -> Return (hd, tl) | ListNil -> Fail end
+ begin match l with
+ | ListCons hd tl -> Return (hd, tl)
+ | ListNil -> Fail Failure
+ end
(** [no_nested_borrows::test_split_list] *)
let test_split_list_fwd : result unit =
let l = ListNil in
begin match split_list_fwd i32 (ListCons 0 l) with
- | Fail -> Fail
- | Return p -> let (hd, _) = p in if not (hd = 0) then Fail else Return ()
+ | Fail e -> Fail e
+ | Return p ->
+ let (hd, _) = p in if not (hd = 0) then Fail Failure else Return ()
end
(** Unit test for [no_nested_borrows::test_split_list] *)
@@ -196,18 +205,20 @@ let choose_back
(** [no_nested_borrows::choose_test] *)
let choose_test_fwd : result unit =
begin match choose_fwd i32 true 0 0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return z ->
begin match i32_add z 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return z0 ->
if not (z0 = 1)
- then Fail
+ then Fail Failure
else
begin match choose_back i32 true 0 0 z0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (x, y) ->
- if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
+ if not (x = 1)
+ then Fail Failure
+ else if not (y = 0) then Fail Failure else Return ()
end
end
end
@@ -233,9 +244,12 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
begin match l with
| ListCons x l1 ->
begin match list_length_fwd t l1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
- begin match u32_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end
+ begin match u32_add 1 i with
+ | Fail e -> Fail e
+ | Return i0 -> Return i0
+ end
end
| ListNil -> Return 0
end
@@ -248,14 +262,14 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
then Return x
else
begin match u32_sub i 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
begin match list_nth_shared_fwd t tl i0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x0 -> Return x0
end
end
- | ListNil -> Fail
+ | ListNil -> Fail Failure
end
(** [no_nested_borrows::list_nth_mut] *)
@@ -266,14 +280,14 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
then Return x
else
begin match u32_sub i 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
begin match list_nth_mut_fwd t tl i0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x0 -> Return x0
end
end
- | ListNil -> Fail
+ | ListNil -> Fail Failure
end
(** [no_nested_borrows::list_nth_mut] *)
@@ -285,14 +299,14 @@ let rec list_nth_mut_back
then Return (ListCons ret tl)
else
begin match u32_sub i 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
begin match list_nth_mut_back t tl i0 ret with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return tl0 -> Return (ListCons x tl0)
end
end
- | ListNil -> Fail
+ | ListNil -> Fail Failure
end
(** [no_nested_borrows::list_rev_aux] *)
@@ -301,7 +315,7 @@ let rec list_rev_aux_fwd
begin match li with
| ListCons hd tl ->
begin match list_rev_aux_fwd t tl (ListCons hd lo) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l -> Return l
end
| ListNil -> Return lo
@@ -311,7 +325,7 @@ let rec list_rev_aux_fwd
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 -> Fail
+ | Fail e -> Fail e
| Return l0 -> Return l0
end
@@ -321,48 +335,48 @@ let test_list_functions_fwd : result unit =
let l0 = ListCons 2 l in
let l1 = ListCons 1 l0 in
begin match list_length_fwd i32 (ListCons 0 l1) with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
if not (i = 3)
- then Fail
+ then Fail Failure
else
begin match list_nth_shared_fwd i32 (ListCons 0 l1) 0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
if not (i0 = 0)
- then Fail
+ then Fail Failure
else
begin match list_nth_shared_fwd i32 (ListCons 0 l1) 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i1 ->
if not (i1 = 1)
- then Fail
+ then Fail Failure
else
begin match list_nth_shared_fwd i32 (ListCons 0 l1) 2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i2 ->
if not (i2 = 2)
- then Fail
+ then Fail Failure
else
begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return ls ->
begin match list_nth_shared_fwd i32 ls 0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i3 ->
if not (i3 = 0)
- then Fail
+ then Fail Failure
else
begin match list_nth_shared_fwd i32 ls 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i4 ->
if not (i4 = 3)
- then Fail
+ then Fail Failure
else
begin match list_nth_shared_fwd i32 ls 2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i5 ->
- if not (i5 = 2) then Fail else Return ()
+ if not (i5 = 2) then Fail Failure else Return ()
end
end
end
@@ -449,31 +463,31 @@ let new_pair1_fwd : result (struct_with_pair_t u32 u32) =
(** [no_nested_borrows::test_constants] *)
let test_constants_fwd : result unit =
begin match new_tuple1_fwd with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return swt ->
let (i, _) = swt.struct_with_tuple_p in
if not (i = 1)
- then Fail
+ then Fail Failure
else
begin match new_tuple2_fwd with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return swt0 ->
let (i0, _) = swt0.struct_with_tuple_p in
if not (i0 = 1)
- then Fail
+ then Fail Failure
else
begin match new_tuple3_fwd with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return swt1 ->
let (i1, _) = swt1.struct_with_tuple_p in
if not (i1 = 1)
- then Fail
+ then Fail Failure
else
begin match new_pair1_fwd with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return swp ->
if not (swp.struct_with_pair_p.pair_x = 1)
- then Fail
+ then Fail Failure
else Return ()
end
end
@@ -491,7 +505,8 @@ let _ = assert_norm (test_weird_borrows1_fwd = Return ())
(** [no_nested_borrows::test_mem_replace] *)
let test_mem_replace_fwd_back (px : u32) : result u32 =
- let y = mem_replace_fwd u32 px 1 in if not (y = 0) then Fail else Return 2
+ let y = mem_replace_fwd u32 px 1 in
+ if not (y = 0) then Fail Failure else Return 2
(** [no_nested_borrows::test_shared_borrow_bool1] *)
let test_shared_borrow_bool1_fwd (b : bool) : result u32 =
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 424889ef..0f8604d1 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -7,13 +7,13 @@ open Primitives
(** [paper::ref_incr] *)
let ref_incr_fwd_back (x : i32) : result i32 =
- begin match i32_add x 1 with | Fail -> Fail | Return x0 -> Return x0 end
+ begin match i32_add x 1 with | Fail e -> Fail e | Return x0 -> Return x0 end
(** [paper::test_incr] *)
let test_incr_fwd : result unit =
begin match ref_incr_fwd_back 0 with
- | Fail -> Fail
- | Return x -> if not (x = 1) then Fail else Return ()
+ | Fail e -> Fail e
+ | Return x -> if not (x = 1) then Fail Failure else Return ()
end
(** Unit test for [paper::test_incr] *)
@@ -31,18 +31,20 @@ let choose_back
(** [paper::test_choose] *)
let test_choose_fwd : result unit =
begin match choose_fwd i32 true 0 0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return z ->
begin match i32_add z 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return z0 ->
if not (z0 = 1)
- then Fail
+ then Fail Failure
else
begin match choose_back i32 true 0 0 z0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (x, y) ->
- if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
+ if not (x = 1)
+ then Fail Failure
+ else if not (y = 0) then Fail Failure else Return ()
end
end
end
@@ -63,14 +65,14 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
then Return x
else
begin match u32_sub i 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
begin match list_nth_mut_fwd t tl i0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x0 -> Return x0
end
end
- | ListNil -> Fail
+ | ListNil -> Fail Failure
end
(** [paper::list_nth_mut] *)
@@ -82,14 +84,14 @@ let rec list_nth_mut_back
then Return (ListCons ret tl)
else
begin match u32_sub i 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i0 ->
begin match list_nth_mut_back t tl i0 ret with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return tl0 -> Return (ListCons x tl0)
end
end
- | ListNil -> Fail
+ | ListNil -> Fail Failure
end
(** [paper::sum] *)
@@ -97,9 +99,12 @@ let rec sum_fwd (l : list_t i32) : result i32 =
begin match l with
| ListCons x tl ->
begin match sum_fwd tl with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return i ->
- begin match i32_add x i with | Fail -> Fail | Return i0 -> Return i0 end
+ begin match i32_add x i with
+ | Fail e -> Fail e
+ | Return i0 -> Return i0
+ end
end
| ListNil -> Return 0
end
@@ -110,17 +115,17 @@ let test_nth_fwd : result unit =
let l0 = ListCons 3 l in
let l1 = ListCons 2 l0 in
begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x ->
begin match i32_add x 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return x0 ->
begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l2 ->
begin match sum_fwd l2 with
- | Fail -> Fail
- | Return i -> if not (i = 7) then Fail else Return ()
+ | Fail e -> Fail e
+ | Return i -> if not (i = 7) then Fail Failure else Return ()
end
end
end
@@ -133,13 +138,13 @@ let _ = assert_norm (test_nth_fwd = Return ())
let call_choose_fwd (p : (u32 & u32)) : result u32 =
let (px, py) = p in
begin match choose_fwd u32 true px py with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return pz ->
begin match u32_add pz 1 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return pz0 ->
begin match choose_back u32 true px py pz0 with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return (px0, _) -> Return px0
end
end
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 73e98884..158a5fc7 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -18,7 +18,7 @@ let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
then Return (ListCons hd tl)
else
begin match get_list_at_x_fwd tl x with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return l -> Return l
end
| ListNil -> Return ListNil
@@ -33,7 +33,7 @@ let rec get_list_at_x_back
then Return ret
else
begin match get_list_at_x_back tl x ret with
- | Fail -> Fail
+ | Fail e -> Fail e
| Return tl0 -> Return (ListCons hd tl0)
end
| ListNil -> Return ret
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index 96138e46..82622656 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
#pop-options
(*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
type result (a : Type0) : Type0 =
| Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
// Monadic bind and return.
// Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
match m with
| Return x -> f x
- | Fail -> Fail
+ | Fail e -> Fail e
// Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
// Normalize and unwrap a successful result (used for globals).
let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
- if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+ if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- if y <> 0 then mk_scalar ty (x / y) else Fail
+ if y <> 0 then mk_scalar ty (x / y) else Fail Failure
/// The remainder operation
let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
let _ = assert_norm(int_rem (-1) (-2) = -1)
let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
- if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+ if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) :
(requires True)
(ensures (fun res ->
match res with
- | Fail -> True
+ | Fail e -> e == Failure
| Return v' -> length v' = length v + 1)) =
if length v < usize_max then begin
(**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) :
(**) assert(length (append v [x]) = length v + 1);
Return (append v [x])
end
- else Fail
+ else Fail Failure
// The **forward** function shouldn't be used
let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
- if i < length v then Return () else Fail
+ if i < length v then Return () else Fail Failure
let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
- if i < length v then Return (list_update v i x) else Fail
+ if i < length v then Return (list_update v i x) else Fail Failure
// The **backward** function shouldn't be used
let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
- if i < length v then Return (index v i) else Fail
+ if i < length v then Return (index v i) else Fail Failure
let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
- if i < length v then Return () else Fail
+ if i < length v then Return () else Fail Failure
let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
- if i < length v then Return (index v i) else Fail
+ if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
- if i < length v then Return (list_update v i nx) else Fail
+ if i < length v then Return (list_update v i nx) else Fail Failure
--
cgit v1.2.3