mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-01 06:12:57 +03:00
43d323f685
Works by running all possible elaborators and checking that exactly one succeeds. Still to do: pruning the list of elaborators by target type, dealing with 'UniqueDefault', checking that delaying on failure works as it should.
50 lines
1.4 KiB
Idris
50 lines
1.4 KiB
Idris
module Main
|
|
|
|
import System
|
|
|
|
%default covering
|
|
|
|
ttimpTests : List String
|
|
ttimpTests
|
|
= ["basic001", "basic002", "basic003", "basic004", "basic005",
|
|
"eta001", "eta002",
|
|
"perf001", "perf002", "perf003"]
|
|
|
|
chdir : String -> IO Bool
|
|
chdir dir
|
|
= do ok <- foreign FFI_C "chdir" (String -> IO Int) dir
|
|
pure (ok == 0)
|
|
|
|
fail : String -> IO ()
|
|
fail err
|
|
= do putStrLn err
|
|
exitWith (ExitFailure 1)
|
|
|
|
runTest : String -> String -> String -> IO Bool
|
|
runTest dir prog test
|
|
= do chdir (dir ++ "/" ++ test)
|
|
putStr $ dir ++ "/" ++ test ++ ": "
|
|
system $ "sh ./run " ++ prog ++ " > output"
|
|
Right out <- readFile "output"
|
|
| Left err => do print err
|
|
pure False
|
|
Right exp <- readFile "expected"
|
|
| Left err => do print err
|
|
pure False
|
|
if (out == exp)
|
|
then putStrLn "success"
|
|
else putStrLn "FAILURE"
|
|
chdir "../.."
|
|
pure (out == exp)
|
|
|
|
main : IO ()
|
|
main
|
|
= do [_, ttimp] <- getArgs
|
|
| _ => do putStrLn "Usage: runtests [ttimp path]"
|
|
ttimps <- traverse (runTest "ttimp" ttimp) ttimpTests
|
|
-- blods <- traverse (runTest "blodwen" blodwen) blodwenTests
|
|
if (any not ttimps)
|
|
then exitWith (ExitFailure 1)
|
|
else exitWith ExitSuccess
|
|
|