From e69382acbcc4bdd27612c9cf8ec282db71f8408d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 13 Jan 2023 16:18:43 +0100 Subject: Improve the pretty names generation for loops --- tests/coq/hashmap/Hashmap_Funs.v | 12 ++++----- tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 12 ++++----- tests/coq/misc/Loops.v | 38 ++++++++++++++-------------- 3 files changed, 31 insertions(+), 31 deletions(-) (limited to 'tests/coq') diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 9c65fb46..0d55b171 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -131,8 +131,8 @@ Fixpoint hash_map_insert_in_list_loop_back if ckey s= key then Return (ListCons ckey value tl) else ( - l <- hash_map_insert_in_list_loop_back T n0 key value tl; - Return (ListCons ckey cvalue l)) + tl0 <- hash_map_insert_in_list_loop_back T n0 key value tl; + Return (ListCons ckey cvalue tl0)) | ListNil => let l := ListNil in Return (ListCons key value l) end end @@ -365,8 +365,8 @@ Fixpoint hash_map_get_mut_in_list_loop_back if ckey s= key then Return (ListCons ckey ret tl) else ( - l <- hash_map_get_mut_in_list_loop_back T n0 tl key ret; - Return (ListCons ckey cvalue l)) + tl0 <- hash_map_get_mut_in_list_loop_back T n0 tl key ret; + Return (ListCons ckey cvalue tl0)) | ListNil => Fail_ Failure end end @@ -448,8 +448,8 @@ Fixpoint hash_map_remove_from_list_loop_back | ListNil => Fail_ Failure end else ( - l <- hash_map_remove_from_list_loop_back T n0 key tl; - Return (ListCons ckey t l)) + tl0 <- hash_map_remove_from_list_loop_back T n0 key tl; + Return (ListCons ckey t tl0)) | ListNil => Return ListNil end end diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 94a9e6a5..670e527a 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -139,8 +139,8 @@ Fixpoint hashmap_hash_map_insert_in_list_loop_back if ckey s= key then Return (HashmapListCons ckey value tl) else ( - l <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl; - Return (HashmapListCons ckey cvalue l)) + tl0 <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl; + Return (HashmapListCons ckey cvalue tl0)) | HashmapListNil => let l := HashmapListNil in Return (HashmapListCons key value l) end @@ -391,8 +391,8 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back if ckey s= key then Return (HashmapListCons ckey ret tl) else ( - l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret; - Return (HashmapListCons ckey cvalue l)) + tl0 <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret; + Return (HashmapListCons ckey cvalue tl0)) | HashmapListNil => Fail_ Failure end end @@ -490,8 +490,8 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_back | HashmapListNil => Fail_ Failure end else ( - l <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl; - Return (HashmapListCons ckey t l)) + tl0 <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl; + Return (HashmapListCons ckey t tl0)) | HashmapListNil => Return HashmapListNil end end diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index ec77e4dd..bcbfc8df 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -147,8 +147,8 @@ Fixpoint list_nth_mut_loop_loop_back then Return (ListCons ret tl) else ( i0 <- u32_sub i 1%u32; - l <- list_nth_mut_loop_loop_back T n0 tl i0 ret; - Return (ListCons x l)) + tl0 <- list_nth_mut_loop_loop_back T n0 tl i0 ret; + Return (ListCons x tl0)) | ListNil => Fail_ Failure end end @@ -217,7 +217,7 @@ Fixpoint get_elem_mut_loop_back | ListCons y tl => if y s= x then Return (ListCons ret tl) - else (l <- get_elem_mut_loop_back n0 x tl ret; Return (ListCons y l)) + else (tl0 <- get_elem_mut_loop_back n0 x tl ret; Return (ListCons y tl0)) | ListNil => Fail_ Failure end end @@ -307,8 +307,8 @@ Fixpoint list_nth_mut_loop_with_id_loop_back then Return (ListCons ret tl) else ( i0 <- u32_sub i 1%u32; - l <- list_nth_mut_loop_with_id_loop_back T n0 i0 tl ret; - Return (ListCons x l)) + tl0 <- list_nth_mut_loop_with_id_loop_back T n0 i0 tl ret; + Return (ListCons x tl0)) | ListNil => Fail_ Failure end end @@ -395,8 +395,8 @@ Fixpoint list_nth_mut_loop_pair_loop_back'a then Return (ListCons ret tl0) else ( i0 <- u32_sub i 1%u32; - l <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret; - Return (ListCons x0 l)) + tl00 <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret; + Return (ListCons x0 tl00)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -428,8 +428,8 @@ Fixpoint list_nth_mut_loop_pair_loop_back'b then Return (ListCons ret tl1) else ( i0 <- u32_sub i 1%u32; - l <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret; - Return (ListCons x1 l)) + tl10 <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret; + Return (ListCons x1 tl10)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -527,8 +527,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_back else ( i0 <- u32_sub i 1%u32; p <- list_nth_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; - let (l, l0) := p in - Return (ListCons x0 l, ListCons x1 l0)) + let (tl00, tl10) := p in + Return (ListCons x0 tl00, ListCons x1 tl10)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -625,8 +625,8 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_back then Return (ListCons ret tl0) else ( i0 <- u32_sub i 1%u32; - l <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x0 l)) + tl00 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret; + Return (ListCons x0 tl00)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -690,9 +690,9 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back then Return (ListCons ret tl0) else ( i0 <- u32_sub i 1%u32; - l <- + tl00 <- list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x0 l)) + Return (ListCons x0 tl00)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -756,8 +756,8 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_back then Return (ListCons ret tl1) else ( i0 <- u32_sub i 1%u32; - l <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x1 l)) + tl10 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret; + Return (ListCons x1 tl10)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -821,9 +821,9 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back then Return (ListCons ret tl1) else ( i0 <- u32_sub i 1%u32; - l <- + tl10 <- list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x1 l)) + Return (ListCons x1 tl10)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure -- cgit v1.2.3