{-|
Module      : Language.Alloy.Call
Description : A simple library to call Alloy given a specification
Copyright   : (c) Marcellus Siegburg, 2019
License     : MIT
Maintainer  : marcellus.siegburg@uni-due.de

This module provides basic functionality to interact with Alloy.
This library contains Alloy and an (internal) interface to interact with it.
These libraries will be placed into the users directory during execution.
A requirement for this library to work is a Java Runtime Environment
(as it is required by Alloy).
-}
{-# LANGUAGE CPP #-}
module Language.Alloy.Call (
  existsInstance,
  getInstances,
  ) where

import qualified Data.ByteString                  as BS (writeFile)

import Control.Monad                    (unless)
import Data.Hashable                    (hash)
import Data.IORef                       (IORef, newIORef, readIORef)
import Data.List                        (intercalate)
import Data.List.Split                  (splitOn)
import Data.Maybe                       (fromMaybe, isJust)
import System.Directory
  (XdgDirectory (..), createDirectory, doesFileExist, doesDirectoryExist,
   getTemporaryDirectory, getXdgDirectory)
import System.Directory.Internal        (setFileMode)
import System.Directory.Internal.Prelude
  (catch, isDoesNotExistError)
import System.Environment               (lookupEnv)
import System.Exit                      (ExitCode (..))
import System.FilePath
  ((</>), (<.>), searchPathSeparator, takeDirectory)
import System.IO                        (hClose, hGetLine, hIsEOF, hPutStr)
import System.IO.Unsafe                 (unsafePerformIO)
import System.Process
#if defined(mingw32_HOST_OS)
import System.Win32.Info                (getUserName)
#else
import System.Posix.User                (getLoginName)
#endif

import Language.Alloy.RessourceNames    (alloyJarName, className, classPackage)
import Language.Alloy.Ressources        (alloyJar, classFile)

data CallAlloyConfig = Config {
    CallAlloyConfig -> FilePath
alloyJarFile   :: FilePath,
    CallAlloyConfig -> FilePath
alloyClassFile :: FilePath,
    CallAlloyConfig -> Bool
keepFiles      :: Bool
  }

{-# NOINLINE mclassPath #-}
{-|
'IORef' for storing the class path.
-}
mclassPath :: IORef (Maybe FilePath)
mclassPath :: IORef (Maybe FilePath)
mclassPath = IO (IORef (Maybe FilePath)) -> IORef (Maybe FilePath)
forall a. IO a -> a
unsafePerformIO (Maybe FilePath -> IO (IORef (Maybe FilePath))
forall a. a -> IO (IORef a)
newIORef Maybe FilePath
forall a. Maybe a
Nothing)

{-|
This function may be used to get all model instances for a given Alloy
specification. It calls Alloy via a Java interface and returns the raw instance
answers as list of 'String's.
-}
getInstances
  :: Maybe Integer
  -- ^ How many instances to return 'Nothing' for all.
  -> String
  -- ^ The Alloy specification which should be loaded.
  -> IO [String]
getInstances :: Maybe Integer -> FilePath -> IO [FilePath]
getInstances maxInstances :: Maybe Integer
maxInstances content :: FilePath
content = do
  FilePath
classPath <- IO FilePath
getClassPath
  let callAlloy :: CreateProcess
callAlloy = FilePath -> [FilePath] -> CreateProcess
proc "java"
        ["-cp", FilePath
classPath, FilePath
classPackage FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ '.' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
className,
         Integer -> FilePath
forall a. Show a => a -> FilePath
show (Integer -> FilePath) -> Integer -> FilePath
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe (-1) Maybe Integer
maxInstances]
  (Just hin :: Handle
hin, Just hout :: Handle
hout, Just herr :: Handle
herr, ph :: ProcessHandle
ph) <-
    CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess CreateProcess
callAlloy {
        std_out :: StdStream
std_out = StdStream
CreatePipe,
        std_in :: StdStream
std_in  = StdStream
CreatePipe,
        std_err :: StdStream
std_err = StdStream
CreatePipe
      }
  Handle -> FilePath -> IO ()
hPutStr Handle
hin FilePath
content
  Handle -> IO ()
hClose Handle
hin
  Handle -> IO ()
printCallErrors Handle
herr
  ProcessHandle -> IO ()
printContentOnError ProcessHandle
ph IO () -> IO [FilePath] -> IO [FilePath]
forall a b. a -> b -> b
`seq`
    ([FilePath] -> FilePath) -> [[FilePath]] -> [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate "\n") ([[FilePath]] -> [FilePath])
-> ([FilePath] -> [[FilePath]]) -> [FilePath] -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [[FilePath]] -> [[FilePath]]
forall a. Int -> [a] -> [a]
drop 1 ([[FilePath]] -> [[FilePath]])
-> ([FilePath] -> [[FilePath]]) -> [FilePath] -> [[FilePath]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> [FilePath] -> [[FilePath]]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn [FilePath
begin] ([FilePath] -> [FilePath]) -> IO [FilePath] -> IO [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Handle -> IO [FilePath]
getWholeOutput Handle
hout
  where
    begin :: FilePath
begin = "---INSTANCE---"
    getWholeOutput :: Handle -> IO [FilePath]
getWholeOutput h :: Handle
h = do
      Bool
eof <- Handle -> IO Bool
hIsEOF Handle
h
      if Bool
eof
        then [FilePath] -> IO [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        else (:) (FilePath -> [FilePath] -> [FilePath])
-> IO FilePath -> IO ([FilePath] -> [FilePath])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Handle -> IO FilePath
hGetLine Handle
h IO ([FilePath] -> [FilePath]) -> IO [FilePath] -> IO [FilePath]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Handle -> IO [FilePath]
getWholeOutput Handle
h
    printContentOnError :: ProcessHandle -> IO ()
printContentOnError ph :: ProcessHandle
ph = do
      ExitCode
code <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ph
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ExitCode
code ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
== ExitCode
ExitSuccess)
        (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Failed parsing your file:\n" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
content
    printCallErrors :: Handle -> IO ()
printCallErrors err :: Handle
err = do
      [FilePath]
errors <- Handle -> IO [FilePath]
getWholeOutput Handle
err
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
errors) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate "\n" [FilePath]
errors

{-|
Check if the class path was determined already, if so use it, otherwise call
'readClassPath'.

Returns the class path.
-}
getClassPath :: IO FilePath
getClassPath :: IO FilePath
getClassPath = do
  Maybe FilePath
mclassPath' <- IORef (Maybe FilePath) -> IO (Maybe FilePath)
forall a. IORef a -> IO a
readIORef IORef (Maybe FilePath)
mclassPath
  IO FilePath
-> (FilePath -> IO FilePath) -> Maybe FilePath -> IO FilePath
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO FilePath
readClassPath FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FilePath
mclassPath'

{-
jarFileEnv :: String
jarFileEnv = "ALLOY_JAR_FILE"

callAlloyEnv :: String
callAlloyEnv = "CALL_ALLOY_CLASS_FILE"

keepFilesEnv :: String
keepFilesEnv = "KEEP_ALLOY_FILES"

{-|
Lookup environment variables which are to prefer if present.
-}
getEnvironmentInformation :: IO CallAlloyConfig
getEnvironmentInformation = do
  alloy     <- lookupEnv jarFileEnv
  callAlloy <- lookupEnv callAlloyEnv
  keep      <- lookupEnv keepFilesEnv
  let mconfig = Config <$> alloy <*> callAlloy <*> pure (isJust keep)
  case mconfig of
    Nothing -> do
      dataDir <- getXdgDirectory XdgData $ appName </> "dataDir" 
    Just c  -> return c
-}
{-
getVersionFile :: IO FilePath
getVersionFile = do
  configDir <- getXdgDirectory XdgConfig appName
  let versionFile = configDir </> "version"
  exists <- doesFileExist versionFile
  if exists
    then do
    version <- read <$> readFile versionFile
    unless (version == versionHash) $ createVersionFile configDir versionFile
    else createVersionFile configDir versionFile 
-}

fallbackToTempDir :: IO FilePath -> IO FilePath
fallbackToTempDir :: IO FilePath -> IO FilePath
fallbackToTempDir m :: IO FilePath
m = IO FilePath -> (IOError -> IO FilePath) -> IO FilePath
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch IO FilePath
m ((IOError -> IO FilePath) -> IO FilePath)
-> (IOError -> IO FilePath) -> IO FilePath
forall a b. (a -> b) -> a -> b
$ \e :: IOError
e ->
  if IOError -> Bool
isDoesNotExistError IOError
e
  then do
    FilePath
tmp    <- IO FilePath
getTemporaryDirectory
#if defined(mingw32_HOST_OS)
    login  <- getUserName
#else
    FilePath
login  <- IO FilePath
getLoginName
#endif
    let tmpDir :: FilePath
tmpDir = FilePath
tmp FilePath -> FilePath -> FilePath
</> Int -> FilePath
forall a. Show a => a -> FilePath
show (FilePath -> Int
forall a. Hashable a => a -> Int
hash FilePath
login) FilePath -> FilePath -> FilePath
</> FilePath
appName
    FilePath -> IO ()
createUserDirectoriesIfMissing (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
tmpDir
    FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
tmpDir
  else FilePath -> IO FilePath
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ IOError -> FilePath
forall a. Show a => a -> FilePath
show IOError
e

{-|
Read the class path version specified in the user directory, if it is not
current or if it does not exist, call 'createVersionFile'.

Returns the class path.
-}
readClassPath :: IO FilePath
readClassPath :: IO FilePath
readClassPath = do
  FilePath
configDir <- IO FilePath -> IO FilePath
fallbackToTempDir (IO FilePath -> IO FilePath) -> IO FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ XdgDirectory -> FilePath -> IO FilePath
getXdgDirectory XdgDirectory
XdgConfig FilePath
appName
  let versionFile :: FilePath
versionFile = FilePath
configDir FilePath -> FilePath -> FilePath
</> "version"
  Bool
exists <- FilePath -> IO Bool
doesFileExist FilePath
versionFile
  if Bool
exists
    then do
    Int
version <- FilePath -> Int
forall a. Read a => FilePath -> a
read (FilePath -> Int) -> IO FilePath -> IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO FilePath
readFile FilePath
versionFile
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
version Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
versionHash) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
createVersionFile FilePath
configDir FilePath
versionFile
    else FilePath -> FilePath -> IO ()
createVersionFile FilePath
configDir FilePath
versionFile
  FilePath
dataDir <- XdgDirectory -> FilePath -> IO FilePath
getXdgDirectory XdgDirectory
XdgData (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
appName FilePath -> FilePath -> FilePath
</> "dataDir"
  FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
dataDir FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Char
searchPathSeparator Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
dataDir FilePath -> FilePath -> FilePath
</> FilePath
alloyJarName

{-|
Create all library files within the users 'XdgDirectory' by calling
'createDataDir' then place the current version number into a configuration File.
-}
createVersionFile :: FilePath -> FilePath -> IO ()
createVersionFile :: FilePath -> FilePath -> IO ()
createVersionFile configDir :: FilePath
configDir versionFile :: FilePath
versionFile = do
  IO ()
createDataDir
  FilePath -> IO ()
createUserDirectoriesIfMissing FilePath
configDir
  FilePath -> FilePath -> IO ()
writeFile FilePath
versionFile (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
versionHash

{-|
Create all library files within the users 'XdgDirectory' based on the source
files enclosed into this library (see also 'Language.Alloy.RessourceNames' and
'Language.Alloy.Ressources').
-}
createDataDir :: IO ()
createDataDir :: IO ()
createDataDir = do
  FilePath
dataDir <- IO FilePath -> IO FilePath
fallbackToTempDir (IO FilePath -> IO FilePath) -> IO FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ XdgDirectory -> FilePath -> IO FilePath
getXdgDirectory XdgDirectory
XdgData (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
appName FilePath -> FilePath -> FilePath
</> "dataDir"
  FilePath -> IO ()
createUserDirectoriesIfMissing (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
dataDir FilePath -> FilePath -> FilePath
</> FilePath
classPackage
  FilePath -> ByteString -> IO ()
BS.writeFile (FilePath
dataDir FilePath -> FilePath -> FilePath
</> FilePath
classPackage FilePath -> FilePath -> FilePath
</> FilePath
className FilePath -> FilePath -> FilePath
<.> "class") ByteString
classFile
  FilePath -> ByteString -> IO ()
BS.writeFile (FilePath
dataDir FilePath -> FilePath -> FilePath
</> FilePath
alloyJarName) ByteString
alloyJar

{-|
Creates user directories using the file permissions 700.
This function creates the specified directory and all its parent directories as
well (if they are also missing).
-}
createUserDirectoriesIfMissing :: FilePath -> IO ()
createUserDirectoriesIfMissing :: FilePath -> IO ()
createUserDirectoriesIfMissing fp :: FilePath
fp = do
  Bool
isDir <- FilePath -> IO Bool
doesDirectoryExist FilePath
fp
  let parent :: FilePath
parent = FilePath -> FilePath
takeDirectory FilePath
fp
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
isDir Bool -> Bool -> Bool
|| FilePath
parent FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
fp) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    FilePath -> IO ()
createUserDirectoriesIfMissing FilePath
parent
    FilePath -> IO ()
createDirectory FilePath
fp
    FilePath -> Mode -> IO ()
setFileMode FilePath
fp (7Mode -> Mode -> Mode
forall a. Num a => a -> a -> a
*8Mode -> Mode -> Mode
forall a. Num a => a -> a -> a
*8)

{-|
Check if there exists a model for the given specification. This function calls
Alloy retrieving one instance. If there is no such instance, it returns false.
This function calls 'getInstances'.
-}
existsInstance
  :: String
  -- ^ The Alloy specification which should be loaded.
  -> IO Bool
  -- ^ Whether there exists an instance (within the given scope)
existsInstance :: FilePath -> IO Bool
existsInstance = ([FilePath] -> Bool) -> IO [FilePath] -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Bool
not (Bool -> Bool) -> ([FilePath] -> Bool) -> [FilePath] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (IO [FilePath] -> IO Bool)
-> (FilePath -> IO [FilePath]) -> FilePath -> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer -> FilePath -> IO [FilePath]
getInstances (Integer -> Maybe Integer
forall a. a -> Maybe a
Just 1)

{-|
The application name (used to store data in a specific directory.
-}
appName :: String
appName :: FilePath
appName = "call-alloy"

{-# INLINE versionHash #-}
{-|
Used to determine possible source code and Alloy version changes across multiple
versions of this library.
-}
versionHash :: Int
versionHash :: Int
versionHash = Int -> Int
forall a. Hashable a => a -> Int
hash (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Int
alloyHash Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
classFileHash
  where
    alloyHash :: Int
alloyHash = ByteString -> Int
forall a. Hashable a => a -> Int
hash ByteString
alloyJar
    classFileHash :: Int
classFileHash = ByteString -> Int
forall a. Hashable a => a -> Int
hash ByteString
classFile