diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean (renamed from tests/lean/hashmap_on_disk/Hashmap/Primitives.lean) | 16 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Hashmap/Opaque.lean | 11 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain.lean (renamed from tests/lean/hashmap_on_disk/Hashmap.lean) | 0 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean (renamed from tests/lean/hashmap_on_disk/Hashmap/Funs.lean) | 211 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 13 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Types.lean (renamed from tests/lean/hashmap_on_disk/Hashmap/Types.lean) | 9 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Main.lean | 4 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/lakefile.lean | 6 |
8 files changed, 138 insertions, 132 deletions
diff --git a/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index d86c0423..9e72b708 100644 --- a/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -131,26 +131,28 @@ macro_rules def vec (α : Type u) := { l : List α // List.length l < USize.size } -def vec_new : result (vec α) := return ⟨ [], by { +def vec_new (α : Type u): result (vec α) := return ⟨ [], by { match USize.size, usize_size_eq with | _, Or.inl rfl => simp | _, Or.inr rfl => simp } ⟩ -def vec_len (v : vec α) : USize := +#check vec_new + +def vec_len (α : Type u) (v : vec α) : USize := let ⟨ v, l ⟩ := v USize.ofNatCore (List.length v) l #eval do - return (vec_len (<- @vec_new Nat)) + return (vec_len Nat (<- vec_new Nat)) -def vec_push_fwd (_ : vec α) (_ : α) : Unit := () +def vec_push_fwd (α : Type u) (_ : vec α) (_ : α) : Unit := () -- TODO: more precise error condition here for the fail case -- TODO: I originally wrote `List.length v.val < USize.size - 1`; how can one -- make the proof work in that case? Probably need to import tactics from -- mathlib to deal with inequalities... would love to see an example. -def vec_push_back (v : vec α) (x : α) : { res: result (vec α) // +def vec_push_back (α : Type u) (v : vec α) (x : α) : { res: result (vec α) // match res with | fail _ => True | ret v' => List.length v'.val = List.length v.val + 1} := if h : List.length v.val + 1 < USize.size then @@ -168,7 +170,7 @@ def vec_push_back (v : vec α) (x : α) : { res: result (vec α) // -- select the `val` field if the context provides a type annotation. We -- annotate `x`, which relieves us of having to write `.val` on the right-hand -- side of the monadic let. - let x: vec Nat ← vec_push_back (<- vec_new) 1 + let x: vec Nat ← vec_push_back Nat (<- vec_new Nat) 1 -- TODO: strengthen post-condition above and do a demo to show that we can -- safely eliminate the `fail` case - return (vec_len x) + return (vec_len Nat x) diff --git a/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean b/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean deleted file mode 100644 index 164995f0..00000000 --- a/tests/lean/hashmap_on_disk/Hashmap/Opaque.lean +++ /dev/null @@ -1,11 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [hashmap_main]: opaque function definitions -import Hashmap.Primitives -import Hashmap.Types - -/- [hashmap_main::hashmap_utils::deserialize] -/ -axiom hashmap_utils_deserialize_fwd: state → result (state × (hashmap_hash_map_t UInt64)) - -/- [hashmap_main::hashmap_utils::serialize] -/ -axiom hashmap_utils_serialize_fwd: hashmap_hash_map_t UInt64 -> state -> result (state × Unit) - diff --git a/tests/lean/hashmap_on_disk/Hashmap.lean b/tests/lean/hashmap_on_disk/HashmapMain.lean index e99d3a6f..e99d3a6f 100644 --- a/tests/lean/hashmap_on_disk/Hashmap.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain.lean diff --git a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index c67a37ff..3fb121d4 100644 --- a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -1,14 +1,11 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [hashmap_main]: function definitions -import Hashmap.Primitives -import Hashmap.Opaque -import Hashmap.Types - -open result -open hashmap_list_t +import Base.Primitives +import HashmapMain.Types +import HashmapMain.Opaque /- [hashmap_main::hashmap::hash_key] -/ -def hashmap_hash_key_fwd (k : USize) : result USize := ret k +def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap_hash_map_allocate_slots_loop_fwd @@ -16,13 +13,11 @@ def hashmap_hash_map_allocate_slots_loop_fwd result (vec (hashmap_list_t T)) := if n > (USize.ofNatCore 0 (by intlit)) - then do - let slots0: vec (hashmap_list_t T) <- @vec_push_back (hashmap_list_t T) slots HashmapListNil - let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) - hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 - else ret slots -termination_by hashmap_hash_map_allocate_slots_loop_fwd _ _ n => n -decreasing_by sorry + then ( + let slots0 <- vec_push_back (hashmap_list_t T) slots HashmapListNil in + let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) in + 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 @@ -41,13 +36,13 @@ def hashmap_hash_map_new_with_capacity_fwd let slots <- hashmap_hash_map_allocate_slots_fwd T v capacity in let i <- USize.checked_mul capacity max_load_dividend in let i0 <- USize.checked_div i max_load_divisor in - ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by simp)) (max_load_dividend, - max_load_divisor) i0 slots) + result.ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by intlit)) + (max_load_dividend, max_load_divisor) i0 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.ofNatCore 32 (by simp)) - (USize.ofNatCore 4 (by simp)) (USize.ofNatCore 5 (by simp)) + hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by intlit)) + (USize.ofNatCore 4 (by intlit)) (USize.ofNatCore 5 (by intlit)) /- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ def hashmap_hash_map_clear_slots_loop_fwd_back @@ -57,11 +52,11 @@ def hashmap_hash_map_clear_slots_loop_fwd_back let i0 <- vec_len (hashmap_list_t T) slots in if i < i0 then ( - let i1 <- USize.checked_add i (USize.ofNatCore 1 (by simp)) in + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) in let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i HashmapListNil in hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1) - else ret slots + else result.ret slots /- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ def hashmap_hash_map_clear_slots_fwd_back @@ -69,20 +64,20 @@ def hashmap_hash_map_clear_slots_fwd_back result (vec (hashmap_list_t T)) := hashmap_hash_map_clear_slots_loop_fwd_back T slots - (USize.ofNatCore 0 (by simp)) + (USize.ofNatCore 0 (by intlit)) /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ def hashmap_hash_map_clear_fwd_back (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := let v <- hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots in - ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by simp)) + result.ret (mkhashmap_hash_map_t (USize.ofNatCore 0 (by intlit)) self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) /- [hashmap_main::hashmap::HashMap::{0}::len] -/ def hashmap_hash_map_len_fwd (T : Type) (self : hashmap_hash_map_t T) : result USize := - ret self.hashmap_hash_map_num_entries + result.ret self.hashmap_hash_map_num_entries /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_loop_fwd @@ -90,9 +85,9 @@ def hashmap_hash_map_insert_in_list_loop_fwd match ls with | HashmapListCons ckey cvalue tl => if ckey = key - then ret false + then result.ret false else hashmap_hash_map_insert_in_list_loop_fwd T key value tl - | HashmapListNil => ret true + | HashmapListNil => result.ret true end /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -108,12 +103,12 @@ def hashmap_hash_map_insert_in_list_loop_back match ls with | HashmapListCons ckey cvalue tl => if ckey = key - then ret (HashmapListCons ckey value tl) + then result.ret (HashmapListCons ckey value tl) else ( let l <- hashmap_hash_map_insert_in_list_loop_back T key value tl in - ret (HashmapListCons ckey cvalue l)) + result.ret (HashmapListCons ckey cvalue l)) | HashmapListNil => - let l <- HashmapListNil in ret (HashmapListCons key value l) + let l <- HashmapListNil in result.ret (HashmapListCons key value l) end /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -138,25 +133,25 @@ def hashmap_hash_map_insert_no_resize_fwd_back if inserted then ( let i0 <- USize.checked_add self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by simp)) in + (USize.ofNatCore 1 (by intlit)) in let l0 <- hashmap_hash_map_insert_in_list_back T key value l in let v <- vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 in - ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor + result.ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)) else ( let l0 <- hashmap_hash_map_insert_in_list_back T key value l in let v <- vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 in - ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v)) /- [core::num::u32::{9}::MAX] -/ def core_num_u32_max_body : result UInt32 := - ret (UInt32.ofNatCore 4294967295 (by simp)) -def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body + result.ret (UInt32.ofNatCore 4294967295 (by intlit)) +def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ def hashmap_hash_map_move_elements_from_list_loop_fwd_back @@ -167,7 +162,7 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back | HashmapListCons k v tl => let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v in hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl - | HashmapListNil => ret ntable + | HashmapListNil => result.ret ntable end /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ @@ -190,11 +185,11 @@ def hashmap_hash_map_move_elements_loop_fwd_back let ls <- mem_replace_fwd (hashmap_list_t T) l HashmapListNil in let ntable0 <- hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls in - let i1 <- USize.checked_add i (USize.ofNatCore 1 (by simp)) in + let i1 <- USize.checked_add i (USize.ofNatCore 1 (by intlit)) in let l0 <- mem_replace_back (hashmap_list_t T) l HashmapListNil in let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i l0 in hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1) - else ret (ntable, slots) + else result.ret (ntable, slots) /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ def hashmap_hash_map_move_elements_fwd_back @@ -209,20 +204,20 @@ def hashmap_hash_map_try_resize_fwd_back (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := let max_usize <- scalar_cast U32 Usize core_num_u32_max_c in let capacity <- vec_len (hashmap_list_t T) self.hashmap_hash_map_slots in - let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by simp)) in + let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by intlit)) in let (i, i0) <- self.hashmap_hash_map_max_load_factor in let i1 <- USize.checked_div n1 i in if capacity <= i1 then ( - let i2 <- USize.checked_mul capacity (USize.ofNatCore 2 (by simp)) in + let i2 <- USize.checked_mul capacity (USize.ofNatCore 2 (by intlit)) in let ntable <- hashmap_hash_map_new_with_capacity_fwd T i2 i i0 in let (ntable0, _) <- hashmap_hash_map_move_elements_fwd_back T ntable - self.hashmap_hash_map_slots (USize.ofNatCore 0 (by simp)) in - ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) + self.hashmap_hash_map_slots (USize.ofNatCore 0 (by intlit)) in + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots)) else - ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) /- [hashmap_main::hashmap::HashMap::{0}::insert] -/ @@ -234,7 +229,7 @@ def hashmap_hash_map_insert_fwd_back let i <- hashmap_hash_map_len_fwd T self0 in if i > self0.hashmap_hash_map_max_load then hashmap_hash_map_try_resize_fwd_back T self0 - else ret self0 + else result.ret self0 /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ def hashmap_hash_map_contains_key_in_list_loop_fwd @@ -242,9 +237,9 @@ def hashmap_hash_map_contains_key_in_list_loop_fwd match ls with | HashmapListCons ckey t tl => if ckey = key - then ret true + then result.ret true else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl - | HashmapListNil => ret false + | HashmapListNil => result.ret false end /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ @@ -268,9 +263,9 @@ def hashmap_hash_map_get_in_list_loop_fwd match ls with | HashmapListCons ckey cvalue tl => if ckey = key - then ret cvalue + then result.ret cvalue else hashmap_hash_map_get_in_list_loop_fwd T key tl - | HashmapListNil => fail_ panic + | HashmapListNil => result.fail panic end /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ @@ -294,9 +289,9 @@ def hashmap_hash_map_get_mut_in_list_loop_fwd match ls with | HashmapListCons ckey cvalue tl => if ckey = key - then ret cvalue + then result.ret cvalue else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key - | HashmapListNil => fail_ panic + | HashmapListNil => result.fail panic end /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -306,25 +301,25 @@ def hashmap_hash_map_get_mut_in_list_fwd /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_loop_back - (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : + (T : Type) (ls : hashmap_list_t T) (key : USize) (ret : T) : result (hashmap_list_t T) := match ls with | HashmapListCons ckey cvalue tl => if ckey = key - then ret (HashmapListCons ckey ret0 tl) + then result.ret (HashmapListCons ckey ret tl) else ( - let l <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 in - ret (HashmapListCons ckey cvalue l)) - | HashmapListNil => fail_ panic + let l <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret in + result.ret (HashmapListCons ckey cvalue l)) + | HashmapListNil => result.fail panic end /- [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) : + (T : Type) (ls : hashmap_list_t T) (key : USize) (ret : T) : result (hashmap_list_t T) := - hashmap_hash_map_get_mut_in_list_loop_back T ls key ret0 + hashmap_hash_map_get_mut_in_list_loop_back T ls key ret /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ def hashmap_hash_map_get_mut_fwd @@ -339,7 +334,7 @@ def hashmap_hash_map_get_mut_fwd /- [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) : + (T : Type) (self : hashmap_hash_map_t T) (key : USize) (ret : T) : result (hashmap_hash_map_t T) := let hash <- hashmap_hash_key_fwd key in @@ -348,11 +343,11 @@ def hashmap_hash_map_get_mut_back let l <- vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod in - let l0 <- hashmap_hash_map_get_mut_in_list_back T l key ret0 in + let l0 <- hashmap_hash_map_get_mut_in_list_back T l key ret in let v <- vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 in - ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ @@ -366,11 +361,11 @@ def hashmap_hash_map_remove_from_list_loop_fwd mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl) HashmapListNil in match mv_ls with - | HashmapListCons i cvalue tl0 => ret (@some cvalue) - | HashmapListNil => fail_ panic + | HashmapListCons i cvalue tl0 => result.ret (@some cvalue) + | HashmapListNil => result.fail panic end else hashmap_hash_map_remove_from_list_loop_fwd T key tl - | HashmapListNil => ret @none + | HashmapListNil => result.ret @none end /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ @@ -391,13 +386,13 @@ def hashmap_hash_map_remove_from_list_loop_back mem_replace_fwd (hashmap_list_t T) (HashmapListCons ckey t tl) HashmapListNil in match mv_ls with - | HashmapListCons i cvalue tl0 => ret tl0 - | HashmapListNil => fail_ panic + | HashmapListCons i cvalue tl0 => result.ret tl0 + | HashmapListNil => result.fail panic end else ( let l <- hashmap_hash_map_remove_from_list_loop_back T key tl in - ret (HashmapListCons ckey t l)) - | HashmapListNil => ret HashmapListNil + result.ret (HashmapListCons ckey t l)) + | HashmapListNil => result.ret HashmapListNil end /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ @@ -418,11 +413,11 @@ def hashmap_hash_map_remove_fwd in let x <- hashmap_hash_map_remove_from_list_fwd T key l in match x with - | @none => ret @none + | @none => result.ret @none | @some x0 => let _ <- USize.checked_sub self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by simp)) in - ret (@some x0) + (USize.ofNatCore 1 (by intlit)) in + result.ret (@some x0) end /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ @@ -443,93 +438,93 @@ def hashmap_hash_map_remove_back let v <- vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 in - ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries + result.ret (mkhashmap_hash_map_t self.hashmap_hash_map_num_entries self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) | @some x0 => let i0 <- USize.checked_sub self.hashmap_hash_map_num_entries - (USize.ofNatCore 1 (by simp)) in + (USize.ofNatCore 1 (by intlit)) in let l0 <- hashmap_hash_map_remove_from_list_back T key l in let v <- vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod l0 in - ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor + result.ret (mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) end /- [hashmap_main::hashmap::test1] -/ -def hashmap_test1_fwd : result unit := +def hashmap_test1_fwd : result Unit := let hm <- hashmap_hash_map_new_fwd UInt64 in let hm0 <- - hashmap_hash_map_insert_fwd_back UInt64 hm (USize.ofNatCore 0 (by simp)) - (UInt64.ofNatCore 42 (by simp)) in + hashmap_hash_map_insert_fwd_back UInt64 hm (USize.ofNatCore 0 (by intlit)) + (UInt64.ofNatCore 42 (by intlit)) in let hm1 <- - hashmap_hash_map_insert_fwd_back UInt64 hm0 (USize.ofNatCore 128 (by simp)) - (UInt64.ofNatCore 18 (by simp)) in + hashmap_hash_map_insert_fwd_back UInt64 hm0 + (USize.ofNatCore 128 (by intlit)) (UInt64.ofNatCore 18 (by intlit)) in let hm2 <- hashmap_hash_map_insert_fwd_back UInt64 hm1 - (USize.ofNatCore 1024 (by simp)) (UInt64.ofNatCore 138 (by simp)) in + (USize.ofNatCore 1024 (by intlit)) (UInt64.ofNatCore 138 (by intlit)) in let hm3 <- hashmap_hash_map_insert_fwd_back UInt64 hm2 - (USize.ofNatCore 1056 (by simp)) (UInt64.ofNatCore 256 (by simp)) in - let i <- hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by simp)) - in - if not (i = (UInt64.ofNatCore 18 (by simp))) - then fail_ panic + (USize.ofNatCore 1056 (by intlit)) (UInt64.ofNatCore 256 (by intlit)) in + let i <- + hashmap_hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by intlit)) in + if not (i = (UInt64.ofNatCore 18 (by intlit))) + then result.fail panic else ( let hm4 <- - hashmap_hash_map_get_mut_back UInt64 hm3 (USize.ofNatCore 1024 (by simp)) - (UInt64.ofNatCore 56 (by simp)) in + hashmap_hash_map_get_mut_back UInt64 hm3 + (USize.ofNatCore 1024 (by intlit)) (UInt64.ofNatCore 56 (by intlit)) in let i0 <- - hashmap_hash_map_get_fwd UInt64 hm4 (USize.ofNatCore 1024 (by simp)) in - if not (i0 = (UInt64.ofNatCore 56 (by simp))) - then fail_ panic + hashmap_hash_map_get_fwd UInt64 hm4 (USize.ofNatCore 1024 (by intlit)) in + if not (i0 = (UInt64.ofNatCore 56 (by intlit))) + then result.fail panic else ( let x <- - hashmap_hash_map_remove_fwd UInt64 hm4 (USize.ofNatCore 1024 (by simp)) - in + hashmap_hash_map_remove_fwd UInt64 hm4 + (USize.ofNatCore 1024 (by intlit)) in match x with - | @none => fail_ panic + | @none => result.fail panic | @some x0 => - if not (x0 = (UInt64.ofNatCore 56 (by simp))) - then fail_ panic + if not (x0 = (UInt64.ofNatCore 56 (by intlit))) + then result.fail panic else ( let hm5 <- hashmap_hash_map_remove_back UInt64 hm4 - (USize.ofNatCore 1024 (by simp)) in + (USize.ofNatCore 1024 (by intlit)) in let i1 <- - hashmap_hash_map_get_fwd UInt64 hm5 (USize.ofNatCore 0 (by simp)) + hashmap_hash_map_get_fwd UInt64 hm5 (USize.ofNatCore 0 (by intlit)) in - if not (i1 = (UInt64.ofNatCore 42 (by simp))) - then fail_ panic + if not (i1 = (UInt64.ofNatCore 42 (by intlit))) + then result.fail panic else ( let i2 <- hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 128 (by simp)) in - if not (i2 = (UInt64.ofNatCore 18 (by simp))) - then fail_ panic + (USize.ofNatCore 128 (by intlit)) in + if not (i2 = (UInt64.ofNatCore 18 (by intlit))) + then result.fail panic else ( let i3 <- hashmap_hash_map_get_fwd UInt64 hm5 - (USize.ofNatCore 1056 (by simp)) in - if not (i3 = (UInt64.ofNatCore 256 (by simp))) - then fail_ panic - else ret ()))) + (USize.ofNatCore 1056 (by intlit)) in + if not (i3 = (UInt64.ofNatCore 256 (by intlit))) + then result.fail panic + else result.ret ()))) end)) /- Unit test for [hashmap_main::hashmap::test1] -/ -#assert (hashmap_test1_fwd = ret ()) +#assert (hashmap_test1_fwd = result.ret ()) /- [hashmap_main::insert_on_disk] -/ def insert_on_disk_fwd - (key : USize) (value : UInt64) (st : state) : result (state × unit) := + (key : USize) (value : UInt64) (st : state) : result (state × Unit) := let (st0, hm) <- hashmap_utils_deserialize_fwd st in let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value in let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 in - ret (st1, ()) + result.ret (st1, ()) /- [hashmap_main::main] -/ -def main_fwd : result unit := ret () +def main_fwd : result Unit := result.ret () /- Unit test for [hashmap_main::main] -/ -#assert (main_fwd = ret ()) +#assert (main_fwd = result.ret ()) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean new file mode 100644 index 00000000..87b10c59 --- /dev/null +++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean @@ -0,0 +1,13 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: opaque function definitions +import Base.Primitives +import HashmapMain.Types + +/- [hashmap_main::hashmap_utils::deserialize] -/ +axiom hashmap_utils_deserialize_fwd + : state -> result (state × (hashmap_hash_map_t UInt64)) + +/- [hashmap_main::hashmap_utils::serialize] -/ +axiom hashmap_utils_serialize_fwd + : hashmap_hash_map_t UInt64 -> state -> result (state × Unit) + diff --git a/tests/lean/hashmap_on_disk/Hashmap/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean index 90022fe5..1b8f8954 100644 --- a/tests/lean/hashmap_on_disk/Hashmap/Types.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -1,6 +1,6 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [hashmap_main]: type definitions -import Hashmap.Primitives +import Base.Primitives /- [hashmap_main::hashmap::List] -/ inductive hashmap_list_t (T : Type) := @@ -9,15 +9,18 @@ inductive hashmap_list_t (T : Type) := /- [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) + /- [core::num::u32::{9}::MAX] -/ def core_num_u32_max_body : result UInt32 := - return (UInt32.ofNatCore 4294967295 (by simp)) + result.ret (UInt32.ofNatCore 4294967295 (by intlit)) def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) /- The state type used in the state-error monad -/ -axiom state : Type
\ No newline at end of file +axiom state : Type + diff --git a/tests/lean/hashmap_on_disk/Main.lean b/tests/lean/hashmap_on_disk/Main.lean index 7bde1315..9fe6cf4a 100644 --- a/tests/lean/hashmap_on_disk/Main.lean +++ b/tests/lean/hashmap_on_disk/Main.lean @@ -1,5 +1,5 @@ -import «Hashmap» -import Hashmap.Primitives +import «HashmapMain» +import Base.Primitives def main : IO Unit := IO.println s!"Hello, {hello}!" diff --git a/tests/lean/hashmap_on_disk/lakefile.lean b/tests/lean/hashmap_on_disk/lakefile.lean index d2a31ffe..5b9adebb 100644 --- a/tests/lean/hashmap_on_disk/lakefile.lean +++ b/tests/lean/hashmap_on_disk/lakefile.lean @@ -5,7 +5,11 @@ package «hashmap» { -- add package configuration options here } -lean_lib «Hashmap» { +lean_lib «HashmapMain» { + -- add library configuration options here +} + +lean_lib «Base» { -- add library configuration options here } |