-----------------------------------------------------------------------------
-- |
-- 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 Control.Monad                      (when)
import Distribution.PackageDescription    (executables, modulePath, package, maintainer, customFieldsBI, homepage, exeName, buildInfo)
import Distribution.Simple                (defaultMainWithHooks, simpleUserHooks, runTests, 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{ runTests = unittest True, postInst = unittest False}
 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 forced _ _ _ 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
                        when (not forced) $
                                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