diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/hashmap/Hashmap.Funs.fst | 198 |
1 files changed, 90 insertions, 108 deletions
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst index d3d09765..4aa6f02c 100644 --- a/tests/hashmap/Hashmap.Funs.fst +++ b/tests/hashmap/Hashmap.Funs.fst @@ -8,7 +8,7 @@ include Hashmap.Clauses #set-options "--z3rlimit 50 --fuel 0 --ifuel 1" (** [hashmap::hash_key] *) -let hash_key_fwd (k : usize) : result usize = Return k +let hash_key_fwd (k : usize) : result usize = let i = k in Return i (** [hashmap::HashMap::allocate_slots] *) let rec hash_map_allocate_slots_fwd @@ -68,8 +68,7 @@ let rec hash_map_clear_slots_fwd_back (decreases (hash_map_clear_slots_decreases t slots i)) = let i0 = vec_len (list_t t) slots in - let b = i < i0 in - if b + if i < i0 then begin match vec_index_mut_back (list_t t) slots i ListNil with | Fail -> Fail @@ -79,21 +78,20 @@ let rec hash_map_clear_slots_fwd_back | Return i1 -> begin match hash_map_clear_slots_fwd_back t v i1 with | Fail -> Fail - | Return v0 -> Return v0 + | Return v0 -> let slots0 = v0 in Return slots0 end end end - else Return slots + else let slots0 = slots in Return slots0 (** [hashmap::HashMap::clear] *) let hash_map_clear_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = let p = self.hash_map_max_load_factor in let i = self.hash_map_max_load in - let v = self.hash_map_slots in - begin match hash_map_clear_slots_fwd_back t v 0 with + begin match hash_map_clear_slots_fwd_back t self.hash_map_slots 0 with | Fail -> Fail - | Return v0 -> let self0 = Mkhash_map_t 0 p i v0 in Return self0 + | Return v -> let self0 = Mkhash_map_t 0 p i v in Return self0 end (** [hashmap::HashMap::len] *) @@ -108,13 +106,12 @@ let rec hash_map_insert_in_list_fwd = begin match ls with | ListCons ckey cvalue ls0 -> - let b = ckey = key in - if b + if ckey = key then Return false else begin match hash_map_insert_in_list_fwd t key value ls0 with | Fail -> Fail - | Return b0 -> Return b0 + | Return b -> Return b end | ListNil -> Return true end @@ -127,8 +124,7 @@ let rec hash_map_insert_in_list_back = begin match ls with | ListCons ckey cvalue ls0 -> - let b = ckey = key in - if b + if ckey = key then let ls1 = ListCons ckey value ls0 in Return ls1 else begin match hash_map_insert_in_list_back t key value ls0 with @@ -149,12 +145,12 @@ let hash_map_insert_no_resize_fwd_back let i0 = self.hash_map_num_entries in let p = self.hash_map_max_load_factor in let i1 = self.hash_map_max_load in - let v = self.hash_map_slots in - let i2 = vec_len (list_t t) v in + let i2 = vec_len (list_t t) self.hash_map_slots in begin match usize_rem i i2 with | Fail -> Fail | Return hash_mod -> - begin match vec_index_mut_fwd (list_t t) v hash_mod with + begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod + with | Fail -> Fail | Return l -> begin match hash_map_insert_in_list_fwd t key value l with @@ -162,16 +158,18 @@ let hash_map_insert_no_resize_fwd_back | Return b -> if b then - begin match usize_add i0 1 with + begin match usize_add self.hash_map_num_entries 1 with | Fail -> Fail | Return i3 -> begin match hash_map_insert_in_list_back t key value l with | Fail -> Fail | Return l0 -> - begin match vec_index_mut_back (list_t t) v hash_mod l0 with + begin match + vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 + with | Fail -> Fail - | Return v0 -> - let self0 = Mkhash_map_t i3 p i1 v0 in Return self0 + | Return v -> + let self0 = Mkhash_map_t i3 p i1 v in Return self0 end end end @@ -179,10 +177,11 @@ let hash_map_insert_no_resize_fwd_back begin match hash_map_insert_in_list_back t key value l with | Fail -> Fail | Return l0 -> - begin match vec_index_mut_back (list_t t) v hash_mod l0 with + begin match + vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 + with | Fail -> Fail - | Return v0 -> - let self0 = Mkhash_map_t i0 p i1 v0 in Return self0 + | Return v -> let self0 = Mkhash_map_t i0 p i1 v in Return self0 end end end @@ -203,10 +202,10 @@ let rec hash_map_move_elements_from_list_fwd_back | Return h -> begin match hash_map_move_elements_from_list_fwd_back t h tl with | Fail -> Fail - | Return h0 -> Return h0 + | Return h0 -> let ntable0 = h0 in Return ntable0 end end - | ListNil -> Return ntable + | ListNil -> let ntable0 = ntable in Return ntable0 end (** [hashmap::HashMap::move_elements] *) @@ -216,8 +215,7 @@ let rec hash_map_move_elements_fwd_back (decreases (hash_map_move_elements_decreases t ntable slots i)) = let i0 = vec_len (list_t t) slots in - let b = i < i0 in - if b + if i < i0 then begin match vec_index_mut_fwd (list_t t) slots i with | Fail -> Fail @@ -235,31 +233,30 @@ let rec hash_map_move_elements_fwd_back | Return i1 -> begin match hash_map_move_elements_fwd_back t h v i1 with | Fail -> Fail - | Return (h0, v0) -> Return (h0, v0) + | Return (h0, v0) -> + let ntable0 = h0 in let slots0 = v0 in Return (ntable0, slots0) end end end end end - else Return (ntable, slots) + else let ntable0 = ntable in let slots0 = slots in Return (ntable0, slots0) (** [hashmap::HashMap::try_resize] *) let hash_map_try_resize_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = let i = self.hash_map_num_entries in - let p = self.hash_map_max_load_factor in let i0 = self.hash_map_max_load in let v = self.hash_map_slots in - let i1 = vec_len (list_t t) v in + let i1 = vec_len (list_t t) self.hash_map_slots in begin match usize_div 4294967295 2 with | Fail -> Fail | Return n1 -> - let (i2, i3) = p in + let (i2, i3) = self.hash_map_max_load_factor in begin match usize_div n1 i2 with | Fail -> Fail | Return i4 -> - let b = i1 <= i4 in - if b + if i1 <= i4 then begin match usize_mul i1 2 with | Fail -> Fail @@ -267,13 +264,14 @@ let hash_map_try_resize_fwd_back begin match hash_map_new_with_capacity_fwd t i5 i2 i3 with | Fail -> Fail | Return h -> - begin match hash_map_move_elements_fwd_back t h v 0 with + begin match + hash_map_move_elements_fwd_back t h self.hash_map_slots 0 with | Fail -> Fail | Return (h0, v0) -> let i6 = h0.hash_map_max_load in - let v1 = h0.hash_map_slots in - let v2 = mem_replace_back (vec (list_t t)) v0 v1 in - let self0 = Mkhash_map_t i (i2, i3) i6 v2 in + let v1 = mem_replace_back (vec (list_t t)) v0 h0.hash_map_slots + in + let self0 = Mkhash_map_t i (i2, i3) i6 v1 in Return self0 end @@ -298,13 +296,12 @@ let hash_map_insert_fwd_back let p = h.hash_map_max_load_factor in let i1 = h.hash_map_max_load in let v = h.hash_map_slots in - let b = i > i1 in - if b + if i > h.hash_map_max_load then begin match hash_map_try_resize_fwd_back t (Mkhash_map_t i0 p i1 v) with | Fail -> Fail - | Return h0 -> Return h0 + | Return h0 -> let self0 = h0 in Return self0 end else let self0 = Mkhash_map_t i0 p i1 v in Return self0 end @@ -318,13 +315,12 @@ let rec hash_map_contains_key_in_list_fwd = begin match ls with | ListCons ckey x ls0 -> - let b = ckey = key in - if b + if ckey = key then Return true else begin match hash_map_contains_key_in_list_fwd t key ls0 with | Fail -> Fail - | Return b0 -> Return b0 + | Return b -> Return b end | ListNil -> Return false end @@ -335,12 +331,11 @@ let hash_map_contains_key_fwd begin match hash_key_fwd key with | Fail -> Fail | Return i -> - let v = self.hash_map_slots in - let i0 = vec_len (list_t t) v in + let i0 = vec_len (list_t t) self.hash_map_slots in begin match usize_rem i i0 with | Fail -> Fail | Return hash_mod -> - begin match vec_index_fwd (list_t t) v hash_mod with + begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with | Fail -> Fail | Return l -> begin match hash_map_contains_key_in_list_fwd t key l with @@ -358,13 +353,12 @@ let rec hash_map_get_in_list_fwd = begin match ls with | ListCons ckey cvalue ls0 -> - let b = ckey = key in - if b + if ckey = key then Return cvalue else begin match hash_map_get_in_list_fwd t key ls0 with | Fail -> Fail - | Return x -> Return x + | Return x -> let x0 = x in Return x0 end | ListNil -> Fail end @@ -375,17 +369,16 @@ let hash_map_get_fwd begin match hash_key_fwd key with | Fail -> Fail | Return i -> - let v = self.hash_map_slots in - let i0 = vec_len (list_t t) v in + let i0 = vec_len (list_t t) self.hash_map_slots in begin match usize_rem i i0 with | Fail -> Fail | Return hash_mod -> - begin match vec_index_fwd (list_t t) v hash_mod with + begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with | Fail -> Fail | Return l -> begin match hash_map_get_in_list_fwd t key l with | Fail -> Fail - | Return x -> Return x + | Return x -> let x0 = x in Return x0 end end end @@ -398,13 +391,12 @@ let rec hash_map_get_mut_in_list_fwd = begin match ls with | ListCons ckey cvalue ls0 -> - let b = ckey = key in - if b + if ckey = key then Return cvalue else begin match hash_map_get_mut_in_list_fwd t key ls0 with | Fail -> Fail - | Return x -> Return x + | Return x -> let x0 = x in Return x0 end | ListNil -> Fail end @@ -417,9 +409,8 @@ let rec hash_map_get_mut_in_list_back = begin match ls with | ListCons ckey cvalue ls0 -> - let b = ckey = key in - if b - then let ls1 = ListCons ckey ret ls0 in Return ls1 + if ckey = key + then let x = ret in let ls1 = ListCons ckey x ls0 in Return ls1 else begin match hash_map_get_mut_in_list_back t key ls0 ret with | Fail -> Fail @@ -434,17 +425,17 @@ let hash_map_get_mut_fwd begin match hash_key_fwd key with | Fail -> Fail | Return i -> - let v = self.hash_map_slots in - let i0 = vec_len (list_t t) v in + let i0 = vec_len (list_t t) self.hash_map_slots in begin match usize_rem i i0 with | Fail -> Fail | Return hash_mod -> - begin match vec_index_mut_fwd (list_t t) v hash_mod with + begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod + with | Fail -> Fail | Return l -> begin match hash_map_get_mut_in_list_fwd t key l with | Fail -> Fail - | Return x -> Return x + | Return x -> let x0 = x in Return x0 end end end @@ -461,20 +452,21 @@ let hash_map_get_mut_back let i0 = self.hash_map_num_entries in let p = self.hash_map_max_load_factor in let i1 = self.hash_map_max_load in - let v = self.hash_map_slots in - let i2 = vec_len (list_t t) v in + let i2 = vec_len (list_t t) self.hash_map_slots in begin match usize_rem i i2 with | Fail -> Fail | Return hash_mod -> - begin match vec_index_mut_fwd (list_t t) v hash_mod with + begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod + with | Fail -> Fail | Return l -> begin match hash_map_get_mut_in_list_back t key l ret with | Fail -> Fail | Return l0 -> - begin match vec_index_mut_back (list_t t) v hash_mod l0 with + begin match + vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with | Fail -> Fail - | Return v0 -> let self0 = Mkhash_map_t i0 p i1 v0 in Return self0 + | Return v -> let self0 = Mkhash_map_t i0 p i1 v in Return self0 end end end @@ -489,8 +481,7 @@ let rec hash_map_remove_from_list_fwd = begin match ls with | ListCons ckey x tl -> - let b = ckey = key in - if b + if ckey = key then let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in begin match mv_ls with @@ -513,12 +504,11 @@ let rec hash_map_remove_from_list_back = begin match ls with | ListCons ckey x tl -> - let b = ckey = key in - if b + if ckey = key then 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 + | ListCons i cvalue tl0 -> let ls0 = tl0 in Return ls0 | ListNil -> Fail end else @@ -535,13 +525,12 @@ let hash_map_remove_fwd begin match hash_key_fwd key with | Fail -> Fail | Return i -> - let i0 = self.hash_map_num_entries in - let v = self.hash_map_slots in - let i1 = vec_len (list_t t) v in - begin match usize_rem i i1 with + let i0 = vec_len (list_t t) self.hash_map_slots in + begin match usize_rem i i0 with | Fail -> Fail | Return hash_mod -> - begin match vec_index_mut_fwd (list_t t) v hash_mod with + begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod + with | Fail -> Fail | Return l -> begin match hash_map_remove_from_list_fwd t key l with @@ -550,7 +539,7 @@ let hash_map_remove_fwd begin match x with | None -> Return None | Some x0 -> - begin match usize_sub i0 1 with + begin match usize_sub self.hash_map_num_entries 1 with | Fail -> Fail | Return _ -> Return (Some x0) end @@ -569,12 +558,12 @@ let hash_map_remove_back let i0 = self.hash_map_num_entries in let p = self.hash_map_max_load_factor in let i1 = self.hash_map_max_load in - let v = self.hash_map_slots in - let i2 = vec_len (list_t t) v in + let i2 = vec_len (list_t t) self.hash_map_slots in begin match usize_rem i i2 with | Fail -> Fail | Return hash_mod -> - begin match vec_index_mut_fwd (list_t t) v hash_mod with + begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod + with | Fail -> Fail | Return l -> begin match hash_map_remove_from_list_fwd t key l with @@ -585,23 +574,26 @@ let hash_map_remove_back begin match hash_map_remove_from_list_back t key l with | Fail -> Fail | Return l0 -> - begin match vec_index_mut_back (list_t t) v hash_mod l0 with + begin match + vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 + with | Fail -> Fail - | Return v0 -> - let self0 = Mkhash_map_t i0 p i1 v0 in Return self0 + | Return v -> let self0 = Mkhash_map_t i0 p i1 v in Return self0 end end | Some x0 -> - begin match usize_sub i0 1 with + begin match usize_sub self.hash_map_num_entries 1 with | Fail -> Fail | Return i3 -> begin match hash_map_remove_from_list_back t key l with | Fail -> Fail | Return l0 -> - begin match vec_index_mut_back (list_t t) v hash_mod l0 with + begin match + vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 + with | Fail -> Fail - | Return v0 -> - let self0 = Mkhash_map_t i3 p i1 v0 in Return self0 + | Return v -> + let self0 = Mkhash_map_t i3 p i1 v in Return self0 end end end @@ -631,9 +623,7 @@ let test1_fwd : result unit = begin match hash_map_get_fwd u64 h3 128 with | Fail -> Fail | Return i -> - let b = i = 18 in - let b0 = not b in - if b0 + if not (i = 18) then Fail else begin match hash_map_get_mut_back u64 h3 1024 56 with @@ -642,9 +632,7 @@ let test1_fwd : result unit = begin match hash_map_get_fwd u64 h4 1024 with | Fail -> Fail | Return i0 -> - let b1 = i0 = 56 in - let b2 = not b1 in - if b2 + if not (i0 = 56) then Fail else begin match hash_map_remove_fwd u64 h4 1024 with @@ -653,9 +641,7 @@ let test1_fwd : result unit = begin match x with | None -> Fail | Some x0 -> - let b3 = x0 = 56 in - let b4 = not b3 in - if b4 + if not (x0 = 56) then Fail else begin match hash_map_remove_back u64 h4 1024 with @@ -664,26 +650,22 @@ let test1_fwd : result unit = begin match hash_map_get_fwd u64 h5 0 with | Fail -> Fail | Return i1 -> - let b5 = i1 = 42 in - let b6 = not b5 in - if b6 + if not (i1 = 42) then Fail else begin match hash_map_get_fwd u64 h5 128 with | Fail -> Fail | Return i2 -> - let b7 = i2 = 18 in - let b8 = not b7 in - if b8 + if not (i2 = 18) then Fail else begin match hash_map_get_fwd u64 h5 1056 with | Fail -> Fail | Return i3 -> - let b9 = i3 = 256 in - let b10 = not b9 in - if b10 then Fail else Return () + if not (i3 = 256) + then Fail + else Return () end end end |