{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-|
Module      : Language.Alloy.Internal.Call
Copyright   : (c) Marcellus Siegburg, 2019 - 2021
License     : MIT

This module provides the basic internal functionality to retrieve the raw
results from calling Alloy.
It provides data types and functions to interact with Alloy.
-}
module Language.Alloy.Internal.Call (
  CallAlloyConfig (maxInstances, noOverflow, satSolver, timeout),
  SatSolver (..),
  defaultCallAlloyConfig,
  getRawInstances,
  getRawInstancesWith,
  ) where

import qualified Data.ByteString                  as BS (
  intercalate,
  stripPrefix,
  )
import qualified Data.ByteString.Char8            as BS (
  hGetLine,
  putStrLn,
  unlines,
  )

import Control.Concurrent (
  threadDelay,
  )
import Control.Concurrent.Async (
  concurrently,
  mapConcurrently_,
  wait,
  withAsync
  )
import Control.Concurrent.Extra         (Lock, newLock, withLock)
import Control.Exception                (IOException, bracket, catch)
import Control.Monad                    (unless, when)
import Control.Monad.Extra              (whenJust)
import Data.ByteString                  (ByteString)
import Data.ByteString.Char8            (unpack)
import Data.IORef (
  IORef,
  atomicWriteIORef,
#ifdef mingw32_HOST_OS
  newIORef,
#endif
  readIORef,
  )
import Data.List                        (intercalate)
import Data.List.Split                  (splitOn)
import Data.Maybe                       (fromMaybe)
import System.Exit                      (ExitCode (..))
import System.FilePath
  (searchPathSeparator)
import System.IO (
#ifndef mingw32_HOST_OS
  BufferMode (..),
  hSetBuffering,
#endif
  Handle,
  hClose,
  hFlush,
  hIsEOF,
  hPutStr,
  hPutStrLn,
  stderr,
  )
import System.IO.Unsafe                 (unsafePerformIO)
import System.Process (
  CreateProcess (..), StdStream (..), ProcessHandle,
  cleanupProcess,
  createProcess, proc, terminateProcess, waitForProcess,
  )

import Language.Alloy.RessourceNames (
  className,
  classPackage,
  )
import Language.Alloy.Ressources (
  alloyJar,
  commonsCliJar,
  slf4jJar,
  )
import Paths_call_alloy                 (getDataDir)

{-|
Available SAT solvers.
-}
data SatSolver
  = BerkMin
  -- ^ BerkMin
  --
  -- * not tested
  | Glucose
  -- ^ Glucose
  --
  -- * incremental
  | Glucose41
  -- ^ Glucose41
  --
  -- * incremental
  | Lingeling
  -- ^ Lingeling
  --
  -- * not incremental
  | MiniSat
  -- ^ MiniSat
  --
  -- * incremental
  | MiniSatProver
  -- ^ MiniSatProver
  --
  -- * incremental
  | PLingeling
  -- ^ PLingeling
  --
  -- * not incremental
  | SAT4J
  -- ^ SAT4J
  --
  -- * incremental
  | Spear
  -- ^ Spear
  --
  -- * not tested
  deriving (SatSolver
SatSolver -> SatSolver -> Bounded SatSolver
forall a. a -> a -> Bounded a
$cminBound :: SatSolver
minBound :: SatSolver
$cmaxBound :: SatSolver
maxBound :: SatSolver
Bounded, Int -> SatSolver
SatSolver -> Int
SatSolver -> [SatSolver]
SatSolver -> SatSolver
SatSolver -> SatSolver -> [SatSolver]
SatSolver -> SatSolver -> SatSolver -> [SatSolver]
(SatSolver -> SatSolver)
-> (SatSolver -> SatSolver)
-> (Int -> SatSolver)
-> (SatSolver -> Int)
-> (SatSolver -> [SatSolver])
-> (SatSolver -> SatSolver -> [SatSolver])
-> (SatSolver -> SatSolver -> [SatSolver])
-> (SatSolver -> SatSolver -> SatSolver -> [SatSolver])
-> Enum SatSolver
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: SatSolver -> SatSolver
succ :: SatSolver -> SatSolver
$cpred :: SatSolver -> SatSolver
pred :: SatSolver -> SatSolver
$ctoEnum :: Int -> SatSolver
toEnum :: Int -> SatSolver
$cfromEnum :: SatSolver -> Int
fromEnum :: SatSolver -> Int
$cenumFrom :: SatSolver -> [SatSolver]
enumFrom :: SatSolver -> [SatSolver]
$cenumFromThen :: SatSolver -> SatSolver -> [SatSolver]
enumFromThen :: SatSolver -> SatSolver -> [SatSolver]
$cenumFromTo :: SatSolver -> SatSolver -> [SatSolver]
enumFromTo :: SatSolver -> SatSolver -> [SatSolver]
$cenumFromThenTo :: SatSolver -> SatSolver -> SatSolver -> [SatSolver]
enumFromThenTo :: SatSolver -> SatSolver -> SatSolver -> [SatSolver]
Enum, SatSolver -> SatSolver -> Bool
(SatSolver -> SatSolver -> Bool)
-> (SatSolver -> SatSolver -> Bool) -> Eq SatSolver
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SatSolver -> SatSolver -> Bool
== :: SatSolver -> SatSolver -> Bool
$c/= :: SatSolver -> SatSolver -> Bool
/= :: SatSolver -> SatSolver -> Bool
Eq, ReadPrec [SatSolver]
ReadPrec SatSolver
Int -> ReadS SatSolver
ReadS [SatSolver]
(Int -> ReadS SatSolver)
-> ReadS [SatSolver]
-> ReadPrec SatSolver
-> ReadPrec [SatSolver]
-> Read SatSolver
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS SatSolver
readsPrec :: Int -> ReadS SatSolver
$creadList :: ReadS [SatSolver]
readList :: ReadS [SatSolver]
$creadPrec :: ReadPrec SatSolver
readPrec :: ReadPrec SatSolver
$creadListPrec :: ReadPrec [SatSolver]
readListPrec :: ReadPrec [SatSolver]
Read, Int -> SatSolver -> ShowS
[SatSolver] -> ShowS
SatSolver -> [Char]
(Int -> SatSolver -> ShowS)
-> (SatSolver -> [Char])
-> ([SatSolver] -> ShowS)
-> Show SatSolver
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SatSolver -> ShowS
showsPrec :: Int -> SatSolver -> ShowS
$cshow :: SatSolver -> [Char]
show :: SatSolver -> [Char]
$cshowList :: [SatSolver] -> ShowS
showList :: [SatSolver] -> ShowS
Show)

toParameter :: SatSolver -> String
toParameter :: SatSolver -> [Char]
toParameter = \case
  SatSolver
BerkMin -> [Char]
"BERKMIN"
  SatSolver
Glucose -> [Char]
"GLUCOSE"
  SatSolver
Glucose41 -> [Char]
"GLUCOSE41"
  SatSolver
Lingeling -> [Char]
"LINGELING"
  SatSolver
MiniSat -> [Char]
"MINISAT"
  SatSolver
MiniSatProver -> [Char]
"MINISAT_PROVER"
  SatSolver
PLingeling -> [Char]
"PLINGELING"
  SatSolver
SAT4J -> [Char]
"SAT4J"
  SatSolver
Spear -> [Char]
"SPEAR"

{-|
Configuration for calling alloy. These are:

 * maximal number of instances to retrieve ('Nothing' for all)
 * whether to not overflow when calculating numbers within Alloy
 * an timeout after which to forcibly kill Alloy
   (retrieving only instances that were returned before killing the process)
-}
data CallAlloyConfig = CallAlloyConfig {
  -- | maximal number of instances to retrieve ('Nothing' for all)
  CallAlloyConfig -> Maybe Integer
maxInstances :: !(Maybe Integer),
  -- | whether to not overflow when calculating numbers within Alloy
  CallAlloyConfig -> Bool
noOverflow   :: !Bool,
  -- | the 'SatSolver' to choose. Note that some are not incremental,
  --   i.e. will return only one solution, even if 'maxInstances' is set higher.
  CallAlloyConfig -> SatSolver
satSolver    :: !SatSolver,
  -- | the time in microseconds after which to forcibly kill Alloy
  --   ('Nothing' for never)
  CallAlloyConfig -> Maybe Int
timeout      :: !(Maybe Int)
  }

{-|
Default configuration for calling Alloy. Defaults to:

 * retrieve all instances
 * do not overflow
 * 'SAT4J'
-}
defaultCallAlloyConfig :: CallAlloyConfig
defaultCallAlloyConfig :: CallAlloyConfig
defaultCallAlloyConfig = CallAlloyConfig {
  maxInstances :: Maybe Integer
maxInstances = Maybe Integer
forall a. Maybe a
Nothing,
  noOverflow :: Bool
noOverflow   = Bool
True,
  satSolver :: SatSolver
satSolver    = SatSolver
SAT4J,
  timeout :: Maybe Int
timeout      = Maybe Int
forall a. Maybe a
Nothing
  }

{-# NOINLINE outLock #-}
outLock :: Lock
outLock :: Lock
outLock = IO Lock -> Lock
forall a. IO a -> a
unsafePerformIO IO Lock
newLock

putOutLn :: String -> IO ()
putOutLn :: [Char] -> IO ()
putOutLn = Lock -> IO () -> IO ()
forall a. Lock -> IO a -> IO a
withLock Lock
outLock (IO () -> IO ()) -> ([Char] -> IO ()) -> [Char] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> IO ()
putStrLn

putErrLn :: String -> IO ()
putErrLn :: [Char] -> IO ()
putErrLn = Lock -> IO () -> IO ()
forall a. Lock -> IO a -> IO a
withLock Lock
outLock (IO () -> IO ()) -> ([Char] -> IO ()) -> [Char] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> [Char] -> IO ()
hPutStrLn Handle
stderr

{-|
This function may be used to get all raw model instances for a given Alloy
specification. It calls Alloy via a Java interface and splits the raw instance
answers before returning the resulting list of raw instances.
-}
getRawInstances
  :: Maybe Integer
  -- ^ How many instances to return; 'Nothing' for all.
  -> String
  -- ^ The Alloy specification which should be loaded.
  -> IO [ByteString]
getRawInstances :: Maybe Integer -> [Char] -> IO [ByteString]
getRawInstances Maybe Integer
maxIs = CallAlloyConfig -> [Char] -> IO [ByteString]
getRawInstancesWith CallAlloyConfig
defaultCallAlloyConfig {
  maxInstances = maxIs
  }

{-|
Creates an Alloy process using the given config.
-}
callAlloyWith
  :: CallAlloyConfig
  -> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
callAlloyWith :: CallAlloyConfig
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
callAlloyWith CallAlloyConfig
config = do
  [Char]
classPath <- IO [Char]
getClassPath
  let callAlloy :: CreateProcess
callAlloy = [Char] -> [[Char]] -> CreateProcess
proc [Char]
"java"
        ([[Char]] -> CreateProcess) -> [[Char]] -> CreateProcess
forall a b. (a -> b) -> a -> b
$ [[Char]
"-cp", [Char]
classPath, [Char]
classPackage [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Char
'.' Char -> ShowS
forall a. a -> [a] -> [a]
: [Char]
className,
           [Char]
"-i", Integer -> [Char]
forall a. Show a => a -> [Char]
show (Integer -> [Char]) -> Integer -> [Char]
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe (-Integer
1) (Maybe Integer -> Integer) -> Maybe Integer -> Integer
forall a b. (a -> b) -> a -> b
$ CallAlloyConfig -> Maybe Integer
maxInstances CallAlloyConfig
config]
        [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]
"-o" | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CallAlloyConfig -> Bool
noOverflow CallAlloyConfig
config]
        [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]
"-s", SatSolver -> [Char]
toParameter (CallAlloyConfig -> SatSolver
satSolver CallAlloyConfig
config)]
  CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess CreateProcess
callAlloy {
    std_out = CreatePipe,
    std_in  = CreatePipe,
    std_err = CreatePipe
  }

{-|
This function may be used to get all raw model instances for a given Alloy
specification. It calls Alloy via a Java interface and splits the raw instance
answers before returning the resulting list of raw instances.
Parameters are set using a 'CallAlloyConfig'.
-}
getRawInstancesWith
  :: CallAlloyConfig
  -- ^ The configuration to be used.
  -> String
  -- ^ The Alloy specification which should be loaded.
  -> IO [ByteString]
getRawInstancesWith :: CallAlloyConfig -> [Char] -> IO [ByteString]
getRawInstancesWith CallAlloyConfig
config [Char]
content
  = IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
-> ((Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
    -> IO ())
-> ((Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
    -> IO [ByteString])
-> IO [ByteString]
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket (CallAlloyConfig
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
callAlloyWith CallAlloyConfig
config) (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle) -> IO ()
cleanupProcess (((Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
  -> IO [ByteString])
 -> IO [ByteString])
-> ((Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
    -> IO [ByteString])
-> IO [ByteString]
forall a b. (a -> b) -> a -> b
$ \(Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
p -> do
  (Just Handle
hin, Just Handle
hout, Just Handle
herr, ProcessHandle
ph) <- (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
p
#ifndef mingw32_HOST_OS
  Handle -> BufferMode -> IO ()
hSetBuffering Handle
hin BufferMode
NoBuffering
  let abort :: Maybe a
abort = Maybe a
forall a. Maybe a
Nothing
#else
  abort <- Just <$> newIORef False
#endif
  let evaluateAlloy' :: IO ()
evaluateAlloy' = do
        Handle -> [Char] -> IO ()
hPutStr Handle
hin [Char]
content
        Handle -> IO ()
hFlush Handle
hin
        Handle -> IO ()
hClose Handle
hin
      evaluateAlloy :: IO ()
evaluateAlloy = IO () -> (IOException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch IO ()
evaluateAlloy' ((IOException -> IO ()) -> IO ())
-> (IOException -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \IOException
e -> do
        let err :: [Char]
err = IOException -> [Char]
forall a. Show a => a -> [Char]
show (IOException
e :: IOException)
            warn :: [Char]
warn = [Char]
"Maybe not complete instance was sent to Alloy "
            explain :: [Char]
explain = [Char]
"(Are timeouts set? Make sure they are not too small!): "
        [Char] -> IO ()
putErrLn ([Char]
"Warning: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
warn [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
explain [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
err)
  Handle
-> Handle
-> Handle
-> ProcessHandle
-> Maybe (IORef Bool)
-> Maybe Int
-> IO [ByteString]
-> IO [ByteString]
forall a.
Handle
-> Handle
-> Handle
-> ProcessHandle
-> Maybe (IORef Bool)
-> Maybe Int
-> IO a
-> IO a
withTimeout Handle
hin Handle
hout Handle
herr ProcessHandle
ph Maybe (IORef Bool)
forall a. Maybe a
abort (CallAlloyConfig -> Maybe Int
timeout CallAlloyConfig
config) (IO [ByteString] -> IO [ByteString])
-> IO [ByteString] -> IO [ByteString]
forall a b. (a -> b) -> a -> b
$ do
    ([ByteString]
out, [ByteString]
err) <- (([ByteString], [ByteString]), ()) -> ([ByteString], [ByteString])
forall a b. (a, b) -> a
fst ((([ByteString], [ByteString]), ())
 -> ([ByteString], [ByteString]))
-> IO (([ByteString], [ByteString]), ())
-> IO ([ByteString], [ByteString])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ([ByteString], [ByteString])
-> IO () -> IO (([ByteString], [ByteString]), ())
forall a b. IO a -> IO b -> IO (a, b)
concurrently
      (IO [ByteString]
-> IO [ByteString] -> IO ([ByteString], [ByteString])
forall a b. IO a -> IO b -> IO (a, b)
concurrently (Handle -> IO [ByteString]
getOutput Handle
hout) (Handle -> IO [ByteString]
getOutput Handle
herr))
      IO ()
evaluateAlloy
    [ByteString] -> Maybe (IORef Bool) -> ProcessHandle -> IO ()
printContentOnError [ByteString]
out Maybe (IORef Bool)
forall a. Maybe a
abort ProcessHandle
ph
    let err' :: [ByteString]
err' = [ByteString] -> [ByteString]
removeInfoLines [ByteString]
err
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ByteString] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ByteString]
err') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
forall a. [Char] -> IO a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ ByteString -> [Char]
unpack (ByteString -> [Char]) -> ByteString -> [Char]
forall a b. (a -> b) -> a -> b
$ [ByteString] -> ByteString
BS.unlines [ByteString]
err'
    [ByteString] -> IO [ByteString]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ByteString] -> IO [ByteString])
-> [ByteString] -> IO [ByteString]
forall a b. (a -> b) -> a -> b
$ ([ByteString] -> ByteString) -> [[ByteString]] -> [ByteString]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ByteString -> [ByteString] -> ByteString
BS.intercalate ByteString
"\n")
      ([[ByteString]] -> [ByteString]) -> [[ByteString]] -> [ByteString]
forall a b. (a -> b) -> a -> b
$ ([ByteString] -> Bool) -> [[ByteString]] -> [[ByteString]]
forall {a}. (a -> Bool) -> [a] -> [a]
filterLast ((ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
partialInstance) (ByteString -> Bool)
-> ([ByteString] -> ByteString) -> [ByteString] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ByteString] -> ByteString
forall a. HasCallStack => [a] -> a
last)
      ([[ByteString]] -> [[ByteString]])
-> [[ByteString]] -> [[ByteString]]
forall a b. (a -> b) -> a -> b
$ Int -> [[ByteString]] -> [[ByteString]]
forall a. Int -> [a] -> [a]
drop Int
1 ([[ByteString]] -> [[ByteString]])
-> [[ByteString]] -> [[ByteString]]
forall a b. (a -> b) -> a -> b
$ [ByteString] -> [ByteString] -> [[ByteString]]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn [ByteString
begin] [ByteString]
out
  where
    begin :: ByteString
    begin :: ByteString
begin = ByteString
"---INSTANCE---"
    filterLast :: (a -> Bool) -> [a] -> [a]
filterLast a -> Bool
_ []     = []
    filterLast a -> Bool
p x :: [a]
x@[a
_]  = (a -> Bool) -> [a] -> [a]
forall {a}. (a -> Bool) -> [a] -> [a]
filter a -> Bool
p [a]
x
    filterLast a -> Bool
p (a
x:[a]
xs) = a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:(a -> Bool) -> [a] -> [a]
filterLast a -> Bool
p [a]
xs
    getOutput' :: Handle -> IO [ByteString]
getOutput' Handle
h = do
      Bool
eof <- Handle -> IO Bool
hIsEOF Handle
h
      if Bool
eof
        then [ByteString] -> IO [ByteString]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        else (:) (ByteString -> [ByteString] -> [ByteString])
-> IO ByteString -> IO ([ByteString] -> [ByteString])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Handle -> IO ByteString
BS.hGetLine Handle
h IO ([ByteString] -> [ByteString])
-> IO [ByteString] -> IO [ByteString]
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Handle -> IO [ByteString]
getOutput Handle
h
    getOutput :: Handle -> IO [ByteString]
getOutput Handle
h = IO [ByteString]
-> (IOException -> IO [ByteString]) -> IO [ByteString]
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch
      (Handle -> IO [ByteString]
getOutput' Handle
h)
      (\(IOException
_ :: IOException) -> [ByteString] -> IO [ByteString]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ByteString
partialInstance])
    printContentOnError :: [ByteString] -> Maybe (IORef Bool) -> ProcessHandle -> IO ()
printContentOnError [ByteString]
out Maybe (IORef Bool)
abort ProcessHandle
ph = do
      ExitCode
code <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ph
      Bool
aborted <- IO Bool -> (IORef Bool -> IO Bool) -> Maybe (IORef Bool) -> IO Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) IORef Bool -> IO Bool
forall a. IORef a -> IO a
readIORef Maybe (IORef Bool)
abort
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ExitCode
code ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> ExitCode
ExitFailure Int
1 Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
aborted)
        (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putOutLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Failed parsing the Alloy code?:\n" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
content
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ExitCode
code ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> ExitCode
ExitFailure Int
2 Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
aborted)
        (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Lock -> IO () -> IO ()
forall a. Lock -> IO a -> IO a
withLock Lock
outLock (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ ByteString -> IO ()
BS.putStrLn (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ [ByteString] -> ByteString
BS.unlines [ByteString]
out

partialInstance :: ByteString
partialInstance :: ByteString
partialInstance = ByteString
"---PARTIAL_INSTANCE---"

{-|
Removes lines such as

@
[main] INFO kodkod.engine.config.Reporter - detecting symmetries ...
[main] INFO kodkod.engine.config.Reporter - detected 16 equivalence classes of atoms ...
[main] INFO kodkod.engine.config.Reporter - optimizing bounds and formula (breaking predicate symmetries, inlining, skolemizing) ...
[main] INFO kodkod.engine.config.Reporter - translating to boolean ...
[main] INFO kodkod.engine.config.Reporter - generating lex-leader symmetry breaking predicate ...
@

and

@
[main] WARN kodkod.engine.config.Reporter - Temporal formula: will be reduced to possibly unsound static version.
@

and

@
PARTIAL_INSTANCE
@

which seem to be appearing since Alloy-6.0.0
-}
removeInfoLines :: [ByteString] -> [ByteString]
removeInfoLines :: [ByteString] -> [ByteString]
removeInfoLines (ByteString
x:[ByteString]
xs)
  | Just ByteString
_ <- ByteString -> ByteString -> Maybe ByteString
BS.stripPrefix ByteString
"[main] INFO" ByteString
x
  = [ByteString] -> [ByteString]
removeInfoLines [ByteString]
xs
  | Just ByteString
_ <- ByteString -> ByteString -> Maybe ByteString
BS.stripPrefix ByteString
"[main] WARN" ByteString
x
  = [ByteString] -> [ByteString]
removeInfoLines [ByteString]
xs
  | ByteString
x ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
partialInstance
  = [ByteString] -> [ByteString]
removeInfoLines [ByteString]
xs
removeInfoLines [ByteString]
xs = [ByteString]
xs

{-|
Start a new sub process that communicates with the worker process
if a timeout is provided.
Execution is aborted by closing all handles and
killing the underlying worker processes after the given amount of time
(if it has not finished by then).
The process will wait for the sub process to make the result available.

If the provided timeout is 'Nothing', evaluation happens without
scheduled interruption in the main thread.
-}
withTimeout
  :: Handle
  -- ^ the input handle (of the worker) to close
  -> Handle
  -- ^ the output handle (of the worker) to close
  -> Handle
  -- ^ the error handle (of the worker) to close
  -> ProcessHandle
  -- ^ the worker process handle
  -> Maybe (IORef Bool)
  -- ^ the IORef to communicate process abortion on Windows
  -> Maybe Int
  -- ^ the timeout (Nothing if no timeout)
  -> IO a
  -- ^ some action interacting with the worker and its handles
  -> IO a
withTimeout :: forall a.
Handle
-> Handle
-> Handle
-> ProcessHandle
-> Maybe (IORef Bool)
-> Maybe Int
-> IO a
-> IO a
withTimeout Handle
_ Handle
_ Handle
_ ProcessHandle
_  Maybe (IORef Bool)
_     Maybe Int
Nothing  IO a
p = IO a
p
withTimeout Handle
i Handle
o Handle
e ProcessHandle
ph Maybe (IORef Bool)
abort (Just Int
t) IO a
p = IO a -> (Async a -> IO a) -> IO a
forall a b. IO a -> (Async a -> IO b) -> IO b
withAsync IO a
p ((Async a -> IO a) -> IO a) -> (Async a -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \Async a
a -> do
  Int -> IO ()
threadDelay Int
t
  Maybe (IORef Bool) -> (IORef Bool -> IO ()) -> IO ()
forall (m :: * -> *) a.
Applicative m =>
Maybe a -> (a -> m ()) -> m ()
whenJust Maybe (IORef Bool)
abort (IORef Bool -> Bool -> IO ()
forall a. IORef a -> a -> IO ()
`atomicWriteIORef` Bool
True)
  (IO () -> IO ()) -> [IO ()] -> IO ()
forall (f :: * -> *) a b. Foldable f => (a -> IO b) -> f a -> IO ()
mapConcurrently_ IO () -> IO ()
forall a. a -> a
id [
    Handle -> IO ()
hClose Handle
e,
    Handle -> IO ()
hClose Handle
o,
    ProcessHandle -> IO ()
terminateProcess ProcessHandle
ph
    ]
  Handle -> IO ()
hClose Handle
i
  Async a -> IO a
forall a. Async a -> IO a
wait Async a
a

{-|
Get the class path of all files in the data directory.

Returns the class path.
-}
getClassPath :: IO FilePath
getClassPath :: IO [Char]
getClassPath =
  [Char] -> [Char] -> [Char] -> ShowS
concatPaths ([Char] -> [Char] -> [Char] -> ShowS)
-> IO [Char] -> IO ([Char] -> [Char] -> ShowS)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [Char]
getDataDir IO ([Char] -> [Char] -> ShowS) -> IO [Char] -> IO ([Char] -> ShowS)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO [Char]
alloyJar IO ([Char] -> ShowS) -> IO [Char] -> IO ShowS
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO [Char]
commonsCliJar IO ShowS -> IO [Char] -> IO [Char]
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO [Char]
slf4jJar
  where
    concatPaths :: [Char] -> [Char] -> [Char] -> ShowS
concatPaths [Char]
w [Char]
x [Char]
y [Char]
z = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate
      [Char
searchPathSeparator]
      [[Char]
w, [Char]
x, [Char]
y, [Char]
z]