diff options
Diffstat (limited to '')
-rw-r--r-- | tests/betree/BetreeMain.Funs.fst | 113 | ||||
-rw-r--r-- | tests/betree/Primitives.fst | 2 | ||||
-rw-r--r-- | tests/hashmap/Hashmap.Funs.fst | 67 | ||||
-rw-r--r-- | tests/hashmap/Primitives.fst | 2 | ||||
-rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Funs.fst | 70 | ||||
-rw-r--r-- | tests/hashmap_on_disk/Primitives.fst | 2 | ||||
-rw-r--r-- | tests/misc/External.Funs.fst | 3 | ||||
-rw-r--r-- | tests/misc/NoNestedBorrows.fst | 49 | ||||
-rw-r--r-- | tests/misc/Paper.fst | 14 | ||||
-rw-r--r-- | tests/misc/Primitives.fst | 2 |
10 files changed, 130 insertions, 194 deletions
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst index b11ca399..9b960ce5 100644 --- a/tests/betree/BetreeMain.Funs.fst +++ b/tests/betree/BetreeMain.Funs.fst @@ -135,9 +135,9 @@ let rec betree_list_split_at_fwd Tot (result ((betree_list_t t) & (betree_list_t t))) (decreases (betree_list_split_at_decreases t self n)) = - begin match n with - | 0 -> Return (BetreeListNil, self) - | _ -> + if n = 0 + then Return (BetreeListNil, self) + else begin match self with | BetreeListCons hd tl -> begin match u64_sub n 1 with @@ -152,7 +152,6 @@ let rec betree_list_split_at_fwd end | BetreeListNil -> Fail end - end (** [betree_main::betree::List::{1}::push_front] *) let betree_list_push_front_fwd_back @@ -528,10 +527,7 @@ and betree_node_lookup_fwd let (k, msg) = p in if k <> key then - begin match - betree_internal_lookup_in_children_fwd (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right) key st0 + begin match betree_internal_lookup_in_children_fwd node key st0 with | Fail -> Fail | Return (st1, opt) -> @@ -559,10 +555,7 @@ and betree_node_lookup_fwd | Return _ -> Return (st0, None) end | BetreeMessageUpsert ufs -> - begin match - betree_internal_lookup_in_children_fwd (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right) key st0 + begin match betree_internal_lookup_in_children_fwd node key st0 with | Fail -> Fail | Return (st1, v) -> @@ -572,10 +565,7 @@ and betree_node_lookup_fwd | Fail -> Fail | Return (st2, v0) -> begin match - betree_internal_lookup_in_children_back - (Mkbetree_internal_t node.betree_internal_id - node.betree_internal_pivot node.betree_internal_left - node.betree_internal_right) key st0 with + betree_internal_lookup_in_children_back node key st0 with | Fail -> Fail | Return node0 -> begin match @@ -601,11 +591,7 @@ and betree_node_lookup_fwd end end | BetreeListNil -> - begin match - betree_internal_lookup_in_children_fwd (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right) key st0 - with + begin match betree_internal_lookup_in_children_fwd node key st0 with | Fail -> Fail | Return (st1, opt) -> begin match @@ -653,10 +639,7 @@ and betree_node_lookup_back (BetreeListCons (k, msg) l) with | Fail -> Fail | Return _ -> - begin match - betree_internal_lookup_in_children_back (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right) key st0 + begin match betree_internal_lookup_in_children_back node key st0 with | Fail -> Fail | Return node0 -> Return (BetreeNodeInternal node0) @@ -669,26 +652,17 @@ and betree_node_lookup_back betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, BetreeMessageInsert v) l) with | Fail -> Fail - | Return _ -> - Return (BetreeNodeInternal (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right)) + | Return _ -> Return (BetreeNodeInternal node) end | BetreeMessageDelete -> begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, BetreeMessageDelete) l) with | Fail -> Fail - | Return _ -> - Return (BetreeNodeInternal (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right)) + | Return _ -> Return (BetreeNodeInternal node) end | BetreeMessageUpsert ufs -> - begin match - betree_internal_lookup_in_children_fwd (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right) key st0 + begin match betree_internal_lookup_in_children_fwd node key st0 with | Fail -> Fail | Return (st1, v) -> @@ -698,10 +672,7 @@ and betree_node_lookup_back | Fail -> Fail | Return (st2, _) -> begin match - betree_internal_lookup_in_children_back - (Mkbetree_internal_t node.betree_internal_id - node.betree_internal_pivot node.betree_internal_left - node.betree_internal_right) key st0 with + betree_internal_lookup_in_children_back node key st0 with | Fail -> Fail | Return node0 -> begin match @@ -718,12 +689,7 @@ and betree_node_lookup_back betree_store_internal_node_fwd node0.betree_internal_id msgs0 st2 with | Fail -> Fail - | Return (_, _) -> - Return (BetreeNodeInternal (Mkbetree_internal_t - node0.betree_internal_id - node0.betree_internal_pivot - node0.betree_internal_left - node0.betree_internal_right)) + | Return (_, _) -> Return (BetreeNodeInternal node0) end end end @@ -737,10 +703,7 @@ and betree_node_lookup_back BetreeListNil with | Fail -> Fail | Return _ -> - begin match - betree_internal_lookup_in_children_back (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right) key st0 + begin match betree_internal_lookup_in_children_back node key st0 with | Fail -> Fail | Return node0 -> Return (BetreeNodeInternal node0) @@ -755,9 +718,7 @@ and betree_node_lookup_back | Return (_, bindings) -> begin match betree_node_lookup_in_bindings_fwd key bindings with | Fail -> Fail - | Return _ -> - Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id - node.betree_leaf_size)) + | Return _ -> Return (BetreeNodeLeaf node) end end end @@ -1323,17 +1284,13 @@ and betree_node_apply_messages_fwd if num_msgs >= params.betree_params_min_flush_size then begin match - betree_internal_flush_fwd (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right) params - node_id_cnt content0 st0 with + betree_internal_flush_fwd node params node_id_cnt content0 st0 + with | Fail -> Fail | Return (st1, content1) -> begin match - betree_internal_flush_back (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right) params - node_id_cnt content0 st0 with + betree_internal_flush_back node params node_id_cnt content0 st0 + with | Fail -> Fail | Return (node0, _) -> begin match @@ -1370,8 +1327,7 @@ and betree_node_apply_messages_fwd if len >= i then begin match - betree_leaf_split_fwd (Mkbetree_leaf_t node.betree_leaf_id - node.betree_leaf_size) content0 params node_id_cnt st0 with + betree_leaf_split_fwd node content0 params node_id_cnt st0 with | Fail -> Fail | Return (st1, _) -> begin match @@ -1418,17 +1374,13 @@ and betree_node_apply_messages_back if num_msgs >= params.betree_params_min_flush_size then begin match - betree_internal_flush_fwd (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right) params - node_id_cnt content0 st0 with + betree_internal_flush_fwd node params node_id_cnt content0 st0 + with | Fail -> Fail | Return (st1, content1) -> begin match - betree_internal_flush_back (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right) params - node_id_cnt content0 st0 with + betree_internal_flush_back node params node_id_cnt content0 st0 + with | Fail -> Fail | Return (node0, node_id_cnt0) -> begin match @@ -1436,10 +1388,7 @@ and betree_node_apply_messages_back content1 st1 with | Fail -> Fail | Return (_, _) -> - Return (BetreeNodeInternal (Mkbetree_internal_t - node0.betree_internal_id node0.betree_internal_pivot - node0.betree_internal_left node0.betree_internal_right), - node_id_cnt0) + Return (BetreeNodeInternal node0, node_id_cnt0) end end end @@ -1448,11 +1397,7 @@ and betree_node_apply_messages_back betree_store_internal_node_fwd node.betree_internal_id content0 st0 with | Fail -> Fail - | Return (_, _) -> - Return (BetreeNodeInternal (Mkbetree_internal_t - node.betree_internal_id node.betree_internal_pivot - node.betree_internal_left node.betree_internal_right), - node_id_cnt) + | Return (_, _) -> Return (BetreeNodeInternal node, node_id_cnt) end end end @@ -1473,8 +1418,7 @@ and betree_node_apply_messages_back if len >= i then begin match - betree_leaf_split_fwd (Mkbetree_leaf_t node.betree_leaf_id - node.betree_leaf_size) content0 params node_id_cnt st0 with + betree_leaf_split_fwd node content0 params node_id_cnt st0 with | Fail -> Fail | Return (st1, new_node) -> begin match @@ -1483,8 +1427,7 @@ and betree_node_apply_messages_back | Fail -> Fail | Return (_, _) -> begin match - betree_leaf_split_back (Mkbetree_leaf_t node.betree_leaf_id - node.betree_leaf_size) content0 params node_id_cnt st0 + betree_leaf_split_back node content0 params node_id_cnt st0 with | Fail -> Fail | Return node_id_cnt0 -> diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst index f73c8c09..fe351f3a 100644 --- a/tests/betree/Primitives.fst +++ b/tests/betree/Primitives.fst @@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala mk_scalar ty (x * y) (** Cast an integer from a [src_ty] to a [tgt_ty] *) -let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = +let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = mk_scalar tgt_ty x /// The scalar types diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst index a97c52b9..83c245fb 100644 --- a/tests/hashmap/Hashmap.Funs.fst +++ b/tests/hashmap/Hashmap.Funs.fst @@ -16,9 +16,9 @@ let rec hash_map_allocate_slots_fwd Tot (result (vec (list_t t))) (decreases (hash_map_allocate_slots_decreases t slots n)) = - begin match n with - | 0 -> Return slots - | _ -> + if n = 0 + then Return slots + else begin match vec_push_back (list_t t) slots ListNil with | Fail -> Fail | Return slots0 -> @@ -31,7 +31,6 @@ let rec hash_map_allocate_slots_fwd end end end - end (** [hashmap::HashMap::{0}::new_with_capacity] *) let hash_map_new_with_capacity_fwd @@ -245,35 +244,39 @@ let rec hash_map_move_elements_fwd_back (** [hashmap::HashMap::{0}::try_resize] *) let hash_map_try_resize_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = - let capacity = vec_len (list_t t) self.hash_map_slots in - begin match usize_div 4294967295 2 with + begin match scalar_cast U32 Usize 4294967295 with | Fail -> Fail - | Return n1 -> - let (i, i0) = self.hash_map_max_load_factor in - begin match usize_div n1 i with + | Return max_usize -> + let capacity = vec_len (list_t t) self.hash_map_slots in + begin match usize_div max_usize 2 with | Fail -> Fail - | Return i1 -> - if capacity <= i1 - then - begin match usize_mul capacity 2 with - | Fail -> Fail - | Return i2 -> - begin match hash_map_new_with_capacity_fwd t i2 i i0 with + | Return n1 -> + let (i, i0) = self.hash_map_max_load_factor in + begin match usize_div n1 i with + | Fail -> Fail + | Return i1 -> + if capacity <= i1 + then + begin match usize_mul capacity 2 with | Fail -> Fail - | Return ntable -> - begin match - hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 - with + | Return i2 -> + begin match hash_map_new_with_capacity_fwd t i2 i i0 with | Fail -> Fail - | Return (ntable0, _) -> - Return (Mkhash_map_t self.hash_map_num_entries (i, i0) - ntable0.hash_map_max_load ntable0.hash_map_slots) + | Return ntable -> + begin match + hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 + with + | Fail -> Fail + | Return (ntable0, _) -> + Return (Mkhash_map_t self.hash_map_num_entries (i, i0) + ntable0.hash_map_max_load ntable0.hash_map_slots) + end end end - end - else - Return (Mkhash_map_t self.hash_map_num_entries (i, i0) - self.hash_map_max_load self.hash_map_slots) + else + Return (Mkhash_map_t self.hash_map_num_entries (i, i0) + self.hash_map_max_load self.hash_map_slots) + end end end @@ -290,17 +293,11 @@ let hash_map_insert_fwd_back | Return i -> if i > self0.hash_map_max_load then - begin match - hash_map_try_resize_fwd_back t (Mkhash_map_t - self0.hash_map_num_entries self0.hash_map_max_load_factor - self0.hash_map_max_load self0.hash_map_slots) with + begin match hash_map_try_resize_fwd_back t self0 with | Fail -> Fail | Return self1 -> Return self1 end - else - Return (Mkhash_map_t self0.hash_map_num_entries - self0.hash_map_max_load_factor self0.hash_map_max_load - self0.hash_map_slots) + else Return self0 end end diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst index f73c8c09..fe351f3a 100644 --- a/tests/hashmap/Primitives.fst +++ b/tests/hashmap/Primitives.fst @@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala mk_scalar ty (x * y) (** Cast an integer from a [src_ty] to a [tgt_ty] *) -let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = +let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = mk_scalar tgt_ty x /// The scalar types diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst index 160df880..d01046ec 100644 --- a/tests/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst @@ -17,9 +17,9 @@ let rec hashmap_hash_map_allocate_slots_fwd Tot (result (vec (hashmap_list_t t))) (decreases (hashmap_hash_map_allocate_slots_decreases t slots n)) = - begin match n with - | 0 -> Return slots - | _ -> + if n = 0 + then Return slots + else begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with | Fail -> Fail | Return slots0 -> @@ -32,7 +32,6 @@ let rec hashmap_hash_map_allocate_slots_fwd end end end - end (** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *) let hashmap_hash_map_new_with_capacity_fwd @@ -258,36 +257,40 @@ let rec hashmap_hash_map_move_elements_fwd_back (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) let hashmap_hash_map_try_resize_fwd_back (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = - let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_div 4294967295 2 with + begin match scalar_cast U32 Usize 4294967295 with | Fail -> Fail - | Return n1 -> - let (i, i0) = self.hashmap_hash_map_max_load_factor in - begin match usize_div n1 i with + | Return max_usize -> + let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + begin match usize_div max_usize 2 with | Fail -> Fail - | Return i1 -> - if capacity <= i1 - then - begin match usize_mul capacity 2 with - | Fail -> Fail - | Return i2 -> - begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with + | Return n1 -> + let (i, i0) = self.hashmap_hash_map_max_load_factor in + begin match usize_div n1 i with + | Fail -> Fail + | Return i1 -> + if capacity <= i1 + then + begin match usize_mul capacity 2 with | Fail -> Fail - | Return ntable -> - begin match - hashmap_hash_map_move_elements_fwd_back t ntable - self.hashmap_hash_map_slots 0 with + | Return i2 -> + begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with | Fail -> Fail - | Return (ntable0, _) -> - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - (i, i0) ntable0.hashmap_hash_map_max_load - ntable0.hashmap_hash_map_slots) + | Return ntable -> + begin match + hashmap_hash_map_move_elements_fwd_back t ntable + self.hashmap_hash_map_slots 0 with + | Fail -> Fail + | Return (ntable0, _) -> + Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + (i, i0) ntable0.hashmap_hash_map_max_load + ntable0.hashmap_hash_map_slots) + end end end - end - else - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) - self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) + else + Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, + i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) + end end end @@ -304,18 +307,11 @@ let hashmap_hash_map_insert_fwd_back | Return i -> if i > self0.hashmap_hash_map_max_load then - begin match - hashmap_hash_map_try_resize_fwd_back t (Mkhashmap_hash_map_t - self0.hashmap_hash_map_num_entries - self0.hashmap_hash_map_max_load_factor - self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) with + begin match hashmap_hash_map_try_resize_fwd_back t self0 with | Fail -> Fail | Return self1 -> Return self1 end - else - Return (Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries - self0.hashmap_hash_map_max_load_factor - self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) + else Return self0 end end diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst index f73c8c09..fe351f3a 100644 --- a/tests/hashmap_on_disk/Primitives.fst +++ b/tests/hashmap_on_disk/Primitives.fst @@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala mk_scalar ty (x * y) (** Cast an integer from a [src_ty] to a [tgt_ty] *) -let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = +let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = mk_scalar tgt_ty x /// The scalar types diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst index aafc0cf6..874b739c 100644 --- a/tests/misc/External.Funs.fst +++ b/tests/misc/External.Funs.fst @@ -109,8 +109,7 @@ let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) = | Return (st0, _) -> begin match swap_back u32 x 0 st with | Fail -> Fail - | Return (x0, _) -> - begin match x0 with | 0 -> Fail | _ -> Return (st0, x0) end + | Return (x0, _) -> if x0 = 0 then Fail else Return (st0, x0) end end diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst index 97688191..35d32514 100644 --- a/tests/misc/NoNestedBorrows.fst +++ b/tests/misc/NoNestedBorrows.fst @@ -56,10 +56,14 @@ let rem_test_fwd (x : u32) (y : u32) : result u32 = (** [no_nested_borrows::cast_test] *) let cast_test_fwd (x : u32) : result i32 = - begin match scalar_cast I32 x with | Fail -> Fail | Return i -> Return i end + begin match scalar_cast U32 I32 x with + | Fail -> Fail + | Return i -> Return i + end (** [no_nested_borrows::test2] *) -let test2_fwd : result unit = Return () +let test2_fwd : result unit = + begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end (** Unit test for [no_nested_borrows::test2] *) let _ = assert_norm (test2_fwd = Return ()) @@ -87,7 +91,11 @@ let test3_fwd : result unit = let _ = assert_norm (test3_fwd = Return ()) (** [no_nested_borrows::test_neg1] *) -let test_neg1_fwd : result unit = Return () +let test_neg1_fwd : result unit = + begin match i32_neg 3 with + | Fail -> Fail + | Return y -> if not (y = -3) then Fail else Return () + end (** Unit test for [no_nested_borrows::test_neg1] *) let _ = assert_norm (test_neg1_fwd = Return ()) @@ -222,27 +230,25 @@ and node_elem_t (t : Type0) = (** [no_nested_borrows::even] *) let rec even_fwd (x : u32) : result bool = - begin match x with - | 0 -> Return true - | _ -> + if x = 0 + then Return true + else begin match u32_sub x 1 with | Fail -> Fail | Return i -> begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end end - end (** [no_nested_borrows::odd] *) and odd_fwd (x : u32) : result bool = - begin match x with - | 0 -> Return false - | _ -> + if x = 0 + then Return false + else begin match u32_sub x 1 with | Fail -> Fail | Return i -> begin match even_fwd i with | Fail -> Fail | Return b -> Return b end end - end (** [no_nested_borrows::test_even_odd] *) let test_even_odd_fwd : result unit = @@ -291,9 +297,9 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 = let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t = begin match l with | ListCons x tl -> - begin match i with - | 0 -> Return x - | _ -> + if i = 0 + then Return x + else begin match u32_sub i 1 with | Fail -> Fail | Return i0 -> @@ -302,7 +308,6 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t = | Return x0 -> Return x0 end end - end | ListNil -> Fail end @@ -310,9 +315,9 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t = let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = begin match l with | ListCons x tl -> - begin match i with - | 0 -> Return x - | _ -> + if i = 0 + then Return x + else begin match u32_sub i 1 with | Fail -> Fail | Return i0 -> @@ -321,7 +326,6 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = | Return x0 -> Return x0 end end - end | ListNil -> Fail end @@ -330,9 +334,9 @@ let rec list_nth_mut_back (t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) = begin match l with | ListCons x tl -> - begin match i with - | 0 -> Return (ListCons ret tl) - | _ -> + if i = 0 + then Return (ListCons ret tl) + else begin match u32_sub i 1 with | Fail -> Fail | Return i0 -> @@ -341,7 +345,6 @@ let rec list_nth_mut_back | Return tl0 -> Return (ListCons x tl0) end end - end | ListNil -> Fail end diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst index d162519a..424889ef 100644 --- a/tests/misc/Paper.fst +++ b/tests/misc/Paper.fst @@ -59,9 +59,9 @@ type list_t (t : Type0) = let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = begin match l with | ListCons x tl -> - begin match i with - | 0 -> Return x - | _ -> + if i = 0 + then Return x + else begin match u32_sub i 1 with | Fail -> Fail | Return i0 -> @@ -70,7 +70,6 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = | Return x0 -> Return x0 end end - end | ListNil -> Fail end @@ -79,9 +78,9 @@ let rec list_nth_mut_back (t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) = begin match l with | ListCons x tl -> - begin match i with - | 0 -> Return (ListCons ret tl) - | _ -> + if i = 0 + then Return (ListCons ret tl) + else begin match u32_sub i 1 with | Fail -> Fail | Return i0 -> @@ -90,7 +89,6 @@ let rec list_nth_mut_back | Return tl0 -> Return (ListCons x tl0) end end - end | ListNil -> Fail end diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst index f73c8c09..fe351f3a 100644 --- a/tests/misc/Primitives.fst +++ b/tests/misc/Primitives.fst @@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala mk_scalar ty (x * y) (** Cast an integer from a [src_ty] to a [tgt_ty] *) -let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = +let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = mk_scalar tgt_ty x /// The scalar types |