Language.Clafer.IG.ClaferIG

Documentation

claferIGVersion :: String

data IGArgs

Constructors

IGArgs

Fields

• all :: Maybe Integer
• saveDir :: Maybe FilePath
• claferModelFile :: FilePath
• alloySolution :: FilePath
• bitwidth :: Integer
• maxInt :: Integer
• useUids :: Bool
• addTypes :: Bool
• json :: Bool
• flatten_inheritance_comp :: Bool
• no_layout_comp :: Bool
• check_duplicates_comp :: Bool
• skip_resolver_comp :: Bool
• scope_strategy_comp :: ScopeStrategy

Instances

Data IGArgs

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IGArgs -> c IGArgs

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IGArgs

toConstr :: IGArgs -> Constr

dataTypeOf :: IGArgs -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c IGArgs)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IGArgs)

gmapT :: (forall b. Data b => b -> b) -> IGArgs -> IGArgs

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IGArgs -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IGArgs -> r

gmapQ :: (forall d. Data d => d -> u) -> IGArgs -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IGArgs -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IGArgs -> m IGArgs

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IGArgs -> m IGArgs

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IGArgs -> m IGArgs

Show IGArgs

Methods

showsPrec :: Int -> IGArgs -> ShowS

show :: IGArgs -> String

showList :: [IGArgs] -> ShowS

data ClaferIGEnv

Constructors

ClaferIGEnv

Fields

• claferEnv' :: ClaferEnv
• claferIGArgs :: IGArgs
• constraints :: [Constraint]
• claferModel :: String
• qNameMaps :: QNameMaps
• info :: UIDIClaferMap
• strMap :: Map Int String
• lineNumMap :: Map Integer String

getClaferEnv :: Monad m => ClaferIGT m ClaferEnv

getClaferIGArgs :: Monad m => ClaferIGT m IGArgs

getConstraints :: Monad m => ClaferIGT m [Constraint]

getClaferModel :: Monad m => ClaferIGT m String

getStrMap :: Monad m => ClaferIGT m (Map Int String)

getUIDIClaferMap :: Monad m => ClaferIGT m UIDIClaferMap

newtype ClaferIGT m a

Constructors

ClaferIGT (StateT ClaferIGEnv (AlloyIGT m) a)

Instances

MonadTrans ClaferIGT

Methods

lift :: Monad m => m a -> ClaferIGT m a

Monad m => Monad (ClaferIGT m)

Methods

(>>=) :: ClaferIGT m a -> (a -> ClaferIGT m b) -> ClaferIGT m b

(>>) :: ClaferIGT m a -> ClaferIGT m b -> ClaferIGT m b

return :: a -> ClaferIGT m a

fail :: String -> ClaferIGT m a

Functor m => Functor (ClaferIGT m)

Methods

fmap :: (a -> b) -> ClaferIGT m a -> ClaferIGT m b

(<$) :: a -> ClaferIGT m b -> ClaferIGT m a

Monad m => Applicative (ClaferIGT m)

Methods

pure :: a -> ClaferIGT m a

(<*>) :: ClaferIGT m (a -> b) -> ClaferIGT m a -> ClaferIGT m b

(*>) :: ClaferIGT m a -> ClaferIGT m b -> ClaferIGT m b

(<*) :: ClaferIGT m a -> ClaferIGT m b -> ClaferIGT m a

MonadIO m => MonadIO (ClaferIGT m)

Methods

liftIO :: IO a -> ClaferIGT m a

MonadException m => MonadException (ClaferIGT m)

Methods

controlIO :: (RunIO (ClaferIGT m) -> IO (ClaferIGT m a)) -> ClaferIGT m a

data Instance

Constructors

Instance

Fields

• modelInstance :: ClaferModel
• alloyModelInstance :: String

UnsatCore

Fields

• unsatConstraints :: [Constraint]
• counterexample :: Maybe Counterexample

NoInstance

data Counterexample

Constructors

Counterexample

Fields

• removedConstraints :: [Constraint]
• counterexampleInstance :: ClaferModel
• counterexampleAlloyInstance :: String

runClaferIGT :: MonadIO m => IGArgs -> ClaferIGT m a -> m (Either ClaferErrs a)

getAlloyModel :: MonadIO m => ClaferIGT m String

solve :: MonadIO m => ClaferIGT m ()

getClafers :: MonadIO m => ClaferIGT m [String]

getGlobalScope :: MonadIO m => ClaferIGT m Integer

getBitwidth :: MonadIO m => ClaferIGT m Integer

setGlobalScope :: MonadIO m => Integer -> ClaferIGT m ()

getScopes :: MonadIO m => ClaferIGT m [(String, Integer)]

getScope :: MonadIO m => QName -> ClaferIGT m [String]

getQNameMaps :: MonadIO m => ClaferIGT m QNameMaps

valueOfScope :: MonadIO m => String -> ClaferIGT m Integer

increaseScope :: MonadIO m => Integer -> (String, Integer) -> ClaferIGT m (Either String ())

setScope :: MonadIO m => Integer -> (String, Integer) -> ClaferIGT m (Either String ())

setAlloyScope :: MonadIO m => Integer -> String -> ClaferIGT m (Either String ())

next :: MonadIO m => ClaferIGT m Instance

setUnsatCoreMinimization :: MonadIO m => Integer -> ClaferIGT m ()

setBitwidth :: MonadIO m => Integer -> ClaferIGT m ()

quit :: MonadIO m => ClaferIGT m ()

reload :: MonadIO m => ClaferIGT m (Either ClaferErrs ())

findRemovable :: ClaferEnv -> [Span] -> [Constraint] -> [Maybe Constraint]

fst3 :: (t, t1, t2) -> t

getlineNumMap :: Monad m => ClaferIGT m (Map Integer String)

strictReadFile :: FilePath -> IO String

sigToClaferName :: String -> String