diff options
Diffstat (limited to 'tests/fstar/misc/Paper.fst')
| -rw-r--r-- | tests/fstar/misc/Paper.fst | 95 |
1 files changed, 26 insertions, 69 deletions
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst index 199ceb63..95f13f62 100644 --- a/tests/fstar/misc/Paper.fst +++ b/tests/fstar/misc/Paper.fst @@ -10,10 +10,8 @@ let ref_incr_fwd_back (x : i32) : result i32 = i32_add x 1 (** [paper::test_incr] *) let test_incr_fwd : result unit = - begin match ref_incr_fwd_back 0 with - | Fail e -> Fail e - | Return x -> if not (x = 1) then Fail Failure else Return () - end + let* x = ref_incr_fwd_back 0 in + if not (x = 1) then Fail Failure else Return () (** Unit test for [paper::test_incr] *) let _ = assert_norm (test_incr_fwd = Return ()) @@ -29,24 +27,15 @@ let choose_back (** [paper::test_choose] *) let test_choose_fwd : result unit = - begin match choose_fwd i32 true 0 0 with - | Fail e -> Fail e - | Return z -> - begin match i32_add z 1 with - | Fail e -> Fail e - | Return z0 -> - if not (z0 = 1) - then Fail Failure - else - begin match choose_back i32 true 0 0 z0 with - | Fail e -> Fail e - | Return (x, y) -> - if not (x = 1) - then Fail Failure - else if not (y = 0) then Fail Failure else Return () - end - end - end + let* z = choose_fwd i32 true 0 0 in + let* z0 = i32_add z 1 in + if not (z0 = 1) + then Fail Failure + else begin + let* (x, y) = choose_back i32 true 0 0 z0 in + if not (x = 1) + then Fail Failure + else if not (y = 0) then Fail Failure else Return () end (** Unit test for [paper::test_choose] *) let _ = assert_norm (test_choose_fwd = Return ()) @@ -62,11 +51,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = | ListCons x tl -> if i = 0 then Return x - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> list_nth_mut_fwd t tl i0 - end + else begin let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 end | ListNil -> Fail Failure end @@ -77,26 +62,17 @@ let rec list_nth_mut_back | ListCons x tl -> if i = 0 then Return (ListCons ret tl) - else - begin match u32_sub i 1 with - | Fail e -> Fail e - | Return i0 -> - begin match list_nth_mut_back t tl i0 ret with - | Fail e -> Fail e - | Return tl0 -> Return (ListCons x tl0) - end - end + else begin + let* i0 = u32_sub i 1 in + let* tl0 = list_nth_mut_back t tl i0 ret in + Return (ListCons x tl0) end | ListNil -> Fail Failure end (** [paper::sum] *) let rec sum_fwd (l : list_t i32) : result i32 = begin match l with - | ListCons x tl -> - begin match sum_fwd tl with - | Fail e -> Fail e - | Return i -> i32_add x i - end + | ListCons x tl -> let* i = sum_fwd tl in i32_add x i | ListNil -> Return 0 end @@ -105,22 +81,11 @@ let test_nth_fwd : result unit = let l = ListNil in 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 e -> Fail e - | Return x -> - begin match i32_add x 1 with - | Fail e -> Fail e - | Return x0 -> - begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with - | Fail e -> Fail e - | Return l2 -> - begin match sum_fwd l2 with - | Fail e -> Fail e - | Return i -> if not (i = 7) then Fail Failure else Return () - end - end - end - end + let* x = list_nth_mut_fwd i32 (ListCons 1 l1) 2 in + let* x0 = i32_add x 1 in + let* l2 = list_nth_mut_back i32 (ListCons 1 l1) 2 x0 in + let* i = sum_fwd l2 in + if not (i = 7) then Fail Failure else Return () (** Unit test for [paper::test_nth] *) let _ = assert_norm (test_nth_fwd = Return ()) @@ -128,16 +93,8 @@ let _ = assert_norm (test_nth_fwd = Return ()) (** [paper::call_choose] *) let call_choose_fwd (p : (u32 & u32)) : result u32 = let (px, py) = p in - begin match choose_fwd u32 true px py with - | Fail e -> Fail e - | Return pz -> - begin match u32_add pz 1 with - | Fail e -> Fail e - | Return pz0 -> - begin match choose_back u32 true px py pz0 with - | Fail e -> Fail e - | Return (px0, _) -> Return px0 - end - end - end + let* pz = choose_fwd u32 true px py in + let* pz0 = u32_add pz 1 in + let* (px0, _) = choose_back u32 true px py pz0 in + Return px0 |