From 87d6f6c7c90bf7b427397d6bd2e2c70d610678e3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 4 Jul 2023 14:57:51 +0200 Subject: Reorganize the Lean tests --- tests/lean/Hashmap/Funs.lean | 474 ++++++++++++++++++++++++++++++++++++++++++ tests/lean/Hashmap/Types.lean | 17 ++ 2 files changed, 491 insertions(+) create mode 100644 tests/lean/Hashmap/Funs.lean create mode 100644 tests/lean/Hashmap/Types.lean (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean new file mode 100644 index 00000000..26742d5d --- /dev/null +++ b/tests/lean/Hashmap/Funs.lean @@ -0,0 +1,474 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap]: function definitions +import Base +import Hashmap.Types +open Primitives + +/- [hashmap::hash_key] -/ +def hash_key_fwd (k : Usize) : Result Usize := + Result.ret k + +/- [hashmap::HashMap::{0}::allocate_slots] -/ +divergent def hash_map_allocate_slots_loop_fwd + (T : Type) (slots : Vec (list_t T)) (n : Usize) : Result (Vec (list_t T)) := + if n > (Usize.ofInt 0 (by intlit)) + then + do + let slots0 ← vec_push_back (list_t T) slots list_t.Nil + let n0 ← n - (Usize.ofInt 1 (by intlit)) + hash_map_allocate_slots_loop_fwd T slots0 n0 + else Result.ret slots + +/- [hashmap::HashMap::{0}::allocate_slots] -/ +def hash_map_allocate_slots_fwd + (T : Type) (slots : Vec (list_t T)) (n : Usize) : Result (Vec (list_t T)) := + hash_map_allocate_slots_loop_fwd T slots n + +/- [hashmap::HashMap::{0}::new_with_capacity] -/ +def hash_map_new_with_capacity_fwd + (T : Type) (capacity : Usize) (max_load_dividend : Usize) + (max_load_divisor : Usize) : + Result (hash_map_t T) + := + do + let v := vec_new (list_t T) + let slots ← hash_map_allocate_slots_fwd T v capacity + let i ← capacity * max_load_dividend + let i0 ← i / max_load_divisor + Result.ret + { + hash_map_num_entries := (Usize.ofInt 0 (by intlit)), + hash_map_max_load_factor := (max_load_dividend, max_load_divisor), + hash_map_max_load := i0, + hash_map_slots := slots + } + +/- [hashmap::HashMap::{0}::new] -/ +def hash_map_new_fwd (T : Type) : Result (hash_map_t T) := + hash_map_new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) + (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) + +/- [hashmap::HashMap::{0}::clear] -/ +divergent def hash_map_clear_loop_fwd_back + (T : Type) (slots : Vec (list_t T)) (i : Usize) : Result (Vec (list_t T)) := + let i0 := vec_len (list_t T) slots + if i < i0 + then + do + let i1 ← i + (Usize.ofInt 1 (by intlit)) + let slots0 ← vec_index_mut_back (list_t T) slots i list_t.Nil + hash_map_clear_loop_fwd_back T slots0 i1 + else Result.ret slots + +/- [hashmap::HashMap::{0}::clear] -/ +def hash_map_clear_fwd_back + (T : Type) (self : hash_map_t T) : Result (hash_map_t T) := + do + let v ← + hash_map_clear_loop_fwd_back T self.hash_map_slots + (Usize.ofInt 0 (by intlit)) + Result.ret + { + self + with + hash_map_num_entries := (Usize.ofInt 0 (by intlit)), + hash_map_slots := v + } + +/- [hashmap::HashMap::{0}::len] -/ +def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result Usize := + Result.ret self.hash_map_num_entries + +/- [hashmap::HashMap::{0}::insert_in_list] -/ +divergent def hash_map_insert_in_list_loop_fwd + (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool := + match h: ls with + | list_t.Cons ckey cvalue tl => + if ckey = key + then Result.ret false + else hash_map_insert_in_list_loop_fwd T key value tl + | list_t.Nil => Result.ret true + +/- [hashmap::HashMap::{0}::insert_in_list] -/ +def hash_map_insert_in_list_fwd + (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool := + hash_map_insert_in_list_loop_fwd T key value ls + +/- [hashmap::HashMap::{0}::insert_in_list] -/ +divergent def hash_map_insert_in_list_loop_back + (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) := + match h: ls with + | list_t.Cons ckey cvalue tl => + if ckey = key + then Result.ret (list_t.Cons ckey value tl) + else + do + let tl0 ← hash_map_insert_in_list_loop_back T key value tl + Result.ret (list_t.Cons ckey cvalue tl0) + | list_t.Nil => let l := list_t.Nil + Result.ret (list_t.Cons key value l) + +/- [hashmap::HashMap::{0}::insert_in_list] -/ +def hash_map_insert_in_list_back + (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) := + hash_map_insert_in_list_loop_back T key value ls + +/- [hashmap::HashMap::{0}::insert_no_resize] -/ +def hash_map_insert_no_resize_fwd_back + (T : Type) (self : hash_map_t T) (key : Usize) (value : T) : + Result (hash_map_t T) + := + do + let hash ← hash_key_fwd key + let i := vec_len (list_t T) self.hash_map_slots + let hash_mod ← hash % i + let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let inserted ← hash_map_insert_in_list_fwd T key value l + if inserted + then + do + let i0 ← self.hash_map_num_entries + (Usize.ofInt 1 (by intlit)) + let l0 ← hash_map_insert_in_list_back T key value l + let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + Result.ret + { self with hash_map_num_entries := i0, hash_map_slots := v } + else + do + let l0 ← hash_map_insert_in_list_back T key value l + let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + Result.ret { self with hash_map_slots := v } + +/- [core::num::u32::{9}::MAX] -/ +def core_num_u32_max_body : Result U32 := + Result.ret (U32.ofInt 4294967295 (by intlit)) +def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) + +/- [hashmap::HashMap::{0}::move_elements_from_list] -/ +divergent def hash_map_move_elements_from_list_loop_fwd_back + (T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) := + match h: ls with + | list_t.Cons k v tl => + do + let ntable0 ← hash_map_insert_no_resize_fwd_back T ntable k v + hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl + | list_t.Nil => Result.ret ntable + +/- [hashmap::HashMap::{0}::move_elements_from_list] -/ +def hash_map_move_elements_from_list_fwd_back + (T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) := + hash_map_move_elements_from_list_loop_fwd_back T ntable ls + +/- [hashmap::HashMap::{0}::move_elements] -/ +divergent def hash_map_move_elements_loop_fwd_back + (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : Usize) : + Result ((hash_map_t T) × (Vec (list_t T))) + := + let i0 := vec_len (list_t T) slots + if i < i0 + then + do + let l ← vec_index_mut_fwd (list_t T) slots i + let ls := mem_replace_fwd (list_t T) l list_t.Nil + let ntable0 ← hash_map_move_elements_from_list_fwd_back T ntable ls + let i1 ← i + (Usize.ofInt 1 (by intlit)) + let l0 := mem_replace_back (list_t T) l list_t.Nil + let slots0 ← vec_index_mut_back (list_t T) slots i l0 + hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 + else Result.ret (ntable, slots) + +/- [hashmap::HashMap::{0}::move_elements] -/ +def hash_map_move_elements_fwd_back + (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : Usize) : + Result ((hash_map_t T) × (Vec (list_t T))) + := + hash_map_move_elements_loop_fwd_back T ntable slots i + +/- [hashmap::HashMap::{0}::try_resize] -/ +def hash_map_try_resize_fwd_back + (T : Type) (self : hash_map_t T) : Result (hash_map_t T) := + do + let max_usize ← Scalar.cast .Usize core_num_u32_max_c + let capacity := vec_len (list_t T) self.hash_map_slots + let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) + let (i, i0) := self.hash_map_max_load_factor + let i1 ← n1 / i + if capacity <= i1 + then + do + let i2 ← capacity * (Usize.ofInt 2 (by intlit)) + let ntable ← hash_map_new_with_capacity_fwd T i2 i i0 + let (ntable0, _) ← + hash_map_move_elements_fwd_back T ntable self.hash_map_slots + (Usize.ofInt 0 (by intlit)) + Result.ret + { + ntable0 + with + hash_map_num_entries := self.hash_map_num_entries, + hash_map_max_load_factor := (i, i0) + } + else Result.ret { self with hash_map_max_load_factor := (i, i0) } + +/- [hashmap::HashMap::{0}::insert] -/ +def hash_map_insert_fwd_back + (T : Type) (self : hash_map_t T) (key : Usize) (value : T) : + Result (hash_map_t T) + := + do + let self0 ← hash_map_insert_no_resize_fwd_back T self key value + let i ← hash_map_len_fwd T self0 + if i > self0.hash_map_max_load + then hash_map_try_resize_fwd_back T self0 + else Result.ret self0 + +/- [hashmap::HashMap::{0}::contains_key_in_list] -/ +divergent def hash_map_contains_key_in_list_loop_fwd + (T : Type) (key : Usize) (ls : list_t T) : Result Bool := + match h: ls with + | list_t.Cons ckey t tl => + if ckey = key + then Result.ret true + else hash_map_contains_key_in_list_loop_fwd T key tl + | list_t.Nil => Result.ret false + +/- [hashmap::HashMap::{0}::contains_key_in_list] -/ +def hash_map_contains_key_in_list_fwd + (T : Type) (key : Usize) (ls : list_t T) : Result Bool := + hash_map_contains_key_in_list_loop_fwd T key ls + +/- [hashmap::HashMap::{0}::contains_key] -/ +def hash_map_contains_key_fwd + (T : Type) (self : hash_map_t T) (key : Usize) : Result Bool := + do + let hash ← hash_key_fwd key + let i := vec_len (list_t T) self.hash_map_slots + let hash_mod ← hash % i + let l ← vec_index_fwd (list_t T) self.hash_map_slots hash_mod + hash_map_contains_key_in_list_fwd T key l + +/- [hashmap::HashMap::{0}::get_in_list] -/ +divergent def hash_map_get_in_list_loop_fwd + (T : Type) (key : Usize) (ls : list_t T) : Result T := + match h: ls with + | list_t.Cons ckey cvalue tl => + if ckey = key + then Result.ret cvalue + else hash_map_get_in_list_loop_fwd T key tl + | list_t.Nil => Result.fail Error.panic + +/- [hashmap::HashMap::{0}::get_in_list] -/ +def hash_map_get_in_list_fwd + (T : Type) (key : Usize) (ls : list_t T) : Result T := + hash_map_get_in_list_loop_fwd T key ls + +/- [hashmap::HashMap::{0}::get] -/ +def hash_map_get_fwd + (T : Type) (self : hash_map_t T) (key : Usize) : Result T := + do + let hash ← hash_key_fwd key + let i := vec_len (list_t T) self.hash_map_slots + let hash_mod ← hash % i + let l ← vec_index_fwd (list_t T) self.hash_map_slots hash_mod + hash_map_get_in_list_fwd T key l + +/- [hashmap::HashMap::{0}::get_mut_in_list] -/ +divergent def hash_map_get_mut_in_list_loop_fwd + (T : Type) (ls : list_t T) (key : Usize) : Result T := + match h: ls with + | list_t.Cons ckey cvalue tl => + if ckey = key + then Result.ret cvalue + else hash_map_get_mut_in_list_loop_fwd T tl key + | list_t.Nil => Result.fail Error.panic + +/- [hashmap::HashMap::{0}::get_mut_in_list] -/ +def hash_map_get_mut_in_list_fwd + (T : Type) (ls : list_t T) (key : Usize) : Result T := + hash_map_get_mut_in_list_loop_fwd T ls key + +/- [hashmap::HashMap::{0}::get_mut_in_list] -/ +divergent def hash_map_get_mut_in_list_loop_back + (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) := + match h: ls with + | list_t.Cons ckey cvalue tl => + if ckey = key + then Result.ret (list_t.Cons ckey ret0 tl) + else + do + let tl0 ← hash_map_get_mut_in_list_loop_back T tl key ret0 + Result.ret (list_t.Cons ckey cvalue tl0) + | list_t.Nil => Result.fail Error.panic + +/- [hashmap::HashMap::{0}::get_mut_in_list] -/ +def hash_map_get_mut_in_list_back + (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) := + hash_map_get_mut_in_list_loop_back T ls key ret0 + +/- [hashmap::HashMap::{0}::get_mut] -/ +def hash_map_get_mut_fwd + (T : Type) (self : hash_map_t T) (key : Usize) : Result T := + do + let hash ← hash_key_fwd key + let i := vec_len (list_t T) self.hash_map_slots + let hash_mod ← hash % i + let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + hash_map_get_mut_in_list_fwd T l key + +/- [hashmap::HashMap::{0}::get_mut] -/ +def hash_map_get_mut_back + (T : Type) (self : hash_map_t T) (key : Usize) (ret0 : T) : + Result (hash_map_t T) + := + do + let hash ← hash_key_fwd key + let i := vec_len (list_t T) self.hash_map_slots + let hash_mod ← hash % i + let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l0 ← hash_map_get_mut_in_list_back T l key ret0 + let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + Result.ret { self with hash_map_slots := v } + +/- [hashmap::HashMap::{0}::remove_from_list] -/ +divergent def hash_map_remove_from_list_loop_fwd + (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) := + match h: ls with + | list_t.Cons ckey t tl => + if ckey = key + then + let mv_ls := + mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil + match h: mv_ls with + | list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | list_t.Nil => Result.fail Error.panic + else hash_map_remove_from_list_loop_fwd T key tl + | list_t.Nil => Result.ret Option.none + +/- [hashmap::HashMap::{0}::remove_from_list] -/ +def hash_map_remove_from_list_fwd + (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) := + hash_map_remove_from_list_loop_fwd T key ls + +/- [hashmap::HashMap::{0}::remove_from_list] -/ +divergent def hash_map_remove_from_list_loop_back + (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) := + match h: ls with + | list_t.Cons ckey t tl => + if ckey = key + then + let mv_ls := + mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil + match h: mv_ls with + | list_t.Cons i cvalue tl0 => Result.ret tl0 + | list_t.Nil => Result.fail Error.panic + else + do + let tl0 ← hash_map_remove_from_list_loop_back T key tl + Result.ret (list_t.Cons ckey t tl0) + | list_t.Nil => Result.ret list_t.Nil + +/- [hashmap::HashMap::{0}::remove_from_list] -/ +def hash_map_remove_from_list_back + (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) := + hash_map_remove_from_list_loop_back T key ls + +/- [hashmap::HashMap::{0}::remove] -/ +def hash_map_remove_fwd + (T : Type) (self : hash_map_t T) (key : Usize) : Result (Option T) := + do + let hash ← hash_key_fwd key + let i := vec_len (list_t T) self.hash_map_slots + let hash_mod ← hash % i + let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let x ← hash_map_remove_from_list_fwd T key l + match h: x with + | Option.none => Result.ret Option.none + | Option.some x0 => + do + let _ ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) + Result.ret (Option.some x0) + +/- [hashmap::HashMap::{0}::remove] -/ +def hash_map_remove_back + (T : Type) (self : hash_map_t T) (key : Usize) : Result (hash_map_t T) := + do + let hash ← hash_key_fwd key + let i := vec_len (list_t T) self.hash_map_slots + let hash_mod ← hash % i + let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let x ← hash_map_remove_from_list_fwd T key l + match h: x with + | Option.none => + do + let l0 ← hash_map_remove_from_list_back T key l + let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + Result.ret { self with hash_map_slots := v } + | Option.some x0 => + do + let i0 ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) + let l0 ← hash_map_remove_from_list_back T key l + let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + Result.ret + { self with hash_map_num_entries := i0, hash_map_slots := v } + +/- [hashmap::test1] -/ +def test1_fwd : Result Unit := + do + let hm ← hash_map_new_fwd U64 + let hm0 ← + hash_map_insert_fwd_back U64 hm (Usize.ofInt 0 (by intlit)) + (U64.ofInt 42 (by intlit)) + let hm1 ← + hash_map_insert_fwd_back U64 hm0 (Usize.ofInt 128 (by intlit)) + (U64.ofInt 18 (by intlit)) + let hm2 ← + hash_map_insert_fwd_back U64 hm1 (Usize.ofInt 1024 (by intlit)) + (U64.ofInt 138 (by intlit)) + let hm3 ← + hash_map_insert_fwd_back U64 hm2 (Usize.ofInt 1056 (by intlit)) + (U64.ofInt 256 (by intlit)) + let i ← hash_map_get_fwd U64 hm3 (Usize.ofInt 128 (by intlit)) + if not (i = (U64.ofInt 18 (by intlit))) + then Result.fail Error.panic + else + do + let hm4 ← + hash_map_get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit)) + (U64.ofInt 56 (by intlit)) + let i0 ← hash_map_get_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) + if not (i0 = (U64.ofInt 56 (by intlit))) + then Result.fail Error.panic + else + do + let x ← + hash_map_remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) + match h: x with + | Option.none => Result.fail Error.panic + | Option.some x0 => + if not (x0 = (U64.ofInt 56 (by intlit))) + then Result.fail Error.panic + else + do + let hm5 ← + hash_map_remove_back U64 hm4 (Usize.ofInt 1024 (by intlit)) + let i1 ← + hash_map_get_fwd U64 hm5 (Usize.ofInt 0 (by intlit)) + if not (i1 = (U64.ofInt 42 (by intlit))) + then Result.fail Error.panic + else + do + let i2 ← + hash_map_get_fwd U64 hm5 (Usize.ofInt 128 (by intlit)) + if not (i2 = (U64.ofInt 18 (by intlit))) + then Result.fail Error.panic + else + do + let i3 ← + hash_map_get_fwd U64 hm5 + (Usize.ofInt 1056 (by intlit)) + if not (i3 = (U64.ofInt 256 (by intlit))) + then Result.fail Error.panic + else Result.ret () + +/- Unit test for [hashmap::test1] -/ +#assert (test1_fwd == .ret ()) + diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean new file mode 100644 index 00000000..af26f363 --- /dev/null +++ b/tests/lean/Hashmap/Types.lean @@ -0,0 +1,17 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap]: type definitions +import Base +open Primitives + +/- [hashmap::List] -/ +inductive list_t (T : Type) := +| Cons : Usize -> T -> list_t T -> list_t T +| Nil : list_t T + +/- [hashmap::HashMap] -/ +structure hash_map_t (T : Type) where + hash_map_num_entries : Usize + hash_map_max_load_factor : (Usize × Usize) + hash_map_max_load : Usize + hash_map_slots : Vec (list_t T) + -- cgit v1.2.3 From b643bd00747e75d69b6066c55a1798b61277c4b6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 4 Jul 2023 18:09:36 +0200 Subject: Regenerate the Lean test files --- tests/lean/Hashmap/Funs.lean | 31 +++++++++++++++++-------------- tests/lean/Hashmap/Types.lean | 5 ++++- 2 files changed, 21 insertions(+), 15 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 26742d5d..b4254726 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -4,6 +4,8 @@ import Base import Hashmap.Types open Primitives +namespace Hashmap + /- [hashmap::hash_key] -/ def hash_key_fwd (k : Usize) : Result Usize := Result.ret k @@ -82,7 +84,7 @@ def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result Usize := /- [hashmap::HashMap::{0}::insert_in_list] -/ divergent def hash_map_insert_in_list_loop_fwd (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool := - match h: ls with + match ls with | list_t.Cons ckey cvalue tl => if ckey = key then Result.ret false @@ -97,7 +99,7 @@ def hash_map_insert_in_list_fwd /- [hashmap::HashMap::{0}::insert_in_list] -/ divergent def hash_map_insert_in_list_loop_back (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) := - match h: ls with + match ls with | list_t.Cons ckey cvalue tl => if ckey = key then Result.ret (list_t.Cons ckey value tl) @@ -146,7 +148,7 @@ def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) /- [hashmap::HashMap::{0}::move_elements_from_list] -/ divergent def hash_map_move_elements_from_list_loop_fwd_back (T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) := - match h: ls with + match ls with | list_t.Cons k v tl => do let ntable0 ← hash_map_insert_no_resize_fwd_back T ntable k v @@ -224,7 +226,7 @@ def hash_map_insert_fwd_back /- [hashmap::HashMap::{0}::contains_key_in_list] -/ divergent def hash_map_contains_key_in_list_loop_fwd (T : Type) (key : Usize) (ls : list_t T) : Result Bool := - match h: ls with + match ls with | list_t.Cons ckey t tl => if ckey = key then Result.ret true @@ -249,7 +251,7 @@ def hash_map_contains_key_fwd /- [hashmap::HashMap::{0}::get_in_list] -/ divergent def hash_map_get_in_list_loop_fwd (T : Type) (key : Usize) (ls : list_t T) : Result T := - match h: ls with + match ls with | list_t.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue @@ -274,7 +276,7 @@ def hash_map_get_fwd /- [hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def hash_map_get_mut_in_list_loop_fwd (T : Type) (ls : list_t T) (key : Usize) : Result T := - match h: ls with + match ls with | list_t.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue @@ -289,7 +291,7 @@ def hash_map_get_mut_in_list_fwd /- [hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def hash_map_get_mut_in_list_loop_back (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) := - match h: ls with + match ls with | list_t.Cons ckey cvalue tl => if ckey = key then Result.ret (list_t.Cons ckey ret0 tl) @@ -331,13 +333,13 @@ def hash_map_get_mut_back /- [hashmap::HashMap::{0}::remove_from_list] -/ divergent def hash_map_remove_from_list_loop_fwd (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) := - match h: ls with + match ls with | list_t.Cons ckey t tl => if ckey = key then let mv_ls := mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil - match h: mv_ls with + match mv_ls with | list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) | list_t.Nil => Result.fail Error.panic else hash_map_remove_from_list_loop_fwd T key tl @@ -351,13 +353,13 @@ def hash_map_remove_from_list_fwd /- [hashmap::HashMap::{0}::remove_from_list] -/ divergent def hash_map_remove_from_list_loop_back (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) := - match h: ls with + match ls with | list_t.Cons ckey t tl => if ckey = key then let mv_ls := mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil - match h: mv_ls with + match mv_ls with | list_t.Cons i cvalue tl0 => Result.ret tl0 | list_t.Nil => Result.fail Error.panic else @@ -380,7 +382,7 @@ def hash_map_remove_fwd let hash_mod ← hash % i let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod let x ← hash_map_remove_from_list_fwd T key l - match h: x with + match x with | Option.none => Result.ret Option.none | Option.some x0 => do @@ -396,7 +398,7 @@ def hash_map_remove_back let hash_mod ← hash % i let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod let x ← hash_map_remove_from_list_fwd T key l - match h: x with + match x with | Option.none => do let l0 ← hash_map_remove_from_list_back T key l @@ -441,7 +443,7 @@ def test1_fwd : Result Unit := do let x ← hash_map_remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) - match h: x with + match x with | Option.none => Result.fail Error.panic | Option.some x0 => if not (x0 = (U64.ofInt 56 (by intlit))) @@ -472,3 +474,4 @@ def test1_fwd : Result Unit := /- Unit test for [hashmap::test1] -/ #assert (test1_fwd == .ret ()) +end Hashmap diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean index af26f363..0aec6acf 100644 --- a/tests/lean/Hashmap/Types.lean +++ b/tests/lean/Hashmap/Types.lean @@ -3,9 +3,11 @@ import Base open Primitives +namespace Hashmap + /- [hashmap::List] -/ inductive list_t (T : Type) := -| Cons : Usize -> T -> list_t T -> list_t T +| Cons : Usize → T → list_t T → list_t T | Nil : list_t T /- [hashmap::HashMap] -/ @@ -15,3 +17,4 @@ structure hash_map_t (T : Type) where hash_map_max_load : Usize hash_map_slots : Vec (list_t T) +end Hashmap -- cgit v1.2.3 From 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jul 2023 14:52:23 +0200 Subject: Start using namespaces in the Lean backend --- tests/lean/Hashmap/Funs.lean | 192 +++++++++++++++++++++--------------------- tests/lean/Hashmap/Types.lean | 5 +- 2 files changed, 97 insertions(+), 100 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index b4254726..8f54eca8 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -3,38 +3,37 @@ import Base import Hashmap.Types open Primitives - -namespace Hashmap +namespace hashmap /- [hashmap::hash_key] -/ def hash_key_fwd (k : Usize) : Result Usize := Result.ret k /- [hashmap::HashMap::{0}::allocate_slots] -/ -divergent def hash_map_allocate_slots_loop_fwd +divergent def HashMap.allocate_slots_loop_fwd (T : Type) (slots : Vec (list_t T)) (n : Usize) : Result (Vec (list_t T)) := if n > (Usize.ofInt 0 (by intlit)) then do let slots0 ← vec_push_back (list_t T) slots list_t.Nil let n0 ← n - (Usize.ofInt 1 (by intlit)) - hash_map_allocate_slots_loop_fwd T slots0 n0 + HashMap.allocate_slots_loop_fwd T slots0 n0 else Result.ret slots /- [hashmap::HashMap::{0}::allocate_slots] -/ -def hash_map_allocate_slots_fwd +def HashMap.allocate_slots_fwd (T : Type) (slots : Vec (list_t T)) (n : Usize) : Result (Vec (list_t T)) := - hash_map_allocate_slots_loop_fwd T slots n + HashMap.allocate_slots_loop_fwd T slots n /- [hashmap::HashMap::{0}::new_with_capacity] -/ -def hash_map_new_with_capacity_fwd +def HashMap.new_with_capacity_fwd (T : Type) (capacity : Usize) (max_load_dividend : Usize) (max_load_divisor : Usize) : Result (hash_map_t T) := do let v := vec_new (list_t T) - let slots ← hash_map_allocate_slots_fwd T v capacity + let slots ← HashMap.allocate_slots_fwd T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor Result.ret @@ -46,12 +45,12 @@ def hash_map_new_with_capacity_fwd } /- [hashmap::HashMap::{0}::new] -/ -def hash_map_new_fwd (T : Type) : Result (hash_map_t T) := - hash_map_new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) +def HashMap.new_fwd (T : Type) : Result (hash_map_t T) := + HashMap.new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) /- [hashmap::HashMap::{0}::clear] -/ -divergent def hash_map_clear_loop_fwd_back +divergent def HashMap.clear_loop_fwd_back (T : Type) (slots : Vec (list_t T)) (i : Usize) : Result (Vec (list_t T)) := let i0 := vec_len (list_t T) slots if i < i0 @@ -59,15 +58,15 @@ divergent def hash_map_clear_loop_fwd_back do let i1 ← i + (Usize.ofInt 1 (by intlit)) let slots0 ← vec_index_mut_back (list_t T) slots i list_t.Nil - hash_map_clear_loop_fwd_back T slots0 i1 + HashMap.clear_loop_fwd_back T slots0 i1 else Result.ret slots /- [hashmap::HashMap::{0}::clear] -/ -def hash_map_clear_fwd_back +def HashMap.clear_fwd_back (T : Type) (self : hash_map_t T) : Result (hash_map_t T) := do let v ← - hash_map_clear_loop_fwd_back T self.hash_map_slots + HashMap.clear_loop_fwd_back T self.hash_map_slots (Usize.ofInt 0 (by intlit)) Result.ret { @@ -78,26 +77,26 @@ def hash_map_clear_fwd_back } /- [hashmap::HashMap::{0}::len] -/ -def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result Usize := +def HashMap.len_fwd (T : Type) (self : hash_map_t T) : Result Usize := Result.ret self.hash_map_num_entries /- [hashmap::HashMap::{0}::insert_in_list] -/ -divergent def hash_map_insert_in_list_loop_fwd +divergent def HashMap.insert_in_list_loop_fwd (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool := match ls with | list_t.Cons ckey cvalue tl => if ckey = key then Result.ret false - else hash_map_insert_in_list_loop_fwd T key value tl + else HashMap.insert_in_list_loop_fwd T key value tl | list_t.Nil => Result.ret true /- [hashmap::HashMap::{0}::insert_in_list] -/ -def hash_map_insert_in_list_fwd +def HashMap.insert_in_list_fwd (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool := - hash_map_insert_in_list_loop_fwd T key value ls + HashMap.insert_in_list_loop_fwd T key value ls /- [hashmap::HashMap::{0}::insert_in_list] -/ -divergent def hash_map_insert_in_list_loop_back +divergent def HashMap.insert_in_list_loop_back (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) := match ls with | list_t.Cons ckey cvalue tl => @@ -105,18 +104,18 @@ divergent def hash_map_insert_in_list_loop_back then Result.ret (list_t.Cons ckey value tl) else do - let tl0 ← hash_map_insert_in_list_loop_back T key value tl + let tl0 ← HashMap.insert_in_list_loop_back T key value tl Result.ret (list_t.Cons ckey cvalue tl0) | list_t.Nil => let l := list_t.Nil Result.ret (list_t.Cons key value l) /- [hashmap::HashMap::{0}::insert_in_list] -/ -def hash_map_insert_in_list_back +def HashMap.insert_in_list_back (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) := - hash_map_insert_in_list_loop_back T key value ls + HashMap.insert_in_list_loop_back T key value ls /- [hashmap::HashMap::{0}::insert_no_resize] -/ -def hash_map_insert_no_resize_fwd_back +def HashMap.insert_no_resize_fwd_back (T : Type) (self : hash_map_t T) (key : Usize) (value : T) : Result (hash_map_t T) := @@ -125,18 +124,18 @@ def hash_map_insert_no_resize_fwd_back let i := vec_len (list_t T) self.hash_map_slots let hash_mod ← hash % i let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod - let inserted ← hash_map_insert_in_list_fwd T key value l + let inserted ← HashMap.insert_in_list_fwd T key value l if inserted then do let i0 ← self.hash_map_num_entries + (Usize.ofInt 1 (by intlit)) - let l0 ← hash_map_insert_in_list_back T key value l + let l0 ← HashMap.insert_in_list_back T key value l let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_num_entries := i0, hash_map_slots := v } else do - let l0 ← hash_map_insert_in_list_back T key value l + let l0 ← HashMap.insert_in_list_back T key value l let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } @@ -146,22 +145,22 @@ def core_num_u32_max_body : Result U32 := def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) /- [hashmap::HashMap::{0}::move_elements_from_list] -/ -divergent def hash_map_move_elements_from_list_loop_fwd_back +divergent def HashMap.move_elements_from_list_loop_fwd_back (T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) := match ls with | list_t.Cons k v tl => do - let ntable0 ← hash_map_insert_no_resize_fwd_back T ntable k v - hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl + let ntable0 ← HashMap.insert_no_resize_fwd_back T ntable k v + HashMap.move_elements_from_list_loop_fwd_back T ntable0 tl | list_t.Nil => Result.ret ntable /- [hashmap::HashMap::{0}::move_elements_from_list] -/ -def hash_map_move_elements_from_list_fwd_back +def HashMap.move_elements_from_list_fwd_back (T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) := - hash_map_move_elements_from_list_loop_fwd_back T ntable ls + HashMap.move_elements_from_list_loop_fwd_back T ntable ls /- [hashmap::HashMap::{0}::move_elements] -/ -divergent def hash_map_move_elements_loop_fwd_back +divergent def HashMap.move_elements_loop_fwd_back (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : Usize) : Result ((hash_map_t T) × (Vec (list_t T))) := @@ -171,22 +170,22 @@ divergent def hash_map_move_elements_loop_fwd_back do let l ← vec_index_mut_fwd (list_t T) slots i let ls := mem_replace_fwd (list_t T) l list_t.Nil - let ntable0 ← hash_map_move_elements_from_list_fwd_back T ntable ls + let ntable0 ← HashMap.move_elements_from_list_fwd_back T ntable ls let i1 ← i + (Usize.ofInt 1 (by intlit)) let l0 := mem_replace_back (list_t T) l list_t.Nil let slots0 ← vec_index_mut_back (list_t T) slots i l0 - hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 + HashMap.move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) /- [hashmap::HashMap::{0}::move_elements] -/ -def hash_map_move_elements_fwd_back +def HashMap.move_elements_fwd_back (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : Usize) : Result ((hash_map_t T) × (Vec (list_t T))) := - hash_map_move_elements_loop_fwd_back T ntable slots i + HashMap.move_elements_loop_fwd_back T ntable slots i /- [hashmap::HashMap::{0}::try_resize] -/ -def hash_map_try_resize_fwd_back +def HashMap.try_resize_fwd_back (T : Type) (self : hash_map_t T) : Result (hash_map_t T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c @@ -198,9 +197,9 @@ def hash_map_try_resize_fwd_back then do let i2 ← capacity * (Usize.ofInt 2 (by intlit)) - let ntable ← hash_map_new_with_capacity_fwd T i2 i i0 + let ntable ← HashMap.new_with_capacity_fwd T i2 i i0 let (ntable0, _) ← - hash_map_move_elements_fwd_back T ntable self.hash_map_slots + HashMap.move_elements_fwd_back T ntable self.hash_map_slots (Usize.ofInt 0 (by intlit)) Result.ret { @@ -212,84 +211,84 @@ def hash_map_try_resize_fwd_back else Result.ret { self with hash_map_max_load_factor := (i, i0) } /- [hashmap::HashMap::{0}::insert] -/ -def hash_map_insert_fwd_back +def HashMap.insert_fwd_back (T : Type) (self : hash_map_t T) (key : Usize) (value : T) : Result (hash_map_t T) := do - let self0 ← hash_map_insert_no_resize_fwd_back T self key value - let i ← hash_map_len_fwd T self0 + let self0 ← HashMap.insert_no_resize_fwd_back T self key value + let i ← HashMap.len_fwd T self0 if i > self0.hash_map_max_load - then hash_map_try_resize_fwd_back T self0 + then HashMap.try_resize_fwd_back T self0 else Result.ret self0 /- [hashmap::HashMap::{0}::contains_key_in_list] -/ -divergent def hash_map_contains_key_in_list_loop_fwd +divergent def HashMap.contains_key_in_list_loop_fwd (T : Type) (key : Usize) (ls : list_t T) : Result Bool := match ls with | list_t.Cons ckey t tl => if ckey = key then Result.ret true - else hash_map_contains_key_in_list_loop_fwd T key tl + else HashMap.contains_key_in_list_loop_fwd T key tl | list_t.Nil => Result.ret false /- [hashmap::HashMap::{0}::contains_key_in_list] -/ -def hash_map_contains_key_in_list_fwd +def HashMap.contains_key_in_list_fwd (T : Type) (key : Usize) (ls : list_t T) : Result Bool := - hash_map_contains_key_in_list_loop_fwd T key ls + HashMap.contains_key_in_list_loop_fwd T key ls /- [hashmap::HashMap::{0}::contains_key] -/ -def hash_map_contains_key_fwd +def HashMap.contains_key_fwd (T : Type) (self : hash_map_t T) (key : Usize) : Result Bool := do let hash ← hash_key_fwd key let i := vec_len (list_t T) self.hash_map_slots let hash_mod ← hash % i let l ← vec_index_fwd (list_t T) self.hash_map_slots hash_mod - hash_map_contains_key_in_list_fwd T key l + HashMap.contains_key_in_list_fwd T key l /- [hashmap::HashMap::{0}::get_in_list] -/ -divergent def hash_map_get_in_list_loop_fwd +divergent def HashMap.get_in_list_loop_fwd (T : Type) (key : Usize) (ls : list_t T) : Result T := match ls with | list_t.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue - else hash_map_get_in_list_loop_fwd T key tl + else HashMap.get_in_list_loop_fwd T key tl | list_t.Nil => Result.fail Error.panic /- [hashmap::HashMap::{0}::get_in_list] -/ -def hash_map_get_in_list_fwd +def HashMap.get_in_list_fwd (T : Type) (key : Usize) (ls : list_t T) : Result T := - hash_map_get_in_list_loop_fwd T key ls + HashMap.get_in_list_loop_fwd T key ls /- [hashmap::HashMap::{0}::get] -/ -def hash_map_get_fwd +def HashMap.get_fwd (T : Type) (self : hash_map_t T) (key : Usize) : Result T := do let hash ← hash_key_fwd key let i := vec_len (list_t T) self.hash_map_slots let hash_mod ← hash % i let l ← vec_index_fwd (list_t T) self.hash_map_slots hash_mod - hash_map_get_in_list_fwd T key l + HashMap.get_in_list_fwd T key l /- [hashmap::HashMap::{0}::get_mut_in_list] -/ -divergent def hash_map_get_mut_in_list_loop_fwd +divergent def HashMap.get_mut_in_list_loop_fwd (T : Type) (ls : list_t T) (key : Usize) : Result T := match ls with | list_t.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue - else hash_map_get_mut_in_list_loop_fwd T tl key + else HashMap.get_mut_in_list_loop_fwd T tl key | list_t.Nil => Result.fail Error.panic /- [hashmap::HashMap::{0}::get_mut_in_list] -/ -def hash_map_get_mut_in_list_fwd +def HashMap.get_mut_in_list_fwd (T : Type) (ls : list_t T) (key : Usize) : Result T := - hash_map_get_mut_in_list_loop_fwd T ls key + HashMap.get_mut_in_list_loop_fwd T ls key /- [hashmap::HashMap::{0}::get_mut_in_list] -/ -divergent def hash_map_get_mut_in_list_loop_back +divergent def HashMap.get_mut_in_list_loop_back (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) := match ls with | list_t.Cons ckey cvalue tl => @@ -297,27 +296,27 @@ divergent def hash_map_get_mut_in_list_loop_back then Result.ret (list_t.Cons ckey ret0 tl) else do - let tl0 ← hash_map_get_mut_in_list_loop_back T tl key ret0 + let tl0 ← HashMap.get_mut_in_list_loop_back T tl key ret0 Result.ret (list_t.Cons ckey cvalue tl0) | list_t.Nil => Result.fail Error.panic /- [hashmap::HashMap::{0}::get_mut_in_list] -/ -def hash_map_get_mut_in_list_back +def HashMap.get_mut_in_list_back (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) := - hash_map_get_mut_in_list_loop_back T ls key ret0 + HashMap.get_mut_in_list_loop_back T ls key ret0 /- [hashmap::HashMap::{0}::get_mut] -/ -def hash_map_get_mut_fwd +def HashMap.get_mut_fwd (T : Type) (self : hash_map_t T) (key : Usize) : Result T := do let hash ← hash_key_fwd key let i := vec_len (list_t T) self.hash_map_slots let hash_mod ← hash % i let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod - hash_map_get_mut_in_list_fwd T l key + HashMap.get_mut_in_list_fwd T l key /- [hashmap::HashMap::{0}::get_mut] -/ -def hash_map_get_mut_back +def HashMap.get_mut_back (T : Type) (self : hash_map_t T) (key : Usize) (ret0 : T) : Result (hash_map_t T) := @@ -326,12 +325,12 @@ def hash_map_get_mut_back let i := vec_len (list_t T) self.hash_map_slots let hash_mod ← hash % i let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod - let l0 ← hash_map_get_mut_in_list_back T l key ret0 + let l0 ← HashMap.get_mut_in_list_back T l key ret0 let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } /- [hashmap::HashMap::{0}::remove_from_list] -/ -divergent def hash_map_remove_from_list_loop_fwd +divergent def HashMap.remove_from_list_loop_fwd (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) := match ls with | list_t.Cons ckey t tl => @@ -342,16 +341,16 @@ divergent def hash_map_remove_from_list_loop_fwd match mv_ls with | list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) | list_t.Nil => Result.fail Error.panic - else hash_map_remove_from_list_loop_fwd T key tl + else HashMap.remove_from_list_loop_fwd T key tl | list_t.Nil => Result.ret Option.none /- [hashmap::HashMap::{0}::remove_from_list] -/ -def hash_map_remove_from_list_fwd +def HashMap.remove_from_list_fwd (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) := - hash_map_remove_from_list_loop_fwd T key ls + HashMap.remove_from_list_loop_fwd T key ls /- [hashmap::HashMap::{0}::remove_from_list] -/ -divergent def hash_map_remove_from_list_loop_back +divergent def HashMap.remove_from_list_loop_back (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) := match ls with | list_t.Cons ckey t tl => @@ -364,24 +363,24 @@ divergent def hash_map_remove_from_list_loop_back | list_t.Nil => Result.fail Error.panic else do - let tl0 ← hash_map_remove_from_list_loop_back T key tl + let tl0 ← HashMap.remove_from_list_loop_back T key tl Result.ret (list_t.Cons ckey t tl0) | list_t.Nil => Result.ret list_t.Nil /- [hashmap::HashMap::{0}::remove_from_list] -/ -def hash_map_remove_from_list_back +def HashMap.remove_from_list_back (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) := - hash_map_remove_from_list_loop_back T key ls + HashMap.remove_from_list_loop_back T key ls /- [hashmap::HashMap::{0}::remove] -/ -def hash_map_remove_fwd +def HashMap.remove_fwd (T : Type) (self : hash_map_t T) (key : Usize) : Result (Option T) := do let hash ← hash_key_fwd key let i := vec_len (list_t T) self.hash_map_slots let hash_mod ← hash % i let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod - let x ← hash_map_remove_from_list_fwd T key l + let x ← HashMap.remove_from_list_fwd T key l match x with | Option.none => Result.ret Option.none | Option.some x0 => @@ -390,24 +389,24 @@ def hash_map_remove_fwd Result.ret (Option.some x0) /- [hashmap::HashMap::{0}::remove] -/ -def hash_map_remove_back +def HashMap.remove_back (T : Type) (self : hash_map_t T) (key : Usize) : Result (hash_map_t T) := do let hash ← hash_key_fwd key let i := vec_len (list_t T) self.hash_map_slots let hash_mod ← hash % i let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod - let x ← hash_map_remove_from_list_fwd T key l + let x ← HashMap.remove_from_list_fwd T key l match x with | Option.none => do - let l0 ← hash_map_remove_from_list_back T key l + let l0 ← HashMap.remove_from_list_back T key l let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } | Option.some x0 => do let i0 ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) - let l0 ← hash_map_remove_from_list_back T key l + let l0 ← HashMap.remove_from_list_back T key l let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_num_entries := i0, hash_map_slots := v } @@ -415,34 +414,33 @@ def hash_map_remove_back /- [hashmap::test1] -/ def test1_fwd : Result Unit := do - let hm ← hash_map_new_fwd U64 + let hm ← HashMap.new_fwd U64 let hm0 ← - hash_map_insert_fwd_back U64 hm (Usize.ofInt 0 (by intlit)) + HashMap.insert_fwd_back U64 hm (Usize.ofInt 0 (by intlit)) (U64.ofInt 42 (by intlit)) let hm1 ← - hash_map_insert_fwd_back U64 hm0 (Usize.ofInt 128 (by intlit)) + HashMap.insert_fwd_back U64 hm0 (Usize.ofInt 128 (by intlit)) (U64.ofInt 18 (by intlit)) let hm2 ← - hash_map_insert_fwd_back U64 hm1 (Usize.ofInt 1024 (by intlit)) + HashMap.insert_fwd_back U64 hm1 (Usize.ofInt 1024 (by intlit)) (U64.ofInt 138 (by intlit)) let hm3 ← - hash_map_insert_fwd_back U64 hm2 (Usize.ofInt 1056 (by intlit)) + HashMap.insert_fwd_back U64 hm2 (Usize.ofInt 1056 (by intlit)) (U64.ofInt 256 (by intlit)) - let i ← hash_map_get_fwd U64 hm3 (Usize.ofInt 128 (by intlit)) + let i ← HashMap.get_fwd U64 hm3 (Usize.ofInt 128 (by intlit)) if not (i = (U64.ofInt 18 (by intlit))) then Result.fail Error.panic else do let hm4 ← - hash_map_get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit)) + HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit)) (U64.ofInt 56 (by intlit)) - let i0 ← hash_map_get_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) + let i0 ← HashMap.get_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) if not (i0 = (U64.ofInt 56 (by intlit))) then Result.fail Error.panic else do - let x ← - hash_map_remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) + let x ← HashMap.remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) match x with | Option.none => Result.fail Error.panic | Option.some x0 => @@ -451,21 +449,21 @@ def test1_fwd : Result Unit := else do let hm5 ← - hash_map_remove_back U64 hm4 (Usize.ofInt 1024 (by intlit)) + HashMap.remove_back U64 hm4 (Usize.ofInt 1024 (by intlit)) let i1 ← - hash_map_get_fwd U64 hm5 (Usize.ofInt 0 (by intlit)) + HashMap.get_fwd U64 hm5 (Usize.ofInt 0 (by intlit)) if not (i1 = (U64.ofInt 42 (by intlit))) then Result.fail Error.panic else do let i2 ← - hash_map_get_fwd U64 hm5 (Usize.ofInt 128 (by intlit)) + HashMap.get_fwd U64 hm5 (Usize.ofInt 128 (by intlit)) if not (i2 = (U64.ofInt 18 (by intlit))) then Result.fail Error.panic else do let i3 ← - hash_map_get_fwd U64 hm5 + HashMap.get_fwd U64 hm5 (Usize.ofInt 1056 (by intlit)) if not (i3 = (U64.ofInt 256 (by intlit))) then Result.fail Error.panic @@ -474,4 +472,4 @@ def test1_fwd : Result Unit := /- Unit test for [hashmap::test1] -/ #assert (test1_fwd == .ret ()) -end Hashmap +end hashmap diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean index 0aec6acf..75a6500f 100644 --- a/tests/lean/Hashmap/Types.lean +++ b/tests/lean/Hashmap/Types.lean @@ -2,8 +2,7 @@ -- [hashmap]: type definitions import Base open Primitives - -namespace Hashmap +namespace hashmap /- [hashmap::List] -/ inductive list_t (T : Type) := @@ -17,4 +16,4 @@ structure hash_map_t (T : Type) where hash_map_max_load : Usize hash_map_slots : Vec (list_t T) -end Hashmap +end hashmap -- cgit v1.2.3 From c07721dedb2cfe4c726c42606e623395cdfe5b80 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jul 2023 15:09:07 +0200 Subject: Simplify the generated names for the types in Lean --- tests/lean/Hashmap/Funs.lean | 203 +++++++++++++++++++++--------------------- tests/lean/Hashmap/Types.lean | 10 +-- 2 files changed, 105 insertions(+), 108 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 8f54eca8..4f16688b 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -11,28 +11,28 @@ def hash_key_fwd (k : Usize) : Result Usize := /- [hashmap::HashMap::{0}::allocate_slots] -/ divergent def HashMap.allocate_slots_loop_fwd - (T : Type) (slots : Vec (list_t T)) (n : Usize) : Result (Vec (list_t T)) := + (T : Type) (slots : Vec (List T)) (n : Usize) : Result (Vec (List T)) := if n > (Usize.ofInt 0 (by intlit)) then do - let slots0 ← vec_push_back (list_t T) slots list_t.Nil + let slots0 ← vec_push_back (List T) slots List.Nil let n0 ← n - (Usize.ofInt 1 (by intlit)) HashMap.allocate_slots_loop_fwd T slots0 n0 else Result.ret slots /- [hashmap::HashMap::{0}::allocate_slots] -/ def HashMap.allocate_slots_fwd - (T : Type) (slots : Vec (list_t T)) (n : Usize) : Result (Vec (list_t T)) := + (T : Type) (slots : Vec (List T)) (n : Usize) : Result (Vec (List T)) := HashMap.allocate_slots_loop_fwd T slots n /- [hashmap::HashMap::{0}::new_with_capacity] -/ def HashMap.new_with_capacity_fwd (T : Type) (capacity : Usize) (max_load_dividend : Usize) (max_load_divisor : Usize) : - Result (hash_map_t T) + Result (HashMap T) := do - let v := vec_new (list_t T) + let v := vec_new (List T) let slots ← HashMap.allocate_slots_fwd T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor @@ -45,25 +45,25 @@ def HashMap.new_with_capacity_fwd } /- [hashmap::HashMap::{0}::new] -/ -def HashMap.new_fwd (T : Type) : Result (hash_map_t T) := +def HashMap.new_fwd (T : Type) : Result (HashMap T) := HashMap.new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) /- [hashmap::HashMap::{0}::clear] -/ divergent def HashMap.clear_loop_fwd_back - (T : Type) (slots : Vec (list_t T)) (i : Usize) : Result (Vec (list_t T)) := - let i0 := vec_len (list_t T) slots + (T : Type) (slots : Vec (List T)) (i : Usize) : Result (Vec (List T)) := + let i0 := vec_len (List T) slots if i < i0 then do let i1 ← i + (Usize.ofInt 1 (by intlit)) - let slots0 ← vec_index_mut_back (list_t T) slots i list_t.Nil + let slots0 ← vec_index_mut_back (List T) slots i List.Nil HashMap.clear_loop_fwd_back T slots0 i1 else Result.ret slots /- [hashmap::HashMap::{0}::clear] -/ def HashMap.clear_fwd_back - (T : Type) (self : hash_map_t T) : Result (hash_map_t T) := + (T : Type) (self : HashMap T) : Result (HashMap T) := do let v ← HashMap.clear_loop_fwd_back T self.hash_map_slots @@ -77,66 +77,66 @@ def HashMap.clear_fwd_back } /- [hashmap::HashMap::{0}::len] -/ -def HashMap.len_fwd (T : Type) (self : hash_map_t T) : Result Usize := +def HashMap.len_fwd (T : Type) (self : HashMap T) : Result Usize := Result.ret self.hash_map_num_entries /- [hashmap::HashMap::{0}::insert_in_list] -/ divergent def HashMap.insert_in_list_loop_fwd - (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool := + (T : Type) (key : Usize) (value : T) (ls : List T) : Result Bool := match ls with - | list_t.Cons ckey cvalue tl => + | List.Cons ckey cvalue tl => if ckey = key then Result.ret false else HashMap.insert_in_list_loop_fwd T key value tl - | list_t.Nil => Result.ret true + | List.Nil => Result.ret true /- [hashmap::HashMap::{0}::insert_in_list] -/ def HashMap.insert_in_list_fwd - (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool := + (T : Type) (key : Usize) (value : T) (ls : List T) : Result Bool := HashMap.insert_in_list_loop_fwd T key value ls /- [hashmap::HashMap::{0}::insert_in_list] -/ divergent def HashMap.insert_in_list_loop_back - (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) := + (T : Type) (key : Usize) (value : T) (ls : List T) : Result (List T) := match ls with - | list_t.Cons ckey cvalue tl => + | List.Cons ckey cvalue tl => if ckey = key - then Result.ret (list_t.Cons ckey value tl) + then Result.ret (List.Cons ckey value tl) else do let tl0 ← HashMap.insert_in_list_loop_back T key value tl - Result.ret (list_t.Cons ckey cvalue tl0) - | list_t.Nil => let l := list_t.Nil - Result.ret (list_t.Cons key value l) + Result.ret (List.Cons ckey cvalue tl0) + | List.Nil => let l := List.Nil + Result.ret (List.Cons key value l) /- [hashmap::HashMap::{0}::insert_in_list] -/ def HashMap.insert_in_list_back - (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) := + (T : Type) (key : Usize) (value : T) (ls : List T) : Result (List T) := HashMap.insert_in_list_loop_back T key value ls /- [hashmap::HashMap::{0}::insert_no_resize] -/ def HashMap.insert_no_resize_fwd_back - (T : Type) (self : hash_map_t T) (key : Usize) (value : T) : - Result (hash_map_t T) + (T : Type) (self : HashMap T) (key : Usize) (value : T) : + Result (HashMap T) := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod let inserted ← HashMap.insert_in_list_fwd T key value l if inserted then do let i0 ← self.hash_map_num_entries + (Usize.ofInt 1 (by intlit)) let l0 ← HashMap.insert_in_list_back T key value l - let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_num_entries := i0, hash_map_slots := v } else do let l0 ← HashMap.insert_in_list_back T key value l - let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } /- [core::num::u32::{9}::MAX] -/ @@ -146,50 +146,50 @@ def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) /- [hashmap::HashMap::{0}::move_elements_from_list] -/ divergent def HashMap.move_elements_from_list_loop_fwd_back - (T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) := + (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) := match ls with - | list_t.Cons k v tl => + | List.Cons k v tl => do let ntable0 ← HashMap.insert_no_resize_fwd_back T ntable k v HashMap.move_elements_from_list_loop_fwd_back T ntable0 tl - | list_t.Nil => Result.ret ntable + | List.Nil => Result.ret ntable /- [hashmap::HashMap::{0}::move_elements_from_list] -/ def HashMap.move_elements_from_list_fwd_back - (T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) := + (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) := HashMap.move_elements_from_list_loop_fwd_back T ntable ls /- [hashmap::HashMap::{0}::move_elements] -/ divergent def HashMap.move_elements_loop_fwd_back - (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : Usize) : - Result ((hash_map_t T) × (Vec (list_t T))) + (T : Type) (ntable : HashMap T) (slots : Vec (List T)) (i : Usize) : + Result ((HashMap T) × (Vec (List T))) := - let i0 := vec_len (list_t T) slots + let i0 := vec_len (List T) slots if i < i0 then do - let l ← vec_index_mut_fwd (list_t T) slots i - let ls := mem_replace_fwd (list_t T) l list_t.Nil + let l ← vec_index_mut_fwd (List T) slots i + let ls := mem_replace_fwd (List T) l List.Nil let ntable0 ← HashMap.move_elements_from_list_fwd_back T ntable ls let i1 ← i + (Usize.ofInt 1 (by intlit)) - let l0 := mem_replace_back (list_t T) l list_t.Nil - let slots0 ← vec_index_mut_back (list_t T) slots i l0 + let l0 := mem_replace_back (List T) l List.Nil + let slots0 ← vec_index_mut_back (List T) slots i l0 HashMap.move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) /- [hashmap::HashMap::{0}::move_elements] -/ def HashMap.move_elements_fwd_back - (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : Usize) : - Result ((hash_map_t T) × (Vec (list_t T))) + (T : Type) (ntable : HashMap T) (slots : Vec (List T)) (i : Usize) : + Result ((HashMap T) × (Vec (List T))) := HashMap.move_elements_loop_fwd_back T ntable slots i /- [hashmap::HashMap::{0}::try_resize] -/ def HashMap.try_resize_fwd_back - (T : Type) (self : hash_map_t T) : Result (hash_map_t T) := + (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c - let capacity := vec_len (list_t T) self.hash_map_slots + let capacity := vec_len (List T) self.hash_map_slots let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) let (i, i0) := self.hash_map_max_load_factor let i1 ← n1 / i @@ -212,8 +212,8 @@ def HashMap.try_resize_fwd_back /- [hashmap::HashMap::{0}::insert] -/ def HashMap.insert_fwd_back - (T : Type) (self : hash_map_t T) (key : Usize) (value : T) : - Result (hash_map_t T) + (T : Type) (self : HashMap T) (key : Usize) (value : T) : + Result (HashMap T) := do let self0 ← HashMap.insert_no_resize_fwd_back T self key value @@ -224,162 +224,159 @@ def HashMap.insert_fwd_back /- [hashmap::HashMap::{0}::contains_key_in_list] -/ divergent def HashMap.contains_key_in_list_loop_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result Bool := + (T : Type) (key : Usize) (ls : List T) : Result Bool := match ls with - | list_t.Cons ckey t tl => + | List.Cons ckey t tl => if ckey = key then Result.ret true else HashMap.contains_key_in_list_loop_fwd T key tl - | list_t.Nil => Result.ret false + | List.Nil => Result.ret false /- [hashmap::HashMap::{0}::contains_key_in_list] -/ def HashMap.contains_key_in_list_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result Bool := + (T : Type) (key : Usize) (ls : List T) : Result Bool := HashMap.contains_key_in_list_loop_fwd T key ls /- [hashmap::HashMap::{0}::contains_key] -/ def HashMap.contains_key_fwd - (T : Type) (self : hash_map_t T) (key : Usize) : Result Bool := + (T : Type) (self : HashMap T) (key : Usize) : Result Bool := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_fwd (List T) self.hash_map_slots hash_mod HashMap.contains_key_in_list_fwd T key l /- [hashmap::HashMap::{0}::get_in_list] -/ divergent def HashMap.get_in_list_loop_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result T := + (T : Type) (key : Usize) (ls : List T) : Result T := match ls with - | list_t.Cons ckey cvalue tl => + | List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue else HashMap.get_in_list_loop_fwd T key tl - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [hashmap::HashMap::{0}::get_in_list] -/ def HashMap.get_in_list_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result T := + (T : Type) (key : Usize) (ls : List T) : Result T := HashMap.get_in_list_loop_fwd T key ls /- [hashmap::HashMap::{0}::get] -/ -def HashMap.get_fwd - (T : Type) (self : hash_map_t T) (key : Usize) : Result T := +def HashMap.get_fwd (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_fwd (List T) self.hash_map_slots hash_mod HashMap.get_in_list_fwd T key l /- [hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def HashMap.get_mut_in_list_loop_fwd - (T : Type) (ls : list_t T) (key : Usize) : Result T := + (T : Type) (ls : List T) (key : Usize) : Result T := match ls with - | list_t.Cons ckey cvalue tl => + | List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue else HashMap.get_mut_in_list_loop_fwd T tl key - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [hashmap::HashMap::{0}::get_mut_in_list] -/ def HashMap.get_mut_in_list_fwd - (T : Type) (ls : list_t T) (key : Usize) : Result T := + (T : Type) (ls : List T) (key : Usize) : Result T := HashMap.get_mut_in_list_loop_fwd T ls key /- [hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def HashMap.get_mut_in_list_loop_back - (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) := + (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) := match ls with - | list_t.Cons ckey cvalue tl => + | List.Cons ckey cvalue tl => if ckey = key - then Result.ret (list_t.Cons ckey ret0 tl) + then Result.ret (List.Cons ckey ret0 tl) else do let tl0 ← HashMap.get_mut_in_list_loop_back T tl key ret0 - Result.ret (list_t.Cons ckey cvalue tl0) - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons ckey cvalue tl0) + | List.Nil => Result.fail Error.panic /- [hashmap::HashMap::{0}::get_mut_in_list] -/ def HashMap.get_mut_in_list_back - (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) := + (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) := HashMap.get_mut_in_list_loop_back T ls key ret0 /- [hashmap::HashMap::{0}::get_mut] -/ def HashMap.get_mut_fwd - (T : Type) (self : hash_map_t T) (key : Usize) : Result T := + (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod HashMap.get_mut_in_list_fwd T l key /- [hashmap::HashMap::{0}::get_mut] -/ def HashMap.get_mut_back - (T : Type) (self : hash_map_t T) (key : Usize) (ret0 : T) : - Result (hash_map_t T) + (T : Type) (self : HashMap T) (key : Usize) (ret0 : T) : + Result (HashMap T) := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod let l0 ← HashMap.get_mut_in_list_back T l key ret0 - let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } /- [hashmap::HashMap::{0}::remove_from_list] -/ divergent def HashMap.remove_from_list_loop_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) := + (T : Type) (key : Usize) (ls : List T) : Result (Option T) := match ls with - | list_t.Cons ckey t tl => + | List.Cons ckey t tl => if ckey = key then - let mv_ls := - mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil + let mv_ls := mem_replace_fwd (List T) (List.Cons ckey t tl) List.Nil match mv_ls with - | list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) - | list_t.Nil => Result.fail Error.panic + | List.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | List.Nil => Result.fail Error.panic else HashMap.remove_from_list_loop_fwd T key tl - | list_t.Nil => Result.ret Option.none + | List.Nil => Result.ret Option.none /- [hashmap::HashMap::{0}::remove_from_list] -/ def HashMap.remove_from_list_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) := + (T : Type) (key : Usize) (ls : List T) : Result (Option T) := HashMap.remove_from_list_loop_fwd T key ls /- [hashmap::HashMap::{0}::remove_from_list] -/ divergent def HashMap.remove_from_list_loop_back - (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) := + (T : Type) (key : Usize) (ls : List T) : Result (List T) := match ls with - | list_t.Cons ckey t tl => + | List.Cons ckey t tl => if ckey = key then - let mv_ls := - mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil + let mv_ls := mem_replace_fwd (List T) (List.Cons ckey t tl) List.Nil match mv_ls with - | list_t.Cons i cvalue tl0 => Result.ret tl0 - | list_t.Nil => Result.fail Error.panic + | List.Cons i cvalue tl0 => Result.ret tl0 + | List.Nil => Result.fail Error.panic else do let tl0 ← HashMap.remove_from_list_loop_back T key tl - Result.ret (list_t.Cons ckey t tl0) - | list_t.Nil => Result.ret list_t.Nil + Result.ret (List.Cons ckey t tl0) + | List.Nil => Result.ret List.Nil /- [hashmap::HashMap::{0}::remove_from_list] -/ def HashMap.remove_from_list_back - (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) := + (T : Type) (key : Usize) (ls : List T) : Result (List T) := HashMap.remove_from_list_loop_back T key ls /- [hashmap::HashMap::{0}::remove] -/ def HashMap.remove_fwd - (T : Type) (self : hash_map_t T) (key : Usize) : Result (Option T) := + (T : Type) (self : HashMap T) (key : Usize) : Result (Option T) := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod let x ← HashMap.remove_from_list_fwd T key l match x with | Option.none => Result.ret Option.none @@ -390,24 +387,24 @@ def HashMap.remove_fwd /- [hashmap::HashMap::{0}::remove] -/ def HashMap.remove_back - (T : Type) (self : hash_map_t T) (key : Usize) : Result (hash_map_t T) := + (T : Type) (self : HashMap T) (key : Usize) : Result (HashMap T) := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod let x ← HashMap.remove_from_list_fwd T key l match x with | Option.none => do let l0 ← HashMap.remove_from_list_back T key l - let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } | Option.some x0 => do let i0 ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) let l0 ← HashMap.remove_from_list_back T key l - let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_num_entries := i0, hash_map_slots := v } diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean index 75a6500f..7530f3b9 100644 --- a/tests/lean/Hashmap/Types.lean +++ b/tests/lean/Hashmap/Types.lean @@ -5,15 +5,15 @@ open Primitives namespace hashmap /- [hashmap::List] -/ -inductive list_t (T : Type) := -| Cons : Usize → T → list_t T → list_t T -| Nil : list_t T +inductive List (T : Type) := +| Cons : Usize → T → List T → List T +| Nil : List T /- [hashmap::HashMap] -/ -structure hash_map_t (T : Type) where +structure HashMap (T : Type) where hash_map_num_entries : Usize hash_map_max_load_factor : (Usize × Usize) hash_map_max_load : Usize - hash_map_slots : Vec (list_t T) + hash_map_slots : Vec (List T) end hashmap -- cgit v1.2.3 From 5ca36bfc50083a01af2b7ae5f75993a520757ef5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jul 2023 15:17:58 +0200 Subject: Simplify the names used in Primitives.lean --- tests/lean/Hashmap/Funs.lean | 62 ++++++++++++++++++++++---------------------- 1 file changed, 31 insertions(+), 31 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 4f16688b..48038bfb 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -15,7 +15,7 @@ divergent def HashMap.allocate_slots_loop_fwd if n > (Usize.ofInt 0 (by intlit)) then do - let slots0 ← vec_push_back (List T) slots List.Nil + let slots0 ← Vec.push (List T) slots List.Nil let n0 ← n - (Usize.ofInt 1 (by intlit)) HashMap.allocate_slots_loop_fwd T slots0 n0 else Result.ret slots @@ -32,7 +32,7 @@ def HashMap.new_with_capacity_fwd Result (HashMap T) := do - let v := vec_new (List T) + let v := Vec.new (List T) let slots ← HashMap.allocate_slots_fwd T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor @@ -52,12 +52,12 @@ def HashMap.new_fwd (T : Type) : Result (HashMap T) := /- [hashmap::HashMap::{0}::clear] -/ divergent def HashMap.clear_loop_fwd_back (T : Type) (slots : Vec (List T)) (i : Usize) : Result (Vec (List T)) := - let i0 := vec_len (List T) slots + let i0 := Vec.len (List T) slots if i < i0 then do let i1 ← i + (Usize.ofInt 1 (by intlit)) - let slots0 ← vec_index_mut_back (List T) slots i List.Nil + let slots0 ← Vec.index_mut_back (List T) slots i List.Nil HashMap.clear_loop_fwd_back T slots0 i1 else Result.ret slots @@ -121,22 +121,22 @@ def HashMap.insert_no_resize_fwd_back := do let hash ← hash_key_fwd key - let i := vec_len (List T) self.hash_map_slots + let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod let inserted ← HashMap.insert_in_list_fwd T key value l if inserted then do let i0 ← self.hash_map_num_entries + (Usize.ofInt 1 (by intlit)) let l0 ← HashMap.insert_in_list_back T key value l - let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 + let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_num_entries := i0, hash_map_slots := v } else do let l0 ← HashMap.insert_in_list_back T key value l - let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 + let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } /- [core::num::u32::{9}::MAX] -/ @@ -164,16 +164,16 @@ divergent def HashMap.move_elements_loop_fwd_back (T : Type) (ntable : HashMap T) (slots : Vec (List T)) (i : Usize) : Result ((HashMap T) × (Vec (List T))) := - let i0 := vec_len (List T) slots + let i0 := Vec.len (List T) slots if i < i0 then do - let l ← vec_index_mut_fwd (List T) slots i - let ls := mem_replace_fwd (List T) l List.Nil + let l ← Vec.index_mut (List T) slots i + let ls := mem.replace_fwd (List T) l List.Nil let ntable0 ← HashMap.move_elements_from_list_fwd_back T ntable ls let i1 ← i + (Usize.ofInt 1 (by intlit)) - let l0 := mem_replace_back (List T) l List.Nil - let slots0 ← vec_index_mut_back (List T) slots i l0 + let l0 := mem.replace_back (List T) l List.Nil + let slots0 ← Vec.index_mut_back (List T) slots i l0 HashMap.move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) @@ -189,7 +189,7 @@ def HashMap.try_resize_fwd_back (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c - let capacity := vec_len (List T) self.hash_map_slots + let capacity := Vec.len (List T) self.hash_map_slots let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) let (i, i0) := self.hash_map_max_load_factor let i1 ← n1 / i @@ -242,9 +242,9 @@ def HashMap.contains_key_fwd (T : Type) (self : HashMap T) (key : Usize) : Result Bool := do let hash ← hash_key_fwd key - let i := vec_len (List T) self.hash_map_slots + let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_fwd (List T) self.hash_map_slots hash_mod + let l ← Vec.index (List T) self.hash_map_slots hash_mod HashMap.contains_key_in_list_fwd T key l /- [hashmap::HashMap::{0}::get_in_list] -/ @@ -266,9 +266,9 @@ def HashMap.get_in_list_fwd def HashMap.get_fwd (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key_fwd key - let i := vec_len (List T) self.hash_map_slots + let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_fwd (List T) self.hash_map_slots hash_mod + let l ← Vec.index (List T) self.hash_map_slots hash_mod HashMap.get_in_list_fwd T key l /- [hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -309,9 +309,9 @@ def HashMap.get_mut_fwd (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key_fwd key - let i := vec_len (List T) self.hash_map_slots + let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod HashMap.get_mut_in_list_fwd T l key /- [hashmap::HashMap::{0}::get_mut] -/ @@ -321,11 +321,11 @@ def HashMap.get_mut_back := do let hash ← hash_key_fwd key - let i := vec_len (List T) self.hash_map_slots + let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod let l0 ← HashMap.get_mut_in_list_back T l key ret0 - let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 + let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } /- [hashmap::HashMap::{0}::remove_from_list] -/ @@ -335,7 +335,7 @@ divergent def HashMap.remove_from_list_loop_fwd | List.Cons ckey t tl => if ckey = key then - let mv_ls := mem_replace_fwd (List T) (List.Cons ckey t tl) List.Nil + let mv_ls := mem.replace_fwd (List T) (List.Cons ckey t tl) List.Nil match mv_ls with | List.Cons i cvalue tl0 => Result.ret (Option.some cvalue) | List.Nil => Result.fail Error.panic @@ -354,7 +354,7 @@ divergent def HashMap.remove_from_list_loop_back | List.Cons ckey t tl => if ckey = key then - let mv_ls := mem_replace_fwd (List T) (List.Cons ckey t tl) List.Nil + let mv_ls := mem.replace_fwd (List T) (List.Cons ckey t tl) List.Nil match mv_ls with | List.Cons i cvalue tl0 => Result.ret tl0 | List.Nil => Result.fail Error.panic @@ -374,9 +374,9 @@ def HashMap.remove_fwd (T : Type) (self : HashMap T) (key : Usize) : Result (Option T) := do let hash ← hash_key_fwd key - let i := vec_len (List T) self.hash_map_slots + let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod let x ← HashMap.remove_from_list_fwd T key l match x with | Option.none => Result.ret Option.none @@ -390,21 +390,21 @@ def HashMap.remove_back (T : Type) (self : HashMap T) (key : Usize) : Result (HashMap T) := do let hash ← hash_key_fwd key - let i := vec_len (List T) self.hash_map_slots + let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod let x ← HashMap.remove_from_list_fwd T key l match x with | Option.none => do let l0 ← HashMap.remove_from_list_back T key l - let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 + let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } | Option.some x0 => do let i0 ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) let l0 ← HashMap.remove_from_list_back T key l - let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 + let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_num_entries := i0, hash_map_slots := v } -- cgit v1.2.3 From 7c95800cefc87fad894f8bf855cfc047e713b3a7 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jul 2023 12:20:28 +0200 Subject: Improve the generated comments --- tests/lean/Hashmap/Funs.lean | 262 ++++++++++++++++++++++--------------------- 1 file changed, 132 insertions(+), 130 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 48038bfb..34ff1379 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -5,35 +5,35 @@ import Hashmap.Types open Primitives namespace hashmap -/- [hashmap::hash_key] -/ -def hash_key_fwd (k : Usize) : Result Usize := +/- [hashmap::hash_key]: forward function -/ +def hash_key (k : Usize) : Result Usize := Result.ret k -/- [hashmap::HashMap::{0}::allocate_slots] -/ -divergent def HashMap.allocate_slots_loop_fwd +/- [hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function -/ +divergent def HashMap.allocate_slots_loop (T : Type) (slots : Vec (List T)) (n : Usize) : Result (Vec (List T)) := if n > (Usize.ofInt 0 (by intlit)) then do let slots0 ← Vec.push (List T) slots List.Nil let n0 ← n - (Usize.ofInt 1 (by intlit)) - HashMap.allocate_slots_loop_fwd T slots0 n0 + HashMap.allocate_slots_loop T slots0 n0 else Result.ret slots -/- [hashmap::HashMap::{0}::allocate_slots] -/ -def HashMap.allocate_slots_fwd +/- [hashmap::HashMap::{0}::allocate_slots]: forward function -/ +def HashMap.allocate_slots (T : Type) (slots : Vec (List T)) (n : Usize) : Result (Vec (List T)) := - HashMap.allocate_slots_loop_fwd T slots n + HashMap.allocate_slots_loop T slots n -/- [hashmap::HashMap::{0}::new_with_capacity] -/ -def HashMap.new_with_capacity_fwd +/- [hashmap::HashMap::{0}::new_with_capacity]: forward function -/ +def HashMap.new_with_capacity (T : Type) (capacity : Usize) (max_load_dividend : Usize) (max_load_divisor : Usize) : Result (HashMap T) := do let v := Vec.new (List T) - let slots ← HashMap.allocate_slots_fwd T v capacity + let slots ← HashMap.allocate_slots T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor Result.ret @@ -44,13 +44,14 @@ def HashMap.new_with_capacity_fwd hash_map_slots := slots } -/- [hashmap::HashMap::{0}::new] -/ -def HashMap.new_fwd (T : Type) : Result (HashMap T) := - HashMap.new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) +/- [hashmap::HashMap::{0}::new]: forward function -/ +def HashMap.new (T : Type) : Result (HashMap T) := + HashMap.new_with_capacity T (Usize.ofInt 32 (by intlit)) (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) -/- [hashmap::HashMap::{0}::clear] -/ -divergent def HashMap.clear_loop_fwd_back +/- [hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +divergent def HashMap.clear_loop (T : Type) (slots : Vec (List T)) (i : Usize) : Result (Vec (List T)) := let i0 := Vec.len (List T) slots if i < i0 @@ -58,16 +59,15 @@ divergent def HashMap.clear_loop_fwd_back do let i1 ← i + (Usize.ofInt 1 (by intlit)) let slots0 ← Vec.index_mut_back (List T) slots i List.Nil - HashMap.clear_loop_fwd_back T slots0 i1 + HashMap.clear_loop T slots0 i1 else Result.ret slots -/- [hashmap::HashMap::{0}::clear] -/ -def HashMap.clear_fwd_back - (T : Type) (self : HashMap T) : Result (HashMap T) := +/- [hashmap::HashMap::{0}::clear]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do let v ← - HashMap.clear_loop_fwd_back T self.hash_map_slots - (Usize.ofInt 0 (by intlit)) + HashMap.clear_loop T self.hash_map_slots (Usize.ofInt 0 (by intlit)) Result.ret { self @@ -76,26 +76,26 @@ def HashMap.clear_fwd_back hash_map_slots := v } -/- [hashmap::HashMap::{0}::len] -/ -def HashMap.len_fwd (T : Type) (self : HashMap T) : Result Usize := +/- [hashmap::HashMap::{0}::len]: forward function -/ +def HashMap.len (T : Type) (self : HashMap T) : Result Usize := Result.ret self.hash_map_num_entries -/- [hashmap::HashMap::{0}::insert_in_list] -/ -divergent def HashMap.insert_in_list_loop_fwd +/- [hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function -/ +divergent def HashMap.insert_in_list_loop (T : Type) (key : Usize) (value : T) (ls : List T) : Result Bool := match ls with | List.Cons ckey cvalue tl => if ckey = key then Result.ret false - else HashMap.insert_in_list_loop_fwd T key value tl + else HashMap.insert_in_list_loop T key value tl | List.Nil => Result.ret true -/- [hashmap::HashMap::{0}::insert_in_list] -/ -def HashMap.insert_in_list_fwd +/- [hashmap::HashMap::{0}::insert_in_list]: forward function -/ +def HashMap.insert_in_list (T : Type) (key : Usize) (value : T) (ls : List T) : Result Bool := - HashMap.insert_in_list_loop_fwd T key value ls + HashMap.insert_in_list_loop T key value ls -/- [hashmap::HashMap::{0}::insert_in_list] -/ +/- [hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 -/ divergent def HashMap.insert_in_list_loop_back (T : Type) (key : Usize) (value : T) (ls : List T) : Result (List T) := match ls with @@ -109,22 +109,23 @@ divergent def HashMap.insert_in_list_loop_back | List.Nil => let l := List.Nil Result.ret (List.Cons key value l) -/- [hashmap::HashMap::{0}::insert_in_list] -/ +/- [hashmap::HashMap::{0}::insert_in_list]: backward function 0 -/ def HashMap.insert_in_list_back (T : Type) (key : Usize) (value : T) (ls : List T) : Result (List T) := HashMap.insert_in_list_loop_back T key value ls -/- [hashmap::HashMap::{0}::insert_no_resize] -/ -def HashMap.insert_no_resize_fwd_back +/- [hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def HashMap.insert_no_resize (T : Type) (self : HashMap T) (key : Usize) (value : T) : Result (HashMap T) := do - let hash ← hash_key_fwd key + let hash ← hash_key key let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod - let inserted ← HashMap.insert_in_list_fwd T key value l + let inserted ← HashMap.insert_in_list T key value l if inserted then do @@ -144,23 +145,26 @@ def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295 (by intlit)) def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) -/- [hashmap::HashMap::{0}::move_elements_from_list] -/ -divergent def HashMap.move_elements_from_list_loop_fwd_back +/- [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +divergent def HashMap.move_elements_from_list_loop (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) := match ls with | List.Cons k v tl => do - let ntable0 ← HashMap.insert_no_resize_fwd_back T ntable k v - HashMap.move_elements_from_list_loop_fwd_back T ntable0 tl + let ntable0 ← HashMap.insert_no_resize T ntable k v + HashMap.move_elements_from_list_loop T ntable0 tl | List.Nil => Result.ret ntable -/- [hashmap::HashMap::{0}::move_elements_from_list] -/ -def HashMap.move_elements_from_list_fwd_back +/- [hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def HashMap.move_elements_from_list (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) := - HashMap.move_elements_from_list_loop_fwd_back T ntable ls + HashMap.move_elements_from_list_loop T ntable ls -/- [hashmap::HashMap::{0}::move_elements] -/ -divergent def HashMap.move_elements_loop_fwd_back +/- [hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +divergent def HashMap.move_elements_loop (T : Type) (ntable : HashMap T) (slots : Vec (List T)) (i : Usize) : Result ((HashMap T) × (Vec (List T))) := @@ -169,24 +173,25 @@ divergent def HashMap.move_elements_loop_fwd_back then do let l ← Vec.index_mut (List T) slots i - let ls := mem.replace_fwd (List T) l List.Nil - let ntable0 ← HashMap.move_elements_from_list_fwd_back T ntable ls + let ls := mem.replace (List T) l List.Nil + let ntable0 ← HashMap.move_elements_from_list T ntable ls let i1 ← i + (Usize.ofInt 1 (by intlit)) let l0 := mem.replace_back (List T) l List.Nil let slots0 ← Vec.index_mut_back (List T) slots i l0 - HashMap.move_elements_loop_fwd_back T ntable0 slots0 i1 + HashMap.move_elements_loop T ntable0 slots0 i1 else Result.ret (ntable, slots) -/- [hashmap::HashMap::{0}::move_elements] -/ -def HashMap.move_elements_fwd_back +/- [hashmap::HashMap::{0}::move_elements]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def HashMap.move_elements (T : Type) (ntable : HashMap T) (slots : Vec (List T)) (i : Usize) : Result ((HashMap T) × (Vec (List T))) := - HashMap.move_elements_loop_fwd_back T ntable slots i + HashMap.move_elements_loop T ntable slots i -/- [hashmap::HashMap::{0}::try_resize] -/ -def HashMap.try_resize_fwd_back - (T : Type) (self : HashMap T) : Result (HashMap T) := +/- [hashmap::HashMap::{0}::try_resize]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c let capacity := Vec.len (List T) self.hash_map_slots @@ -197,9 +202,9 @@ def HashMap.try_resize_fwd_back then do let i2 ← capacity * (Usize.ofInt 2 (by intlit)) - let ntable ← HashMap.new_with_capacity_fwd T i2 i i0 + let ntable ← HashMap.new_with_capacity T i2 i i0 let (ntable0, _) ← - HashMap.move_elements_fwd_back T ntable self.hash_map_slots + HashMap.move_elements T ntable self.hash_map_slots (Usize.ofInt 0 (by intlit)) Result.ret { @@ -210,83 +215,83 @@ def HashMap.try_resize_fwd_back } else Result.ret { self with hash_map_max_load_factor := (i, i0) } -/- [hashmap::HashMap::{0}::insert] -/ -def HashMap.insert_fwd_back +/- [hashmap::HashMap::{0}::insert]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def HashMap.insert (T : Type) (self : HashMap T) (key : Usize) (value : T) : Result (HashMap T) := do - let self0 ← HashMap.insert_no_resize_fwd_back T self key value - let i ← HashMap.len_fwd T self0 + let self0 ← HashMap.insert_no_resize T self key value + let i ← HashMap.len T self0 if i > self0.hash_map_max_load - then HashMap.try_resize_fwd_back T self0 + then HashMap.try_resize T self0 else Result.ret self0 -/- [hashmap::HashMap::{0}::contains_key_in_list] -/ -divergent def HashMap.contains_key_in_list_loop_fwd +/- [hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function -/ +divergent def HashMap.contains_key_in_list_loop (T : Type) (key : Usize) (ls : List T) : Result Bool := match ls with | List.Cons ckey t tl => if ckey = key then Result.ret true - else HashMap.contains_key_in_list_loop_fwd T key tl + else HashMap.contains_key_in_list_loop T key tl | List.Nil => Result.ret false -/- [hashmap::HashMap::{0}::contains_key_in_list] -/ -def HashMap.contains_key_in_list_fwd +/- [hashmap::HashMap::{0}::contains_key_in_list]: forward function -/ +def HashMap.contains_key_in_list (T : Type) (key : Usize) (ls : List T) : Result Bool := - HashMap.contains_key_in_list_loop_fwd T key ls + HashMap.contains_key_in_list_loop T key ls -/- [hashmap::HashMap::{0}::contains_key] -/ -def HashMap.contains_key_fwd +/- [hashmap::HashMap::{0}::contains_key]: forward function -/ +def HashMap.contains_key (T : Type) (self : HashMap T) (key : Usize) : Result Bool := do - let hash ← hash_key_fwd key + let hash ← hash_key key let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i let l ← Vec.index (List T) self.hash_map_slots hash_mod - HashMap.contains_key_in_list_fwd T key l + HashMap.contains_key_in_list T key l -/- [hashmap::HashMap::{0}::get_in_list] -/ -divergent def HashMap.get_in_list_loop_fwd +/- [hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/ +divergent def HashMap.get_in_list_loop (T : Type) (key : Usize) (ls : List T) : Result T := match ls with | List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue - else HashMap.get_in_list_loop_fwd T key tl + else HashMap.get_in_list_loop T key tl | List.Nil => Result.fail Error.panic -/- [hashmap::HashMap::{0}::get_in_list] -/ -def HashMap.get_in_list_fwd - (T : Type) (key : Usize) (ls : List T) : Result T := - HashMap.get_in_list_loop_fwd T key ls +/- [hashmap::HashMap::{0}::get_in_list]: forward function -/ +def HashMap.get_in_list (T : Type) (key : Usize) (ls : List T) : Result T := + HashMap.get_in_list_loop T key ls -/- [hashmap::HashMap::{0}::get] -/ -def HashMap.get_fwd (T : Type) (self : HashMap T) (key : Usize) : Result T := +/- [hashmap::HashMap::{0}::get]: forward function -/ +def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T := do - let hash ← hash_key_fwd key + let hash ← hash_key key let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i let l ← Vec.index (List T) self.hash_map_slots hash_mod - HashMap.get_in_list_fwd T key l + HashMap.get_in_list T key l -/- [hashmap::HashMap::{0}::get_mut_in_list] -/ -divergent def HashMap.get_mut_in_list_loop_fwd +/- [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/ +divergent def HashMap.get_mut_in_list_loop (T : Type) (ls : List T) (key : Usize) : Result T := match ls with | List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue - else HashMap.get_mut_in_list_loop_fwd T tl key + else HashMap.get_mut_in_list_loop T tl key | List.Nil => Result.fail Error.panic -/- [hashmap::HashMap::{0}::get_mut_in_list] -/ -def HashMap.get_mut_in_list_fwd +/- [hashmap::HashMap::{0}::get_mut_in_list]: forward function -/ +def HashMap.get_mut_in_list (T : Type) (ls : List T) (key : Usize) : Result T := - HashMap.get_mut_in_list_loop_fwd T ls key + HashMap.get_mut_in_list_loop T ls key -/- [hashmap::HashMap::{0}::get_mut_in_list] -/ +/- [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 -/ divergent def HashMap.get_mut_in_list_loop_back (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) := match ls with @@ -299,28 +304,27 @@ divergent def HashMap.get_mut_in_list_loop_back Result.ret (List.Cons ckey cvalue tl0) | List.Nil => Result.fail Error.panic -/- [hashmap::HashMap::{0}::get_mut_in_list] -/ +/- [hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 -/ def HashMap.get_mut_in_list_back (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) := HashMap.get_mut_in_list_loop_back T ls key ret0 -/- [hashmap::HashMap::{0}::get_mut] -/ -def HashMap.get_mut_fwd - (T : Type) (self : HashMap T) (key : Usize) : Result T := +/- [hashmap::HashMap::{0}::get_mut]: forward function -/ +def HashMap.get_mut (T : Type) (self : HashMap T) (key : Usize) : Result T := do - let hash ← hash_key_fwd key + let hash ← hash_key key let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod - HashMap.get_mut_in_list_fwd T l key + HashMap.get_mut_in_list T l key -/- [hashmap::HashMap::{0}::get_mut] -/ +/- [hashmap::HashMap::{0}::get_mut]: backward function 0 -/ def HashMap.get_mut_back (T : Type) (self : HashMap T) (key : Usize) (ret0 : T) : Result (HashMap T) := do - let hash ← hash_key_fwd key + let hash ← hash_key key let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod @@ -328,33 +332,33 @@ def HashMap.get_mut_back let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } -/- [hashmap::HashMap::{0}::remove_from_list] -/ -divergent def HashMap.remove_from_list_loop_fwd +/- [hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function -/ +divergent def HashMap.remove_from_list_loop (T : Type) (key : Usize) (ls : List T) : Result (Option T) := match ls with | List.Cons ckey t tl => if ckey = key then - let mv_ls := mem.replace_fwd (List T) (List.Cons ckey t tl) List.Nil + let mv_ls := mem.replace (List T) (List.Cons ckey t tl) List.Nil match mv_ls with | List.Cons i cvalue tl0 => Result.ret (Option.some cvalue) | List.Nil => Result.fail Error.panic - else HashMap.remove_from_list_loop_fwd T key tl + else HashMap.remove_from_list_loop T key tl | List.Nil => Result.ret Option.none -/- [hashmap::HashMap::{0}::remove_from_list] -/ -def HashMap.remove_from_list_fwd +/- [hashmap::HashMap::{0}::remove_from_list]: forward function -/ +def HashMap.remove_from_list (T : Type) (key : Usize) (ls : List T) : Result (Option T) := - HashMap.remove_from_list_loop_fwd T key ls + HashMap.remove_from_list_loop T key ls -/- [hashmap::HashMap::{0}::remove_from_list] -/ +/- [hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 -/ divergent def HashMap.remove_from_list_loop_back (T : Type) (key : Usize) (ls : List T) : Result (List T) := match ls with | List.Cons ckey t tl => if ckey = key then - let mv_ls := mem.replace_fwd (List T) (List.Cons ckey t tl) List.Nil + let mv_ls := mem.replace (List T) (List.Cons ckey t tl) List.Nil match mv_ls with | List.Cons i cvalue tl0 => Result.ret tl0 | List.Nil => Result.fail Error.panic @@ -364,20 +368,20 @@ divergent def HashMap.remove_from_list_loop_back Result.ret (List.Cons ckey t tl0) | List.Nil => Result.ret List.Nil -/- [hashmap::HashMap::{0}::remove_from_list] -/ +/- [hashmap::HashMap::{0}::remove_from_list]: backward function 1 -/ def HashMap.remove_from_list_back (T : Type) (key : Usize) (ls : List T) : Result (List T) := HashMap.remove_from_list_loop_back T key ls -/- [hashmap::HashMap::{0}::remove] -/ -def HashMap.remove_fwd +/- [hashmap::HashMap::{0}::remove]: forward function -/ +def HashMap.remove (T : Type) (self : HashMap T) (key : Usize) : Result (Option T) := do - let hash ← hash_key_fwd key + let hash ← hash_key key let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod - let x ← HashMap.remove_from_list_fwd T key l + let x ← HashMap.remove_from_list T key l match x with | Option.none => Result.ret Option.none | Option.some x0 => @@ -385,15 +389,15 @@ def HashMap.remove_fwd let _ ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) Result.ret (Option.some x0) -/- [hashmap::HashMap::{0}::remove] -/ +/- [hashmap::HashMap::{0}::remove]: backward function 0 -/ def HashMap.remove_back (T : Type) (self : HashMap T) (key : Usize) : Result (HashMap T) := do - let hash ← hash_key_fwd key + let hash ← hash_key key let i := Vec.len (List T) self.hash_map_slots let hash_mod ← hash % i let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod - let x ← HashMap.remove_from_list_fwd T key l + let x ← HashMap.remove_from_list T key l match x with | Option.none => do @@ -408,23 +412,23 @@ def HashMap.remove_back Result.ret { self with hash_map_num_entries := i0, hash_map_slots := v } -/- [hashmap::test1] -/ -def test1_fwd : Result Unit := +/- [hashmap::test1]: forward function -/ +def test1 : Result Unit := do - let hm ← HashMap.new_fwd U64 + let hm ← HashMap.new U64 let hm0 ← - HashMap.insert_fwd_back U64 hm (Usize.ofInt 0 (by intlit)) + HashMap.insert U64 hm (Usize.ofInt 0 (by intlit)) (U64.ofInt 42 (by intlit)) let hm1 ← - HashMap.insert_fwd_back U64 hm0 (Usize.ofInt 128 (by intlit)) + HashMap.insert U64 hm0 (Usize.ofInt 128 (by intlit)) (U64.ofInt 18 (by intlit)) let hm2 ← - HashMap.insert_fwd_back U64 hm1 (Usize.ofInt 1024 (by intlit)) + HashMap.insert U64 hm1 (Usize.ofInt 1024 (by intlit)) (U64.ofInt 138 (by intlit)) let hm3 ← - HashMap.insert_fwd_back U64 hm2 (Usize.ofInt 1056 (by intlit)) + HashMap.insert U64 hm2 (Usize.ofInt 1056 (by intlit)) (U64.ofInt 256 (by intlit)) - let i ← HashMap.get_fwd U64 hm3 (Usize.ofInt 128 (by intlit)) + let i ← HashMap.get U64 hm3 (Usize.ofInt 128 (by intlit)) if not (i = (U64.ofInt 18 (by intlit))) then Result.fail Error.panic else @@ -432,12 +436,12 @@ def test1_fwd : Result Unit := let hm4 ← HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit)) (U64.ofInt 56 (by intlit)) - let i0 ← HashMap.get_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) + let i0 ← HashMap.get U64 hm4 (Usize.ofInt 1024 (by intlit)) if not (i0 = (U64.ofInt 56 (by intlit))) then Result.fail Error.panic else do - let x ← HashMap.remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) + let x ← HashMap.remove U64 hm4 (Usize.ofInt 1024 (by intlit)) match x with | Option.none => Result.fail Error.panic | Option.some x0 => @@ -447,26 +451,24 @@ def test1_fwd : Result Unit := do let hm5 ← HashMap.remove_back U64 hm4 (Usize.ofInt 1024 (by intlit)) - let i1 ← - HashMap.get_fwd U64 hm5 (Usize.ofInt 0 (by intlit)) + let i1 ← HashMap.get U64 hm5 (Usize.ofInt 0 (by intlit)) if not (i1 = (U64.ofInt 42 (by intlit))) then Result.fail Error.panic else do let i2 ← - HashMap.get_fwd U64 hm5 (Usize.ofInt 128 (by intlit)) + HashMap.get U64 hm5 (Usize.ofInt 128 (by intlit)) if not (i2 = (U64.ofInt 18 (by intlit))) then Result.fail Error.panic else do let i3 ← - HashMap.get_fwd U64 hm5 - (Usize.ofInt 1056 (by intlit)) + HashMap.get U64 hm5 (Usize.ofInt 1056 (by intlit)) if not (i3 = (U64.ofInt 256 (by intlit))) then Result.fail Error.panic else Result.ret () /- Unit test for [hashmap::test1] -/ -#assert (test1_fwd == .ret ()) +#assert (test1 == .ret ()) end hashmap -- cgit v1.2.3 From 36c3348bacf7127d3736f9aac16a430a30424020 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jul 2023 13:46:26 +0200 Subject: Use short names for the structure fields in Lean --- tests/lean/Hashmap/Funs.lean | 90 +++++++++++++++++++------------------------ tests/lean/Hashmap/Types.lean | 8 ++-- 2 files changed, 44 insertions(+), 54 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 34ff1379..5e11ffdd 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -38,10 +38,10 @@ def HashMap.new_with_capacity let i0 ← i / max_load_divisor Result.ret { - hash_map_num_entries := (Usize.ofInt 0 (by intlit)), - hash_map_max_load_factor := (max_load_dividend, max_load_divisor), - hash_map_max_load := i0, - hash_map_slots := slots + num_entries := (Usize.ofInt 0 (by intlit)), + max_load_factor := (max_load_dividend, max_load_divisor), + max_load := i0, + slots := slots } /- [hashmap::HashMap::{0}::new]: forward function -/ @@ -66,19 +66,13 @@ divergent def HashMap.clear_loop (there is a single backward function, and the forward function returns ()) -/ def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do - let v ← - HashMap.clear_loop T self.hash_map_slots (Usize.ofInt 0 (by intlit)) + let v ← HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit)) Result.ret - { - self - with - hash_map_num_entries := (Usize.ofInt 0 (by intlit)), - hash_map_slots := v - } + { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v } /- [hashmap::HashMap::{0}::len]: forward function -/ def HashMap.len (T : Type) (self : HashMap T) : Result Usize := - Result.ret self.hash_map_num_entries + Result.ret self.num_entries /- [hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function -/ divergent def HashMap.insert_in_list_loop @@ -122,23 +116,22 @@ def HashMap.insert_no_resize := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.slots hash_mod let inserted ← HashMap.insert_in_list T key value l if inserted then do - let i0 ← self.hash_map_num_entries + (Usize.ofInt 1 (by intlit)) + let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit)) let l0 ← HashMap.insert_in_list_back T key value l - let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 - Result.ret - { self with hash_map_num_entries := i0, hash_map_slots := v } + let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 + Result.ret { self with num_entries := i0, slots := v } else do let l0 ← HashMap.insert_in_list_back T key value l - let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 - Result.ret { self with hash_map_slots := v } + let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 + Result.ret { self with slots := v } /- [core::num::u32::{9}::MAX] -/ def core_num_u32_max_body : Result U32 := @@ -194,9 +187,9 @@ def HashMap.move_elements def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c - let capacity := Vec.len (List T) self.hash_map_slots + let capacity := Vec.len (List T) self.slots let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) - let (i, i0) := self.hash_map_max_load_factor + let (i, i0) := self.max_load_factor let i1 ← n1 / i if capacity <= i1 then @@ -204,16 +197,14 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := let i2 ← capacity * (Usize.ofInt 2 (by intlit)) let ntable ← HashMap.new_with_capacity T i2 i i0 let (ntable0, _) ← - HashMap.move_elements T ntable self.hash_map_slots - (Usize.ofInt 0 (by intlit)) + HashMap.move_elements T ntable self.slots (Usize.ofInt 0 (by intlit)) Result.ret { ntable0 with - hash_map_num_entries := self.hash_map_num_entries, - hash_map_max_load_factor := (i, i0) + num_entries := self.num_entries, max_load_factor := (i, i0) } - else Result.ret { self with hash_map_max_load_factor := (i, i0) } + else Result.ret { self with max_load_factor := (i, i0) } /- [hashmap::HashMap::{0}::insert]: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ @@ -224,7 +215,7 @@ def HashMap.insert do let self0 ← HashMap.insert_no_resize T self key value let i ← HashMap.len T self0 - if i > self0.hash_map_max_load + if i > self0.max_load then HashMap.try_resize T self0 else Result.ret self0 @@ -248,9 +239,9 @@ def HashMap.contains_key (T : Type) (self : HashMap T) (key : Usize) : Result Bool := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index (List T) self.hash_map_slots hash_mod + let l ← Vec.index (List T) self.slots hash_mod HashMap.contains_key_in_list T key l /- [hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/ @@ -271,9 +262,9 @@ def HashMap.get_in_list (T : Type) (key : Usize) (ls : List T) : Result T := def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index (List T) self.hash_map_slots hash_mod + let l ← Vec.index (List T) self.slots hash_mod HashMap.get_in_list T key l /- [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/ @@ -313,9 +304,9 @@ def HashMap.get_mut_in_list_back def HashMap.get_mut (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.slots hash_mod HashMap.get_mut_in_list T l key /- [hashmap::HashMap::{0}::get_mut]: backward function 0 -/ @@ -325,12 +316,12 @@ def HashMap.get_mut_back := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.slots hash_mod let l0 ← HashMap.get_mut_in_list_back T l key ret0 - let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 - Result.ret { self with hash_map_slots := v } + let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 + Result.ret { self with slots := v } /- [hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function -/ divergent def HashMap.remove_from_list_loop @@ -378,15 +369,15 @@ def HashMap.remove (T : Type) (self : HashMap T) (key : Usize) : Result (Option T) := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.slots hash_mod let x ← HashMap.remove_from_list T key l match x with | Option.none => Result.ret Option.none | Option.some x0 => do - let _ ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) + let _ ← self.num_entries - (Usize.ofInt 1 (by intlit)) Result.ret (Option.some x0) /- [hashmap::HashMap::{0}::remove]: backward function 0 -/ @@ -394,23 +385,22 @@ def HashMap.remove_back (T : Type) (self : HashMap T) (key : Usize) : Result (HashMap T) := do let hash ← hash_key key - let i := Vec.len (List T) self.hash_map_slots + let i := Vec.len (List T) self.slots let hash_mod ← hash % i - let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod + let l ← Vec.index_mut (List T) self.slots hash_mod let x ← HashMap.remove_from_list T key l match x with | Option.none => do let l0 ← HashMap.remove_from_list_back T key l - let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 - Result.ret { self with hash_map_slots := v } + let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 + Result.ret { self with slots := v } | Option.some x0 => do - let i0 ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) + let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit)) let l0 ← HashMap.remove_from_list_back T key l - let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0 - Result.ret - { self with hash_map_num_entries := i0, hash_map_slots := v } + let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 + Result.ret { self with num_entries := i0, slots := v } /- [hashmap::test1]: forward function -/ def test1 : Result Unit := diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean index 7530f3b9..6606cf9e 100644 --- a/tests/lean/Hashmap/Types.lean +++ b/tests/lean/Hashmap/Types.lean @@ -11,9 +11,9 @@ inductive List (T : Type) := /- [hashmap::HashMap] -/ structure HashMap (T : Type) where - hash_map_num_entries : Usize - hash_map_max_load_factor : (Usize × Usize) - hash_map_max_load : Usize - hash_map_slots : Vec (List T) + num_entries : Usize + max_load_factor : (Usize × Usize) + max_load : Usize + slots : Vec (List T) end hashmap -- cgit v1.2.3 From e010c10fb9a1e2d88b52a4f6b4a0865448276013 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 12 Jul 2023 15:58:38 +0200 Subject: Make the `by inlit` implicit --- tests/lean/Hashmap/Funs.lean | 81 ++++++++++++++++++-------------------------- 1 file changed, 33 insertions(+), 48 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 5e11ffdd..870693b5 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -12,11 +12,11 @@ def hash_key (k : Usize) : Result Usize := /- [hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function -/ divergent def HashMap.allocate_slots_loop (T : Type) (slots : Vec (List T)) (n : Usize) : Result (Vec (List T)) := - if n > (Usize.ofInt 0 (by intlit)) + if n > (Usize.ofInt 0) then do let slots0 ← Vec.push (List T) slots List.Nil - let n0 ← n - (Usize.ofInt 1 (by intlit)) + let n0 ← n - (Usize.ofInt 1) HashMap.allocate_slots_loop T slots0 n0 else Result.ret slots @@ -38,7 +38,7 @@ def HashMap.new_with_capacity let i0 ← i / max_load_divisor Result.ret { - num_entries := (Usize.ofInt 0 (by intlit)), + num_entries := (Usize.ofInt 0), max_load_factor := (max_load_dividend, max_load_divisor), max_load := i0, slots := slots @@ -46,8 +46,7 @@ def HashMap.new_with_capacity /- [hashmap::HashMap::{0}::new]: forward function -/ def HashMap.new (T : Type) : Result (HashMap T) := - HashMap.new_with_capacity T (Usize.ofInt 32 (by intlit)) - (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) + HashMap.new_with_capacity T (Usize.ofInt 32) (Usize.ofInt 4) (Usize.ofInt 5) /- [hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ @@ -57,7 +56,7 @@ divergent def HashMap.clear_loop if i < i0 then do - let i1 ← i + (Usize.ofInt 1 (by intlit)) + let i1 ← i + (Usize.ofInt 1) let slots0 ← Vec.index_mut_back (List T) slots i List.Nil HashMap.clear_loop T slots0 i1 else Result.ret slots @@ -66,9 +65,8 @@ divergent def HashMap.clear_loop (there is a single backward function, and the forward function returns ()) -/ def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do - let v ← HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit)) - Result.ret - { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v } + let v ← HashMap.clear_loop T self.slots (Usize.ofInt 0) + Result.ret { self with num_entries := (Usize.ofInt 0), slots := v } /- [hashmap::HashMap::{0}::len]: forward function -/ def HashMap.len (T : Type) (self : HashMap T) : Result Usize := @@ -123,7 +121,7 @@ def HashMap.insert_no_resize if inserted then do - let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit)) + let i0 ← self.num_entries + (Usize.ofInt 1) let l0 ← HashMap.insert_in_list_back T key value l let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 Result.ret { self with num_entries := i0, slots := v } @@ -134,8 +132,7 @@ def HashMap.insert_no_resize Result.ret { self with slots := v } /- [core::num::u32::{9}::MAX] -/ -def core_num_u32_max_body : Result U32 := - Result.ret (U32.ofInt 4294967295 (by intlit)) +def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295) def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) /- [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function @@ -168,7 +165,7 @@ divergent def HashMap.move_elements_loop let l ← Vec.index_mut (List T) slots i let ls := mem.replace (List T) l List.Nil let ntable0 ← HashMap.move_elements_from_list T ntable ls - let i1 ← i + (Usize.ofInt 1 (by intlit)) + let i1 ← i + (Usize.ofInt 1) let l0 := mem.replace_back (List T) l List.Nil let slots0 ← Vec.index_mut_back (List T) slots i l0 HashMap.move_elements_loop T ntable0 slots0 i1 @@ -188,16 +185,16 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c let capacity := Vec.len (List T) self.slots - let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) + let n1 ← max_usize / (Usize.ofInt 2) let (i, i0) := self.max_load_factor let i1 ← n1 / i if capacity <= i1 then do - let i2 ← capacity * (Usize.ofInt 2 (by intlit)) + let i2 ← capacity * (Usize.ofInt 2) let ntable ← HashMap.new_with_capacity T i2 i i0 let (ntable0, _) ← - HashMap.move_elements T ntable self.slots (Usize.ofInt 0 (by intlit)) + HashMap.move_elements T ntable self.slots (Usize.ofInt 0) Result.ret { ntable0 @@ -377,7 +374,7 @@ def HashMap.remove | Option.none => Result.ret Option.none | Option.some x0 => do - let _ ← self.num_entries - (Usize.ofInt 1 (by intlit)) + let _ ← self.num_entries - (Usize.ofInt 1) Result.ret (Option.some x0) /- [hashmap::HashMap::{0}::remove]: backward function 0 -/ @@ -397,7 +394,7 @@ def HashMap.remove_back Result.ret { self with slots := v } | Option.some x0 => do - let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit)) + let i0 ← self.num_entries - (Usize.ofInt 1) let l0 ← HashMap.remove_from_list_back T key l let v ← Vec.index_mut_back (List T) self.slots hash_mod l0 Result.ret { self with num_entries := i0, slots := v } @@ -406,55 +403,43 @@ def HashMap.remove_back def test1 : Result Unit := do let hm ← HashMap.new U64 - let hm0 ← - HashMap.insert U64 hm (Usize.ofInt 0 (by intlit)) - (U64.ofInt 42 (by intlit)) - let hm1 ← - HashMap.insert U64 hm0 (Usize.ofInt 128 (by intlit)) - (U64.ofInt 18 (by intlit)) - let hm2 ← - HashMap.insert U64 hm1 (Usize.ofInt 1024 (by intlit)) - (U64.ofInt 138 (by intlit)) - let hm3 ← - HashMap.insert U64 hm2 (Usize.ofInt 1056 (by intlit)) - (U64.ofInt 256 (by intlit)) - let i ← HashMap.get U64 hm3 (Usize.ofInt 128 (by intlit)) - if not (i = (U64.ofInt 18 (by intlit))) + let hm0 ← HashMap.insert U64 hm (Usize.ofInt 0) (U64.ofInt 42) + let hm1 ← HashMap.insert U64 hm0 (Usize.ofInt 128) (U64.ofInt 18) + let hm2 ← HashMap.insert U64 hm1 (Usize.ofInt 1024) (U64.ofInt 138) + let hm3 ← HashMap.insert U64 hm2 (Usize.ofInt 1056) (U64.ofInt 256) + let i ← HashMap.get U64 hm3 (Usize.ofInt 128) + if not (i = (U64.ofInt 18)) then Result.fail Error.panic else do let hm4 ← - HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit)) - (U64.ofInt 56 (by intlit)) - let i0 ← HashMap.get U64 hm4 (Usize.ofInt 1024 (by intlit)) - if not (i0 = (U64.ofInt 56 (by intlit))) + HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024) (U64.ofInt 56) + let i0 ← HashMap.get U64 hm4 (Usize.ofInt 1024) + if not (i0 = (U64.ofInt 56)) then Result.fail Error.panic else do - let x ← HashMap.remove U64 hm4 (Usize.ofInt 1024 (by intlit)) + let x ← HashMap.remove U64 hm4 (Usize.ofInt 1024) match x with | Option.none => Result.fail Error.panic | Option.some x0 => - if not (x0 = (U64.ofInt 56 (by intlit))) + if not (x0 = (U64.ofInt 56)) then Result.fail Error.panic else do - let hm5 ← - HashMap.remove_back U64 hm4 (Usize.ofInt 1024 (by intlit)) - let i1 ← HashMap.get U64 hm5 (Usize.ofInt 0 (by intlit)) - if not (i1 = (U64.ofInt 42 (by intlit))) + let hm5 ← HashMap.remove_back U64 hm4 (Usize.ofInt 1024) + let i1 ← HashMap.get U64 hm5 (Usize.ofInt 0) + if not (i1 = (U64.ofInt 42)) then Result.fail Error.panic else do - let i2 ← - HashMap.get U64 hm5 (Usize.ofInt 128 (by intlit)) - if not (i2 = (U64.ofInt 18 (by intlit))) + let i2 ← HashMap.get U64 hm5 (Usize.ofInt 128) + if not (i2 = (U64.ofInt 18)) then Result.fail Error.panic else do - let i3 ← - HashMap.get U64 hm5 (Usize.ofInt 1056 (by intlit)) - if not (i3 = (U64.ofInt 256 (by intlit))) + let i3 ← HashMap.get U64 hm5 (Usize.ofInt 1056) + if not (i3 = (U64.ofInt 256)) then Result.fail Error.panic else Result.ret () -- cgit v1.2.3 From 510e409b551f876a28f93f869e108f3f9e761212 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 17 Jul 2023 16:09:33 +0200 Subject: With @sonmarcho, some Lean proofs for hashmaps + comments about possible improvements --- tests/lean/Hashmap/Properties.lean | 195 +++++++++++++++++++++++++++++++++++++ 1 file changed, 195 insertions(+) create mode 100644 tests/lean/Hashmap/Properties.lean (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean new file mode 100644 index 00000000..ca1f29c4 --- /dev/null +++ b/tests/lean/Hashmap/Properties.lean @@ -0,0 +1,195 @@ +import Hashmap.Funs + +open Primitives +open Result + + +namespace List + +theorem index_ne + {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (j: ℤ) (x: α) : + 0 ≤ i → i < l.len → 0 ≤ j → j < l.len → j ≠ i → + (l.update i x).index j = l.index j + := + λ _ _ _ _ _ => match l with + | [] => by simp at * + | hd :: tl => + if h: i = 0 then + have : j ≠ 0 := by scalar_tac + by simp [*] + else if h : j = 0 then + have : i ≠ 0 := by scalar_tac + by simp [*] + else + by + simp [*] + simp at * + apply index_ne <;> scalar_tac + +theorem index_eq + {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (x: α) : + 0 ≤ i → i < l.len → + (l.update i x).index i = x + := + fun _ _ => match l with + | [] => by simp at *; exfalso; scalar_tac -- TODO: exfalso needed. Son FIXME + | hd :: tl => + if h: i = 0 then + by + simp [*] + else + by + simp [*] + simp at * + apply index_eq <;> scalar_tac + +end List + + +namespace Primitives + +@[pspec] +theorem Vec.index_mut_spec + {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) (h: i.val < v.val.len) : + ∃ x, + v.index_mut α i = ret x ∧ x = v.val.index i.val + := by sorry + +@[pspec] +theorem Vec.index_mut_back_spec + {α : Type u} (v: Vec α) (i: Usize) (x:α) : + i.val < v.val.len → ∃ nv, + v.index_mut_back α i x = ret nv ∧ nv.val = v.val.update i.val x + := by sorry + +end Primitives + +namespace List + +def allP {α : Type u} (l : List α) (p: α → Prop) : Prop := + foldr (fun a r => p a ∧ r) True l + +@[simp] +theorem allP_nil {α : Type u} (p: α → Prop) : allP [] p := + by simp [allP, foldr] + +@[simp] +theorem allP_cons {α : Type u} (hd: α) (tl : List α) (p: α → Prop) : + allP (hd :: tl) p ↔ p hd ∧ allP tl p + := by simp [allP, foldr] + + +def pairwise_rel + {α : Type u} (rel : α → α → Prop) (l: List α) : Prop + := match l with + | [] => True + | hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl + +@[simp] +theorem pairwise_rel_nil {α : Type u} (rel : α → α → Prop) : + pairwise_rel rel [] + := by simp [pairwise_rel] + +@[simp] +theorem pairwise_rel_cons {α : Type u} (rel : α → α → Prop) (hd: α) (tl: List α) : + pairwise_rel rel (hd :: tl) ↔ allP tl (rel hd) ∧ pairwise_rel rel tl + := by simp [pairwise_rel] + +end List + +namespace hashmap + +namespace List + +def v {α : Type} (ls: List α) : _root_.List (Usize × α) := + match ls with + | Nil => [] + | Cons k x tl => (k, x) :: v tl + +def lookup {α : Type} (ls: _root_.List (Usize × α)) (key: Usize) : Option α := + match ls with + | [] => none + | (k, x) :: tl => if k = key then some x else lookup tl key + +end List + +namespace HashMap + +@[pspec] +theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : + ∃ b, + insert_in_list α key value ls = ret b ∧ + (b ↔ List.lookup ls.v key = none) + := match ls with + | .Nil => by simp [insert_in_list, insert_in_list_loop, List.lookup] + | .Cons k v tl => + if h: k = key then -- TODO: The order of k/key matters + by + simp [insert_in_list, List.lookup] + rw [insert_in_list_loop] + simp [h] + else + by + have ⟨ b, hi ⟩ := insert_in_list_spec key value tl + exists b + simp [insert_in_list, List.lookup] + rw [insert_in_list_loop] -- TODO: Using it in simp leads to infinite recursion + simp [h] + simp [insert_in_list] at hi + exact hi + +/-- +@[pspec] +theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) : + ∃ b, + insert_in_list α key value ls = ret b ∧ + (b = (List.lookup ls.v key = none)) + := by + induction ls + case Nil => simp [insert_in_list, insert_in_list_loop, List.lookup] + case Cons k v tl ih => + simp only [insert_in_list, List.lookup] + rw [insert_in_list_loop] + simp only + if h: k = key then + simp [h] + else + conv => + rhs; ext; arg 1; simp [h] -- TODO: Simplify + simp [insert_in_list] at ih; + progress -- TODO: Does not work +--/ + +@[pspec] +theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List α) : + ∃ l1, + insert_in_list_back α key value l0 = ret l1 ∧ + List.lookup l1.v key = value ∧ + (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k) + := match l0 with + | .Nil => by simp [insert_in_list_back, insert_in_list_loop_back, List.lookup]; tauto + | .Cons k v tl => + if h: k = key then + by + simp [insert_in_list_back, List.lookup] + rw [insert_in_list_loop_back] + simp [h, List.lookup] + intro k1 h1 + have h2 : ¬(key = k1) := by tauto -- TODO: Why is the order of args in eq swapped + simp [h2] + else + by + simp [insert_in_list_back, List.lookup] + rw [insert_in_list_loop_back] + simp [h, List.lookup] + have ⟨tl0 , _, _ ⟩ := insert_in_list_back_spec key value tl -- TODO: Use progress + simp [insert_in_list_back] at * + simp [*] + have : ¬ (key = k) := by tauto + simp [List.lookup, *] + simp (config := {contextual := true}) [*] + +end HashMap +-- def distinct_keys {α : Type u} + +end hashmap -- cgit v1.2.3 From aaa2fdfd104f7010ebaf2977a22280716ac15d13 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 17 Jul 2023 23:42:25 +0200 Subject: Make minor modifications --- tests/lean/Hashmap/Properties.lean | 25 ------------------------- 1 file changed, 25 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index ca1f29c4..1db39422 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -3,7 +3,6 @@ import Hashmap.Funs open Primitives open Result - namespace List theorem index_ne @@ -43,29 +42,6 @@ theorem index_eq simp at * apply index_eq <;> scalar_tac -end List - - -namespace Primitives - -@[pspec] -theorem Vec.index_mut_spec - {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) (h: i.val < v.val.len) : - ∃ x, - v.index_mut α i = ret x ∧ x = v.val.index i.val - := by sorry - -@[pspec] -theorem Vec.index_mut_back_spec - {α : Type u} (v: Vec α) (i: Usize) (x:α) : - i.val < v.val.len → ∃ nv, - v.index_mut_back α i x = ret nv ∧ nv.val = v.val.update i.val x - := by sorry - -end Primitives - -namespace List - def allP {α : Type u} (l : List α) (p: α → Prop) : Prop := foldr (fun a r => p a ∧ r) True l @@ -78,7 +54,6 @@ theorem allP_cons {α : Type u} (hd: α) (tl : List α) (p: α → Prop) : allP (hd :: tl) p ↔ p hd ∧ allP tl p := by simp [allP, foldr] - def pairwise_rel {α : Type u} (rel : α → α → Prop) (l: List α) : Prop := match l with -- cgit v1.2.3 From e07177ee2de3fd1346ab6b1fc09aefbcb0e24459 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 18 Jul 2023 12:22:59 +0200 Subject: Improve progress --- tests/lean/Hashmap/Properties.lean | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 1db39422..ee22bebd 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -105,6 +105,8 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : simp [h] else by + -- TODO: use progress: detect that this is a recursive call, or give + -- the possibility of specifying an identifier have ⟨ b, hi ⟩ := insert_in_list_spec key value tl exists b simp [insert_in_list, List.lookup] @@ -112,13 +114,12 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : simp [h] simp [insert_in_list] at hi exact hi - -/-- + @[pspec] theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ - (b = (List.lookup ls.v key = none)) + (b ↔ (List.lookup ls.v key = none)) := by induction ls case Nil => simp [insert_in_list, insert_in_list_loop, List.lookup] @@ -130,11 +131,12 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) simp [h] else conv => - rhs; ext; arg 1; simp [h] -- TODO: Simplify - simp [insert_in_list] at ih; - progress -- TODO: Does not work ---/ - + rhs; ext; left; simp [h] -- TODO: Simplify + simp only [insert_in_list] at ih; + -- TODO: give the possibility of using underscores + progress as ⟨ b h ⟩ + simp [*] + @[pspec] theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List α) : ∃ l1, @@ -150,8 +152,7 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List rw [insert_in_list_loop_back] simp [h, List.lookup] intro k1 h1 - have h2 : ¬(key = k1) := by tauto -- TODO: Why is the order of args in eq swapped - simp [h2] + simp [*] else by simp [insert_in_list_back, List.lookup] @@ -159,12 +160,9 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List simp [h, List.lookup] have ⟨tl0 , _, _ ⟩ := insert_in_list_back_spec key value tl -- TODO: Use progress simp [insert_in_list_back] at * - simp [*] - have : ¬ (key = k) := by tauto simp [List.lookup, *] simp (config := {contextual := true}) [*] end HashMap --- def distinct_keys {α : Type u} end hashmap -- cgit v1.2.3 From 204742bf2449c88abaea8ebd284c55d98b43488a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 19 Jul 2023 14:48:08 +0200 Subject: Improve progress --- tests/lean/Hashmap/Properties.lean | 34 ++++++++++++++++++++++++++++++++-- 1 file changed, 32 insertions(+), 2 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index ee22bebd..3b9b960f 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -115,6 +115,37 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : simp [insert_in_list] at hi exact hi +set_option trace.Progress true +@[pspec] +theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) : + ∃ b, + insert_in_list α key value ls = ret b ∧ + (b ↔ List.lookup ls.v key = none) + := match ls with + | .Nil => by simp [insert_in_list, insert_in_list_loop, List.lookup] + | .Cons k v tl => + if h: k = key then -- TODO: The order of k/key matters + by + simp [insert_in_list, List.lookup] + rw [insert_in_list_loop] + simp [h] + else + by + simp only [insert_in_list] + rw [insert_in_list_loop] + conv => rhs; ext; simp [*] + progress as ⟨ b hi ⟩ + + -- TODO: use progress: detect that this is a recursive call, or give + -- the possibility of specifying an identifier + have ⟨ b, hi ⟩ := insert_in_list_spec key value tl + exists b + simp [insert_in_list, List.lookup] + rw [insert_in_list_loop] -- TODO: Using it in simp leads to infinite recursion + simp [h] + simp [insert_in_list] at hi + exact hi + @[pspec] theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, @@ -130,8 +161,7 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) if h: k = key then simp [h] else - conv => - rhs; ext; left; simp [h] -- TODO: Simplify + conv => rhs; ext; left; simp [h] -- TODO: Simplify simp only [insert_in_list] at ih; -- TODO: give the possibility of using underscores progress as ⟨ b h ⟩ -- cgit v1.2.3 From 6ef1d360b89fd9f9383e63609888bf925a6a16ab Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 20 Jul 2023 12:08:09 +0200 Subject: Improve progress further and move some lemmas --- tests/lean/Hashmap/Properties.lean | 92 ++++---------------------------------- 1 file changed, 8 insertions(+), 84 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 3b9b960f..baa8f5c8 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -3,75 +3,6 @@ import Hashmap.Funs open Primitives open Result -namespace List - -theorem index_ne - {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (j: ℤ) (x: α) : - 0 ≤ i → i < l.len → 0 ≤ j → j < l.len → j ≠ i → - (l.update i x).index j = l.index j - := - λ _ _ _ _ _ => match l with - | [] => by simp at * - | hd :: tl => - if h: i = 0 then - have : j ≠ 0 := by scalar_tac - by simp [*] - else if h : j = 0 then - have : i ≠ 0 := by scalar_tac - by simp [*] - else - by - simp [*] - simp at * - apply index_ne <;> scalar_tac - -theorem index_eq - {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (x: α) : - 0 ≤ i → i < l.len → - (l.update i x).index i = x - := - fun _ _ => match l with - | [] => by simp at *; exfalso; scalar_tac -- TODO: exfalso needed. Son FIXME - | hd :: tl => - if h: i = 0 then - by - simp [*] - else - by - simp [*] - simp at * - apply index_eq <;> scalar_tac - -def allP {α : Type u} (l : List α) (p: α → Prop) : Prop := - foldr (fun a r => p a ∧ r) True l - -@[simp] -theorem allP_nil {α : Type u} (p: α → Prop) : allP [] p := - by simp [allP, foldr] - -@[simp] -theorem allP_cons {α : Type u} (hd: α) (tl : List α) (p: α → Prop) : - allP (hd :: tl) p ↔ p hd ∧ allP tl p - := by simp [allP, foldr] - -def pairwise_rel - {α : Type u} (rel : α → α → Prop) (l: List α) : Prop - := match l with - | [] => True - | hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl - -@[simp] -theorem pairwise_rel_nil {α : Type u} (rel : α → α → Prop) : - pairwise_rel rel [] - := by simp [pairwise_rel] - -@[simp] -theorem pairwise_rel_cons {α : Type u} (rel : α → α → Prop) (hd: α) (tl: List α) : - pairwise_rel rel (hd :: tl) ↔ allP tl (rel hd) ∧ pairwise_rel rel tl - := by simp [pairwise_rel] - -end List - namespace hashmap namespace List @@ -104,18 +35,16 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : rw [insert_in_list_loop] simp [h] else + have ⟨ b, hi ⟩ := insert_in_list_spec key value tl by - -- TODO: use progress: detect that this is a recursive call, or give - -- the possibility of specifying an identifier - have ⟨ b, hi ⟩ := insert_in_list_spec key value tl exists b simp [insert_in_list, List.lookup] - rw [insert_in_list_loop] -- TODO: Using it in simp leads to infinite recursion + rw [insert_in_list_loop] -- TODO: Using simp leads to infinite recursion simp [h] simp [insert_in_list] at hi exact hi -set_option trace.Progress true +-- Variation: use progress @[pspec] theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, @@ -134,18 +63,13 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) simp only [insert_in_list] rw [insert_in_list_loop] conv => rhs; ext; simp [*] - progress as ⟨ b hi ⟩ - - -- TODO: use progress: detect that this is a recursive call, or give - -- the possibility of specifying an identifier - have ⟨ b, hi ⟩ := insert_in_list_spec key value tl + progress keep as heq as ⟨ b hi ⟩ + simp only [insert_in_list] at heq exists b - simp [insert_in_list, List.lookup] - rw [insert_in_list_loop] -- TODO: Using it in simp leads to infinite recursion - simp [h] - simp [insert_in_list] at hi - exact hi + simp only [heq, hi] + simp [*, List.lookup] +-- Variation: use tactics from the beginning @[pspec] theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, -- cgit v1.2.3 From 03492250b45855fe9db5e0a28a96166607cd84a1 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 20 Jul 2023 14:14:34 +0200 Subject: Make some proofs in Hashmap/Properties.lean and improve progress --- tests/lean/Hashmap/Properties.lean | 76 ++++++++++++++++++++++++++++++++------ 1 file changed, 65 insertions(+), 11 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index baa8f5c8..e065bb36 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -21,8 +21,9 @@ end List namespace HashMap -@[pspec] -theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : +abbrev Core.List := _root_.List + +theorem insert_in_list_spec0 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ (b ↔ List.lookup ls.v key = none) @@ -35,7 +36,7 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : rw [insert_in_list_loop] simp [h] else - have ⟨ b, hi ⟩ := insert_in_list_spec key value tl + have ⟨ b, hi ⟩ := insert_in_list_spec0 key value tl by exists b simp [insert_in_list, List.lookup] @@ -45,7 +46,6 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : exact hi -- Variation: use progress -@[pspec] theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ @@ -70,7 +70,6 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) simp [*, List.lookup] -- Variation: use tactics from the beginning -@[pspec] theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ @@ -91,10 +90,10 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) progress as ⟨ b h ⟩ simp [*] -@[pspec] theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List α) : ∃ l1, insert_in_list_back α key value l0 = ret l1 ∧ + -- We update the binding List.lookup l1.v key = value ∧ (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k) := match l0 with @@ -112,11 +111,66 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List simp [insert_in_list_back, List.lookup] rw [insert_in_list_loop_back] simp [h, List.lookup] - have ⟨tl0 , _, _ ⟩ := insert_in_list_back_spec key value tl -- TODO: Use progress - simp [insert_in_list_back] at * - simp [List.lookup, *] - simp (config := {contextual := true}) [*] - + progress keep as heq as ⟨ tl hp1 hp2 ⟩ + simp [insert_in_list_back] at heq + simp (config := {contextual := true}) [*, List.lookup] + +def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x.fst ≠ y.fst) + +def hash_mod_key (k : Usize) (l : Int) : Int := + match hash_key k with + | .ret k => k.val % l + | _ => 0 + +def slot_s_inv_hash (l i : Int) (ls : Core.List (Usize × α)) : Prop := + ls.allP (λ (k, _) => hash_mod_key k l = i) + +@[simp] +def slot_s_inv (l i : Int) (ls : Core.List (Usize × α)) : Prop := + distinct_keys ls ∧ + slot_s_inv_hash l i ls + +def slot_t_inv (l i : Int) (s : List α) : Prop := slot_s_inv l i s.v + +@[pspec] +theorem insert_in_list_back_spec1 {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α) + (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) : + ∃ l1, + insert_in_list_back α key value l0 = ret l1 ∧ + -- We update the binding + List.lookup l1.v key = value ∧ + (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k) ∧ + -- We preserve part of the key invariant + slot_s_inv_hash l (hash_mod_key key l) l1.v + := match l0 with + | .Nil => by + simp [insert_in_list_back, insert_in_list_loop_back, List.lookup, List.v, slot_s_inv_hash] + tauto + | .Cons k v tl0 => + if h: k = key then + by + simp [insert_in_list_back, List.lookup] + rw [insert_in_list_loop_back] + simp [h, List.lookup] + constructor + . intros; simp [*] + . simp [List.v, slot_s_inv_hash] at * + simp [*] + else + by + simp [insert_in_list_back, List.lookup] + rw [insert_in_list_loop_back] + simp [h, List.lookup] + have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by + simp_all [List.v, slot_s_inv_hash] + progress keep as heq as ⟨ tl1 hp1 hp2 hp3 ⟩ + simp only [insert_in_list_back] at heq + have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by + simp [List.v, slot_s_inv_hash] at * + simp [*] + simp (config := {contextual := true}) [*, List.lookup] + + end HashMap end hashmap -- cgit v1.2.3 From e58872aa4dc31f0819fe17b13e6b7e4b0d9635c8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 20 Jul 2023 15:46:11 +0200 Subject: Make progress on some of the hashmap proofs --- tests/lean/Hashmap/Properties.lean | 167 ++++++++++++++++++++++++++++--------- 1 file changed, 127 insertions(+), 40 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index e065bb36..66c386f2 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -3,6 +3,18 @@ import Hashmap.Funs open Primitives open Result +namespace List + +-- TODO: we don't want to use the original List.lookup because it uses BEq +-- TODO: rewrite rule: match x == y with ... -> if x = y then ... else ... ? +@[simp] +def lookup' {α : Type} (ls: _root_.List (Usize × α)) (key: Usize) : Option α := + match ls with + | [] => none + | (k, x) :: tl => if k = key then some x else lookup' tl key + +end List + namespace hashmap namespace List @@ -12,10 +24,15 @@ def v {α : Type} (ls: List α) : _root_.List (Usize × α) := | Nil => [] | Cons k x tl => (k, x) :: v tl -def lookup {α : Type} (ls: _root_.List (Usize × α)) (key: Usize) : Option α := - match ls with - | [] => none - | (k, x) :: tl => if k = key then some x else lookup tl key +@[simp] theorem v_nil (α : Type) : (Nil : List α).v = [] := by rfl +@[simp] theorem v_cons {α : Type} k x (tl: List α) : (Cons k x tl).v = (k, x) :: v tl := by rfl + +@[simp] +abbrev lookup {α : Type} (ls: List α) (key: Usize) : Option α := + ls.v.lookup' key + +@[simp] +abbrev len {α : Type} (ls : List α) : Int := ls.v.len end List @@ -23,39 +40,51 @@ namespace HashMap abbrev Core.List := _root_.List +namespace List + +end List + +-- TODO: move +@[simp] theorem neq_imp_nbeq [BEq α] [LawfulBEq α] (x y : α) (heq : ¬ x = y) : ¬ x == y := by simp [*] +@[simp] theorem neq_imp_nbeq_rev [BEq α] [LawfulBEq α] (x y : α) (heq : ¬ x = y) : ¬ y == x := by simp [*] + +-- TODO: move +theorem match_lawful_beq [BEq α] [LawfulBEq α] [DecidableEq α] (x y : α) : + (x == y) = (if x = y then true else false) := by + split <;> simp_all + theorem insert_in_list_spec0 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ - (b ↔ List.lookup ls.v key = none) + (b ↔ ls.lookup key = none) := match ls with - | .Nil => by simp [insert_in_list, insert_in_list_loop, List.lookup] + | .Nil => by simp [insert_in_list, insert_in_list_loop] | .Cons k v tl => if h: k = key then -- TODO: The order of k/key matters by - simp [insert_in_list, List.lookup] + simp [insert_in_list] rw [insert_in_list_loop] simp [h] else have ⟨ b, hi ⟩ := insert_in_list_spec0 key value tl by exists b - simp [insert_in_list, List.lookup] + simp [insert_in_list] rw [insert_in_list_loop] -- TODO: Using simp leads to infinite recursion - simp [h] - simp [insert_in_list] at hi - exact hi + simp only [insert_in_list] at hi + simp [*] -- Variation: use progress theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ - (b ↔ List.lookup ls.v key = none) + (b ↔ ls.lookup key = none) := match ls with - | .Nil => by simp [insert_in_list, insert_in_list_loop, List.lookup] + | .Nil => by simp [insert_in_list, insert_in_list_loop] | .Cons k v tl => if h: k = key then -- TODO: The order of k/key matters by - simp [insert_in_list, List.lookup] + simp [insert_in_list] rw [insert_in_list_loop] simp [h] else @@ -66,19 +95,17 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) progress keep as heq as ⟨ b hi ⟩ simp only [insert_in_list] at heq exists b - simp only [heq, hi] - simp [*, List.lookup] -- Variation: use tactics from the beginning theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ - (b ↔ (List.lookup ls.v key = none)) + (b ↔ (ls.lookup key = none)) := by induction ls - case Nil => simp [insert_in_list, insert_in_list_loop, List.lookup] + case Nil => simp [insert_in_list, insert_in_list_loop] case Cons k v tl ih => - simp only [insert_in_list, List.lookup] + simp only [insert_in_list] rw [insert_in_list_loop] simp only if h: k = key then @@ -94,26 +121,27 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List ∃ l1, insert_in_list_back α key value l0 = ret l1 ∧ -- We update the binding - List.lookup l1.v key = value ∧ - (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k) + l1.lookup key = value ∧ + (∀ k, k ≠ key → l1.lookup k = l0.lookup k) := match l0 with - | .Nil => by simp [insert_in_list_back, insert_in_list_loop_back, List.lookup]; tauto + | .Nil => by + simp (config := {contextual := true}) [insert_in_list_back, insert_in_list_loop_back] | .Cons k v tl => if h: k = key then by - simp [insert_in_list_back, List.lookup] + simp [insert_in_list_back] rw [insert_in_list_loop_back] - simp [h, List.lookup] + simp [h] intro k1 h1 simp [*] else by - simp [insert_in_list_back, List.lookup] + simp [insert_in_list_back] rw [insert_in_list_loop_back] - simp [h, List.lookup] + simp [h] progress keep as heq as ⟨ tl hp1 hp2 ⟩ simp [insert_in_list_back] at heq - simp (config := {contextual := true}) [*, List.lookup] + simp (config := {contextual := true}) [*] def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x.fst ≠ y.fst) @@ -132,44 +160,103 @@ def slot_s_inv (l i : Int) (ls : Core.List (Usize × α)) : Prop := def slot_t_inv (l i : Int) (s : List α) : Prop := slot_s_inv l i s.v -@[pspec] -theorem insert_in_list_back_spec1 {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α) +theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α) (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) : ∃ l1, insert_in_list_back α key value l0 = ret l1 ∧ -- We update the binding - List.lookup l1.v key = value ∧ - (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k) ∧ + l1.lookup key = value ∧ + (∀ k, k ≠ key → l1.lookup k = l0.lookup k) ∧ -- We preserve part of the key invariant - slot_s_inv_hash l (hash_mod_key key l) l1.v + slot_s_inv_hash l (hash_mod_key key l) l1.v ∧ + -- Reasoning about the length + match l0.lookup key with + | none => l1.len = l0.len + 1 + | some _ => l1.len = l0.len := match l0 with | .Nil => by - simp [insert_in_list_back, insert_in_list_loop_back, List.lookup, List.v, slot_s_inv_hash] - tauto + simp (config := {contextual := true}) [insert_in_list_back, insert_in_list_loop_back, List.v, slot_s_inv_hash] | .Cons k v tl0 => if h: k = key then by - simp [insert_in_list_back, List.lookup] + simp [insert_in_list_back] rw [insert_in_list_loop_back] - simp [h, List.lookup] + simp [h] constructor . intros; simp [*] . simp [List.v, slot_s_inv_hash] at * simp [*] else by - simp [insert_in_list_back, List.lookup] + simp [insert_in_list_back] rw [insert_in_list_loop_back] - simp [h, List.lookup] + simp [h] have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by simp_all [List.v, slot_s_inv_hash] - progress keep as heq as ⟨ tl1 hp1 hp2 hp3 ⟩ + progress keep as heq as ⟨ tl1 hp1 hp2 hp3 hp4 ⟩ simp only [insert_in_list_back] at heq have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by simp [List.v, slot_s_inv_hash] at * simp [*] - simp (config := {contextual := true}) [*, List.lookup] + -- TODO: canonize addition by default? + simp_all [Int.add_assoc, Int.add_comm, Int.add_left_comm] +theorem insert_in_list_back_spec_aux1 {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α) + (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) + (hdk : distinct_keys l0.v) : + ∃ l1, + insert_in_list_back α key value l0 = ret l1 ∧ + -- We update the binding + l1.lookup key = value ∧ + (∀ k, k ≠ key → l1.lookup k = l0.lookup k) ∧ + -- We preserve part of the key invariant + slot_s_inv_hash l (hash_mod_key key l) l1.v ∧ + -- Reasoning about the length + (match l0.lookup key with + | none => l1.len = l0.len + 1 + | some _ => l1.len = l0.len) ∧ + -- The keys are distinct + distinct_keys l1.v ∧ + -- We need this auxiliary property to prove that the keys distinct properties is preserved + (∀ k, k ≠ key → l0.v.allP (λ (k1, _) => k ≠ k1) → l1.v.allP (λ (k1, _) => k ≠ k1)) + := match l0 with + | .Nil => by + simp (config := {contextual := true}) + [insert_in_list_back, insert_in_list_loop_back, + List.v, slot_s_inv_hash, distinct_keys, List.pairwise_rel] + | .Cons k v tl0 => + if h: k = key then + by + simp [insert_in_list_back] + rw [insert_in_list_loop_back] + simp [h] + split_target_conjs + . intros; simp [*] + . simp [List.v, slot_s_inv_hash] at * + simp [*] + . simp [*, distinct_keys] at * + apply hdk + . tauto + else + by + simp [insert_in_list_back] + rw [insert_in_list_loop_back] + simp [h] + have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by + simp_all [List.v, slot_s_inv_hash] + have : distinct_keys (List.v tl0) := by + simp [distinct_keys] at hdk + simp [hdk, distinct_keys] + progress keep as heq as ⟨ tl1 hp1 hp2 hp3 hp4 hp5 hp6 ⟩ -- TODO: naming is weird + simp only [insert_in_list_back] at heq + have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by + simp [List.v, slot_s_inv_hash] at * + simp [*] + have : distinct_keys ((k, v) :: List.v tl1) := by + simp [distinct_keys] at * + simp [*] + -- TODO: canonize addition by default? + simp_all [Int.add_assoc, Int.add_comm, Int.add_left_comm] end HashMap -- cgit v1.2.3 From c5536f372194240d164583cecee5265213b3e671 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 20 Jul 2023 16:13:47 +0200 Subject: Improve the interactivity of some hashmap proofs --- tests/lean/Hashmap/Properties.lean | 109 ++++++++++++------------------------- 1 file changed, 34 insertions(+), 75 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 66c386f2..dce33fa4 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -6,7 +6,8 @@ open Result namespace List -- TODO: we don't want to use the original List.lookup because it uses BEq --- TODO: rewrite rule: match x == y with ... -> if x = y then ... else ... ? +-- TODO: rewrite rule: match x == y with ... -> if x = y then ... else ... ? (actually doesn't work because of sugar) +-- TODO: move? @[simp] def lookup' {α : Type} (ls: _root_.List (Usize × α)) (key: Usize) : Option α := match ls with @@ -49,6 +50,7 @@ end List @[simp] theorem neq_imp_nbeq_rev [BEq α] [LawfulBEq α] (x y : α) (heq : ¬ x = y) : ¬ y == x := by simp [*] -- TODO: move +-- TODO: this doesn't work because of sugar theorem match_lawful_beq [BEq α] [LawfulBEq α] [DecidableEq α] (x y : α) : (x == y) = (if x = y then true else false) := by split <;> simp_all @@ -161,47 +163,6 @@ def slot_s_inv (l i : Int) (ls : Core.List (Usize × α)) : Prop := def slot_t_inv (l i : Int) (s : List α) : Prop := slot_s_inv l i s.v theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α) - (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) : - ∃ l1, - insert_in_list_back α key value l0 = ret l1 ∧ - -- We update the binding - l1.lookup key = value ∧ - (∀ k, k ≠ key → l1.lookup k = l0.lookup k) ∧ - -- We preserve part of the key invariant - slot_s_inv_hash l (hash_mod_key key l) l1.v ∧ - -- Reasoning about the length - match l0.lookup key with - | none => l1.len = l0.len + 1 - | some _ => l1.len = l0.len - := match l0 with - | .Nil => by - simp (config := {contextual := true}) [insert_in_list_back, insert_in_list_loop_back, List.v, slot_s_inv_hash] - | .Cons k v tl0 => - if h: k = key then - by - simp [insert_in_list_back] - rw [insert_in_list_loop_back] - simp [h] - constructor - . intros; simp [*] - . simp [List.v, slot_s_inv_hash] at * - simp [*] - else - by - simp [insert_in_list_back] - rw [insert_in_list_loop_back] - simp [h] - have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by - simp_all [List.v, slot_s_inv_hash] - progress keep as heq as ⟨ tl1 hp1 hp2 hp3 hp4 ⟩ - simp only [insert_in_list_back] at heq - have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by - simp [List.v, slot_s_inv_hash] at * - simp [*] - -- TODO: canonize addition by default? - simp_all [Int.add_assoc, Int.add_comm, Int.add_left_comm] - -theorem insert_in_list_back_spec_aux1 {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α) (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) (hdk : distinct_keys l0.v) : ∃ l1, @@ -220,43 +181,41 @@ theorem insert_in_list_back_spec_aux1 {α : Type} (l : Int) (key: Usize) (value: -- We need this auxiliary property to prove that the keys distinct properties is preserved (∀ k, k ≠ key → l0.v.allP (λ (k1, _) => k ≠ k1) → l1.v.allP (λ (k1, _) => k ≠ k1)) := match l0 with - | .Nil => by + | .Nil => by checkpoint simp (config := {contextual := true}) [insert_in_list_back, insert_in_list_loop_back, List.v, slot_s_inv_hash, distinct_keys, List.pairwise_rel] | .Cons k v tl0 => - if h: k = key then - by - simp [insert_in_list_back] - rw [insert_in_list_loop_back] - simp [h] - split_target_conjs - . intros; simp [*] - . simp [List.v, slot_s_inv_hash] at * - simp [*] - . simp [*, distinct_keys] at * - apply hdk - . tauto - else - by - simp [insert_in_list_back] - rw [insert_in_list_loop_back] - simp [h] - have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by - simp_all [List.v, slot_s_inv_hash] - have : distinct_keys (List.v tl0) := by - simp [distinct_keys] at hdk - simp [hdk, distinct_keys] - progress keep as heq as ⟨ tl1 hp1 hp2 hp3 hp4 hp5 hp6 ⟩ -- TODO: naming is weird - simp only [insert_in_list_back] at heq - have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by - simp [List.v, slot_s_inv_hash] at * - simp [*] - have : distinct_keys ((k, v) :: List.v tl1) := by - simp [distinct_keys] at * - simp [*] - -- TODO: canonize addition by default? - simp_all [Int.add_assoc, Int.add_comm, Int.add_left_comm] + if h: k = key then by checkpoint + simp [insert_in_list_back] + rw [insert_in_list_loop_back] + simp [h] + split_target_conjs + . intros; simp [*] + . simp [List.v, slot_s_inv_hash] at * + simp [*] + . simp [*, distinct_keys] at * + apply hdk + . tauto + else by checkpoint + simp [insert_in_list_back] + rw [insert_in_list_loop_back] + simp [h] + have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by checkpoint + simp_all [List.v, slot_s_inv_hash] + have : distinct_keys (List.v tl0) := by checkpoint + simp [distinct_keys] at hdk + simp [hdk, distinct_keys] + progress keep as heq as ⟨ tl1 hp1 hp2 hp3 hp4 hp5 hp6 ⟩ + simp only [insert_in_list_back] at heq + have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by checkpoint + simp [List.v, slot_s_inv_hash] at * + simp [*] + have : distinct_keys ((k, v) :: List.v tl1) := by checkpoint + simp [distinct_keys] at * + simp [*] + -- TODO: canonize addition by default? + simp_all [Int.add_assoc, Int.add_comm, Int.add_left_comm] end HashMap -- cgit v1.2.3 From 2dd56a51df01421fe7766858c9d37998db4123b5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 25 Jul 2023 11:53:49 +0200 Subject: Improve the syntax of progress: `as ⟨ x, y .. ⟩` --- tests/lean/Hashmap/Properties.lean | 34 ++++------------------------------ 1 file changed, 4 insertions(+), 30 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index dce33fa4..de6bf636 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -94,7 +94,7 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) simp only [insert_in_list] rw [insert_in_list_loop] conv => rhs; ext; simp [*] - progress keep as heq as ⟨ b hi ⟩ + progress keep as heq as ⟨ b, hi ⟩ simp only [insert_in_list] at heq exists b @@ -116,35 +116,9 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) conv => rhs; ext; left; simp [h] -- TODO: Simplify simp only [insert_in_list] at ih; -- TODO: give the possibility of using underscores - progress as ⟨ b h ⟩ + progress as ⟨ b, h ⟩ simp [*] -theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List α) : - ∃ l1, - insert_in_list_back α key value l0 = ret l1 ∧ - -- We update the binding - l1.lookup key = value ∧ - (∀ k, k ≠ key → l1.lookup k = l0.lookup k) - := match l0 with - | .Nil => by - simp (config := {contextual := true}) [insert_in_list_back, insert_in_list_loop_back] - | .Cons k v tl => - if h: k = key then - by - simp [insert_in_list_back] - rw [insert_in_list_loop_back] - simp [h] - intro k1 h1 - simp [*] - else - by - simp [insert_in_list_back] - rw [insert_in_list_loop_back] - simp [h] - progress keep as heq as ⟨ tl hp1 hp2 ⟩ - simp [insert_in_list_back] at heq - simp (config := {contextual := true}) [*] - def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x.fst ≠ y.fst) def hash_mod_key (k : Usize) (l : Int) : Int := @@ -190,7 +164,7 @@ theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value: simp [insert_in_list_back] rw [insert_in_list_loop_back] simp [h] - split_target_conjs + split_conjs . intros; simp [*] . simp [List.v, slot_s_inv_hash] at * simp [*] @@ -206,7 +180,7 @@ theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value: have : distinct_keys (List.v tl0) := by checkpoint simp [distinct_keys] at hdk simp [hdk, distinct_keys] - progress keep as heq as ⟨ tl1 hp1 hp2 hp3 hp4 hp5 hp6 ⟩ + progress keep as heq as ⟨ tl1 .. ⟩ simp only [insert_in_list_back] at heq have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by checkpoint simp [List.v, slot_s_inv_hash] at * -- cgit v1.2.3 From 1854c631a6a7a3f8d45ad18e05547f9d3782c3ee Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 25 Jul 2023 16:26:08 +0200 Subject: Make progress on the hashmap properties --- tests/lean/Hashmap/Properties.lean | 92 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 92 insertions(+) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index de6bf636..b2d5570a 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -136,6 +136,40 @@ def slot_s_inv (l i : Int) (ls : Core.List (Usize × α)) : Prop := def slot_t_inv (l i : Int) (s : List α) : Prop := slot_s_inv l i s.v +-- Interpret the hashmap as a list of lists +def v (hm : HashMap α) : Core.List (Core.List (Usize × α)) := + hm.slots.val.map List.v + +-- Interpret the hashmap as an associative list +def al_v (hm : HashMap α) : Core.List (Usize × α) := + hm.v.flatten + +-- TODO: automatic derivation +instance : Inhabited (List α) where + default := .Nil + +@[simp] +def slots_s_inv (s : Core.List (List α)) : Prop := + ∀ (i : Int), 0 ≤ i → i < s.len → slot_t_inv s.len i (s.index i) + +def slots_t_inv (s : Vec (List α)) : Prop := + slots_s_inv s.v + +@[simp] +def base_inv (hm : HashMap α) : Prop := + -- [num_entries] correctly tracks the number of entries + hm.num_entries.val = hm.al_v.len ∧ + -- Slots invariant + slots_t_inv hm.slots ∧ + -- The capacity must be > 0 (otherwise we can't resize) + 0 < hm.slots.length + -- TODO: load computation + +def inv (hm : HashMap α) : Prop := + -- Base invariant + base_inv hm + -- TODO: either the hashmap is not overloaded, or we can't resize it + theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α) (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) (hdk : distinct_keys l0.v) : @@ -191,6 +225,64 @@ theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value: -- TODO: canonize addition by default? simp_all [Int.add_assoc, Int.add_comm, Int.add_left_comm] +@[pspec] +theorem insert_in_list_back_spec {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α) + (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) + (hdk : distinct_keys l0.v) : + ∃ l1, + insert_in_list_back α key value l0 = ret l1 ∧ + -- We update the binding + l1.lookup key = value ∧ + (∀ k, k ≠ key → l1.lookup k = l0.lookup k) ∧ + -- We preserve part of the key invariant + slot_s_inv_hash l (hash_mod_key key l) l1.v ∧ + -- Reasoning about the length + (match l0.lookup key with + | none => l1.len = l0.len + 1 + | some _ => l1.len = l0.len) ∧ + -- The keys are distinct + distinct_keys l1.v + := by + progress with insert_in_list_back_spec_aux as ⟨ l1 .. ⟩ + exists l1 + +def slots_t_lookup (s : Core.List (List α)) (k : Usize) : Option α := + let i := hash_mod_key k s.len + let slot := s.index i + slot.lookup k + +def lookup (hm : HashMap α) (k : Usize) : Option α := + slots_t_lookup hm.slots.val k + +@[simp] +abbrev len_s (hm : HashMap α) : Int := hm.al_v.len + +set_option trace.Progress true +/-set_option pp.explicit true +set_option pp.universes true +set_option pp.notation false-/ + +theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α) + (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) : + ∃ nhm, hm.insert_no_resize α key value = ret nhm ∧ + -- We preserve the invariant + nhm.inv ∧ + -- We updated the binding for key + nhm.lookup key = some value ∧ + -- We left the other bindings unchanged + (∀ k, k ≠ key → nhm.lookup k = hm.lookup k) ∧ + -- Reasoning about the length + (match hm.lookup key with + | none => nhm.len_s = hm.len_s + 1 + | some _ => nhm.len_s = hm.len_s) := by + rw [insert_no_resize] + simp [hash_key] + have : (Vec.len (List α) hm.slots).val ≠ 0 := by + intro + simp_all [inv] + progress as ⟨ hash_mod ⟩ + progress + end HashMap end hashmap -- cgit v1.2.3 From 0cc3c78137434d848188eee2a66b1e2cacfd102e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 25 Jul 2023 19:06:05 +0200 Subject: Make progress on the proofs of the hashmap --- tests/lean/Hashmap/Properties.lean | 116 +++++++++++++++++++++++++++++++++++-- 1 file changed, 112 insertions(+), 4 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index b2d5570a..92285c0d 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -55,6 +55,7 @@ theorem match_lawful_beq [BEq α] [LawfulBEq α] [DecidableEq α] (x y : α) : (x == y) = (if x = y then true else false) := by split <;> simp_all +@[pspec] theorem insert_in_list_spec0 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ @@ -126,6 +127,10 @@ def hash_mod_key (k : Usize) (l : Int) : Int := | .ret k => k.val % l | _ => 0 +@[simp] +theorem hash_mod_key_eq : hash_mod_key k l = k.val % l := by + simp [hash_mod_key, hash_key] + def slot_s_inv_hash (l i : Int) (ls : Core.List (Usize × α)) : Prop := ls.allP (λ (k, _) => hash_mod_key k l = i) @@ -246,6 +251,7 @@ theorem insert_in_list_back_spec {α : Type} (l : Int) (key: Usize) (value: α) progress with insert_in_list_back_spec_aux as ⟨ l1 .. ⟩ exists l1 +@[simp] def slots_t_lookup (s : Core.List (List α)) (k : Usize) : Option α := let i := hash_mod_key k s.len let slot := s.index i @@ -260,7 +266,15 @@ abbrev len_s (hm : HashMap α) : Int := hm.al_v.len set_option trace.Progress true /-set_option pp.explicit true set_option pp.universes true -set_option pp.notation false-/ +set_option pp.notation false -/ + +-- Remark: α and β must live in the same universe, otherwise the +-- bind doesn't work +theorem if_update_eq + {α β : Type u} (b : Bool) (y : α) (e : Result α) (f : α → Result β) : + (if b then Bind.bind e f else f y) = Bind.bind (if b then e else pure y) f + := by + split <;> simp [Pure.pure] theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α) (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) : @@ -270,18 +284,112 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value -- We updated the binding for key nhm.lookup key = some value ∧ -- We left the other bindings unchanged - (∀ k, k ≠ key → nhm.lookup k = hm.lookup k) ∧ + (∀ k, ¬ k = key → nhm.lookup k = hm.lookup k) ∧ -- Reasoning about the length (match hm.lookup key with | none => nhm.len_s = hm.len_s + 1 | some _ => nhm.len_s = hm.len_s) := by rw [insert_no_resize] simp [hash_key] - have : (Vec.len (List α) hm.slots).val ≠ 0 := by + have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint intro simp_all [inv] - progress as ⟨ hash_mod ⟩ + -- TODO: progress keep as ⟨ ... ⟩ : conflict + progress keep as h as ⟨ hash_mod, hhm ⟩ + have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac + have _ : hash_mod.val < Vec.length hm.slots := by sorry + -- have h := Primitives.Vec.index_mut_spec hm.slots hash_mod + -- TODO: change the spec of Vec.index_mut to introduce a let-binding. + -- or: make progress introduce the let-binding by itself (this is clearer) progress + -- TODO: make progress use the names written in the goal + progress as ⟨ inserted ⟩ + rw [if_update_eq] -- TODO: necessary because we don't have a join + -- TODO: progress to ... + have hipost : + ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ret i0 ∧ + i0.val = if inserted then hm.num_entries.val + 1 else hm.num_entries.val + := by sorry + progress as ⟨ i0 ⟩ + -- TODO: progress "eager" to match premises with assumptions while instantiating + -- meta-variables + have h_slot : slot_s_inv_hash hm.slots.length hash_mod.val (hm.slots.v.index hash_mod.val).v := by sorry + have hd : distinct_keys (hm.slots.v.index hash_mod.val).v := by checkpoint + simp [inv, slots_t_inv, slot_t_inv] at hinv + have h := hinv.right.left hash_mod.val (by assumption) (by assumption) + simp [h] + -- TODO: hide the variables and only keep the props + -- TODO: allow providing terms to progress to instantiate the meta variables + -- which are not propositions + progress as ⟨ l0, _, _, _, hlen .. ⟩ + . checkpoint exact hm.slots.length + . checkpoint simp_all + . -- Finishing the proof + progress as ⟨ v ⟩ + -- TODO: update progress to automate that + let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v } + exists nhm + have hupdt : lookup nhm key = some value := by checkpoint + simp [lookup, List.lookup] at * + simp_all + have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by checkpoint + simp [lookup, List.lookup] at * + intro k hk + -- We have to make a case disjunction: either the hashes are different, + -- in which case we don't even lookup the same slots, or the hashes + -- are the same, in which case we have to reason about what happens + -- in one slot + let k_hash_mod := k.val % v.val.len + have _ : 0 ≤ k_hash_mod := by sorry + have _ : k_hash_mod < Vec.length hm.slots := by sorry + if h_hm : k_hash_mod = hash_mod.val then + simp_all + else + simp_all + have _ : + match hm.lookup key with + | none => nhm.len_s = hm.len_s + 1 + | some _ => nhm.len_s = hm.len_s := by checkpoint + simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_t_lookup] at * + -- We have to do a case disjunction + simp_all + simp [_root_.List.update_map_eq] + -- TODO: dependent rewrites + have _ : key.val % hm.slots.val.len < (List.map List.v hm.slots.val).len := by + simp [*] + simp [_root_.List.len_flatten_update_eq, *] + split <;> + rename_i heq <;> + simp [heq] at hlen <;> + -- TODO: canonize addition by default? We need a tactic to simplify arithmetic equalities + -- with addition and substractions ((ℤ, +) is a ring or something - there should exist a tactic + -- somewhere in mathlib?) + simp [Int.add_assoc, Int.add_comm, Int.add_left_comm] <;> + int_tac + have hinv : inv nhm := by + simp [inv] at * + split_conjs + . match h: lookup hm key with + | none => + simp [h, lookup] at * + simp_all + | some _ => + simp_all [lookup] + . simp [slots_t_inv, slot_t_inv] at * + intro i hipos _ + have hs := hinv.right.left i hipos (by simp_all) + -- We need a case disjunction + if i = key.val % _root_.List.len hm.slots.val then + simp_all + else + simp_all + . match h: lookup hm key with + | none => + simp [h] at * + simp [*] + | some _ => + simp_all + simp_all end HashMap -- cgit v1.2.3 From 9e8fccbe4b667fc341b6544030f85af05fe89307 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 25 Jul 2023 20:12:48 +0200 Subject: Make progress on the proofs of the hashmap --- tests/lean/Hashmap/Properties.lean | 58 ++++++++++++++++++++++++++------------ 1 file changed, 40 insertions(+), 18 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 92285c0d..40b5009d 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -263,11 +263,6 @@ def lookup (hm : HashMap α) (k : Usize) : Option α := @[simp] abbrev len_s (hm : HashMap α) : Int := hm.al_v.len -set_option trace.Progress true -/-set_option pp.explicit true -set_option pp.universes true -set_option pp.notation false -/ - -- Remark: α and β must live in the same universe, otherwise the -- bind doesn't work theorem if_update_eq @@ -297,7 +292,12 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value -- TODO: progress keep as ⟨ ... ⟩ : conflict progress keep as h as ⟨ hash_mod, hhm ⟩ have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac - have _ : hash_mod.val < Vec.length hm.slots := by sorry + have _ : hash_mod.val < Vec.length hm.slots := by + have : 0 < hm.slots.val.len := by + simp [inv] at hinv + simp [hinv] + -- TODO: we want to automate that + simp [*, Int.emod_lt_of_pos] -- have h := Primitives.Vec.index_mut_spec hm.slots hash_mod -- TODO: change the spec of Vec.index_mut to introduce a let-binding. -- or: make progress introduce the let-binding by itself (this is clearer) @@ -309,11 +309,26 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value have hipost : ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ret i0 ∧ i0.val = if inserted then hm.num_entries.val + 1 else hm.num_entries.val - := by sorry + := by + if inserted then + simp [*] + have : hm.num_entries.val + (Usize.ofInt 1).val ≤ Usize.max := by + simp [lookup] at hnsat + simp_all + simp [inv] at hinv + int_tac + progress + simp_all + else + simp_all [Pure.pure] progress as ⟨ i0 ⟩ -- TODO: progress "eager" to match premises with assumptions while instantiating -- meta-variables - have h_slot : slot_s_inv_hash hm.slots.length hash_mod.val (hm.slots.v.index hash_mod.val).v := by sorry + have h_slot : slot_s_inv_hash hm.slots.length hash_mod.val (hm.slots.v.index hash_mod.val).v := by + simp [inv] at hinv + have h := hinv.right.left hash_mod.val (by assumption) (by assumption) + simp [slot_t_inv] at h + simp [h] have hd : distinct_keys (hm.slots.v.index hash_mod.val).v := by checkpoint simp [inv, slots_t_inv, slot_t_inv] at hinv have h := hinv.right.left hash_mod.val (by assumption) (by assumption) @@ -329,10 +344,11 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value -- TODO: update progress to automate that let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v } exists nhm + -- TODO: later I don't want to inline nhm - we need to control simp have hupdt : lookup nhm key = some value := by checkpoint simp [lookup, List.lookup] at * simp_all - have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by checkpoint + have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by simp [lookup, List.lookup] at * intro k hk -- We have to make a case disjunction: either the hashes are different, @@ -340,8 +356,19 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value -- are the same, in which case we have to reason about what happens -- in one slot let k_hash_mod := k.val % v.val.len - have _ : 0 ≤ k_hash_mod := by sorry - have _ : k_hash_mod < Vec.length hm.slots := by sorry + have : 0 < hm.slots.val.len := by simp_all [inv] + have hvpos : 0 < v.val.len := by simp_all + have hvnz: v.val.len ≠ 0 := by + simp_all + have _ : 0 ≤ k_hash_mod := by + -- TODO: we want to automate this + simp + apply Int.emod_nonneg k.val hvnz + have _ : k_hash_mod < Vec.length hm.slots := by + -- TODO: we want to automate this + simp + have h := Int.emod_lt_of_pos k.val hvpos + simp_all if h_hm : k_hash_mod = hash_mod.val then simp_all else @@ -377,18 +404,13 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value simp_all [lookup] . simp [slots_t_inv, slot_t_inv] at * intro i hipos _ - have hs := hinv.right.left i hipos (by simp_all) + have _ := hinv.right.left i hipos (by simp_all) -- We need a case disjunction if i = key.val % _root_.List.len hm.slots.val then simp_all else simp_all - . match h: lookup hm key with - | none => - simp [h] at * - simp [*] - | some _ => - simp_all + . simp_all simp_all end HashMap -- cgit v1.2.3 From 032db82439d9b379b5435d8349c1ecf55eeb2875 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 26 Jul 2023 11:41:32 +0200 Subject: Fix a proof for the hashmap --- tests/lean/Hashmap/Properties.lean | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 40b5009d..208875a6 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -340,7 +340,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value . checkpoint exact hm.slots.length . checkpoint simp_all . -- Finishing the proof - progress as ⟨ v ⟩ + progress keep as hv as ⟨ v, h_veq ⟩ -- TODO: update progress to automate that let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v } exists nhm @@ -405,12 +405,19 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value . simp [slots_t_inv, slot_t_inv] at * intro i hipos _ have _ := hinv.right.left i hipos (by simp_all) + simp [hhm, h_veq] at * -- TODO: annoying -- We need a case disjunction - if i = key.val % _root_.List.len hm.slots.val then - simp_all + if h_ieq : i = key.val % _root_.List.len hm.slots.val then + -- TODO: simp_all loops (investigate). + -- Also, it is annoying to do this kind + -- of rewritings by hand. We could have a different simp + -- which safely substitutes variables when we have an + -- equality `x = ...` and `x` doesn't appear in the rhs + simp [h_ieq] at * + simp [*] else - simp_all - . simp_all + simp [*] + . simp [*] simp_all end HashMap -- cgit v1.2.3 From 81e991822879a942af34489b7a072f31739f28f6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 26 Jul 2023 12:37:17 +0200 Subject: Update the syntax of the progress tactic --- tests/lean/Hashmap/Properties.lean | 171 ++++++++++++++++++------------------- 1 file changed, 85 insertions(+), 86 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 208875a6..96b8193d 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -95,7 +95,7 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) simp only [insert_in_list] rw [insert_in_list_loop] conv => rhs; ext; simp [*] - progress keep as heq as ⟨ b, hi ⟩ + progress keep heq as ⟨ b, hi ⟩ simp only [insert_in_list] at heq exists b @@ -219,7 +219,7 @@ theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value: have : distinct_keys (List.v tl0) := by checkpoint simp [distinct_keys] at hdk simp [hdk, distinct_keys] - progress keep as heq as ⟨ tl1 .. ⟩ + progress keep heq as ⟨ tl1 .. ⟩ simp only [insert_in_list_back] at heq have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by checkpoint simp [List.v, slot_s_inv_hash] at * @@ -289,8 +289,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint intro simp_all [inv] - -- TODO: progress keep as ⟨ ... ⟩ : conflict - progress keep as h as ⟨ hash_mod, hhm ⟩ + progress keep _ as ⟨ hash_mod, hhm ⟩ have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac have _ : hash_mod.val < Vec.length hm.slots := by have : 0 < hm.slots.val.len := by @@ -324,11 +323,12 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value progress as ⟨ i0 ⟩ -- TODO: progress "eager" to match premises with assumptions while instantiating -- meta-variables - have h_slot : slot_s_inv_hash hm.slots.length hash_mod.val (hm.slots.v.index hash_mod.val).v := by + have h_slot : slot_s_inv_hash hm.slots.length (hash_mod_key key hm.slots.length) + (List.v (List.index (hm.slots.val) hash_mod.val)) := by simp [inv] at hinv - have h := hinv.right.left hash_mod.val (by assumption) (by assumption) - simp [slot_t_inv] at h - simp [h] + have h := (hinv.right.left hash_mod.val (by assumption) (by assumption)).right + simp [slot_t_inv, hhm] at h + simp [h, hhm] have hd : distinct_keys (hm.slots.v.index hash_mod.val).v := by checkpoint simp [inv, slots_t_inv, slot_t_inv] at hinv have h := hinv.right.left hash_mod.val (by assumption) (by assumption) @@ -337,88 +337,87 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value -- TODO: allow providing terms to progress to instantiate the meta variables -- which are not propositions progress as ⟨ l0, _, _, _, hlen .. ⟩ - . checkpoint exact hm.slots.length - . checkpoint simp_all - . -- Finishing the proof - progress keep as hv as ⟨ v, h_veq ⟩ - -- TODO: update progress to automate that - let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v } - exists nhm - -- TODO: later I don't want to inline nhm - we need to control simp - have hupdt : lookup nhm key = some value := by checkpoint - simp [lookup, List.lookup] at * + -- Finishing the proof + progress keep hv as ⟨ v, h_veq ⟩ + -- TODO: update progress to automate that + let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v } + exists nhm + -- TODO: later I don't want to inline nhm - we need to control simp + have hupdt : lookup nhm key = some value := by checkpoint + simp [lookup, List.lookup] at * + simp_all + have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by + simp [lookup, List.lookup] at * + intro k hk + -- We have to make a case disjunction: either the hashes are different, + -- in which case we don't even lookup the same slots, or the hashes + -- are the same, in which case we have to reason about what happens + -- in one slot + let k_hash_mod := k.val % v.val.len + have : 0 < hm.slots.val.len := by simp_all [inv] + have hvpos : 0 < v.val.len := by simp_all + have hvnz: v.val.len ≠ 0 := by simp_all - have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by - simp [lookup, List.lookup] at * - intro k hk - -- We have to make a case disjunction: either the hashes are different, - -- in which case we don't even lookup the same slots, or the hashes - -- are the same, in which case we have to reason about what happens - -- in one slot - let k_hash_mod := k.val % v.val.len - have : 0 < hm.slots.val.len := by simp_all [inv] - have hvpos : 0 < v.val.len := by simp_all - have hvnz: v.val.len ≠ 0 := by - simp_all - have _ : 0 ≤ k_hash_mod := by - -- TODO: we want to automate this - simp - apply Int.emod_nonneg k.val hvnz - have _ : k_hash_mod < Vec.length hm.slots := by - -- TODO: we want to automate this - simp - have h := Int.emod_lt_of_pos k.val hvpos - simp_all - if h_hm : k_hash_mod = hash_mod.val then + have _ : 0 ≤ k_hash_mod := by + -- TODO: we want to automate this + simp + apply Int.emod_nonneg k.val hvnz + have _ : k_hash_mod < Vec.length hm.slots := by + -- TODO: we want to automate this + simp + have h := Int.emod_lt_of_pos k.val hvpos + simp_all + if h_hm : k_hash_mod = hash_mod.val then + simp_all + else + simp_all + have _ : + match hm.lookup key with + | none => nhm.len_s = hm.len_s + 1 + | some _ => nhm.len_s = hm.len_s := by checkpoint + simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_t_lookup] at * + -- We have to do a case disjunction + simp_all + simp [_root_.List.update_map_eq] + -- TODO: dependent rewrites + have _ : key.val % hm.slots.val.len < (List.map List.v hm.slots.val).len := by + simp [*] + simp [_root_.List.len_flatten_update_eq, *] + split <;> + rename_i heq <;> + simp [heq] at hlen <;> + -- TODO: canonize addition by default? We need a tactic to simplify arithmetic equalities + -- with addition and substractions ((ℤ, +) is a ring or something - there should exist a tactic + -- somewhere in mathlib?) + simp [Int.add_assoc, Int.add_comm, Int.add_left_comm] <;> + int_tac + have hinv : inv nhm := by + simp [inv] at * + split_conjs + . match h: lookup hm key with + | none => + simp [h, lookup] at * simp_all + | some _ => + simp_all [lookup] + . simp [slots_t_inv, slot_t_inv] at * + intro i hipos _ + have _ := hinv.right.left i hipos (by simp_all) + simp [hhm, h_veq] at * -- TODO: annoying + -- We need a case disjunction + if h_ieq : i = key.val % _root_.List.len hm.slots.val then + -- TODO: simp_all fails: "(deterministic) timeout at 'whnf'" + -- Also, it is annoying to do this kind + -- of rewritings by hand. We could have a different simp + -- which safely substitutes variables when we have an + -- equality `x = ...` and `x` doesn't appear in the rhs + simp [h_ieq] at * + simp [*] else - simp_all - have _ : - match hm.lookup key with - | none => nhm.len_s = hm.len_s + 1 - | some _ => nhm.len_s = hm.len_s := by checkpoint - simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_t_lookup] at * - -- We have to do a case disjunction - simp_all - simp [_root_.List.update_map_eq] - -- TODO: dependent rewrites - have _ : key.val % hm.slots.val.len < (List.map List.v hm.slots.val).len := by simp [*] - simp [_root_.List.len_flatten_update_eq, *] - split <;> - rename_i heq <;> - simp [heq] at hlen <;> - -- TODO: canonize addition by default? We need a tactic to simplify arithmetic equalities - -- with addition and substractions ((ℤ, +) is a ring or something - there should exist a tactic - -- somewhere in mathlib?) - simp [Int.add_assoc, Int.add_comm, Int.add_left_comm] <;> - int_tac - have hinv : inv nhm := by - simp [inv] at * - split_conjs - . match h: lookup hm key with - | none => - simp [h, lookup] at * - simp_all - | some _ => - simp_all [lookup] - . simp [slots_t_inv, slot_t_inv] at * - intro i hipos _ - have _ := hinv.right.left i hipos (by simp_all) - simp [hhm, h_veq] at * -- TODO: annoying - -- We need a case disjunction - if h_ieq : i = key.val % _root_.List.len hm.slots.val then - -- TODO: simp_all loops (investigate). - -- Also, it is annoying to do this kind - -- of rewritings by hand. We could have a different simp - -- which safely substitutes variables when we have an - -- equality `x = ...` and `x` doesn't appear in the rhs - simp [h_ieq] at * - simp [*] - else - simp [*] - . simp [*] - simp_all + . -- TODO: simp[*] fails: "(deterministic) timeout at 'whnf'" + simp [hinv, h_veq] + simp_all end HashMap -- cgit v1.2.3 From 3337c4ac3326c3132dcc322f55f23a7d2054ceb0 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 26 Jul 2023 15:00:11 +0200 Subject: Update some of the Vec function specs --- tests/lean/Hashmap/Properties.lean | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 96b8193d..5d340b5c 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -285,7 +285,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value | none => nhm.len_s = hm.len_s + 1 | some _ => nhm.len_s = hm.len_s) := by rw [insert_no_resize] - simp [hash_key] + simp only [hash_key, bind_tc_ret] -- TODO: annoying have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint intro simp_all [inv] @@ -297,10 +297,9 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value simp [hinv] -- TODO: we want to automate that simp [*, Int.emod_lt_of_pos] - -- have h := Primitives.Vec.index_mut_spec hm.slots hash_mod -- TODO: change the spec of Vec.index_mut to introduce a let-binding. -- or: make progress introduce the let-binding by itself (this is clearer) - progress + progress as ⟨ l, h_leq ⟩ -- TODO: make progress use the names written in the goal progress as ⟨ inserted ⟩ rw [if_update_eq] -- TODO: necessary because we don't have a join @@ -311,38 +310,42 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value := by if inserted then simp [*] - have : hm.num_entries.val + (Usize.ofInt 1).val ≤ Usize.max := by + have hbounds : hm.num_entries.val + (Usize.ofInt 1).val ≤ Usize.max := by simp [lookup] at hnsat simp_all simp [inv] at hinv int_tac - progress - simp_all + -- TODO: progress fails in command line mode with "index out of bounds" + -- and I have no idea how to fix this. The error happens after progress + -- introduced the new goals. It must be when we exit the "withApp", etc. + -- helpers. + have ⟨ z, hp ⟩ := Usize.add_spec hbounds + simp [hp] else - simp_all [Pure.pure] + simp [*, Pure.pure] progress as ⟨ i0 ⟩ -- TODO: progress "eager" to match premises with assumptions while instantiating -- meta-variables - have h_slot : slot_s_inv_hash hm.slots.length (hash_mod_key key hm.slots.length) - (List.v (List.index (hm.slots.val) hash_mod.val)) := by + have h_slot : slot_s_inv_hash hm.slots.length (hash_mod_key key hm.slots.length) l.v + := by simp [inv] at hinv have h := (hinv.right.left hash_mod.val (by assumption) (by assumption)).right simp [slot_t_inv, hhm] at h - simp [h, hhm] - have hd : distinct_keys (hm.slots.v.index hash_mod.val).v := by checkpoint + simp [h, hhm, h_leq] + have hd : distinct_keys l.v := by checkpoint simp [inv, slots_t_inv, slot_t_inv] at hinv have h := hinv.right.left hash_mod.val (by assumption) (by assumption) - simp [h] + simp [h, h_leq] -- TODO: hide the variables and only keep the props -- TODO: allow providing terms to progress to instantiate the meta variables -- which are not propositions progress as ⟨ l0, _, _, _, hlen .. ⟩ - -- Finishing the proof progress keep hv as ⟨ v, h_veq ⟩ -- TODO: update progress to automate that let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v } exists nhm - -- TODO: later I don't want to inline nhm - we need to control simp + -- TODO: later I don't want to inline nhm - we need to control simp: deactivate + -- zeta reduction? have hupdt : lookup nhm key = some value := by checkpoint simp [lookup, List.lookup] at * simp_all @@ -387,7 +390,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value rename_i heq <;> simp [heq] at hlen <;> -- TODO: canonize addition by default? We need a tactic to simplify arithmetic equalities - -- with addition and substractions ((ℤ, +) is a ring or something - there should exist a tactic + -- with addition and substractions ((ℤ, +) is a group or something - there should exist a tactic -- somewhere in mathlib?) simp [Int.add_assoc, Int.add_comm, Int.add_left_comm] <;> int_tac @@ -403,7 +406,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value . simp [slots_t_inv, slot_t_inv] at * intro i hipos _ have _ := hinv.right.left i hipos (by simp_all) - simp [hhm, h_veq] at * -- TODO: annoying + simp [hhm, h_veq] at * -- TODO: annoying, we do that because simp_all fails below -- We need a case disjunction if h_ieq : i = key.val % _root_.List.len hm.slots.val then -- TODO: simp_all fails: "(deterministic) timeout at 'whnf'" -- cgit v1.2.3 From 31de6eb8a82e17b4113262a18abf61e6233b55df Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 26 Jul 2023 15:00:29 +0200 Subject: Make a minor modification to a hashmap proof --- tests/lean/Hashmap/Properties.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 5d340b5c..ee63a065 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -271,6 +271,10 @@ theorem if_update_eq := by split <;> simp [Pure.pure] +-- TODO: move: small helper +def mk_opaque {α : Sort u} (x : α) : { y : α // y = x} := + ⟨ x, by simp ⟩ + theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α) (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) : ∃ nhm, hm.insert_no_resize α key value = ret nhm ∧ @@ -342,10 +346,10 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value progress as ⟨ l0, _, _, _, hlen .. ⟩ progress keep hv as ⟨ v, h_veq ⟩ -- TODO: update progress to automate that - let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v } - exists nhm -- TODO: later I don't want to inline nhm - we need to control simp: deactivate - -- zeta reduction? + -- zeta reduction? For now I have to do this peculiar manipulation + have ⟨ nhm, nhm_eq ⟩ := @mk_opaque (HashMap α) { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v } + exists nhm have hupdt : lookup nhm key = some value := by checkpoint simp [lookup, List.lookup] at * simp_all @@ -406,7 +410,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value . simp [slots_t_inv, slot_t_inv] at * intro i hipos _ have _ := hinv.right.left i hipos (by simp_all) - simp [hhm, h_veq] at * -- TODO: annoying, we do that because simp_all fails below + simp [hhm, h_veq, nhm_eq] at * -- TODO: annoying, we do that because simp_all fails below -- We need a case disjunction if h_ieq : i = key.val % _root_.List.len hm.slots.val then -- TODO: simp_all fails: "(deterministic) timeout at 'whnf'" @@ -419,7 +423,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value else simp [*] . -- TODO: simp[*] fails: "(deterministic) timeout at 'whnf'" - simp [hinv, h_veq] + simp [hinv, h_veq, nhm_eq] simp_all end HashMap -- cgit v1.2.3 From 42551283ecab981b9bb646cab2e8da5491d71b17 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 26 Jul 2023 15:07:09 +0200 Subject: Make minor modifications --- tests/lean/Hashmap/Properties.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index ee63a065..e1bd8669 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -271,7 +271,8 @@ theorem if_update_eq := by split <;> simp [Pure.pure] --- TODO: move: small helper +-- Small helper +-- TODO: move, and introduce a better solution with nice syntax def mk_opaque {α : Sort u} (x : α) : { y : α // y = x} := ⟨ x, by simp ⟩ @@ -328,8 +329,6 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value else simp [*, Pure.pure] progress as ⟨ i0 ⟩ - -- TODO: progress "eager" to match premises with assumptions while instantiating - -- meta-variables have h_slot : slot_s_inv_hash hm.slots.length (hash_mod_key key hm.slots.length) l.v := by simp [inv] at hinv -- cgit v1.2.3 From 9b3a58e423333fc9a4a5a264c3beb0a3d951e86b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 31 Jul 2023 15:56:52 +0200 Subject: Make minor modifications --- tests/lean/Hashmap/Properties.lean | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'tests/lean/Hashmap') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index e1bd8669..3652f608 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -276,6 +276,14 @@ theorem if_update_eq def mk_opaque {α : Sort u} (x : α) : { y : α // y = x} := ⟨ x, by simp ⟩ +--set_option profiler true +--set_option profiler.threshold 10 +--set_option trace.profiler true + +-- For pretty printing (useful when copy-pasting goals) +attribute [pp_dot] List.length -- use the dot notation when printing +set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse) + theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α) (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) : ∃ nhm, hm.insert_no_resize α key value = ret nhm ∧ @@ -324,6 +332,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value -- and I have no idea how to fix this. The error happens after progress -- introduced the new goals. It must be when we exit the "withApp", etc. -- helpers. + -- progress as ⟨ z, hp ⟩ have ⟨ z, hp ⟩ := Usize.add_spec hbounds simp [hp] else -- cgit v1.2.3