diff options
author | Son Ho | 2022-05-15 22:35:23 +0200 |
---|---|---|
committer | Son Ho | 2022-05-15 22:35:23 +0200 |
commit | 7ca25ab5c3e686eaca2716d003bfb04e742209ec (patch) | |
tree | ace85685c7ec3019d707d7e9532974b13e17c03a /tests/hashmap | |
parent | ffc93a3f4d3b29e3a6805f9882f20dd22d184939 (diff) |
Regenerate the F* files
Diffstat (limited to 'tests/hashmap')
-rw-r--r-- | tests/hashmap/Hashmap.Funs.fst | 67 | ||||
-rw-r--r-- | tests/hashmap/Primitives.fst | 2 |
2 files changed, 33 insertions, 36 deletions
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 |