diff --git a/tests/bench/hashmap.lean b/tests/bench/hashmap.lean index 80e5cfefec..b33272fdb6 100644 --- a/tests/bench/hashmap.lean +++ b/tests/bench/hashmap.lean @@ -34,10 +34,10 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n := .defaultImplementation -def mkMapWithCap (seed : UInt64) (size : Nat) : Std.HashMap UInt64 String := Id.run do +def mkMapWithCap (seed : UInt64) (size : Nat) : Std.HashMap UInt64 UInt64 := Id.run do let mut map := Std.HashMap.emptyWithCapacity size for val in iterRand seed |>.take size |>.allowNontermination do - map := map.insert val s!"{val}" + map := map.insert val val return map def timeNanos (reps : Nat) (x : IO Unit) : IO Float := do @@ -105,7 +105,7 @@ def benchInsertIfNewHit (seed : UInt64) (size : Nat) : IO Float := do let mut map := map while todo != 0 do for val in iterRand seed |>.take size |>.allowNontermination do - map := map.insertIfNew val s!"{val}" + map := map.insertIfNew val val if map.size != size then throw <| .userError "Fail" todo := todo - size @@ -122,7 +122,7 @@ def benchInsertHit (seed : UInt64) (size : Nat) : IO Float := do let mut map := map while todo != 0 do for val in iterRand seed |>.take size |>.allowNontermination do - map := map.insert val s!"{val}" + map := map.insert val val if map.size != size then throw <| .userError "Fail" todo := todo - size @@ -170,7 +170,7 @@ def benchEraseInsert (seed : UInt64) (size : Nat) : IO Float := do let mut todo := checks while todo != 0 do for (eraseVal, newVal) in eraseIter.zip newIter |>.take size |>.allowNontermination do - map := map.erase eraseVal |>.insert newVal s!"{newVal}" + map := map.erase eraseVal |>.insert newVal newVal if map.size != size then throw <| .userError "Fail" todo := todo - size diff --git a/tests/bench/phashmap.lean b/tests/bench/phashmap.lean index 121743c97a..967ed7340e 100644 --- a/tests/bench/phashmap.lean +++ b/tests/bench/phashmap.lean @@ -34,10 +34,10 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n := .defaultImplementation -def mkMapWithCap (seed : UInt64) (size : Nat) : Lean.PersistentHashMap UInt64 String := Id.run do +def mkMapWithCap (seed : UInt64) (size : Nat) : Lean.PersistentHashMap UInt64 UInt64 := Id.run do let mut map := Lean.PersistentHashMap.empty for val in iterRand seed |>.take size |>.allowNontermination do - map := map.insert val s!"{val}" + map := map.insert val val return map def timeNanos (reps : Nat) (x : IO Unit) : IO Float := do @@ -105,7 +105,7 @@ def benchInsertHit (seed : UInt64) (size : Nat) : IO Float := do let mut map := map while todo != 0 do for val in iterRand seed |>.take size |>.allowNontermination do - map := map.insert val s!"{val}" + map := map.insert val val if map.isEmpty then throw <| .userError "Fail" todo := todo - size @@ -158,7 +158,7 @@ def benchEraseInsert (seed : UInt64) (size : Nat) : IO Float := do let mut todo := checks while todo != 0 do for (eraseVal, newVal) in eraseIter.zip newIter |>.take size |>.allowNontermination do - map := map.erase eraseVal |>.insert newVal s!"{newVal}" + map := map.erase eraseVal |>.insert newVal newVal if map.isEmpty then throw <| .userError "Fail" todo := todo - size diff --git a/tests/bench/treemap.lean b/tests/bench/treemap.lean index e18bde71b1..b1b242b5df 100644 --- a/tests/bench/treemap.lean +++ b/tests/bench/treemap.lean @@ -31,10 +31,10 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n := .defaultImplementation -def mkMap (seed : UInt64) (size : Nat) : Std.TreeMap UInt64 String := Id.run do +def mkMap (seed : UInt64) (size : Nat) : Std.TreeMap UInt64 UInt64 := Id.run do let mut map := {} for val in iterRand seed |>.take size |>.allowNontermination do - map := map.insert val s!"{val}" + map := map.insert val val return map def timeNanos (reps : Nat) (x : IO Unit) : IO Float := do @@ -102,7 +102,7 @@ def benchInsertIfNewHit (seed : UInt64) (size : Nat) : IO Float := do let mut map := map while todo != 0 do for val in iterRand seed |>.take size |>.allowNontermination do - map := map.insertIfNew val s!"{val}" + map := map.insertIfNew val val if map.size != size then throw <| .userError "Fail" todo := todo - size @@ -119,7 +119,7 @@ def benchInsertHit (seed : UInt64) (size : Nat) : IO Float := do let mut map := map while todo != 0 do for val in iterRand seed |>.take size |>.allowNontermination do - map := map.insert val s!"{val}" + map := map.insert val val if map.size != size then throw <| .userError "Fail" todo := todo - size @@ -187,7 +187,7 @@ def benchEraseInsert (seed : UInt64) (size : Nat) : IO Float := do let mut todo := checks while todo != 0 do for (eraseVal, newVal) in eraseIter.zip newIter |>.take size |>.allowNontermination do - map := map.erase eraseVal |>.insert newVal s!"{newVal}" + map := map.erase eraseVal |>.insert newVal newVal if map.size != size then throw <| .userError "Fail" todo := todo - size