diff options
| -rw-r--r-- | compiler/Extract.ml | 8 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 891 |
2 files changed, 444 insertions, 455 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index a5ff6796..d707dc81 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1661,25 +1661,25 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) Collections.List.iter_link (fun () -> F.pp_print_string fmt ","; - F.pp_close_box fmt (); F.pp_print_space fmt () ) (fun ((fid, _), e) -> - F.pp_open_hovbox fmt 0; + F.pp_open_hvbox fmt ctx.indent_incr; let f = ctx_get_field adt_cons.adt_id fid ctx in F.pp_print_string fmt f; F.pp_print_string fmt " := "; F.pp_open_hvbox fmt ctx.indent_incr; extract_texpression ctx fmt true e; + F.pp_close_box fmt (); F.pp_close_box fmt () ) (List.combine fields args); F.pp_close_box fmt (); F.pp_close_box fmt (); F.pp_close_box fmt (); - F.pp_close_box fmt (); F.pp_print_space fmt (); - F.pp_print_string fmt "}" + F.pp_print_string fmt "}"; + F.pp_close_box fmt () else let use_parentheses = inside && args <> [] in if use_parentheses then F.pp_print_string fmt "("; diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 79d711e9..5e78d9cf 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -182,261 +182,365 @@ def hashmap_hash_map_insert_no_resize_fwd_back hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, hashmap_hash_map_slots := v } - else - do - let l0 <- hashmap_hash_map_insert_in_list_back T key value l - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 - result.ret - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v - } - - /- [core::num::u32::{9}::MAX] -/ - def core_num_u32_max_body : result UInt32 := - result.ret (UInt32.ofNatCore 4294967295 (by intlit)) - def core_num_u32_max_c : UInt32 := - eval_global core_num_u32_max_body (by simp) - - /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ - def hashmap_hash_map_move_elements_from_list_loop_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : - (result (hashmap_hash_map_t T)) - := - match ls with - | hashmap_list_t.HashmapListCons k v tl => + else do - let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v - hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl - | hashmap_list_t.HashmapListNil => result.ret ntable - - termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable - ls => hashmap_hash_map_move_elements_from_list_loop_terminates - T ntable ls - decreasing_by - hashmap_hash_map_move_elements_from_list_loop_decreases ntable ls - - /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ - def hashmap_hash_map_move_elements_from_list_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : - result (hashmap_hash_map_t T) - := - hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable ls + let l0 <- hashmap_hash_map_insert_in_list_back T key value l + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + result.ret + { + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, + hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, + hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, + hashmap_hash_map_slots := v + } + +/- [core::num::u32::{9}::MAX] -/ +def core_num_u32_max_body : result UInt32 := + result.ret (UInt32.ofNatCore 4294967295 (by intlit)) +def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ +def hashmap_hash_map_move_elements_from_list_loop_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : + (result (hashmap_hash_map_t T)) + := + match ls with + | hashmap_list_t.HashmapListCons k v tl => + do + let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v + hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl + | hashmap_list_t.HashmapListNil => result.ret ntable - /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ - def hashmap_hash_map_move_elements_loop_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) - (i : USize) : - (result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))) - := - let i0 := vec_len (hashmap_list_t T) slots - if i < i0 +termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls + => hashmap_hash_map_move_elements_from_list_loop_terminates T + ntable ls +decreasing_by hashmap_hash_map_move_elements_from_list_loop_decreases ntable ls + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ +def hashmap_hash_map_move_elements_from_list_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : + result (hashmap_hash_map_t T) + := + hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable ls + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ +def hashmap_hash_map_move_elements_loop_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) + (i : USize) : + (result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))) + := + let i0 := vec_len (hashmap_list_t T) slots + if i < i0 + then + do + let l <- vec_index_mut_fwd (hashmap_list_t T) slots i + let ls := + mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.HashmapListNil + let ntable0 <- + hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) + let l0 := + mem_replace_back (hashmap_list_t T) l hashmap_list_t.HashmapListNil + let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i l0 + hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 + else result.ret (ntable, slots) +termination_by hashmap_hash_map_move_elements_loop_fwd_back ntable slots i => + hashmap_hash_map_move_elements_loop_terminates T ntable slots i +decreasing_by hashmap_hash_map_move_elements_loop_decreases ntable slots i + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ +def hashmap_hash_map_move_elements_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) + (i : USize) : + result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) + := + hashmap_hash_map_move_elements_loop_fwd_back T ntable slots i + +/- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ +def hashmap_hash_map_try_resize_fwd_back + (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := + do + let max_usize <- scalar_cast USize core_num_u32_max_c + let capacity := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by intlit)) + let (i, i0) := self.hashmap_hash_map_max_load_factor + let i1 <- USize.checked_div n1 i + if capacity <= i1 then do - let l <- vec_index_mut_fwd (hashmap_list_t T) slots i - let ls := - mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.HashmapListNil - let ntable0 <- - hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls - let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) - let l0 := - mem_replace_back (hashmap_list_t T) l hashmap_list_t.HashmapListNil - let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i l0 - hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 - else result.ret (ntable, slots) - termination_by hashmap_hash_map_move_elements_loop_fwd_back ntable slots i => - hashmap_hash_map_move_elements_loop_terminates T ntable slots i - decreasing_by hashmap_hash_map_move_elements_loop_decreases ntable slots i + let i2 <- USize.checked_mul capacity (USize.ofNatCore 2 (by intlit)) + let ntable <- hashmap_hash_map_new_with_capacity_fwd T i2 i i0 + let (ntable0, _) <- + hashmap_hash_map_move_elements_fwd_back T ntable + self.hashmap_hash_map_slots (USize.ofNatCore 0 (by intlit)) + result.ret + { + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, + hashmap_hash_map_max_load_factor := (i, i0), + hashmap_hash_map_max_load := ntable0.hashmap_hash_map_max_load, + hashmap_hash_map_slots := ntable0.hashmap_hash_map_slots + } + else + result.ret + { + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, + hashmap_hash_map_max_load_factor := (i, i0), + hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, + hashmap_hash_map_slots := self.hashmap_hash_map_slots + } + +/- [hashmap_main::hashmap::HashMap::{0}::insert] -/ +def hashmap_hash_map_insert_fwd_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) : + result (hashmap_hash_map_t T) + := + do + let self0 <- hashmap_hash_map_insert_no_resize_fwd_back T self key value + let i <- hashmap_hash_map_len_fwd T self0 + if i > self0.hashmap_hash_map_max_load + then hashmap_hash_map_try_resize_fwd_back T self0 + else result.ret self0 + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ +def hashmap_hash_map_contains_key_in_list_loop_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : (result Bool) := + match ls with + | hashmap_list_t.HashmapListCons ckey t tl => + if ckey = key + then result.ret true + else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl + | hashmap_list_t.HashmapListNil => result.ret false - /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ - def hashmap_hash_map_move_elements_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) - (i : USize) : - result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) - := - hashmap_hash_map_move_elements_loop_fwd_back T ntable slots i +termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls => + hashmap_hash_map_contains_key_in_list_loop_terminates T key ls +decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ +def hashmap_hash_map_contains_key_in_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := + hashmap_hash_map_contains_key_in_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ +def hashmap_hash_map_contains_key_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result Bool := + do + let hash <- hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + hashmap_hash_map_contains_key_in_list_fwd T key l + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ +def hashmap_hash_map_get_in_list_loop_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : (result T) := + match ls with + | hashmap_list_t.HashmapListCons ckey cvalue tl => + if ckey = key + then result.ret cvalue + else hashmap_hash_map_get_in_list_loop_fwd T key tl + | hashmap_list_t.HashmapListNil => result.fail error.panic - /- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ - def hashmap_hash_map_try_resize_fwd_back - (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := - do - let max_usize <- scalar_cast USize core_num_u32_max_c - let capacity := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots - let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by intlit)) - let (i, i0) := self.hashmap_hash_map_max_load_factor - let i1 <- USize.checked_div n1 i - if capacity <= i1 - then - do - let i2 <- USize.checked_mul capacity (USize.ofNatCore 2 (by intlit)) - let ntable <- hashmap_hash_map_new_with_capacity_fwd T i2 i i0 - let (ntable0, _) <- - hashmap_hash_map_move_elements_fwd_back T ntable - self.hashmap_hash_map_slots (USize.ofNatCore 0 (by intlit)) - result.ret - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := (i, i0), - hashmap_hash_map_max_load := ntable0.hashmap_hash_map_max_load, - hashmap_hash_map_slots := ntable0.hashmap_hash_map_slots - } - else - result.ret - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := (i, i0), - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := self.hashmap_hash_map_slots - } - - /- [hashmap_main::hashmap::HashMap::{0}::insert] -/ - def hashmap_hash_map_insert_fwd_back - (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) : - result (hashmap_hash_map_t T) - := - do - let self0 <- - hashmap_hash_map_insert_no_resize_fwd_back T self key value - let i <- hashmap_hash_map_len_fwd T self0 - if i > self0.hashmap_hash_map_max_load - then hashmap_hash_map_try_resize_fwd_back T self0 - else result.ret self0 - - /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ - def hashmap_hash_map_contains_key_in_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : (result Bool) := - match ls with - | hashmap_list_t.HashmapListCons ckey t tl => - if ckey = key - then result.ret true - else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => result.ret false - - termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls => - hashmap_hash_map_contains_key_in_list_loop_terminates T key ls - decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls - - /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ - def hashmap_hash_map_contains_key_in_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := - hashmap_hash_map_contains_key_in_list_loop_fwd T key ls - - /- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ - def hashmap_hash_map_contains_key_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result Bool := - do - let hash <- hashmap_hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots - let hash_mod <- USize.checked_rem hash i - let l <- - vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - hashmap_hash_map_contains_key_in_list_fwd T key l - - /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ - def hashmap_hash_map_get_in_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : (result T) := - match ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => - if ckey = key - then result.ret cvalue - else hashmap_hash_map_get_in_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => result.fail error.panic - - termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => - hashmap_hash_map_get_in_list_loop_terminates - T key ls - decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls - - /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ - def hashmap_hash_map_get_in_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := - hashmap_hash_map_get_in_list_loop_fwd T key ls - - /- [hashmap_main::hashmap::HashMap::{0}::get] -/ - def hashmap_hash_map_get_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := +termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => + hashmap_hash_map_get_in_list_loop_terminates + T key ls +decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ +def hashmap_hash_map_get_in_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := + hashmap_hash_map_get_in_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::get] -/ +def hashmap_hash_map_get_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := + do + let hash <- hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + hashmap_hash_map_get_in_list_fwd T key l + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_loop_fwd + (T : Type) (ls : hashmap_list_t T) (key : USize) : (result T) := + match ls with + | hashmap_list_t.HashmapListCons ckey cvalue tl => + if ckey = key + then result.ret cvalue + else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key + | hashmap_list_t.HashmapListNil => result.fail error.panic + +termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key => + hashmap_hash_map_get_mut_in_list_loop_terminates + T ls key +decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_fwd + (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := + hashmap_hash_map_get_mut_in_list_loop_fwd T ls key + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_loop_back + (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : + (result (hashmap_list_t T)) + := + match ls with + | hashmap_list_t.HashmapListCons ckey cvalue tl => + if ckey = key + then result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl) + else do - let hash <- hashmap_hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots - let hash_mod <- USize.checked_rem hash i - let l <- - vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - hashmap_hash_map_get_in_list_fwd T key l - - /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ - def hashmap_hash_map_get_mut_in_list_loop_fwd - (T : Type) (ls : hashmap_list_t T) (key : USize) : (result T) := - match ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => - if ckey = key - then result.ret cvalue - else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key + let l <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 + result.ret (hashmap_list_t.HashmapListCons ckey cvalue l) + | hashmap_list_t.HashmapListNil => result.fail error.panic + +termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 => + hashmap_hash_map_get_mut_in_list_loop_terminates T ls key +decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_back + (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : + result (hashmap_list_t T) + := + hashmap_hash_map_get_mut_in_list_loop_back T ls key ret0 + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ +def hashmap_hash_map_get_mut_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := + do + let hash <- hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + hashmap_hash_map_get_mut_in_list_fwd T l key + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ +def hashmap_hash_map_get_mut_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) (ret0 : T) : + result (hashmap_hash_map_t T) + := + do + let hash <- hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let l0 <- hashmap_hash_map_get_mut_in_list_back T l key ret0 + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + result.ret + { + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, + hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, + hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, + hashmap_hash_map_slots := v + } + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_loop_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : (result (Option T)) := + match ls with + | hashmap_list_t.HashmapListCons ckey t tl => + if ckey = key + then + let mv_ls := + mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey + t tl) hashmap_list_t.HashmapListNil + match mv_ls with + | hashmap_list_t.HashmapListCons i cvalue tl0 => + result.ret (Option.some cvalue) | hashmap_list_t.HashmapListNil => result.fail error.panic - termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key => - hashmap_hash_map_get_mut_in_list_loop_terminates T ls key - decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key - - /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ - def hashmap_hash_map_get_mut_in_list_fwd - (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := - hashmap_hash_map_get_mut_in_list_loop_fwd T ls key - - /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ - def hashmap_hash_map_get_mut_in_list_loop_back - (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : - (result (hashmap_list_t T)) - := - match ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => - if ckey = key - then result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl) - else - do - let l <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 - result.ret (hashmap_list_t.HashmapListCons ckey cvalue l) + else hashmap_hash_map_remove_from_list_loop_fwd T key tl + | hashmap_list_t.HashmapListNil => result.ret Option.none + +termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls => + hashmap_hash_map_remove_from_list_loop_terminates + T key ls +decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_fwd + (T : Type) (key : USize) (ls : hashmap_list_t T) : result (Option T) := + hashmap_hash_map_remove_from_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_loop_back + (T : Type) (key : USize) (ls : hashmap_list_t T) : + (result (hashmap_list_t T)) + := + match ls with + | hashmap_list_t.HashmapListCons ckey t tl => + if ckey = key + then + let mv_ls := + mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey + t tl) hashmap_list_t.HashmapListNil + match mv_ls with + | hashmap_list_t.HashmapListCons i cvalue tl0 => result.ret tl0 | hashmap_list_t.HashmapListNil => result.fail error.panic - termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 => - hashmap_hash_map_get_mut_in_list_loop_terminates T ls key - decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key - - /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ - def hashmap_hash_map_get_mut_in_list_back - (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : - result (hashmap_list_t T) - := - hashmap_hash_map_get_mut_in_list_loop_back T ls key ret0 - - /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ - def hashmap_hash_map_get_mut_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result T := + else + do + let l <- hashmap_hash_map_remove_from_list_loop_back T key tl + result.ret (hashmap_list_t.HashmapListCons ckey t l) + | hashmap_list_t.HashmapListNil => result.ret hashmap_list_t.HashmapListNil + +termination_by hashmap_hash_map_remove_from_list_loop_back key ls => + hashmap_hash_map_remove_from_list_loop_terminates + T key ls +decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_back + (T : Type) (key : USize) (ls : hashmap_list_t T) : + result (hashmap_list_t T) + := + hashmap_hash_map_remove_from_list_loop_back T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ +def hashmap_hash_map_remove_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : result (Option T) := + do + let hash <- hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let x <- hashmap_hash_map_remove_from_list_fwd T key l + match x with + | Option.none => result.ret Option.none + | Option.some x0 => do - let hash <- hashmap_hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots - let hash_mod <- USize.checked_rem hash i - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod - hashmap_hash_map_get_mut_in_list_fwd T l key + let _ <- USize.checked_sub self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by intlit)) + result.ret (Option.some x0) - /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ - def hashmap_hash_map_get_mut_back - (T : Type) (self : hashmap_hash_map_t T) (key : USize) (ret0 : T) : - result (hashmap_hash_map_t T) - := + +/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ +def hashmap_hash_map_remove_back + (T : Type) (self : hashmap_hash_map_t T) (key : USize) : + result (hashmap_hash_map_t T) + := + do + let hash <- hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod <- USize.checked_rem hash i + let l <- + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let x <- hashmap_hash_map_remove_from_list_fwd T key l + match x with + | Option.none => do - let hash <- hashmap_hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots - let hash_mod <- USize.checked_rem hash i - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod - let l0 <- hashmap_hash_map_get_mut_in_list_back T l key ret0 + let l0 <- hashmap_hash_map_remove_from_list_back T key l let v <- vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 @@ -447,221 +551,106 @@ def hashmap_hash_map_insert_no_resize_fwd_back hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, hashmap_hash_map_slots := v } - - /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ - def hashmap_hash_map_remove_from_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : (result (Option T)) := - match ls with - | hashmap_list_t.HashmapListCons ckey t tl => - if ckey = key - then - let mv_ls := - mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons - ckey t tl) hashmap_list_t.HashmapListNil - match mv_ls with - | hashmap_list_t.HashmapListCons i cvalue tl0 => - result.ret (Option.some cvalue) - | hashmap_list_t.HashmapListNil => result.fail error.panic - - else hashmap_hash_map_remove_from_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => result.ret Option.none - - termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls => - hashmap_hash_map_remove_from_list_loop_terminates T key ls - decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls - - /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ - def hashmap_hash_map_remove_from_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result (Option T) := - hashmap_hash_map_remove_from_list_loop_fwd T key ls - - /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ - def hashmap_hash_map_remove_from_list_loop_back - (T : Type) (key : USize) (ls : hashmap_list_t T) : - (result (hashmap_list_t T)) - := - match ls with - | hashmap_list_t.HashmapListCons ckey t tl => - if ckey = key - then - let mv_ls := - mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons - ckey t tl) hashmap_list_t.HashmapListNil - match mv_ls with - | hashmap_list_t.HashmapListCons i cvalue tl0 => result.ret tl0 - | hashmap_list_t.HashmapListNil => result.fail error.panic - - else - do - let l <- hashmap_hash_map_remove_from_list_loop_back T key tl - result.ret (hashmap_list_t.HashmapListCons ckey t l) - | hashmap_list_t.HashmapListNil => - result.ret hashmap_list_t.HashmapListNil - - termination_by hashmap_hash_map_remove_from_list_loop_back key ls => - hashmap_hash_map_remove_from_list_loop_terminates T key ls - decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls - - /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ - def hashmap_hash_map_remove_from_list_back - (T : Type) (key : USize) (ls : hashmap_list_t T) : - result (hashmap_list_t T) - := - hashmap_hash_map_remove_from_list_loop_back T key ls - - /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ - def hashmap_hash_map_remove_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : - result (Option T) - := + | Option.some x0 => do - let hash <- hashmap_hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots - let hash_mod <- USize.checked_rem hash i - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod - let x <- hashmap_hash_map_remove_from_list_fwd T key l - match x with - | Option.none => result.ret Option.none - | Option.some x0 => - do - let _ <- USize.checked_sub self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by intlit)) - result.ret (Option.some x0) - + let i0 <- USize.checked_sub self.hashmap_hash_map_num_entries + (USize.ofNatCore 1 (by intlit)) + let l0 <- hashmap_hash_map_remove_from_list_back T key l + let v <- + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + result.ret + { + hashmap_hash_map_num_entries := i0, + hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, + hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, + hashmap_hash_map_slots := v + } - /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ - def hashmap_hash_map_remove_back - (T : Type) (self : hashmap_hash_map_t T) (key : USize) : - result (hashmap_hash_map_t T) - := + +/- [hashmap_main::hashmap::test1] -/ +def hashmap_test1_fwd : result Unit := + do + let hm <- hashmap_hash_map_new_fwd UInt64 + let hm0 <- + hashmap_hash_map_insert_fwd_back UInt64 hm + (USize.ofNatCore 0 (by intlit)) (UInt64.ofNatCore 42 (by intlit)) + let hm1 <- + hashmap_hash_map_insert_fwd_back UInt64 hm0 + (USize.ofNatCore 128 (by intlit)) (UInt64.ofNatCore 18 (by intlit)) + let hm2 <- + hashmap_hash_map_insert_fwd_back UInt64 hm1 + (USize.ofNatCore 1024 (by intlit)) (UInt64.ofNatCore 138 (by intlit)) + let hm3 <- + hashmap_hash_map_insert_fwd_back UInt64 hm2 + (USize.ofNatCore 1056 (by intlit)) (UInt64.ofNatCore 256 (by intlit)) + let i <- + hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by intlit)) + if not (i = (UInt64.ofNatCore 18 (by intlit))) + then result.fail error.panic + else do - let hash <- hashmap_hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots - let hash_mod <- USize.checked_rem hash i - let l <- - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod - let x <- hashmap_hash_map_remove_from_list_fwd T key l - match x with - | Option.none => + let hm4 <- + hashmap_hash_map_get_mut_back UInt64 hm3 + (USize.ofNatCore 1024 (by intlit)) + (UInt64.ofNatCore 56 (by intlit)) + let i0 <- + hashmap_hash_map_get_fwd UInt64 hm4 + (USize.ofNatCore 1024 (by intlit)) + if not (i0 = (UInt64.ofNatCore 56 (by intlit))) + then result.fail error.panic + else do - let l0 <- hashmap_hash_map_remove_from_list_back T key l - let v <- - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 - result.ret - { - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v - } - | Option.some x0 => - do - let i0 <- USize.checked_sub self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by intlit)) - let l0 <- hashmap_hash_map_remove_from_list_back T key l - let v <- - vec_index_mut_back (hashmap_list_t T) - self.hashmap_hash_map_slots hash_mod l0 - result.ret - { - hashmap_hash_map_num_entries := i0, - hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, - hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, - hashmap_hash_map_slots := v - } - - /- [hashmap_main::hashmap::test1] -/ - def hashmap_test1_fwd : result Unit := - do - let hm <- hashmap_hash_map_new_fwd UInt64 - let hm0 <- - hashmap_hash_map_insert_fwd_back UInt64 hm - (USize.ofNatCore 0 (by intlit)) (UInt64.ofNatCore 42 (by intlit)) - let hm1 <- - hashmap_hash_map_insert_fwd_back UInt64 hm0 - (USize.ofNatCore 128 (by intlit)) - (UInt64.ofNatCore 18 (by intlit)) - let hm2 <- - hashmap_hash_map_insert_fwd_back UInt64 hm1 - (USize.ofNatCore 1024 (by intlit)) - (UInt64.ofNatCore 138 (by intlit)) - let hm3 <- - hashmap_hash_map_insert_fwd_back UInt64 hm2 - (USize.ofNatCore 1056 (by intlit)) - (UInt64.ofNatCore 256 (by intlit)) - let i <- - hashmap_hash_map_get_fwd UInt64 hm3 - (USize.ofNatCore 128 (by intlit)) - if not (i = (UInt64.ofNatCore 18 (by intlit))) - then result.fail error.panic - else - do - let hm4 <- - hashmap_hash_map_get_mut_back UInt64 hm3 - (USize.ofNatCore 1024 (by intlit)) - (UInt64.ofNatCore 56 (by intlit)) - let i0 <- - hashmap_hash_map_get_fwd UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) - if not (i0 = (UInt64.ofNatCore 56 (by intlit))) + let x <- + hashmap_hash_map_remove_fwd UInt64 hm4 + (USize.ofNatCore 1024 (by intlit)) + match x with + | Option.none => result.fail error.panic + | Option.some x0 => + if not (x0 = (UInt64.ofNatCore 56 (by intlit))) then result.fail error.panic else do - let x <- - hashmap_hash_map_remove_fwd UInt64 hm4 + let hm5 <- + hashmap_hash_map_remove_back UInt64 hm4 (USize.ofNatCore 1024 (by intlit)) - match x with - | Option.none => result.fail error.panic - | Option.some x0 => - if not (x0 = (UInt64.ofNatCore 56 (by intlit))) - then result.fail error.panic - else - do - let hm5 <- - hashmap_hash_map_remove_back UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) - let i1 <- - hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 0 (by intlit)) - if not (i1 = (UInt64.ofNatCore 42 (by intlit))) - then result.fail error.panic - else - do - let i2 <- - hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 128 (by intlit)) - if not (i2 = (UInt64.ofNatCore 18 (by intlit))) - then result.fail error.panic - else - do - let i3 <- - hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 1056 (by intlit)) - if not (i3 = - (UInt64.ofNatCore 256 (by intlit))) - then result.fail error.panic - else result.ret () - - - /- Unit test for [hashmap_main::hashmap::test1] -/ - #assert (hashmap_test1_fwd = ret ()) - - /- [hashmap_main::insert_on_disk] -/ - def insert_on_disk_fwd - (key : USize) (value : UInt64) (st : state) : result (state × Unit) := - do - let (st0, hm) <- hashmap_utils_deserialize_fwd st - let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value - let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 - result.ret (st1, ()) - - /- [hashmap_main::main] -/ - def main_fwd : result Unit := result.ret () - - /- Unit test for [hashmap_main::main] -/ - #assert (main_fwd = ret ()) - + let i1 <- + hashmap_hash_map_get_fwd UInt64 hm5 + (USize.ofNatCore 0 (by intlit)) + if not (i1 = (UInt64.ofNatCore 42 (by intlit))) + then result.fail error.panic + else + do + let i2 <- + hashmap_hash_map_get_fwd UInt64 hm5 + (USize.ofNatCore 128 (by intlit)) + if not (i2 = (UInt64.ofNatCore 18 (by intlit))) + then result.fail error.panic + else + do + let i3 <- + hashmap_hash_map_get_fwd UInt64 hm5 + (USize.ofNatCore 1056 (by intlit)) + if not (i3 = (UInt64.ofNatCore 256 (by intlit))) + then result.fail error.panic + else result.ret () + + +/- Unit test for [hashmap_main::hashmap::test1] -/ +#assert (hashmap_test1_fwd = ret ()) + +/- [hashmap_main::insert_on_disk] -/ +def insert_on_disk_fwd + (key : USize) (value : UInt64) (st : state) : result (state × Unit) := + do + let (st0, hm) <- hashmap_utils_deserialize_fwd st + let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value + let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 + result.ret (st1, ()) + +/- [hashmap_main::main] -/ +def main_fwd : result Unit := result.ret () + +/- Unit test for [hashmap_main::main] -/ +#assert (main_fwd = ret ()) + |