08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
43 lines
1,022 B
Text
43 lines
1,022 B
Text
def mkByteArray (n : Nat) : ByteArray := Id.run <| do
|
|
let mut r := {}
|
|
for i in *...n do
|
|
r := r.push (UInt8.ofNat i)
|
|
return r
|
|
|
|
def tst1 (n : Nat) (expected : UInt32) : IO Unit := do
|
|
let bs := mkByteArray n
|
|
let sum := bs.foldl (init := 0) fun s b => s + b.toUInt32
|
|
assert! sum == expected
|
|
IO.println sum
|
|
|
|
/-- info: 4950 -/
|
|
#guard_msgs in
|
|
#eval tst1 100 4950
|
|
|
|
def tst2 (n : Nat) (expected : UInt32) : IO Unit := do
|
|
let bs := mkByteArray n
|
|
let mut sum := 0
|
|
for b in bs do
|
|
sum := sum + b.toUInt32
|
|
assert! sum == expected
|
|
IO.println sum
|
|
|
|
/-- info: 4950 -/
|
|
#guard_msgs in
|
|
#eval tst2 100 4950
|
|
|
|
def tst3 (n : Nat) (expected : UInt32) : IO Unit := do
|
|
let bs := mkByteArray n
|
|
let mut sum := 0
|
|
for i in *...bs.size do
|
|
sum := sum + bs[i]!.toUInt32
|
|
assert! sum == expected
|
|
IO.println sum
|
|
|
|
/-- info: 4950 -/
|
|
#guard_msgs in
|
|
#eval tst3 100 4950
|
|
|
|
set_option trace.compiler.ir.result true in
|
|
def computeByteHash (bytes : ByteArray) :=
|
|
bytes.foldl (init := 1723) fun h b => mixHash h (hash b)
|