Language.Clafer.IG.AlloyIGInterface

Synopsis

• newtype AlloyIGT m a = AlloyIGT (StateT (Maybe AlloyIGEnv) (ReaderT Process m) a)
• fetch :: Monad m => AlloyIGT m AlloyIGEnv
• fetches :: Monad m => (AlloyIGEnv -> a) -> AlloyIGT m a
• set :: Monad m => AlloyIGEnv -> AlloyIGT m ()
• proc :: Monad m => AlloyIGT m Process
• data AlloyIGEnv = AlloyIGEnv {
  • alloyModel :: String
  • sigMap :: Map String Sig
  • scopes :: Map String Integer
  • globalScope :: Integer
  }
• data Sig = Sig {
  • s_name :: String
  • s_multiplicity :: Multiplicity
  • s_subset :: Maybe String
  • s_startingScope :: Maybe Integer
  }
• data Multiplicity
  • = One
  • | Lone
  • | Some
  • | Any
• data UnsatCore = UnsatCore {
  • core :: [Span]
  }
• withinRange :: Integer -> Multiplicity -> Bool
• runAlloyIGT :: MonadIO m => AlloyIGT m a -> m a
• getAlloyModel :: MonadIO m => AlloyIGT m String
• getSigs :: MonadIO m => AlloyIGT m [String]
• load :: Process -> String -> IO AlloyIGEnv
• sendLoadCommand :: MonadIO m => String -> AlloyIGT m ()
• sendNextCommand :: MonadIO m => AlloyIGT m (Maybe String)
• getScope :: MonadIO m => String -> AlloyIGT m Integer
• getScopes :: MonadIO m => AlloyIGT m [(String, Integer)]
• sendSetScopeCommand :: MonadIO m => String -> Integer -> AlloyIGT m (Maybe String)
• getGlobalScope :: MonadIO m => AlloyIGT m Integer
• sendSetGlobalScopeCommand :: MonadIO m => Integer -> AlloyIGT m ()
• sendResolveCommand :: MonadIO m => AlloyIGT m ()
• sendSaveStateCommand :: MonadIO m => AlloyIGT m ()
• sendRestoreStateCommand :: MonadIO m => AlloyIGT m ()
• sendRemoveConstraintCommand :: MonadIO m => Span -> AlloyIGT m ()
• sendUnsatCoreCommand :: MonadIO m => AlloyIGT m UnsatCore
• sendSetUnsatCoreMinimizationCommand :: MonadIO m => Integer -> AlloyIGT m ()
• sendSetBitwidthCommand :: MonadIO m => Integer -> AlloyIGT m ()
• sendQuitCommand :: MonadIO m => AlloyIGT m ()
• getMsg :: MonadIO m => AlloyIGT m String
• readMsg :: (MonadIO m, Read r) => AlloyIGT m r
• putMsg :: MonadIO m => String -> AlloyIGT m ()

Documentation