{- |
Module      :  ./Common/ProverTools.hs
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.FilePath

missingExecutableInPath :: String -> IO Bool
missingExecutableInPath :: String -> IO Bool
missingExecutableInPath name :: String
name = do
  Maybe String
mp <- String -> IO (Maybe String)
findExecutable String
name
  case Maybe String
mp of
    Nothing -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Just name' :: String
name' -> do
      [()]
p1 <- String -> String -> () -> IO [()]
forall a. String -> String -> a -> IO [a]
check4File (String -> String
takeFileName String
name') "PATH" ()
      [()]
p2 <- String -> String -> () -> IO [()]
forall a. String -> String -> a -> IO [a]
check4File (String -> String
takeFileName String
name') "Path" ()
      Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> ([()] -> Bool) -> [()] -> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([()] -> IO Bool) -> [()] -> IO Bool
forall a b. (a -> b) -> a -> b
$ [()]
p1 [()] -> [()] -> [()]
forall a. [a] -> [a] -> [a]
++ [()]
p2

check4FileAux :: String -- ^ file name
              -> String -- ^ Environment Variable
              -> IO [String]
check4FileAux :: String -> String -> IO [String]
check4FileAux name :: String
name env :: String
env = do
      String
pPath <- String -> String -> IO String
getEnvDef String
env ""
      let path :: [String]
path = "" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
splitPaths String
pPath
      [Bool]
exIT <- (String -> IO Bool) -> [String] -> IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> IO Bool
doesFileExist (String -> IO Bool) -> (String -> String) -> String -> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
</> String
name)) [String]
path
      [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ ((String, Bool) -> String) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Bool) -> String
forall a b. (a, b) -> a
fst ([(String, Bool)] -> [String]) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> a -> b
$ ((String, Bool) -> Bool) -> [(String, Bool)] -> [(String, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (String, Bool) -> Bool
forall a b. (a, b) -> b
snd ([(String, Bool)] -> [(String, Bool)])
-> [(String, Bool)] -> [(String, Bool)]
forall a b. (a -> b) -> a -> b
$ [String] -> [Bool] -> [(String, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
path [Bool]
exIT

-- | Checks if a file exists in PATH
checkBinary :: String -> IO (Maybe String)
checkBinary :: String -> IO (Maybe String)
checkBinary name :: String
name = ([String] -> Maybe String) -> IO [String] -> IO (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
  (\ l :: [String]
l -> if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
l
          then String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ "missing binary in $PATH: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name
          else Maybe String
forall a. Maybe a
Nothing)
  (IO [String] -> IO (Maybe String))
-> IO [String] -> IO (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> String -> IO [String]
check4FileAux String
name "PATH"

-- | Checks if a file exists
check4File :: String -- ^ file name
           -> String -- ^ Environment Variable
           -> a
           -> IO [a]
check4File :: String -> String -> a -> IO [a]
check4File name :: String
name env :: String
env a :: a
a = do
      [String]
ex <- String -> String -> IO [String]
check4FileAux String
name String
env
      [a] -> IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a
a | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
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 :: String -> String -> IO (Bool, String)
check4jarFile = String -> String -> String -> IO (Bool, String)
check4jarFileWithDefault ""

check4jarFileWithDefault
  :: String -- ^ default path
  -> String -- ^ environment Variable
  -> String -- ^ jar file name
  -> IO (Bool, FilePath)
check4jarFileWithDefault :: String -> String -> String -> IO (Bool, String)
check4jarFileWithDefault def :: String
def var :: String
var jar :: String
jar = do
  String
pPath <- String -> String -> IO String
getEnvDef String
var String
def
  Bool
hasJar <- String -> IO Bool
doesFileExist (String -> IO Bool) -> String -> IO Bool
forall a b. (a -> b) -> a -> b
$ String
pPath String -> String -> String
</> String
jar
  (Bool, String) -> IO (Bool, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
hasJar, String
pPath)

-- | environment variable for HETS_OWL_TOOLS
hetsOWLenv :: String
hetsOWLenv :: String
hetsOWLenv = "HETS_OWL_TOOLS"

-- | check for the jar file under HETS_OWL_TOOLS
check4HetsOWLjar :: String -- ^ jar file name
  -> IO (Bool, FilePath)
check4HetsOWLjar :: String -> IO (Bool, String)
check4HetsOWLjar = String -> String -> String -> IO (Bool, String)
check4jarFileWithDefault "OWL2" String
hetsOWLenv

checkOWLjar :: String -> IO (Maybe String)
checkOWLjar :: String -> IO (Maybe String)
checkOWLjar name :: String
name =
  ((Bool, String) -> Maybe String)
-> IO (Bool, String) -> IO (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (b :: Bool
b, p :: String
p) -> if Bool
b then Maybe String
forall a. Maybe a
Nothing else
       String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ "missing jar ($" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
hetsOWLenv String -> String -> String
forall a. [a] -> [a] -> [a]
++ "): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String
p String -> String -> String
</> String
name))
  (IO (Bool, String) -> IO (Maybe String))
-> IO (Bool, String) -> IO (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> IO (Bool, String)
check4HetsOWLjar String
name