summaryrefslogtreecommitdiff
path: root/tests/hashmap
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Hashmap.Funs.fst67
-rw-r--r--tests/hashmap/Primitives.fst2
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Funs.fst70
-rw-r--r--tests/hashmap_on_disk/Primitives.fst2
4 files changed, 67 insertions, 74 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
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
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 15:37:38 +0000