diff options
author | Son HO | 2024-04-04 14:31:03 +0200 |
---|---|---|
committer | GitHub | 2024-04-04 14:31:03 +0200 |
commit | b4f5719a10427dfc168f1210b05397599e761f9a (patch) | |
tree | 55906070f19df2a3185250df2aef36f47669842a /tests/coq/hashmap | |
parent | 88cb18c614819f4abba1e0dfdb80c455d334d595 (diff) | |
parent | 0c3be2a82205d2737546c7ce8b15b6ad07f34095 (diff) |
Merge pull request #111 from AeneasVerif/son/names
Improve the names used for the variables in the generated code
Diffstat (limited to 'tests/coq/hashmap')
-rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 30 |
1 files changed, 15 insertions, 15 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 |