Hets - the Heterogeneous Tool Set

Copyright	(c) J. von Schroeder DFKI Bremen 2012
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability	provisional
Portability	non-portable
Safe Haskell	None

THF.Utils

Description

Documentation

newtype Unique a Source #

Constructors

Unique (UniqueT Identity a)

Instances

Instances details

Monad Unique Source #
Instance details Defined in THF.Utils Methods (>>=) :: Unique a -> (a -> Unique b) -> Unique b (>>) :: Unique a -> Unique b -> Unique b return :: a -> Unique a
Functor Unique Source #
Instance details Defined in THF.Utils Methods fmap :: (a -> b) -> Unique a -> Unique b (<$) :: a -> Unique b -> Unique a
Applicative Unique Source #
Instance details Defined in THF.Utils Methods pure :: a -> Unique a (<>) :: Unique (a -> b) -> Unique a -> Unique b liftA2 :: (a -> b -> c) -> Unique a -> Unique b -> Unique c (>) :: Unique a -> Unique b -> Unique b (<*) :: Unique a -> Unique b -> Unique a

data UniqueT m a Source #

Instances

Instances details

MonadTrans UniqueT Source #
Instance details Defined in THF.Utils Methods lift :: Monad m => m a -> UniqueT m a
Monad m => Monad (UniqueT m) Source #
Instance details Defined in THF.Utils Methods (>>=) :: UniqueT m a -> (a -> UniqueT m b) -> UniqueT m b (>>) :: UniqueT m a -> UniqueT m b -> UniqueT m b return :: a -> UniqueT m a
Functor m => Functor (UniqueT m) Source #
Instance details Defined in THF.Utils Methods fmap :: (a -> b) -> UniqueT m a -> UniqueT m b (<$) :: a -> UniqueT m b -> UniqueT m a
Monad m => Applicative (UniqueT m) Source #
Instance details Defined in THF.Utils Methods pure :: a -> UniqueT m a (<>) :: UniqueT m (a -> b) -> UniqueT m a -> UniqueT m b liftA2 :: (a -> b -> c) -> UniqueT m a -> UniqueT m b -> UniqueT m c (>) :: UniqueT m a -> UniqueT m b -> UniqueT m b (<*) :: UniqueT m a -> UniqueT m b -> UniqueT m a
MonadIO m => MonadIO (UniqueT m) Source #
Instance details Defined in THF.Utils Methods liftIO :: IO a -> UniqueT m a

fresh :: MonadUnique m => m Integer Source #

evalUniqueT :: Monad m => UniqueT m a -> m a Source #

evalUnique :: Unique a -> a Source #

numbered :: Monad m => AtomicWord -> UniqueT m AtomicWord Source #

numberedTok :: Monad m => Token -> UniqueT m Token Source #

mkNames :: Constant -> Name -> Int -> [(Constant, Name)] Source #

addSuffix :: String -> AtomicWord -> AtomicWord Source #

recreateSymbols :: SignTHF -> SignTHF Source #

thfTopLevelTypeToType :: THFTopLevelType -> Maybe Type Source #

typeToTopLevelType :: Type -> Result THFTopLevelType Source #

typeToUnitaryType :: Type -> Result THFUnitaryType Source #

typeToBinaryType :: Type -> Result THFBinaryType Source #

toToken :: Constant -> Token Source #

toId :: Constant -> Id Source #

data RewriteFuns a Source #

Constructors

Fields

rewriteLogicFormula :: (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
rewriteBinaryFormula :: (RewriteFuns a, a) -> THFBinaryFormula -> Result THFBinaryFormula
rewriteUnitaryFormula :: (RewriteFuns a, a) -> THFUnitaryFormula -> Result THFUnitaryFormula
rewriteBinaryPair :: (RewriteFuns a, a) -> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula) -> Result THFBinaryFormula
rewriteBinaryTuple :: (RewriteFuns a, a) -> THFBinaryTuple -> Result THFBinaryTuple
rewriteQuantifiedFormula :: (RewriteFuns a, a) -> THFQuantifiedFormula -> Result THFQuantifiedFormula
rewriteAtom :: (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula
rewriteVariableList :: (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
rewriteConst :: (RewriteFuns a, a) -> Constant -> Result THFUnitaryFormula
rewriteConnTerm :: (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm

rewriteSenFun :: (RewriteFuns a, a) -> Named THFFormula -> Result (Named THFFormula) Source #

rewriteTHF0 :: RewriteFuns a Source #

data AnaFuns a b Source #

Constructors

Fields

anaLogicFormula :: (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaBinaryFormula :: (AnaFuns a b, a) -> THFBinaryFormula -> Result [b]
anaUnitaryFormula :: (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaBinaryPair :: (AnaFuns a b, a) -> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula) -> Result [b]
anaBinaryTuple :: (AnaFuns a b, a) -> THFBinaryTuple -> Result [b]
anaQuantifiedFormula :: (AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b]
anaAtom :: (AnaFuns a b, a) -> THFAtom -> Result [b]
anaVariableList :: (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaConst :: (AnaFuns a b, a) -> Constant -> Result [b]
anaConnTerm :: (AnaFuns a b, a) -> THFConnTerm -> Result [b]

anaSenFun :: (AnaFuns a b, a) -> Named THFFormula -> Result [b] Source #

anaTHF0 :: AnaFuns a b Source #