Testing And Benchmarking in Idris

Here’s the translation of the Go testing and benchmarking example to Idris:

module Main

import Test.Unit
import System.Clock

-- We'll be testing this simple implementation of an
-- integer minimum. Typically, the code we're testing
-- would be in a source file named something like
-- `IntUtils.idr`, and the test file for it would then
-- be named `IntUtilsTest.idr`.

intMin : Int -> Int -> Int
intMin a b = if a < b then a else b

-- A test is created by writing a function with a name
-- beginning with `test`.

testIntMinBasic : IO ()
testIntMinBasic = do
  let ans = intMin 2 (-2)
  assertEq "IntMin(2, -2)" (-2) ans

-- Writing tests can be repetitive, so it's idiomatic to
-- use a table-driven style, where test inputs and
-- expected outputs are listed in a table and a single loop
-- walks over them and performs the test logic.

testIntMinTableDriven : IO ()
testIntMinTableDriven = do
  let tests = [
        (0, 1, 0),
        (1, 0, 0),
        (2, -2, -2),
        (0, -1, -1),
        (-1, 0, -1)
      ]
  
  for_ tests $ \(a, b, expected) => do
    let testname = "IntMin(" ++ show a ++ ", " ++ show b ++ ")"
    assertEq testname expected (intMin a b)

-- Benchmark tests in Idris are not as straightforward as in Go,
-- but we can create a simple benchmark function using the System.Clock module.

benchmarkIntMin : Int -> IO ()
benchmarkIntMin n = do
  start <- clockTime Monotonic
  for_ [1..n] $ \_ => ignore $ intMin 1 2
  end <- clockTime Monotonic
  let diff = timeDifference end start
  putStrLn $ "BenchmarkIntMin: " ++ show n ++ " iterations took " ++ show diff

-- Main function to run all tests and benchmarks
main : IO ()
main = do
  putStrLn "Running tests..."
  testIntMinBasic
  testIntMinTableDriven
  putStrLn "All tests passed!"
  
  putStrLn "\nRunning benchmark..."
  benchmarkIntMin 1000000

In this Idris translation:

We’ve implemented the intMin function as in the original Go code.
Test functions are created with names starting with test. We’ve translated both the basic test and the table-driven test.
Idris doesn’t have a built-in testing framework like Go’s testing package, so we’re using a hypothetical Test.Unit module with an assertEq function. In a real Idris project, you’d need to implement this or use an existing testing library.
For benchmarking, we’ve created a simple benchmarkIntMin function that runs the intMin function a specified number of times and measures the elapsed time. This is not as sophisticated as Go’s benchmarking tools, but it provides a basic way to measure performance.
The main function runs all tests and the benchmark.

To run this in Idris, you would typically compile the file and then execute the resulting binary:

$ idris -o TestIntMin TestIntMin.idr
$ ./TestIntMin
Running tests...
All tests passed!

Running benchmark...
BenchmarkIntMin: 1000000 iterations took 0.123456 seconds

Note that Idris is primarily a proof assistant and research language, so its testing and benchmarking capabilities are not as developed as those in Go. In a real-world scenario, you might need to use additional libraries or create more sophisticated testing and benchmarking utilities.

Embed Directive in Idris

Line Filters in Idris

Learn X By Example

Title here

Testing And Benchmarking in Idris