diff options
Diffstat (limited to '')
3 files changed, 232 insertions, 129 deletions
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean new file mode 100644 index 00000000..16a4ea4c --- /dev/null +++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean @@ -0,0 +1,111 @@ +-- [hashmap_main]: decreases clauses +import Base.Primitives +import HashmapMain.Types + +/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: termination measure -/ +@[simp] +def hashmap_hash_map_allocate_slots_loop_terminates (T : Type) + (slots : vec (hashmap_list_t T)) (n : USize) := + (slots, n) + +syntax "hashmap_hash_map_allocate_slots_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::clear]: termination measure -/ +@[simp] +def hashmap_hash_map_clear_loop_terminates (T : Type) + (slots : vec (hashmap_list_t T)) (i : USize) := + (slots, i) + +syntax "hashmap_hash_map_clear_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_clear_loop_decreases $slots $i) =>`(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_insert_in_list_loop_terminates (T : Type) (key : USize) + (value : T) (ls : hashmap_list_t T) := + (key, value, ls) + +syntax "hashmap_hash_map_insert_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_insert_in_list_loop_decreases $key $value $ls) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: termination measure -/ +@[simp] +def hashmap_hash_map_move_elements_from_list_loop_terminates (T : Type) + (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) := + (ntable, ls) + +syntax "hashmap_hash_map_move_elements_from_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_move_elements_from_list_loop_decreases $ntable +$ls) =>`(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements]: termination measure -/ +@[simp] +def hashmap_hash_map_move_elements_loop_terminates (T : Type) + (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) (i : USize) + := + (ntable, slots, i) + +syntax "hashmap_hash_map_move_elements_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_move_elements_loop_decreases $ntable $slots $i) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_contains_key_in_list_loop_terminates (T : Type) + (key : USize) (ls : hashmap_list_t T) := + (key, ls) + +syntax "hashmap_hash_map_contains_key_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_contains_key_in_list_loop_decreases $key $ls) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_get_in_list_loop_terminates (T : Type) (key : USize) + (ls : hashmap_list_t T) := + (key, ls) + +syntax "hashmap_hash_map_get_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_get_in_list_loop_decreases $key $ls) =>`(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_get_mut_in_list_loop_terminates (T : Type) + (ls : hashmap_list_t T) (key : USize) := + (ls, key) + +syntax "hashmap_hash_map_get_mut_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_get_mut_in_list_loop_decreases $ls $key) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: termination measure -/ +@[simp] +def hashmap_hash_map_remove_from_list_loop_terminates (T : Type) (key : USize) + (ls : hashmap_list_t T) := + (key, ls) + +syntax "hashmap_hash_map_remove_from_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_remove_from_list_loop_decreases $key $ls) => + `(tactic| sorry) + diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean index bf331d6e..3466e7e0 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean @@ -15,17 +15,16 @@ macro_rules | `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) => `(tactic| sorry) -/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/ +/- [hashmap_main::hashmap::HashMap::{0}::clear]: termination measure -/ @[simp] -def hashmap_hash_map_clear_slots_loop_terminates (T : Type) +def hashmap_hash_map_clear_loop_terminates (T : Type) (slots : vec (hashmap_list_t T)) (i : USize) := (slots, i) -syntax "hashmap_hash_map_clear_slots_loop_decreases" term+ : tactic +syntax "hashmap_hash_map_clear_loop_decreases" term+ : tactic macro_rules -| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) => - `(tactic| sorry) +| `(tactic| hashmap_hash_map_clear_loop_decreases $slots $i) =>`(tactic| sorry) /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/ @[simp] diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index b0c4d683..5134f483 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -3,7 +3,7 @@ import Base.Primitives import HashmapMain.Types import HashmapMain.Opaque -import HashmapMain.Clauses.Template +import HashmapMain.Clauses.Clauses section variable (opaque_defs: OpaqueDefs) @@ -19,13 +19,13 @@ def hashmap_hash_map_allocate_slots_loop_fwd then do let slots0 <- - vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil - let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) + vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil + let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 else result.ret slots termination_by hashmap_hash_map_allocate_slots_loop_fwd slots n => hashmap_hash_map_allocate_slots_loop_terminates - T slots n + T slots n decreasing_by hashmap_hash_map_allocate_slots_loop_decreases slots n /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ @@ -42,10 +42,10 @@ def hashmap_hash_map_new_with_capacity_fwd result (hashmap_hash_map_t T) := do - let v := vec_new (hashmap_list_t T) - let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity - let i <- USize.checked_mul capacity max_load_dividend - let i0 <- USize.checked_div i max_load_divisor + let v := vec_new (hashmap_list_t T) + let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity + let i <- USize.checked_mul capacity max_load_dividend + let i0 <- USize.checked_div i max_load_divisor result.ret { hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), @@ -60,40 +60,33 @@ def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) := hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by intlit)) (USize.ofNatCore 4 (by intlit)) (USize.ofNatCore 5 (by intlit)) -/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ -def hashmap_hash_map_clear_slots_loop_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ +def hashmap_hash_map_clear_loop_fwd_back (T : Type) (slots : vec (hashmap_list_t T)) (i : USize) : (result (vec (hashmap_list_t T))) := - let i0 := vec_len (hashmap_list_t T) slots + let i0 := vec_len (hashmap_list_t T) slots if i < i0 then do - let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i - hashmap_list_t.HashmapListNil - hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1 + hashmap_list_t.HashmapListNil + hashmap_hash_map_clear_loop_fwd_back T slots0 i1 else result.ret slots -termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i => - hashmap_hash_map_clear_slots_loop_terminates - T slots i -decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i - -/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ -def hashmap_hash_map_clear_slots_fwd_back - (T : Type) (slots : vec (hashmap_list_t T)) : - result (vec (hashmap_list_t T)) - := - hashmap_hash_map_clear_slots_loop_fwd_back T slots - (USize.ofNatCore 0 (by intlit)) +termination_by hashmap_hash_map_clear_loop_fwd_back slots i => + hashmap_hash_map_clear_loop_terminates + T slots i +decreasing_by hashmap_hash_map_clear_loop_decreases slots i /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ def hashmap_hash_map_clear_fwd_back (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := do let v <- - hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots + hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots + (USize.ofNatCore 0 (by intlit)) result.ret { hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), @@ -120,7 +113,7 @@ def hashmap_hash_map_insert_in_list_loop_fwd | hashmap_list_t.HashmapListNil => result.ret true termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls => - hashmap_hash_map_insert_in_list_loop_terminates T key value ls + hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -139,14 +132,14 @@ def hashmap_hash_map_insert_in_list_loop_back then result.ret (hashmap_list_t.HashmapListCons ckey value tl) else do - let l <- hashmap_hash_map_insert_in_list_loop_back T key value tl - result.ret (hashmap_list_t.HashmapListCons ckey cvalue l) + let tl0 <- hashmap_hash_map_insert_in_list_loop_back T key value tl + result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) | hashmap_list_t.HashmapListNil => - let l := hashmap_list_t.HashmapListNil + let l := hashmap_list_t.HashmapListNil result.ret (hashmap_list_t.HashmapListCons key value l) termination_by hashmap_hash_map_insert_in_list_loop_back key value ls => - hashmap_hash_map_insert_in_list_loop_terminates T key value ls + hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -162,21 +155,21 @@ def hashmap_hash_map_insert_no_resize_fwd_back 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 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 inserted <- hashmap_hash_map_insert_in_list_fwd T key value l + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let inserted <- hashmap_hash_map_insert_in_list_fwd T key value l if inserted then do let i0 <- USize.checked_add self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by intlit)) - let l0 <- hashmap_hash_map_insert_in_list_back T key value l + (USize.ofNatCore 1 (by intlit)) + 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 + hash_mod l0 result.ret { hashmap_hash_map_num_entries := i0, @@ -186,10 +179,10 @@ def hashmap_hash_map_insert_no_resize_fwd_back } else do - let l0 <- hashmap_hash_map_insert_in_list_back T key value l + 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 + hash_mod l0 result.ret { hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, @@ -211,13 +204,13 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back 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 + 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 + ntable ls decreasing_by hashmap_hash_map_move_elements_from_list_loop_decreases ntable ls /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ @@ -233,23 +226,23 @@ def hashmap_hash_map_move_elements_loop_fwd_back (i : USize) : (result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))) := - let i0 := vec_len (hashmap_list_t T) slots + 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 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 + 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)) + 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 + 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 + 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] -/ @@ -264,19 +257,19 @@ def hashmap_hash_map_move_elements_fwd_back 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 + 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 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)) + self.hashmap_hash_map_slots (USize.ofNatCore 0 (by intlit)) result.ret { hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, @@ -299,8 +292,8 @@ def hashmap_hash_map_insert_fwd_back 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 + 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 @@ -316,7 +309,7 @@ def hashmap_hash_map_contains_key_in_list_loop_fwd | 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 + 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] -/ @@ -328,11 +321,11 @@ def hashmap_hash_map_contains_key_in_list_fwd 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 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 + 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] -/ @@ -347,7 +340,7 @@ def hashmap_hash_map_get_in_list_loop_fwd termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => hashmap_hash_map_get_in_list_loop_terminates - T key ls + T key ls decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ @@ -359,11 +352,11 @@ def hashmap_hash_map_get_in_list_fwd 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 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 + 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] -/ @@ -378,7 +371,7 @@ def hashmap_hash_map_get_mut_in_list_loop_fwd 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 + 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] -/ @@ -397,12 +390,12 @@ def hashmap_hash_map_get_mut_in_list_loop_back 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) + let tl0 <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 + result.ret (hashmap_list_t.HashmapListCons ckey cvalue 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 + 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] -/ @@ -416,11 +409,11 @@ def hashmap_hash_map_get_mut_in_list_back 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 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 + 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] -/ @@ -429,15 +422,15 @@ def hashmap_hash_map_get_mut_back 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 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 + 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 + hash_mod l0 result.ret { hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, @@ -455,7 +448,7 @@ def hashmap_hash_map_remove_from_list_loop_fwd then let mv_ls := mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey - t tl) hashmap_list_t.HashmapListNil + t tl) hashmap_list_t.HashmapListNil match mv_ls with | hashmap_list_t.HashmapListCons i cvalue tl0 => result.ret (Option.some cvalue) @@ -466,7 +459,7 @@ def hashmap_hash_map_remove_from_list_loop_fwd termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls => hashmap_hash_map_remove_from_list_loop_terminates - T key ls + T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ @@ -485,20 +478,20 @@ def hashmap_hash_map_remove_from_list_loop_back then let mv_ls := mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey - t tl) hashmap_list_t.HashmapListNil + 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) + let tl0 <- hashmap_hash_map_remove_from_list_loop_back T key tl + result.ret (hashmap_list_t.HashmapListCons ckey t tl0) | 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 + T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ @@ -512,18 +505,18 @@ def hashmap_hash_map_remove_from_list_back 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 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 + 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)) + (USize.ofNatCore 1 (by intlit)) result.ret (Option.some x0) @@ -533,19 +526,19 @@ def hashmap_hash_map_remove_back 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 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 + 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 l0 <- hashmap_hash_map_remove_from_list_back T key l + 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 + hash_mod l0 result.ret { hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, @@ -556,11 +549,11 @@ def hashmap_hash_map_remove_back | 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 + (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 + hash_mod l0 result.ret { hashmap_hash_map_num_entries := i0, @@ -573,21 +566,21 @@ def hashmap_hash_map_remove_back /- [hashmap_main::hashmap::test1] -/ def hashmap_test1_fwd : result Unit := do - let hm <- hashmap_hash_map_new_fwd UInt64 + 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)) + (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)) + (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)) + (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)) + (USize.ofNatCore 1056 (by intlit)) (UInt64.ofNatCore 256 (by intlit)) let i <- - hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by intlit)) + 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 @@ -595,17 +588,17 @@ def hashmap_test1_fwd : result Unit := let hm4 <- hashmap_hash_map_get_mut_back UInt64 hm3 (USize.ofNatCore 1024 (by intlit)) - (UInt64.ofNatCore 56 (by intlit)) + (UInt64.ofNatCore 56 (by intlit)) let i0 <- hashmap_hash_map_get_fwd UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) + (USize.ofNatCore 1024 (by intlit)) if not (i0 = (UInt64.ofNatCore 56 (by intlit))) then result.fail error.panic else do let x <- hashmap_hash_map_remove_fwd UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) + (USize.ofNatCore 1024 (by intlit)) match x with | Option.none => result.fail error.panic | Option.some x0 => @@ -615,24 +608,24 @@ def hashmap_test1_fwd : result Unit := do let hm5 <- hashmap_hash_map_remove_back UInt64 hm4 - (USize.ofNatCore 1024 (by intlit)) + (USize.ofNatCore 1024 (by intlit)) let i1 <- hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 0 (by intlit)) + (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)) + (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)) + (USize.ofNatCore 1056 (by intlit)) if not (i3 = (UInt64.ofNatCore 256 (by intlit))) then result.fail error.panic else result.ret () @@ -645,9 +638,9 @@ def hashmap_test1_fwd : result Unit := def insert_on_disk_fwd (key : USize) (value : UInt64) (st : state) : result (state × Unit) := do - let (st0, hm) <- opaque_defs.hashmap_utils_deserialize_fwd st - let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value - let (st1, _) <- opaque_defs.hashmap_utils_serialize_fwd hm0 st0 + let (st0, hm) <- opaque_defs.hashmap_utils_deserialize_fwd st + let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value + let (st1, _) <- opaque_defs.hashmap_utils_serialize_fwd hm0 st0 result.ret (st1, ()) /- [hashmap_main::main] -/ |