summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/hashmap')
-rw-r--r--tests/fstar/hashmap/Hashmap.Clauses.Template.fst4
-rw-r--r--tests/fstar/hashmap/Hashmap.Clauses.fst4
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst16
-rw-r--r--tests/fstar/hashmap/Hashmap.Properties.fst28
4 files changed, 26 insertions, 26 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index 3e51c6f1..ce86071c 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
@@ -54,8 +54,8 @@ let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) :
(** [hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
unfold
-let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
- (ls : list_t t) : nat =
+let hash_map_get_mut_in_list_decreases (t : Type0) (ls : list_t t)
+ (key : usize) : nat =
admit ()
(** [hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.fst b/tests/fstar/hashmap/Hashmap.Clauses.fst
index 4f3e37e9..2a9c0242 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.fst
@@ -49,8 +49,8 @@ let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) :
(** [hashmap::HashMap::get_mut_in_list]: decreases clause *)
unfold
-let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
- (ls : list_t t) : list_t t =
+let hash_map_get_mut_in_list_decreases (t : Type0) (ls : list_t t)
+ (key : usize) : list_t t =
ls
(** [hashmap::HashMap::remove_from_list]: decreases clause *)
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 81b253ad..14cea9cb 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -384,34 +384,34 @@ let hash_map_get_fwd
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
let rec hash_map_get_mut_in_list_loop_fwd
- (t : Type0) (key : usize) (ls : list_t t) :
- Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls))
+ (t : Type0) (ls : list_t t) (key : usize) :
+ Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t ls key))
=
begin match ls with
| ListCons ckey cvalue tl ->
if ckey = key
then Return cvalue
- else hash_map_get_mut_in_list_loop_fwd t key tl
+ else hash_map_get_mut_in_list_loop_fwd t tl key
| ListNil -> Fail Failure
end
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
let hash_map_get_mut_in_list_fwd
(t : Type0) (ls : list_t t) (key : usize) : result t =
- hash_map_get_mut_in_list_loop_fwd t key ls
+ hash_map_get_mut_in_list_loop_fwd t ls key
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
let rec hash_map_get_mut_in_list_loop_back
- (t : Type0) (key : usize) (ls : list_t t) (ret : t) :
+ (t : Type0) (ls : list_t t) (key : usize) (ret : t) :
Tot (result (list_t t))
- (decreases (hash_map_get_mut_in_list_decreases t key ls))
+ (decreases (hash_map_get_mut_in_list_decreases t ls key))
=
begin match ls with
| ListCons ckey cvalue tl ->
if ckey = key
then Return (ListCons ckey ret tl)
else
- begin match hash_map_get_mut_in_list_loop_back t key tl ret with
+ begin match hash_map_get_mut_in_list_loop_back t tl key ret with
| Fail e -> Fail e
| Return l -> Return (ListCons ckey cvalue l)
end
@@ -421,7 +421,7 @@ let rec hash_map_get_mut_in_list_loop_back
(** [hashmap::HashMap::{0}::get_mut_in_list] *)
let hash_map_get_mut_in_list_back
(t : Type0) (ls : list_t t) (key : usize) (ret : t) : result (list_t t) =
- hash_map_get_mut_in_list_loop_back t key ls ret
+ hash_map_get_mut_in_list_loop_back t ls key ret
(** [hashmap::HashMap::{0}::get_mut] *)
let hash_map_get_mut_fwd
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 11:28:39 +0000