diff options
author | Son Ho | 2023-01-07 16:47:33 +0100 |
---|---|---|
committer | Son HO | 2023-02-03 11:21:46 +0100 |
commit | f8b7206e0d92aa33812047c521a3c2278fdb6327 (patch) | |
tree | 2f7a37aa85200f5757d0c9fa9d9bd46ae6c6fcff /tests/coq | |
parent | 9a94302823e07c4e8a50ea4e67c8f61e8827c23c (diff) |
Improve the heuristic to find pretty names for the variables in the loops
Diffstat (limited to '')
-rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 81 | ||||
-rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 84 | ||||
-rw-r--r-- | tests/coq/misc/Loops.v | 138 |
3 files changed, 153 insertions, 150 deletions
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 diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 9ae7942c..2a8ab5b5 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -15,7 +15,7 @@ Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k. (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) Fixpoint hashmap_hash_map_allocate_slots_loop_fwd - (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (n0 : usize) : + (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) : result (vec (Hashmap_list_t T)) := match n with @@ -23,10 +23,10 @@ Fixpoint hashmap_hash_map_allocate_slots_loop_fwd | S n1 => if n0 s> 0%usize then ( - slots <- vec_push_back (Hashmap_list_t T) v HashmapListNil; + slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil; n2 <- usize_sub n0 1%usize; - hashmap_hash_map_allocate_slots_loop_fwd T n1 slots n2) - else Return v + hashmap_hash_map_allocate_slots_loop_fwd T n1 slots0 n2) + else Return slots end . @@ -60,19 +60,19 @@ Definition hashmap_hash_map_new_fwd (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back - (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (i : usize) : + (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) : result (vec (Hashmap_list_t T)) := match n with | O => Fail_ OutOfFuel | S n0 => - let i0 := vec_len (Hashmap_list_t T) v in + let i0 := vec_len (Hashmap_list_t T) slots in if i s< i0 then ( i1 <- usize_add i 1%usize; - slots <- vec_index_mut_back (Hashmap_list_t T) v i HashmapListNil; - hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots i1) - else Return v + slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil; + hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots0 i1) + else Return slots end . @@ -192,7 +192,8 @@ Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back - (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (ls : Hashmap_list_t T) : + (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T) + : result (Hashmap_hash_map_t T) := match n with @@ -200,9 +201,9 @@ Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back | S n0 => match ls with | HashmapListCons k v tl => - ntable <- hashmap_hash_map_insert_no_resize_fwd_back T n0 hm k v; - hashmap_hash_map_move_elements_from_list_loop_fwd_back T n0 ntable tl - | HashmapListNil => Return hm + ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 ntable k v; + hashmap_hash_map_move_elements_from_list_loop_fwd_back T n0 ntable0 tl + | HashmapListNil => Return ntable end end . @@ -218,24 +219,25 @@ Definition hashmap_hash_map_move_elements_from_list_fwd_back (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) Fixpoint hashmap_hash_map_move_elements_loop_fwd_back - (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (v : vec (Hashmap_list_t T)) - (i : usize) : + (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) + (slots : vec (Hashmap_list_t T)) (i : usize) : result ((Hashmap_hash_map_t T) * (vec (Hashmap_list_t T))) := match n with | O => Fail_ OutOfFuel | S n0 => - let i0 := vec_len (Hashmap_list_t T) v in + let i0 := vec_len (Hashmap_list_t T) slots in if i s< i0 then ( - l <- vec_index_mut_fwd (Hashmap_list_t T) v i; + l <- vec_index_mut_fwd (Hashmap_list_t T) slots i; let ls := mem_replace_fwd (Hashmap_list_t T) l HashmapListNil in - ntable <- hashmap_hash_map_move_elements_from_list_fwd_back T n0 hm ls; + ntable0 <- + hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable ls; i1 <- usize_add i 1%usize; let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in - slots <- vec_index_mut_back (Hashmap_list_t T) v i l0; - hashmap_hash_map_move_elements_loop_fwd_back T n0 ntable slots i1) - else Return (hm, v) + slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0; + hashmap_hash_map_move_elements_loop_fwd_back T n0 ntable0 slots0 i1) + else Return (ntable, slots) end . @@ -288,15 +290,15 @@ Definition hashmap_hash_map_insert_fwd_back (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd - (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result bool := + (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | HashmapListCons ckey t tl => - if ckey s= i + if ckey s= key then Return true - else hashmap_hash_map_contains_key_in_list_loop_fwd T n0 i tl + else hashmap_hash_map_contains_key_in_list_loop_fwd T n0 key tl | HashmapListNil => Return false end end @@ -322,15 +324,15 @@ Definition hashmap_hash_map_contains_key_fwd (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) Fixpoint hashmap_hash_map_get_in_list_loop_fwd - (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T := + (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | HashmapListCons ckey cvalue tl => - if ckey s= i + if ckey s= key then Return cvalue - else hashmap_hash_map_get_in_list_loop_fwd T n0 i tl + else hashmap_hash_map_get_in_list_loop_fwd T n0 key tl | HashmapListNil => Fail_ Failure end end @@ -356,15 +358,15 @@ Definition hashmap_hash_map_get_fwd (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd - (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T := + (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | HashmapListCons ckey cvalue tl => - if ckey s= i + if ckey s= key then Return cvalue - else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 i tl + else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 key tl | HashmapListNil => Fail_ Failure end end @@ -378,7 +380,7 @@ Definition hashmap_hash_map_get_mut_in_list_fwd (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hashmap_hash_map_get_mut_in_list_loop_back - (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) (ret : T) : + (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) : result (Hashmap_list_t T) := match n with @@ -386,10 +388,10 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back | S n0 => match ls with | HashmapListCons ckey cvalue tl => - if ckey s= i + if ckey s= key then Return (HashmapListCons ckey ret tl) else ( - l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 i tl ret; + l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 key tl ret; Return (HashmapListCons ckey cvalue l)) | HashmapListNil => Fail_ Failure end @@ -437,7 +439,7 @@ Definition hashmap_hash_map_get_mut_back (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) Fixpoint hashmap_hash_map_remove_from_list_loop_fwd - (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : + (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result (option T) := match n with @@ -445,16 +447,16 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_fwd | S n0 => match ls with | HashmapListCons ckey t tl => - if ckey s= i + if ckey s= key then let mv_ls := mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl) HashmapListNil in match mv_ls with - | HashmapListCons i0 cvalue tl0 => Return (Some cvalue) + | HashmapListCons i cvalue tl0 => Return (Some cvalue) | HashmapListNil => Fail_ Failure end - else hashmap_hash_map_remove_from_list_loop_fwd T n0 i tl + else hashmap_hash_map_remove_from_list_loop_fwd T n0 key tl | HashmapListNil => Return None end end @@ -470,7 +472,7 @@ Definition hashmap_hash_map_remove_from_list_fwd (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) Fixpoint hashmap_hash_map_remove_from_list_loop_back - (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : + (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result (Hashmap_list_t T) := match n with @@ -478,17 +480,17 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_back | S n0 => match ls with | HashmapListCons ckey t tl => - if ckey s= i + if ckey s= key then let mv_ls := mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl) HashmapListNil in match mv_ls with - | HashmapListCons i0 cvalue tl0 => Return tl0 + | HashmapListCons i cvalue tl0 => Return tl0 | HashmapListNil => Fail_ Failure end else ( - l <- hashmap_hash_map_remove_from_list_loop_back T n0 i tl; + l <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl; Return (HashmapListCons ckey t l)) | HashmapListNil => Return HashmapListNil end diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 22c2fd19..4fbb7da0 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -94,13 +94,13 @@ Arguments ListNil {T}. (** [loops::list_mem] *) Fixpoint list_mem_loop_fwd - (n : nat) (i : u32) (ls : List_t u32) : result bool := + (n : nat) (x : u32) (ls : List_t u32) : result bool := match n with | O => Fail_ OutOfFuel | S n0 => match ls with | ListCons y tl => - if y s= i then Return true else list_mem_loop_fwd n0 i tl + if y s= x then Return true else list_mem_loop_fwd n0 x tl | ListNil => Return false end end @@ -235,16 +235,16 @@ Definition get_elem_mut_back (** [loops::get_elem_shared] *) Fixpoint get_elem_shared_loop_fwd - (n : nat) (x : usize) (v : vec (List_t usize)) (l : List_t usize) - (ls : List_t usize) : + (n : nat) (x : usize) (slots : vec (List_t usize)) (ls : List_t usize) + (ls0 : List_t usize) : result usize := match n with | O => Fail_ OutOfFuel | S n0 => - match ls with + match ls0 with | ListCons y tl => - if y s= x then Return y else get_elem_shared_loop_fwd n0 x v l tl + if y s= x then Return y else get_elem_shared_loop_fwd n0 x slots ls tl | ListNil => Fail_ Failure end end @@ -329,17 +329,17 @@ Definition list_nth_mut_loop_with_id_back (** [loops::list_nth_shared_loop_with_id] *) Fixpoint list_nth_shared_loop_with_id_loop_fwd - (T : Type) (n : nat) (l : List_t T) (i : u32) (ls : List_t T) : result T := + (T : Type) (n : nat) (ls : List_t T) (i : u32) (ls0 : List_t T) : result T := match n with | O => Fail_ OutOfFuel | S n0 => - match ls with + match ls0 with | ListCons x tl => if i s= 0%u32 then Return x else ( i0 <- u32_sub i 1%u32; - list_nth_shared_loop_with_id_loop_fwd T n0 l i0 tl) + list_nth_shared_loop_with_id_loop_fwd T n0 ls i0 tl) | ListNil => Fail_ Failure end end @@ -353,15 +353,15 @@ Definition list_nth_shared_loop_with_id_fwd (** [loops::list_nth_mut_loop_pair] *) Fixpoint list_nth_mut_loop_pair_loop_fwd - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (x0, x1) @@ -385,22 +385,22 @@ Definition list_nth_mut_loop_pair_fwd (** [loops::list_nth_mut_loop_pair] *) Fixpoint list_nth_mut_loop_pair_loop_back'a - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (ListCons ret tl0) else ( i0 <- u32_sub i 1%u32; - l1 <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret; - Return (ListCons x0 l1)) + l <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret; + Return (ListCons x0 l)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -418,22 +418,22 @@ Definition list_nth_mut_loop_pair_back'a (** [loops::list_nth_mut_loop_pair] *) Fixpoint list_nth_mut_loop_pair_loop_back'b - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (ListCons ret tl1) else ( i0 <- u32_sub i 1%u32; - l1 <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret; - Return (ListCons x1 l1)) + l <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret; + Return (ListCons x1 l)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -451,15 +451,15 @@ Definition list_nth_mut_loop_pair_back'b (** [loops::list_nth_shared_loop_pair] *) Fixpoint list_nth_shared_loop_pair_loop_fwd - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (x0, x1) @@ -483,15 +483,15 @@ Definition list_nth_shared_loop_pair_fwd (** [loops::list_nth_mut_loop_pair_merge] *) Fixpoint list_nth_mut_loop_pair_merge_loop_fwd - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (x0, x1) @@ -515,24 +515,24 @@ Definition list_nth_mut_loop_pair_merge_fwd (** [loops::list_nth_mut_loop_pair_merge] *) Fixpoint list_nth_mut_loop_pair_merge_loop_back - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : (T * T)) - : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) + (ret : (T * T)) : result ((List_t T) * (List_t T)) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then let (t, t0) := ret in Return (ListCons t tl0, ListCons t0 tl1) else ( i0 <- u32_sub i 1%u32; p <- list_nth_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; - let (l1, l2) := p in - Return (ListCons x0 l1, ListCons x1 l2)) + let (l, l0) := p in + Return (ListCons x0 l, ListCons x1 l0)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -551,15 +551,15 @@ Definition list_nth_mut_loop_pair_merge_back (** [loops::list_nth_shared_loop_pair_merge] *) Fixpoint list_nth_shared_loop_pair_merge_loop_fwd - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (x0, x1) @@ -583,15 +583,15 @@ Definition list_nth_shared_loop_pair_merge_fwd (** [loops::list_nth_mut_shared_loop_pair] *) Fixpoint list_nth_mut_shared_loop_pair_loop_fwd - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (x0, x1) @@ -615,22 +615,22 @@ Definition list_nth_mut_shared_loop_pair_fwd (** [loops::list_nth_mut_shared_loop_pair] *) Fixpoint list_nth_mut_shared_loop_pair_loop_back - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (ListCons ret tl0) else ( i0 <- u32_sub i 1%u32; - l1 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x0 l1)) + l <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret; + Return (ListCons x0 l)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -648,15 +648,15 @@ Definition list_nth_mut_shared_loop_pair_back (** [loops::list_nth_mut_shared_loop_pair_merge] *) Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (x0, x1) @@ -680,23 +680,23 @@ Definition list_nth_mut_shared_loop_pair_merge_fwd (** [loops::list_nth_mut_shared_loop_pair_merge] *) Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (ListCons ret tl0) else ( i0 <- u32_sub i 1%u32; - l1 <- + l <- list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x0 l1)) + Return (ListCons x0 l)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -714,15 +714,15 @@ Definition list_nth_mut_shared_loop_pair_merge_back (** [loops::list_nth_shared_mut_loop_pair] *) Fixpoint list_nth_shared_mut_loop_pair_loop_fwd - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (x0, x1) @@ -746,22 +746,22 @@ Definition list_nth_shared_mut_loop_pair_fwd (** [loops::list_nth_shared_mut_loop_pair] *) Fixpoint list_nth_shared_mut_loop_pair_loop_back - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (ListCons ret tl1) else ( i0 <- u32_sub i 1%u32; - l1 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x1 l1)) + l <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret; + Return (ListCons x1 l)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure @@ -779,15 +779,15 @@ Definition list_nth_shared_mut_loop_pair_back (** [loops::list_nth_shared_mut_loop_pair_merge] *) Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (x0, x1) @@ -811,23 +811,23 @@ Definition list_nth_shared_mut_loop_pair_merge_fwd (** [loops::list_nth_shared_mut_loop_pair_merge] *) Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back - (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) : + (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) := match n with | O => Fail_ OutOfFuel | S n0 => - match l with + match ls0 with | ListCons x0 tl0 => - match l0 with + match ls1 with | ListCons x1 tl1 => if i s= 0%u32 then Return (ListCons ret tl1) else ( i0 <- u32_sub i 1%u32; - l1 <- + l <- list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret; - Return (ListCons x1 l1)) + Return (ListCons x1 l)) | ListNil => Fail_ Failure end | ListNil => Fail_ Failure |