From f8b7206e0d92aa33812047c521a3c2278fdb6327 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sat, 7 Jan 2023 16:47:33 +0100 Subject: Improve the heuristic to find pretty names for the variables in the loops --- tests/coq/hashmap/Hashmap_Funs.v | 81 ++++++++++++++++++++-------------------- 1 file changed, 41 insertions(+), 40 deletions(-) (limited to 'tests/coq/hashmap') diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 5ec021d1..1cbff379 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -13,7 +13,7 @@ Definition hash_key_fwd (k : usize) : result usize := Return k. (** [hashmap::HashMap::{0}::allocate_slots] *) Fixpoint hash_map_allocate_slots_loop_fwd - (T : Type) (n : nat) (v : vec (List_t T)) (n0 : usize) : + (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) : result (vec (List_t T)) := match n with @@ -21,10 +21,10 @@ Fixpoint hash_map_allocate_slots_loop_fwd | S n1 => if n0 s> 0%usize then ( - slots <- vec_push_back (List_t T) v ListNil; + slots0 <- vec_push_back (List_t T) slots ListNil; n2 <- usize_sub n0 1%usize; - hash_map_allocate_slots_loop_fwd T n1 slots n2) - else Return v + hash_map_allocate_slots_loop_fwd T n1 slots0 n2) + else Return slots end . @@ -57,19 +57,19 @@ Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) := (** [hashmap::HashMap::{0}::clear_slots] *) Fixpoint hash_map_clear_slots_loop_fwd_back - (T : Type) (n : nat) (v : vec (List_t T)) (i : usize) : + (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) : result (vec (List_t T)) := match n with | O => Fail_ OutOfFuel | S n0 => - let i0 := vec_len (List_t T) v in + let i0 := vec_len (List_t T) slots in if i s< i0 then ( i1 <- usize_add i 1%usize; - slots <- vec_index_mut_back (List_t T) v i ListNil; - hash_map_clear_slots_loop_fwd_back T n0 slots i1) - else Return v + slots0 <- vec_index_mut_back (List_t T) slots i ListNil; + hash_map_clear_slots_loop_fwd_back T n0 slots0 i1) + else Return slots end . @@ -176,7 +176,7 @@ Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. (** [hashmap::HashMap::{0}::move_elements_from_list] *) Fixpoint hash_map_move_elements_from_list_loop_fwd_back - (T : Type) (n : nat) (hm : Hash_map_t T) (ls : List_t T) : + (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) : result (Hash_map_t T) := match n with @@ -184,9 +184,9 @@ Fixpoint hash_map_move_elements_from_list_loop_fwd_back | S n0 => match ls with | ListCons k v tl => - ntable <- hash_map_insert_no_resize_fwd_back T n0 hm k v; - hash_map_move_elements_from_list_loop_fwd_back T n0 ntable tl - | ListNil => Return hm + ntable0 <- hash_map_insert_no_resize_fwd_back T n0 ntable k v; + hash_map_move_elements_from_list_loop_fwd_back T n0 ntable0 tl + | ListNil => Return ntable end end . @@ -201,23 +201,24 @@ Definition hash_map_move_elements_from_list_fwd_back (** [hashmap::HashMap::{0}::move_elements] *) Fixpoint hash_map_move_elements_loop_fwd_back - (T : Type) (n : nat) (hm : Hash_map_t T) (v : vec (List_t T)) (i : usize) : + (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T)) + (i : usize) : result ((Hash_map_t T) * (vec (List_t T))) := match n with | O => Fail_ OutOfFuel | S n0 => - let i0 := vec_len (List_t T) v in + let i0 := vec_len (List_t T) slots in if i s< i0 then ( - l <- vec_index_mut_fwd (List_t T) v i; + l <- vec_index_mut_fwd (List_t T) slots i; let ls := mem_replace_fwd (List_t T) l ListNil in - ntable <- hash_map_move_elements_from_list_fwd_back T n0 hm ls; + ntable0 <- hash_map_move_elements_from_list_fwd_back T n0 ntable ls; i1 <- usize_add i 1%usize; let l0 := mem_replace_back (List_t T) l ListNil in - slots <- vec_index_mut_back (List_t T) v i l0; - hash_map_move_elements_loop_fwd_back T n0 ntable slots i1) - else Return (hm, v) + slots0 <- vec_index_mut_back (List_t T) slots i l0; + hash_map_move_elements_loop_fwd_back T n0 ntable0 slots0 i1) + else Return (ntable, slots) end . @@ -267,15 +268,15 @@ Definition hash_map_insert_fwd_back (** [hashmap::HashMap::{0}::contains_key_in_list] *) Fixpoint hash_map_contains_key_in_list_loop_fwd - (T : Type) (n : nat) (i : usize) (ls : List_t T) : result bool := + (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | ListCons ckey t tl => - if ckey s= i + if ckey s= key then Return true - else hash_map_contains_key_in_list_loop_fwd T n0 i tl + else hash_map_contains_key_in_list_loop_fwd T n0 key tl | ListNil => Return false end end @@ -299,15 +300,15 @@ Definition hash_map_contains_key_fwd (** [hashmap::HashMap::{0}::get_in_list] *) Fixpoint hash_map_get_in_list_loop_fwd - (T : Type) (n : nat) (i : usize) (ls : List_t T) : result T := + (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | ListCons ckey cvalue tl => - if ckey s= i + if ckey s= key then Return cvalue - else hash_map_get_in_list_loop_fwd T n0 i tl + else hash_map_get_in_list_loop_fwd T n0 key tl | ListNil => Fail_ Failure end end @@ -331,15 +332,15 @@ Definition hash_map_get_fwd (** [hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hash_map_get_mut_in_list_loop_fwd - (T : Type) (n : nat) (i : usize) (ls : List_t T) : result T := + (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | ListCons ckey cvalue tl => - if ckey s= i + if ckey s= key then Return cvalue - else hash_map_get_mut_in_list_loop_fwd T n0 i tl + else hash_map_get_mut_in_list_loop_fwd T n0 key tl | ListNil => Fail_ Failure end end @@ -353,7 +354,7 @@ Definition hash_map_get_mut_in_list_fwd (** [hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hash_map_get_mut_in_list_loop_back - (T : Type) (n : nat) (i : usize) (ls : List_t T) (ret : T) : + (T : Type) (n : nat) (key : usize) (ls : List_t T) (ret : T) : result (List_t T) := match n with @@ -361,10 +362,10 @@ Fixpoint hash_map_get_mut_in_list_loop_back | S n0 => match ls with | ListCons ckey cvalue tl => - if ckey s= i + if ckey s= key then Return (ListCons ckey ret tl) else ( - l <- hash_map_get_mut_in_list_loop_back T n0 i tl ret; + l <- hash_map_get_mut_in_list_loop_back T n0 key tl ret; Return (ListCons ckey cvalue l)) | ListNil => Fail_ Failure end @@ -406,20 +407,20 @@ Definition hash_map_get_mut_back (** [hashmap::HashMap::{0}::remove_from_list] *) Fixpoint hash_map_remove_from_list_loop_fwd - (T : Type) (n : nat) (i : usize) (ls : List_t T) : result (option T) := + (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | ListCons ckey t tl => - if ckey s= i + if ckey s= key then let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in match mv_ls with - | ListCons i0 cvalue tl0 => Return (Some cvalue) + | ListCons i cvalue tl0 => Return (Some cvalue) | ListNil => Fail_ Failure end - else hash_map_remove_from_list_loop_fwd T n0 i tl + else hash_map_remove_from_list_loop_fwd T n0 key tl | ListNil => Return None end end @@ -433,21 +434,21 @@ Definition hash_map_remove_from_list_fwd (** [hashmap::HashMap::{0}::remove_from_list] *) Fixpoint hash_map_remove_from_list_loop_back - (T : Type) (n : nat) (i : usize) (ls : List_t T) : result (List_t T) := + (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | ListCons ckey t tl => - if ckey s= i + if ckey s= key then let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in match mv_ls with - | ListCons i0 cvalue tl0 => Return tl0 + | ListCons i cvalue tl0 => Return tl0 | ListNil => Fail_ Failure end else ( - l <- hash_map_remove_from_list_loop_back T n0 i tl; + l <- hash_map_remove_from_list_loop_back T n0 key tl; Return (ListCons ckey t l)) | ListNil => Return ListNil end -- cgit v1.2.3