From 25973ee8ef28e2d5b8a9b9ec3de4d6ff340db18b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 14:41:00 +0200 Subject: Tweak a path --- tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 64 +++++++++++----------- .../HashmapMain_FunsExternal_Template.v | 4 +- tests/coq/hashmap_on_disk/HashmapMain_Types.v | 4 +- 3 files changed, 36 insertions(+), 36 deletions(-) (limited to 'tests/coq/hashmap_on_disk') diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 79da6e80..facd84ea 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -13,12 +13,12 @@ Include HashmapMain_FunsExternal. Module HashmapMain_Funs. (** [hashmap_main::hashmap::hash_key]: - Source: 'src/hashmap.rs', lines 27:0-27:32 *) + Source: 'tests/src/hashmap.rs', lines 27:0-27:32 *) Definition hashmap_hash_key (k : usize) : result usize := Ok k. (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: loop 0: - Source: 'src/hashmap.rs', lines 50:4-56:5 *) + Source: 'tests/src/hashmap.rs', lines 50:4-56:5 *) Fixpoint hashmap_HashMap_allocate_slots_loop (T : Type) (n : nat) (slots : alloc_vec_Vec (hashmap_List_t T)) (n1 : usize) : @@ -37,7 +37,7 @@ Fixpoint hashmap_HashMap_allocate_slots_loop . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: - Source: 'src/hashmap.rs', lines 50:4-50:76 *) + Source: 'tests/src/hashmap.rs', lines 50:4-50:76 *) Definition hashmap_HashMap_allocate_slots (T : Type) (n : nat) (slots : alloc_vec_Vec (hashmap_List_t T)) (n1 : usize) : @@ -47,7 +47,7 @@ Definition hashmap_HashMap_allocate_slots . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new_with_capacity]: - Source: 'src/hashmap.rs', lines 59:4-63:13 *) + Source: 'tests/src/hashmap.rs', lines 59:4-63:13 *) Definition hashmap_HashMap_new_with_capacity (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : @@ -68,14 +68,14 @@ Definition hashmap_HashMap_new_with_capacity . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new]: - Source: 'src/hashmap.rs', lines 75:4-75:24 *) + Source: 'tests/src/hashmap.rs', lines 75:4-75:24 *) Definition hashmap_HashMap_new (T : Type) (n : nat) : result (hashmap_HashMap_t T) := hashmap_HashMap_new_with_capacity T n 32%usize 4%usize 5%usize . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::clear]: loop 0: - Source: 'src/hashmap.rs', lines 80:4-88:5 *) + Source: 'tests/src/hashmap.rs', lines 80:4-88:5 *) Fixpoint hashmap_HashMap_clear_loop (T : Type) (n : nat) (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : result (alloc_vec_Vec (hashmap_List_t T)) @@ -99,7 +99,7 @@ Fixpoint hashmap_HashMap_clear_loop . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::clear]: - Source: 'src/hashmap.rs', lines 80:4-80:27 *) + Source: 'tests/src/hashmap.rs', lines 80:4-80:27 *) Definition hashmap_HashMap_clear (T : Type) (n : nat) (self : hashmap_HashMap_t T) : result (hashmap_HashMap_t T) @@ -115,14 +115,14 @@ Definition hashmap_HashMap_clear . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::len]: - Source: 'src/hashmap.rs', lines 90:4-90:30 *) + Source: 'tests/src/hashmap.rs', lines 90:4-90:30 *) Definition hashmap_HashMap_len (T : Type) (self : hashmap_HashMap_t T) : result usize := Ok self.(hashmap_HashMap_num_entries) . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: loop 0: - Source: 'src/hashmap.rs', lines 97:4-114:5 *) + Source: 'tests/src/hashmap.rs', lines 97:4-114:5 *) Fixpoint hashmap_HashMap_insert_in_list_loop (T : Type) (n : nat) (key : usize) (value : T) (ls : hashmap_List_t T) : result (bool * (hashmap_List_t T)) @@ -145,7 +145,7 @@ Fixpoint hashmap_HashMap_insert_in_list_loop . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: - Source: 'src/hashmap.rs', lines 97:4-97:71 *) + Source: 'tests/src/hashmap.rs', lines 97:4-97:71 *) Definition hashmap_HashMap_insert_in_list (T : Type) (n : nat) (key : usize) (value : T) (ls : hashmap_List_t T) : result (bool * (hashmap_List_t T)) @@ -154,7 +154,7 @@ Definition hashmap_HashMap_insert_in_list . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_no_resize]: - Source: 'src/hashmap.rs', lines 117:4-117:54 *) + Source: 'tests/src/hashmap.rs', lines 117:4-117:54 *) Definition hashmap_HashMap_insert_no_resize (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) : result (hashmap_HashMap_t T) @@ -194,7 +194,7 @@ Definition hashmap_HashMap_insert_no_resize . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: loop 0: - Source: 'src/hashmap.rs', lines 183:4-196:5 *) + Source: 'tests/src/hashmap.rs', lines 183:4-196:5 *) Fixpoint hashmap_HashMap_move_elements_from_list_loop (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) (ls : hashmap_List_t T) : result (hashmap_HashMap_t T) @@ -212,7 +212,7 @@ Fixpoint hashmap_HashMap_move_elements_from_list_loop . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: - Source: 'src/hashmap.rs', lines 183:4-183:72 *) + Source: 'tests/src/hashmap.rs', lines 183:4-183:72 *) Definition hashmap_HashMap_move_elements_from_list (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) (ls : hashmap_List_t T) : result (hashmap_HashMap_t T) @@ -221,7 +221,7 @@ Definition hashmap_HashMap_move_elements_from_list . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: loop 0: - Source: 'src/hashmap.rs', lines 171:4-180:5 *) + Source: 'tests/src/hashmap.rs', lines 171:4-180:5 *) Fixpoint hashmap_HashMap_move_elements_loop (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : @@ -248,7 +248,7 @@ Fixpoint hashmap_HashMap_move_elements_loop . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: - Source: 'src/hashmap.rs', lines 171:4-171:95 *) + Source: 'tests/src/hashmap.rs', lines 171:4-171:95 *) Definition hashmap_HashMap_move_elements (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : @@ -258,7 +258,7 @@ Definition hashmap_HashMap_move_elements . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::try_resize]: - Source: 'src/hashmap.rs', lines 140:4-140:28 *) + Source: 'tests/src/hashmap.rs', lines 140:4-140:28 *) Definition hashmap_HashMap_try_resize (T : Type) (n : nat) (self : hashmap_HashMap_t T) : result (hashmap_HashMap_t T) @@ -295,7 +295,7 @@ Definition hashmap_HashMap_try_resize . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert]: - Source: 'src/hashmap.rs', lines 129:4-129:48 *) + Source: 'tests/src/hashmap.rs', lines 129:4-129:48 *) Definition hashmap_HashMap_insert (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) : result (hashmap_HashMap_t T) @@ -308,7 +308,7 @@ Definition hashmap_HashMap_insert . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: loop 0: - Source: 'src/hashmap.rs', lines 206:4-219:5 *) + Source: 'tests/src/hashmap.rs', lines 206:4-219:5 *) Fixpoint hashmap_HashMap_contains_key_in_list_loop (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result bool := match n with @@ -325,14 +325,14 @@ Fixpoint hashmap_HashMap_contains_key_in_list_loop . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: - Source: 'src/hashmap.rs', lines 206:4-206:68 *) + Source: 'tests/src/hashmap.rs', lines 206:4-206:68 *) Definition hashmap_HashMap_contains_key_in_list (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result bool := hashmap_HashMap_contains_key_in_list_loop T n key ls . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key]: - Source: 'src/hashmap.rs', lines 199:4-199:49 *) + Source: 'tests/src/hashmap.rs', lines 199:4-199:49 *) Definition hashmap_HashMap_contains_key (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : result bool @@ -348,7 +348,7 @@ Definition hashmap_HashMap_contains_key . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: loop 0: - Source: 'src/hashmap.rs', lines 224:4-237:5 *) + Source: 'tests/src/hashmap.rs', lines 224:4-237:5 *) Fixpoint hashmap_HashMap_get_in_list_loop (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result T := match n with @@ -365,14 +365,14 @@ Fixpoint hashmap_HashMap_get_in_list_loop . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: - Source: 'src/hashmap.rs', lines 224:4-224:70 *) + Source: 'tests/src/hashmap.rs', lines 224:4-224:70 *) Definition hashmap_HashMap_get_in_list (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result T := hashmap_HashMap_get_in_list_loop T n key ls . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get]: - Source: 'src/hashmap.rs', lines 239:4-239:55 *) + Source: 'tests/src/hashmap.rs', lines 239:4-239:55 *) Definition hashmap_HashMap_get (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : result T := hash <- hashmap_hash_key key; @@ -386,7 +386,7 @@ Definition hashmap_HashMap_get . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: loop 0: - Source: 'src/hashmap.rs', lines 245:4-254:5 *) + Source: 'tests/src/hashmap.rs', lines 245:4-254:5 *) Fixpoint hashmap_HashMap_get_mut_in_list_loop (T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) : result (T * (T -> result (hashmap_List_t T))) @@ -413,7 +413,7 @@ Fixpoint hashmap_HashMap_get_mut_in_list_loop . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: - Source: 'src/hashmap.rs', lines 245:4-245:86 *) + Source: 'tests/src/hashmap.rs', lines 245:4-245:86 *) Definition hashmap_HashMap_get_mut_in_list (T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) : result (T * (T -> result (hashmap_List_t T))) @@ -422,7 +422,7 @@ Definition hashmap_HashMap_get_mut_in_list . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut]: - Source: 'src/hashmap.rs', lines 257:4-257:67 *) + Source: 'tests/src/hashmap.rs', lines 257:4-257:67 *) Definition hashmap_HashMap_get_mut (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : result (T * (T -> result (hashmap_HashMap_t T))) @@ -453,7 +453,7 @@ Definition hashmap_HashMap_get_mut . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: loop 0: - Source: 'src/hashmap.rs', lines 265:4-291:5 *) + Source: 'tests/src/hashmap.rs', lines 265:4-291:5 *) Fixpoint hashmap_HashMap_remove_from_list_loop (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result ((option T) * (hashmap_List_t T)) @@ -482,7 +482,7 @@ Fixpoint hashmap_HashMap_remove_from_list_loop . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: - Source: 'src/hashmap.rs', lines 265:4-265:69 *) + Source: 'tests/src/hashmap.rs', lines 265:4-265:69 *) Definition hashmap_HashMap_remove_from_list (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result ((option T) * (hashmap_List_t T)) @@ -491,7 +491,7 @@ Definition hashmap_HashMap_remove_from_list . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove]: - Source: 'src/hashmap.rs', lines 294:4-294:52 *) + Source: 'tests/src/hashmap.rs', lines 294:4-294:52 *) Definition hashmap_HashMap_remove (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : result ((option T) * (hashmap_HashMap_t T)) @@ -532,7 +532,7 @@ Definition hashmap_HashMap_remove . (** [hashmap_main::hashmap::test1]: - Source: 'src/hashmap.rs', lines 315:0-315:10 *) + Source: 'tests/src/hashmap.rs', lines 315:0-315:10 *) Definition hashmap_test1 (n : nat) : result unit := hm <- hashmap_HashMap_new u64 n; hm1 <- hashmap_HashMap_insert u64 n hm 0%usize 42%u64; @@ -572,7 +572,7 @@ Definition hashmap_test1 (n : nat) : result unit := . (** [hashmap_main::insert_on_disk]: - Source: 'src/hashmap_main.rs', lines 7:0-7:43 *) + Source: 'tests/src/hashmap_main.rs', lines 7:0-7:43 *) Definition insert_on_disk (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) := p <- hashmap_utils_deserialize st; @@ -582,7 +582,7 @@ Definition insert_on_disk . (** [hashmap_main::main]: - Source: 'src/hashmap_main.rs', lines 16:0-16:13 *) + Source: 'tests/src/hashmap_main.rs', lines 16:0-16:13 *) Definition main : result unit := Ok tt. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v index fb2e052a..f9e3f747 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v @@ -12,13 +12,13 @@ Include HashmapMain_Types. Module HashmapMain_FunsExternal_Template. (** [hashmap_main::hashmap_utils::deserialize]: - Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *) + Source: 'tests/src/hashmap_utils.rs', lines 10:0-10:43 *) Axiom hashmap_utils_deserialize : state -> result (state * (hashmap_HashMap_t u64)) . (** [hashmap_main::hashmap_utils::serialize]: - Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *) + Source: 'tests/src/hashmap_utils.rs', lines 5:0-5:42 *) Axiom hashmap_utils_serialize : hashmap_HashMap_t u64 -> state -> result (state * unit) . diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v index 8d3d72aa..26029c9d 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v @@ -11,7 +11,7 @@ Include HashmapMain_TypesExternal. Module HashmapMain_Types. (** [hashmap_main::hashmap::List] - Source: 'src/hashmap.rs', lines 19:0-19:16 *) + Source: 'tests/src/hashmap.rs', lines 19:0-19:16 *) Inductive hashmap_List_t (T : Type) := | Hashmap_List_Cons : usize -> T -> hashmap_List_t T -> hashmap_List_t T | Hashmap_List_Nil : hashmap_List_t T @@ -21,7 +21,7 @@ Arguments Hashmap_List_Cons { _ }. Arguments Hashmap_List_Nil { _ }. (** [hashmap_main::hashmap::HashMap] - Source: 'src/hashmap.rs', lines 35:0-35:21 *) + Source: 'tests/src/hashmap.rs', lines 35:0-35:21 *) Record hashmap_HashMap_t (T : Type) := mkhashmap_HashMap_t { hashmap_HashMap_num_entries : usize; -- cgit v1.2.3