{-# LANGUAGE CPP #-}
-- | Defines a Monad context for calling Alloy

module Capabilities.Alloy (
  MonadAlloy (..),
  getInstances,
  maxBitWidth,
  ) where

import Control.Monad.Trans.Class        (MonadTrans (lift))
import Language.Alloy.Call (
  AlloyInstance,
  CallAlloyConfig (..),
  SatSolver (..),
  defaultCallAlloyConfig,
  )
import Control.OutputCapable.Blocks.Generic (
  GenericReportT
  )

class Monad m => MonadAlloy m where
  getInstancesWith :: CallAlloyConfig -> String -> m [AlloyInstance]

instance MonadAlloy m => MonadAlloy (GenericReportT l o m)  where
  getInstancesWith :: CallAlloyConfig -> String -> GenericReportT l o m [AlloyInstance]
getInstancesWith CallAlloyConfig
config = m [AlloyInstance] -> GenericReportT l o m [AlloyInstance]
forall (m :: * -> *) a. Monad m => m a -> GenericReportT l o m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m [AlloyInstance] -> GenericReportT l o m [AlloyInstance])
-> (String -> m [AlloyInstance])
-> String
-> GenericReportT l o m [AlloyInstance]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallAlloyConfig -> String -> m [AlloyInstance]
forall (m :: * -> *).
MonadAlloy m =>
CallAlloyConfig -> String -> m [AlloyInstance]
getInstancesWith CallAlloyConfig
config

getInstances
  :: MonadAlloy m
  => Maybe Integer
  -> Maybe Int
  -> String
  -> m [AlloyInstance]
getInstances :: forall (m :: * -> *).
MonadAlloy m =>
Maybe Integer -> Maybe Int -> String -> m [AlloyInstance]
getInstances Maybe Integer
maybeMaxInstances Maybe Int
maybeTimeout = CallAlloyConfig -> String -> m [AlloyInstance]
forall (m :: * -> *).
MonadAlloy m =>
CallAlloyConfig -> String -> m [AlloyInstance]
getInstancesWith
  (CallAlloyConfig -> String -> m [AlloyInstance])
-> CallAlloyConfig -> String -> m [AlloyInstance]
forall a b. (a -> b) -> a -> b
$ CallAlloyConfig
defaultCallAlloyConfig {
    maxInstances = maybeMaxInstances,
#if ALLOY_USE_SAT4J
    satSolver    = SAT4J,
#else
    satSolver    = MiniSat,
#endif
    timeout      = maybeTimeout
    }

maxBitWidth :: Maybe Int
maxBitWidth :: Maybe Int
maxBitWidth =
#ifdef MAX_BIT_WIDTH
  Just MAX_BIT_WIDTH
#else
  Maybe Int
forall a. Maybe a
Nothing
#endif