{-|
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, satSolver, timeout),
  SatSolver (..),
  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.Catch              (MonadThrow)
import Control.Monad.IO.Class           (MonadIO (liftIO))

{-|
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
  :: (MonadIO m, MonadThrow m)
  => Maybe Integer
  -- ^ How many instances to return; 'Nothing' for all.
  -> String
  -- ^ The Alloy specification which should be loaded.
  -> m [AlloyInstance]
getInstances :: forall (m :: * -> *).
(MonadIO m, MonadThrow m) =>
Maybe Integer -> String -> m [AlloyInstance]
getInstances Maybe Integer
maxIs = CallAlloyConfig -> String -> m [AlloyInstance]
forall (m :: * -> *).
(MonadIO m, MonadThrow m) =>
CallAlloyConfig -> String -> m [AlloyInstance]
getInstancesWith CallAlloyConfig
defaultCallAlloyConfig {
  maxInstances = 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
  :: (MonadIO m, MonadThrow m)
  => CallAlloyConfig
  -- ^ The configuration to be used.
  -> String
  -- ^ The Alloy specification which should be loaded.
  -> m [AlloyInstance]
getInstancesWith :: forall (m :: * -> *).
(MonadIO m, MonadThrow m) =>
CallAlloyConfig -> String -> m [AlloyInstance]
getInstancesWith CallAlloyConfig
config String
content =
  IO [ByteString] -> m [ByteString]
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (CallAlloyConfig -> String -> IO [ByteString]
getRawInstancesWith CallAlloyConfig
config String
content)
  m [ByteString]
-> ([ByteString] -> m [AlloyInstance]) -> m [AlloyInstance]
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (ByteString -> m AlloyInstance)
-> [ByteString] -> m [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 ByteString -> m AlloyInstance
forall (m :: * -> *).
(MonadIO m, MonadThrow 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
  :: (MonadIO m, MonadThrow m)
  => String
  -- ^ The Alloy specification which should be loaded.
  -> m Bool
  -- ^ Whether there exists an instance (within the relevant scope).
existsInstance :: forall (m :: * -> *). (MonadIO m, MonadThrow m) => String -> m Bool
existsInstance = ([AlloyInstance] -> Bool) -> m [AlloyInstance] -> m Bool
forall a b. (a -> b) -> m a -> m 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) (m [AlloyInstance] -> m Bool)
-> (String -> m [AlloyInstance]) -> String -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer -> String -> m [AlloyInstance]
forall (m :: * -> *).
(MonadIO m, MonadThrow m) =>
Maybe Integer -> String -> m [AlloyInstance]
getInstances (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1)