summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v85
-rw-r--r--tests/coq/hashmap/_CoqProject2
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v89
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Opaque.v6
4 files changed, 100 insertions, 82 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 6bc82677..c8630eb6 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -8,11 +8,11 @@ Require Export Hashmap_Types.
Import Hashmap_Types.
Module Hashmap_Funs.
-(** [hashmap::hash_key] *)
+(** [hashmap::hash_key]: forward function *)
Definition hash_key_fwd (k : usize) : result usize :=
Return k.
-(** [hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *)
Fixpoint hash_map_allocate_slots_loop_fwd
(T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) :
result (vec (List_t T))
@@ -29,7 +29,7 @@ Fixpoint hash_map_allocate_slots_loop_fwd
end
.
-(** [hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap::HashMap::{0}::allocate_slots]: forward function *)
Definition hash_map_allocate_slots_fwd
(T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) :
result (vec (List_t T))
@@ -37,7 +37,7 @@ Definition hash_map_allocate_slots_fwd
hash_map_allocate_slots_loop_fwd T n slots n0
.
-(** [hashmap::HashMap::{0}::new_with_capacity] *)
+(** [hashmap::HashMap::{0}::new_with_capacity]: forward function *)
Definition hash_map_new_with_capacity_fwd
(T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
(max_load_divisor : usize) :
@@ -56,12 +56,13 @@ Definition hash_map_new_with_capacity_fwd
|}
.
-(** [hashmap::HashMap::{0}::new] *)
+(** [hashmap::HashMap::{0}::new]: forward function *)
Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
hash_map_new_with_capacity_fwd T n 32%usize 4%usize 5%usize
.
-(** [hashmap::HashMap::{0}::clear] *)
+(** [hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Fixpoint hash_map_clear_loop_fwd_back
(T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) :
result (vec (List_t T))
@@ -79,7 +80,8 @@ Fixpoint hash_map_clear_loop_fwd_back
end
.
-(** [hashmap::HashMap::{0}::clear] *)
+(** [hashmap::HashMap::{0}::clear]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition hash_map_clear_fwd_back
(T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) 0%usize;
@@ -92,12 +94,12 @@ Definition hash_map_clear_fwd_back
|}
.
-(** [hashmap::HashMap::{0}::len] *)
+(** [hashmap::HashMap::{0}::len]: forward function *)
Definition hash_map_len_fwd (T : Type) (self : Hash_map_t T) : result usize :=
Return self.(Hash_map_num_entries)
.
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *)
Fixpoint hash_map_insert_in_list_loop_fwd
(T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
result bool
@@ -115,7 +117,7 @@ Fixpoint hash_map_insert_in_list_loop_fwd
end
.
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: forward function *)
Definition hash_map_insert_in_list_fwd
(T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
result bool
@@ -123,7 +125,7 @@ Definition hash_map_insert_in_list_fwd
hash_map_insert_in_list_loop_fwd T n key value ls
.
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *)
Fixpoint hash_map_insert_in_list_loop_back
(T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
result (List_t T)
@@ -143,7 +145,7 @@ Fixpoint hash_map_insert_in_list_loop_back
end
.
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: backward function 0 *)
Definition hash_map_insert_in_list_back
(T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) :
result (List_t T)
@@ -151,7 +153,8 @@ Definition hash_map_insert_in_list_back
hash_map_insert_in_list_loop_back T n key value ls
.
-(** [hashmap::HashMap::{0}::insert_no_resize] *)
+(** [hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition hash_map_insert_no_resize_fwd_back
(T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
result (Hash_map_t T)
@@ -189,7 +192,8 @@ Definition hash_map_insert_no_resize_fwd_back
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::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Fixpoint hash_map_move_elements_from_list_loop_fwd_back
(T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) :
result (Hash_map_t T)
@@ -206,7 +210,8 @@ Fixpoint hash_map_move_elements_from_list_loop_fwd_back
end
.
-(** [hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition hash_map_move_elements_from_list_fwd_back
(T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) :
result (Hash_map_t T)
@@ -214,7 +219,8 @@ Definition hash_map_move_elements_from_list_fwd_back
hash_map_move_elements_from_list_loop_fwd_back T n ntable ls
.
-(** [hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Fixpoint hash_map_move_elements_loop_fwd_back
(T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T))
(i : usize) :
@@ -237,7 +243,8 @@ Fixpoint hash_map_move_elements_loop_fwd_back
end
.
-(** [hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap::HashMap::{0}::move_elements]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition hash_map_move_elements_fwd_back
(T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T))
(i : usize) :
@@ -246,7 +253,8 @@ Definition hash_map_move_elements_fwd_back
hash_map_move_elements_loop_fwd_back T n ntable slots i
.
-(** [hashmap::HashMap::{0}::try_resize] *)
+(** [hashmap::HashMap::{0}::try_resize]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition hash_map_try_resize_fwd_back
(T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
@@ -278,7 +286,8 @@ Definition hash_map_try_resize_fwd_back
|}
.
-(** [hashmap::HashMap::{0}::insert] *)
+(** [hashmap::HashMap::{0}::insert]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition hash_map_insert_fwd_back
(T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) :
result (Hash_map_t T)
@@ -290,7 +299,7 @@ Definition hash_map_insert_fwd_back
else Return self0
.
-(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *)
Fixpoint hash_map_contains_key_in_list_loop_fwd
(T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool :=
match n with
@@ -306,13 +315,13 @@ Fixpoint hash_map_contains_key_in_list_loop_fwd
end
.
-(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap::HashMap::{0}::contains_key_in_list]: forward function *)
Definition hash_map_contains_key_in_list_fwd
(T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool :=
hash_map_contains_key_in_list_loop_fwd T n key ls
.
-(** [hashmap::HashMap::{0}::contains_key] *)
+(** [hashmap::HashMap::{0}::contains_key]: forward function *)
Definition hash_map_contains_key_fwd
(T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result bool :=
hash <- hash_key_fwd key;
@@ -322,7 +331,7 @@ Definition hash_map_contains_key_fwd
hash_map_contains_key_in_list_fwd T n key l
.
-(** [hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *)
Fixpoint hash_map_get_in_list_loop_fwd
(T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
match n with
@@ -338,13 +347,13 @@ Fixpoint hash_map_get_in_list_loop_fwd
end
.
-(** [hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap::HashMap::{0}::get_in_list]: forward function *)
Definition hash_map_get_in_list_fwd
(T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
hash_map_get_in_list_loop_fwd T n key ls
.
-(** [hashmap::HashMap::{0}::get] *)
+(** [hashmap::HashMap::{0}::get]: forward function *)
Definition hash_map_get_fwd
(T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
hash <- hash_key_fwd key;
@@ -354,7 +363,7 @@ Definition hash_map_get_fwd
hash_map_get_in_list_fwd T n key l
.
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *)
Fixpoint hash_map_get_mut_in_list_loop_fwd
(T : Type) (n : nat) (ls : List_t T) (key : usize) : result T :=
match n with
@@ -370,13 +379,13 @@ Fixpoint hash_map_get_mut_in_list_loop_fwd
end
.
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: forward function *)
Definition hash_map_get_mut_in_list_fwd
(T : Type) (n : nat) (ls : List_t T) (key : usize) : result T :=
hash_map_get_mut_in_list_loop_fwd T n ls key
.
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *)
Fixpoint hash_map_get_mut_in_list_loop_back
(T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) :
result (List_t T)
@@ -396,7 +405,7 @@ Fixpoint hash_map_get_mut_in_list_loop_back
end
.
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *)
Definition hash_map_get_mut_in_list_back
(T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) :
result (List_t T)
@@ -404,7 +413,7 @@ Definition hash_map_get_mut_in_list_back
hash_map_get_mut_in_list_loop_back T n ls key ret
.
-(** [hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap::HashMap::{0}::get_mut]: forward function *)
Definition hash_map_get_mut_fwd
(T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T :=
hash <- hash_key_fwd key;
@@ -414,7 +423,7 @@ Definition hash_map_get_mut_fwd
hash_map_get_mut_in_list_fwd T n l key
.
-(** [hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap::HashMap::{0}::get_mut]: backward function 0 *)
Definition hash_map_get_mut_back
(T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (ret : T) :
result (Hash_map_t T)
@@ -434,7 +443,7 @@ Definition hash_map_get_mut_back
|}
.
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *)
Fixpoint hash_map_remove_from_list_loop_fwd
(T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) :=
match n with
@@ -455,13 +464,13 @@ Fixpoint hash_map_remove_from_list_loop_fwd
end
.
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: forward function *)
Definition hash_map_remove_from_list_fwd
(T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) :=
hash_map_remove_from_list_loop_fwd T n key ls
.
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *)
Fixpoint hash_map_remove_from_list_loop_back
(T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) :=
match n with
@@ -484,13 +493,13 @@ Fixpoint hash_map_remove_from_list_loop_back
end
.
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: backward function 1 *)
Definition hash_map_remove_from_list_back
(T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) :=
hash_map_remove_from_list_loop_back T n key ls
.
-(** [hashmap::HashMap::{0}::remove] *)
+(** [hashmap::HashMap::{0}::remove]: forward function *)
Definition hash_map_remove_fwd
(T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
result (option T)
@@ -507,7 +516,7 @@ Definition hash_map_remove_fwd
end
.
-(** [hashmap::HashMap::{0}::remove] *)
+(** [hashmap::HashMap::{0}::remove]: backward function 0 *)
Definition hash_map_remove_back
(T : Type) (n : nat) (self : Hash_map_t T) (key : usize) :
result (Hash_map_t T)
@@ -542,7 +551,7 @@ Definition hash_map_remove_back
end
.
-(** [hashmap::test1] *)
+(** [hashmap::test1]: forward function *)
Definition test1_fwd (n : nat) : result unit :=
hm <- hash_map_new_fwd u64 n;
hm0 <- hash_map_insert_fwd_back u64 n hm 0%usize 42%u64;
diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject
index daa9b2ba..7f80afbf 100644
--- a/tests/coq/hashmap/_CoqProject
+++ b/tests/coq/hashmap/_CoqProject
@@ -3,6 +3,6 @@
-arg -w
-arg all
-Primitives.v
Hashmap_Types.v
+Primitives.v
Hashmap_Funs.v
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 2d1bcda6..1b7304cc 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -10,11 +10,11 @@ Require Export HashmapMain_Opaque.
Import HashmapMain_Opaque.
Module HashmapMain_Funs.
-(** [hashmap_main::hashmap::hash_key] *)
+(** [hashmap_main::hashmap::hash_key]: forward function *)
Definition hashmap_hash_key_fwd (k : usize) : result usize :=
Return k.
-(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *)
Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
(T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
result (vec (Hashmap_list_t T))
@@ -31,7 +31,7 @@ Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function *)
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))
@@ -39,7 +39,7 @@ Definition hashmap_hash_map_allocate_slots_fwd
hashmap_hash_map_allocate_slots_loop_fwd T n slots n0
.
-(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
+(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity]: forward function *)
Definition hashmap_hash_map_new_with_capacity_fwd
(T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize)
(max_load_divisor : usize) :
@@ -58,13 +58,14 @@ Definition hashmap_hash_map_new_with_capacity_fwd
|}
.
-(** [hashmap_main::hashmap::HashMap::{0}::new] *)
+(** [hashmap_main::hashmap::HashMap::{0}::new]: forward function *)
Definition hashmap_hash_map_new_fwd
(T : Type) (n : nat) : result (Hashmap_hash_map_t T) :=
hashmap_hash_map_new_with_capacity_fwd T n 32%usize 4%usize 5%usize
.
-(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+(** [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Fixpoint hashmap_hash_map_clear_loop_fwd_back
(T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) :
result (vec (Hashmap_list_t T))
@@ -82,7 +83,8 @@ Fixpoint hashmap_hash_map_clear_loop_fwd_back
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+(** [hashmap_main::hashmap::HashMap::{0}::clear]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition hashmap_hash_map_clear_fwd_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
result (Hashmap_hash_map_t T)
@@ -100,13 +102,13 @@ Definition hashmap_hash_map_clear_fwd_back
|}
.
-(** [hashmap_main::hashmap::HashMap::{0}::len] *)
+(** [hashmap_main::hashmap::HashMap::{0}::len]: forward function *)
Definition hashmap_hash_map_len_fwd
(T : Type) (self : Hashmap_hash_map_t T) : result usize :=
Return self.(Hashmap_hash_map_num_entries)
.
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *)
Fixpoint hashmap_hash_map_insert_in_list_loop_fwd
(T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
result bool
@@ -124,7 +126,7 @@ Fixpoint hashmap_hash_map_insert_in_list_loop_fwd
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: forward function *)
Definition hashmap_hash_map_insert_in_list_fwd
(T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) :
result bool
@@ -132,7 +134,7 @@ Definition hashmap_hash_map_insert_in_list_fwd
hashmap_hash_map_insert_in_list_loop_fwd T n key value ls
.
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *)
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)
@@ -153,7 +155,7 @@ Fixpoint hashmap_hash_map_insert_in_list_loop_back
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: backward function 0 *)
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)
@@ -161,7 +163,8 @@ Definition hashmap_hash_map_insert_in_list_back
hashmap_hash_map_insert_in_list_loop_back T n key value ls
.
-(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition hashmap_hash_map_insert_no_resize_fwd_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T)
:
@@ -207,7 +210,8 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back
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] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
(T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
:
@@ -225,7 +229,8 @@ Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
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)
:
@@ -234,7 +239,8 @@ Definition hashmap_hash_map_move_elements_from_list_fwd_back
hashmap_hash_map_move_elements_from_list_loop_fwd_back T n ntable ls
.
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Fixpoint hashmap_hash_map_move_elements_loop_fwd_back
(T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
(slots : vec (Hashmap_list_t T)) (i : usize) :
@@ -258,7 +264,8 @@ Fixpoint hashmap_hash_map_move_elements_loop_fwd_back
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
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) :
@@ -267,7 +274,8 @@ Definition hashmap_hash_map_move_elements_fwd_back
hashmap_hash_map_move_elements_loop_fwd_back T n ntable slots i
.
-(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
+(** [hashmap_main::hashmap::HashMap::{0}::try_resize]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition hashmap_hash_map_try_resize_fwd_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
result (Hashmap_hash_map_t T)
@@ -302,7 +310,8 @@ Definition hashmap_hash_map_try_resize_fwd_back
|}
.
-(** [hashmap_main::hashmap::HashMap::{0}::insert] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition hashmap_hash_map_insert_fwd_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T)
:
@@ -315,7 +324,7 @@ Definition hashmap_hash_map_insert_fwd_back
else Return self0
.
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *)
Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd
(T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
match n with
@@ -331,13 +340,13 @@ Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: forward function *)
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] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key]: forward function *)
Definition hashmap_hash_map_contains_key_fwd
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
result bool
@@ -349,7 +358,7 @@ Definition hashmap_hash_map_contains_key_fwd
hashmap_hash_map_contains_key_in_list_fwd T n key l
.
-(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *)
Fixpoint hashmap_hash_map_get_in_list_loop_fwd
(T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
match n with
@@ -365,13 +374,13 @@ Fixpoint hashmap_hash_map_get_in_list_loop_fwd
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: forward function *)
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] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get]: forward function *)
Definition hashmap_hash_map_get_fwd
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
result T
@@ -383,7 +392,7 @@ Definition hashmap_hash_map_get_fwd
hashmap_hash_map_get_in_list_fwd T n key l
.
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *)
Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
(T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T :=
match n with
@@ -399,13 +408,13 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: forward function *)
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 ls key
.
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *)
Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
(T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) :
result (Hashmap_list_t T)
@@ -425,7 +434,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *)
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)
@@ -433,7 +442,7 @@ Definition hashmap_hash_map_get_mut_in_list_back
hashmap_hash_map_get_mut_in_list_loop_back T n ls key ret
.
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: forward function *)
Definition hashmap_hash_map_get_mut_fwd
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
result T
@@ -446,7 +455,7 @@ Definition hashmap_hash_map_get_mut_fwd
hashmap_hash_map_get_mut_in_list_fwd T n l key
.
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 *)
Definition hashmap_hash_map_get_mut_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (ret : T) :
result (Hashmap_hash_map_t T)
@@ -470,7 +479,7 @@ Definition hashmap_hash_map_get_mut_back
|}
.
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *)
Fixpoint hashmap_hash_map_remove_from_list_loop_fwd
(T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
result (option T)
@@ -495,7 +504,7 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_fwd
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function *)
Definition hashmap_hash_map_remove_from_list_fwd
(T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
result (option T)
@@ -503,7 +512,7 @@ Definition hashmap_hash_map_remove_from_list_fwd
hashmap_hash_map_remove_from_list_loop_fwd T n key ls
.
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *)
Fixpoint hashmap_hash_map_remove_from_list_loop_back
(T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
result (Hashmap_list_t T)
@@ -530,7 +539,7 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_back
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: backward function 1 *)
Definition hashmap_hash_map_remove_from_list_back
(T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
result (Hashmap_list_t T)
@@ -538,7 +547,7 @@ Definition hashmap_hash_map_remove_from_list_back
hashmap_hash_map_remove_from_list_loop_back T n key ls
.
-(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove]: forward function *)
Definition hashmap_hash_map_remove_fwd
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
result (option T)
@@ -557,7 +566,7 @@ Definition hashmap_hash_map_remove_fwd
end
.
-(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 *)
Definition hashmap_hash_map_remove_back
(T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) :
result (Hashmap_hash_map_t T)
@@ -599,7 +608,7 @@ Definition hashmap_hash_map_remove_back
end
.
-(** [hashmap_main::hashmap::test1] *)
+(** [hashmap_main::hashmap::test1]: forward function *)
Definition hashmap_test1_fwd (n : nat) : result unit :=
hm <- hashmap_hash_map_new_fwd u64 n;
hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm 0%usize 42%u64;
@@ -636,7 +645,7 @@ Definition hashmap_test1_fwd (n : nat) : result unit :=
end))
.
-(** [hashmap_main::insert_on_disk] *)
+(** [hashmap_main::insert_on_disk]: forward function *)
Definition insert_on_disk_fwd
(n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) :=
p <- hashmap_utils_deserialize_fwd st;
@@ -647,7 +656,7 @@ Definition insert_on_disk_fwd
Return (st1, tt)
.
-(** [hashmap_main::main] *)
+(** [hashmap_main::main]: forward function *)
Definition main_fwd : result unit :=
Return tt.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
index 6152b94b..1ad9c697 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
@@ -1,5 +1,5 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: opaque function definitions *)
+(** [hashmap_main]: external function declarations *)
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
@@ -8,12 +8,12 @@ Require Export HashmapMain_Types.
Import HashmapMain_Types.
Module HashmapMain_Opaque.
-(** [hashmap_main::hashmap_utils::deserialize] *)
+(** [hashmap_main::hashmap_utils::deserialize]: forward function *)
Axiom hashmap_utils_deserialize_fwd
: state -> result (state * (Hashmap_hash_map_t u64))
.
-(** [hashmap_main::hashmap_utils::serialize] *)
+(** [hashmap_main::hashmap_utils::serialize]: forward function *)
Axiom hashmap_utils_serialize_fwd
: Hashmap_hash_map_t u64 -> state -> result (state * unit)
.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 07:10:28 +0000