diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/hashmap/Hashmap__Funs.v | 130 | ||||
| -rw-r--r-- | tests/coq/hashmap/Hashmap__Types.v | 23 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain__Funs.v | 150 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain__Opaque.v | 10 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain__Types.v | 23 |
5 files changed, 168 insertions, 168 deletions
diff --git a/tests/coq/hashmap/Hashmap__Funs.v b/tests/coq/hashmap/Hashmap__Funs.v index 93aa389b..7d897c8a 100644 --- a/tests/coq/hashmap/Hashmap__Funs.v +++ b/tests/coq/hashmap/Hashmap__Funs.v @@ -4,12 +4,12 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export Hashmap__Types . -Import Hashmap__Types . -Module Hashmap__Funs . +Require Export Hashmap__Types. +Import Hashmap__Types. +Module Hashmap__Funs. (** [hashmap::hash_key] *) -Definition hash_key_fwd (k : usize) : result usize := Return k . +Definition hash_key_fwd (k : usize) : result usize := Return k. (** [hashmap::HashMap::{0}::allocate_slots] *) Fixpoint hash_map_allocate_slots_fwd @@ -19,15 +19,15 @@ Fixpoint hash_map_allocate_slots_fwd match n with | O => Fail_ OutOfFuel | S n1 => - if n0 s= 0 %usize + if n0 s= 0%usize then Return slots else ( slots0 <- vec_push_back (List_t T) slots ListNil; - i <- usize_sub n0 1 %usize; + i <- usize_sub n0 1%usize; v <- hash_map_allocate_slots_fwd T n1 slots0 i; Return v) end - . +. (** [hashmap::HashMap::{0}::new_with_capacity] *) Definition hash_map_new_with_capacity_fwd @@ -42,21 +42,20 @@ Definition hash_map_new_with_capacity_fwd slots <- hash_map_allocate_slots_fwd T n0 v capacity; i <- usize_mul capacity max_load_dividend; i0 <- usize_div i max_load_divisor; - Return (mkHash_map_t (0 %usize) (max_load_dividend, max_load_divisor) i0 + Return (mkHash_map_t (0%usize) (max_load_dividend, max_load_divisor) i0 slots) end - . +. (** [hashmap::HashMap::{0}::new] *) Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) := match n with | O => Fail_ OutOfFuel | S n0 => - hm <- - hash_map_new_with_capacity_fwd T n0 (32 %usize) (4 %usize) (5 %usize); + hm <- hash_map_new_with_capacity_fwd T n0 (32%usize) (4%usize) (5%usize); Return hm end - . +. (** [hashmap::HashMap::{0}::clear_slots] *) Fixpoint hash_map_clear_slots_fwd_back @@ -70,12 +69,12 @@ Fixpoint hash_map_clear_slots_fwd_back if i s< i0 then ( slots0 <- vec_index_mut_back (List_t T) slots i ListNil; - i1 <- usize_add i 1 %usize; + i1 <- usize_add i 1%usize; slots1 <- hash_map_clear_slots_fwd_back T n0 slots0 i1; Return slots1) else Return slots end - . +. (** [hashmap::HashMap::{0}::clear] *) Definition hash_map_clear_fwd_back @@ -85,15 +84,16 @@ Definition hash_map_clear_fwd_back | S n0 => match self with | mkHash_map_t i p i0 v => - v0 <- hash_map_clear_slots_fwd_back T n0 v (0 %usize); - Return (mkHash_map_t (0 %usize) p i0 v0) + v0 <- hash_map_clear_slots_fwd_back T n0 v (0%usize); + Return (mkHash_map_t (0%usize) p i0 v0) end end - . +. (** [hashmap::HashMap::{0}::len] *) Definition hash_map_len_fwd (T : Type) (self : Hash_map_t T) : result usize := - match self with | mkHash_map_t i p i0 v => Return i end . + match self with | mkHash_map_t i p i0 v => Return i end +. (** [hashmap::HashMap::{0}::insert_in_list] *) Fixpoint hash_map_insert_in_list_fwd @@ -111,7 +111,7 @@ Fixpoint hash_map_insert_in_list_fwd | ListNil => Return true end end - . +. (** [hashmap::HashMap::{0}::insert_in_list] *) Fixpoint hash_map_insert_in_list_back @@ -131,7 +131,7 @@ Fixpoint hash_map_insert_in_list_back | ListNil => let l := ListNil in Return (ListCons key value l) end end - . +. (** [hashmap::HashMap::{0}::insert_no_resize] *) Definition hash_map_insert_no_resize_fwd_back @@ -150,7 +150,7 @@ Definition hash_map_insert_no_resize_fwd_back inserted <- hash_map_insert_in_list_fwd T n0 key value l; if inserted then ( - i2 <- usize_add i 1 %usize; + i2 <- usize_add i 1%usize; l0 <- hash_map_insert_in_list_back T n0 key value l; v0 <- vec_index_mut_back (List_t T) v hash_mod l0; Return (mkHash_map_t i2 p i0 v0)) @@ -160,11 +160,11 @@ Definition hash_map_insert_no_resize_fwd_back Return (mkHash_map_t i p i0 v0)) end end - . +. (** [core::num::u32::{9}::MAX] *) -Definition core_num_u32_max_body : result u32 := Return (4294967295 %u32) . -Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global . +Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). +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_fwd_back @@ -182,7 +182,7 @@ Fixpoint hash_map_move_elements_from_list_fwd_back | ListNil => Return ntable end end - . +. (** [hashmap::HashMap::{0}::move_elements] *) Fixpoint hash_map_move_elements_fwd_back @@ -201,13 +201,13 @@ Fixpoint hash_map_move_elements_fwd_back ntable0 <- hash_map_move_elements_from_list_fwd_back T n0 ntable ls; let l0 := mem_replace_back (List_t T) l ListNil in slots0 <- vec_index_mut_back (List_t T) slots i l0; - i1 <- usize_add i 1 %usize; + i1 <- usize_add i 1%usize; p <- hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1; let (ntable1, slots1) := p in Return (ntable1, slots1)) else Return (ntable, slots) end - . +. (** [hashmap::HashMap::{0}::try_resize] *) Definition hash_map_try_resize_fwd_back @@ -219,14 +219,14 @@ Definition hash_map_try_resize_fwd_back match self with | mkHash_map_t i p i0 v => let capacity := vec_len (List_t T) v in - n1 <- usize_div max_usize 2 %usize; + n1 <- usize_div max_usize 2%usize; let (i1, i2) := p in i3 <- usize_div n1 i1; if capacity s<= i3 then ( - i4 <- usize_mul capacity 2 %usize; + i4 <- usize_mul capacity 2%usize; ntable <- hash_map_new_with_capacity_fwd T n0 i4 i1 i2; - p0 <- hash_map_move_elements_fwd_back T n0 ntable v (0 %usize); + p0 <- hash_map_move_elements_fwd_back T n0 ntable v (0%usize); let (ntable0, _) := p0 in match ntable0 with | mkHash_map_t i5 p1 i6 v0 => Return (mkHash_map_t i (i1, i2) i6 v0) @@ -234,7 +234,7 @@ Definition hash_map_try_resize_fwd_back else Return (mkHash_map_t i (i1, i2) i0 v) end end - . +. (** [hashmap::HashMap::{0}::insert] *) Definition hash_map_insert_fwd_back @@ -255,7 +255,7 @@ Definition hash_map_insert_fwd_back else Return (mkHash_map_t i0 p i1 v) end end - . +. (** [hashmap::HashMap::{0}::contains_key_in_list] *) Fixpoint hash_map_contains_key_in_list_fwd @@ -271,7 +271,7 @@ Fixpoint hash_map_contains_key_in_list_fwd | ListNil => Return false end end - . +. (** [hashmap::HashMap::{0}::contains_key] *) Definition hash_map_contains_key_fwd @@ -289,7 +289,7 @@ Definition hash_map_contains_key_fwd Return b end end - . +. (** [hashmap::HashMap::{0}::get_in_list] *) Fixpoint hash_map_get_in_list_fwd @@ -305,7 +305,7 @@ Fixpoint hash_map_get_in_list_fwd | ListNil => Fail_ Failure end end - . +. (** [hashmap::HashMap::{0}::get] *) Definition hash_map_get_fwd @@ -323,7 +323,7 @@ Definition hash_map_get_fwd Return t end end - . +. (** [hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hash_map_get_mut_in_list_fwd @@ -339,7 +339,7 @@ Fixpoint hash_map_get_mut_in_list_fwd | ListNil => Fail_ Failure end end - . +. (** [hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hash_map_get_mut_in_list_back @@ -359,7 +359,7 @@ Fixpoint hash_map_get_mut_in_list_back | ListNil => Fail_ Failure end end - . +. (** [hashmap::HashMap::{0}::get_mut] *) Definition hash_map_get_mut_fwd @@ -377,7 +377,7 @@ Definition hash_map_get_mut_fwd Return t end end - . +. (** [hashmap::HashMap::{0}::get_mut] *) Definition hash_map_get_mut_back @@ -398,7 +398,7 @@ Definition hash_map_get_mut_back Return (mkHash_map_t i p i0 v0) end end - . +. (** [hashmap::HashMap::{0}::remove_from_list] *) Fixpoint hash_map_remove_from_list_fwd @@ -419,7 +419,7 @@ Fixpoint hash_map_remove_from_list_fwd | ListNil => Return None end end - . +. (** [hashmap::HashMap::{0}::remove_from_list] *) Fixpoint hash_map_remove_from_list_back @@ -442,7 +442,7 @@ Fixpoint hash_map_remove_from_list_back | ListNil => Return ListNil end end - . +. (** [hashmap::HashMap::{0}::remove] *) Definition hash_map_remove_fwd @@ -461,11 +461,11 @@ Definition hash_map_remove_fwd x <- hash_map_remove_from_list_fwd T n0 key l; match x with | None => Return None - | Some x0 => i2 <- usize_sub i 1 %usize; let _ := i2 in Return (Some x0) + | Some x0 => i2 <- usize_sub i 1%usize; let _ := i2 in Return (Some x0) end end end - . +. (** [hashmap::HashMap::{0}::remove] *) Definition hash_map_remove_back @@ -488,14 +488,14 @@ Definition hash_map_remove_back v0 <- vec_index_mut_back (List_t T) v hash_mod l0; Return (mkHash_map_t i p i0 v0) | Some x0 => - i2 <- usize_sub i 1 %usize; + i2 <- usize_sub i 1%usize; l0 <- hash_map_remove_from_list_back T n0 key l; v0 <- vec_index_mut_back (List_t T) v hash_mod l0; Return (mkHash_map_t i2 p i0 v0) end end end - . +. (** [hashmap::test1] *) Definition test1_fwd (n : nat) : result unit := @@ -503,39 +503,39 @@ Definition test1_fwd (n : nat) : result unit := | O => Fail_ OutOfFuel | S n0 => hm <- hash_map_new_fwd u64 n0; - hm0 <- hash_map_insert_fwd_back u64 n0 hm (0 %usize) (42 %u64); - hm1 <- hash_map_insert_fwd_back u64 n0 hm0 (128 %usize) (18 %u64); - hm2 <- hash_map_insert_fwd_back u64 n0 hm1 (1024 %usize) (138 %u64); - hm3 <- hash_map_insert_fwd_back u64 n0 hm2 (1056 %usize) (256 %u64); - i <- hash_map_get_fwd u64 n0 hm3 (128 %usize); - if negb (i s= 18 %u64) + hm0 <- hash_map_insert_fwd_back u64 n0 hm (0%usize) (42%u64); + hm1 <- hash_map_insert_fwd_back u64 n0 hm0 (128%usize) (18%u64); + hm2 <- hash_map_insert_fwd_back u64 n0 hm1 (1024%usize) (138%u64); + hm3 <- hash_map_insert_fwd_back u64 n0 hm2 (1056%usize) (256%u64); + i <- hash_map_get_fwd u64 n0 hm3 (128%usize); + if negb (i s= 18%u64) then Fail_ Failure else ( - hm4 <- hash_map_get_mut_back u64 n0 hm3 (1024 %usize) (56 %u64); - i0 <- hash_map_get_fwd u64 n0 hm4 (1024 %usize); - if negb (i0 s= 56 %u64) + hm4 <- hash_map_get_mut_back u64 n0 hm3 (1024%usize) (56%u64); + i0 <- hash_map_get_fwd u64 n0 hm4 (1024%usize); + if negb (i0 s= 56%u64) then Fail_ Failure else ( - x <- hash_map_remove_fwd u64 n0 hm4 (1024 %usize); + x <- hash_map_remove_fwd u64 n0 hm4 (1024%usize); match x with | None => Fail_ Failure | Some x0 => - if negb (x0 s= 56 %u64) + if negb (x0 s= 56%u64) then Fail_ Failure else ( - hm5 <- hash_map_remove_back u64 n0 hm4 (1024 %usize); - i1 <- hash_map_get_fwd u64 n0 hm5 (0 %usize); - if negb (i1 s= 42 %u64) + hm5 <- hash_map_remove_back u64 n0 hm4 (1024%usize); + i1 <- hash_map_get_fwd u64 n0 hm5 (0%usize); + if negb (i1 s= 42%u64) then Fail_ Failure else ( - i2 <- hash_map_get_fwd u64 n0 hm5 (128 %usize); - if negb (i2 s= 18 %u64) + i2 <- hash_map_get_fwd u64 n0 hm5 (128%usize); + if negb (i2 s= 18%u64) then Fail_ Failure else ( - i3 <- hash_map_get_fwd u64 n0 hm5 (1056 %usize); - if negb (i3 s= 256 %u64) then Fail_ Failure else Return tt))) + i3 <- hash_map_get_fwd u64 n0 hm5 (1056%usize); + if negb (i3 s= 256%u64) then Fail_ Failure else Return tt))) end)) end - . +. End Hashmap__Funs . diff --git a/tests/coq/hashmap/Hashmap__Types.v b/tests/coq/hashmap/Hashmap__Types.v index b665179e..e1add060 100644 --- a/tests/coq/hashmap/Hashmap__Types.v +++ b/tests/coq/hashmap/Hashmap__Types.v @@ -4,7 +4,7 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Module Hashmap__Types . +Module Hashmap__Types. (** [hashmap::List] *) Inductive List_t (T : Type) := @@ -12,13 +12,12 @@ Inductive List_t (T : Type) := | ListNil : List_t T . -Arguments ListCons {T} _ _ _ . -Arguments ListNil {T} . +Arguments ListCons {T} _ _ _. +Arguments ListNil {T}. (** [hashmap::HashMap] *) Record Hash_map_t (T : Type) := -mkHash_map_t -{ +mkHash_map_t { Hash_map_num_entries : usize; Hash_map_max_load_factor : (usize * usize); Hash_map_max_load : usize; @@ -26,14 +25,14 @@ mkHash_map_t } . -Arguments mkHash_map_t {T} _ _ _ _ . -Arguments Hash_map_num_entries {T} . -Arguments Hash_map_max_load_factor {T} . -Arguments Hash_map_max_load {T} . -Arguments Hash_map_slots {T} . +Arguments mkHash_map_t {T} _ _ _ _. +Arguments Hash_map_num_entries {T}. +Arguments Hash_map_max_load_factor {T}. +Arguments Hash_map_max_load {T}. +Arguments Hash_map_slots {T}. (** [core::num::u32::{9}::MAX] *) -Definition core_num_u32_max_body : result u32 := Return (4294967295 %u32) . -Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global . +Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). +Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. End Hashmap__Types . diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Funs.v b/tests/coq/hashmap_on_disk/HashmapMain__Funs.v index c390ac1d..249adbe9 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain__Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain__Funs.v @@ -4,14 +4,14 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export HashmapMain__Types . -Import HashmapMain__Types . -Require Export HashmapMain__Opaque . -Import HashmapMain__Opaque . -Module HashmapMain__Funs . +Require Export HashmapMain__Types. +Import HashmapMain__Types. +Require Export HashmapMain__Opaque. +Import HashmapMain__Opaque. +Module HashmapMain__Funs. (** [hashmap_main::hashmap::hash_key] *) -Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k . +Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k. (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) Fixpoint hashmap_hash_map_allocate_slots_fwd @@ -21,15 +21,15 @@ Fixpoint hashmap_hash_map_allocate_slots_fwd match n with | O => Fail_ OutOfFuel | S n1 => - if n0 s= 0 %usize + if n0 s= 0%usize then Return slots else ( slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil; - i <- usize_sub n0 1 %usize; + i <- usize_sub n0 1%usize; v <- hashmap_hash_map_allocate_slots_fwd T n1 slots0 i; Return v) end - . +. (** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *) Definition hashmap_hash_map_new_with_capacity_fwd @@ -44,10 +44,10 @@ Definition hashmap_hash_map_new_with_capacity_fwd slots <- hashmap_hash_map_allocate_slots_fwd T n0 v capacity; i <- usize_mul capacity max_load_dividend; i0 <- usize_div i max_load_divisor; - Return (mkHashmap_hash_map_t (0 %usize) (max_load_dividend, + Return (mkHashmap_hash_map_t (0%usize) (max_load_dividend, max_load_divisor) i0 slots) end - . +. (** [hashmap_main::hashmap::HashMap::{0}::new] *) Definition hashmap_hash_map_new_fwd @@ -56,11 +56,11 @@ Definition hashmap_hash_map_new_fwd | O => Fail_ OutOfFuel | S n0 => hm <- - hashmap_hash_map_new_with_capacity_fwd T n0 (32 %usize) (4 %usize) (5 - %usize); + hashmap_hash_map_new_with_capacity_fwd T n0 (32%usize) (4%usize) + (5%usize); Return hm end - . +. (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) Fixpoint hashmap_hash_map_clear_slots_fwd_back @@ -74,12 +74,12 @@ Fixpoint hashmap_hash_map_clear_slots_fwd_back if i s< i0 then ( slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil; - i1 <- usize_add i 1 %usize; + i1 <- usize_add i 1%usize; slots1 <- hashmap_hash_map_clear_slots_fwd_back T n0 slots0 i1; Return slots1) else Return slots end - . +. (** [hashmap_main::hashmap::HashMap::{0}::clear] *) Definition hashmap_hash_map_clear_fwd_back @@ -91,16 +91,17 @@ Definition hashmap_hash_map_clear_fwd_back | S n0 => match self with | mkHashmap_hash_map_t i p i0 v => - v0 <- hashmap_hash_map_clear_slots_fwd_back T n0 v (0 %usize); - Return (mkHashmap_hash_map_t (0 %usize) p i0 v0) + v0 <- hashmap_hash_map_clear_slots_fwd_back T n0 v (0%usize); + Return (mkHashmap_hash_map_t (0%usize) p i0 v0) end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::len] *) Definition hashmap_hash_map_len_fwd (T : Type) (self : Hashmap_hash_map_t T) : result usize := - match self with | mkHashmap_hash_map_t i p i0 v => Return i end . + match self with | mkHashmap_hash_map_t i p i0 v => Return i end +. (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) Fixpoint hashmap_hash_map_insert_in_list_fwd @@ -119,7 +120,7 @@ Fixpoint hashmap_hash_map_insert_in_list_fwd | HashmapListNil => Return true end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) Fixpoint hashmap_hash_map_insert_in_list_back @@ -140,11 +141,12 @@ Fixpoint hashmap_hash_map_insert_in_list_back let l := HashmapListNil in Return (HashmapListCons key value l) end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *) Definition hashmap_hash_map_insert_no_resize_fwd_back - (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T) : + (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T) + : result (Hashmap_hash_map_t T) := match n with @@ -159,7 +161,7 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back inserted <- hashmap_hash_map_insert_in_list_fwd T n0 key value l; if inserted then ( - i2 <- usize_add i 1 %usize; + i2 <- usize_add i 1%usize; l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l; v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0; Return (mkHashmap_hash_map_t i2 p i0 v0)) @@ -169,15 +171,16 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back Return (mkHashmap_hash_map_t i p i0 v0)) end end - . +. (** [core::num::u32::{9}::MAX] *) -Definition core_num_u32_max_body : result u32 := Return (4294967295 %u32) . -Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global . +Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). +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_fwd_back - (T : Type) (n : nat) (ntable : 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 @@ -192,7 +195,7 @@ Fixpoint hashmap_hash_map_move_elements_from_list_fwd_back | HashmapListNil => Return ntable end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) Fixpoint hashmap_hash_map_move_elements_fwd_back @@ -212,13 +215,13 @@ Fixpoint hashmap_hash_map_move_elements_fwd_back hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable ls; let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0; - i1 <- usize_add i 1 %usize; + i1 <- usize_add i 1%usize; p <- hashmap_hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1; let (ntable1, slots1) := p in Return (ntable1, slots1)) else Return (ntable, slots) end - . +. (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) Definition hashmap_hash_map_try_resize_fwd_back @@ -232,14 +235,14 @@ Definition hashmap_hash_map_try_resize_fwd_back match self with | mkHashmap_hash_map_t i p i0 v => let capacity := vec_len (Hashmap_list_t T) v in - n1 <- usize_div max_usize 2 %usize; + n1 <- usize_div max_usize 2%usize; let (i1, i2) := p in i3 <- usize_div n1 i1; if capacity s<= i3 then ( - i4 <- usize_mul capacity 2 %usize; + i4 <- usize_mul capacity 2%usize; ntable <- hashmap_hash_map_new_with_capacity_fwd T n0 i4 i1 i2; - p0 <- hashmap_hash_map_move_elements_fwd_back T n0 ntable v (0 %usize); + p0 <- hashmap_hash_map_move_elements_fwd_back T n0 ntable v (0%usize); let (ntable0, _) := p0 in match ntable0 with | mkHashmap_hash_map_t i5 p1 i6 v0 => @@ -248,11 +251,12 @@ Definition hashmap_hash_map_try_resize_fwd_back else Return (mkHashmap_hash_map_t i (i1, i2) i0 v) end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::insert] *) Definition hashmap_hash_map_insert_fwd_back - (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T) : + (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T) + : result (Hashmap_hash_map_t T) := match n with @@ -271,7 +275,7 @@ Definition hashmap_hash_map_insert_fwd_back else Return (mkHashmap_hash_map_t i0 p i1 v) end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) Fixpoint hashmap_hash_map_contains_key_in_list_fwd @@ -288,7 +292,7 @@ Fixpoint hashmap_hash_map_contains_key_in_list_fwd | HashmapListNil => Return false end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::contains_key] *) Definition hashmap_hash_map_contains_key_fwd @@ -308,7 +312,7 @@ Definition hashmap_hash_map_contains_key_fwd Return b end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) Fixpoint hashmap_hash_map_get_in_list_fwd @@ -324,7 +328,7 @@ Fixpoint hashmap_hash_map_get_in_list_fwd | HashmapListNil => Fail_ Failure end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::get] *) Definition hashmap_hash_map_get_fwd @@ -344,7 +348,7 @@ Definition hashmap_hash_map_get_fwd Return t end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hashmap_hash_map_get_mut_in_list_fwd @@ -360,7 +364,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_fwd | HashmapListNil => Fail_ Failure end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hashmap_hash_map_get_mut_in_list_back @@ -380,7 +384,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_back | HashmapListNil => Fail_ Failure end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) Definition hashmap_hash_map_get_mut_fwd @@ -400,7 +404,7 @@ Definition hashmap_hash_map_get_mut_fwd Return t end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) Definition hashmap_hash_map_get_mut_back @@ -421,7 +425,7 @@ Definition hashmap_hash_map_get_mut_back Return (mkHashmap_hash_map_t i p i0 v0) end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) Fixpoint hashmap_hash_map_remove_from_list_fwd @@ -447,7 +451,7 @@ Fixpoint hashmap_hash_map_remove_from_list_fwd | HashmapListNil => Return None end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) Fixpoint hashmap_hash_map_remove_from_list_back @@ -474,7 +478,7 @@ Fixpoint hashmap_hash_map_remove_from_list_back | HashmapListNil => Return HashmapListNil end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::remove] *) Definition hashmap_hash_map_remove_fwd @@ -493,11 +497,11 @@ Definition hashmap_hash_map_remove_fwd x <- hashmap_hash_map_remove_from_list_fwd T n0 key l; match x with | None => Return None - | Some x0 => i2 <- usize_sub i 1 %usize; let _ := i2 in Return (Some x0) + | Some x0 => i2 <- usize_sub i 1%usize; let _ := i2 in Return (Some x0) end end end - . +. (** [hashmap_main::hashmap::HashMap::{0}::remove] *) Definition hashmap_hash_map_remove_back @@ -520,14 +524,14 @@ Definition hashmap_hash_map_remove_back v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0; Return (mkHashmap_hash_map_t i p i0 v0) | Some x0 => - i2 <- usize_sub i 1 %usize; + i2 <- usize_sub i 1%usize; l0 <- hashmap_hash_map_remove_from_list_back T n0 key l; v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0; Return (mkHashmap_hash_map_t i2 p i0 v0) end end end - . +. (** [hashmap_main::hashmap::test1] *) Definition hashmap_test1_fwd (n : nat) : result unit := @@ -535,42 +539,40 @@ Definition hashmap_test1_fwd (n : nat) : result unit := | O => Fail_ OutOfFuel | S n0 => hm <- hashmap_hash_map_new_fwd u64 n0; - hm0 <- hashmap_hash_map_insert_fwd_back u64 n0 hm (0 %usize) (42 %u64); - hm1 <- hashmap_hash_map_insert_fwd_back u64 n0 hm0 (128 %usize) (18 %u64); - hm2 <- - hashmap_hash_map_insert_fwd_back u64 n0 hm1 (1024 %usize) (138 %u64); - hm3 <- - hashmap_hash_map_insert_fwd_back u64 n0 hm2 (1056 %usize) (256 %u64); - i <- hashmap_hash_map_get_fwd u64 n0 hm3 (128 %usize); - if negb (i s= 18 %u64) + hm0 <- hashmap_hash_map_insert_fwd_back u64 n0 hm (0%usize) (42%u64); + hm1 <- hashmap_hash_map_insert_fwd_back u64 n0 hm0 (128%usize) (18%u64); + hm2 <- hashmap_hash_map_insert_fwd_back u64 n0 hm1 (1024%usize) (138%u64); + hm3 <- hashmap_hash_map_insert_fwd_back u64 n0 hm2 (1056%usize) (256%u64); + i <- hashmap_hash_map_get_fwd u64 n0 hm3 (128%usize); + if negb (i s= 18%u64) then Fail_ Failure else ( - hm4 <- hashmap_hash_map_get_mut_back u64 n0 hm3 (1024 %usize) (56 %u64); - i0 <- hashmap_hash_map_get_fwd u64 n0 hm4 (1024 %usize); - if negb (i0 s= 56 %u64) + hm4 <- hashmap_hash_map_get_mut_back u64 n0 hm3 (1024%usize) (56%u64); + i0 <- hashmap_hash_map_get_fwd u64 n0 hm4 (1024%usize); + if negb (i0 s= 56%u64) then Fail_ Failure else ( - x <- hashmap_hash_map_remove_fwd u64 n0 hm4 (1024 %usize); + x <- hashmap_hash_map_remove_fwd u64 n0 hm4 (1024%usize); match x with | None => Fail_ Failure | Some x0 => - if negb (x0 s= 56 %u64) + if negb (x0 s= 56%u64) then Fail_ Failure else ( - hm5 <- hashmap_hash_map_remove_back u64 n0 hm4 (1024 %usize); - i1 <- hashmap_hash_map_get_fwd u64 n0 hm5 (0 %usize); - if negb (i1 s= 42 %u64) + hm5 <- hashmap_hash_map_remove_back u64 n0 hm4 (1024%usize); + i1 <- hashmap_hash_map_get_fwd u64 n0 hm5 (0%usize); + if negb (i1 s= 42%u64) then Fail_ Failure else ( - i2 <- hashmap_hash_map_get_fwd u64 n0 hm5 (128 %usize); - if negb (i2 s= 18 %u64) + i2 <- hashmap_hash_map_get_fwd u64 n0 hm5 (128%usize); + if negb (i2 s= 18%u64) then Fail_ Failure else ( - i3 <- hashmap_hash_map_get_fwd u64 n0 hm5 (1056 %usize); - if negb (i3 s= 256 %u64) then Fail_ Failure else Return tt))) + i3 <- hashmap_hash_map_get_fwd u64 n0 hm5 (1056%usize); + if negb (i3 s= 256%u64) then Fail_ Failure else Return tt))) end)) end - . +. (** [hashmap_main::insert_on_disk] *) Definition insert_on_disk_fwd @@ -585,10 +587,10 @@ Definition insert_on_disk_fwd let (st1, _) := p0 in Return (st1, tt) end - . +. (** [hashmap_main::main] *) -Definition main_fwd : result unit := Return tt . +Definition main_fwd : result unit := Return tt. (** Unit test for [hashmap_main::main] *) Check (main_fwd )%return. diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v index f41c3ddf..4b6db927 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v +++ b/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v @@ -4,18 +4,18 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export HashmapMain__Types . -Import HashmapMain__Types . -Module HashmapMain__Opaque . +Require Export HashmapMain__Types. +Import HashmapMain__Types. +Module HashmapMain__Opaque. (** [hashmap_main::hashmap_utils::deserialize] *) Axiom hashmap_utils_deserialize_fwd : state -> result (state * (Hashmap_hash_map_t u64)) - . +. (** [hashmap_main::hashmap_utils::serialize] *) Axiom hashmap_utils_serialize_fwd : Hashmap_hash_map_t u64 -> state -> result (state * unit) - . +. End HashmapMain__Opaque . diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Types.v b/tests/coq/hashmap_on_disk/HashmapMain__Types.v index 8bdbd0bd..5d609937 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain__Types.v +++ b/tests/coq/hashmap_on_disk/HashmapMain__Types.v @@ -4,7 +4,7 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Module HashmapMain__Types . +Module HashmapMain__Types. (** [hashmap_main::hashmap::List] *) Inductive Hashmap_list_t (T : Type) := @@ -12,13 +12,12 @@ Inductive Hashmap_list_t (T : Type) := | HashmapListNil : Hashmap_list_t T . -Arguments HashmapListCons {T} _ _ _ . -Arguments HashmapListNil {T} . +Arguments HashmapListCons {T} _ _ _. +Arguments HashmapListNil {T}. (** [hashmap_main::hashmap::HashMap] *) Record Hashmap_hash_map_t (T : Type) := -mkHashmap_hash_map_t -{ +mkHashmap_hash_map_t { Hashmap_hash_map_num_entries : usize; Hashmap_hash_map_max_load_factor : (usize * usize); Hashmap_hash_map_max_load : usize; @@ -26,15 +25,15 @@ mkHashmap_hash_map_t } . -Arguments mkHashmap_hash_map_t {T} _ _ _ _ . -Arguments Hashmap_hash_map_num_entries {T} . -Arguments Hashmap_hash_map_max_load_factor {T} . -Arguments Hashmap_hash_map_max_load {T} . -Arguments Hashmap_hash_map_slots {T} . +Arguments mkHashmap_hash_map_t {T} _ _ _ _. +Arguments Hashmap_hash_map_num_entries {T}. +Arguments Hashmap_hash_map_max_load_factor {T}. +Arguments Hashmap_hash_map_max_load {T}. +Arguments Hashmap_hash_map_slots {T}. (** [core::num::u32::{9}::MAX] *) -Definition core_num_u32_max_body : result u32 := Return (4294967295 %u32) . -Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global . +Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). +Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. (** The state type used in the state-error monad *) Axiom state : Type. |