{- |

Module : $Header$

Description : Check for availability of provers

Copyright : (c) Dminik Luecke, and Uni Bremen 2008

License : GPLv2 or higher, see LICENSE.txt

Maintainer : luecke@informatik.uni-bremen.de

Stability : provisional

Portability : portable

check for provers

-}

module Common.ProverTools where

import Common.Utils

import System.Directory

import System.IO.Unsafe

import System.FilePath

import System.IO.Error

import Control.Exception as Exception

-- | Checks if a Prover Binary exists and is executable in an unsafe manner

unsafeProverCheck :: String -- ^ prover Name

-> String -- ^ Environment Variable

-> a

-> [a]

unsafeProverCheck name env = unsafePerformIO . check4Prover name env

-- | Checks if a Prover Binary exists and is executable

check4Prover :: String -- ^ prover Name

-> String -- ^ Environment Variable

-> a

-> IO [a]

check4Prover name env a = do

ex <- check4FileAux name env

case ex of

[] -> return []

_ -> do

execI <- mapM (tryPermissions . (</> name)) ex

return [ a | any executable execI ]

-- assume executability if permissions cannot be read (on Mac)

tryPermissions :: FilePath -> IO Permissions

tryPermissions f = Exception.catch (getPermissions f) $ \ e ->

return $ (if isPermissionError e then setOwnerExecutable True else id)

emptyPermissions

missingExecutableInPath :: String -> IO Bool

missingExecutableInPath name = do

mp <- findExecutable name

case mp of

Nothing -> return True

Just _ -> fmap null $ check4Prover name "PATH" ()

-- | Checks if a file exists in an unsafe manner

unsafeFileCheck :: String -- ^ prover Name

-> String -- ^ Environment Variable

-> a

-> [a]

unsafeFileCheck name env = unsafePerformIO . check4File name env

check4FileAux :: String -- ^ file name

-> String -- ^ Environment Variable

-> IO [String]

check4FileAux name env = do

pPath <- getEnvDef env ""

let path = "" : splitOn ':' pPath

exIT <- mapM (doesFileExist . (</> name)) path

return $ map fst $ filter snd $ zip path exIT

-- | Checks if a file exists

check4File :: String -- ^ file name

-> String -- ^ Environment Variable

-> a

-> IO [a]

check4File name env a = do

ex <- check4FileAux name env

return [a | not $ null ex ]

-- | check for java and the jar file in the directory of the variable

check4jarFile :: String -- ^ environment Variable

-> String -- ^ jar file name

-> IO (Bool, FilePath)

check4jarFile = check4jarFileWithDefault ""

check4jarFileWithDefault

:: String -- ^ default path

-> String -- ^ environment Variable

-> String -- ^ jar file name

-> IO (Bool, FilePath)

check4jarFileWithDefault def var jar = do

noJava <- missingExecutableInPath "java"

pPath <- getEnvDef var def

hasJar <- doesFileExist $ pPath </> jar

return (not noJava && hasJar, pPath)

-- | environment variable for HETS_OWL_TOOLS

hetsOWLenv :: String

hetsOWLenv = "HETS_OWL_TOOLS"

-- | check for the jar file under HETS_OWL_TOOLS

check4HetsOWLjar :: String -- ^ jar file name

-> IO (Bool, FilePath)

check4HetsOWLjar = check4jarFileWithDefault "OWL2" hetsOWLenv