sbv-0.9.11: Setup.hs

-----------------------------------------------------------------------------
-- |
-- Module      :  Main
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
-- Portability :  portable
--
-- Setup module for the sbv library
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall #-}
module Main(main) where

import Distribution.PackageDescription    (executables, modulePath, package, maintainer, customFieldsBI, homepage, exeName, buildInfo)
import Distribution.Simple                (defaultMainWithHooks, simpleUserHooks, postInst)
import Distribution.Simple.LocalBuildInfo (LocalBuildInfo(..))
import Distribution.Text                  (display)
import System.Directory                   (findExecutable)
import System.Exit                        (exitWith, ExitCode(..))
import System.Process                     (system)

import Data.SBV.Provers.Prover            (SMTSolver(..), yices)

main :: IO ()
main = defaultMainWithHooks simpleUserHooks{ postInst = unittest }
 where checkDefSolver = do
                let ex = executable yices
                    nm = name yices
                mbP <- findExecutable ex
                case mbP of
                  Nothing -> do putStrLn $ "*** The sbv library requires the default solver " ++ nm ++ " to be installed."
                                putStrLn $ "*** The executable " ++ show ex ++ " must be in your path."
                                putStrLn $ "*** Do not forget to install " ++ nm ++ "!"
                  Just _  -> return ()
       unittest _ _ _ lbi = do
         let testers = [ex | ex <- executables pkgDesc, modulePath ex == "SBVUnitTest/SBVUnitTest.hs"]
         case testers of
           [tp] -> runTester tp
           _    -> bailOut
         where pkgDesc  = localPkgDescr lbi
               sbvName  = display $ package pkgDesc
               report  = putStrLn $ "*** Please report to the maintainer: " ++ maintainer pkgDesc
               bailOut = do putStrLn "*** Cannot find SBV unit-tester program!"
                            report
                            exitWith $ ExitFailure 1
               runTester tp = do
                        case lookup "x-run-unittests" (customFieldsBI (buildInfo tp)) of
                                 Just "False" -> do checkDefSolver
                                                    putStrLn "*** Please run \"SBVUnitTests\" executable to perform unit-tests."
                                                    putStrLn $ "*** Package " ++ sbvName ++ " installed successfully. Enjoy!"
                                                    putStrLn $ "*** Further info: " ++ homepage pkgDesc
                                                    exitWith ExitSuccess
                                 _            -> return ()
                        mbP <- findExecutable $ exeName tp
                        case mbP of
                          Nothing -> bailOut
                          Just p  -> do ec <- system p
                                        case ec of
                                          ExitSuccess   -> putStrLn $ sbvName ++ " installed and unit-tests successfully run. Enjoy!"
                                          ExitFailure n -> if n == 1 --  couldn't run test cases..
                                                           then putStrLn "*** SBV unit-tests failed! Bailing out."
                                                           else putStrLn "*** Some SBV unit-tests failed!" >> report
                                        exitWith ec