summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap_on_disk
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/hashmap_on_disk')
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v243
1 files changed, 165 insertions, 78 deletions
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 3eaaec8a..9ae7942c 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -14,22 +14,30 @@ Module HashmapMain_Funs.
Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k.
(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
-Fixpoint hashmap_hash_map_allocate_slots_fwd
- (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
+Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
+ (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (n0 : usize) :
result (vec (Hashmap_list_t T))
:=
match n with
| O => Fail_ OutOfFuel
| S n1 =>
- if n0 s= 0%usize
- then Return slots
- else (
- slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil;
- i <- usize_sub n0 1%usize;
- hashmap_hash_map_allocate_slots_fwd T n1 slots0 i)
+ if n0 s> 0%usize
+ then (
+ slots <- vec_push_back (Hashmap_list_t T) v HashmapListNil;
+ n2 <- usize_sub n0 1%usize;
+ hashmap_hash_map_allocate_slots_loop_fwd T n1 slots n2)
+ else Return v
end
.
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+Definition hashmap_hash_map_allocate_slots_fwd
+ (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
+ result (vec (Hashmap_list_t T))
+ :=
+ hashmap_hash_map_allocate_slots_loop_fwd T n slots n0
+.
+
(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
Definition hashmap_hash_map_new_with_capacity_fwd
(T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
@@ -51,31 +59,37 @@ Definition hashmap_hash_map_new_fwd
.
(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
-Fixpoint hashmap_hash_map_clear_slots_fwd_back
- (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) :
+Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back
+ (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (i : usize) :
result (vec (Hashmap_list_t T))
:=
match n with
| O => Fail_ OutOfFuel
| S n0 =>
- let i0 := vec_len (Hashmap_list_t T) slots in
+ let i0 := vec_len (Hashmap_list_t T) v in
if i s< i0
then (
- slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil;
i1 <- usize_add i 1%usize;
- hashmap_hash_map_clear_slots_fwd_back T n0 slots0 i1)
- else Return slots
+ slots <- vec_index_mut_back (Hashmap_list_t T) v i HashmapListNil;
+ hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots i1)
+ else Return v
end
.
+(** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
+Definition hashmap_hash_map_clear_slots_fwd_back
+ (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) :
+ result (vec (Hashmap_list_t T))
+ :=
+ hashmap_hash_map_clear_slots_loop_fwd_back T n slots (0%usize)
+.
+
(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
Definition hashmap_hash_map_clear_fwd_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
result (Hashmap_hash_map_t T)
:=
- v <-
- hashmap_hash_map_clear_slots_fwd_back T n self.(Hashmap_hash_map_slots)
- (0%usize);
+ v <- hashmap_hash_map_clear_slots_fwd_back T n self.(Hashmap_hash_map_slots);
Return (mkHashmap_hash_map_t (0%usize)
self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v)
.
@@ -87,7 +101,7 @@ Definition hashmap_hash_map_len_fwd
.
(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
-Fixpoint hashmap_hash_map_insert_in_list_fwd
+Fixpoint hashmap_hash_map_insert_in_list_loop_fwd
(T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
result bool
:=
@@ -95,17 +109,25 @@ Fixpoint hashmap_hash_map_insert_in_list_fwd
| O => Fail_ OutOfFuel
| S n0 =>
match ls with
- | HashmapListCons ckey cvalue ls0 =>
+ | HashmapListCons ckey cvalue tl =>
if ckey s= key
then Return false
- else hashmap_hash_map_insert_in_list_fwd T n0 key value ls0
+ else hashmap_hash_map_insert_in_list_loop_fwd T n0 key value tl
| HashmapListNil => Return true
end
end
.
(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
-Fixpoint hashmap_hash_map_insert_in_list_back
+Definition hashmap_hash_map_insert_in_list_fwd
+ (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
+ result bool
+ :=
+ hashmap_hash_map_insert_in_list_loop_fwd T n key value ls
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+Fixpoint hashmap_hash_map_insert_in_list_loop_back
(T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
result (Hashmap_list_t T)
:=
@@ -113,18 +135,26 @@ Fixpoint hashmap_hash_map_insert_in_list_back
| O => Fail_ OutOfFuel
| S n0 =>
match ls with
- | HashmapListCons ckey cvalue ls0 =>
+ | HashmapListCons ckey cvalue tl =>
if ckey s= key
- then Return (HashmapListCons ckey value ls0)
+ then Return (HashmapListCons ckey value tl)
else (
- ls1 <- hashmap_hash_map_insert_in_list_back T n0 key value ls0;
- Return (HashmapListCons ckey cvalue ls1))
+ l <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl;
+ Return (HashmapListCons ckey cvalue l))
| HashmapListNil =>
let l := HashmapListNil in Return (HashmapListCons key value l)
end
end
.
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+Definition hashmap_hash_map_insert_in_list_back
+ (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
+ result (Hashmap_list_t T)
+ :=
+ hashmap_hash_map_insert_in_list_loop_back T n key value ls
+.
+
(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
Definition hashmap_hash_map_insert_no_resize_fwd_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T)
@@ -161,9 +191,8 @@ Definition core_num_u32_max_body : result u32 := Return (4294967295%u32).
Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
-Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back
- (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
- :
+Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
+ (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (ls : Hashmap_list_t T) :
result (Hashmap_hash_map_t T)
:=
match n with
@@ -171,37 +200,54 @@ Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back
| S n0 =>
match ls with
| HashmapListCons k v tl =>
- ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 ntable k v;
- hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable0 tl
- | HashmapListNil => Return ntable
+ ntable <- hashmap_hash_map_insert_no_resize_fwd_back T n0 hm k v;
+ hashmap_hash_map_move_elements_from_list_loop_fwd_back T n0 ntable tl
+ | HashmapListNil => Return hm
end
end
.
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+Definition hashmap_hash_map_move_elements_from_list_fwd_back
+ (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
+ :
+ result (Hashmap_hash_map_t T)
+ :=
+ hashmap_hash_map_move_elements_from_list_loop_fwd_back T n ntable ls
+.
+
(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
-Fixpoint hashmap_hash_map_move_elements_fwd_back
- (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
- (slots : vec (Hashmap_list_t T)) (i : usize) :
+Fixpoint hashmap_hash_map_move_elements_loop_fwd_back
+ (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (v : vec (Hashmap_list_t T))
+ (i : usize) :
result ((Hashmap_hash_map_t T) * (vec (Hashmap_list_t T)))
:=
match n with
| O => Fail_ OutOfFuel
| S n0 =>
- let i0 := vec_len (Hashmap_list_t T) slots in
+ let i0 := vec_len (Hashmap_list_t T) v in
if i s< i0
then (
- l <- vec_index_mut_fwd (Hashmap_list_t T) slots i;
+ l <- vec_index_mut_fwd (Hashmap_list_t T) v i;
let ls := mem_replace_fwd (Hashmap_list_t T) l HashmapListNil in
- ntable0 <-
- hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
- let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in
- slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0;
+ ntable <- hashmap_hash_map_move_elements_from_list_fwd_back T n0 hm ls;
i1 <- usize_add i 1%usize;
- hashmap_hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1)
- else Return (ntable, slots)
+ let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in
+ slots <- vec_index_mut_back (Hashmap_list_t T) v i l0;
+ hashmap_hash_map_move_elements_loop_fwd_back T n0 ntable slots i1)
+ else Return (hm, v)
end
.
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+Definition hashmap_hash_map_move_elements_fwd_back
+ (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
+ (slots : vec (Hashmap_list_t T)) (i : usize) :
+ result ((Hashmap_hash_map_t T) * (vec (Hashmap_list_t T)))
+ :=
+ hashmap_hash_map_move_elements_loop_fwd_back T n ntable slots i
+.
+
(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
Definition hashmap_hash_map_try_resize_fwd_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
@@ -241,21 +287,27 @@ Definition hashmap_hash_map_insert_fwd_back
.
(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
-Fixpoint hashmap_hash_map_contains_key_in_list_fwd
- (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
+Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd
+ (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result bool :=
match n with
| O => Fail_ OutOfFuel
| S n0 =>
match ls with
- | HashmapListCons ckey t ls0 =>
- if ckey s= key
+ | HashmapListCons ckey t tl =>
+ if ckey s= i
then Return true
- else hashmap_hash_map_contains_key_in_list_fwd T n0 key ls0
+ else hashmap_hash_map_contains_key_in_list_loop_fwd T n0 i tl
| HashmapListNil => Return false
end
end
.
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+Definition hashmap_hash_map_contains_key_in_list_fwd
+ (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
+ hashmap_hash_map_contains_key_in_list_loop_fwd T n key ls
+.
+
(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
Definition hashmap_hash_map_contains_key_fwd
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
@@ -269,21 +321,27 @@ Definition hashmap_hash_map_contains_key_fwd
.
(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
-Fixpoint hashmap_hash_map_get_in_list_fwd
- (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
+Fixpoint hashmap_hash_map_get_in_list_loop_fwd
+ (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T :=
match n with
| O => Fail_ OutOfFuel
| S n0 =>
match ls with
- | HashmapListCons ckey cvalue ls0 =>
- if ckey s= key
+ | HashmapListCons ckey cvalue tl =>
+ if ckey s= i
then Return cvalue
- else hashmap_hash_map_get_in_list_fwd T n0 key ls0
+ else hashmap_hash_map_get_in_list_loop_fwd T n0 i tl
| HashmapListNil => Fail_ Failure
end
end
.
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+Definition hashmap_hash_map_get_in_list_fwd
+ (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
+ hashmap_hash_map_get_in_list_loop_fwd T n key ls
+.
+
(** [hashmap_main::hashmap::HashMap::{0}::get] *)
Definition hashmap_hash_map_get_fwd
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
@@ -297,41 +355,55 @@ Definition hashmap_hash_map_get_fwd
.
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
-Fixpoint hashmap_hash_map_get_mut_in_list_fwd
- (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
+Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
+ (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T :=
match n with
| O => Fail_ OutOfFuel
| S n0 =>
match ls with
- | HashmapListCons ckey cvalue ls0 =>
- if ckey s= key
+ | HashmapListCons ckey cvalue tl =>
+ if ckey s= i
then Return cvalue
- else hashmap_hash_map_get_mut_in_list_fwd T n0 key ls0
+ else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 i tl
| HashmapListNil => Fail_ Failure
end
end
.
(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
-Fixpoint hashmap_hash_map_get_mut_in_list_back
- (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) :
+Definition hashmap_hash_map_get_mut_in_list_fwd
+ (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T :=
+ hashmap_hash_map_get_mut_in_list_loop_fwd T n key ls
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
+ (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) (ret : T) :
result (Hashmap_list_t T)
:=
match n with
| O => Fail_ OutOfFuel
| S n0 =>
match ls with
- | HashmapListCons ckey cvalue ls0 =>
- if ckey s= key
- then Return (HashmapListCons ckey ret ls0)
+ | HashmapListCons ckey cvalue tl =>
+ if ckey s= i
+ then Return (HashmapListCons ckey ret tl)
else (
- ls1 <- hashmap_hash_map_get_mut_in_list_back T n0 key ls0 ret;
- Return (HashmapListCons ckey cvalue ls1))
+ l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 i tl ret;
+ Return (HashmapListCons ckey cvalue l))
| HashmapListNil => Fail_ Failure
end
end
.
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+Definition hashmap_hash_map_get_mut_in_list_back
+ (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) :
+ result (Hashmap_list_t T)
+ :=
+ hashmap_hash_map_get_mut_in_list_loop_back T n key ls ret
+.
+
(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
Definition hashmap_hash_map_get_mut_fwd
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
@@ -342,7 +414,7 @@ Definition hashmap_hash_map_get_mut_fwd
hash_mod <- usize_rem hash i;
l <-
vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
- hashmap_hash_map_get_mut_in_list_fwd T n key l
+ hashmap_hash_map_get_mut_in_list_fwd T n l key
.
(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
@@ -355,7 +427,7 @@ Definition hashmap_hash_map_get_mut_back
hash_mod <- usize_rem hash i;
l <-
vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod;
- l0 <- hashmap_hash_map_get_mut_in_list_back T n key l ret;
+ l0 <- hashmap_hash_map_get_mut_in_list_back T n l key ret;
v <-
vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots)
hash_mod l0;
@@ -364,8 +436,8 @@ Definition hashmap_hash_map_get_mut_back
.
(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
-Fixpoint hashmap_hash_map_remove_from_list_fwd
- (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
+Fixpoint hashmap_hash_map_remove_from_list_loop_fwd
+ (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) :
result (option T)
:=
match n with
@@ -373,24 +445,32 @@ Fixpoint hashmap_hash_map_remove_from_list_fwd
| S n0 =>
match ls with
| HashmapListCons ckey t tl =>
- if ckey s= key
+ if ckey s= i
then
let mv_ls :=
mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
HashmapListNil in
match mv_ls with
- | HashmapListCons i cvalue tl0 => Return (Some cvalue)
+ | HashmapListCons i0 cvalue tl0 => Return (Some cvalue)
| HashmapListNil => Fail_ Failure
end
- else hashmap_hash_map_remove_from_list_fwd T n0 key tl
+ else hashmap_hash_map_remove_from_list_loop_fwd T n0 i tl
| HashmapListNil => Return None
end
end
.
(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
-Fixpoint hashmap_hash_map_remove_from_list_back
+Definition hashmap_hash_map_remove_from_list_fwd
(T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
+ result (option T)
+ :=
+ hashmap_hash_map_remove_from_list_loop_fwd T n key ls
+.
+
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+Fixpoint hashmap_hash_map_remove_from_list_loop_back
+ (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) :
result (Hashmap_list_t T)
:=
match n with
@@ -398,23 +478,31 @@ Fixpoint hashmap_hash_map_remove_from_list_back
| S n0 =>
match ls with
| HashmapListCons ckey t tl =>
- if ckey s= key
+ if ckey s= i
then
let mv_ls :=
mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
HashmapListNil in
match mv_ls with
- | HashmapListCons i cvalue tl0 => Return tl0
+ | HashmapListCons i0 cvalue tl0 => Return tl0
| HashmapListNil => Fail_ Failure
end
else (
- tl0 <- hashmap_hash_map_remove_from_list_back T n0 key tl;
- Return (HashmapListCons ckey t tl0))
+ l <- hashmap_hash_map_remove_from_list_loop_back T n0 i tl;
+ Return (HashmapListCons ckey t l))
| HashmapListNil => Return HashmapListNil
end
end
.
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+Definition hashmap_hash_map_remove_from_list_back
+ (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
+ result (Hashmap_list_t T)
+ :=
+ hashmap_hash_map_remove_from_list_loop_back T n key ls
+.
+
(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
Definition hashmap_hash_map_remove_fwd
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
@@ -429,8 +517,7 @@ Definition hashmap_hash_map_remove_fwd
match x with
| None => Return None
| Some x0 =>
- i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
- let _ := i0 in
+ _ <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize;
Return (Some x0)
end
.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 02:24:12 +0000