summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap_on_disk
diff options
context:
space:
mode:
authorSon Ho2023-01-13 21:44:26 +0100
committerSon HO2023-02-03 11:21:46 +0100
commit71863baf896d0f6c07473fce16e7568aa39064bc (patch)
tree9b3e3c2143c38e3a1b1ead64c315781c23ef4524 /tests/fstar/hashmap_on_disk
parent5eca1a621a6446dfc3e5e63e76f4f810ece9c6e3 (diff)
Do not unfold the monadic lets for the generated F* code
Diffstat (limited to 'tests/fstar/hashmap_on_disk')
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst607
-rw-r--r--tests/fstar/hashmap_on_disk/Primitives.fst4
2 files changed, 188 insertions, 423 deletions
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