{-|
Module      : Language.Alloy.Call
Description : A simple library to call Alloy given a specification
Copyright   : (c) Marcellus Siegburg, 2019 - 2021
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 user's 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 (
  CallAlloyConfig (maxInstances, noOverflow, timeout),
  defaultCallAlloyConfig,
  existsInstance,
  getInstances,
  getInstancesWith,
  module Functions,
  module Types,
  ) where

import Language.Alloy.Functions         as Functions
import Language.Alloy.Internal.Call
import Language.Alloy.Parser            (parseInstance)
import Language.Alloy.Types             as Types
  (AlloyInstance, AlloySig, Entries, Object, Signature)

import Control.Monad.Trans.Except       (runExceptT)

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

{-|
This function may be used to get all model instances for a given Alloy
specification. It calls Alloy via a Java interface and parses the raw instance
answers before returning the resulting list of 'AlloyInstance's.
Parameters are set using a 'CallAlloyConfig'.
-}
getInstancesWith
  :: CallAlloyConfig
  -- ^ The configuration to be used.
  -> String
  -- ^ The Alloy specification which should be loaded.
  -> IO [AlloyInstance]
getInstancesWith :: CallAlloyConfig -> String -> IO [AlloyInstance]
getInstancesWith CallAlloyConfig
config String
content =
  CallAlloyConfig -> String -> IO [ByteString]
getRawInstancesWith CallAlloyConfig
config String
content
  IO [ByteString]
-> ([ByteString] -> IO [AlloyInstance]) -> IO [AlloyInstance]
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (ByteString -> IO AlloyInstance)
-> [ByteString] -> IO [AlloyInstance]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Either ErrInfo AlloyInstance -> AlloyInstance)
-> IO (Either ErrInfo AlloyInstance) -> IO AlloyInstance
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ErrInfo -> AlloyInstance)
-> (AlloyInstance -> AlloyInstance)
-> Either ErrInfo AlloyInstance
-> AlloyInstance
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> AlloyInstance
forall a. HasCallStack => String -> a
error (String -> AlloyInstance)
-> (ErrInfo -> String) -> ErrInfo -> AlloyInstance
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrInfo -> String
forall a. Show a => a -> String
show) AlloyInstance -> AlloyInstance
forall a. a -> a
id) (IO (Either ErrInfo AlloyInstance) -> IO AlloyInstance)
-> (ByteString -> IO (Either ErrInfo AlloyInstance))
-> ByteString
-> IO AlloyInstance
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT ErrInfo IO AlloyInstance
-> IO (Either ErrInfo AlloyInstance)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT ErrInfo IO AlloyInstance
 -> IO (Either ErrInfo AlloyInstance))
-> (ByteString -> ExceptT ErrInfo IO AlloyInstance)
-> ByteString
-> IO (Either ErrInfo AlloyInstance)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ExceptT ErrInfo IO AlloyInstance
forall (m :: * -> *).
(MonadIO m, MonadError ErrInfo m) =>
ByteString -> m AlloyInstance
parseInstance)

{-|
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 relevant scope).
existsInstance :: String -> IO Bool
existsInstance = ([AlloyInstance] -> Bool) -> IO [AlloyInstance] -> IO Bool
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Bool
not (Bool -> Bool)
-> ([AlloyInstance] -> Bool) -> [AlloyInstance] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AlloyInstance] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (IO [AlloyInstance] -> IO Bool)
-> (String -> IO [AlloyInstance]) -> String -> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer -> String -> IO [AlloyInstance]
getInstances (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1)