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/HashmapMain/Funs.lean | 557 +++++++++++++++++++++++++++++++++++++ tests/lean/HashmapMain/Opaque.lean | 16 ++ tests/lean/HashmapMain/Types.lean | 20 ++ 3 files changed, 593 insertions(+) create mode 100644 tests/lean/HashmapMain/Funs.lean create mode 100644 tests/lean/HashmapMain/Opaque.lean create mode 100644 tests/lean/HashmapMain/Types.lean (limited to 'tests/lean/HashmapMain') diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean new file mode 100644 index 00000000..a59a9f26 --- /dev/null +++ b/tests/lean/HashmapMain/Funs.lean @@ -0,0 +1,557 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: function definitions +import Base +import HashmapMain.Types +import HashmapMain.ExternalFuns +open Primitives + +/- [hashmap_main::hashmap::hash_key] -/ +def hashmap_hash_key_fwd (k : Usize) : Result Usize := + Result.ret k + +/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ +divergent def hashmap_hash_map_allocate_slots_loop_fwd + (T : Type) (slots : Vec (hashmap_list_t T)) (n : Usize) : + Result (Vec (hashmap_list_t T)) + := + if n > (Usize.ofInt 0 (by intlit)) + then + do + let slots0 ← vec_push_back (hashmap_list_t T) slots hashmap_list_t.Nil + let n0 ← n - (Usize.ofInt 1 (by intlit)) + hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 + else Result.ret slots + +/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ +def hashmap_hash_map_allocate_slots_fwd + (T : Type) (slots : Vec (hashmap_list_t T)) (n : Usize) : + Result (Vec (hashmap_list_t T)) + := + hashmap_hash_map_allocate_slots_loop_fwd T slots n + +/- [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] -/ +def hashmap_hash_map_new_with_capacity_fwd + (T : Type) (capacity : Usize) (max_load_dividend : Usize) + (max_load_divisor : Usize) : + Result (hashmap_hash_map_t T) + := + do + let v := vec_new (hashmap_list_t T) + let slots ← hashmap_hash_map_allocate_slots_fwd T v capacity + let i ← capacity * max_load_dividend + let i0 ← i / max_load_divisor + Result.ret + { + hashmap_hash_map_num_entries := (Usize.ofInt 0 (by intlit)), + hashmap_hash_map_max_load_factor := + (max_load_dividend, max_load_divisor), + hashmap_hash_map_max_load := i0, + hashmap_hash_map_slots := slots + } + +/- [hashmap_main::hashmap::HashMap::{0}::new] -/ +def hashmap_hash_map_new_fwd (T : Type) : Result (hashmap_hash_map_t T) := + hashmap_hash_map_new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) + (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) + +/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ +divergent def hashmap_hash_map_clear_loop_fwd_back + (T : Type) (slots : Vec (hashmap_list_t T)) (i : Usize) : + Result (Vec (hashmap_list_t T)) + := + let i0 := vec_len (hashmap_list_t T) slots + if i < i0 + then + do + let i1 ← i + (Usize.ofInt 1 (by intlit)) + let slots0 ← + vec_index_mut_back (hashmap_list_t T) slots i hashmap_list_t.Nil + hashmap_hash_map_clear_loop_fwd_back T slots0 i1 + else Result.ret slots + +/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ +def hashmap_hash_map_clear_fwd_back + (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := + do + let v ← + hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots + (Usize.ofInt 0 (by intlit)) + Result.ret + { + self + with + hashmap_hash_map_num_entries := (Usize.ofInt 0 (by intlit)), + hashmap_hash_map_slots := v + } + +/- [hashmap_main::hashmap::HashMap::{0}::len] -/ +def hashmap_hash_map_len_fwd + (T : Type) (self : hashmap_hash_map_t T) : Result Usize := + Result.ret self.hashmap_hash_map_num_entries + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ +divergent def hashmap_hash_map_insert_in_list_loop_fwd + (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool := + match h: ls with + | hashmap_list_t.Cons ckey cvalue tl => + if ckey = key + then Result.ret false + else hashmap_hash_map_insert_in_list_loop_fwd T key value tl + | hashmap_list_t.Nil => Result.ret true + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ +def hashmap_hash_map_insert_in_list_fwd + (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool := + hashmap_hash_map_insert_in_list_loop_fwd T key value ls + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ +divergent def hashmap_hash_map_insert_in_list_loop_back + (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : + Result (hashmap_list_t T) + := + match h: ls with + | hashmap_list_t.Cons ckey cvalue tl => + if ckey = key + then Result.ret (hashmap_list_t.Cons ckey value tl) + else + do + let tl0 ← hashmap_hash_map_insert_in_list_loop_back T key value tl + Result.ret (hashmap_list_t.Cons ckey cvalue tl0) + | hashmap_list_t.Nil => + let l := hashmap_list_t.Nil + Result.ret (hashmap_list_t.Cons key value l) + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ +def hashmap_hash_map_insert_in_list_back + (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : + Result (hashmap_list_t T) + := + hashmap_hash_map_insert_in_list_loop_back T key value ls + +/- [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] -/ +def hashmap_hash_map_insert_no_resize_fwd_back + (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (value : T) : + Result (hashmap_hash_map_t T) + := + do + let hash ← hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod ← hash % i + let l ← + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let inserted ← hashmap_hash_map_insert_in_list_fwd T key value l + if inserted + then + do + let i0 ← self.hashmap_hash_map_num_entries + + (Usize.ofInt 1 (by intlit)) + let l0 ← hashmap_hash_map_insert_in_list_back T key value l + let v ← + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + Result.ret + { + self + with + hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v + } + else + do + let l0 ← hashmap_hash_map_insert_in_list_back T key value l + let v ← + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + Result.ret { self with hashmap_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_main::hashmap::HashMap::{0}::move_elements_from_list] -/ +divergent def hashmap_hash_map_move_elements_from_list_loop_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : + Result (hashmap_hash_map_t T) + := + match h: ls with + | hashmap_list_t.Cons k v tl => + do + let ntable0 ← hashmap_hash_map_insert_no_resize_fwd_back T ntable k v + hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl + | hashmap_list_t.Nil => Result.ret ntable + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ +def hashmap_hash_map_move_elements_from_list_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : + Result (hashmap_hash_map_t T) + := + hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable ls + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ +divergent def hashmap_hash_map_move_elements_loop_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) + (i : Usize) : + Result ((hashmap_hash_map_t T) × (Vec (hashmap_list_t T))) + := + let i0 := vec_len (hashmap_list_t T) slots + if i < i0 + then + do + let l ← vec_index_mut_fwd (hashmap_list_t T) slots i + let ls := mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.Nil + let ntable0 ← + hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls + let i1 ← i + (Usize.ofInt 1 (by intlit)) + let l0 := mem_replace_back (hashmap_list_t T) l hashmap_list_t.Nil + let slots0 ← vec_index_mut_back (hashmap_list_t T) slots i l0 + hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 + else Result.ret (ntable, slots) + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ +def hashmap_hash_map_move_elements_fwd_back + (T : Type) (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) + (i : Usize) : + Result ((hashmap_hash_map_t T) × (Vec (hashmap_list_t T))) + := + hashmap_hash_map_move_elements_loop_fwd_back T ntable slots i + +/- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ +def hashmap_hash_map_try_resize_fwd_back + (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := + do + let max_usize ← Scalar.cast .Usize core_num_u32_max_c + let capacity := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) + let (i, i0) := self.hashmap_hash_map_max_load_factor + let i1 ← n1 / i + if capacity <= i1 + then + do + let i2 ← capacity * (Usize.ofInt 2 (by intlit)) + let ntable ← hashmap_hash_map_new_with_capacity_fwd T i2 i i0 + let (ntable0, _) ← + hashmap_hash_map_move_elements_fwd_back T ntable + self.hashmap_hash_map_slots (Usize.ofInt 0 (by intlit)) + Result.ret + { + ntable0 + with + hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, + hashmap_hash_map_max_load_factor := (i, i0) + } + else Result.ret { self with hashmap_hash_map_max_load_factor := (i, i0) } + +/- [hashmap_main::hashmap::HashMap::{0}::insert] -/ +def hashmap_hash_map_insert_fwd_back + (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (value : T) : + Result (hashmap_hash_map_t T) + := + do + let self0 ← hashmap_hash_map_insert_no_resize_fwd_back T self key value + let i ← hashmap_hash_map_len_fwd T self0 + if i > self0.hashmap_hash_map_max_load + then hashmap_hash_map_try_resize_fwd_back T self0 + else Result.ret self0 + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ +divergent def hashmap_hash_map_contains_key_in_list_loop_fwd + (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool := + match h: ls with + | hashmap_list_t.Cons ckey t tl => + if ckey = key + then Result.ret true + else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl + | hashmap_list_t.Nil => Result.ret false + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ +def hashmap_hash_map_contains_key_in_list_fwd + (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool := + hashmap_hash_map_contains_key_in_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ +def hashmap_hash_map_contains_key_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result Bool := + do + let hash ← hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod ← hash % i + let l ← + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + hashmap_hash_map_contains_key_in_list_fwd T key l + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ +divergent def hashmap_hash_map_get_in_list_loop_fwd + (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T := + match h: ls with + | hashmap_list_t.Cons ckey cvalue tl => + if ckey = key + then Result.ret cvalue + else hashmap_hash_map_get_in_list_loop_fwd T key tl + | hashmap_list_t.Nil => Result.fail Error.panic + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ +def hashmap_hash_map_get_in_list_fwd + (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T := + hashmap_hash_map_get_in_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::get] -/ +def hashmap_hash_map_get_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result T := + do + let hash ← hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod ← hash % i + let l ← + vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + hashmap_hash_map_get_in_list_fwd T key l + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +divergent def hashmap_hash_map_get_mut_in_list_loop_fwd + (T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T := + match h: ls with + | hashmap_list_t.Cons ckey cvalue tl => + if ckey = key + then Result.ret cvalue + else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key + | hashmap_list_t.Nil => Result.fail Error.panic + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_fwd + (T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T := + hashmap_hash_map_get_mut_in_list_loop_fwd T ls key + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +divergent def hashmap_hash_map_get_mut_in_list_loop_back + (T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) : + Result (hashmap_list_t T) + := + match h: ls with + | hashmap_list_t.Cons ckey cvalue tl => + if ckey = key + then Result.ret (hashmap_list_t.Cons ckey ret0 tl) + else + do + let tl0 ← hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 + Result.ret (hashmap_list_t.Cons ckey cvalue tl0) + | hashmap_list_t.Nil => Result.fail Error.panic + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +def hashmap_hash_map_get_mut_in_list_back + (T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) : + Result (hashmap_list_t T) + := + hashmap_hash_map_get_mut_in_list_loop_back T ls key ret0 + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ +def hashmap_hash_map_get_mut_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result T := + do + let hash ← hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod ← hash % i + let l ← + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + hashmap_hash_map_get_mut_in_list_fwd T l key + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ +def hashmap_hash_map_get_mut_back + (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (ret0 : T) : + Result (hashmap_hash_map_t T) + := + do + let hash ← hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod ← hash % i + let l ← + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let l0 ← hashmap_hash_map_get_mut_in_list_back T l key ret0 + let v ← + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + Result.ret { self with hashmap_hash_map_slots := v } + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +divergent def hashmap_hash_map_remove_from_list_loop_fwd + (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) := + match h: ls with + | hashmap_list_t.Cons ckey t tl => + if ckey = key + then + let mv_ls := + mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl) + hashmap_list_t.Nil + match h: mv_ls with + | hashmap_list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | hashmap_list_t.Nil => Result.fail Error.panic + else hashmap_hash_map_remove_from_list_loop_fwd T key tl + | hashmap_list_t.Nil => Result.ret Option.none + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_fwd + (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) := + hashmap_hash_map_remove_from_list_loop_fwd T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +divergent def hashmap_hash_map_remove_from_list_loop_back + (T : Type) (key : Usize) (ls : hashmap_list_t T) : + Result (hashmap_list_t T) + := + match h: ls with + | hashmap_list_t.Cons ckey t tl => + if ckey = key + then + let mv_ls := + mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl) + hashmap_list_t.Nil + match h: mv_ls with + | hashmap_list_t.Cons i cvalue tl0 => Result.ret tl0 + | hashmap_list_t.Nil => Result.fail Error.panic + else + do + let tl0 ← hashmap_hash_map_remove_from_list_loop_back T key tl + Result.ret (hashmap_list_t.Cons ckey t tl0) + | hashmap_list_t.Nil => Result.ret hashmap_list_t.Nil + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +def hashmap_hash_map_remove_from_list_back + (T : Type) (key : Usize) (ls : hashmap_list_t T) : + Result (hashmap_list_t T) + := + hashmap_hash_map_remove_from_list_loop_back T key ls + +/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ +def hashmap_hash_map_remove_fwd + (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result (Option T) := + do + let hash ← hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod ← hash % i + let l ← + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let x ← hashmap_hash_map_remove_from_list_fwd T key l + match h: x with + | Option.none => Result.ret Option.none + | Option.some x0 => + do + let _ ← self.hashmap_hash_map_num_entries - + (Usize.ofInt 1 (by intlit)) + Result.ret (Option.some x0) + +/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ +def hashmap_hash_map_remove_back + (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : + Result (hashmap_hash_map_t T) + := + do + let hash ← hashmap_hash_key_fwd key + let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let hash_mod ← hash % i + let l ← + vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + let x ← hashmap_hash_map_remove_from_list_fwd T key l + match h: x with + | Option.none => + do + let l0 ← hashmap_hash_map_remove_from_list_back T key l + let v ← + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + Result.ret { self with hashmap_hash_map_slots := v } + | Option.some x0 => + do + let i0 ← self.hashmap_hash_map_num_entries - + (Usize.ofInt 1 (by intlit)) + let l0 ← hashmap_hash_map_remove_from_list_back T key l + let v ← + vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + hash_mod l0 + Result.ret + { + self + with + hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v + } + +/- [hashmap_main::hashmap::test1] -/ +def hashmap_test1_fwd : Result Unit := + do + let hm ← hashmap_hash_map_new_fwd U64 + let hm0 ← + hashmap_hash_map_insert_fwd_back U64 hm (Usize.ofInt 0 (by intlit)) + (U64.ofInt 42 (by intlit)) + let hm1 ← + hashmap_hash_map_insert_fwd_back U64 hm0 (Usize.ofInt 128 (by intlit)) + (U64.ofInt 18 (by intlit)) + let hm2 ← + hashmap_hash_map_insert_fwd_back U64 hm1 (Usize.ofInt 1024 (by intlit)) + (U64.ofInt 138 (by intlit)) + let hm3 ← + hashmap_hash_map_insert_fwd_back U64 hm2 (Usize.ofInt 1056 (by intlit)) + (U64.ofInt 256 (by intlit)) + let i ← hashmap_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 ← + hashmap_hash_map_get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit)) + (U64.ofInt 56 (by intlit)) + let i0 ← + hashmap_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 ← + hashmap_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 ← + hashmap_hash_map_remove_back U64 hm4 + (Usize.ofInt 1024 (by intlit)) + let i1 ← + hashmap_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 ← + hashmap_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 ← + hashmap_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_main::hashmap::test1] -/ +#assert (hashmap_test1_fwd == .ret ()) + +/- [hashmap_main::insert_on_disk] -/ +def insert_on_disk_fwd + (key : Usize) (value : U64) (st : State) : Result (State × Unit) := + do + let (st0, hm) ← opaque_defs.hashmap_utils_deserialize_fwd st + let hm0 ← hashmap_hash_map_insert_fwd_back U64 hm key value + let (st1, _) ← opaque_defs.hashmap_utils_serialize_fwd hm0 st0 + Result.ret (st1, ()) + +/- [hashmap_main::main] -/ +def main_fwd : Result Unit := + Result.ret () + +/- Unit test for [hashmap_main::main] -/ +#assert (main_fwd == .ret ()) + diff --git a/tests/lean/HashmapMain/Opaque.lean b/tests/lean/HashmapMain/Opaque.lean new file mode 100644 index 00000000..bef4f3fb --- /dev/null +++ b/tests/lean/HashmapMain/Opaque.lean @@ -0,0 +1,16 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: opaque function definitions +import Base +import HashmapMain.Types +open Primitives + +structure OpaqueDefs where + + /- [hashmap_main::hashmap_utils::deserialize] -/ + hashmap_utils_deserialize_fwd + : State -> Result (State × (hashmap_hash_map_t U64)) + + /- [hashmap_main::hashmap_utils::serialize] -/ + hashmap_utils_serialize_fwd + : hashmap_hash_map_t U64 -> State -> Result (State × Unit) + diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean new file mode 100644 index 00000000..858e1c51 --- /dev/null +++ b/tests/lean/HashmapMain/Types.lean @@ -0,0 +1,20 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: type definitions +import Base +open Primitives + +/- [hashmap_main::hashmap::List] -/ +inductive hashmap_list_t (T : Type) := +| Cons : Usize -> T -> hashmap_list_t T -> hashmap_list_t T +| Nil : hashmap_list_t T + +/- [hashmap_main::hashmap::HashMap] -/ +structure hashmap_hash_map_t (T : Type) where + hashmap_hash_map_num_entries : Usize + hashmap_hash_map_max_load_factor : (Usize × Usize) + hashmap_hash_map_max_load : Usize + hashmap_hash_map_slots : Vec (hashmap_list_t T) + +/- The state type used in the state-error monad -/ +axiom State : Type + -- 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/HashmapMain/ExternalFuns.lean | 9 +++++++++ tests/lean/HashmapMain/Funs.lean | 31 +++++++++++++++++-------------- tests/lean/HashmapMain/Opaque.lean | 7 +++++-- tests/lean/HashmapMain/Types.lean | 5 ++++- 4 files changed, 35 insertions(+), 17 deletions(-) create mode 100644 tests/lean/HashmapMain/ExternalFuns.lean (limited to 'tests/lean/HashmapMain') diff --git a/tests/lean/HashmapMain/ExternalFuns.lean b/tests/lean/HashmapMain/ExternalFuns.lean new file mode 100644 index 00000000..bc831158 --- /dev/null +++ b/tests/lean/HashmapMain/ExternalFuns.lean @@ -0,0 +1,9 @@ +import Base +import HashmapMain.Types +import HashmapMain.Opaque + +namespace HashmapMain + +def opaque_defs : OpaqueDefs := by sorry + +end HashmapMain diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index a59a9f26..34a0eca1 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -5,6 +5,8 @@ import HashmapMain.Types import HashmapMain.ExternalFuns open Primitives +namespace HashmapMain + /- [hashmap_main::hashmap::hash_key] -/ def hashmap_hash_key_fwd (k : Usize) : Result Usize := Result.ret k @@ -92,7 +94,7 @@ def hashmap_hash_map_len_fwd /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ divergent def hashmap_hash_map_insert_in_list_loop_fwd (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool := - match h: ls with + match ls with | hashmap_list_t.Cons ckey cvalue tl => if ckey = key then Result.ret false @@ -109,7 +111,7 @@ divergent def hashmap_hash_map_insert_in_list_loop_back (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result (hashmap_list_t T) := - match h: ls with + match ls with | hashmap_list_t.Cons ckey cvalue tl => if ckey = key then Result.ret (hashmap_list_t.Cons ckey value tl) @@ -173,7 +175,7 @@ divergent def hashmap_hash_map_move_elements_from_list_loop_fwd_back (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : Result (hashmap_hash_map_t T) := - match h: ls with + match ls with | hashmap_list_t.Cons k v tl => do let ntable0 ← hashmap_hash_map_insert_no_resize_fwd_back T ntable k v @@ -256,7 +258,7 @@ def hashmap_hash_map_insert_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ divergent def hashmap_hash_map_contains_key_in_list_loop_fwd (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool := - match h: ls with + match ls with | hashmap_list_t.Cons ckey t tl => if ckey = key then Result.ret true @@ -282,7 +284,7 @@ def hashmap_hash_map_contains_key_fwd /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ divergent def hashmap_hash_map_get_in_list_loop_fwd (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T := - match h: ls with + match ls with | hashmap_list_t.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue @@ -308,7 +310,7 @@ def hashmap_hash_map_get_fwd /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def hashmap_hash_map_get_mut_in_list_loop_fwd (T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T := - match h: ls with + match ls with | hashmap_list_t.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue @@ -325,7 +327,7 @@ divergent def hashmap_hash_map_get_mut_in_list_loop_back (T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) : Result (hashmap_list_t T) := - match h: ls with + match ls with | hashmap_list_t.Cons ckey cvalue tl => if ckey = key then Result.ret (hashmap_list_t.Cons ckey ret0 tl) @@ -373,14 +375,14 @@ def hashmap_hash_map_get_mut_back /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ divergent def hashmap_hash_map_remove_from_list_loop_fwd (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) := - match h: ls with + match ls with | hashmap_list_t.Cons ckey t tl => if ckey = key then let mv_ls := mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl) hashmap_list_t.Nil - match h: mv_ls with + match mv_ls with | hashmap_list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) | hashmap_list_t.Nil => Result.fail Error.panic else hashmap_hash_map_remove_from_list_loop_fwd T key tl @@ -396,14 +398,14 @@ divergent def hashmap_hash_map_remove_from_list_loop_back (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (hashmap_list_t T) := - match h: ls with + match ls with | hashmap_list_t.Cons ckey t tl => if ckey = key then let mv_ls := mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl) hashmap_list_t.Nil - match h: mv_ls with + match mv_ls with | hashmap_list_t.Cons i cvalue tl0 => Result.ret tl0 | hashmap_list_t.Nil => Result.fail Error.panic else @@ -429,7 +431,7 @@ def hashmap_hash_map_remove_fwd let l ← vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod let x ← hashmap_hash_map_remove_from_list_fwd T key l - match h: x with + match x with | Option.none => Result.ret Option.none | Option.some x0 => do @@ -449,7 +451,7 @@ def hashmap_hash_map_remove_back let l ← vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod let x ← hashmap_hash_map_remove_from_list_fwd T key l - match h: x with + match x with | Option.none => do let l0 ← hashmap_hash_map_remove_from_list_back T key l @@ -505,7 +507,7 @@ def hashmap_test1_fwd : Result Unit := let x ← hashmap_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))) @@ -555,3 +557,4 @@ def main_fwd : Result Unit := /- Unit test for [hashmap_main::main] -/ #assert (main_fwd == .ret ()) +end HashmapMain diff --git a/tests/lean/HashmapMain/Opaque.lean b/tests/lean/HashmapMain/Opaque.lean index bef4f3fb..10e4d8bd 100644 --- a/tests/lean/HashmapMain/Opaque.lean +++ b/tests/lean/HashmapMain/Opaque.lean @@ -4,13 +4,16 @@ import Base import HashmapMain.Types open Primitives +namespace HashmapMain + structure OpaqueDefs where /- [hashmap_main::hashmap_utils::deserialize] -/ hashmap_utils_deserialize_fwd - : State -> Result (State × (hashmap_hash_map_t U64)) + : State → Result (State × (hashmap_hash_map_t U64)) /- [hashmap_main::hashmap_utils::serialize] -/ hashmap_utils_serialize_fwd - : hashmap_hash_map_t U64 -> State -> Result (State × Unit) + : hashmap_hash_map_t U64 → State → Result (State × Unit) +end HashmapMain diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean index 858e1c51..b91ff3a7 100644 --- a/tests/lean/HashmapMain/Types.lean +++ b/tests/lean/HashmapMain/Types.lean @@ -3,9 +3,11 @@ import Base open Primitives +namespace HashmapMain + /- [hashmap_main::hashmap::List] -/ inductive hashmap_list_t (T : Type) := -| Cons : Usize -> T -> hashmap_list_t T -> hashmap_list_t T +| Cons : Usize → T → hashmap_list_t T → hashmap_list_t T | Nil : hashmap_list_t T /- [hashmap_main::hashmap::HashMap] -/ @@ -18,3 +20,4 @@ structure hashmap_hash_map_t (T : Type) where /- The state type used in the state-error monad -/ axiom State : Type +end HashmapMain -- 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/HashmapMain/ExternalFuns.lean | 9 - tests/lean/HashmapMain/Funs.lean | 221 +++++++++++----------- tests/lean/HashmapMain/FunsExternal.lean | 17 ++ tests/lean/HashmapMain/FunsExternal_Template.lean | 16 ++ tests/lean/HashmapMain/Opaque.lean | 8 +- tests/lean/HashmapMain/Types.lean | 5 +- 6 files changed, 148 insertions(+), 128 deletions(-) delete mode 100644 tests/lean/HashmapMain/ExternalFuns.lean create mode 100644 tests/lean/HashmapMain/FunsExternal.lean create mode 100644 tests/lean/HashmapMain/FunsExternal_Template.lean (limited to 'tests/lean/HashmapMain') diff --git a/tests/lean/HashmapMain/ExternalFuns.lean b/tests/lean/HashmapMain/ExternalFuns.lean deleted file mode 100644 index bc831158..00000000 --- a/tests/lean/HashmapMain/ExternalFuns.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Base -import HashmapMain.Types -import HashmapMain.Opaque - -namespace HashmapMain - -def opaque_defs : OpaqueDefs := by sorry - -end HashmapMain diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index 34a0eca1..06929431 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -2,17 +2,16 @@ -- [hashmap_main]: function definitions import Base import HashmapMain.Types -import HashmapMain.ExternalFuns +import HashmapMain.FunsExternal open Primitives - -namespace HashmapMain +namespace hashmap_main /- [hashmap_main::hashmap::hash_key] -/ -def hashmap_hash_key_fwd (k : Usize) : Result Usize := +def hashmap.hash_key_fwd (k : Usize) : Result Usize := Result.ret k /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ -divergent def hashmap_hash_map_allocate_slots_loop_fwd +divergent def hashmap.HashMap.allocate_slots_loop_fwd (T : Type) (slots : Vec (hashmap_list_t T)) (n : Usize) : Result (Vec (hashmap_list_t T)) := @@ -21,25 +20,25 @@ divergent def hashmap_hash_map_allocate_slots_loop_fwd do let slots0 ← vec_push_back (hashmap_list_t T) slots hashmap_list_t.Nil let n0 ← n - (Usize.ofInt 1 (by intlit)) - hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 + hashmap.HashMap.allocate_slots_loop_fwd T slots0 n0 else Result.ret slots /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ -def hashmap_hash_map_allocate_slots_fwd +def hashmap.HashMap.allocate_slots_fwd (T : Type) (slots : Vec (hashmap_list_t T)) (n : Usize) : Result (Vec (hashmap_list_t T)) := - hashmap_hash_map_allocate_slots_loop_fwd T slots n + hashmap.HashMap.allocate_slots_loop_fwd T slots n /- [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] -/ -def hashmap_hash_map_new_with_capacity_fwd +def hashmap.HashMap.new_with_capacity_fwd (T : Type) (capacity : Usize) (max_load_dividend : Usize) (max_load_divisor : Usize) : Result (hashmap_hash_map_t T) := do let v := vec_new (hashmap_list_t T) - let slots ← hashmap_hash_map_allocate_slots_fwd T v capacity + let slots ← hashmap.HashMap.allocate_slots_fwd T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor Result.ret @@ -52,12 +51,12 @@ def hashmap_hash_map_new_with_capacity_fwd } /- [hashmap_main::hashmap::HashMap::{0}::new] -/ -def hashmap_hash_map_new_fwd (T : Type) : Result (hashmap_hash_map_t T) := - hashmap_hash_map_new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) +def hashmap.HashMap.new_fwd (T : Type) : Result (hashmap_hash_map_t T) := + hashmap.HashMap.new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ -divergent def hashmap_hash_map_clear_loop_fwd_back +divergent def hashmap.HashMap.clear_loop_fwd_back (T : Type) (slots : Vec (hashmap_list_t T)) (i : Usize) : Result (Vec (hashmap_list_t T)) := @@ -68,15 +67,15 @@ divergent def hashmap_hash_map_clear_loop_fwd_back let i1 ← i + (Usize.ofInt 1 (by intlit)) let slots0 ← vec_index_mut_back (hashmap_list_t T) slots i hashmap_list_t.Nil - hashmap_hash_map_clear_loop_fwd_back T slots0 i1 + hashmap.HashMap.clear_loop_fwd_back T slots0 i1 else Result.ret slots /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ -def hashmap_hash_map_clear_fwd_back +def hashmap.HashMap.clear_fwd_back (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := do let v ← - hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots + hashmap.HashMap.clear_loop_fwd_back T self.hashmap_hash_map_slots (Usize.ofInt 0 (by intlit)) Result.ret { @@ -87,27 +86,27 @@ def hashmap_hash_map_clear_fwd_back } /- [hashmap_main::hashmap::HashMap::{0}::len] -/ -def hashmap_hash_map_len_fwd +def hashmap.HashMap.len_fwd (T : Type) (self : hashmap_hash_map_t T) : Result Usize := Result.ret self.hashmap_hash_map_num_entries /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ -divergent def hashmap_hash_map_insert_in_list_loop_fwd +divergent def hashmap.HashMap.insert_in_list_loop_fwd (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool := match ls with | hashmap_list_t.Cons ckey cvalue tl => if ckey = key then Result.ret false - else hashmap_hash_map_insert_in_list_loop_fwd T key value tl + else hashmap.HashMap.insert_in_list_loop_fwd T key value tl | hashmap_list_t.Nil => Result.ret true /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ -def hashmap_hash_map_insert_in_list_fwd +def hashmap.HashMap.insert_in_list_fwd (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool := - hashmap_hash_map_insert_in_list_loop_fwd T key value ls + hashmap.HashMap.insert_in_list_loop_fwd T key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ -divergent def hashmap_hash_map_insert_in_list_loop_back +divergent def hashmap.HashMap.insert_in_list_loop_back (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result (hashmap_list_t T) := @@ -117,37 +116,37 @@ divergent def hashmap_hash_map_insert_in_list_loop_back then Result.ret (hashmap_list_t.Cons ckey value tl) else do - let tl0 ← hashmap_hash_map_insert_in_list_loop_back T key value tl + let tl0 ← hashmap.HashMap.insert_in_list_loop_back T key value tl Result.ret (hashmap_list_t.Cons ckey cvalue tl0) | hashmap_list_t.Nil => let l := hashmap_list_t.Nil Result.ret (hashmap_list_t.Cons key value l) /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ -def hashmap_hash_map_insert_in_list_back +def hashmap.HashMap.insert_in_list_back (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result (hashmap_list_t T) := - hashmap_hash_map_insert_in_list_loop_back T key value ls + hashmap.HashMap.insert_in_list_loop_back T key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] -/ -def hashmap_hash_map_insert_no_resize_fwd_back +def hashmap.HashMap.insert_no_resize_fwd_back (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (value : T) : Result (hashmap_hash_map_t T) := do - let hash ← hashmap_hash_key_fwd key + let hash ← hashmap.hash_key_fwd key let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - let inserted ← hashmap_hash_map_insert_in_list_fwd T key value l + let inserted ← hashmap.HashMap.insert_in_list_fwd T key value l if inserted then do let i0 ← self.hashmap_hash_map_num_entries + (Usize.ofInt 1 (by intlit)) - let l0 ← hashmap_hash_map_insert_in_list_back T key value l + let l0 ← hashmap.HashMap.insert_in_list_back T key value l let v ← vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 @@ -159,7 +158,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back } else do - let l0 ← hashmap_hash_map_insert_in_list_back T key value l + let l0 ← hashmap.HashMap.insert_in_list_back T key value l let v ← vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 @@ -171,26 +170,26 @@ 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_main::hashmap::HashMap::{0}::move_elements_from_list] -/ -divergent def hashmap_hash_map_move_elements_from_list_loop_fwd_back +divergent def hashmap.HashMap.move_elements_from_list_loop_fwd_back (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : Result (hashmap_hash_map_t T) := match ls with | hashmap_list_t.Cons k v tl => do - let ntable0 ← hashmap_hash_map_insert_no_resize_fwd_back T ntable k v - hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl + let ntable0 ← hashmap.HashMap.insert_no_resize_fwd_back T ntable k v + hashmap.HashMap.move_elements_from_list_loop_fwd_back T ntable0 tl | hashmap_list_t.Nil => Result.ret ntable /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ -def hashmap_hash_map_move_elements_from_list_fwd_back +def hashmap.HashMap.move_elements_from_list_fwd_back (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : Result (hashmap_hash_map_t T) := - hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable ls + hashmap.HashMap.move_elements_from_list_loop_fwd_back T ntable ls /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ -divergent def hashmap_hash_map_move_elements_loop_fwd_back +divergent def hashmap.HashMap.move_elements_loop_fwd_back (T : Type) (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) (i : Usize) : Result ((hashmap_hash_map_t T) × (Vec (hashmap_list_t T))) @@ -202,23 +201,23 @@ divergent def hashmap_hash_map_move_elements_loop_fwd_back let l ← vec_index_mut_fwd (hashmap_list_t T) slots i let ls := mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.Nil let ntable0 ← - hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls + hashmap.HashMap.move_elements_from_list_fwd_back T ntable ls let i1 ← i + (Usize.ofInt 1 (by intlit)) let l0 := mem_replace_back (hashmap_list_t T) l hashmap_list_t.Nil let slots0 ← vec_index_mut_back (hashmap_list_t T) slots i l0 - hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 + hashmap.HashMap.move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ -def hashmap_hash_map_move_elements_fwd_back +def hashmap.HashMap.move_elements_fwd_back (T : Type) (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) (i : Usize) : Result ((hashmap_hash_map_t T) × (Vec (hashmap_list_t T))) := - hashmap_hash_map_move_elements_loop_fwd_back T ntable slots i + hashmap.HashMap.move_elements_loop_fwd_back T ntable slots i /- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ -def hashmap_hash_map_try_resize_fwd_back +def hashmap.HashMap.try_resize_fwd_back (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c @@ -230,9 +229,9 @@ def hashmap_hash_map_try_resize_fwd_back then do let i2 ← capacity * (Usize.ofInt 2 (by intlit)) - let ntable ← hashmap_hash_map_new_with_capacity_fwd T i2 i i0 + let ntable ← hashmap.HashMap.new_with_capacity_fwd T i2 i i0 let (ntable0, _) ← - hashmap_hash_map_move_elements_fwd_back T ntable + hashmap.HashMap.move_elements_fwd_back T ntable self.hashmap_hash_map_slots (Usize.ofInt 0 (by intlit)) Result.ret { @@ -244,86 +243,86 @@ def hashmap_hash_map_try_resize_fwd_back else Result.ret { self with hashmap_hash_map_max_load_factor := (i, i0) } /- [hashmap_main::hashmap::HashMap::{0}::insert] -/ -def hashmap_hash_map_insert_fwd_back +def hashmap.HashMap.insert_fwd_back (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (value : T) : Result (hashmap_hash_map_t T) := do - let self0 ← hashmap_hash_map_insert_no_resize_fwd_back T self key value - let i ← hashmap_hash_map_len_fwd T self0 + let self0 ← hashmap.HashMap.insert_no_resize_fwd_back T self key value + let i ← hashmap.HashMap.len_fwd T self0 if i > self0.hashmap_hash_map_max_load - then hashmap_hash_map_try_resize_fwd_back T self0 + then hashmap.HashMap.try_resize_fwd_back T self0 else Result.ret self0 /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ -divergent def hashmap_hash_map_contains_key_in_list_loop_fwd +divergent def hashmap.HashMap.contains_key_in_list_loop_fwd (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool := match ls with | hashmap_list_t.Cons ckey t tl => if ckey = key then Result.ret true - else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl + else hashmap.HashMap.contains_key_in_list_loop_fwd T key tl | hashmap_list_t.Nil => Result.ret false /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ -def hashmap_hash_map_contains_key_in_list_fwd +def hashmap.HashMap.contains_key_in_list_fwd (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool := - hashmap_hash_map_contains_key_in_list_loop_fwd T key ls + hashmap.HashMap.contains_key_in_list_loop_fwd T key ls /- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ -def hashmap_hash_map_contains_key_fwd +def hashmap.HashMap.contains_key_fwd (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result Bool := do - let hash ← hashmap_hash_key_fwd key + let hash ← hashmap.hash_key_fwd key let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - hashmap_hash_map_contains_key_in_list_fwd T key l + hashmap.HashMap.contains_key_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ -divergent def hashmap_hash_map_get_in_list_loop_fwd +divergent def hashmap.HashMap.get_in_list_loop_fwd (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T := match ls with | hashmap_list_t.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue - else hashmap_hash_map_get_in_list_loop_fwd T key tl + else hashmap.HashMap.get_in_list_loop_fwd T key tl | hashmap_list_t.Nil => Result.fail Error.panic /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ -def hashmap_hash_map_get_in_list_fwd +def hashmap.HashMap.get_in_list_fwd (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T := - hashmap_hash_map_get_in_list_loop_fwd T key ls + hashmap.HashMap.get_in_list_loop_fwd T key ls /- [hashmap_main::hashmap::HashMap::{0}::get] -/ -def hashmap_hash_map_get_fwd +def hashmap.HashMap.get_fwd (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result T := do - let hash ← hashmap_hash_key_fwd key + let hash ← hashmap.hash_key_fwd key let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - hashmap_hash_map_get_in_list_fwd T key l + hashmap.HashMap.get_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -divergent def hashmap_hash_map_get_mut_in_list_loop_fwd +divergent def hashmap.HashMap.get_mut_in_list_loop_fwd (T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T := match ls with | hashmap_list_t.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue - else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key + else hashmap.HashMap.get_mut_in_list_loop_fwd T tl key | hashmap_list_t.Nil => Result.fail Error.panic /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -def hashmap_hash_map_get_mut_in_list_fwd +def hashmap.HashMap.get_mut_in_list_fwd (T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T := - hashmap_hash_map_get_mut_in_list_loop_fwd T ls key + hashmap.HashMap.get_mut_in_list_loop_fwd T ls key /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -divergent def hashmap_hash_map_get_mut_in_list_loop_back +divergent def hashmap.HashMap.get_mut_in_list_loop_back (T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) : Result (hashmap_list_t T) := @@ -333,47 +332,47 @@ divergent def hashmap_hash_map_get_mut_in_list_loop_back then Result.ret (hashmap_list_t.Cons ckey ret0 tl) else do - let tl0 ← hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 + let tl0 ← hashmap.HashMap.get_mut_in_list_loop_back T tl key ret0 Result.ret (hashmap_list_t.Cons ckey cvalue tl0) | hashmap_list_t.Nil => Result.fail Error.panic /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -def hashmap_hash_map_get_mut_in_list_back +def hashmap.HashMap.get_mut_in_list_back (T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) : Result (hashmap_list_t T) := - hashmap_hash_map_get_mut_in_list_loop_back T ls key ret0 + hashmap.HashMap.get_mut_in_list_loop_back T ls key ret0 /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ -def hashmap_hash_map_get_mut_fwd +def hashmap.HashMap.get_mut_fwd (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result T := do - let hash ← hashmap_hash_key_fwd key + let hash ← hashmap.hash_key_fwd key let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - hashmap_hash_map_get_mut_in_list_fwd T l key + hashmap.HashMap.get_mut_in_list_fwd T l key /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ -def hashmap_hash_map_get_mut_back +def hashmap.HashMap.get_mut_back (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (ret0 : T) : Result (hashmap_hash_map_t T) := do - let hash ← hashmap_hash_key_fwd key + let hash ← hashmap.hash_key_fwd key let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - let l0 ← hashmap_hash_map_get_mut_in_list_back T l key ret0 + let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0 let v ← vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { self with hashmap_hash_map_slots := v } /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -divergent def hashmap_hash_map_remove_from_list_loop_fwd +divergent def hashmap.HashMap.remove_from_list_loop_fwd (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) := match ls with | hashmap_list_t.Cons ckey t tl => @@ -385,16 +384,16 @@ divergent def hashmap_hash_map_remove_from_list_loop_fwd match mv_ls with | hashmap_list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) | hashmap_list_t.Nil => Result.fail Error.panic - else hashmap_hash_map_remove_from_list_loop_fwd T key tl + else hashmap.HashMap.remove_from_list_loop_fwd T key tl | hashmap_list_t.Nil => Result.ret Option.none /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -def hashmap_hash_map_remove_from_list_fwd +def hashmap.HashMap.remove_from_list_fwd (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) := - hashmap_hash_map_remove_from_list_loop_fwd T key ls + hashmap.HashMap.remove_from_list_loop_fwd T key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -divergent def hashmap_hash_map_remove_from_list_loop_back +divergent def hashmap.HashMap.remove_from_list_loop_back (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (hashmap_list_t T) := @@ -410,27 +409,27 @@ divergent def hashmap_hash_map_remove_from_list_loop_back | hashmap_list_t.Nil => Result.fail Error.panic else do - let tl0 ← hashmap_hash_map_remove_from_list_loop_back T key tl + let tl0 ← hashmap.HashMap.remove_from_list_loop_back T key tl Result.ret (hashmap_list_t.Cons ckey t tl0) | hashmap_list_t.Nil => Result.ret hashmap_list_t.Nil /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -def hashmap_hash_map_remove_from_list_back +def hashmap.HashMap.remove_from_list_back (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (hashmap_list_t T) := - hashmap_hash_map_remove_from_list_loop_back T key ls + hashmap.HashMap.remove_from_list_loop_back T key ls /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ -def hashmap_hash_map_remove_fwd +def hashmap.HashMap.remove_fwd (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result (Option T) := do - let hash ← hashmap_hash_key_fwd key + let hash ← hashmap.hash_key_fwd key let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - let x ← hashmap_hash_map_remove_from_list_fwd T key l + let x ← hashmap.HashMap.remove_from_list_fwd T key l match x with | Option.none => Result.ret Option.none | Option.some x0 => @@ -440,21 +439,21 @@ def hashmap_hash_map_remove_fwd Result.ret (Option.some x0) /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ -def hashmap_hash_map_remove_back +def hashmap.HashMap.remove_back (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result (hashmap_hash_map_t T) := do - let hash ← hashmap_hash_key_fwd key + let hash ← hashmap.hash_key_fwd key let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod - let x ← hashmap_hash_map_remove_from_list_fwd T key l + let x ← hashmap.HashMap.remove_from_list_fwd T key l match x with | Option.none => do - let l0 ← hashmap_hash_map_remove_from_list_back T key l + let l0 ← hashmap.HashMap.remove_from_list_back T key l let v ← vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 @@ -463,7 +462,7 @@ def hashmap_hash_map_remove_back do let i0 ← self.hashmap_hash_map_num_entries - (Usize.ofInt 1 (by intlit)) - let l0 ← hashmap_hash_map_remove_from_list_back T key l + let l0 ← hashmap.HashMap.remove_from_list_back T key l let v ← vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 @@ -475,38 +474,37 @@ def hashmap_hash_map_remove_back } /- [hashmap_main::hashmap::test1] -/ -def hashmap_test1_fwd : Result Unit := +def hashmap.test1_fwd : Result Unit := do - let hm ← hashmap_hash_map_new_fwd U64 + let hm ← hashmap.HashMap.new_fwd U64 let hm0 ← - hashmap_hash_map_insert_fwd_back U64 hm (Usize.ofInt 0 (by intlit)) + hashmap.HashMap.insert_fwd_back U64 hm (Usize.ofInt 0 (by intlit)) (U64.ofInt 42 (by intlit)) let hm1 ← - hashmap_hash_map_insert_fwd_back U64 hm0 (Usize.ofInt 128 (by intlit)) + hashmap.HashMap.insert_fwd_back U64 hm0 (Usize.ofInt 128 (by intlit)) (U64.ofInt 18 (by intlit)) let hm2 ← - hashmap_hash_map_insert_fwd_back U64 hm1 (Usize.ofInt 1024 (by intlit)) + hashmap.HashMap.insert_fwd_back U64 hm1 (Usize.ofInt 1024 (by intlit)) (U64.ofInt 138 (by intlit)) let hm3 ← - hashmap_hash_map_insert_fwd_back U64 hm2 (Usize.ofInt 1056 (by intlit)) + hashmap.HashMap.insert_fwd_back U64 hm2 (Usize.ofInt 1056 (by intlit)) (U64.ofInt 256 (by intlit)) - let i ← hashmap_hash_map_get_fwd U64 hm3 (Usize.ofInt 128 (by intlit)) + let i ← hashmap.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 ← - hashmap_hash_map_get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit)) + hashmap.HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit)) (U64.ofInt 56 (by intlit)) let i0 ← - hashmap_hash_map_get_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) + hashmap.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 ← - hashmap_hash_map_remove_fwd U64 hm4 - (Usize.ofInt 1024 (by intlit)) + hashmap.HashMap.remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) match x with | Option.none => Result.fail Error.panic | Option.some x0 => @@ -515,39 +513,38 @@ def hashmap_test1_fwd : Result Unit := else do let hm5 ← - hashmap_hash_map_remove_back U64 hm4 + hashmap.HashMap.remove_back U64 hm4 (Usize.ofInt 1024 (by intlit)) let i1 ← - hashmap_hash_map_get_fwd U64 hm5 - (Usize.ofInt 0 (by intlit)) + hashmap.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 ← - hashmap_hash_map_get_fwd U64 hm5 + hashmap.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 ← - hashmap_hash_map_get_fwd U64 hm5 + hashmap.HashMap.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_main::hashmap::test1] -/ -#assert (hashmap_test1_fwd == .ret ()) +#assert (hashmap.test1_fwd == .ret ()) /- [hashmap_main::insert_on_disk] -/ def insert_on_disk_fwd (key : Usize) (value : U64) (st : State) : Result (State × Unit) := do - let (st0, hm) ← opaque_defs.hashmap_utils_deserialize_fwd st - let hm0 ← hashmap_hash_map_insert_fwd_back U64 hm key value - let (st1, _) ← opaque_defs.hashmap_utils_serialize_fwd hm0 st0 + let (st0, hm) ← hashmap_utils.deserialize_fwd st + let hm0 ← hashmap.HashMap.insert_fwd_back U64 hm key value + let (st1, _) ← hashmap_utils.serialize_fwd hm0 st0 Result.ret (st1, ()) /- [hashmap_main::main] -/ @@ -557,4 +554,4 @@ def main_fwd : Result Unit := /- Unit test for [hashmap_main::main] -/ #assert (main_fwd == .ret ()) -end HashmapMain +end hashmap_main diff --git a/tests/lean/HashmapMain/FunsExternal.lean b/tests/lean/HashmapMain/FunsExternal.lean new file mode 100644 index 00000000..d917b485 --- /dev/null +++ b/tests/lean/HashmapMain/FunsExternal.lean @@ -0,0 +1,17 @@ +-- [hashmap_main]: templates for the external functions. +import Base +import HashmapMain.Types +open Primitives +open hashmap_main + +-- TODO: fill those bodies + +/- [hashmap_main::hashmap_utils::deserialize] -/ +def hashmap_utils.deserialize_fwd + : State → Result (State × (hashmap_hash_map_t U64)) := + fun _ => .fail .panic + +/- [hashmap_main::hashmap_utils::serialize] -/ +def hashmap_utils.serialize_fwd + : hashmap_hash_map_t U64 → State → Result (State × Unit) := + fun _ _ => .fail .panic diff --git a/tests/lean/HashmapMain/FunsExternal_Template.lean b/tests/lean/HashmapMain/FunsExternal_Template.lean new file mode 100644 index 00000000..86286373 --- /dev/null +++ b/tests/lean/HashmapMain/FunsExternal_Template.lean @@ -0,0 +1,16 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. +import Base +import HashmapMain.Types +open Primitives +open hashmap_main + +/- [hashmap_main::hashmap_utils::deserialize] -/ +axiom hashmap_utils.deserialize_fwd + : State → Result (State × (hashmap_hash_map_t U64)) + +/- [hashmap_main::hashmap_utils::serialize] -/ +axiom hashmap_utils.serialize_fwd + : hashmap_hash_map_t U64 → State → Result (State × Unit) + diff --git a/tests/lean/HashmapMain/Opaque.lean b/tests/lean/HashmapMain/Opaque.lean index 10e4d8bd..abf04c94 100644 --- a/tests/lean/HashmapMain/Opaque.lean +++ b/tests/lean/HashmapMain/Opaque.lean @@ -4,16 +4,16 @@ import Base import HashmapMain.Types open Primitives -namespace HashmapMain +namespace hashmap_main structure OpaqueDefs where /- [hashmap_main::hashmap_utils::deserialize] -/ - hashmap_utils_deserialize_fwd + hashmap_utils.deserialize_fwd : State → Result (State × (hashmap_hash_map_t U64)) /- [hashmap_main::hashmap_utils::serialize] -/ - hashmap_utils_serialize_fwd + hashmap_utils.serialize_fwd : hashmap_hash_map_t U64 → State → Result (State × Unit) -end HashmapMain +end hashmap_main diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean index b91ff3a7..16641146 100644 --- a/tests/lean/HashmapMain/Types.lean +++ b/tests/lean/HashmapMain/Types.lean @@ -2,8 +2,7 @@ -- [hashmap_main]: type definitions import Base open Primitives - -namespace HashmapMain +namespace hashmap_main /- [hashmap_main::hashmap::List] -/ inductive hashmap_list_t (T : Type) := @@ -20,4 +19,4 @@ structure hashmap_hash_map_t (T : Type) where /- The state type used in the state-error monad -/ axiom State : Type -end HashmapMain +end hashmap_main -- 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/HashmapMain/Funs.lean | 232 +++++++++++----------- tests/lean/HashmapMain/FunsExternal.lean | 4 +- tests/lean/HashmapMain/FunsExternal_Template.lean | 4 +- tests/lean/HashmapMain/Types.lean | 10 +- 4 files changed, 123 insertions(+), 127 deletions(-) (limited to 'tests/lean/HashmapMain') diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index 06929431..fd556878 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -12,21 +12,21 @@ def hashmap.hash_key_fwd (k : Usize) : Result Usize := /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ divergent def hashmap.HashMap.allocate_slots_loop_fwd - (T : Type) (slots : Vec (hashmap_list_t T)) (n : Usize) : - Result (Vec (hashmap_list_t T)) + (T : Type) (slots : Vec (hashmap.List T)) (n : Usize) : + Result (Vec (hashmap.List T)) := if n > (Usize.ofInt 0 (by intlit)) then do - let slots0 ← vec_push_back (hashmap_list_t T) slots hashmap_list_t.Nil + let slots0 ← vec_push_back (hashmap.List T) slots hashmap.List.Nil let n0 ← n - (Usize.ofInt 1 (by intlit)) hashmap.HashMap.allocate_slots_loop_fwd T slots0 n0 else Result.ret slots /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap.HashMap.allocate_slots_fwd - (T : Type) (slots : Vec (hashmap_list_t T)) (n : Usize) : - Result (Vec (hashmap_list_t T)) + (T : Type) (slots : Vec (hashmap.List T)) (n : Usize) : + Result (Vec (hashmap.List T)) := hashmap.HashMap.allocate_slots_loop_fwd T slots n @@ -34,10 +34,10 @@ def hashmap.HashMap.allocate_slots_fwd def hashmap.HashMap.new_with_capacity_fwd (T : Type) (capacity : Usize) (max_load_dividend : Usize) (max_load_divisor : Usize) : - Result (hashmap_hash_map_t T) + Result (hashmap.HashMap T) := do - let v := vec_new (hashmap_list_t T) + let v := vec_new (hashmap.List T) let slots ← hashmap.HashMap.allocate_slots_fwd T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor @@ -51,28 +51,28 @@ def hashmap.HashMap.new_with_capacity_fwd } /- [hashmap_main::hashmap::HashMap::{0}::new] -/ -def hashmap.HashMap.new_fwd (T : Type) : Result (hashmap_hash_map_t T) := +def hashmap.HashMap.new_fwd (T : Type) : Result (hashmap.HashMap T) := hashmap.HashMap.new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ divergent def hashmap.HashMap.clear_loop_fwd_back - (T : Type) (slots : Vec (hashmap_list_t T)) (i : Usize) : - Result (Vec (hashmap_list_t T)) + (T : Type) (slots : Vec (hashmap.List T)) (i : Usize) : + Result (Vec (hashmap.List T)) := - let i0 := vec_len (hashmap_list_t T) slots + let i0 := vec_len (hashmap.List T) slots if i < i0 then do let i1 ← i + (Usize.ofInt 1 (by intlit)) let slots0 ← - vec_index_mut_back (hashmap_list_t T) slots i hashmap_list_t.Nil + vec_index_mut_back (hashmap.List T) slots i hashmap.List.Nil hashmap.HashMap.clear_loop_fwd_back T slots0 i1 else Result.ret slots /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ def hashmap.HashMap.clear_fwd_back - (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := + (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let v ← hashmap.HashMap.clear_loop_fwd_back T self.hashmap_hash_map_slots @@ -87,59 +87,59 @@ def hashmap.HashMap.clear_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::len] -/ def hashmap.HashMap.len_fwd - (T : Type) (self : hashmap_hash_map_t T) : Result Usize := + (T : Type) (self : hashmap.HashMap T) : Result Usize := Result.ret self.hashmap_hash_map_num_entries /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ divergent def hashmap.HashMap.insert_in_list_loop_fwd - (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool := + (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : Result Bool := match ls with - | hashmap_list_t.Cons ckey cvalue tl => + | hashmap.List.Cons ckey cvalue tl => if ckey = key then Result.ret false else hashmap.HashMap.insert_in_list_loop_fwd T key value tl - | hashmap_list_t.Nil => Result.ret true + | hashmap.List.Nil => Result.ret true /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap.HashMap.insert_in_list_fwd - (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool := + (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : Result Bool := hashmap.HashMap.insert_in_list_loop_fwd T key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ divergent def hashmap.HashMap.insert_in_list_loop_back - (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : - Result (hashmap_list_t T) + (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : + Result (hashmap.List T) := match ls with - | hashmap_list_t.Cons ckey cvalue tl => + | hashmap.List.Cons ckey cvalue tl => if ckey = key - then Result.ret (hashmap_list_t.Cons ckey value tl) + then Result.ret (hashmap.List.Cons ckey value tl) else do let tl0 ← hashmap.HashMap.insert_in_list_loop_back T key value tl - Result.ret (hashmap_list_t.Cons ckey cvalue tl0) - | hashmap_list_t.Nil => - let l := hashmap_list_t.Nil - Result.ret (hashmap_list_t.Cons key value l) + Result.ret (hashmap.List.Cons ckey cvalue tl0) + | hashmap.List.Nil => + let l := hashmap.List.Nil + Result.ret (hashmap.List.Cons key value l) /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap.HashMap.insert_in_list_back - (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : - Result (hashmap_list_t T) + (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : + Result (hashmap.List T) := hashmap.HashMap.insert_in_list_loop_back T key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] -/ def hashmap.HashMap.insert_no_resize_fwd_back - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (value : T) : - Result (hashmap_hash_map_t T) + (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) : + Result (hashmap.HashMap T) := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod let inserted ← hashmap.HashMap.insert_in_list_fwd T key value l if inserted then @@ -148,7 +148,7 @@ def hashmap.HashMap.insert_no_resize_fwd_back (Usize.ofInt 1 (by intlit)) let l0 ← hashmap.HashMap.insert_in_list_back T key value l let v ← - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { @@ -160,7 +160,7 @@ def hashmap.HashMap.insert_no_resize_fwd_back do let l0 ← hashmap.HashMap.insert_in_list_back T key value l let v ← - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { self with hashmap_hash_map_slots := v } @@ -171,57 +171,57 @@ def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ divergent def hashmap.HashMap.move_elements_from_list_loop_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : - Result (hashmap_hash_map_t T) + (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) : + Result (hashmap.HashMap T) := match ls with - | hashmap_list_t.Cons k v tl => + | hashmap.List.Cons k v tl => do let ntable0 ← hashmap.HashMap.insert_no_resize_fwd_back T ntable k v hashmap.HashMap.move_elements_from_list_loop_fwd_back T ntable0 tl - | hashmap_list_t.Nil => Result.ret ntable + | hashmap.List.Nil => Result.ret ntable /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ def hashmap.HashMap.move_elements_from_list_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : - Result (hashmap_hash_map_t T) + (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) : + Result (hashmap.HashMap T) := hashmap.HashMap.move_elements_from_list_loop_fwd_back T ntable ls /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ divergent def hashmap.HashMap.move_elements_loop_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) + (T : Type) (ntable : hashmap.HashMap T) (slots : Vec (hashmap.List T)) (i : Usize) : - Result ((hashmap_hash_map_t T) × (Vec (hashmap_list_t T))) + Result ((hashmap.HashMap T) × (Vec (hashmap.List T))) := - let i0 := vec_len (hashmap_list_t T) slots + let i0 := vec_len (hashmap.List T) slots if i < i0 then do - let l ← vec_index_mut_fwd (hashmap_list_t T) slots i - let ls := mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.Nil + let l ← vec_index_mut_fwd (hashmap.List T) slots i + let ls := mem_replace_fwd (hashmap.List T) l hashmap.List.Nil let ntable0 ← hashmap.HashMap.move_elements_from_list_fwd_back T ntable ls let i1 ← i + (Usize.ofInt 1 (by intlit)) - let l0 := mem_replace_back (hashmap_list_t T) l hashmap_list_t.Nil - let slots0 ← vec_index_mut_back (hashmap_list_t T) slots i l0 + let l0 := mem_replace_back (hashmap.List T) l hashmap.List.Nil + let slots0 ← vec_index_mut_back (hashmap.List T) slots i l0 hashmap.HashMap.move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ def hashmap.HashMap.move_elements_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) + (T : Type) (ntable : hashmap.HashMap T) (slots : Vec (hashmap.List T)) (i : Usize) : - Result ((hashmap_hash_map_t T) × (Vec (hashmap_list_t T))) + Result ((hashmap.HashMap T) × (Vec (hashmap.List T))) := hashmap.HashMap.move_elements_loop_fwd_back T ntable slots i /- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ def hashmap.HashMap.try_resize_fwd_back - (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := + (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c - let capacity := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let capacity := vec_len (hashmap.List T) self.hashmap_hash_map_slots let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) let (i, i0) := self.hashmap_hash_map_max_load_factor let i1 ← n1 / i @@ -244,8 +244,8 @@ def hashmap.HashMap.try_resize_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::insert] -/ def hashmap.HashMap.insert_fwd_back - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (value : T) : - Result (hashmap_hash_map_t T) + (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) : + Result (hashmap.HashMap T) := do let self0 ← hashmap.HashMap.insert_no_resize_fwd_back T self key value @@ -256,179 +256,175 @@ def hashmap.HashMap.insert_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ divergent def hashmap.HashMap.contains_key_in_list_loop_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool := match ls with - | hashmap_list_t.Cons ckey t tl => + | hashmap.List.Cons ckey t tl => if ckey = key then Result.ret true else hashmap.HashMap.contains_key_in_list_loop_fwd T key tl - | hashmap_list_t.Nil => Result.ret false + | hashmap.List.Nil => Result.ret false /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ def hashmap.HashMap.contains_key_in_list_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool := hashmap.HashMap.contains_key_in_list_loop_fwd T key ls /- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ def hashmap.HashMap.contains_key_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result Bool := + (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod hashmap.HashMap.contains_key_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ divergent def hashmap.HashMap.get_in_list_loop_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result T := match ls with - | hashmap_list_t.Cons ckey cvalue tl => + | hashmap.List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue else hashmap.HashMap.get_in_list_loop_fwd T key tl - | hashmap_list_t.Nil => Result.fail Error.panic + | hashmap.List.Nil => Result.fail Error.panic /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ def hashmap.HashMap.get_in_list_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result T := hashmap.HashMap.get_in_list_loop_fwd T key ls /- [hashmap_main::hashmap::HashMap::{0}::get] -/ def hashmap.HashMap.get_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result T := + (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod hashmap.HashMap.get_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def hashmap.HashMap.get_mut_in_list_loop_fwd - (T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T := + (T : Type) (ls : hashmap.List T) (key : Usize) : Result T := match ls with - | hashmap_list_t.Cons ckey cvalue tl => + | hashmap.List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue else hashmap.HashMap.get_mut_in_list_loop_fwd T tl key - | hashmap_list_t.Nil => Result.fail Error.panic + | hashmap.List.Nil => Result.fail Error.panic /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap.HashMap.get_mut_in_list_fwd - (T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T := + (T : Type) (ls : hashmap.List T) (key : Usize) : Result T := hashmap.HashMap.get_mut_in_list_loop_fwd T ls key /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def hashmap.HashMap.get_mut_in_list_loop_back - (T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) : - Result (hashmap_list_t T) + (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) : + Result (hashmap.List T) := match ls with - | hashmap_list_t.Cons ckey cvalue tl => + | hashmap.List.Cons ckey cvalue tl => if ckey = key - then Result.ret (hashmap_list_t.Cons ckey ret0 tl) + then Result.ret (hashmap.List.Cons ckey ret0 tl) else do let tl0 ← hashmap.HashMap.get_mut_in_list_loop_back T tl key ret0 - Result.ret (hashmap_list_t.Cons ckey cvalue tl0) - | hashmap_list_t.Nil => Result.fail Error.panic + Result.ret (hashmap.List.Cons ckey cvalue tl0) + | hashmap.List.Nil => Result.fail Error.panic /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap.HashMap.get_mut_in_list_back - (T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) : - Result (hashmap_list_t T) + (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) : + Result (hashmap.List T) := hashmap.HashMap.get_mut_in_list_loop_back T ls key ret0 /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ def hashmap.HashMap.get_mut_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result T := + (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod hashmap.HashMap.get_mut_in_list_fwd T l key /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ def hashmap.HashMap.get_mut_back - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (ret0 : T) : - Result (hashmap_hash_map_t T) + (T : Type) (self : hashmap.HashMap T) (key : Usize) (ret0 : T) : + Result (hashmap.HashMap T) := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0 let v ← - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 + vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod + l0 Result.ret { self with hashmap_hash_map_slots := v } /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ divergent def hashmap.HashMap.remove_from_list_loop_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result (Option T) := match ls with - | hashmap_list_t.Cons ckey t tl => + | hashmap.List.Cons ckey t tl => if ckey = key then let mv_ls := - mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl) - hashmap_list_t.Nil + mem_replace_fwd (hashmap.List T) (hashmap.List.Cons ckey t tl) + hashmap.List.Nil match mv_ls with - | hashmap_list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) - | hashmap_list_t.Nil => Result.fail Error.panic + | hashmap.List.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | hashmap.List.Nil => Result.fail Error.panic else hashmap.HashMap.remove_from_list_loop_fwd T key tl - | hashmap_list_t.Nil => Result.ret Option.none + | hashmap.List.Nil => Result.ret Option.none /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap.HashMap.remove_from_list_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result (Option T) := hashmap.HashMap.remove_from_list_loop_fwd T key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ divergent def hashmap.HashMap.remove_from_list_loop_back - (T : Type) (key : Usize) (ls : hashmap_list_t T) : - Result (hashmap_list_t T) - := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result (hashmap.List T) := match ls with - | hashmap_list_t.Cons ckey t tl => + | hashmap.List.Cons ckey t tl => if ckey = key then let mv_ls := - mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl) - hashmap_list_t.Nil + mem_replace_fwd (hashmap.List T) (hashmap.List.Cons ckey t tl) + hashmap.List.Nil match mv_ls with - | hashmap_list_t.Cons i cvalue tl0 => Result.ret tl0 - | hashmap_list_t.Nil => Result.fail Error.panic + | hashmap.List.Cons i cvalue tl0 => Result.ret tl0 + | hashmap.List.Nil => Result.fail Error.panic else do let tl0 ← hashmap.HashMap.remove_from_list_loop_back T key tl - Result.ret (hashmap_list_t.Cons ckey t tl0) - | hashmap_list_t.Nil => Result.ret hashmap_list_t.Nil + Result.ret (hashmap.List.Cons ckey t tl0) + | hashmap.List.Nil => Result.ret hashmap.List.Nil /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap.HashMap.remove_from_list_back - (T : Type) (key : Usize) (ls : hashmap_list_t T) : - Result (hashmap_list_t T) - := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result (hashmap.List T) := hashmap.HashMap.remove_from_list_loop_back T key ls /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ def hashmap.HashMap.remove_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result (Option T) := + (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result (Option T) := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod let x ← hashmap.HashMap.remove_from_list_fwd T key l match x with | Option.none => Result.ret Option.none @@ -440,22 +436,22 @@ def hashmap.HashMap.remove_fwd /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ def hashmap.HashMap.remove_back - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : - Result (hashmap_hash_map_t T) + (T : Type) (self : hashmap.HashMap T) (key : Usize) : + Result (hashmap.HashMap T) := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod let x ← hashmap.HashMap.remove_from_list_fwd T key l match x with | Option.none => do let l0 ← hashmap.HashMap.remove_from_list_back T key l let v ← - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { self with hashmap_hash_map_slots := v } | Option.some x0 => @@ -464,7 +460,7 @@ def hashmap.HashMap.remove_back (Usize.ofInt 1 (by intlit)) let l0 ← hashmap.HashMap.remove_from_list_back T key l let v ← - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { diff --git a/tests/lean/HashmapMain/FunsExternal.lean b/tests/lean/HashmapMain/FunsExternal.lean index d917b485..3689dd45 100644 --- a/tests/lean/HashmapMain/FunsExternal.lean +++ b/tests/lean/HashmapMain/FunsExternal.lean @@ -8,10 +8,10 @@ open hashmap_main /- [hashmap_main::hashmap_utils::deserialize] -/ def hashmap_utils.deserialize_fwd - : State → Result (State × (hashmap_hash_map_t U64)) := + : State → Result (State × (hashmap.HashMap U64)) := fun _ => .fail .panic /- [hashmap_main::hashmap_utils::serialize] -/ def hashmap_utils.serialize_fwd - : hashmap_hash_map_t U64 → State → Result (State × Unit) := + : hashmap.HashMap U64 → State → Result (State × Unit) := fun _ _ => .fail .panic diff --git a/tests/lean/HashmapMain/FunsExternal_Template.lean b/tests/lean/HashmapMain/FunsExternal_Template.lean index 86286373..8853b7fc 100644 --- a/tests/lean/HashmapMain/FunsExternal_Template.lean +++ b/tests/lean/HashmapMain/FunsExternal_Template.lean @@ -8,9 +8,9 @@ open hashmap_main /- [hashmap_main::hashmap_utils::deserialize] -/ axiom hashmap_utils.deserialize_fwd - : State → Result (State × (hashmap_hash_map_t U64)) + : State → Result (State × (hashmap.HashMap U64)) /- [hashmap_main::hashmap_utils::serialize] -/ axiom hashmap_utils.serialize_fwd - : hashmap_hash_map_t U64 → State → Result (State × Unit) + : hashmap.HashMap U64 → State → Result (State × Unit) diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean index 16641146..ac195e3d 100644 --- a/tests/lean/HashmapMain/Types.lean +++ b/tests/lean/HashmapMain/Types.lean @@ -5,16 +5,16 @@ open Primitives namespace hashmap_main /- [hashmap_main::hashmap::List] -/ -inductive hashmap_list_t (T : Type) := -| Cons : Usize → T → hashmap_list_t T → hashmap_list_t T -| Nil : hashmap_list_t T +inductive hashmap.List (T : Type) := +| Cons : Usize → T → hashmap.List T → hashmap.List T +| Nil : hashmap.List T /- [hashmap_main::hashmap::HashMap] -/ -structure hashmap_hash_map_t (T : Type) where +structure hashmap.HashMap (T : Type) where hashmap_hash_map_num_entries : Usize hashmap_hash_map_max_load_factor : (Usize × Usize) hashmap_hash_map_max_load : Usize - hashmap_hash_map_slots : Vec (hashmap_list_t T) + hashmap_hash_map_slots : Vec (hashmap.List T) /- The state type used in the state-error monad -/ axiom State : Type -- 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/HashmapMain/Funs.lean | 64 +++++++++++++++++++--------------------- 1 file changed, 31 insertions(+), 33 deletions(-) (limited to 'tests/lean/HashmapMain') diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index fd556878..1a741a2d 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -18,7 +18,7 @@ divergent def hashmap.HashMap.allocate_slots_loop_fwd if n > (Usize.ofInt 0 (by intlit)) then do - let slots0 ← vec_push_back (hashmap.List T) slots hashmap.List.Nil + let slots0 ← Vec.push (hashmap.List T) slots hashmap.List.Nil let n0 ← n - (Usize.ofInt 1 (by intlit)) hashmap.HashMap.allocate_slots_loop_fwd T slots0 n0 else Result.ret slots @@ -37,7 +37,7 @@ def hashmap.HashMap.new_with_capacity_fwd Result (hashmap.HashMap T) := do - let v := vec_new (hashmap.List T) + let v := Vec.new (hashmap.List T) let slots ← hashmap.HashMap.allocate_slots_fwd T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor @@ -60,13 +60,13 @@ divergent def hashmap.HashMap.clear_loop_fwd_back (T : Type) (slots : Vec (hashmap.List T)) (i : Usize) : Result (Vec (hashmap.List T)) := - let i0 := vec_len (hashmap.List T) slots + let i0 := Vec.len (hashmap.List T) slots if i < i0 then do let i1 ← i + (Usize.ofInt 1 (by intlit)) let slots0 ← - vec_index_mut_back (hashmap.List T) slots i hashmap.List.Nil + Vec.index_mut_back (hashmap.List T) slots i hashmap.List.Nil hashmap.HashMap.clear_loop_fwd_back T slots0 i1 else Result.ret slots @@ -136,10 +136,10 @@ def hashmap.HashMap.insert_no_resize_fwd_back := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod + Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod let inserted ← hashmap.HashMap.insert_in_list_fwd T key value l if inserted then @@ -148,7 +148,7 @@ def hashmap.HashMap.insert_no_resize_fwd_back (Usize.ofInt 1 (by intlit)) let l0 ← hashmap.HashMap.insert_in_list_back T key value l let v ← - vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots + Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { @@ -160,7 +160,7 @@ def hashmap.HashMap.insert_no_resize_fwd_back do let l0 ← hashmap.HashMap.insert_in_list_back T key value l let v ← - vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots + Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { self with hashmap_hash_map_slots := v } @@ -194,17 +194,17 @@ divergent def hashmap.HashMap.move_elements_loop_fwd_back (i : Usize) : Result ((hashmap.HashMap T) × (Vec (hashmap.List T))) := - let i0 := vec_len (hashmap.List T) slots + let i0 := Vec.len (hashmap.List T) slots if i < i0 then do - let l ← vec_index_mut_fwd (hashmap.List T) slots i - let ls := mem_replace_fwd (hashmap.List T) l hashmap.List.Nil + let l ← Vec.index_mut (hashmap.List T) slots i + let ls := mem.replace_fwd (hashmap.List T) l hashmap.List.Nil let ntable0 ← hashmap.HashMap.move_elements_from_list_fwd_back T ntable ls let i1 ← i + (Usize.ofInt 1 (by intlit)) - let l0 := mem_replace_back (hashmap.List T) l hashmap.List.Nil - let slots0 ← vec_index_mut_back (hashmap.List T) slots i l0 + let l0 := mem.replace_back (hashmap.List T) l hashmap.List.Nil + let slots0 ← Vec.index_mut_back (hashmap.List T) slots i l0 hashmap.HashMap.move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) @@ -221,7 +221,7 @@ def hashmap.HashMap.try_resize_fwd_back (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c - let capacity := vec_len (hashmap.List T) self.hashmap_hash_map_slots + let capacity := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) let (i, i0) := self.hashmap_hash_map_max_load_factor let i1 ← n1 / i @@ -274,10 +274,9 @@ def hashmap.HashMap.contains_key_fwd (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i - let l ← - vec_index_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index (hashmap.List T) self.hashmap_hash_map_slots hash_mod hashmap.HashMap.contains_key_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ @@ -300,10 +299,9 @@ def hashmap.HashMap.get_fwd (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i - let l ← - vec_index_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index (hashmap.List T) self.hashmap_hash_map_slots hash_mod hashmap.HashMap.get_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -348,10 +346,10 @@ def hashmap.HashMap.get_mut_fwd (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod + Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod hashmap.HashMap.get_mut_in_list_fwd T l key /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ @@ -361,13 +359,13 @@ def hashmap.HashMap.get_mut_back := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod + Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0 let v ← - vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod + Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { self with hashmap_hash_map_slots := v } @@ -379,7 +377,7 @@ divergent def hashmap.HashMap.remove_from_list_loop_fwd if ckey = key then let mv_ls := - mem_replace_fwd (hashmap.List T) (hashmap.List.Cons ckey t tl) + mem.replace_fwd (hashmap.List T) (hashmap.List.Cons ckey t tl) hashmap.List.Nil match mv_ls with | hashmap.List.Cons i cvalue tl0 => Result.ret (Option.some cvalue) @@ -400,7 +398,7 @@ divergent def hashmap.HashMap.remove_from_list_loop_back if ckey = key then let mv_ls := - mem_replace_fwd (hashmap.List T) (hashmap.List.Cons ckey t tl) + mem.replace_fwd (hashmap.List T) (hashmap.List.Cons ckey t tl) hashmap.List.Nil match mv_ls with | hashmap.List.Cons i cvalue tl0 => Result.ret tl0 @@ -421,10 +419,10 @@ def hashmap.HashMap.remove_fwd (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result (Option T) := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod + Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod let x ← hashmap.HashMap.remove_from_list_fwd T key l match x with | Option.none => Result.ret Option.none @@ -441,17 +439,17 @@ def hashmap.HashMap.remove_back := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod + Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod let x ← hashmap.HashMap.remove_from_list_fwd T key l match x with | Option.none => do let l0 ← hashmap.HashMap.remove_from_list_back T key l let v ← - vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots + Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { self with hashmap_hash_map_slots := v } | Option.some x0 => @@ -460,7 +458,7 @@ def hashmap.HashMap.remove_back (Usize.ofInt 1 (by intlit)) let l0 ← hashmap.HashMap.remove_from_list_back T key l let v ← - vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots + Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { -- 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/HashmapMain/Funs.lean | 276 +++++++++++----------- tests/lean/HashmapMain/FunsExternal.lean | 4 +- tests/lean/HashmapMain/FunsExternal_Template.lean | 8 +- 3 files changed, 147 insertions(+), 141 deletions(-) (limited to 'tests/lean/HashmapMain') diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index 1a741a2d..b1afcd44 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -6,12 +6,12 @@ import HashmapMain.FunsExternal open Primitives namespace hashmap_main -/- [hashmap_main::hashmap::hash_key] -/ -def hashmap.hash_key_fwd (k : Usize) : Result Usize := +/- [hashmap_main::hashmap::hash_key]: forward function -/ +def hashmap.hash_key (k : Usize) : Result Usize := Result.ret k -/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ -divergent def hashmap.HashMap.allocate_slots_loop_fwd +/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function -/ +divergent def hashmap.HashMap.allocate_slots_loop (T : Type) (slots : Vec (hashmap.List T)) (n : Usize) : Result (Vec (hashmap.List T)) := @@ -20,25 +20,25 @@ divergent def hashmap.HashMap.allocate_slots_loop_fwd do let slots0 ← Vec.push (hashmap.List T) slots hashmap.List.Nil let n0 ← n - (Usize.ofInt 1 (by intlit)) - hashmap.HashMap.allocate_slots_loop_fwd T slots0 n0 + hashmap.HashMap.allocate_slots_loop T slots0 n0 else Result.ret slots -/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ -def hashmap.HashMap.allocate_slots_fwd +/- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function -/ +def hashmap.HashMap.allocate_slots (T : Type) (slots : Vec (hashmap.List T)) (n : Usize) : Result (Vec (hashmap.List T)) := - hashmap.HashMap.allocate_slots_loop_fwd T slots n + hashmap.HashMap.allocate_slots_loop T slots n -/- [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] -/ -def hashmap.HashMap.new_with_capacity_fwd +/- [hashmap_main::hashmap::HashMap::{0}::new_with_capacity]: forward function -/ +def hashmap.HashMap.new_with_capacity (T : Type) (capacity : Usize) (max_load_dividend : Usize) (max_load_divisor : Usize) : Result (hashmap.HashMap T) := do let v := Vec.new (hashmap.List T) - let slots ← hashmap.HashMap.allocate_slots_fwd T v capacity + let slots ← hashmap.HashMap.allocate_slots T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor Result.ret @@ -50,13 +50,14 @@ def hashmap.HashMap.new_with_capacity_fwd hashmap_hash_map_slots := slots } -/- [hashmap_main::hashmap::HashMap::{0}::new] -/ -def hashmap.HashMap.new_fwd (T : Type) : Result (hashmap.HashMap T) := - hashmap.HashMap.new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) +/- [hashmap_main::hashmap::HashMap::{0}::new]: forward function -/ +def hashmap.HashMap.new (T : Type) : Result (hashmap.HashMap T) := + hashmap.HashMap.new_with_capacity T (Usize.ofInt 32 (by intlit)) (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) -/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ -divergent def hashmap.HashMap.clear_loop_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +divergent def hashmap.HashMap.clear_loop (T : Type) (slots : Vec (hashmap.List T)) (i : Usize) : Result (Vec (hashmap.List T)) := @@ -67,15 +68,16 @@ divergent def hashmap.HashMap.clear_loop_fwd_back let i1 ← i + (Usize.ofInt 1 (by intlit)) let slots0 ← Vec.index_mut_back (hashmap.List T) slots i hashmap.List.Nil - hashmap.HashMap.clear_loop_fwd_back T slots0 i1 + hashmap.HashMap.clear_loop T slots0 i1 else Result.ret slots -/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ -def hashmap.HashMap.clear_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::clear]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def hashmap.HashMap.clear (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let v ← - hashmap.HashMap.clear_loop_fwd_back T self.hashmap_hash_map_slots + hashmap.HashMap.clear_loop T self.hashmap_hash_map_slots (Usize.ofInt 0 (by intlit)) Result.ret { @@ -85,27 +87,26 @@ def hashmap.HashMap.clear_fwd_back hashmap_hash_map_slots := v } -/- [hashmap_main::hashmap::HashMap::{0}::len] -/ -def hashmap.HashMap.len_fwd - (T : Type) (self : hashmap.HashMap T) : Result Usize := +/- [hashmap_main::hashmap::HashMap::{0}::len]: forward function -/ +def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize := Result.ret self.hashmap_hash_map_num_entries -/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ -divergent def hashmap.HashMap.insert_in_list_loop_fwd +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function -/ +divergent def hashmap.HashMap.insert_in_list_loop (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : Result Bool := match ls with | hashmap.List.Cons ckey cvalue tl => if ckey = key then Result.ret false - else hashmap.HashMap.insert_in_list_loop_fwd T key value tl + else hashmap.HashMap.insert_in_list_loop T key value tl | hashmap.List.Nil => Result.ret true -/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ -def hashmap.HashMap.insert_in_list_fwd +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: forward function -/ +def hashmap.HashMap.insert_in_list (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : Result Bool := - hashmap.HashMap.insert_in_list_loop_fwd T key value ls + hashmap.HashMap.insert_in_list_loop T key value ls -/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 -/ divergent def hashmap.HashMap.insert_in_list_loop_back (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : Result (hashmap.List T) @@ -122,25 +123,26 @@ divergent def hashmap.HashMap.insert_in_list_loop_back let l := hashmap.List.Nil Result.ret (hashmap.List.Cons key value l) -/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: backward function 0 -/ def hashmap.HashMap.insert_in_list_back (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : Result (hashmap.List T) := hashmap.HashMap.insert_in_list_loop_back T key value ls -/- [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] -/ -def hashmap.HashMap.insert_no_resize_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def hashmap.HashMap.insert_no_resize (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) : Result (hashmap.HashMap T) := do - let hash ← hashmap.hash_key_fwd key + let hash ← hashmap.hash_key key let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod - let inserted ← hashmap.HashMap.insert_in_list_fwd T key value l + let inserted ← hashmap.HashMap.insert_in_list T key value l if inserted then do @@ -169,27 +171,30 @@ 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_main::hashmap::HashMap::{0}::move_elements_from_list] -/ -divergent def hashmap.HashMap.move_elements_from_list_loop_fwd_back +/- [hashmap_main::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.HashMap.move_elements_from_list_loop (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) : Result (hashmap.HashMap T) := match ls with | hashmap.List.Cons k v tl => do - let ntable0 ← hashmap.HashMap.insert_no_resize_fwd_back T ntable k v - hashmap.HashMap.move_elements_from_list_loop_fwd_back T ntable0 tl + let ntable0 ← hashmap.HashMap.insert_no_resize T ntable k v + hashmap.HashMap.move_elements_from_list_loop T ntable0 tl | hashmap.List.Nil => Result.ret ntable -/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ -def hashmap.HashMap.move_elements_from_list_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def hashmap.HashMap.move_elements_from_list (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) : Result (hashmap.HashMap T) := - hashmap.HashMap.move_elements_from_list_loop_fwd_back T ntable ls + hashmap.HashMap.move_elements_from_list_loop T ntable ls -/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ -divergent def hashmap.HashMap.move_elements_loop_fwd_back +/- [hashmap_main::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.HashMap.move_elements_loop (T : Type) (ntable : hashmap.HashMap T) (slots : Vec (hashmap.List T)) (i : Usize) : Result ((hashmap.HashMap T) × (Vec (hashmap.List T))) @@ -199,25 +204,26 @@ divergent def hashmap.HashMap.move_elements_loop_fwd_back then do let l ← Vec.index_mut (hashmap.List T) slots i - let ls := mem.replace_fwd (hashmap.List T) l hashmap.List.Nil - let ntable0 ← - hashmap.HashMap.move_elements_from_list_fwd_back T ntable ls + let ls := mem.replace (hashmap.List T) l hashmap.List.Nil + let ntable0 ← hashmap.HashMap.move_elements_from_list T ntable ls let i1 ← i + (Usize.ofInt 1 (by intlit)) let l0 := mem.replace_back (hashmap.List T) l hashmap.List.Nil let slots0 ← Vec.index_mut_back (hashmap.List T) slots i l0 - hashmap.HashMap.move_elements_loop_fwd_back T ntable0 slots0 i1 + hashmap.HashMap.move_elements_loop T ntable0 slots0 i1 else Result.ret (ntable, slots) -/- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ -def hashmap.HashMap.move_elements_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def hashmap.HashMap.move_elements (T : Type) (ntable : hashmap.HashMap T) (slots : Vec (hashmap.List T)) (i : Usize) : Result ((hashmap.HashMap T) × (Vec (hashmap.List T))) := - hashmap.HashMap.move_elements_loop_fwd_back T ntable slots i + hashmap.HashMap.move_elements_loop T ntable slots i -/- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ -def hashmap.HashMap.try_resize_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::try_resize]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def hashmap.HashMap.try_resize (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c @@ -229,10 +235,10 @@ def hashmap.HashMap.try_resize_fwd_back then do let i2 ← capacity * (Usize.ofInt 2 (by intlit)) - let ntable ← hashmap.HashMap.new_with_capacity_fwd T i2 i i0 + let ntable ← hashmap.HashMap.new_with_capacity T i2 i i0 let (ntable0, _) ← - hashmap.HashMap.move_elements_fwd_back T ntable - self.hashmap_hash_map_slots (Usize.ofInt 0 (by intlit)) + hashmap.HashMap.move_elements T ntable self.hashmap_hash_map_slots + (Usize.ofInt 0 (by intlit)) Result.ret { ntable0 @@ -242,84 +248,85 @@ def hashmap.HashMap.try_resize_fwd_back } else Result.ret { self with hashmap_hash_map_max_load_factor := (i, i0) } -/- [hashmap_main::hashmap::HashMap::{0}::insert] -/ -def hashmap.HashMap.insert_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def hashmap.HashMap.insert (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) : Result (hashmap.HashMap T) := do - let self0 ← hashmap.HashMap.insert_no_resize_fwd_back T self key value - let i ← hashmap.HashMap.len_fwd T self0 + let self0 ← hashmap.HashMap.insert_no_resize T self key value + let i ← hashmap.HashMap.len T self0 if i > self0.hashmap_hash_map_max_load - then hashmap.HashMap.try_resize_fwd_back T self0 + then hashmap.HashMap.try_resize T self0 else Result.ret self0 -/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ -divergent def hashmap.HashMap.contains_key_in_list_loop_fwd +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function -/ +divergent def hashmap.HashMap.contains_key_in_list_loop (T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool := match ls with | hashmap.List.Cons ckey t tl => if ckey = key then Result.ret true - else hashmap.HashMap.contains_key_in_list_loop_fwd T key tl + else hashmap.HashMap.contains_key_in_list_loop T key tl | hashmap.List.Nil => Result.ret false -/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ -def hashmap.HashMap.contains_key_in_list_fwd +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: forward function -/ +def hashmap.HashMap.contains_key_in_list (T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool := - hashmap.HashMap.contains_key_in_list_loop_fwd T key ls + hashmap.HashMap.contains_key_in_list_loop T key ls -/- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ -def hashmap.HashMap.contains_key_fwd +/- [hashmap_main::hashmap::HashMap::{0}::contains_key]: forward function -/ +def hashmap.HashMap.contains_key (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool := do - let hash ← hashmap.hash_key_fwd key + let hash ← hashmap.hash_key key let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← Vec.index (hashmap.List T) self.hashmap_hash_map_slots hash_mod - hashmap.HashMap.contains_key_in_list_fwd T key l + hashmap.HashMap.contains_key_in_list T key l -/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ -divergent def hashmap.HashMap.get_in_list_loop_fwd +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/ +divergent def hashmap.HashMap.get_in_list_loop (T : Type) (key : Usize) (ls : hashmap.List T) : Result T := match ls with | hashmap.List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue - else hashmap.HashMap.get_in_list_loop_fwd T key tl + else hashmap.HashMap.get_in_list_loop T key tl | hashmap.List.Nil => Result.fail Error.panic -/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ -def hashmap.HashMap.get_in_list_fwd +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: forward function -/ +def hashmap.HashMap.get_in_list (T : Type) (key : Usize) (ls : hashmap.List T) : Result T := - hashmap.HashMap.get_in_list_loop_fwd T key ls + hashmap.HashMap.get_in_list_loop T key ls -/- [hashmap_main::hashmap::HashMap::{0}::get] -/ -def hashmap.HashMap.get_fwd +/- [hashmap_main::hashmap::HashMap::{0}::get]: forward function -/ +def hashmap.HashMap.get (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do - let hash ← hashmap.hash_key_fwd key + let hash ← hashmap.hash_key key let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← Vec.index (hashmap.List T) self.hashmap_hash_map_slots hash_mod - hashmap.HashMap.get_in_list_fwd T key l + hashmap.HashMap.get_in_list T key l -/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -divergent def hashmap.HashMap.get_mut_in_list_loop_fwd +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/ +divergent def hashmap.HashMap.get_mut_in_list_loop (T : Type) (ls : hashmap.List T) (key : Usize) : Result T := match ls with | hashmap.List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue - else hashmap.HashMap.get_mut_in_list_loop_fwd T tl key + else hashmap.HashMap.get_mut_in_list_loop T tl key | hashmap.List.Nil => Result.fail Error.panic -/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ -def hashmap.HashMap.get_mut_in_list_fwd +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: forward function -/ +def hashmap.HashMap.get_mut_in_list (T : Type) (ls : hashmap.List T) (key : Usize) : Result T := - hashmap.HashMap.get_mut_in_list_loop_fwd T ls key + hashmap.HashMap.get_mut_in_list_loop T ls key -/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 -/ divergent def hashmap.HashMap.get_mut_in_list_loop_back (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) : Result (hashmap.List T) @@ -334,31 +341,31 @@ divergent def hashmap.HashMap.get_mut_in_list_loop_back Result.ret (hashmap.List.Cons ckey cvalue tl0) | hashmap.List.Nil => Result.fail Error.panic -/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 -/ def hashmap.HashMap.get_mut_in_list_back (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) : Result (hashmap.List T) := hashmap.HashMap.get_mut_in_list_loop_back T ls key ret0 -/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ -def hashmap.HashMap.get_mut_fwd +/- [hashmap_main::hashmap::HashMap::{0}::get_mut]: forward function -/ +def hashmap.HashMap.get_mut (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do - let hash ← hashmap.hash_key_fwd key + let hash ← hashmap.hash_key key let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod - hashmap.HashMap.get_mut_in_list_fwd T l key + hashmap.HashMap.get_mut_in_list T l key -/- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ +/- [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 -/ def hashmap.HashMap.get_mut_back (T : Type) (self : hashmap.HashMap T) (key : Usize) (ret0 : T) : Result (hashmap.HashMap T) := do - let hash ← hashmap.hash_key_fwd key + let hash ← hashmap.hash_key key let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← @@ -369,28 +376,28 @@ def hashmap.HashMap.get_mut_back l0 Result.ret { self with hashmap_hash_map_slots := v } -/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -divergent def hashmap.HashMap.remove_from_list_loop_fwd +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function -/ +divergent def hashmap.HashMap.remove_from_list_loop (T : Type) (key : Usize) (ls : hashmap.List T) : Result (Option T) := match ls with | hashmap.List.Cons ckey t tl => if ckey = key then let mv_ls := - mem.replace_fwd (hashmap.List T) (hashmap.List.Cons ckey t tl) + mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl) hashmap.List.Nil match mv_ls with | hashmap.List.Cons i cvalue tl0 => Result.ret (Option.some cvalue) | hashmap.List.Nil => Result.fail Error.panic - else hashmap.HashMap.remove_from_list_loop_fwd T key tl + else hashmap.HashMap.remove_from_list_loop T key tl | hashmap.List.Nil => Result.ret Option.none -/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ -def hashmap.HashMap.remove_from_list_fwd +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function -/ +def hashmap.HashMap.remove_from_list (T : Type) (key : Usize) (ls : hashmap.List T) : Result (Option T) := - hashmap.HashMap.remove_from_list_loop_fwd T key ls + hashmap.HashMap.remove_from_list_loop T key ls -/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 -/ divergent def hashmap.HashMap.remove_from_list_loop_back (T : Type) (key : Usize) (ls : hashmap.List T) : Result (hashmap.List T) := match ls with @@ -398,7 +405,7 @@ divergent def hashmap.HashMap.remove_from_list_loop_back if ckey = key then let mv_ls := - mem.replace_fwd (hashmap.List T) (hashmap.List.Cons ckey t tl) + mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl) hashmap.List.Nil match mv_ls with | hashmap.List.Cons i cvalue tl0 => Result.ret tl0 @@ -409,21 +416,21 @@ divergent def hashmap.HashMap.remove_from_list_loop_back Result.ret (hashmap.List.Cons ckey t tl0) | hashmap.List.Nil => Result.ret hashmap.List.Nil -/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: backward function 1 -/ def hashmap.HashMap.remove_from_list_back (T : Type) (key : Usize) (ls : hashmap.List T) : Result (hashmap.List T) := hashmap.HashMap.remove_from_list_loop_back T key ls -/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ -def hashmap.HashMap.remove_fwd +/- [hashmap_main::hashmap::HashMap::{0}::remove]: forward function -/ +def hashmap.HashMap.remove (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result (Option T) := do - let hash ← hashmap.hash_key_fwd key + let hash ← hashmap.hash_key key let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod - let x ← hashmap.HashMap.remove_from_list_fwd T key l + let x ← hashmap.HashMap.remove_from_list T key l match x with | Option.none => Result.ret Option.none | Option.some x0 => @@ -432,18 +439,18 @@ def hashmap.HashMap.remove_fwd (Usize.ofInt 1 (by intlit)) Result.ret (Option.some x0) -/- [hashmap_main::hashmap::HashMap::{0}::remove] -/ +/- [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 -/ def hashmap.HashMap.remove_back (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result (hashmap.HashMap T) := do - let hash ← hashmap.hash_key_fwd key + let hash ← hashmap.hash_key key let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod - let x ← hashmap.HashMap.remove_from_list_fwd T key l + let x ← hashmap.HashMap.remove_from_list T key l match x with | Option.none => do @@ -467,23 +474,23 @@ def hashmap.HashMap.remove_back hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v } -/- [hashmap_main::hashmap::test1] -/ -def hashmap.test1_fwd : Result Unit := +/- [hashmap_main::hashmap::test1]: forward function -/ +def hashmap.test1 : Result Unit := do - let hm ← hashmap.HashMap.new_fwd U64 + let hm ← hashmap.HashMap.new U64 let hm0 ← - hashmap.HashMap.insert_fwd_back U64 hm (Usize.ofInt 0 (by intlit)) + hashmap.HashMap.insert U64 hm (Usize.ofInt 0 (by intlit)) (U64.ofInt 42 (by intlit)) let hm1 ← - hashmap.HashMap.insert_fwd_back U64 hm0 (Usize.ofInt 128 (by intlit)) + hashmap.HashMap.insert U64 hm0 (Usize.ofInt 128 (by intlit)) (U64.ofInt 18 (by intlit)) let hm2 ← - hashmap.HashMap.insert_fwd_back U64 hm1 (Usize.ofInt 1024 (by intlit)) + hashmap.HashMap.insert U64 hm1 (Usize.ofInt 1024 (by intlit)) (U64.ofInt 138 (by intlit)) let hm3 ← - hashmap.HashMap.insert_fwd_back U64 hm2 (Usize.ofInt 1056 (by intlit)) + hashmap.HashMap.insert U64 hm2 (Usize.ofInt 1056 (by intlit)) (U64.ofInt 256 (by intlit)) - let i ← hashmap.HashMap.get_fwd U64 hm3 (Usize.ofInt 128 (by intlit)) + let i ← hashmap.HashMap.get U64 hm3 (Usize.ofInt 128 (by intlit)) if not (i = (U64.ofInt 18 (by intlit))) then Result.fail Error.panic else @@ -491,14 +498,13 @@ def hashmap.test1_fwd : Result Unit := let hm4 ← hashmap.HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit)) (U64.ofInt 56 (by intlit)) - let i0 ← - hashmap.HashMap.get_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) + let i0 ← hashmap.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.HashMap.remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit)) + hashmap.HashMap.remove U64 hm4 (Usize.ofInt 1024 (by intlit)) match x with | Option.none => Result.fail Error.panic | Option.some x0 => @@ -510,42 +516,42 @@ def hashmap.test1_fwd : Result Unit := hashmap.HashMap.remove_back U64 hm4 (Usize.ofInt 1024 (by intlit)) let i1 ← - hashmap.HashMap.get_fwd U64 hm5 (Usize.ofInt 0 (by intlit)) + hashmap.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.HashMap.get_fwd U64 hm5 + hashmap.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.HashMap.get_fwd U64 hm5 + hashmap.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_main::hashmap::test1] -/ -#assert (hashmap.test1_fwd == .ret ()) +#assert (hashmap.test1 == .ret ()) -/- [hashmap_main::insert_on_disk] -/ -def insert_on_disk_fwd +/- [hashmap_main::insert_on_disk]: forward function -/ +def insert_on_disk (key : Usize) (value : U64) (st : State) : Result (State × Unit) := do - let (st0, hm) ← hashmap_utils.deserialize_fwd st - let hm0 ← hashmap.HashMap.insert_fwd_back U64 hm key value - let (st1, _) ← hashmap_utils.serialize_fwd hm0 st0 + let (st0, hm) ← hashmap_utils.deserialize st + let hm0 ← hashmap.HashMap.insert U64 hm key value + let (st1, _) ← hashmap_utils.serialize hm0 st0 Result.ret (st1, ()) -/- [hashmap_main::main] -/ -def main_fwd : Result Unit := +/- [hashmap_main::main]: forward function -/ +def main : Result Unit := Result.ret () /- Unit test for [hashmap_main::main] -/ -#assert (main_fwd == .ret ()) +#assert (main == .ret ()) end hashmap_main diff --git a/tests/lean/HashmapMain/FunsExternal.lean b/tests/lean/HashmapMain/FunsExternal.lean index 3689dd45..b394b32b 100644 --- a/tests/lean/HashmapMain/FunsExternal.lean +++ b/tests/lean/HashmapMain/FunsExternal.lean @@ -7,11 +7,11 @@ open hashmap_main -- TODO: fill those bodies /- [hashmap_main::hashmap_utils::deserialize] -/ -def hashmap_utils.deserialize_fwd +def hashmap_utils.deserialize : State → Result (State × (hashmap.HashMap U64)) := fun _ => .fail .panic /- [hashmap_main::hashmap_utils::serialize] -/ -def hashmap_utils.serialize_fwd +def hashmap_utils.serialize : hashmap.HashMap U64 → State → Result (State × Unit) := fun _ _ => .fail .panic diff --git a/tests/lean/HashmapMain/FunsExternal_Template.lean b/tests/lean/HashmapMain/FunsExternal_Template.lean index 8853b7fc..f537fc8f 100644 --- a/tests/lean/HashmapMain/FunsExternal_Template.lean +++ b/tests/lean/HashmapMain/FunsExternal_Template.lean @@ -6,11 +6,11 @@ import HashmapMain.Types open Primitives open hashmap_main -/- [hashmap_main::hashmap_utils::deserialize] -/ -axiom hashmap_utils.deserialize_fwd +/- [hashmap_main::hashmap_utils::deserialize]: forward function -/ +axiom hashmap_utils.deserialize : State → Result (State × (hashmap.HashMap U64)) -/- [hashmap_main::hashmap_utils::serialize] -/ -axiom hashmap_utils.serialize_fwd +/- [hashmap_main::hashmap_utils::serialize]: forward function -/ +axiom hashmap_utils.serialize : hashmap.HashMap U64 → State → Result (State × Unit) -- 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/HashmapMain/Funs.lean | 116 +++++++++++++------------------------- tests/lean/HashmapMain/Types.lean | 8 +-- 2 files changed, 44 insertions(+), 80 deletions(-) (limited to 'tests/lean/HashmapMain') diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index b1afcd44..e82cc9b2 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -43,11 +43,10 @@ def hashmap.HashMap.new_with_capacity let i0 ← i / max_load_divisor Result.ret { - hashmap_hash_map_num_entries := (Usize.ofInt 0 (by intlit)), - hashmap_hash_map_max_load_factor := - (max_load_dividend, max_load_divisor), - hashmap_hash_map_max_load := i0, - hashmap_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_main::hashmap::HashMap::{0}::new]: forward function -/ @@ -77,19 +76,13 @@ def hashmap.HashMap.clear (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let v ← - hashmap.HashMap.clear_loop T self.hashmap_hash_map_slots - (Usize.ofInt 0 (by intlit)) + hashmap.HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit)) Result.ret - { - self - with - hashmap_hash_map_num_entries := (Usize.ofInt 0 (by intlit)), - hashmap_hash_map_slots := v - } + { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v } /- [hashmap_main::hashmap::HashMap::{0}::len]: forward function -/ def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize := - Result.ret self.hashmap_hash_map_num_entries + Result.ret self.num_entries /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function -/ divergent def hashmap.HashMap.insert_in_list_loop @@ -138,33 +131,22 @@ def hashmap.HashMap.insert_no_resize := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← - Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod let inserted ← hashmap.HashMap.insert_in_list T key value l if inserted then do - let i0 ← self.hashmap_hash_map_num_entries + - (Usize.ofInt 1 (by intlit)) + let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit)) let l0 ← hashmap.HashMap.insert_in_list_back T key value l - let v ← - Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots - hash_mod l0 - Result.ret - { - self - with - hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v - } + let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + Result.ret { self with num_entries := i0, slots := v } else do let l0 ← hashmap.HashMap.insert_in_list_back T key value l - let v ← - Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots - hash_mod l0 - Result.ret { self with hashmap_hash_map_slots := v } + let v ← Vec.index_mut_back (hashmap.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 := @@ -227,9 +209,9 @@ def hashmap.HashMap.try_resize (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c - let capacity := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let capacity := Vec.len (hashmap.List T) self.slots let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) - let (i, i0) := self.hashmap_hash_map_max_load_factor + let (i, i0) := self.max_load_factor let i1 ← n1 / i if capacity <= i1 then @@ -237,16 +219,15 @@ def hashmap.HashMap.try_resize let i2 ← capacity * (Usize.ofInt 2 (by intlit)) let ntable ← hashmap.HashMap.new_with_capacity T i2 i i0 let (ntable0, _) ← - hashmap.HashMap.move_elements T ntable self.hashmap_hash_map_slots + hashmap.HashMap.move_elements T ntable self.slots (Usize.ofInt 0 (by intlit)) Result.ret { ntable0 with - hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries, - hashmap_hash_map_max_load_factor := (i, i0) + num_entries := self.num_entries, max_load_factor := (i, i0) } - else Result.ret { self with hashmap_hash_map_max_load_factor := (i, i0) } + else Result.ret { self with max_load_factor := (i, i0) } /- [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ @@ -257,7 +238,7 @@ def hashmap.HashMap.insert do let self0 ← hashmap.HashMap.insert_no_resize T self key value let i ← hashmap.HashMap.len T self0 - if i > self0.hashmap_hash_map_max_load + if i > self0.max_load then hashmap.HashMap.try_resize T self0 else Result.ret self0 @@ -281,9 +262,9 @@ def hashmap.HashMap.contains_key (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index (hashmap.List T) self.slots hash_mod hashmap.HashMap.contains_key_in_list T key l /- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/ @@ -306,9 +287,9 @@ def hashmap.HashMap.get (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← Vec.index (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index (hashmap.List T) self.slots hash_mod hashmap.HashMap.get_in_list T key l /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/ @@ -353,10 +334,9 @@ def hashmap.HashMap.get_mut (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← - Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod hashmap.HashMap.get_mut_in_list T l key /- [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 -/ @@ -366,15 +346,12 @@ def hashmap.HashMap.get_mut_back := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← - Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0 - let v ← - Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod - l0 - Result.ret { self with hashmap_hash_map_slots := v } + let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + Result.ret { self with slots := v } /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function -/ divergent def hashmap.HashMap.remove_from_list_loop @@ -426,17 +403,15 @@ def hashmap.HashMap.remove (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result (Option T) := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← - Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod let x ← hashmap.HashMap.remove_from_list T key l match x with | Option.none => Result.ret Option.none | Option.some x0 => do - let _ ← self.hashmap_hash_map_num_entries - - (Usize.ofInt 1 (by intlit)) + let _ ← self.num_entries - (Usize.ofInt 1 (by intlit)) Result.ret (Option.some x0) /- [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 -/ @@ -446,33 +421,22 @@ def hashmap.HashMap.remove_back := do let hash ← hashmap.hash_key key - let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots + let i := Vec.len (hashmap.List T) self.slots let hash_mod ← hash % i - let l ← - Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod + let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod let x ← hashmap.HashMap.remove_from_list T key l match x with | Option.none => do let l0 ← hashmap.HashMap.remove_from_list_back T key l - let v ← - Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots - hash_mod l0 - Result.ret { self with hashmap_hash_map_slots := v } + let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + Result.ret { self with slots := v } | Option.some x0 => do - let i0 ← self.hashmap_hash_map_num_entries - - (Usize.ofInt 1 (by intlit)) + let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit)) let l0 ← hashmap.HashMap.remove_from_list_back T key l - let v ← - Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots - hash_mod l0 - Result.ret - { - self - with - hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v - } + let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 + Result.ret { self with num_entries := i0, slots := v } /- [hashmap_main::hashmap::test1]: forward function -/ def hashmap.test1 : Result Unit := diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean index ac195e3d..3b3d0d7c 100644 --- a/tests/lean/HashmapMain/Types.lean +++ b/tests/lean/HashmapMain/Types.lean @@ -11,10 +11,10 @@ inductive hashmap.List (T : Type) := /- [hashmap_main::hashmap::HashMap] -/ structure hashmap.HashMap (T : Type) where - hashmap_hash_map_num_entries : Usize - hashmap_hash_map_max_load_factor : (Usize × Usize) - hashmap_hash_map_max_load : Usize - hashmap_hash_map_slots : Vec (hashmap.List T) + num_entries : Usize + max_load_factor : (Usize × Usize) + max_load : Usize + slots : Vec (hashmap.List T) /- The state type used in the state-error monad -/ axiom State : Type -- 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/HashmapMain/Funs.lean | 86 ++++++++++++++++------------------------ 1 file changed, 35 insertions(+), 51 deletions(-) (limited to 'tests/lean/HashmapMain') diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index e82cc9b2..610bae46 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -15,11 +15,11 @@ divergent def hashmap.HashMap.allocate_slots_loop (T : Type) (slots : Vec (hashmap.List T)) (n : Usize) : Result (Vec (hashmap.List T)) := - if n > (Usize.ofInt 0 (by intlit)) + if n > (Usize.ofInt 0) then do let slots0 ← Vec.push (hashmap.List T) slots hashmap.List.Nil - let n0 ← n - (Usize.ofInt 1 (by intlit)) + let n0 ← n - (Usize.ofInt 1) hashmap.HashMap.allocate_slots_loop T slots0 n0 else Result.ret slots @@ -43,7 +43,7 @@ def hashmap.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 @@ -51,8 +51,8 @@ def hashmap.HashMap.new_with_capacity /- [hashmap_main::hashmap::HashMap::{0}::new]: forward function -/ def hashmap.HashMap.new (T : Type) : Result (hashmap.HashMap T) := - hashmap.HashMap.new_with_capacity T (Usize.ofInt 32 (by intlit)) - (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) + hashmap.HashMap.new_with_capacity T (Usize.ofInt 32) (Usize.ofInt 4) + (Usize.ofInt 5) /- [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ @@ -64,7 +64,7 @@ divergent def hashmap.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 (hashmap.List T) slots i hashmap.List.Nil hashmap.HashMap.clear_loop T slots0 i1 @@ -75,10 +75,8 @@ divergent def hashmap.HashMap.clear_loop def hashmap.HashMap.clear (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do - let v ← - hashmap.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.HashMap.clear_loop T self.slots (Usize.ofInt 0) + Result.ret { self with num_entries := (Usize.ofInt 0), slots := v } /- [hashmap_main::hashmap::HashMap::{0}::len]: forward function -/ def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize := @@ -138,7 +136,7 @@ def hashmap.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.HashMap.insert_in_list_back T key value l let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 Result.ret { self with num_entries := i0, slots := v } @@ -149,8 +147,7 @@ def hashmap.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_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function @@ -188,7 +185,7 @@ divergent def hashmap.HashMap.move_elements_loop let l ← Vec.index_mut (hashmap.List T) slots i let ls := mem.replace (hashmap.List T) l hashmap.List.Nil let ntable0 ← hashmap.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 (hashmap.List T) l hashmap.List.Nil let slots0 ← Vec.index_mut_back (hashmap.List T) slots i l0 hashmap.HashMap.move_elements_loop T ntable0 slots0 i1 @@ -210,17 +207,16 @@ def hashmap.HashMap.try_resize do let max_usize ← Scalar.cast .Usize core_num_u32_max_c let capacity := Vec.len (hashmap.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.HashMap.new_with_capacity T i2 i i0 let (ntable0, _) ← - hashmap.HashMap.move_elements T ntable self.slots - (Usize.ofInt 0 (by intlit)) + hashmap.HashMap.move_elements T ntable self.slots (Usize.ofInt 0) Result.ret { ntable0 @@ -411,7 +407,7 @@ def hashmap.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_main::hashmap::HashMap::{0}::remove]: backward function 0 -/ @@ -433,7 +429,7 @@ def hashmap.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.HashMap.remove_from_list_back T key l let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0 Result.ret { self with num_entries := i0, slots := v } @@ -442,60 +438,48 @@ def hashmap.HashMap.remove_back def hashmap.test1 : Result Unit := do let hm ← hashmap.HashMap.new U64 - let hm0 ← - hashmap.HashMap.insert U64 hm (Usize.ofInt 0 (by intlit)) - (U64.ofInt 42 (by intlit)) - let hm1 ← - hashmap.HashMap.insert U64 hm0 (Usize.ofInt 128 (by intlit)) - (U64.ofInt 18 (by intlit)) + let hm0 ← hashmap.HashMap.insert U64 hm (Usize.ofInt 0) (U64.ofInt 42) + let hm1 ← hashmap.HashMap.insert U64 hm0 (Usize.ofInt 128) (U64.ofInt 18) let hm2 ← - hashmap.HashMap.insert U64 hm1 (Usize.ofInt 1024 (by intlit)) - (U64.ofInt 138 (by intlit)) + hashmap.HashMap.insert U64 hm1 (Usize.ofInt 1024) (U64.ofInt 138) let hm3 ← - hashmap.HashMap.insert U64 hm2 (Usize.ofInt 1056 (by intlit)) - (U64.ofInt 256 (by intlit)) - let i ← hashmap.HashMap.get U64 hm3 (Usize.ofInt 128 (by intlit)) - if not (i = (U64.ofInt 18 (by intlit))) + hashmap.HashMap.insert U64 hm2 (Usize.ofInt 1056) (U64.ofInt 256) + let i ← hashmap.HashMap.get U64 hm3 (Usize.ofInt 128) + if not (i = (U64.ofInt 18)) then Result.fail Error.panic else do let hm4 ← - hashmap.HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit)) - (U64.ofInt 56 (by intlit)) - let i0 ← hashmap.HashMap.get U64 hm4 (Usize.ofInt 1024 (by intlit)) - if not (i0 = (U64.ofInt 56 (by intlit))) + hashmap.HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024) + (U64.ofInt 56) + let i0 ← hashmap.HashMap.get U64 hm4 (Usize.ofInt 1024) + if not (i0 = (U64.ofInt 56)) then Result.fail Error.panic else do - let x ← - hashmap.HashMap.remove U64 hm4 (Usize.ofInt 1024 (by intlit)) + let x ← hashmap.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.HashMap.remove_back U64 hm4 - (Usize.ofInt 1024 (by intlit)) - let i1 ← - hashmap.HashMap.get U64 hm5 (Usize.ofInt 0 (by intlit)) - if not (i1 = (U64.ofInt 42 (by intlit))) + hashmap.HashMap.remove_back U64 hm4 (Usize.ofInt 1024) + let i1 ← hashmap.HashMap.get U64 hm5 (Usize.ofInt 0) + if not (i1 = (U64.ofInt 42)) then Result.fail Error.panic else do - let i2 ← - hashmap.HashMap.get U64 hm5 - (Usize.ofInt 128 (by intlit)) - if not (i2 = (U64.ofInt 18 (by intlit))) + let i2 ← hashmap.HashMap.get U64 hm5 (Usize.ofInt 128) + if not (i2 = (U64.ofInt 18)) then Result.fail Error.panic else do let i3 ← - hashmap.HashMap.get U64 hm5 - (Usize.ofInt 1056 (by intlit)) - if not (i3 = (U64.ofInt 256 (by intlit))) + hashmap.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