diff options
Diffstat (limited to 'tests/coq')
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 12 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 12 | ||||
| -rw-r--r-- | tests/coq/misc/Loops.v | 8 |
3 files changed, 16 insertions, 16 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 1cbff379..9c65fb46 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -332,7 +332,7 @@ 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) (key : usize) (ls : List_t T) : result T := + (T : Type) (n : nat) (ls : List_t T) (key : usize) : result T := match n with | O => Fail_ OutOfFuel | S n0 => @@ -340,7 +340,7 @@ Fixpoint hash_map_get_mut_in_list_loop_fwd | ListCons ckey cvalue tl => if ckey s= key then Return cvalue - else hash_map_get_mut_in_list_loop_fwd T n0 key tl + else hash_map_get_mut_in_list_loop_fwd T n0 tl key | ListNil => Fail_ Failure end end @@ -349,12 +349,12 @@ Fixpoint hash_map_get_mut_in_list_loop_fwd (** [hashmap::HashMap::{0}::get_mut_in_list] *) Definition hash_map_get_mut_in_list_fwd (T : Type) (n : nat) (ls : List_t T) (key : usize) : result T := - hash_map_get_mut_in_list_loop_fwd T n key ls + hash_map_get_mut_in_list_loop_fwd T n ls key . (** [hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hash_map_get_mut_in_list_loop_back - (T : Type) (n : nat) (key : usize) (ls : List_t T) (ret : T) : + (T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) : result (List_t T) := match n with @@ -365,7 +365,7 @@ Fixpoint hash_map_get_mut_in_list_loop_back if ckey s= key then Return (ListCons ckey ret tl) else ( - l <- hash_map_get_mut_in_list_loop_back T n0 key tl ret; + l <- hash_map_get_mut_in_list_loop_back T n0 tl key ret; Return (ListCons ckey cvalue l)) | ListNil => Fail_ Failure end @@ -377,7 +377,7 @@ Definition hash_map_get_mut_in_list_back (T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) : result (List_t T) := - hash_map_get_mut_in_list_loop_back T n key ls ret + hash_map_get_mut_in_list_loop_back T n ls key ret . (** [hashmap::HashMap::{0}::get_mut] *) diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 2a8ab5b5..94a9e6a5 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -358,7 +358,7 @@ 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) (key : usize) (ls : Hashmap_list_t T) : result T := + (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T := match n with | O => Fail_ OutOfFuel | S n0 => @@ -366,7 +366,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd | HashmapListCons ckey cvalue tl => if ckey s= key then Return cvalue - else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 key tl + else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 tl key | HashmapListNil => Fail_ Failure end end @@ -375,12 +375,12 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) Definition hashmap_hash_map_get_mut_in_list_fwd (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T := - hashmap_hash_map_get_mut_in_list_loop_fwd T n key ls + hashmap_hash_map_get_mut_in_list_loop_fwd T n ls key . (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hashmap_hash_map_get_mut_in_list_loop_back - (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) : + (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) : result (Hashmap_list_t T) := match n with @@ -391,7 +391,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back if ckey s= key then Return (HashmapListCons ckey ret tl) else ( - l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 key tl ret; + l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret; Return (HashmapListCons ckey cvalue l)) | HashmapListNil => Fail_ Failure end @@ -403,7 +403,7 @@ Definition hashmap_hash_map_get_mut_in_list_back (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) : result (Hashmap_list_t T) := - hashmap_hash_map_get_mut_in_list_loop_back T n key ls ret + hashmap_hash_map_get_mut_in_list_loop_back T n ls key ret . (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 4fbb7da0..9d416bb0 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -235,16 +235,16 @@ Definition get_elem_mut_back (** [loops::get_elem_shared] *) Fixpoint get_elem_shared_loop_fwd - (n : nat) (x : usize) (slots : vec (List_t usize)) (ls : List_t usize) + (n : nat) (slots : vec (List_t usize)) (x : usize) (ls : List_t usize) (ls0 : List_t usize) : result usize := match n with | O => Fail_ OutOfFuel | S n0 => - match ls0 with + match ls with | ListCons y tl => - if y s= x then Return y else get_elem_shared_loop_fwd n0 x slots ls tl + if y s= x then Return y else get_elem_shared_loop_fwd n0 slots x tl ls0 | ListNil => Fail_ Failure end end @@ -254,7 +254,7 @@ Fixpoint get_elem_shared_loop_fwd Definition get_elem_shared_fwd (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize := l <- vec_index_fwd (List_t usize) slots (0%usize); - get_elem_shared_loop_fwd n x slots l l + get_elem_shared_loop_fwd n slots x l l . (** [loops::id_mut] *) |