diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/misc/Paper.fst | 53 |
1 files changed, 29 insertions, 24 deletions
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 |