diff options
Diffstat (limited to 'tests/fstar')
| -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 |
6 files changed, 234 insertions, 227 deletions
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 |