{-|
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).
-}
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)
import System.Directory
  (XdgDirectory (..), createDirectoryIfMissing, doesFileExist, getXdgDirectory)
import System.Exit                      (ExitCode (..))
import System.FilePath                  ((</>), (<.>), searchPathSeparator)
import System.IO                        (hClose, hGetLine, hIsEOF, hPutStr)
import System.IO.Unsafe                 (unsafePerformIO)
import System.Process

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

{-# 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.
-}
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'

{-|
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 <- 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
  Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True 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 <- 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"
  Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True (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

{-|
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 a 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