[Agda] Unit testing

[Alan Jeffrey]

Hi everyone,

Unit testing is very exciting. Oh yes it is. Wake up!

I knocked up a quick binding for the Agda JS back end to the QUnit unit 
testing framework (it's the unit testing framework used by jQuery). The 
results can be seen at:

   http://ect.bell-labs.com/who/ajeffrey/agda-frp-js/tests.html

And yes, those unit tests are being run in your browser.

The API for test suites is at:

 
https://github.com/agda/agda-frp-js/blob/master/test/agda/FRP/JS/QUnit.agda

For example, some quick and dirty tests for lists are at:

 
https://github.com/agda/agda-frp-js/blob/master/test/agda/FRP/JS/Test/List.agda

Just about the only interesting thing about the testing framework is 
that the type of an atomic test is:

   ok : String → (b : Bool) → {b✓ : True b} → Test

that is, the test is run both at compile time (by the True b optional 
argument) and at run time.

Of course, such unit tests are only really necessary to test the 
soundness of FFI bindings, because (er, of course) the compiler itself 
is sound.

It might be nice to bundle some such test framework in with the compiler 
build, to do regression tests of the GHC, Epic and JS back ends. 
Ideally, most of the tests could be shared. Is this something other back 
end maintainers are interested in?

A.