Unit Tests as a Type Provider
Fun code snippet
Idris type providers run an IO action while the module is being compiled. I used one to run a list of assertions: each passing one prints “pass”, and the first failing one returns an Error with its description, which makes compilation fail.
module TestProvider
%default total
%access export
compileTest : List (Bool, String) -> IO (Provider String)
compileTest [] = pure $ Provide "success"
compileTest ((True, _) :: xs) = do
printLn "pass"
compileTest xs
compileTest ((False, description) :: xs) = do
printLn "failed"
pure $ Error description
module Test
import TestProvider
%default total
%language TypeProviders
add : Int -> Int -> Int
add x y = 0
%provide (result : String) with compileTest [
(add 1 2 == 0, "1 + 2 = 3")
, (add 1 2 == 0, "1 + 2 = 3")
, (add 1 2 == 0, "1 + 2 = 3")
]
Here add is just a stub that returns 0, and the assertions match it, so the module compiles.