From 71863baf896d0f6c07473fce16e7568aa39064bc Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 13 Jan 2023 21:44:26 +0100 Subject: Do not unfold the monadic lets for the generated F* code --- tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 607 +++++++---------------- tests/fstar/hashmap_on_disk/Primitives.fst | 4 +- 2 files changed, 188 insertions(+), 423 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 56cff453..51021daf 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -18,15 +18,10 @@ let rec hashmap_hash_map_allocate_slots_loop_fwd (decreases (hashmap_hash_map_allocate_slots_loop_decreases t slots n)) = if n > 0 - then - begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with - | Fail e -> Fail e - | Return slots0 -> - begin match usize_sub n 1 with - | Fail e -> Fail e - | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 - end - end + then begin + let* slots0 = vec_push_back (hashmap_list_t t) slots HashmapListNil in + let* n0 = usize_sub n 1 in + hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 end else Return slots (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) @@ -43,20 +38,11 @@ let hashmap_hash_map_new_with_capacity_fwd result (hashmap_hash_map_t t) = let v = vec_new (hashmap_list_t t) in - begin match hashmap_hash_map_allocate_slots_fwd t v capacity with - | Fail e -> Fail e - | Return slots -> - begin match usize_mul capacity max_load_dividend with - | Fail e -> Fail e - | Return i -> - begin match usize_div i max_load_divisor with - | Fail e -> Fail e - | Return i0 -> - Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0 - slots) - end - end - end + 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) (** [hashmap_main::hashmap::HashMap::{0}::new] *) let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) = @@ -70,28 +56,20 @@ let rec hashmap_hash_map_clear_loop_fwd_back = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 - then - begin match usize_add i 1 with - | Fail e -> Fail e - | Return i1 -> - begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil - with - | Fail e -> Fail e - | Return slots0 -> hashmap_hash_map_clear_loop_fwd_back t slots0 i1 - end - end + then begin + let* i1 = usize_add i 1 in + let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil + in + hashmap_hash_map_clear_loop_fwd_back t slots0 i1 end else Return slots (** [hashmap_main::hashmap::HashMap::{0}::clear] *) let hashmap_hash_map_clear_fwd_back (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = - begin match - hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end + 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) (** [hashmap_main::hashmap::HashMap::{0}::len] *) let hashmap_hash_map_len_fwd @@ -127,11 +105,9 @@ let rec hashmap_hash_map_insert_in_list_loop_back | HashmapListCons ckey cvalue tl -> if ckey = key then Return (HashmapListCons ckey value tl) - else - begin match hashmap_hash_map_insert_in_list_loop_back t key value tl with - | Fail e -> Fail e - | Return tl0 -> Return (HashmapListCons ckey cvalue tl0) - end + else begin + let* tl0 = hashmap_hash_map_insert_in_list_loop_back t key value tl in + Return (HashmapListCons ckey cvalue tl0) end | HashmapListNil -> let l = HashmapListNil in Return (HashmapListCons key value l) end @@ -148,59 +124,30 @@ let hashmap_hash_map_insert_no_resize_fwd_back (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_insert_in_list_fwd t key value l with - | Fail e -> Fail e - | Return inserted -> - if inserted - then - begin match usize_add self.hashmap_hash_map_num_entries 1 with - | Fail e -> Fail e - | Return i0 -> - begin match hashmap_hash_map_insert_in_list_back t key value l - with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhashmap_hash_map_t i0 - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - end - else - begin match hashmap_hash_map_insert_in_list_back t key value l with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail e -> Fail e - | Return v -> - 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) - end - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + in + let* inserted = hashmap_hash_map_insert_in_list_fwd t key value l in + if inserted + then begin + let* i0 = usize_add self.hashmap_hash_map_num_entries 1 in + 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 i0 self.hashmap_hash_map_max_load_factor + self.hashmap_hash_map_max_load v) end + else begin + 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) end - end (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -215,11 +162,8 @@ let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back = begin match ls with | HashmapListCons k v tl -> - begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with - | Fail e -> Fail e - | Return ntable0 -> - hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl - end + let* ntable0 = hashmap_hash_map_insert_no_resize_fwd_back t ntable k v in + hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl | HashmapListNil -> Return ntable end @@ -239,27 +183,15 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 - then - begin match vec_index_mut_fwd (hashmap_list_t t) slots i with - | Fail e -> Fail e - | Return l -> - let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in - begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls - with - | Fail e -> Fail e - | Return ntable0 -> - begin match usize_add i 1 with - | Fail e -> Fail e - | Return i1 -> - let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in - begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with - | Fail e -> Fail e - | Return slots0 -> - hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 - end - end - end - end + then begin + let* l = vec_index_mut_fwd (hashmap_list_t t) slots i in + let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in + let* ntable0 = + hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls in + let* i1 = usize_add i 1 in + let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in + let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i l0 in + hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end else Return (ntable, slots) (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) @@ -273,59 +205,34 @@ let 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) = - begin match scalar_cast U32 Usize core_num_u32_max_c with - | Fail e -> Fail e - | 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 e -> Fail e - | Return n1 -> - let (i, i0) = self.hashmap_hash_map_max_load_factor in - begin match usize_div n1 i with - | Fail e -> Fail e - | Return i1 -> - if capacity <= i1 - then - begin match usize_mul capacity 2 with - | Fail e -> Fail e - | Return i2 -> - begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with - | Fail e -> Fail e - | Return ntable -> - begin match - hashmap_hash_map_move_elements_fwd_back t ntable - self.hashmap_hash_map_slots 0 with - | Fail e -> Fail e - | 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 - 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 + let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in + let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* n1 = usize_div max_usize 2 in + let (i, i0) = self.hashmap_hash_map_max_load_factor in + let* i1 = usize_div n1 i in + if capacity <= i1 + then begin + let* i2 = usize_mul capacity 2 in + let* ntable = hashmap_hash_map_new_with_capacity_fwd t i2 i i0 in + 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) 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) (** [hashmap_main::hashmap::HashMap::{0}::insert] *) let hashmap_hash_map_insert_fwd_back (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_map_insert_no_resize_fwd_back t self key value with - | Fail e -> Fail e - | Return self0 -> - begin match hashmap_hash_map_len_fwd t self0 with - | Fail e -> Fail e - | Return i -> - if i > self0.hashmap_hash_map_max_load - then hashmap_hash_map_try_resize_fwd_back t self0 - else Return self0 - end - end + let* self0 = hashmap_hash_map_insert_no_resize_fwd_back t self key value in + let* i = hashmap_hash_map_len_fwd t self0 in + if i > self0.hashmap_hash_map_max_load + then hashmap_hash_map_try_resize_fwd_back t self0 + else Return self0 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) let rec hashmap_hash_map_contains_key_in_list_loop_fwd @@ -349,21 +256,12 @@ let hashmap_hash_map_contains_key_in_list_fwd (** [hashmap_main::hashmap::HashMap::{0}::contains_key] *) let hashmap_hash_map_contains_key_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod - with - | Fail e -> Fail e - | Return l -> hashmap_hash_map_contains_key_in_list_fwd t key l - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod in + hashmap_hash_map_contains_key_in_list_fwd t key l (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) let rec hashmap_hash_map_get_in_list_loop_fwd @@ -387,21 +285,12 @@ let hashmap_hash_map_get_in_list_fwd (** [hashmap_main::hashmap::HashMap::{0}::get] *) let hashmap_hash_map_get_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod - with - | Fail e -> Fail e - | Return l -> hashmap_hash_map_get_in_list_fwd t key l - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod in + hashmap_hash_map_get_in_list_fwd t key l (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) let rec hashmap_hash_map_get_mut_in_list_loop_fwd @@ -432,11 +321,9 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back | HashmapListCons ckey cvalue tl -> if ckey = key then Return (HashmapListCons ckey ret tl) - else - begin match hashmap_hash_map_get_mut_in_list_loop_back t tl key ret with - | Fail e -> Fail e - | Return tl0 -> Return (HashmapListCons ckey cvalue tl0) - end + else begin + let* tl0 = hashmap_hash_map_get_mut_in_list_loop_back t tl key ret in + Return (HashmapListCons ckey cvalue tl0) end | HashmapListNil -> Fail Failure end @@ -450,55 +337,31 @@ let hashmap_hash_map_get_mut_in_list_back (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) let hashmap_hash_map_get_mut_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail e -> Fail e - | Return l -> hashmap_hash_map_get_mut_in_list_fwd t l key - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + in + hashmap_hash_map_get_mut_in_list_fwd t l key (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) let hashmap_hash_map_get_mut_back (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_get_mut_in_list_back t l key ret with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod l0 with - | Fail e -> Fail e - | Return v -> - 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) - end - end - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + in + let* l0 = hashmap_hash_map_get_mut_in_list_back t l key ret 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) (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) let rec hashmap_hash_map_remove_from_list_loop_fwd @@ -543,11 +406,9 @@ let rec hashmap_hash_map_remove_from_list_loop_back | HashmapListCons i cvalue tl0 -> Return tl0 | HashmapListNil -> Fail Failure end - else - begin match hashmap_hash_map_remove_from_list_loop_back t key tl with - | Fail e -> Fail e - | Return tl0 -> Return (HashmapListCons ckey x tl0) - end + else begin + let* tl0 = hashmap_hash_map_remove_from_list_loop_back t key tl in + Return (HashmapListCons ckey x tl0) end | HashmapListNil -> Return HashmapListNil end @@ -561,32 +422,17 @@ let hashmap_hash_map_remove_from_list_back (** [hashmap_main::hashmap::HashMap::{0}::remove] *) let hashmap_hash_map_remove_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_remove_from_list_fwd t key l with - | Fail e -> Fail e - | Return x -> - begin match x with - | None -> Return None - | Some x0 -> - begin match usize_sub self.hashmap_hash_map_num_entries 1 with - | Fail e -> Fail e - | Return _ -> Return (Some x0) - end - end - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + in + let* x = hashmap_hash_map_remove_from_list_fwd t key l in + begin match x with + | None -> Return None + | Some x0 -> + let* _ = usize_sub self.hashmap_hash_map_num_entries 1 in Return (Some x0) end (** [hashmap_main::hashmap::HashMap::{0}::remove] *) @@ -594,141 +440,66 @@ let hashmap_hash_map_remove_back (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (hashmap_hash_map_t t) = - begin match hashmap_hash_key_fwd key with - | Fail e -> Fail e - | Return hash -> - let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in - begin match usize_rem hash i with - | Fail e -> Fail e - | Return hash_mod -> - begin match - vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots - hash_mod with - | Fail e -> Fail e - | Return l -> - begin match hashmap_hash_map_remove_from_list_fwd t key l with - | Fail e -> Fail e - | Return x -> - begin match x with - | None -> - begin match hashmap_hash_map_remove_from_list_back t key l with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail e -> Fail e - | Return v -> - 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) - end - end - | Some x0 -> - begin match usize_sub self.hashmap_hash_map_num_entries 1 with - | Fail e -> Fail e - | Return i0 -> - begin match hashmap_hash_map_remove_from_list_back t key l with - | Fail e -> Fail e - | Return l0 -> - begin match - vec_index_mut_back (hashmap_list_t t) - self.hashmap_hash_map_slots hash_mod l0 with - | Fail e -> Fail e - | Return v -> - Return (Mkhashmap_hash_map_t i0 - self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) - end - end - end - end - end - end - end + let* hash = hashmap_hash_key_fwd key in + let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in + let* hash_mod = usize_rem hash i in + let* l = + vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod + in + let* x = hashmap_hash_map_remove_from_list_fwd t key l in + begin match x with + | None -> + 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 self.hashmap_hash_map_num_entries + self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load 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) end (** [hashmap_main::hashmap::test1] *) let hashmap_test1_fwd : result unit = - begin match hashmap_hash_map_new_fwd u64 with - | Fail e -> Fail e - | Return hm -> - begin match hashmap_hash_map_insert_fwd_back u64 hm 0 42 with - | Fail e -> Fail e - | Return hm0 -> - begin match hashmap_hash_map_insert_fwd_back u64 hm0 128 18 with - | Fail e -> Fail e - | Return hm1 -> - begin match hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 with - | Fail e -> Fail e - | Return hm2 -> - begin match hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 with - | Fail e -> Fail e - | Return hm3 -> - begin match hashmap_hash_map_get_fwd u64 hm3 128 with - | Fail e -> Fail e - | Return i -> - if not (i = 18) - then Fail Failure - else - begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 with - | Fail e -> Fail e - | Return hm4 -> - begin match hashmap_hash_map_get_fwd u64 hm4 1024 with - | Fail e -> Fail e - | Return i0 -> - if not (i0 = 56) - then Fail Failure - else - begin match hashmap_hash_map_remove_fwd u64 hm4 1024 with - | Fail e -> Fail e - | Return x -> - begin match x with - | None -> Fail Failure - | Some x0 -> - if not (x0 = 56) - then Fail Failure - else - begin match - hashmap_hash_map_remove_back u64 hm4 1024 with - | Fail e -> Fail e - | Return hm5 -> - begin match hashmap_hash_map_get_fwd u64 hm5 0 - with - | Fail e -> Fail e - | Return i1 -> - if not (i1 = 42) - then Fail Failure - else - begin match - hashmap_hash_map_get_fwd u64 hm5 128 with - | Fail e -> Fail e - | Return i2 -> - if not (i2 = 18) - then Fail Failure - else - begin match - hashmap_hash_map_get_fwd u64 hm5 1056 - with - | Fail e -> Fail e - | Return i3 -> - if not (i3 = 256) - then Fail Failure - else Return () - end - end - end - end - end - end - end - end - end - end - end - end - end - end + let* hm = hashmap_hash_map_new_fwd u64 in + let* hm0 = hashmap_hash_map_insert_fwd_back u64 hm 0 42 in + let* hm1 = hashmap_hash_map_insert_fwd_back u64 hm0 128 18 in + let* hm2 = hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 in + let* hm3 = hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 in + let* i = hashmap_hash_map_get_fwd u64 hm3 128 in + if not (i = 18) + then Fail Failure + else begin + let* hm4 = hashmap_hash_map_get_mut_back u64 hm3 1024 56 in + let* i0 = hashmap_hash_map_get_fwd u64 hm4 1024 in + if not (i0 = 56) + then Fail Failure + else begin + let* x = hashmap_hash_map_remove_fwd u64 hm4 1024 in + begin match x with + | None -> Fail Failure + | Some x0 -> + if not (x0 = 56) + then Fail Failure + else begin + let* hm5 = hashmap_hash_map_remove_back u64 hm4 1024 in + let* i1 = hashmap_hash_map_get_fwd u64 hm5 0 in + if not (i1 = 42) + then Fail Failure + else begin + let* i2 = hashmap_hash_map_get_fwd u64 hm5 128 in + if not (i2 = 18) + then Fail Failure + else begin + let* i3 = hashmap_hash_map_get_fwd u64 hm5 1056 in + if not (i3 = 256) then Fail Failure else Return () end end end + end end end (** Unit test for [hashmap_main::hashmap::test1] *) let _ = assert_norm (hashmap_test1_fwd = Return ()) @@ -736,18 +507,10 @@ let _ = assert_norm (hashmap_test1_fwd = Return ()) (** [hashmap_main::insert_on_disk] *) let insert_on_disk_fwd (key : usize) (value : u64) (st : state) : result (state & unit) = - begin match hashmap_utils_deserialize_fwd st with - | Fail e -> Fail e - | Return (st0, hm) -> - begin match hashmap_hash_map_insert_fwd_back u64 hm key value with - | Fail e -> Fail e - | Return hm0 -> - begin match hashmap_utils_serialize_fwd hm0 st0 with - | Fail e -> Fail e - | Return (st1, _) -> Return (st1, ()) - end - end - end + let* (st0, hm) = hashmap_utils_deserialize_fwd st in + let* hm0 = hashmap_hash_map_insert_fwd_back u64 hm key value in + let* (st1, _) = hashmap_utils_serialize_fwd hm0 st0 in + Return (st1, ()) (** [hashmap_main::main] *) let main_fwd : result unit = Return () diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst index bf0f9078..98a696b6 100644 --- a/tests/fstar/hashmap_on_disk/Primitives.fst +++ b/tests/fstar/hashmap_on_disk/Primitives.fst @@ -35,7 +35,9 @@ unfold let return (#a : Type0) (x : a) : result a = Return x // let* x = y in // ... // ``` -unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b = +unfold let (let*) (#a #b : Type0) (m: result a) + (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) : + result b = match m with | Return x -> f x | Fail e -> Fail e -- cgit v1.2.3