diff options
Diffstat (limited to 'tests/fstar/misc/Constants.fst')
-rw-r--r-- | tests/fstar/misc/Constants.fst | 38 |
1 files changed, 25 insertions, 13 deletions
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 |