summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v12
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v12
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst12
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst12
-rw-r--r--tests/lean/Hashmap/Funs.lean12
-rw-r--r--tests/lean/HashmapMain/Funs.lean12
6 files changed, 36 insertions, 36 deletions
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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::remove_from_list]:
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 19:34:05 +0000