From ca77353c20e425c687ba207023d56828de6495b6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 7 Mar 2023 23:50:36 +0100 Subject: Start updating simplify_aggregates --- tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 85 +++++++++++++++++++----- 1 file changed, 67 insertions(+), 18 deletions(-) (limited to 'tests/fstar/hashmap_on_disk') diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 7e1a7636..ae98386a 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -42,8 +42,13 @@ let hashmap_hash_map_new_with_capacity_fwd let* slots = hashmap_hash_map_allocate_slots_fwd t v capacity in let* i = usize_mul capacity max_load_dividend in let* i0 = usize_div i max_load_divisor in - Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0 - slots) + Return + { + hashmap_hash_map_num_entries = 0; + hashmap_hash_map_max_load_factor = (max_load_dividend, max_load_divisor); + hashmap_hash_map_max_load = i0; + hashmap_hash_map_slots = slots + } (** [hashmap_main::hashmap::HashMap::{0}::new] *) let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) = @@ -69,8 +74,13 @@ let hashmap_hash_map_clear_fwd_back (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = let* v = hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0 in - Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) + Return + { + hashmap_hash_map_num_entries = 0; + hashmap_hash_map_max_load_factor = self.hashmap_hash_map_max_load_factor; + hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; + hashmap_hash_map_slots = v + } (** [hashmap_main::hashmap::HashMap::{0}::len] *) let hashmap_hash_map_len_fwd @@ -139,15 +149,27 @@ let hashmap_hash_map_insert_no_resize_fwd_back let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in - Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) + Return + { + hashmap_hash_map_num_entries = i0; + hashmap_hash_map_max_load_factor = + self.hashmap_hash_map_max_load_factor; + hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; + hashmap_hash_map_slots = v + } else let* l0 = hashmap_hash_map_insert_in_list_back t key value l in let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + Return + { + hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; + hashmap_hash_map_max_load_factor = + self.hashmap_hash_map_max_load_factor; + hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; + hashmap_hash_map_slots = v + } (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -217,11 +239,21 @@ let hashmap_hash_map_try_resize_fwd_back let* (ntable0, _) = hashmap_hash_map_move_elements_fwd_back t ntable self.hashmap_hash_map_slots 0 in - 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 + { + hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; + hashmap_hash_map_max_load_factor = (i, i0); + hashmap_hash_map_max_load = ntable0.hashmap_hash_map_max_load; + hashmap_hash_map_slots = ntable0.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) + Return + { + hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; + hashmap_hash_map_max_load_factor = (i, i0); + hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; + hashmap_hash_map_slots = self.hashmap_hash_map_slots + } (** [hashmap_main::hashmap::HashMap::{0}::insert] *) let hashmap_hash_map_insert_fwd_back @@ -360,8 +392,13 @@ let hashmap_hash_map_get_mut_back let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + Return + { + hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; + hashmap_hash_map_max_load_factor = self.hashmap_hash_map_max_load_factor; + hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; + hashmap_hash_map_slots = v + } (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) let rec hashmap_hash_map_remove_from_list_loop_fwd @@ -453,16 +490,28 @@ let hashmap_hash_map_remove_back let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) + Return + { + hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; + hashmap_hash_map_max_load_factor = + self.hashmap_hash_map_max_load_factor; + hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; + hashmap_hash_map_slots = v + } | Some x0 -> let* i0 = usize_sub self.hashmap_hash_map_num_entries 1 in let* l0 = hashmap_hash_map_remove_from_list_back t key l in let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in - Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) + Return + { + hashmap_hash_map_num_entries = i0; + hashmap_hash_map_max_load_factor = + self.hashmap_hash_map_max_load_factor; + hashmap_hash_map_max_load = self.hashmap_hash_map_max_load; + hashmap_hash_map_slots = v + } end (** [hashmap_main::hashmap::test1] *) -- cgit v1.2.3