From 08530a51b8861e3dbb1a409d0c6f0e8c44adec83 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 16 Nov 2022 15:02:40 +0100 Subject: Do not introduce match on the fuel for non-recursive functions --- tests/coq/betree/BetreeMain_Funs.v | 445 +++++++++++---------------- tests/coq/hashmap/Hashmap_Funs.v | 316 ++++++++----------- tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 383 ++++++++++------------- 3 files changed, 477 insertions(+), 667 deletions(-) (limited to 'tests') diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index d60ef718..ddcff646 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -218,28 +218,24 @@ Definition betree_leaf_split_fwd (st : state) : result (state * Betree_internal_t) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- - betree_list_split_at_fwd (u64 * u64) n0 content - params.(Betree_params_split_size); - let (content0, content1) := p in - p0 <- betree_list_hd_fwd (u64 * u64) content1; - let (pivot, _) := p0 in - id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; - node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; - id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; - p1 <- betree_store_leaf_node_fwd id0 content0 st; - let (st0, _) := p1 in - p2 <- betree_store_leaf_node_fwd id1 content1 st0; - let (st1, _) := p2 in - let n1 := BetreeNodeLeaf (mkBetree_leaf_t id0 - params.(Betree_params_split_size)) in - let n2 := BetreeNodeLeaf (mkBetree_leaf_t id1 - params.(Betree_params_split_size)) in - Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n1 n2) - end + p <- + betree_list_split_at_fwd (u64 * u64) n content + params.(Betree_params_split_size); + let (content0, content1) := p in + p0 <- betree_list_hd_fwd (u64 * u64) content1; + let (pivot, _) := p0 in + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + p1 <- betree_store_leaf_node_fwd id0 content0 st; + let (st0, _) := p1 in + p2 <- betree_store_leaf_node_fwd id1 content1 st0; + let (st1, _) := p2 in + let n0 := BetreeNodeLeaf (mkBetree_leaf_t id0 + params.(Betree_params_split_size)) in + let n1 := BetreeNodeLeaf (mkBetree_leaf_t id1 + params.(Betree_params_split_size)) in + Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n0 n1) . (** [betree_main::betree::Leaf::{3}::split] *) @@ -249,25 +245,21 @@ Definition betree_leaf_split_back (st : state) : result Betree_node_id_counter_t := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- - betree_list_split_at_fwd (u64 * u64) n0 content - params.(Betree_params_split_size); - let (content0, content1) := p in - p0 <- betree_list_hd_fwd (u64 * u64) content1; - let _ := p0 in - id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; - node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; - id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; - p1 <- betree_store_leaf_node_fwd id0 content0 st; - let (st0, _) := p1 in - p2 <- betree_store_leaf_node_fwd id1 content1 st0; - let (_, _) := p2 in - node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0; - Return node_id_cnt1 - end + p <- + betree_list_split_at_fwd (u64 * u64) n content + params.(Betree_params_split_size); + let (content0, content1) := p in + p0 <- betree_list_hd_fwd (u64 * u64) content1; + let _ := p0 in + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + p1 <- betree_store_leaf_node_fwd id0 content0 st; + let (st0, _) := p1 in + p2 <- betree_store_leaf_node_fwd id1 content1 st0; + let (_, _) := p2 in + node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0; + Return node_id_cnt1 . (** [betree_main::betree::Node::{5}::lookup_in_bindings] *) @@ -641,58 +633,54 @@ Definition betree_node_apply_to_leaf_fwd_back (new_msg : Betree_message_t) : result (Betree_list_t (u64 * u64)) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - bindings0 <- betree_node_lookup_mut_in_bindings_fwd n0 key bindings; - b <- betree_list_head_has_key_fwd u64 bindings0 key; - if b - then ( - hd <- betree_list_pop_front_fwd (u64 * u64) bindings0; - match new_msg with - | BetreeMessageInsert v => - bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; - bindings2 <- - betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); - bindings3 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2; - Return bindings3 - | BetreeMessageDelete => - bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; - bindings2 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; - Return bindings2 - | BetreeMessageUpsert s => - let (_, i) := hd in - v <- betree_upsert_update_fwd (Some i) s; - bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; - bindings2 <- - betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); - bindings3 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2; - Return bindings3 - end) - else - match new_msg with - | BetreeMessageInsert v => - bindings1 <- - betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); - bindings2 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; - Return bindings2 - | BetreeMessageDelete => - bindings1 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings0; - Return bindings1 - | BetreeMessageUpsert s => - v <- betree_upsert_update_fwd None s; - bindings1 <- - betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); - bindings2 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; - Return bindings2 - end - end + bindings0 <- betree_node_lookup_mut_in_bindings_fwd n key bindings; + b <- betree_list_head_has_key_fwd u64 bindings0 key; + if b + then ( + hd <- betree_list_pop_front_fwd (u64 * u64) bindings0; + match new_msg with + | BetreeMessageInsert v => + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); + bindings3 <- + betree_node_lookup_mut_in_bindings_back n key bindings bindings2; + Return bindings3 + | BetreeMessageDelete => + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_node_lookup_mut_in_bindings_back n key bindings bindings1; + Return bindings2 + | BetreeMessageUpsert s => + let (_, i) := hd in + v <- betree_upsert_update_fwd (Some i) s; + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); + bindings3 <- + betree_node_lookup_mut_in_bindings_back n key bindings bindings2; + Return bindings3 + end) + else + match new_msg with + | BetreeMessageInsert v => + bindings1 <- + betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); + bindings2 <- + betree_node_lookup_mut_in_bindings_back n key bindings bindings1; + Return bindings2 + | BetreeMessageDelete => + bindings1 <- + betree_node_lookup_mut_in_bindings_back n key bindings bindings0; + Return bindings1 + | BetreeMessageUpsert s => + v <- betree_upsert_update_fwd None s; + bindings1 <- + betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); + bindings2 <- + betree_node_lookup_mut_in_bindings_back n key bindings bindings1; + Return bindings2 + end . (** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *) @@ -790,71 +778,65 @@ Definition betree_node_apply_to_internal_fwd_back (new_msg : Betree_message_t) : result (Betree_list_t (u64 * Betree_message_t)) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - msgs0 <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; - b <- betree_list_head_has_key_fwd Betree_message_t msgs0 key; - if b - then - match new_msg with - | BetreeMessageInsert i => - msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + msgs0 <- betree_node_lookup_first_message_for_key_fwd n key msgs; + b <- betree_list_head_has_key_fwd Betree_message_t msgs0 key; + if b + then + match new_msg with + | BetreeMessageInsert i => + msgs1 <- betree_node_filter_messages_for_key_fwd_back n key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, + BetreeMessageInsert i); + msgs3 <- betree_node_lookup_first_message_for_key_back n key msgs msgs2; + Return msgs3 + | BetreeMessageDelete => + msgs1 <- betree_node_filter_messages_for_key_fwd_back n key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, + BetreeMessageDelete); + msgs3 <- betree_node_lookup_first_message_for_key_back n key msgs msgs2; + Return msgs3 + | BetreeMessageUpsert s => + p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0; + let (_, m) := p in + match m with + | BetreeMessageInsert prev => + v <- betree_upsert_update_fwd (Some prev) s; + msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; msgs2 <- betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, - BetreeMessageInsert i); + BetreeMessageInsert v); msgs3 <- - betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + betree_node_lookup_first_message_for_key_back n key msgs msgs2; Return msgs3 | BetreeMessageDelete => - msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + v <- betree_upsert_update_fwd None s; + msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; msgs2 <- betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, - BetreeMessageDelete); + BetreeMessageInsert v); msgs3 <- - betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + betree_node_lookup_first_message_for_key_back n key msgs msgs2; Return msgs3 - | BetreeMessageUpsert s => - p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0; - let (_, m) := p in - match m with - | BetreeMessageInsert prev => - v <- betree_upsert_update_fwd (Some prev) s; - msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; - msgs2 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 - (key, BetreeMessageInsert v); - msgs3 <- - betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; - Return msgs3 - | BetreeMessageDelete => - v <- betree_upsert_update_fwd None s; - msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; - msgs2 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 - (key, BetreeMessageInsert v); - msgs3 <- - betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; - Return msgs3 - | BetreeMessageUpsert ufs => - msgs1 <- betree_node_lookup_first_message_after_key_fwd n0 key msgs0; - msgs2 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 - (key, BetreeMessageUpsert s); - msgs3 <- - betree_node_lookup_first_message_after_key_back n0 key msgs0 msgs2; - msgs4 <- - betree_node_lookup_first_message_for_key_back n0 key msgs msgs3; - Return msgs4 - end + | BetreeMessageUpsert ufs => + msgs1 <- betree_node_lookup_first_message_after_key_fwd n key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, + BetreeMessageUpsert s); + msgs3 <- + betree_node_lookup_first_message_after_key_back n key msgs0 msgs2; + msgs4 <- + betree_node_lookup_first_message_for_key_back n key msgs msgs3; + Return msgs4 end - else ( - msgs1 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key, - new_msg); - msgs2 <- betree_node_lookup_first_message_for_key_back n0 key msgs msgs1; - Return msgs2) - end + end + else ( + msgs1 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key, + new_msg); + msgs2 <- betree_node_lookup_first_message_for_key_back n key msgs msgs1; + Return msgs2) . (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) @@ -1099,20 +1081,16 @@ Definition betree_node_apply_fwd (new_msg : Betree_message_t) (st : state) : result (state * unit) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - let l := BetreeListNil in - p <- - betree_node_apply_messages_fwd n0 self params node_id_cnt (BetreeListCons - (key, new_msg) l) st; - let (st0, _) := p in - p0 <- - betree_node_apply_messages_back n0 self params node_id_cnt - (BetreeListCons (key, new_msg) l) st; - let (_, _) := p0 in - Return (st0, tt) - end + let l := BetreeListNil in + p <- + betree_node_apply_messages_fwd n self params node_id_cnt (BetreeListCons + (key, new_msg) l) st; + let (st0, _) := p in + p0 <- + betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons + (key, new_msg) l) st; + let (_, _) := p0 in + Return (st0, tt) . (** [betree_main::betree::Node::{5}::apply] *) @@ -1122,16 +1100,12 @@ Definition betree_node_apply_back (new_msg : Betree_message_t) (st : state) : result (Betree_node_t * Betree_node_id_counter_t) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - let l := BetreeListNil in - p <- - betree_node_apply_messages_back n0 self params node_id_cnt - (BetreeListCons (key, new_msg) l) st; - let (self0, node_id_cnt0) := p in - Return (self0, node_id_cnt0) - end + let l := BetreeListNil in + p <- + betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons + (key, new_msg) l) st; + let (self0, node_id_cnt0) := p in + Return (self0, node_id_cnt0) . (** [betree_main::betree::BeTree::{6}::new] *) @@ -1154,21 +1128,15 @@ Definition betree_be_tree_apply_fwd (st : state) : result (state * unit) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- - betree_node_apply_fwd n0 self.(Betree_be_tree_root) - self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg - st; - let (st0, _) := p in - p0 <- - betree_node_apply_back n0 self.(Betree_be_tree_root) - self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg - st; - let (_, _) := p0 in - Return (st0, tt) - end + p <- + betree_node_apply_fwd n self.(Betree_be_tree_root) + self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st; + let (st0, _) := p in + p0 <- + betree_node_apply_back n self.(Betree_be_tree_root) + self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st; + let (_, _) := p0 in + Return (st0, tt) . (** [betree_main::betree::BeTree::{6}::apply] *) @@ -1177,16 +1145,11 @@ Definition betree_be_tree_apply_back (st : state) : result Betree_be_tree_t := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- - betree_node_apply_back n0 self.(Betree_be_tree_root) - self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg - st; - let (n1, nic) := p in - Return (mkBetree_be_tree_t self.(Betree_be_tree_params) nic n1) - end + p <- + betree_node_apply_back n self.(Betree_be_tree_root) + self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st; + let (n0, nic) := p in + Return (mkBetree_be_tree_t self.(Betree_be_tree_params) nic n0) . (** [betree_main::betree::BeTree::{6}::insert] *) @@ -1194,15 +1157,11 @@ Definition betree_be_tree_insert_fwd (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : result (state * unit) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageInsert value) st; - let (st0, _) := p in - bt <- betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st; - let _ := bt in - Return (st0, tt) - end + p <- betree_be_tree_apply_fwd n self key (BetreeMessageInsert value) st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st; + let _ := bt in + Return (st0, tt) . (** [betree_main::betree::BeTree::{6}::insert] *) @@ -1210,13 +1169,8 @@ Definition betree_be_tree_insert_back (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : result Betree_be_tree_t := - match n with - | O => Fail_ OutOfFuel - | S n0 => - self0 <- - betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st; - Return self0 - end + self0 <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st; + Return self0 . (** [betree_main::betree::BeTree::{6}::delete] *) @@ -1224,15 +1178,11 @@ Definition betree_be_tree_delete_fwd (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : result (state * unit) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- betree_be_tree_apply_fwd n0 self key BetreeMessageDelete st; - let (st0, _) := p in - bt <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st; - let _ := bt in - Return (st0, tt) - end + p <- betree_be_tree_apply_fwd n self key BetreeMessageDelete st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n self key BetreeMessageDelete st; + let _ := bt in + Return (st0, tt) . (** [betree_main::betree::BeTree::{6}::delete] *) @@ -1240,12 +1190,8 @@ Definition betree_be_tree_delete_back (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : result Betree_be_tree_t := - match n with - | O => Fail_ OutOfFuel - | S n0 => - self0 <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st; - Return self0 - end + self0 <- betree_be_tree_apply_back n self key BetreeMessageDelete st; + Return self0 . (** [betree_main::betree::BeTree::{6}::upsert] *) @@ -1254,15 +1200,11 @@ Definition betree_be_tree_upsert_fwd (upd : Betree_upsert_fun_state_t) (st : state) : result (state * unit) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageUpsert upd) st; - let (st0, _) := p in - bt <- betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st; - let _ := bt in - Return (st0, tt) - end + p <- betree_be_tree_apply_fwd n self key (BetreeMessageUpsert upd) st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st; + let _ := bt in + Return (st0, tt) . (** [betree_main::betree::BeTree::{6}::upsert] *) @@ -1271,13 +1213,8 @@ Definition betree_be_tree_upsert_back (upd : Betree_upsert_fun_state_t) (st : state) : result Betree_be_tree_t := - match n with - | O => Fail_ OutOfFuel - | S n0 => - self0 <- - betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st; - Return self0 - end + self0 <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st; + Return self0 . (** [betree_main::betree::BeTree::{6}::lookup] *) @@ -1285,13 +1222,9 @@ Definition betree_be_tree_lookup_fwd (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : result (state * (option u64)) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- betree_node_lookup_fwd n0 self.(Betree_be_tree_root) key st; - let (st0, opt) := p in - Return (st0, opt) - end + p <- betree_node_lookup_fwd n self.(Betree_be_tree_root) key st; + let (st0, opt) := p in + Return (st0, opt) . (** [betree_main::betree::BeTree::{6}::lookup] *) @@ -1299,13 +1232,9 @@ Definition betree_be_tree_lookup_back (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : result Betree_be_tree_t := - match n with - | O => Fail_ OutOfFuel - | S n0 => - n1 <- betree_node_lookup_back n0 self.(Betree_be_tree_root) key st; - Return (mkBetree_be_tree_t self.(Betree_be_tree_params) - self.(Betree_be_tree_node_id_cnt) n1) - end + n0 <- betree_node_lookup_back n self.(Betree_be_tree_root) key st; + Return (mkBetree_be_tree_t self.(Betree_be_tree_params) + self.(Betree_be_tree_node_id_cnt) n0) . (** [betree_main::main] *) diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index d12ee1b9..17456d81 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -35,26 +35,18 @@ Definition hash_map_new_with_capacity_fwd (max_load_divisor : usize) : result (Hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - let v := vec_new (List_t T) in - 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 - slots) - end + let v := vec_new (List_t T) in + slots <- hash_map_allocate_slots_fwd T n 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 + slots) . (** [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); - Return hm - end + hm <- hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize); + Return hm . (** [hashmap::HashMap::{0}::clear_slots] *) @@ -79,13 +71,9 @@ Fixpoint hash_map_clear_slots_fwd_back (** [hashmap::HashMap::{0}::clear] *) Definition hash_map_clear_fwd_back (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - v <- hash_map_clear_slots_fwd_back T n0 self.(Hash_map_slots) (0%usize); - Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor) - self.(Hash_map_max_load) v) - end + v <- hash_map_clear_slots_fwd_back T n self.(Hash_map_slots) (0%usize); + Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor) + self.(Hash_map_max_load) v) . (** [hashmap::HashMap::{0}::len] *) @@ -136,27 +124,23 @@ Definition hash_map_insert_no_resize_fwd_back (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) : result (Hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hash_key_fwd key; - let i := vec_len (List_t T) self.(Hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; - inserted <- hash_map_insert_in_list_fwd T n0 key value l; - if inserted - then ( - i0 <- usize_add self.(Hash_map_num_entries) 1%usize; - l0 <- hash_map_insert_in_list_back T n0 key value l; - v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; - Return (mkHash_map_t i0 self.(Hash_map_max_load_factor) - self.(Hash_map_max_load) v)) - else ( - l0 <- hash_map_insert_in_list_back T n0 key value l; - v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; - Return (mkHash_map_t self.(Hash_map_num_entries) - self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)) - end + hash <- hash_key_fwd key; + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; + inserted <- hash_map_insert_in_list_fwd T n key value l; + if inserted + then ( + i0 <- usize_add self.(Hash_map_num_entries) 1%usize; + l0 <- hash_map_insert_in_list_back T n key value l; + v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; + Return (mkHash_map_t i0 self.(Hash_map_max_load_factor) + self.(Hash_map_max_load) v)) + else ( + l0 <- hash_map_insert_in_list_back T n key value l; + v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; + Return (mkHash_map_t self.(Hash_map_num_entries) + self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)) . (** [core::num::u32::{9}::MAX] *) @@ -209,28 +193,24 @@ Fixpoint hash_map_move_elements_fwd_back (** [hashmap::HashMap::{0}::try_resize] *) Definition hash_map_try_resize_fwd_back (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - max_usize <- scalar_cast U32 Usize core_num_u32_max_c; - let capacity := vec_len (List_t T) self.(Hash_map_slots) in - n1 <- usize_div max_usize 2%usize; - let (i, i0) := self.(Hash_map_max_load_factor) in - i1 <- usize_div n1 i; - if capacity s<= i1 - then ( - i2 <- usize_mul capacity 2%usize; - ntable <- hash_map_new_with_capacity_fwd T n0 i2 i i0; - p <- - hash_map_move_elements_fwd_back T n0 ntable self.(Hash_map_slots) - (0%usize); - let (ntable0, _) := p in - Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0) - ntable0.(Hash_map_max_load) ntable0.(Hash_map_slots))) - else - Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0) - self.(Hash_map_max_load) self.(Hash_map_slots)) - end + max_usize <- scalar_cast U32 Usize core_num_u32_max_c; + let capacity := vec_len (List_t T) self.(Hash_map_slots) in + n1 <- usize_div max_usize 2%usize; + let (i, i0) := self.(Hash_map_max_load_factor) in + i1 <- usize_div n1 i; + if capacity s<= i1 + then ( + i2 <- usize_mul capacity 2%usize; + ntable <- hash_map_new_with_capacity_fwd T n i2 i i0; + p <- + hash_map_move_elements_fwd_back T n ntable self.(Hash_map_slots) + (0%usize); + let (ntable0, _) := p in + Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0) + ntable0.(Hash_map_max_load) ntable0.(Hash_map_slots))) + else + Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0) + self.(Hash_map_max_load) self.(Hash_map_slots)) . (** [hashmap::HashMap::{0}::insert] *) @@ -238,15 +218,11 @@ Definition hash_map_insert_fwd_back (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (value : T) : result (Hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - self0 <- hash_map_insert_no_resize_fwd_back T n0 self key value; - i <- hash_map_len_fwd T self0; - if i s> self0.(Hash_map_max_load) - then (self1 <- hash_map_try_resize_fwd_back T n0 self0; Return self1) - else Return self0 - end + self0 <- hash_map_insert_no_resize_fwd_back T n self key value; + i <- hash_map_len_fwd T self0; + if i s> self0.(Hash_map_max_load) + then (self1 <- hash_map_try_resize_fwd_back T n self0; Return self1) + else Return self0 . (** [hashmap::HashMap::{0}::contains_key_in_list] *) @@ -268,16 +244,12 @@ Fixpoint hash_map_contains_key_in_list_fwd (** [hashmap::HashMap::{0}::contains_key] *) Definition hash_map_contains_key_fwd (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result bool := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hash_key_fwd key; - let i := vec_len (List_t T) self.(Hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod; - b <- hash_map_contains_key_in_list_fwd T n0 key l; - Return b - end + hash <- hash_key_fwd key; + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod; + b <- hash_map_contains_key_in_list_fwd T n key l; + Return b . (** [hashmap::HashMap::{0}::get_in_list] *) @@ -299,16 +271,12 @@ Fixpoint hash_map_get_in_list_fwd (** [hashmap::HashMap::{0}::get] *) Definition hash_map_get_fwd (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hash_key_fwd key; - let i := vec_len (List_t T) self.(Hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod; - t <- hash_map_get_in_list_fwd T n0 key l; - Return t - end + hash <- hash_key_fwd key; + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod; + t <- hash_map_get_in_list_fwd T n key l; + Return t . (** [hashmap::HashMap::{0}::get_mut_in_list] *) @@ -350,16 +318,12 @@ Fixpoint hash_map_get_mut_in_list_back (** [hashmap::HashMap::{0}::get_mut] *) Definition hash_map_get_mut_fwd (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result T := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hash_key_fwd key; - let i := vec_len (List_t T) self.(Hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; - t <- hash_map_get_mut_in_list_fwd T n0 key l; - Return t - end + hash <- hash_key_fwd key; + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; + t <- hash_map_get_mut_in_list_fwd T n key l; + Return t . (** [hashmap::HashMap::{0}::get_mut] *) @@ -367,18 +331,14 @@ Definition hash_map_get_mut_back (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) (ret : T) : result (Hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hash_key_fwd key; - let i := vec_len (List_t T) self.(Hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; - l0 <- hash_map_get_mut_in_list_back T n0 key l ret; - v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; - Return (mkHash_map_t self.(Hash_map_num_entries) - self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v) - end + hash <- hash_key_fwd key; + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; + l0 <- hash_map_get_mut_in_list_back T n key l ret; + v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; + Return (mkHash_map_t self.(Hash_map_num_entries) + self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v) . (** [hashmap::HashMap::{0}::remove_from_list] *) @@ -430,21 +390,17 @@ Definition hash_map_remove_fwd (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result (option T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hash_key_fwd key; - let i := vec_len (List_t T) self.(Hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; - x <- hash_map_remove_from_list_fwd T n0 key l; - match x with - | None => Return None - | Some x0 => - i0 <- usize_sub self.(Hash_map_num_entries) 1%usize; - let _ := i0 in - Return (Some x0) - end + hash <- hash_key_fwd key; + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; + x <- hash_map_remove_from_list_fwd T n key l; + match x with + | None => Return None + | Some x0 => + i0 <- usize_sub self.(Hash_map_num_entries) 1%usize; + let _ := i0 in + Return (Some x0) end . @@ -453,69 +409,61 @@ Definition hash_map_remove_back (T : Type) (n : nat) (self : Hash_map_t T) (key : usize) : result (Hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hash_key_fwd key; - let i := vec_len (List_t T) self.(Hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; - x <- hash_map_remove_from_list_fwd T n0 key l; - match x with - | None => - l0 <- hash_map_remove_from_list_back T n0 key l; - v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; - Return (mkHash_map_t self.(Hash_map_num_entries) - self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v) - | Some x0 => - i0 <- usize_sub self.(Hash_map_num_entries) 1%usize; - l0 <- hash_map_remove_from_list_back T n0 key l; - v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; - Return (mkHash_map_t i0 self.(Hash_map_max_load_factor) - self.(Hash_map_max_load) v) - end + hash <- hash_key_fwd key; + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; + x <- hash_map_remove_from_list_fwd T n key l; + match x with + | None => + l0 <- hash_map_remove_from_list_back T n key l; + v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; + Return (mkHash_map_t self.(Hash_map_num_entries) + self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v) + | Some x0 => + i0 <- usize_sub self.(Hash_map_num_entries) 1%usize; + l0 <- hash_map_remove_from_list_back T n key l; + v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; + Return (mkHash_map_t i0 self.(Hash_map_max_load_factor) + self.(Hash_map_max_load) v) end . (** [hashmap::test1] *) Definition test1_fwd (n : nat) : result unit := - match n with - | 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) + hm <- hash_map_new_fwd u64 n; + hm0 <- hash_map_insert_fwd_back u64 n hm (0%usize) (42%u64); + hm1 <- hash_map_insert_fwd_back u64 n hm0 (128%usize) (18%u64); + hm2 <- hash_map_insert_fwd_back u64 n hm1 (1024%usize) (138%u64); + hm3 <- hash_map_insert_fwd_back u64 n hm2 (1056%usize) (256%u64); + i <- hash_map_get_fwd u64 n hm3 (128%usize); + if negb (i s= 18%u64) + then Fail_ Failure + else ( + hm4 <- hash_map_get_mut_back u64 n hm3 (1024%usize) (56%u64); + i0 <- hash_map_get_fwd u64 n hm4 (1024%usize); + if negb (i0 s= 56%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) - then Fail_ Failure - else ( - x <- hash_map_remove_fwd u64 n0 hm4 (1024%usize); - match x with - | None => Fail_ Failure - | Some x0 => - if negb (x0 s= 56%u64) + x <- hash_map_remove_fwd u64 n hm4 (1024%usize); + match x with + | None => Fail_ Failure + | Some x0 => + if negb (x0 s= 56%u64) + then Fail_ Failure + else ( + hm5 <- hash_map_remove_back u64 n hm4 (1024%usize); + i1 <- hash_map_get_fwd u64 n hm5 (0%usize); + if negb (i1 s= 42%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) + i2 <- hash_map_get_fwd u64 n hm5 (128%usize); + if negb (i2 s= 18%u64) then Fail_ Failure else ( - 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))) - end)) - end + i3 <- hash_map_get_fwd u64 n hm5 (1056%usize); + if negb (i3 s= 256%u64) then Fail_ Failure else Return tt))) + end)) . End Hashmap_Funs . diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 94a390df..295ec489 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -37,29 +37,20 @@ Definition hashmap_hash_map_new_with_capacity_fwd (max_load_divisor : usize) : result (Hashmap_hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - let v := vec_new (Hashmap_list_t T) in - 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, - max_load_divisor) i0 slots) - end + let v := vec_new (Hashmap_list_t T) in + slots <- hashmap_hash_map_allocate_slots_fwd T n 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, max_load_divisor) + i0 slots) . (** [hashmap_main::hashmap::HashMap::{0}::new] *) Definition hashmap_hash_map_new_fwd (T : Type) (n : nat) : result (Hashmap_hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hm <- - hashmap_hash_map_new_with_capacity_fwd T n0 (32%usize) (4%usize) - (5%usize); - Return hm - end + hm <- + hashmap_hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize); + Return hm . (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *) @@ -86,16 +77,11 @@ Definition hashmap_hash_map_clear_fwd_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) : result (Hashmap_hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - v <- - hashmap_hash_map_clear_slots_fwd_back T n0 self.(Hashmap_hash_map_slots) - (0%usize); - Return (mkHashmap_hash_map_t (0%usize) - self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) - v) - end + v <- + hashmap_hash_map_clear_slots_fwd_back T n self.(Hashmap_hash_map_slots) + (0%usize); + Return (mkHashmap_hash_map_t (0%usize) + self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v) . (** [hashmap_main::hashmap::HashMap::{0}::len] *) @@ -150,34 +136,29 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back : result (Hashmap_hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hashmap_hash_key_fwd key; - let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- - vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) - hash_mod; - inserted <- hashmap_hash_map_insert_in_list_fwd T n0 key value l; - if inserted - then ( - i0 <- usize_add self.(Hashmap_hash_map_num_entries) 1%usize; - l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l; - v <- - vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) - hash_mod l0; - Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor) - self.(Hashmap_hash_map_max_load) v)) - else ( - l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l; - v <- - vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) - hash_mod l0; - Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) - self.(Hashmap_hash_map_max_load_factor) - self.(Hashmap_hash_map_max_load) v)) - end + hash <- hashmap_hash_key_fwd key; + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; + inserted <- hashmap_hash_map_insert_in_list_fwd T n key value l; + if inserted + then ( + i0 <- usize_add self.(Hashmap_hash_map_num_entries) 1%usize; + l0 <- hashmap_hash_map_insert_in_list_back T n key value l; + v <- + vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod l0; + Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor) + self.(Hashmap_hash_map_max_load) v)) + else ( + l0 <- hashmap_hash_map_insert_in_list_back T n key value l; + v <- + vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod l0; + Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) + self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) + v)) . (** [core::num::u32::{9}::MAX] *) @@ -235,28 +216,24 @@ Definition hashmap_hash_map_try_resize_fwd_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) : result (Hashmap_hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - max_usize <- scalar_cast U32 Usize core_num_u32_max_c; - let capacity := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in - n1 <- usize_div max_usize 2%usize; - let (i, i0) := self.(Hashmap_hash_map_max_load_factor) in - i1 <- usize_div n1 i; - if capacity s<= i1 - then ( - i2 <- usize_mul capacity 2%usize; - ntable <- hashmap_hash_map_new_with_capacity_fwd T n0 i2 i i0; - p <- - hashmap_hash_map_move_elements_fwd_back T n0 ntable - self.(Hashmap_hash_map_slots) (0%usize); - let (ntable0, _) := p in - Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) (i, i0) - ntable0.(Hashmap_hash_map_max_load) ntable0.(Hashmap_hash_map_slots))) - else - Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) (i, i0) - self.(Hashmap_hash_map_max_load) self.(Hashmap_hash_map_slots)) - end + max_usize <- scalar_cast U32 Usize core_num_u32_max_c; + let capacity := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + n1 <- usize_div max_usize 2%usize; + let (i, i0) := self.(Hashmap_hash_map_max_load_factor) in + i1 <- usize_div n1 i; + if capacity s<= i1 + then ( + i2 <- usize_mul capacity 2%usize; + ntable <- hashmap_hash_map_new_with_capacity_fwd T n i2 i i0; + p <- + hashmap_hash_map_move_elements_fwd_back T n ntable + self.(Hashmap_hash_map_slots) (0%usize); + let (ntable0, _) := p in + Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) (i, i0) + ntable0.(Hashmap_hash_map_max_load) ntable0.(Hashmap_hash_map_slots))) + else + Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) (i, i0) + self.(Hashmap_hash_map_max_load) self.(Hashmap_hash_map_slots)) . (** [hashmap_main::hashmap::HashMap::{0}::insert] *) @@ -265,16 +242,11 @@ Definition hashmap_hash_map_insert_fwd_back : result (Hashmap_hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - self0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 self key value; - i <- hashmap_hash_map_len_fwd T self0; - if i s> self0.(Hashmap_hash_map_max_load) - then ( - self1 <- hashmap_hash_map_try_resize_fwd_back T n0 self0; Return self1) - else Return self0 - end + self0 <- hashmap_hash_map_insert_no_resize_fwd_back T n self key value; + i <- hashmap_hash_map_len_fwd T self0; + if i s> self0.(Hashmap_hash_map_max_load) + then (self1 <- hashmap_hash_map_try_resize_fwd_back T n self0; Return self1) + else Return self0 . (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) @@ -299,17 +271,12 @@ Definition hashmap_hash_map_contains_key_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : result bool := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hashmap_hash_key_fwd key; - let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- - vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; - b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key l; - Return b - end + hash <- hashmap_hash_key_fwd key; + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; + b <- hashmap_hash_map_contains_key_in_list_fwd T n key l; + Return b . (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) @@ -333,17 +300,12 @@ Definition hashmap_hash_map_get_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : result T := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hashmap_hash_key_fwd key; - let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- - vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; - t <- hashmap_hash_map_get_in_list_fwd T n0 key l; - Return t - end + hash <- hashmap_hash_key_fwd key; + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; + t <- hashmap_hash_map_get_in_list_fwd T n key l; + Return t . (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) @@ -387,18 +349,13 @@ Definition hashmap_hash_map_get_mut_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : result T := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hashmap_hash_key_fwd key; - let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- - vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) - hash_mod; - t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key l; - Return t - end + hash <- hashmap_hash_key_fwd key; + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; + t <- hashmap_hash_map_get_mut_in_list_fwd T n key l; + Return t . (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) @@ -406,23 +363,17 @@ Definition hashmap_hash_map_get_mut_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (ret : T) : result (Hashmap_hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hashmap_hash_key_fwd key; - let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- - vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) - hash_mod; - l0 <- hashmap_hash_map_get_mut_in_list_back T n0 key l ret; - v <- - vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) - hash_mod l0; - Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) - self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) - v) - end + hash <- hashmap_hash_key_fwd key; + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; + l0 <- hashmap_hash_map_get_mut_in_list_back T n key l ret; + v <- + vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod l0; + Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) + self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) v) . (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) @@ -483,23 +434,18 @@ Definition hashmap_hash_map_remove_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : result (option T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hashmap_hash_key_fwd key; - let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- - vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) - hash_mod; - x <- hashmap_hash_map_remove_from_list_fwd T n0 key l; - match x with - | None => Return None - | Some x0 => - i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize; - let _ := i0 in - Return (Some x0) - end + hash <- hashmap_hash_key_fwd key; + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; + x <- hashmap_hash_map_remove_from_list_fwd T n key l; + match x with + | None => Return None + | Some x0 => + i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize; + let _ := i0 in + Return (Some x0) end . @@ -508,91 +454,78 @@ Definition hashmap_hash_map_remove_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : result (Hashmap_hash_map_t T) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - hash <- hashmap_hash_key_fwd key; - let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in - hash_mod <- usize_rem hash i; - l <- - vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) - hash_mod; - x <- hashmap_hash_map_remove_from_list_fwd T n0 key l; - match x with - | None => - l0 <- hashmap_hash_map_remove_from_list_back T n0 key l; - v <- - vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) - hash_mod l0; - Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) - self.(Hashmap_hash_map_max_load_factor) - self.(Hashmap_hash_map_max_load) v) - | Some x0 => - i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize; - l0 <- hashmap_hash_map_remove_from_list_back T n0 key l; - v <- - vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) - hash_mod l0; - Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor) - self.(Hashmap_hash_map_max_load) v) - end + hash <- hashmap_hash_key_fwd key; + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; + x <- hashmap_hash_map_remove_from_list_fwd T n key l; + match x with + | None => + l0 <- hashmap_hash_map_remove_from_list_back T n key l; + v <- + vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod l0; + Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) + self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) + v) + | Some x0 => + i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize; + l0 <- hashmap_hash_map_remove_from_list_back T n key l; + v <- + vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod l0; + Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor) + self.(Hashmap_hash_map_max_load) v) end . (** [hashmap_main::hashmap::test1] *) Definition hashmap_test1_fwd (n : nat) : result unit := - match n with - | 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) + hm <- hashmap_hash_map_new_fwd u64 n; + hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm (0%usize) (42%u64); + hm1 <- hashmap_hash_map_insert_fwd_back u64 n hm0 (128%usize) (18%u64); + hm2 <- hashmap_hash_map_insert_fwd_back u64 n hm1 (1024%usize) (138%u64); + hm3 <- hashmap_hash_map_insert_fwd_back u64 n hm2 (1056%usize) (256%u64); + i <- hashmap_hash_map_get_fwd u64 n hm3 (128%usize); + if negb (i s= 18%u64) + then Fail_ Failure + else ( + hm4 <- hashmap_hash_map_get_mut_back u64 n hm3 (1024%usize) (56%u64); + i0 <- hashmap_hash_map_get_fwd u64 n hm4 (1024%usize); + if negb (i0 s= 56%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) - then Fail_ Failure - else ( - 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) + x <- hashmap_hash_map_remove_fwd u64 n hm4 (1024%usize); + match x with + | None => Fail_ Failure + | Some x0 => + if negb (x0 s= 56%u64) + then Fail_ Failure + else ( + hm5 <- hashmap_hash_map_remove_back u64 n hm4 (1024%usize); + i1 <- hashmap_hash_map_get_fwd u64 n hm5 (0%usize); + if negb (i1 s= 42%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) + i2 <- hashmap_hash_map_get_fwd u64 n hm5 (128%usize); + if negb (i2 s= 18%u64) then Fail_ Failure else ( - 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))) - end)) - end + i3 <- hashmap_hash_map_get_fwd u64 n hm5 (1056%usize); + if negb (i3 s= 256%u64) then Fail_ Failure else Return tt))) + end)) . (** [hashmap_main::insert_on_disk] *) Definition insert_on_disk_fwd (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- hashmap_utils_deserialize_fwd st; - let (st0, hm) := p in - hm0 <- hashmap_hash_map_insert_fwd_back u64 n0 hm key value; - p0 <- hashmap_utils_serialize_fwd hm0 st0; - let (st1, _) := p0 in - Return (st1, tt) - end + p <- hashmap_utils_deserialize_fwd st; + let (st0, hm) := p in + hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm key value; + p0 <- hashmap_utils_serialize_fwd hm0 st0; + let (st1, _) := p0 in + Return (st1, tt) . (** [hashmap_main::main] *) -- cgit v1.2.3