diff options
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 | ||||
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Clauses.Template.fst | 26 | ||||
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 108 | ||||
-rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst | 17 | ||||
-rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 109 | ||||
-rw-r--r-- | tests/fstar/misc/Loops.Clauses.Template.fst | 42 | ||||
-rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 159 |
9 files changed, 387 insertions, 377 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 diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst index b8890f86..3e51c6f1 100644 --- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst +++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst @@ -8,14 +8,14 @@ open Hashmap.Types (** [hashmap::HashMap::{0}::allocate_slots]: decreases clause *) unfold -let hash_map_allocate_slots_decreases (t : Type0) (v : vec (list_t t)) +let hash_map_allocate_slots_decreases (t : Type0) (slots : vec (list_t t)) (n : usize) : nat = admit () (** [hashmap::HashMap::{0}::clear_slots]: decreases clause *) unfold -let hash_map_clear_slots_decreases (t : Type0) (v : vec (list_t t)) (i : usize) - : nat = +let hash_map_clear_slots_decreases (t : Type0) (slots : vec (list_t t)) + (i : usize) : nat = admit () (** [hashmap::HashMap::{0}::insert_in_list]: decreases clause *) @@ -30,37 +30,37 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body (** [hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *) unfold -let hash_map_move_elements_from_list_decreases (t : Type0) (hm : hash_map_t t) - (ls : list_t t) : nat = +let hash_map_move_elements_from_list_decreases (t : Type0) + (ntable : hash_map_t t) (ls : list_t t) : nat = admit () (** [hashmap::HashMap::{0}::move_elements]: decreases clause *) unfold -let hash_map_move_elements_decreases (t : Type0) (hm : hash_map_t t) - (v : vec (list_t t)) (i : usize) : nat = +let hash_map_move_elements_decreases (t : Type0) (ntable : hash_map_t t) + (slots : vec (list_t t)) (i : usize) : nat = admit () (** [hashmap::HashMap::{0}::contains_key_in_list]: decreases clause *) unfold -let hash_map_contains_key_in_list_decreases (t : Type0) (i : usize) +let hash_map_contains_key_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) : nat = admit () (** [hashmap::HashMap::{0}::get_in_list]: decreases clause *) unfold -let hash_map_get_in_list_decreases (t : Type0) (i : usize) (ls : list_t t) : +let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) : nat = admit () (** [hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *) unfold -let hash_map_get_mut_in_list_decreases (t : Type0) (i : usize) (ls : list_t t) - : nat = +let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize) + (ls : list_t t) : nat = admit () (** [hashmap::HashMap::{0}::remove_from_list]: decreases clause *) unfold -let hash_map_remove_from_list_decreases (t : Type0) (i : usize) (ls : list_t t) - : nat = +let hash_map_remove_from_list_decreases (t : Type0) (key : usize) + (ls : list_t t) : nat = admit () diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index d81da40b..81b253ad 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -12,21 +12,21 @@ let hash_key_fwd (k : usize) : result usize = Return k (** [hashmap::HashMap::{0}::allocate_slots] *) let rec hash_map_allocate_slots_loop_fwd - (t : Type0) (v : vec (list_t t)) (n : usize) : + (t : Type0) (slots : vec (list_t t)) (n : usize) : Tot (result (vec (list_t t))) - (decreases (hash_map_allocate_slots_decreases t v n)) + (decreases (hash_map_allocate_slots_decreases t slots n)) = if n > 0 then - begin match vec_push_back (list_t t) v ListNil with + begin match vec_push_back (list_t t) slots ListNil with | Fail e -> Fail e - | Return slots -> + | Return slots0 -> begin match usize_sub n 1 with | Fail e -> Fail e - | Return n0 -> hash_map_allocate_slots_loop_fwd t slots n0 + | Return n0 -> hash_map_allocate_slots_loop_fwd t slots0 n0 end end - else Return v + else Return slots (** [hashmap::HashMap::{0}::allocate_slots] *) let hash_map_allocate_slots_fwd @@ -60,22 +60,22 @@ let hash_map_new_fwd (t : Type0) : result (hash_map_t t) = (** [hashmap::HashMap::{0}::clear_slots] *) let rec hash_map_clear_slots_loop_fwd_back - (t : Type0) (v : vec (list_t t)) (i : usize) : + (t : Type0) (slots : vec (list_t t)) (i : usize) : Tot (result (vec (list_t t))) - (decreases (hash_map_clear_slots_decreases t v i)) + (decreases (hash_map_clear_slots_decreases t slots i)) = - let i0 = vec_len (list_t t) v in + let i0 = vec_len (list_t t) slots in if i < i0 then begin match usize_add i 1 with | Fail e -> Fail e | Return i1 -> - begin match vec_index_mut_back (list_t t) v i ListNil with + begin match vec_index_mut_back (list_t t) slots i ListNil with | Fail e -> Fail e - | Return slots -> hash_map_clear_slots_loop_fwd_back t slots i1 + | Return slots0 -> hash_map_clear_slots_loop_fwd_back t slots0 i1 end end - else Return v + else Return slots (** [hashmap::HashMap::{0}::clear_slots] *) let hash_map_clear_slots_fwd_back @@ -199,18 +199,18 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body (** [hashmap::HashMap::{0}::move_elements_from_list] *) let rec hash_map_move_elements_from_list_loop_fwd_back - (t : Type0) (hm : hash_map_t t) (ls : list_t t) : + (t : Type0) (ntable : hash_map_t t) (ls : list_t t) : Tot (result (hash_map_t t)) - (decreases (hash_map_move_elements_from_list_decreases t hm ls)) + (decreases (hash_map_move_elements_from_list_decreases t ntable ls)) = begin match ls with | ListCons k v tl -> - begin match hash_map_insert_no_resize_fwd_back t hm k v with + begin match hash_map_insert_no_resize_fwd_back t ntable k v with | Fail e -> Fail e - | Return ntable -> - hash_map_move_elements_from_list_loop_fwd_back t ntable tl + | Return ntable0 -> + hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl end - | ListNil -> Return hm + | ListNil -> Return ntable end (** [hashmap::HashMap::{0}::move_elements_from_list] *) @@ -220,33 +220,33 @@ let hash_map_move_elements_from_list_fwd_back (** [hashmap::HashMap::{0}::move_elements] *) let rec hash_map_move_elements_loop_fwd_back - (t : Type0) (hm : hash_map_t t) (v : vec (list_t t)) (i : usize) : + (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) : Tot (result ((hash_map_t t) & (vec (list_t t)))) - (decreases (hash_map_move_elements_decreases t hm v i)) + (decreases (hash_map_move_elements_decreases t ntable slots i)) = - let i0 = vec_len (list_t t) v in + let i0 = vec_len (list_t t) slots in if i < i0 then - begin match vec_index_mut_fwd (list_t t) v i with + begin match vec_index_mut_fwd (list_t t) slots i with | Fail e -> Fail e | Return l -> let ls = mem_replace_fwd (list_t t) l ListNil in - begin match hash_map_move_elements_from_list_fwd_back t hm ls with + begin match hash_map_move_elements_from_list_fwd_back t ntable ls with | Fail e -> Fail e - | Return ntable -> + | Return ntable0 -> begin match usize_add i 1 with | Fail e -> Fail e | Return i1 -> let l0 = mem_replace_back (list_t t) l ListNil in - begin match vec_index_mut_back (list_t t) v i l0 with + begin match vec_index_mut_back (list_t t) slots i l0 with | Fail e -> Fail e - | Return slots -> - hash_map_move_elements_loop_fwd_back t ntable slots i1 + | Return slots0 -> + hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end end end end - else Return (hm, v) + else Return (ntable, slots) (** [hashmap::HashMap::{0}::move_elements] *) let hash_map_move_elements_fwd_back @@ -313,15 +313,15 @@ let hash_map_insert_fwd_back (** [hashmap::HashMap::{0}::contains_key_in_list] *) let rec hash_map_contains_key_in_list_loop_fwd - (t : Type0) (i : usize) (ls : list_t t) : + (t : Type0) (key : usize) (ls : list_t t) : Tot (result bool) - (decreases (hash_map_contains_key_in_list_decreases t i ls)) + (decreases (hash_map_contains_key_in_list_decreases t key ls)) = begin match ls with | ListCons ckey x tl -> - if ckey = i + if ckey = key then Return true - else hash_map_contains_key_in_list_loop_fwd t i tl + else hash_map_contains_key_in_list_loop_fwd t key tl | ListNil -> Return false end @@ -349,12 +349,14 @@ let hash_map_contains_key_fwd (** [hashmap::HashMap::{0}::get_in_list] *) let rec hash_map_get_in_list_loop_fwd - (t : Type0) (i : usize) (ls : list_t t) : - Tot (result t) (decreases (hash_map_get_in_list_decreases t i ls)) + (t : Type0) (key : usize) (ls : list_t t) : + Tot (result t) (decreases (hash_map_get_in_list_decreases t key ls)) = begin match ls with | ListCons ckey cvalue tl -> - if ckey = i then Return cvalue else hash_map_get_in_list_loop_fwd t i tl + if ckey = key + then Return cvalue + else hash_map_get_in_list_loop_fwd t key tl | ListNil -> Fail Failure end @@ -382,14 +384,14 @@ let hash_map_get_fwd (** [hashmap::HashMap::{0}::get_mut_in_list] *) let rec hash_map_get_mut_in_list_loop_fwd - (t : Type0) (i : usize) (ls : list_t t) : - Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t i ls)) + (t : Type0) (key : usize) (ls : list_t t) : + Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls)) = begin match ls with | ListCons ckey cvalue tl -> - if ckey = i + if ckey = key then Return cvalue - else hash_map_get_mut_in_list_loop_fwd t i tl + else hash_map_get_mut_in_list_loop_fwd t key tl | ListNil -> Fail Failure end @@ -400,16 +402,16 @@ let hash_map_get_mut_in_list_fwd (** [hashmap::HashMap::{0}::get_mut_in_list] *) let rec hash_map_get_mut_in_list_loop_back - (t : Type0) (i : usize) (ls : list_t t) (ret : t) : + (t : Type0) (key : usize) (ls : list_t t) (ret : t) : Tot (result (list_t t)) - (decreases (hash_map_get_mut_in_list_decreases t i ls)) + (decreases (hash_map_get_mut_in_list_decreases t key ls)) = begin match ls with | ListCons ckey cvalue tl -> - if ckey = i + if ckey = key then Return (ListCons ckey ret tl) else - begin match hash_map_get_mut_in_list_loop_back t i tl ret with + begin match hash_map_get_mut_in_list_loop_back t key tl ret with | Fail e -> Fail e | Return l -> Return (ListCons ckey cvalue l) end @@ -472,20 +474,20 @@ let hash_map_get_mut_back (** [hashmap::HashMap::{0}::remove_from_list] *) let rec hash_map_remove_from_list_loop_fwd - (t : Type0) (i : usize) (ls : list_t t) : + (t : Type0) (key : usize) (ls : list_t t) : Tot (result (option t)) - (decreases (hash_map_remove_from_list_decreases t i ls)) + (decreases (hash_map_remove_from_list_decreases t key ls)) = begin match ls with | ListCons ckey x tl -> - if ckey = i + if ckey = key then let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in begin 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 i tl + else hash_map_remove_from_list_loop_fwd t key tl | ListNil -> Return None end @@ -496,21 +498,21 @@ let hash_map_remove_from_list_fwd (** [hashmap::HashMap::{0}::remove_from_list] *) let rec hash_map_remove_from_list_loop_back - (t : Type0) (i : usize) (ls : list_t t) : + (t : Type0) (key : usize) (ls : list_t t) : Tot (result (list_t t)) - (decreases (hash_map_remove_from_list_decreases t i ls)) + (decreases (hash_map_remove_from_list_decreases t key ls)) = begin match ls with | ListCons ckey x tl -> - if ckey = i + if ckey = key then let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in begin match mv_ls with - | ListCons i0 cvalue tl0 -> Return tl0 + | ListCons i cvalue tl0 -> Return tl0 | ListNil -> Fail Failure end else - begin match hash_map_remove_from_list_loop_back t i tl with + begin match hash_map_remove_from_list_loop_back t key tl with | Fail e -> Fail e | Return l -> Return (ListCons ckey x l) end diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst index b3081cd6..55685114 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst @@ -9,13 +9,13 @@ open HashmapMain.Types (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: decreases clause *) unfold let hashmap_hash_map_allocate_slots_decreases (t : Type0) - (v : vec (hashmap_list_t t)) (n : usize) : nat = + (slots : vec (hashmap_list_t t)) (n : usize) : nat = admit () (** [hashmap_main::hashmap::HashMap::{0}::clear_slots]: decreases clause *) unfold let hashmap_hash_map_clear_slots_decreases (t : Type0) - (v : vec (hashmap_list_t t)) (i : usize) : nat = + (slots : vec (hashmap_list_t t)) (i : usize) : nat = admit () (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: decreases clause *) @@ -31,36 +31,37 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *) unfold let hashmap_hash_map_move_elements_from_list_decreases (t : Type0) - (hm : hashmap_hash_map_t t) (ls : hashmap_list_t t) : nat = + (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : nat = admit () (** [hashmap_main::hashmap::HashMap::{0}::move_elements]: decreases clause *) unfold let hashmap_hash_map_move_elements_decreases (t : Type0) - (hm : hashmap_hash_map_t t) (v : vec (hashmap_list_t t)) (i : usize) : nat = + (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) (i : usize) + : nat = admit () (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: decreases clause *) unfold -let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (i : usize) +let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) : nat = admit () (** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: decreases clause *) unfold -let hashmap_hash_map_get_in_list_decreases (t : Type0) (i : usize) +let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) : nat = admit () (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *) unfold -let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (i : usize) +let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) : nat = admit () (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: decreases clause *) unfold -let hashmap_hash_map_remove_from_list_decreases (t : Type0) (i : usize) +let hashmap_hash_map_remove_from_list_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) : nat = admit () diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 3da56f41..fdbf1404 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -13,21 +13,21 @@ let hashmap_hash_key_fwd (k : usize) : result usize = Return k (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) let rec hashmap_hash_map_allocate_slots_loop_fwd - (t : Type0) (v : vec (hashmap_list_t t)) (n : usize) : + (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) : Tot (result (vec (hashmap_list_t t))) - (decreases (hashmap_hash_map_allocate_slots_decreases t v n)) + (decreases (hashmap_hash_map_allocate_slots_decreases t slots n)) = if n > 0 then - begin match vec_push_back (hashmap_list_t t) v HashmapListNil with + begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with | Fail e -> Fail e - | Return slots -> + | Return slots0 -> begin match usize_sub n 1 with | Fail e -> Fail e - | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots n0 + | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 end end - else Return v + else Return slots (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) let hashmap_hash_map_allocate_slots_fwd @@ -64,22 +64,23 @@ let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) = (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) let rec hashmap_hash_map_clear_slots_loop_fwd_back - (t : Type0) (v : vec (hashmap_list_t t)) (i : usize) : + (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) : Tot (result (vec (hashmap_list_t t))) - (decreases (hashmap_hash_map_clear_slots_decreases t v i)) + (decreases (hashmap_hash_map_clear_slots_decreases t slots i)) = - let i0 = vec_len (hashmap_list_t t) v in + let i0 = vec_len (hashmap_list_t t) slots in if i < i0 then begin match usize_add i 1 with | Fail e -> Fail e | Return i1 -> - begin match vec_index_mut_back (hashmap_list_t t) v i HashmapListNil with + begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil + with | Fail e -> Fail e - | Return slots -> hashmap_hash_map_clear_slots_loop_fwd_back t slots i1 + | Return slots0 -> hashmap_hash_map_clear_slots_loop_fwd_back t slots0 i1 end end - else Return v + else Return slots (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) let hashmap_hash_map_clear_slots_fwd_back @@ -214,18 +215,18 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back - (t : Type0) (hm : hashmap_hash_map_t t) (ls : hashmap_list_t t) : + (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : Tot (result (hashmap_hash_map_t t)) - (decreases (hashmap_hash_map_move_elements_from_list_decreases t hm ls)) + (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls)) = begin match ls with | HashmapListCons k v tl -> - begin match hashmap_hash_map_insert_no_resize_fwd_back t hm k v with + begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with | Fail e -> Fail e - | Return ntable -> - hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable tl + | Return ntable0 -> + hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl end - | HashmapListNil -> Return hm + | HashmapListNil -> Return ntable end (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) @@ -237,35 +238,35 @@ let hashmap_hash_map_move_elements_from_list_fwd_back (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) let rec hashmap_hash_map_move_elements_loop_fwd_back - (t : Type0) (hm : hashmap_hash_map_t t) (v : vec (hashmap_list_t t)) + (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) (i : usize) : Tot (result ((hashmap_hash_map_t t) & (vec (hashmap_list_t t)))) - (decreases (hashmap_hash_map_move_elements_decreases t hm v i)) + (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i)) = - let i0 = vec_len (hashmap_list_t t) v in + let i0 = vec_len (hashmap_list_t t) slots in if i < i0 then - begin match vec_index_mut_fwd (hashmap_list_t t) v i with + begin match vec_index_mut_fwd (hashmap_list_t t) slots i with | Fail e -> Fail e | Return l -> let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in - begin match hashmap_hash_map_move_elements_from_list_fwd_back t hm ls + begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls with | Fail e -> Fail e - | Return ntable -> + | Return ntable0 -> begin match usize_add i 1 with | Fail e -> Fail e | Return i1 -> let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in - begin match vec_index_mut_back (hashmap_list_t t) v i l0 with + begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with | Fail e -> Fail e - | Return slots -> - hashmap_hash_map_move_elements_loop_fwd_back t ntable slots i1 + | Return slots0 -> + hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end end end end - else Return (hm, v) + else Return (ntable, slots) (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) let hashmap_hash_map_move_elements_fwd_back @@ -334,15 +335,15 @@ let hashmap_hash_map_insert_fwd_back (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) let rec hashmap_hash_map_contains_key_in_list_loop_fwd - (t : Type0) (i : usize) (ls : hashmap_list_t t) : + (t : Type0) (key : usize) (ls : hashmap_list_t t) : Tot (result bool) - (decreases (hashmap_hash_map_contains_key_in_list_decreases t i ls)) + (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey x tl -> - if ckey = i + if ckey = key then Return true - else hashmap_hash_map_contains_key_in_list_loop_fwd t i tl + else hashmap_hash_map_contains_key_in_list_loop_fwd t key tl | HashmapListNil -> Return false end @@ -372,14 +373,14 @@ let hashmap_hash_map_contains_key_fwd (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) let rec hashmap_hash_map_get_in_list_loop_fwd - (t : Type0) (i : usize) (ls : hashmap_list_t t) : - Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t i ls)) + (t : Type0) (key : usize) (ls : hashmap_list_t t) : + Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey cvalue tl -> - if ckey = i + if ckey = key then Return cvalue - else hashmap_hash_map_get_in_list_loop_fwd t i tl + else hashmap_hash_map_get_in_list_loop_fwd t key tl | HashmapListNil -> Fail Failure end @@ -409,15 +410,15 @@ let hashmap_hash_map_get_fwd (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) let rec hashmap_hash_map_get_mut_in_list_loop_fwd - (t : Type0) (i : usize) (ls : hashmap_list_t t) : + (t : Type0) (key : usize) (ls : hashmap_list_t t) : Tot (result t) - (decreases (hashmap_hash_map_get_mut_in_list_decreases t i ls)) + (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey cvalue tl -> - if ckey = i + if ckey = key then Return cvalue - else hashmap_hash_map_get_mut_in_list_loop_fwd t i tl + else hashmap_hash_map_get_mut_in_list_loop_fwd t key tl | HashmapListNil -> Fail Failure end @@ -428,16 +429,16 @@ let hashmap_hash_map_get_mut_in_list_fwd (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) let rec hashmap_hash_map_get_mut_in_list_loop_back - (t : Type0) (i : usize) (ls : hashmap_list_t t) (ret : t) : + (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) : Tot (result (hashmap_list_t t)) - (decreases (hashmap_hash_map_get_mut_in_list_decreases t i ls)) + (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey cvalue tl -> - if ckey = i + if ckey = key then Return (HashmapListCons ckey ret tl) else - begin match hashmap_hash_map_get_mut_in_list_loop_back t i tl ret with + begin match hashmap_hash_map_get_mut_in_list_loop_back t key tl ret with | Fail e -> Fail e | Return l -> Return (HashmapListCons ckey cvalue l) end @@ -506,22 +507,22 @@ let hashmap_hash_map_get_mut_back (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) let rec hashmap_hash_map_remove_from_list_loop_fwd - (t : Type0) (i : usize) (ls : hashmap_list_t t) : + (t : Type0) (key : usize) (ls : hashmap_list_t t) : Tot (result (option t)) - (decreases (hashmap_hash_map_remove_from_list_decreases t i ls)) + (decreases (hashmap_hash_map_remove_from_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey x tl -> - if ckey = i + if ckey = key then let mv_ls = mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl) HashmapListNil in begin 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 i tl + else hashmap_hash_map_remove_from_list_loop_fwd t key tl | HashmapListNil -> Return None end @@ -532,23 +533,23 @@ let hashmap_hash_map_remove_from_list_fwd (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) let rec hashmap_hash_map_remove_from_list_loop_back - (t : Type0) (i : usize) (ls : hashmap_list_t t) : + (t : Type0) (key : usize) (ls : hashmap_list_t t) : Tot (result (hashmap_list_t t)) - (decreases (hashmap_hash_map_remove_from_list_decreases t i ls)) + (decreases (hashmap_hash_map_remove_from_list_decreases t key ls)) = begin match ls with | HashmapListCons ckey x tl -> - if ckey = i + if ckey = key then let mv_ls = mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl) HashmapListNil in begin match mv_ls with - | HashmapListCons i0 cvalue tl0 -> Return tl0 + | HashmapListCons i cvalue tl0 -> Return tl0 | HashmapListNil -> Fail Failure end else - begin match hashmap_hash_map_remove_from_list_loop_back t i tl with + begin match hashmap_hash_map_remove_from_list_loop_back t key tl with | Fail e -> Fail e | Return l -> Return (HashmapListCons ckey x l) end diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst index 3d475d20..1b141d64 100644 --- a/tests/fstar/misc/Loops.Clauses.Template.fst +++ b/tests/fstar/misc/Loops.Clauses.Template.fst @@ -23,7 +23,7 @@ let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat = unfold let clear_decreases (v : vec u32) (i : usize) : nat = admit () (** [loops::list_mem]: decreases clause *) -unfold let list_mem_decreases (i : u32) (ls : list_t u32) : nat = admit () +unfold let list_mem_decreases (x : u32) (ls : list_t u32) : nat = admit () (** [loops::list_nth_mut_loop]: decreases clause *) unfold @@ -42,8 +42,8 @@ let get_elem_mut_decreases (x : usize) (ls : list_t usize) : nat = admit () (** [loops::get_elem_shared]: decreases clause *) unfold -let get_elem_shared_decreases (x : usize) (v : vec (list_t usize)) - (l : list_t usize) (ls : list_t usize) : nat = +let get_elem_shared_decreases (x : usize) (slots : vec (list_t usize)) + (ls : list_t usize) (ls0 : list_t usize) : nat = admit () (** [loops::list_nth_mut_loop_with_id]: decreases clause *) @@ -54,55 +54,55 @@ let list_nth_mut_loop_with_id_decreases (t : Type0) (i : u32) (ls : list_t t) : (** [loops::list_nth_shared_loop_with_id]: decreases clause *) unfold -let list_nth_shared_loop_with_id_decreases (t : Type0) (l : list_t t) - (i : u32) (ls : list_t t) : nat = +let list_nth_shared_loop_with_id_decreases (t : Type0) (ls : list_t t) + (i : u32) (ls0 : list_t t) : nat = admit () (** [loops::list_nth_mut_loop_pair]: decreases clause *) unfold -let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t) - (i : u32) : nat = +let list_nth_mut_loop_pair_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = admit () (** [loops::list_nth_shared_loop_pair]: decreases clause *) unfold -let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t) - (l0 : list_t t) (i : u32) : nat = +let list_nth_shared_loop_pair_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = admit () (** [loops::list_nth_mut_loop_pair_merge]: decreases clause *) unfold -let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t) - (l0 : list_t t) (i : u32) : nat = +let list_nth_mut_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = admit () (** [loops::list_nth_shared_loop_pair_merge]: decreases clause *) unfold -let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t) - (l0 : list_t t) (i : u32) : nat = +let list_nth_shared_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = admit () (** [loops::list_nth_mut_shared_loop_pair]: decreases clause *) unfold -let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t) - (l0 : list_t t) (i : u32) : nat = +let list_nth_mut_shared_loop_pair_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = admit () (** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *) unfold -let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t) - (l0 : list_t t) (i : u32) : nat = +let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = admit () (** [loops::list_nth_shared_mut_loop_pair]: decreases clause *) unfold -let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t) - (l0 : list_t t) (i : u32) : nat = +let list_nth_shared_mut_loop_pair_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = admit () (** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *) unfold -let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t) - (l0 : list_t t) (i : u32) : nat = +let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = admit () diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index b7dcd045..ca918e35 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -92,11 +92,11 @@ let clear_fwd_back (v : vec u32) : result (vec u32) = clear_loop_fwd_back v 0 (** [loops::list_mem] *) let rec list_mem_loop_fwd - (i : u32) (ls : list_t u32) : - Tot (result bool) (decreases (list_mem_decreases i ls)) + (x : u32) (ls : list_t u32) : + Tot (result bool) (decreases (list_mem_decreases x ls)) = begin match ls with - | ListCons y tl -> if y = i then Return true else list_mem_loop_fwd i tl + | ListCons y tl -> if y = x then Return true else list_mem_loop_fwd x tl | ListNil -> Return false end @@ -222,12 +222,13 @@ let get_elem_mut_back (** [loops::get_elem_shared] *) let rec get_elem_shared_loop_fwd - (x : usize) (v : vec (list_t usize)) (l : list_t usize) (ls : list_t usize) : - Tot (result usize) (decreases (get_elem_shared_decreases x v l ls)) + (x : usize) (slots : vec (list_t usize)) (ls : list_t usize) + (ls0 : list_t usize) : + Tot (result usize) (decreases (get_elem_shared_decreases x slots ls ls0)) = - begin match ls with + begin match ls0 with | ListCons y tl -> - if y = x then Return y else get_elem_shared_loop_fwd x v l tl + if y = x then Return y else get_elem_shared_loop_fwd x slots ls tl | ListNil -> Fail Failure end @@ -311,17 +312,18 @@ let list_nth_mut_loop_with_id_back (** [loops::list_nth_shared_loop_with_id] *) let rec list_nth_shared_loop_with_id_loop_fwd - (t : Type0) (l : list_t t) (i : u32) (ls : list_t t) : - Tot (result t) (decreases (list_nth_shared_loop_with_id_decreases t l i ls)) + (t : Type0) (ls : list_t t) (i : u32) (ls0 : list_t t) : + Tot (result t) + (decreases (list_nth_shared_loop_with_id_decreases t ls i ls0)) = - begin match ls with + begin match ls0 with | ListCons x tl -> if i = 0 then Return x else begin match u32_sub i 1 with | Fail e -> Fail e - | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t l i0 tl + | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t ls i0 tl end | ListNil -> Fail Failure end @@ -336,12 +338,13 @@ let list_nth_shared_loop_with_id_fwd (** [loops::list_nth_mut_loop_pair] *) let rec list_nth_mut_loop_pair_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : - Tot (result (t & t)) (decreases (list_nth_mut_loop_pair_decreases t l l0 i)) + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -362,13 +365,13 @@ let list_nth_mut_loop_pair_fwd (** [loops::list_nth_mut_loop_pair] *) let rec list_nth_mut_loop_pair_loop_back'a - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_mut_loop_pair_decreases t l l0 i)) + (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) @@ -378,7 +381,7 @@ let rec list_nth_mut_loop_pair_loop_back'a | Return i0 -> begin match list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x0 l1) + | Return l -> Return (ListCons x0 l) end end | ListNil -> Fail Failure @@ -395,13 +398,13 @@ let list_nth_mut_loop_pair_back'a (** [loops::list_nth_mut_loop_pair] *) let rec list_nth_mut_loop_pair_loop_back'b - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_mut_loop_pair_decreases t l l0 i)) + (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) @@ -411,7 +414,7 @@ let rec list_nth_mut_loop_pair_loop_back'b | Return i0 -> begin match list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x1 l1) + | Return l -> Return (ListCons x1 l) end end | ListNil -> Fail Failure @@ -428,13 +431,13 @@ let list_nth_mut_loop_pair_back'b (** [loops::list_nth_shared_loop_pair] *) let rec list_nth_shared_loop_pair_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_shared_loop_pair_decreases t l l0 i)) + (decreases (list_nth_shared_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -455,13 +458,13 @@ let list_nth_shared_loop_pair_fwd (** [loops::list_nth_mut_loop_pair_merge] *) let rec list_nth_mut_loop_pair_merge_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_mut_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_mut_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -482,13 +485,13 @@ let list_nth_mut_loop_pair_merge_fwd (** [loops::list_nth_mut_loop_pair_merge] *) let rec list_nth_mut_loop_pair_merge_loop_back - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : (t & t)) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) : Tot (result ((list_t t) & (list_t t))) - (decreases (list_nth_mut_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_mut_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then let (x, x2) = ret in Return (ListCons x tl0, ListCons x2 tl1) @@ -499,7 +502,7 @@ let rec list_nth_mut_loop_pair_merge_loop_back begin match list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return (l1, l2) -> Return (ListCons x0 l1, ListCons x1 l2) + | Return (l, l0) -> Return (ListCons x0 l, ListCons x1 l0) end end | ListNil -> Fail Failure @@ -516,13 +519,13 @@ let list_nth_mut_loop_pair_merge_back (** [loops::list_nth_shared_loop_pair_merge] *) let rec list_nth_shared_loop_pair_merge_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_shared_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_shared_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -543,13 +546,13 @@ let list_nth_shared_loop_pair_merge_fwd (** [loops::list_nth_mut_shared_loop_pair] *) let rec list_nth_mut_shared_loop_pair_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i)) + (decreases (list_nth_mut_shared_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -570,13 +573,13 @@ let list_nth_mut_shared_loop_pair_fwd (** [loops::list_nth_mut_shared_loop_pair] *) let rec list_nth_mut_shared_loop_pair_loop_back - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i)) + (decreases (list_nth_mut_shared_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) @@ -587,7 +590,7 @@ let rec list_nth_mut_shared_loop_pair_loop_back begin match list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x0 l1) + | Return l -> Return (ListCons x0 l) end end | ListNil -> Fail Failure @@ -604,13 +607,13 @@ let list_nth_mut_shared_loop_pair_back (** [loops::list_nth_mut_shared_loop_pair_merge] *) let rec list_nth_mut_shared_loop_pair_merge_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_mut_shared_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -632,13 +635,13 @@ let list_nth_mut_shared_loop_pair_merge_fwd (** [loops::list_nth_mut_shared_loop_pair_merge] *) let rec list_nth_mut_shared_loop_pair_merge_loop_back - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_mut_shared_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) @@ -649,7 +652,7 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back begin match list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x0 l1) + | Return l -> Return (ListCons x0 l) end end | ListNil -> Fail Failure @@ -666,13 +669,13 @@ let list_nth_mut_shared_loop_pair_merge_back (** [loops::list_nth_shared_mut_loop_pair] *) let rec list_nth_shared_mut_loop_pair_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i)) + (decreases (list_nth_shared_mut_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -693,13 +696,13 @@ let list_nth_shared_mut_loop_pair_fwd (** [loops::list_nth_shared_mut_loop_pair] *) let rec list_nth_shared_mut_loop_pair_loop_back - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i)) + (decreases (list_nth_shared_mut_loop_pair_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) @@ -710,7 +713,7 @@ let rec list_nth_shared_mut_loop_pair_loop_back begin match list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x1 l1) + | Return l -> Return (ListCons x1 l) end end | ListNil -> Fail Failure @@ -727,13 +730,13 @@ let list_nth_shared_mut_loop_pair_back (** [loops::list_nth_shared_mut_loop_pair_merge] *) let rec list_nth_shared_mut_loop_pair_merge_loop_fwd - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : Tot (result (t & t)) - (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_shared_mut_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) @@ -755,13 +758,13 @@ let list_nth_shared_mut_loop_pair_merge_fwd (** [loops::list_nth_shared_mut_loop_pair_merge] *) let rec list_nth_shared_mut_loop_pair_merge_loop_back - (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) : + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) - (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i)) + (decreases (list_nth_shared_mut_loop_pair_merge_decreases t ls0 ls1 i)) = - begin match l with + begin match ls0 with | ListCons x0 tl0 -> - begin match l0 with + begin match ls1 with | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) @@ -772,7 +775,7 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back begin match list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with | Fail e -> Fail e - | Return l1 -> Return (ListCons x1 l1) + | Return l -> Return (ListCons x1 l) end end | ListNil -> Fail Failure |