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
-> String
-> 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
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"
check4File :: String
-> String
-> 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 ]
check4jarFile :: String
-> String
-> IO (Bool, FilePath)
check4jarFile :: String -> String -> IO (Bool, String)
check4jarFile = String -> String -> String -> IO (Bool, String)
check4jarFileWithDefault ""
check4jarFileWithDefault
:: String
-> String
-> String
-> 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)
hetsOWLenv :: String
hetsOWLenv :: String
hetsOWLenv = "HETS_OWL_TOOLS"
check4HetsOWLjar :: String
-> 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