summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap
diff options
context:
space:
mode:
authorSon HO2024-04-04 14:31:03 +0200
committerGitHub2024-04-04 14:31:03 +0200
commitb4f5719a10427dfc168f1210b05397599e761f9a (patch)
tree55906070f19df2a3185250df2aef36f47669842a /tests/coq/hashmap
parent88cb18c614819f4abba1e0dfdb80c455d334d595 (diff)
parent0c3be2a82205d2737546c7ce8b15b6ad07f34095 (diff)
Merge pull request #111 from AeneasVerif/son/names
Improve the names used for the variables in the generated code
Diffstat (limited to '')
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v30
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v29
2 files changed, 29 insertions, 30 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index d709a8d5..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
@@ -376,15 +376,15 @@ Fixpoint hashMap_get_mut_in_list_loop
| List_Cons ckey cvalue tl =>
if ckey s= key
then
- let back_'a := fun (ret : T) => Return (List_Cons ckey ret tl) in
- Return (cvalue, back_'a)
+ let back := fun (ret : T) => Return (List_Cons ckey ret tl) in
+ Return (cvalue, back)
else (
p <- hashMap_get_mut_in_list_loop T n1 tl key;
- let (t, back_'a) := p in
- let back_'a1 :=
- fun (ret : T) =>
- tl1 <- back_'a ret; Return (List_Cons ckey cvalue tl1) in
- Return (t, back_'a1))
+ let (t, back) := p in
+ let back1 :=
+ fun (ret : T) => tl1 <- back ret; Return (List_Cons ckey cvalue tl1)
+ in
+ Return (t, back1))
| List_Nil => Fail_ Failure
end
end
@@ -415,7 +415,7 @@ Definition hashMap_get_mut
let (l, index_mut_back) := p in
p1 <- hashMap_get_mut_in_list T n l key;
let (t, get_mut_in_list_back) := p1 in
- let back_'a :=
+ let back :=
fun (ret : T) =>
l1 <- get_mut_in_list_back ret;
v <- index_mut_back l1;
@@ -426,7 +426,7 @@ Definition hashMap_get_mut
hashMap_max_load := self.(hashMap_max_load);
hashMap_slots := v
|} in
- Return (t, back_'a)
+ Return (t, back)
.
(** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
@@ -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 9fb3c482..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
@@ -398,16 +398,15 @@ Fixpoint hashmap_HashMap_get_mut_in_list_loop
| Hashmap_List_Cons ckey cvalue tl =>
if ckey s= key
then
- let back_'a := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl)
- in
- Return (cvalue, back_'a)
+ let back := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl) in
+ Return (cvalue, back)
else (
p <- hashmap_HashMap_get_mut_in_list_loop T n1 tl key;
- let (t, back_'a) := p in
- let back_'a1 :=
+ let (t, back) := p in
+ let back1 :=
fun (ret : T) =>
- tl1 <- back_'a ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
- Return (t, back_'a1))
+ tl1 <- back ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
+ Return (t, back1))
| Hashmap_List_Nil => Fail_ Failure
end
end
@@ -438,7 +437,7 @@ Definition hashmap_HashMap_get_mut
let (l, index_mut_back) := p in
p1 <- hashmap_HashMap_get_mut_in_list T n l key;
let (t, get_mut_in_list_back) := p1 in
- let back_'a :=
+ let back :=
fun (ret : T) =>
l1 <- get_mut_in_list_back ret;
v <- index_mut_back l1;
@@ -450,7 +449,7 @@ Definition hashmap_HashMap_get_mut
hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load);
hashmap_HashMap_slots := v
|} in
- Return (t, back_'a)
+ Return (t, back)
.
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
@@ -475,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