diff options
Diffstat (limited to 'tests/lean/hashmap_on_disk/HashmapMain')
4 files changed, 247 insertions, 221 deletions
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean index 3466e7e0..a514c58a 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean @@ -6,7 +6,7 @@ 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 : Vec (hashmap_list_t T)) (n : USize) := (slots, n) syntax "hashmap_hash_map_allocate_slots_loop_decreases" term+ : tactic @@ -15,16 +15,17 @@ macro_rules | `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) => `(tactic| sorry) -/- [hashmap_main::hashmap::HashMap::{0}::clear]: termination measure -/ +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/ @[simp] -def hashmap_hash_map_clear_loop_terminates (T : Type) - (slots : vec (hashmap_list_t T)) (i : USize) := +def hashmap_hash_map_clear_slots_loop_terminates (T : Type) + (slots : Vec (hashmap_list_t T)) (i : USize) := (slots, i) -syntax "hashmap_hash_map_clear_loop_decreases" term+ : tactic +syntax "hashmap_hash_map_clear_slots_loop_decreases" term+ : tactic macro_rules -| `(tactic| hashmap_hash_map_clear_loop_decreases $slots $i) =>`(tactic| sorry) +| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) => + `(tactic| sorry) /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/ @[simp] @@ -53,7 +54,7 @@ $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 : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) (i : USize) := (ntable, slots, i) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 1abc9f8d..ee50f126 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -3,35 +3,35 @@ import Base.Primitives import HashmapMain.Types import HashmapMain.Opaque -import HashmapMain.Clauses.Clauses +import HashmapMain.Clauses.Template section variable (opaque_defs: OpaqueDefs) /- [hashmap_main::hashmap::hash_key] -/ -def hashmap_hash_key_fwd (k : USize) : result USize := - result.ret k +def hashmap_hash_key_fwd (k : USize) : Result USize := Result.ret k /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap_hash_map_allocate_slots_loop_fwd - (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) : - (result (vec (hashmap_list_t T))) + (T : Type) (slots : Vec (hashmap_list_t T)) (n : USize) : + (Result (Vec (hashmap_list_t T))) := if n > (USize.ofNatCore 0 (by intlit)) 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 + 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 + hashmap_hash_map_allocate_slots_loop_terminates + T slots n decreasing_by hashmap_hash_map_allocate_slots_loop_decreases slots n /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap_hash_map_allocate_slots_fwd - (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) : - result (vec (hashmap_list_t T)) + (T : Type) (slots : Vec (hashmap_list_t T)) (n : USize) : + Result (Vec (hashmap_list_t T)) := hashmap_hash_map_allocate_slots_loop_fwd T slots n @@ -39,14 +39,14 @@ def hashmap_hash_map_allocate_slots_fwd def hashmap_hash_map_new_with_capacity_fwd (T : Type) (capacity : USize) (max_load_dividend : USize) (max_load_divisor : USize) : - result (hashmap_hash_map_t T) + 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 - result.ret + 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)), hashmap_hash_map_max_load_factor := (max_load_dividend, @@ -56,37 +56,45 @@ def hashmap_hash_map_new_with_capacity_fwd } /- [hashmap_main::hashmap::HashMap::{0}::new] -/ -def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) := +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] -/ -def hashmap_hash_map_clear_loop_fwd_back - (T : Type) (slots : vec (hashmap_list_t T)) (i : USize) : - (result (vec (hashmap_list_t T))) +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ +def hashmap_hash_map_clear_slots_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_loop_fwd_back T slots0 i1 - else result.ret slots -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_list_t.HashmapListNil + hashmap_hash_map_clear_slots_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)) /- [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) := + (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := do let v <- - hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots - (USize.ofNatCore 0 (by intlit)) - result.ret + hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots + Result.ret { hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, @@ -96,78 +104,80 @@ def hashmap_hash_map_clear_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::len] -/ def hashmap_hash_map_len_fwd - (T : Type) (self : hashmap_hash_map_t T) : result USize := - result.ret self.hashmap_hash_map_num_entries + (T : Type) (self : hashmap_hash_map_t T) : Result USize := + Result.ret self.hashmap_hash_map_num_entries /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_loop_fwd (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : - (result Bool) + (Result Bool) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key - then result.ret false + then Result.ret false else hashmap_hash_map_insert_in_list_loop_fwd T key value tl - | hashmap_list_t.HashmapListNil => result.ret true + | 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] -/ def hashmap_hash_map_insert_in_list_fwd - (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : result Bool := + (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : Result Bool := hashmap_hash_map_insert_in_list_loop_fwd T key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_loop_back (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : - (result (hashmap_list_t 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 value tl) + then Result.ret (hashmap_list_t.HashmapListCons ckey value tl) else do - let tl0 <- hashmap_hash_map_insert_in_list_loop_back T key value tl - result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) + 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 - result.ret (hashmap_list_t.HashmapListCons key value l) + 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] -/ def hashmap_hash_map_insert_in_list_back (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : - result (hashmap_list_t T) + Result (hashmap_list_t T) := hashmap_hash_map_insert_in_list_loop_back T key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] -/ def hashmap_hash_map_insert_no_resize_fwd_back (T : Type) (self : hashmap_hash_map_t T) (key : USize) (value : T) : - result (hashmap_hash_map_t 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 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 - result.ret + hash_mod l0 + Result.ret { hashmap_hash_map_num_entries := i0, hashmap_hash_map_max_load_factor := self.hashmap_hash_map_max_load_factor, @@ -176,11 +186,11 @@ 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 - result.ret + 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, @@ -189,84 +199,85 @@ def hashmap_hash_map_insert_no_resize_fwd_back } /- [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_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)) + (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 + 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_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 + => 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) + 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)) + (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)))) + (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) + 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] -/ def hashmap_hash_map_move_elements_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) + (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))) + 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) := + (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)) - result.ret + 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), @@ -274,7 +285,7 @@ def hashmap_hash_map_try_resize_fwd_back hashmap_hash_map_slots := ntable0.hashmap_hash_map_slots } else - result.ret + Result.ret { hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, hashmap_hash_map_max_load_factor := (i, i0), @@ -285,143 +296,149 @@ def hashmap_hash_map_try_resize_fwd_back /- [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) + 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 + 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) := + (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 + 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_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] -/ def hashmap_hash_map_contains_key_in_list_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := + (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 := + (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] -/ def hashmap_hash_map_get_in_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : (result T) := + (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 + 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_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 + 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 := + (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 := + (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] -/ def hashmap_hash_map_get_mut_in_list_loop_fwd - (T : Type) (ls : hashmap_list_t T) (key : USize) : (result T) := + (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 + 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 + | 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 + 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 := + (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)) + (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) + then Result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl) else do - 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 + 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] -/ 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) + 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 := + (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] -/ 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) + 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 - result.ret + 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, @@ -431,33 +448,36 @@ def hashmap_hash_map_get_mut_back /- [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)) := + (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 + 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 + 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 + | 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 + 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) := + (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)) + (Result (hashmap_list_t T)) := match ls with | hashmap_list_t.HashmapListCons ckey t tl => @@ -465,64 +485,68 @@ 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 + | hashmap_list_t.HashmapListCons i cvalue tl0 => Result.ret tl0 + | hashmap_list_t.HashmapListNil => Result.fail Error.panic + else do - 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 + 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 + 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) + 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) := + (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.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) + (USize.ofNatCore 1 (by intlit)) + Result.ret (Option.some x0) + /- [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) + 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 - result.ret + 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, @@ -532,101 +556,102 @@ 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 - result.ret + 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 := +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 + 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)) + (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 + 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.none => Result.fail Error.panic | Option.some x0 => if not (x0 = (UInt64.ofNatCore 56 (by intlit))) - then result.fail error.panic + then Result.fail Error.panic else 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 + 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 + 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 () + 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) := + (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 - result.ret (st1, ()) + 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] -/ -def main_fwd : result Unit := - result.ret () +def main_fwd : Result Unit := Result.ret () /- Unit test for [hashmap_main::main] -/ #assert (main_fwd = .ret ()) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean index ce618a6c..3531e6e0 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean @@ -7,9 +7,9 @@ structure OpaqueDefs where /- [hashmap_main::hashmap_utils::deserialize] -/ hashmap_utils_deserialize_fwd - : state -> result (state × (hashmap_hash_map_t UInt64)) + : State -> Result (State × (hashmap_hash_map_t UInt64)) /- [hashmap_main::hashmap_utils::serialize] -/ hashmap_utils_serialize_fwd - : hashmap_hash_map_t UInt64 -> state -> result (state × Unit) + : hashmap_hash_map_t UInt64 -> State -> Result (State × Unit) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean index 2a3ea462..40f9b7e9 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -13,7 +13,7 @@ structure hashmap_hash_map_t (T : Type) where hashmap_hash_map_num_entries : USize hashmap_hash_map_max_load_factor : (USize × USize) hashmap_hash_map_max_load : USize - hashmap_hash_map_slots : vec (hashmap_list_t T) + hashmap_hash_map_slots : Vec (hashmap_list_t T) -/- The state type used in the state-error monad -/ axiom state : Type +/- The state type used in the state-error monad -/ axiom State : Type |