diff options
Diffstat (limited to 'tests/fstar/hashmap/Hashmap.Funs.fst')
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 200 |
1 files changed, 100 insertions, 100 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 6e67fca4..e3ae587f 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -20,13 +20,13 @@ let rec hash_map_allocate_slots_fwd then Return slots else begin match vec_push_back (list_t t) slots ListNil with - | Fail -> Fail + | Fail e -> Fail e | Return slots0 -> begin match usize_sub n 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> begin match hash_map_allocate_slots_fwd t slots0 i with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return v end end @@ -40,13 +40,13 @@ let hash_map_new_with_capacity_fwd = let v = vec_new (list_t t) in begin match hash_map_allocate_slots_fwd t v capacity with - | Fail -> Fail + | Fail e -> Fail e | Return slots -> begin match usize_mul capacity max_load_dividend with - | Fail -> Fail + | Fail e -> Fail e | Return i -> begin match usize_div i max_load_divisor with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 slots) end @@ -56,7 +56,7 @@ let hash_map_new_with_capacity_fwd (** [hashmap::HashMap::{0}::new] *) let hash_map_new_fwd (t : Type0) : result (hash_map_t t) = begin match hash_map_new_with_capacity_fwd t 32 4 5 with - | Fail -> Fail + | Fail e -> Fail e | Return hm -> Return hm end @@ -70,13 +70,13 @@ let rec hash_map_clear_slots_fwd_back if i < i0 then begin match vec_index_mut_back (list_t t) slots i ListNil with - | Fail -> Fail + | Fail e -> Fail e | Return slots0 -> begin match usize_add i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> begin match hash_map_clear_slots_fwd_back t slots0 i1 with - | Fail -> Fail + | Fail e -> Fail e | Return slots1 -> Return slots1 end end @@ -87,7 +87,7 @@ let rec hash_map_clear_slots_fwd_back let hash_map_clear_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = begin match hash_map_clear_slots_fwd_back t self.hash_map_slots 0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load v) @@ -109,7 +109,7 @@ let rec hash_map_insert_in_list_fwd then Return false else begin match hash_map_insert_in_list_fwd t key value ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return b -> Return b end | ListNil -> Return true @@ -127,7 +127,7 @@ let rec hash_map_insert_in_list_back then Return (ListCons ckey value ls0) else begin match hash_map_insert_in_list_back t key value ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return ls1 -> Return (ListCons ckey cvalue ls1) end | ListNil -> let l = ListNil in Return (ListCons key value l) @@ -139,31 +139,31 @@ let hash_map_insert_no_resize_fwd_back result (hash_map_t t) = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_insert_in_list_fwd t key value l with - | Fail -> Fail + | Fail e -> Fail e | Return inserted -> if inserted then begin match usize_add self.hash_map_num_entries 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match hash_map_insert_in_list_back t key value l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t i0 self.hash_map_max_load_factor self.hash_map_max_load v) @@ -172,12 +172,12 @@ let hash_map_insert_no_resize_fwd_back end else begin match hash_map_insert_in_list_back t key value l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t self.hash_map_num_entries self.hash_map_max_load_factor self.hash_map_max_load v) @@ -201,10 +201,10 @@ let rec hash_map_move_elements_from_list_fwd_back begin match ls with | ListCons k v tl -> begin match hash_map_insert_no_resize_fwd_back t ntable k v with - | Fail -> Fail + | Fail e -> Fail e | Return ntable0 -> begin match hash_map_move_elements_from_list_fwd_back t ntable0 tl with - | Fail -> Fail + | Fail e -> Fail e | Return ntable1 -> Return ntable1 end end @@ -221,22 +221,22 @@ let rec hash_map_move_elements_fwd_back if i < i0 then begin match vec_index_mut_fwd (list_t t) slots i with - | Fail -> Fail + | Fail e -> Fail e | Return l -> let ls = mem_replace_fwd (list_t t) l ListNil in begin match hash_map_move_elements_from_list_fwd_back t ntable ls with - | Fail -> Fail + | Fail e -> Fail e | Return ntable0 -> let l0 = mem_replace_back (list_t t) l ListNil in begin match vec_index_mut_back (list_t t) slots i l0 with - | Fail -> Fail + | Fail e -> Fail e | Return slots0 -> begin match usize_add i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> begin match hash_map_move_elements_fwd_back t ntable0 slots0 i1 with - | Fail -> Fail + | Fail e -> Fail e | Return (ntable1, slots1) -> Return (ntable1, slots1) end end @@ -249,28 +249,28 @@ let rec hash_map_move_elements_fwd_back let hash_map_try_resize_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = begin match scalar_cast U32 Usize core_num_u32_max_c with - | Fail -> Fail + | Fail e -> Fail e | 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 + | Fail e -> Fail e | Return n1 -> let (i, i0) = self.hash_map_max_load_factor in begin match usize_div n1 i with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> if capacity <= i1 then begin match usize_mul capacity 2 with - | Fail -> Fail + | Fail e -> Fail e | Return i2 -> begin match hash_map_new_with_capacity_fwd t i2 i i0 with - | Fail -> Fail + | Fail e -> Fail e | Return ntable -> begin match hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 with - | Fail -> Fail + | Fail e -> Fail e | Return (ntable0, _) -> Return (Mkhash_map_t self.hash_map_num_entries (i, i0) ntable0.hash_map_max_load ntable0.hash_map_slots) @@ -290,15 +290,15 @@ let hash_map_insert_fwd_back result (hash_map_t t) = begin match hash_map_insert_no_resize_fwd_back t self key value with - | Fail -> Fail + | Fail e -> Fail e | Return self0 -> begin match hash_map_len_fwd t self0 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if i > self0.hash_map_max_load then begin match hash_map_try_resize_fwd_back t self0 with - | Fail -> Fail + | Fail e -> Fail e | Return self1 -> Return self1 end else Return self0 @@ -317,7 +317,7 @@ let rec hash_map_contains_key_in_list_fwd then Return true else begin match hash_map_contains_key_in_list_fwd t key ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return b -> Return b end | ListNil -> Return false @@ -327,17 +327,17 @@ let rec hash_map_contains_key_in_list_fwd let hash_map_contains_key_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result bool = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_contains_key_in_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return b -> Return b end end @@ -355,27 +355,27 @@ let rec hash_map_get_in_list_fwd then Return cvalue else begin match hash_map_get_in_list_fwd t key ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [hashmap::HashMap::{0}::get] *) let hash_map_get_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result t = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_get_in_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end end @@ -393,10 +393,10 @@ let rec hash_map_get_mut_in_list_fwd then Return cvalue else begin match hash_map_get_mut_in_list_fwd t key ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [hashmap::HashMap::{0}::get_mut_in_list] *) @@ -411,28 +411,28 @@ let rec hash_map_get_mut_in_list_back then Return (ListCons ckey ret ls0) else begin match hash_map_get_mut_in_list_back t key ls0 ret with - | Fail -> Fail + | Fail e -> Fail e | Return ls1 -> Return (ListCons ckey cvalue ls1) end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [hashmap::HashMap::{0}::get_mut] *) let hash_map_get_mut_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result t = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_get_mut_in_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end end @@ -445,22 +445,22 @@ let hash_map_get_mut_back result (hash_map_t t) = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_get_mut_in_list_back t key l ret with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t self.hash_map_num_entries self.hash_map_max_load_factor self.hash_map_max_load v) @@ -483,11 +483,11 @@ let rec hash_map_remove_from_list_fwd let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in begin match mv_ls with | ListCons i cvalue tl0 -> Return (Some cvalue) - | ListNil -> Fail + | ListNil -> Fail Failure end else begin match hash_map_remove_from_list_fwd t key tl with - | Fail -> Fail + | Fail e -> Fail e | Return opt -> Return opt end | ListNil -> Return None @@ -506,11 +506,11 @@ let rec hash_map_remove_from_list_back let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in begin match mv_ls with | ListCons i cvalue tl0 -> Return tl0 - | ListNil -> Fail + | ListNil -> Fail Failure end else begin match hash_map_remove_from_list_back t key tl with - | Fail -> Fail + | Fail e -> Fail e | Return tl0 -> Return (ListCons ckey x tl0) end | ListNil -> Return ListNil @@ -520,24 +520,24 @@ let rec hash_map_remove_from_list_back let hash_map_remove_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_remove_from_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match x with | None -> Return None | Some x0 -> begin match usize_sub self.hash_map_num_entries 1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (Some x0) end end @@ -550,28 +550,28 @@ let hash_map_remove_fwd let hash_map_remove_back (t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_remove_from_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match x with | None -> begin match hash_map_remove_from_list_back t key l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t self.hash_map_num_entries self.hash_map_max_load_factor self.hash_map_max_load v) @@ -579,15 +579,15 @@ let hash_map_remove_back end | Some x0 -> begin match usize_sub self.hash_map_num_entries 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match hash_map_remove_from_list_back t key l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t i0 self.hash_map_max_load_factor self.hash_map_max_load v) @@ -603,65 +603,65 @@ let hash_map_remove_back (** [hashmap::test1] *) let test1_fwd : result unit = begin match hash_map_new_fwd u64 with - | Fail -> Fail + | Fail e -> Fail e | Return hm -> begin match hash_map_insert_fwd_back u64 hm 0 42 with - | Fail -> Fail + | Fail e -> Fail e | Return hm0 -> begin match hash_map_insert_fwd_back u64 hm0 128 18 with - | Fail -> Fail + | Fail e -> Fail e | Return hm1 -> begin match hash_map_insert_fwd_back u64 hm1 1024 138 with - | Fail -> Fail + | Fail e -> Fail e | Return hm2 -> begin match hash_map_insert_fwd_back u64 hm2 1056 256 with - | Fail -> Fail + | Fail e -> Fail e | Return hm3 -> begin match hash_map_get_fwd u64 hm3 128 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if not (i = 18) - then Fail + then Fail Failure else begin match hash_map_get_mut_back u64 hm3 1024 56 with - | Fail -> Fail + | Fail e -> Fail e | Return hm4 -> begin match hash_map_get_fwd u64 hm4 1024 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> if not (i0 = 56) - then Fail + then Fail Failure else begin match hash_map_remove_fwd u64 hm4 1024 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match x with - | None -> Fail + | None -> Fail Failure | Some x0 -> if not (x0 = 56) - then Fail + then Fail Failure else begin match hash_map_remove_back u64 hm4 1024 with - | Fail -> Fail + | Fail e -> Fail e | Return hm5 -> begin match hash_map_get_fwd u64 hm5 0 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> if not (i1 = 42) - then Fail + then Fail Failure else begin match hash_map_get_fwd u64 hm5 128 with - | Fail -> Fail + | Fail e -> Fail e | Return i2 -> if not (i2 = 18) - then Fail + then Fail Failure else begin match hash_map_get_fwd u64 hm5 1056 with - | Fail -> Fail + | Fail e -> Fail e | Return i3 -> if not (i3 = 256) - then Fail + then Fail Failure else Return () end end |