content: --------------------------------------------------------------------------------
  -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
  --------------------------------------------------------------------------------
  
  -- | A test suite to check for basic functionality.
  
  module Main where
  
  import System.Directory ( removeDirectoryRecursive
                          , doesDirectoryExist
                          , doesFileExist
                          , removeFile )
  import qualified Copilot.Compile.C99 as C99
  import qualified Copilot.Compile.SBV as SBV
  import qualified Copilot.Tools.CBMC as M
  import Control.Monad (when, unless)
  import Data.Maybe (catMaybes)
  
  import AddMult
  import Array
  --import BadExtVars
  import Cast
  import ClockExamples
  import EngineExample
  import Examples
  import Examples2
  import ExtFuns
  import Languages
  import Local
  import LTLExamples
  import PTLTLExamples
  import Random
  import RegExpExamples
  import Sat
  import StackExamples
  import StatExamples
  import VotingExamples
  
  
  --------------------------------------------------------------------------------
  
  main :: IO ()
  main = do
    ls <- checkExists
    when (null ls) runTests
    unless (null ls) $ do putStrLn "*** Warning! ***"
                          putStrLn "Cannot run tests in this directory.  You have the following files or directories that would be deleted: "
                          mapM_ putStrLn ls
                                  
  runTests :: IO ()
  runTests = do
    cleanup
    putStrLn "Testing addMult ..."
    addMult         >> cleanup
    putStrLn ""
    putStrLn "Testing array ..."
    array           >> cleanup
    putStrLn ""
  --  putStrLn "Testing badExtVars ..."
  --  badExtVars      >> cleanup
    putStrLn ""
    putStrLn "Testing castEx ..."
    castEx          >> cleanup
    putStrLn ""
    putStrLn "Testing clockExamples ..."
    clockExamples   >> cleanup
    putStrLn ""
    putStrLn "Testing engineExample ..."
    engineExample   >> cleanup
    putStrLn ""
    putStrLn "Testing examples ..."
    examples        >> cleanup
    putStrLn ""
    putStrLn "Testing examples2 ..."
    examples2       >> cleanup
    putStrLn ""
    putStrLn "Testing extFuns ..."
    extFuns         >> cleanup
    putStrLn ""
    putStrLn "Testing language ..."
    languages       >> cleanup
    putStrLn ""
    putStrLn "Testing localEx ..."
    localEx         >> cleanup
    putStrLn ""
    putStrLn "Testing ltlExamples ..."
    ltlExamples     >> cleanup
    putStrLn ""
    putStrLn "Testing ptltlExamples ..."
    ptltlExamples   >> cleanup
    putStrLn ""
    putStrLn "Testing randomEx ..."
    randomEx        >> cleanup
    putStrLn ""
    putStrLn "Testing regExpExamples ..."
    regExpExamples  >> cleanup
    putStrLn ""
    putStrLn "Testing satExamples ..."
    satExamples     >> cleanup
    putStrLn ""
    putStrLn "Testing stackExamples ..."
    stackExamples   >> cleanup
    putStrLn ""
    putStrLn "Testing statExamples ..."
    statExamples    >> cleanup
    putStrLn ""
    putStrLn "Testing votingExamples ..."
    votingExamples  >> cleanup
    putStrLn ""
    putStrLn ""
    putStrLn "************************************"
    putStrLn " Ok, the basic tests passed.  Enjoy!"
    putStrLn "************************************"
  
  --------------------------------------------------------------------------------
  
  cbmcName :: String
  cbmcName = "cbmc_driver.c"
  
  atomCBMC :: String
  atomCBMC = M.appendPrefix M.atomPrefix C99.c99DirName
  
  sbvCBMC :: String
  sbvCBMC = M.appendPrefix M.sbvPrefix SBV.sbvDirName
  
  --------------------------------------------------------------------------------
  
  checkExists :: IO [String]
  checkExists = do
    b0 <- nmBool doesDirectoryExist SBV.sbvDirName
    b1 <- nmBool doesDirectoryExist C99.c99DirName
    b2 <- nmBool doesFileExist cbmcName
    b3 <- nmBool doesDirectoryExist atomCBMC
    b4 <- nmBool doesDirectoryExist sbvCBMC
    return $ catMaybes $ map getName [b0, b1, b2, b3, b4]
  
    where
    getName (nm, bool) = if bool then Just nm else Nothing
    nmBool f nm = do b <- f nm 
                     return (nm, b)
  
  --------------------------------------------------------------------------------
  
  cleanup :: IO ()
  cleanup = do
  
    b0 <- doesDirectoryExist SBV.sbvDirName
    when b0 (removeDirectoryRecursive SBV.sbvDirName)
  
    b1 <- doesDirectoryExist C99.c99DirName
    when b1 (removeDirectoryRecursive C99.c99DirName)
  
    b2 <- doesFileExist cbmcName
    when b2 (removeFile cbmcName)
  
    b3 <- doesDirectoryExist atomCBMC
    when b3 (removeDirectoryRecursive atomCBMC)
  
    b4 <- doesDirectoryExist sbvCBMC
    when b4 (removeDirectoryRecursive sbvCBMC)
  
  --------------------------------------------------------------------------------
  