From 46f64c1b9f3bfc2703186b32a74c611e0e43f63f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 13:21:47 +0200 Subject: Regenerate the test files --- tests/coq/hashmap/Hashmap_Funs.v | 12 ++++++------ tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 12 ++++++------ tests/fstar/hashmap/Hashmap.Funs.fst | 12 ++++++------ tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 12 ++++++------ tests/lean/Hashmap/Funs.lean | 12 ++++++------ tests/lean/HashmapMain/Funs.lean | 12 ++++++------ 6 files changed, 36 insertions(+), 36 deletions(-) (limited to 'tests') diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 67543c8e..c0cde78d 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -94,13 +94,13 @@ Fixpoint hashMap_clear_loop Source: 'src/hashmap.rs', lines 80:4-80:27 *) Definition hashMap_clear (T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) := - back <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize; + hm <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize; Return {| hashMap_num_entries := 0%usize; hashMap_max_load_factor := self.(hashMap_max_load_factor); hashMap_max_load := self.(hashMap_max_load); - hashMap_slots := back + hashMap_slots := hm |} . @@ -125,8 +125,8 @@ Fixpoint hashMap_insert_in_list_loop then Return (false, List_Cons ckey value tl) else ( p <- hashMap_insert_in_list_loop T n1 key value tl; - let (b, back) := p in - Return (b, List_Cons ckey cvalue back)) + let (b, tl1) := p in + Return (b, List_Cons ckey cvalue tl1)) | List_Nil => Return (true, List_Cons key value List_Nil) end end @@ -450,8 +450,8 @@ Fixpoint hashMap_remove_from_list_loop end else ( p <- hashMap_remove_from_list_loop T n1 key tl; - let (o, back) := p in - Return (o, List_Cons ckey t back)) + let (o, tl1) := p in + Return (o, List_Cons ckey t tl1)) | List_Nil => Return (None, List_Nil) end end diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index a614e52d..8e299800 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -104,13 +104,13 @@ Definition hashmap_HashMap_clear (T : Type) (n : nat) (self : hashmap_HashMap_t T) : result (hashmap_HashMap_t T) := - back <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize; + hm <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize; Return {| hashmap_HashMap_num_entries := 0%usize; hashmap_HashMap_max_load_factor := self.(hashmap_HashMap_max_load_factor); hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); - hashmap_HashMap_slots := back + hashmap_HashMap_slots := hm |} . @@ -136,8 +136,8 @@ Fixpoint hashmap_HashMap_insert_in_list_loop then Return (false, Hashmap_List_Cons ckey value tl) else ( p <- hashmap_HashMap_insert_in_list_loop T n1 key value tl; - let (b, back) := p in - Return (b, Hashmap_List_Cons ckey cvalue back)) + let (b, tl1) := p in + Return (b, Hashmap_List_Cons ckey cvalue tl1)) | Hashmap_List_Nil => Return (true, Hashmap_List_Cons key value Hashmap_List_Nil) end @@ -474,8 +474,8 @@ Fixpoint hashmap_HashMap_remove_from_list_loop end else ( p <- hashmap_HashMap_remove_from_list_loop T n1 key tl; - let (o, back) := p in - Return (o, Hashmap_List_Cons ckey t back)) + let (o, tl1) := p in + Return (o, Hashmap_List_Cons ckey t tl1)) | Hashmap_List_Nil => Return (None, Hashmap_List_Nil) end end diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 0e770ac9..d897933a 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -79,8 +79,8 @@ let rec hashMap_clear_loop (** [hashmap::{hashmap::HashMap}::clear]: Source: 'src/hashmap.rs', lines 80:4-80:27 *) let hashMap_clear (t : Type0) (self : hashMap_t t) : result (hashMap_t t) = - let* back = hashMap_clear_loop t self.slots 0 in - Return { self with num_entries = 0; slots = back } + let* hm = hashMap_clear_loop t self.slots 0 in + Return { self with num_entries = 0; slots = hm } (** [hashmap::{hashmap::HashMap}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 *) @@ -99,8 +99,8 @@ let rec hashMap_insert_in_list_loop if ckey = key then Return (false, List_Cons ckey value tl) else - let* (b, back) = hashMap_insert_in_list_loop t key value tl in - Return (b, List_Cons ckey cvalue back) + let* (b, tl1) = hashMap_insert_in_list_loop t key value tl in + Return (b, List_Cons ckey cvalue tl1) | List_Nil -> Return (true, List_Cons key value List_Nil) end @@ -344,8 +344,8 @@ let rec hashMap_remove_from_list_loop | List_Nil -> Fail Failure end else - let* (o, back) = hashMap_remove_from_list_loop t key tl in - Return (o, List_Cons ckey x back) + let* (o, tl1) = hashMap_remove_from_list_loop t key tl in + Return (o, List_Cons ckey x tl1) | List_Nil -> Return (None, List_Nil) end diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 09928620..e0005c81 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -84,8 +84,8 @@ let rec hashmap_HashMap_clear_loop Source: 'src/hashmap.rs', lines 80:4-80:27 *) let hashmap_HashMap_clear (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) = - let* back = hashmap_HashMap_clear_loop t self.slots 0 in - Return { self with num_entries = 0; slots = back } + let* hm = hashmap_HashMap_clear_loop t self.slots 0 in + Return { self with num_entries = 0; slots = hm } (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 *) @@ -105,8 +105,8 @@ let rec hashmap_HashMap_insert_in_list_loop if ckey = key then Return (false, Hashmap_List_Cons ckey value tl) else - let* (b, back) = hashmap_HashMap_insert_in_list_loop t key value tl in - Return (b, Hashmap_List_Cons ckey cvalue back) + let* (b, tl1) = hashmap_HashMap_insert_in_list_loop t key value tl in + Return (b, Hashmap_List_Cons ckey cvalue tl1) | Hashmap_List_Nil -> Return (true, Hashmap_List_Cons key value Hashmap_List_Nil) end @@ -364,8 +364,8 @@ let rec hashmap_HashMap_remove_from_list_loop | Hashmap_List_Nil -> Fail Failure end else - let* (o, back) = hashmap_HashMap_remove_from_list_loop t key tl in - Return (o, Hashmap_List_Cons ckey x back) + let* (o, tl1) = hashmap_HashMap_remove_from_list_loop t key tl in + Return (o, Hashmap_List_Cons ckey x tl1) | Hashmap_List_Nil -> Return (None, Hashmap_List_Nil) end diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 0067538e..363d751a 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -79,8 +79,8 @@ divergent def HashMap.clear_loop Source: 'src/hashmap.rs', lines 80:4-80:27 -/ def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do - let back ← HashMap.clear_loop T self.slots 0#usize - Result.ret { self with num_entries := 0#usize, slots := back } + let hm ← HashMap.clear_loop T self.slots 0#usize + Result.ret { self with num_entries := 0#usize, slots := hm } /- [hashmap::{hashmap::HashMap}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 -/ @@ -99,8 +99,8 @@ divergent def HashMap.insert_in_list_loop then Result.ret (false, List.Cons ckey value tl) else do - let (b, back) ← HashMap.insert_in_list_loop T key value tl - Result.ret (b, List.Cons ckey cvalue back) + let (b, tl1) ← HashMap.insert_in_list_loop T key value tl + Result.ret (b, List.Cons ckey cvalue tl1) | List.Nil => Result.ret (true, List.Cons key value List.Nil) /- [hashmap::{hashmap::HashMap}::insert_in_list]: @@ -345,8 +345,8 @@ divergent def HashMap.remove_from_list_loop | List.Nil => Result.fail .panic else do - let (o, back) ← HashMap.remove_from_list_loop T key tl - Result.ret (o, List.Cons ckey t back) + let (o, tl1) ← HashMap.remove_from_list_loop T key tl + Result.ret (o, List.Cons ckey t tl1) | List.Nil => Result.ret (none, List.Nil) /- [hashmap::{hashmap::HashMap}::remove_from_list]: diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index 0bf6c641..6fac6940 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -83,8 +83,8 @@ divergent def hashmap.HashMap.clear_loop def hashmap.HashMap.clear (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do - let back ← hashmap.HashMap.clear_loop T self.slots 0#usize - Result.ret { self with num_entries := 0#usize, slots := back } + let hm ← hashmap.HashMap.clear_loop T self.slots 0#usize + Result.ret { self with num_entries := 0#usize, slots := hm } /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 -/ @@ -103,8 +103,8 @@ divergent def hashmap.HashMap.insert_in_list_loop then Result.ret (false, hashmap.List.Cons ckey value tl) else do - let (b, back) ← hashmap.HashMap.insert_in_list_loop T key value tl - Result.ret (b, hashmap.List.Cons ckey cvalue back) + let (b, tl1) ← hashmap.HashMap.insert_in_list_loop T key value tl + Result.ret (b, hashmap.List.Cons ckey cvalue tl1) | hashmap.List.Nil => Result.ret (true, hashmap.List.Cons key value hashmap.List.Nil) @@ -364,8 +364,8 @@ divergent def hashmap.HashMap.remove_from_list_loop | hashmap.List.Nil => Result.fail .panic else do - let (o, back) ← hashmap.HashMap.remove_from_list_loop T key tl - Result.ret (o, hashmap.List.Cons ckey t back) + let (o, tl1) ← hashmap.HashMap.remove_from_list_loop T key tl + Result.ret (o, hashmap.List.Cons ckey t tl1) | hashmap.List.Nil => Result.ret (none, hashmap.List.Nil) /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: -- cgit v1.2.3