diff options
Diffstat (limited to 'tests/hashmap_on_disk/HashmapMain.Funs.fst')
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Funs.fst | 70 |
1 files changed, 33 insertions, 37 deletions
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 |