summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-10-26 15:06:36 +0200
committerSon Ho2023-10-26 15:06:36 +0200
commit7ffcb8e9c5c03f198362fd27bd42f30064541509 (patch)
treedaddf078ec50f175c2cf4f9124e63c433be04aef
parent76e7a6e4c4ead2e48bc56118b38347b59f4f30db (diff)
Fix some issues and regenerate the HashmapMain example for Lean
-rw-r--r--compiler/ExtractBuiltin.ml11
-rw-r--r--compiler/FunsAnalysis.ml11
-rw-r--r--compiler/InterpreterExpressions.ml3
-rw-r--r--tests/lean/HashmapMain/Funs.lean226
-rw-r--r--tests/lean/HashmapMain/Types.lean2
5 files changed, 147 insertions, 106 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 363955bf..2dbacce3 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -381,6 +381,7 @@ let builtin_fun_effects =
let int_funs = List.concat int_funs in
let no_fail_no_state_funs =
[
+ (* TODO: redundancy with the funs information below *)
"alloc::vec::Vec::new";
"alloc::vec::Vec::len";
"alloc::boxed::Box::deref";
@@ -395,7 +396,15 @@ let builtin_fun_effects =
(fun n -> (n, { can_fail = false; stateful = false }))
no_fail_no_state_funs
in
- let no_state_funs = [ "alloc::vec::Vec::push" ] in
+ let no_state_funs =
+ [
+ (* TODO: redundancy with the funs information below *)
+ "alloc::vec::Vec::push";
+ "alloc::vec::Vec::index";
+ "alloc::vec::Vec::index_mut";
+ "alloc::vec::Vec::index_mut_back";
+ ]
+ in
let no_state_funs =
List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs
in
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 9eac3e6f..69c0df71 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -76,6 +76,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
object (self)
inherit [_] iter_statement as super
method may_fail b = can_fail := !can_fail || b
+ method maybe_stateful b = stateful := !stateful || b
method! visit_Assert env a =
self#may_fail true;
@@ -126,14 +127,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
| None ->
let info_can_fail, info_stateful =
match builtin_info with
- | None -> (true, false)
+ | None -> (true, use_state)
| Some { can_fail; stateful } -> (can_fail, stateful)
in
obj#may_fail info_can_fail;
- stateful :=
- (not f.is_global_decl_body)
- && use_state
- && not (has_builtin_info && not info_stateful)
+ obj#maybe_stateful
+ (if f.is_global_decl_body then false
+ else if not use_state then false
+ else info_stateful)
| Some body -> obj#visit_statement () body.body
in
List.iter visit_fun d;
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 341e97eb..245f3b77 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -144,7 +144,8 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
(match v.V.ty with
| T.Adt (T.Assumed T.Box, _) ->
raise (Failure "Can't copy an assumed value other than Option")
- | T.Adt (T.AdtId _, _) -> assert allow_adt_copy
+ | T.Adt (T.AdtId _, _) as ty ->
+ assert (allow_adt_copy || ty_is_primitively_copyable ty)
| T.Adt (T.Tuple, _) -> () (* Ok *)
| T.Adt
( T.Assumed (Slice | T.Array),
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 848b1a35..74fa8653 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -13,21 +13,21 @@ def hashmap.hash_key (k : Usize) : Result Usize :=
/- [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))
+ (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) :
+ Result (alloc.vec.Vec (hashmap.List T))
:=
- if n > (Usize.ofInt 0)
+ if n > 0#usize
then
do
- let slots0 ← Vec.push (hashmap.List T) slots hashmap.List.Nil
- let n0 ← n - (Usize.ofInt 1)
+ let slots0 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil
+ let n0 ← n - 1#usize
hashmap.HashMap.allocate_slots_loop T slots0 n0
else Result.ret slots
/- [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))
+ (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) :
+ Result (alloc.vec.Vec (hashmap.List T))
:=
hashmap.HashMap.allocate_slots_loop T slots n
@@ -38,13 +38,13 @@ def hashmap.HashMap.new_with_capacity
Result (hashmap.HashMap T)
:=
do
- let v := Vec.new (hashmap.List T)
+ let v := alloc.vec.Vec.new (hashmap.List T)
let slots ← hashmap.HashMap.allocate_slots T v capacity
let i ← capacity * max_load_dividend
let i0 ← i / max_load_divisor
Result.ret
{
- num_entries := (Usize.ofInt 0),
+ num_entries := 0#usize,
max_load_factor := (max_load_dividend, max_load_divisor),
max_load := i0,
slots := slots
@@ -52,22 +52,23 @@ 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) (Usize.ofInt 4)
- (Usize.ofInt 5)
+ hashmap.HashMap.new_with_capacity T 32#usize 4#usize 5#usize
/- [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))
+ (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
+ Result (alloc.vec.Vec (hashmap.List T))
:=
- let i0 := Vec.len (hashmap.List T) slots
+ let i0 := alloc.vec.Vec.len (hashmap.List T) slots
if i < i0
then
do
- let i1 ← i + (Usize.ofInt 1)
+ let i1 ← i + 1#usize
let slots0 ←
- Vec.index_mut_back (hashmap.List T) slots i hashmap.List.Nil
+ alloc.vec.Vec.index_mut_back (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List
+ T)) slots i hashmap.List.Nil
hashmap.HashMap.clear_loop T slots0 i1
else Result.ret slots
@@ -76,8 +77,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)
- Result.ret { self with num_entries := (Usize.ofInt 0), slots := v }
+ let v ← hashmap.HashMap.clear_loop T self.slots 0#usize
+ Result.ret { self with num_entries := 0#usize, slots := v }
/- [hashmap_main::hashmap::HashMap::{0}::len]: forward function -/
def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize :=
@@ -130,21 +131,30 @@ def hashmap.HashMap.insert_no_resize
:=
do
let hash ← hashmap.hash_key key
- let i := Vec.len (hashmap.List T) self.slots
+ let i := alloc.vec.Vec.len (hashmap.List T) self.slots
let hash_mod ← hash % i
- let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod
+ let l ←
+ alloc.vec.Vec.index_mut (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (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.num_entries + (Usize.ofInt 1)
+ let i0 ← self.num_entries + 1#usize
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
+ let v ←
+ alloc.vec.Vec.index_mut_back (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (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.slots hash_mod l0
+ let v ←
+ alloc.vec.Vec.index_mut_back (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List
+ T)) self.slots hash_mod l0
Result.ret { self with slots := v }
/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
@@ -171,29 +181,35 @@ def hashmap.HashMap.move_elements_from_list
/- [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)))
+ (T : Type) (ntable : hashmap.HashMap T)
+ (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
+ Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T)))
:=
- let i0 := Vec.len (hashmap.List T) slots
+ let i0 := alloc.vec.Vec.len (hashmap.List T) slots
if i < i0
then
do
- let l ← Vec.index_mut (hashmap.List T) slots i
- let ls := mem.replace (hashmap.List T) l hashmap.List.Nil
+ let l ←
+ alloc.vec.Vec.index_mut (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List
+ T)) slots i
+ let ls := core.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)
- 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 i1 ← i + 1#usize
+ let l0 := core.mem.replace_back (hashmap.List T) l hashmap.List.Nil
+ let slots0 ←
+ alloc.vec.Vec.index_mut_back (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List
+ T)) slots i l0
hashmap.HashMap.move_elements_loop T ntable0 slots0 i1
else Result.ret (ntable, slots)
/- [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)))
+ (T : Type) (ntable : hashmap.HashMap T)
+ (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
+ Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T)))
:=
hashmap.HashMap.move_elements_loop T ntable slots i
@@ -203,17 +219,17 @@ def hashmap.HashMap.try_resize
(T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
do
let max_usize ← Scalar.cast .Usize core_u32_max
- let capacity := Vec.len (hashmap.List T) self.slots
- let n1 ← max_usize / (Usize.ofInt 2)
+ let capacity := alloc.vec.Vec.len (hashmap.List T) self.slots
+ let n1 ← max_usize / 2#usize
let (i, i0) := self.max_load_factor
let i1 ← n1 / i
if capacity <= i1
then
do
- let i2 ← capacity * (Usize.ofInt 2)
+ let i2 ← capacity * 2#usize
let ntable ← hashmap.HashMap.new_with_capacity T i2 i i0
let (ntable0, _) ←
- hashmap.HashMap.move_elements T ntable self.slots (Usize.ofInt 0)
+ hashmap.HashMap.move_elements T ntable self.slots 0#usize
Result.ret
{
ntable0
@@ -255,9 +271,12 @@ 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.slots
+ let i := alloc.vec.Vec.len (hashmap.List T) self.slots
let hash_mod ← hash % i
- let l ← Vec.index_shared (hashmap.List T) self.slots hash_mod
+ let l ←
+ alloc.vec.Vec.index (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (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 -/
@@ -280,9 +299,12 @@ 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.slots
+ let i := alloc.vec.Vec.len (hashmap.List T) self.slots
let hash_mod ← hash % i
- let l ← Vec.index_shared (hashmap.List T) self.slots hash_mod
+ let l ←
+ alloc.vec.Vec.index (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (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 -/
@@ -327,9 +349,12 @@ 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.slots
+ let i := alloc.vec.Vec.len (hashmap.List T) self.slots
let hash_mod ← hash % i
- let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod
+ let l ←
+ alloc.vec.Vec.index_mut (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (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 -/
@@ -339,11 +364,17 @@ def hashmap.HashMap.get_mut_back
:=
do
let hash ← hashmap.hash_key key
- let i := Vec.len (hashmap.List T) self.slots
+ let i := alloc.vec.Vec.len (hashmap.List T) self.slots
let hash_mod ← hash % i
- let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod
+ let l ←
+ alloc.vec.Vec.index_mut (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (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.slots hash_mod l0
+ let v ←
+ alloc.vec.Vec.index_mut_back (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (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 -/
@@ -354,13 +385,13 @@ divergent def hashmap.HashMap.remove_from_list_loop
if ckey = key
then
let mv_ls :=
- mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl)
+ core.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.Cons i cvalue tl0 => Result.ret (some cvalue)
| hashmap.List.Nil => Result.fail Error.panic
else hashmap.HashMap.remove_from_list_loop T key tl
- | hashmap.List.Nil => Result.ret Option.none
+ | hashmap.List.Nil => Result.ret none
/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function -/
def hashmap.HashMap.remove_from_list
@@ -375,7 +406,7 @@ divergent def hashmap.HashMap.remove_from_list_loop_back
if ckey = key
then
let mv_ls :=
- mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl)
+ core.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
@@ -396,16 +427,18 @@ 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.slots
+ let i := alloc.vec.Vec.len (hashmap.List T) self.slots
let hash_mod ← hash % i
- let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod
+ let l ←
+ alloc.vec.Vec.index_mut (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (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.num_entries - (Usize.ofInt 1)
- Result.ret (Option.some x0)
+ | none => Result.ret none
+ | some x0 => do
+ let _ ← self.num_entries - 1#usize
+ Result.ret (some x0)
/- [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 -/
def hashmap.HashMap.remove_back
@@ -414,75 +447,75 @@ def hashmap.HashMap.remove_back
:=
do
let hash ← hashmap.hash_key key
- let i := Vec.len (hashmap.List T) self.slots
+ let i := alloc.vec.Vec.len (hashmap.List T) self.slots
let hash_mod ← hash % i
- let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod
+ let l ←
+ alloc.vec.Vec.index_mut (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List T))
+ self.slots hash_mod
let x ← hashmap.HashMap.remove_from_list T key l
match x with
- | Option.none =>
+ | none =>
do
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
+ let v ←
+ alloc.vec.Vec.index_mut_back (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (hashmap.List
+ T)) self.slots hash_mod l0
Result.ret { self with slots := v }
- | Option.some x0 =>
+ | some x0 =>
do
- let i0 ← self.num_entries - (Usize.ofInt 1)
+ let i0 ← self.num_entries - 1#usize
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
+ let v ←
+ alloc.vec.Vec.index_mut_back (hashmap.List T) Usize
+ (core.slice.index.usize.coresliceindexSliceIndexInst (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 :=
do
let hm ← hashmap.HashMap.new U64
- 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) (U64.ofInt 138)
- let hm3 ←
- 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))
+ let hm0 ← hashmap.HashMap.insert U64 hm 0#usize 42#u64
+ let hm1 ← hashmap.HashMap.insert U64 hm0 128#usize 18#u64
+ let hm2 ← hashmap.HashMap.insert U64 hm1 1024#usize 138#u64
+ let hm3 ← hashmap.HashMap.insert U64 hm2 1056#usize 256#u64
+ let i ← hashmap.HashMap.get U64 hm3 128#usize
+ if not (i = 18#u64)
then Result.fail Error.panic
else
do
- let hm4 ←
- 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))
+ let hm4 ← hashmap.HashMap.get_mut_back U64 hm3 1024#usize 56#u64
+ let i0 ← hashmap.HashMap.get U64 hm4 1024#usize
+ if not (i0 = 56#u64)
then Result.fail Error.panic
else
do
- let x ← hashmap.HashMap.remove U64 hm4 (Usize.ofInt 1024)
+ let x ← hashmap.HashMap.remove U64 hm4 1024#usize
match x with
- | Option.none => Result.fail Error.panic
- | Option.some x0 =>
- if not (x0 = (U64.ofInt 56))
+ | none => Result.fail Error.panic
+ | some x0 =>
+ if not (x0 = 56#u64)
then Result.fail Error.panic
else
do
- let hm5 ←
- 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))
+ let hm5 ← hashmap.HashMap.remove_back U64 hm4 1024#usize
+ let i1 ← hashmap.HashMap.get U64 hm5 0#usize
+ if not (i1 = 42#u64)
then Result.fail Error.panic
else
do
- let i2 ← hashmap.HashMap.get U64 hm5 (Usize.ofInt 128)
- if not (i2 = (U64.ofInt 18))
+ let i2 ← hashmap.HashMap.get U64 hm5 128#usize
+ if not (i2 = 18#u64)
then Result.fail Error.panic
else
do
- let i3 ←
- hashmap.HashMap.get U64 hm5 (Usize.ofInt 1056)
- if not (i3 = (U64.ofInt 256))
+ let i3 ← hashmap.HashMap.get U64 hm5 1056#usize
+ if not (i3 = 256#u64)
then Result.fail Error.panic
else Result.ret ()
-/- Unit test for [hashmap_main::hashmap::test1] -/
-#assert (hashmap.test1 == .ret ())
-
/- [hashmap_main::insert_on_disk]: forward function -/
def insert_on_disk
(key : Usize) (value : U64) (st : State) : Result (State × Unit) :=
@@ -496,7 +529,4 @@ def insert_on_disk
def main : Result Unit :=
Result.ret ()
-/- Unit test for [hashmap_main::main] -/
-#assert (main == .ret ())
-
end hashmap_main
diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean
index 2b5cbd6c..065c109b 100644
--- a/tests/lean/HashmapMain/Types.lean
+++ b/tests/lean/HashmapMain/Types.lean
@@ -15,7 +15,7 @@ structure hashmap.HashMap (T : Type) where
num_entries : Usize
max_load_factor : (Usize × Usize)
max_load : Usize
- slots : Vec (hashmap.List T)
+ slots : alloc.vec.Vec (hashmap.List T)
/- The state type used in the state-error monad -/
axiom State : Type