diff options
author | Son Ho | 2023-01-07 17:21:27 +0100 |
---|---|---|
committer | Son HO | 2023-02-03 11:21:46 +0100 |
commit | af929939c44116cdfd5faa845273d0f032d761bf (patch) | |
tree | 6f59e4a60d060bc2f755aa9b4fbf02bd41e90381 /tests/fstar/hashmap/Hashmap.Properties.fst | |
parent | f8b7206e0d92aa33812047c521a3c2278fdb6327 (diff) |
Improve the order of the loop input parameters
Diffstat (limited to 'tests/fstar/hashmap/Hashmap.Properties.fst')
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Properties.fst | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst index 724ca741..e1d0a541 100644 --- a/tests/fstar/hashmap/Hashmap.Properties.fst +++ b/tests/fstar/hashmap/Hashmap.Properties.fst @@ -2704,16 +2704,16 @@ let hash_map_get_fwd_lem #t self key = hash_map_get_fwd_lem_aux #t self key (**** get_mut_in_list'fwd *) val hash_map_get_mut_in_list_loop_fwd_lem - (#t : Type0) (key : usize) (ls : list_t t) : + (#t : Type0) (ls : list_t t) (key : usize) : Lemma (ensures ( - match hash_map_get_mut_in_list_loop_fwd t key ls, slot_t_find_s key ls with + match hash_map_get_mut_in_list_loop_fwd t ls key, slot_t_find_s key ls with | Fail _, None -> True | Return x, Some x' -> x == x' | _ -> False)) #push-options "--fuel 1" -let rec hash_map_get_mut_in_list_loop_fwd_lem #t key ls = +let rec hash_map_get_mut_in_list_loop_fwd_lem #t ls key = begin match ls with | ListCons ckey cvalue ls0 -> let b = ckey = key in @@ -2721,8 +2721,8 @@ let rec hash_map_get_mut_in_list_loop_fwd_lem #t key ls = then () else begin - hash_map_get_mut_in_list_loop_fwd_lem key ls0; - match hash_map_get_mut_in_list_loop_fwd t key ls0 with + hash_map_get_mut_in_list_loop_fwd_lem ls0 key; + match hash_map_get_mut_in_list_loop_fwd t ls0 key with | Fail _ -> () | Return x -> () end @@ -2754,8 +2754,8 @@ let hash_map_get_mut_fwd_lem_aux #t self key = | Fail _ -> () | Return l -> begin - hash_map_get_mut_in_list_loop_fwd_lem key l; - match hash_map_get_mut_in_list_loop_fwd t key l with + hash_map_get_mut_in_list_loop_fwd_lem l key; + match hash_map_get_mut_in_list_loop_fwd t l key with | Fail _ -> () | Return x -> () end @@ -2771,17 +2771,17 @@ let hash_map_get_mut_fwd_lem #t self key = (**** get_mut_in_list'back *) val hash_map_get_mut_in_list_loop_back_lem - (#t : Type0) (key : usize) (ls : list_t t) (ret : t) : + (#t : Type0) (ls : list_t t) (key : usize) (ret : t) : Lemma (requires (Some? (slot_t_find_s key ls))) (ensures ( - match hash_map_get_mut_in_list_loop_back t key ls ret with + match hash_map_get_mut_in_list_loop_back t ls key ret with | Fail _ -> False | Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,ret) | _ -> False)) #push-options "--fuel 1" -let rec hash_map_get_mut_in_list_loop_back_lem #t key ls ret = +let rec hash_map_get_mut_in_list_loop_back_lem #t ls key ret = begin match ls with | ListCons ckey cvalue ls0 -> let b = ckey = key in @@ -2789,8 +2789,8 @@ let rec hash_map_get_mut_in_list_loop_back_lem #t key ls ret = then let ls1 = ListCons ckey ret ls0 in () else begin - hash_map_get_mut_in_list_loop_back_lem key ls0 ret; - match hash_map_get_mut_in_list_loop_back t key ls0 ret with + hash_map_get_mut_in_list_loop_back_lem ls0 key ret; + match hash_map_get_mut_in_list_loop_back t ls0 key ret with | Fail _ -> () | Return l -> let ls1 = ListCons ckey cvalue l in () end @@ -2828,8 +2828,8 @@ let hash_map_get_mut_back_lem_refin #t self key ret = | Fail _ -> () | Return l -> begin - hash_map_get_mut_in_list_loop_back_lem key l ret; - match hash_map_get_mut_in_list_loop_back t key l ret with + hash_map_get_mut_in_list_loop_back_lem l key ret; + match hash_map_get_mut_in_list_loop_back t l key ret with | Fail _ -> () | Return l0 -> begin match vec_index_mut_back (list_t t) v hash_mod l0 with |