{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./TPTP/Sign.hs Description : Data structures representing TPTP signatures. Copyright : (c) Eugen Kuksa University of Magdeburg 2017 License : GPLv2 or higher, see LICENSE.txt Maintainer : Eugen Kuksa <kuksa@iks.cs.ovgu.de> Stability : provisional Portability : non-portable (imports Logic) Data structures representing TPTP signatures. -} module TPTP.Sign where import TPTP.AS import Common.Id import Data.Data import qualified Data.Map as Map import qualified Data.Set as Set type Sentence = Annotated_formula data Symbol = Symbol { Symbol -> Token symbolId :: Token , Symbol -> SymbolType symbolType :: SymbolType } deriving (Int -> Symbol -> ShowS [Symbol] -> ShowS Symbol -> String (Int -> Symbol -> ShowS) -> (Symbol -> String) -> ([Symbol] -> ShowS) -> Show Symbol forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Symbol] -> ShowS $cshowList :: [Symbol] -> ShowS show :: Symbol -> String $cshow :: Symbol -> String showsPrec :: Int -> Symbol -> ShowS $cshowsPrec :: Int -> Symbol -> ShowS Show, Eq Symbol Eq Symbol => (Symbol -> Symbol -> Ordering) -> (Symbol -> Symbol -> Bool) -> (Symbol -> Symbol -> Bool) -> (Symbol -> Symbol -> Bool) -> (Symbol -> Symbol -> Bool) -> (Symbol -> Symbol -> Symbol) -> (Symbol -> Symbol -> Symbol) -> Ord Symbol Symbol -> Symbol -> Bool Symbol -> Symbol -> Ordering Symbol -> Symbol -> Symbol forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Symbol -> Symbol -> Symbol $cmin :: Symbol -> Symbol -> Symbol max :: Symbol -> Symbol -> Symbol $cmax :: Symbol -> Symbol -> Symbol >= :: Symbol -> Symbol -> Bool $c>= :: Symbol -> Symbol -> Bool > :: Symbol -> Symbol -> Bool $c> :: Symbol -> Symbol -> Bool <= :: Symbol -> Symbol -> Bool $c<= :: Symbol -> Symbol -> Bool < :: Symbol -> Symbol -> Bool $c< :: Symbol -> Symbol -> Bool compare :: Symbol -> Symbol -> Ordering $ccompare :: Symbol -> Symbol -> Ordering $cp1Ord :: Eq Symbol Ord, Symbol -> Symbol -> Bool (Symbol -> Symbol -> Bool) -> (Symbol -> Symbol -> Bool) -> Eq Symbol forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Symbol -> Symbol -> Bool $c/= :: Symbol -> Symbol -> Bool == :: Symbol -> Symbol -> Bool $c== :: Symbol -> Symbol -> Bool Eq, Typeable Symbol Constr DataType Typeable Symbol => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol) -> (Symbol -> Constr) -> (Symbol -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Symbol)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)) -> ((forall b. Data b => b -> b) -> Symbol -> Symbol) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r) -> (forall u. (forall d. Data d => d -> u) -> Symbol -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol) -> Data Symbol Symbol -> Constr Symbol -> DataType (forall b. Data b => b -> b) -> Symbol -> Symbol (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u forall u. (forall d. Data d => d -> u) -> Symbol -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Symbol) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol) $cSymbol :: Constr $tSymbol :: DataType gmapMo :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol gmapMp :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol gmapM :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol gmapQi :: Int -> (forall d. Data d => d -> u) -> Symbol -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u gmapQ :: (forall d. Data d => d -> u) -> Symbol -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Symbol -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r gmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol $cgmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Symbol) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Symbol) dataTypeOf :: Symbol -> DataType $cdataTypeOf :: Symbol -> DataType toConstr :: Symbol -> Constr $ctoConstr :: Symbol -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol $cp1Data :: Typeable Symbol Data, Typeable) instance GetRange Symbol where getRange :: Symbol -> Range getRange = [Pos] -> Range Range ([Pos] -> Range) -> (Symbol -> [Pos]) -> Symbol -> Range forall b c a. (b -> c) -> (a -> b) -> a -> c . Symbol -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan rangeSpan :: Symbol -> [Pos] rangeSpan = Token -> [Pos] tokenRange (Token -> [Pos]) -> (Symbol -> Token) -> Symbol -> [Pos] forall b c a. (b -> c) -> (a -> b) -> a -> c . Symbol -> Token symbolId data SymbolType = Constant | Number | Predicate | Proposition | Function | TypeConstant | TypeFunctor deriving (Int -> SymbolType -> ShowS [SymbolType] -> ShowS SymbolType -> String (Int -> SymbolType -> ShowS) -> (SymbolType -> String) -> ([SymbolType] -> ShowS) -> Show SymbolType forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [SymbolType] -> ShowS $cshowList :: [SymbolType] -> ShowS show :: SymbolType -> String $cshow :: SymbolType -> String showsPrec :: Int -> SymbolType -> ShowS $cshowsPrec :: Int -> SymbolType -> ShowS Show, Eq SymbolType Eq SymbolType => (SymbolType -> SymbolType -> Ordering) -> (SymbolType -> SymbolType -> Bool) -> (SymbolType -> SymbolType -> Bool) -> (SymbolType -> SymbolType -> Bool) -> (SymbolType -> SymbolType -> Bool) -> (SymbolType -> SymbolType -> SymbolType) -> (SymbolType -> SymbolType -> SymbolType) -> Ord SymbolType SymbolType -> SymbolType -> Bool SymbolType -> SymbolType -> Ordering SymbolType -> SymbolType -> SymbolType forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: SymbolType -> SymbolType -> SymbolType $cmin :: SymbolType -> SymbolType -> SymbolType max :: SymbolType -> SymbolType -> SymbolType $cmax :: SymbolType -> SymbolType -> SymbolType >= :: SymbolType -> SymbolType -> Bool $c>= :: SymbolType -> SymbolType -> Bool > :: SymbolType -> SymbolType -> Bool $c> :: SymbolType -> SymbolType -> Bool <= :: SymbolType -> SymbolType -> Bool $c<= :: SymbolType -> SymbolType -> Bool < :: SymbolType -> SymbolType -> Bool $c< :: SymbolType -> SymbolType -> Bool compare :: SymbolType -> SymbolType -> Ordering $ccompare :: SymbolType -> SymbolType -> Ordering $cp1Ord :: Eq SymbolType Ord, SymbolType -> SymbolType -> Bool (SymbolType -> SymbolType -> Bool) -> (SymbolType -> SymbolType -> Bool) -> Eq SymbolType forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: SymbolType -> SymbolType -> Bool $c/= :: SymbolType -> SymbolType -> Bool == :: SymbolType -> SymbolType -> Bool $c== :: SymbolType -> SymbolType -> Bool Eq, Typeable SymbolType Constr DataType Typeable SymbolType => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolType -> c SymbolType) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolType) -> (SymbolType -> Constr) -> (SymbolType -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymbolType)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType)) -> ((forall b. Data b => b -> b) -> SymbolType -> SymbolType) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r) -> (forall u. (forall d. Data d => d -> u) -> SymbolType -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> SymbolType -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType) -> Data SymbolType SymbolType -> Constr SymbolType -> DataType (forall b. Data b => b -> b) -> SymbolType -> SymbolType (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolType -> c SymbolType (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolType forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> SymbolType -> u forall u. (forall d. Data d => d -> u) -> SymbolType -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolType forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolType -> c SymbolType forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymbolType) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType) $cTypeFunctor :: Constr $cTypeConstant :: Constr $cFunction :: Constr $cProposition :: Constr $cPredicate :: Constr $cNumber :: Constr $cConstant :: Constr $tSymbolType :: DataType gmapMo :: (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType gmapMp :: (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType gmapM :: (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbolType -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymbolType -> u gmapQ :: (forall d. Data d => d -> u) -> SymbolType -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymbolType -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r gmapT :: (forall b. Data b => b -> b) -> SymbolType -> SymbolType $cgmapT :: (forall b. Data b => b -> b) -> SymbolType -> SymbolType dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SymbolType) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymbolType) dataTypeOf :: SymbolType -> DataType $cdataTypeOf :: SymbolType -> DataType toConstr :: SymbolType -> Constr $ctoConstr :: SymbolType -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolType $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolType gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolType -> c SymbolType $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolType -> c SymbolType $cp1Data :: Typeable SymbolType Data, Typeable) instance GetRange SymbolType symbolTypeS :: Symbol -> String symbolTypeS :: Symbol -> String symbolTypeS = SymbolType -> String forall a. Show a => a -> String show (SymbolType -> String) -> (Symbol -> SymbolType) -> Symbol -> String forall b c a. (b -> c) -> (a -> b) -> a -> c . Symbol -> SymbolType symbolType type ConstantSet = Set.Set Constant type FunctorMap = Map.Map TPTP_functor FunctorType type NumberSet = Set.Set Number type PropositionSet = Set.Set Proposition type THFTypeDeclarationMap = Map.Map THFTypeable THF_top_level_type type TFFTypeDeclarationMap = Map.Map Untyped_atom TFF_top_level_type type THFPredicateMap = THFTypeDeclarationMap type TFFPredicateMap = TFFTypeDeclarationMap type FOFPredicateMap = Map.Map Predicate (Set.Set Int) type FOFFunctorMap = Map.Map TPTP_functor (Set.Set Int) type THFTypeConstantMap = THFTypeDeclarationMap type TFFTypeConstantMap = TFFTypeDeclarationMap type THFTypeFunctorMap = THFTypeDeclarationMap type TFFTypeFunctorMap = TFFTypeDeclarationMap type THFSubTypeMap = Map.Map THF_atom THF_atom type TFFSubTypeMap = Map.Map Untyped_atom Atom data THFTypeable = THFTypeFormula THF_typeable_formula | THFTypeConstant Constant deriving (Int -> THFTypeable -> ShowS [THFTypeable] -> ShowS THFTypeable -> String (Int -> THFTypeable -> ShowS) -> (THFTypeable -> String) -> ([THFTypeable] -> ShowS) -> Show THFTypeable forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [THFTypeable] -> ShowS $cshowList :: [THFTypeable] -> ShowS show :: THFTypeable -> String $cshow :: THFTypeable -> String showsPrec :: Int -> THFTypeable -> ShowS $cshowsPrec :: Int -> THFTypeable -> ShowS Show, THFTypeable -> THFTypeable -> Bool (THFTypeable -> THFTypeable -> Bool) -> (THFTypeable -> THFTypeable -> Bool) -> Eq THFTypeable forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: THFTypeable -> THFTypeable -> Bool $c/= :: THFTypeable -> THFTypeable -> Bool == :: THFTypeable -> THFTypeable -> Bool $c== :: THFTypeable -> THFTypeable -> Bool Eq, Eq THFTypeable Eq THFTypeable => (THFTypeable -> THFTypeable -> Ordering) -> (THFTypeable -> THFTypeable -> Bool) -> (THFTypeable -> THFTypeable -> Bool) -> (THFTypeable -> THFTypeable -> Bool) -> (THFTypeable -> THFTypeable -> Bool) -> (THFTypeable -> THFTypeable -> THFTypeable) -> (THFTypeable -> THFTypeable -> THFTypeable) -> Ord THFTypeable THFTypeable -> THFTypeable -> Bool THFTypeable -> THFTypeable -> Ordering THFTypeable -> THFTypeable -> THFTypeable forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: THFTypeable -> THFTypeable -> THFTypeable $cmin :: THFTypeable -> THFTypeable -> THFTypeable max :: THFTypeable -> THFTypeable -> THFTypeable $cmax :: THFTypeable -> THFTypeable -> THFTypeable >= :: THFTypeable -> THFTypeable -> Bool $c>= :: THFTypeable -> THFTypeable -> Bool > :: THFTypeable -> THFTypeable -> Bool $c> :: THFTypeable -> THFTypeable -> Bool <= :: THFTypeable -> THFTypeable -> Bool $c<= :: THFTypeable -> THFTypeable -> Bool < :: THFTypeable -> THFTypeable -> Bool $c< :: THFTypeable -> THFTypeable -> Bool compare :: THFTypeable -> THFTypeable -> Ordering $ccompare :: THFTypeable -> THFTypeable -> Ordering $cp1Ord :: Eq THFTypeable Ord, Typeable THFTypeable Constr DataType Typeable THFTypeable => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFTypeable -> c THFTypeable) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFTypeable) -> (THFTypeable -> Constr) -> (THFTypeable -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFTypeable)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFTypeable)) -> ((forall b. Data b => b -> b) -> THFTypeable -> THFTypeable) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeable -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeable -> r) -> (forall u. (forall d. Data d => d -> u) -> THFTypeable -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> THFTypeable -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable) -> Data THFTypeable THFTypeable -> Constr THFTypeable -> DataType (forall b. Data b => b -> b) -> THFTypeable -> THFTypeable (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFTypeable -> c THFTypeable (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFTypeable forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> THFTypeable -> u forall u. (forall d. Data d => d -> u) -> THFTypeable -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeable -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeable -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFTypeable forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFTypeable -> c THFTypeable forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFTypeable) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFTypeable) $cTHFTypeConstant :: Constr $cTHFTypeFormula :: Constr $tTHFTypeable :: DataType gmapMo :: (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable gmapMp :: (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable gmapM :: (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> THFTypeable -> m THFTypeable gmapQi :: Int -> (forall d. Data d => d -> u) -> THFTypeable -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> THFTypeable -> u gmapQ :: (forall d. Data d => d -> u) -> THFTypeable -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> THFTypeable -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeable -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeable -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeable -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeable -> r gmapT :: (forall b. Data b => b -> b) -> THFTypeable -> THFTypeable $cgmapT :: (forall b. Data b => b -> b) -> THFTypeable -> THFTypeable dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFTypeable) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFTypeable) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c THFTypeable) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFTypeable) dataTypeOf :: THFTypeable -> DataType $cdataTypeOf :: THFTypeable -> DataType toConstr :: THFTypeable -> Constr $ctoConstr :: THFTypeable -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFTypeable $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFTypeable gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFTypeable -> c THFTypeable $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFTypeable -> c THFTypeable $cp1Data :: Typeable THFTypeable Data, Typeable) data FunctorType = FunctorTHF THF_arguments | FunctorFOF FOF_arguments deriving (Int -> FunctorType -> ShowS [FunctorType] -> ShowS FunctorType -> String (Int -> FunctorType -> ShowS) -> (FunctorType -> String) -> ([FunctorType] -> ShowS) -> Show FunctorType forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [FunctorType] -> ShowS $cshowList :: [FunctorType] -> ShowS show :: FunctorType -> String $cshow :: FunctorType -> String showsPrec :: Int -> FunctorType -> ShowS $cshowsPrec :: Int -> FunctorType -> ShowS Show, FunctorType -> FunctorType -> Bool (FunctorType -> FunctorType -> Bool) -> (FunctorType -> FunctorType -> Bool) -> Eq FunctorType forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: FunctorType -> FunctorType -> Bool $c/= :: FunctorType -> FunctorType -> Bool == :: FunctorType -> FunctorType -> Bool $c== :: FunctorType -> FunctorType -> Bool Eq, Eq FunctorType Eq FunctorType => (FunctorType -> FunctorType -> Ordering) -> (FunctorType -> FunctorType -> Bool) -> (FunctorType -> FunctorType -> Bool) -> (FunctorType -> FunctorType -> Bool) -> (FunctorType -> FunctorType -> Bool) -> (FunctorType -> FunctorType -> FunctorType) -> (FunctorType -> FunctorType -> FunctorType) -> Ord FunctorType FunctorType -> FunctorType -> Bool FunctorType -> FunctorType -> Ordering FunctorType -> FunctorType -> FunctorType forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: FunctorType -> FunctorType -> FunctorType $cmin :: FunctorType -> FunctorType -> FunctorType max :: FunctorType -> FunctorType -> FunctorType $cmax :: FunctorType -> FunctorType -> FunctorType >= :: FunctorType -> FunctorType -> Bool $c>= :: FunctorType -> FunctorType -> Bool > :: FunctorType -> FunctorType -> Bool $c> :: FunctorType -> FunctorType -> Bool <= :: FunctorType -> FunctorType -> Bool $c<= :: FunctorType -> FunctorType -> Bool < :: FunctorType -> FunctorType -> Bool $c< :: FunctorType -> FunctorType -> Bool compare :: FunctorType -> FunctorType -> Ordering $ccompare :: FunctorType -> FunctorType -> Ordering $cp1Ord :: Eq FunctorType Ord, Typeable FunctorType Constr DataType Typeable FunctorType => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctorType -> c FunctorType) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunctorType) -> (FunctorType -> Constr) -> (FunctorType -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunctorType)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunctorType)) -> ((forall b. Data b => b -> b) -> FunctorType -> FunctorType) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctorType -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctorType -> r) -> (forall u. (forall d. Data d => d -> u) -> FunctorType -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> FunctorType -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType) -> Data FunctorType FunctorType -> Constr FunctorType -> DataType (forall b. Data b => b -> b) -> FunctorType -> FunctorType (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctorType -> c FunctorType (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunctorType forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> FunctorType -> u forall u. (forall d. Data d => d -> u) -> FunctorType -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctorType -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctorType -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunctorType forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctorType -> c FunctorType forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunctorType) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunctorType) $cFunctorFOF :: Constr $cFunctorTHF :: Constr $tFunctorType :: DataType gmapMo :: (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType gmapMp :: (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType gmapM :: (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> FunctorType -> m FunctorType gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctorType -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FunctorType -> u gmapQ :: (forall d. Data d => d -> u) -> FunctorType -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> FunctorType -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctorType -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctorType -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctorType -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctorType -> r gmapT :: (forall b. Data b => b -> b) -> FunctorType -> FunctorType $cgmapT :: (forall b. Data b => b -> b) -> FunctorType -> FunctorType dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunctorType) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunctorType) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FunctorType) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunctorType) dataTypeOf :: FunctorType -> DataType $cdataTypeOf :: FunctorType -> DataType toConstr :: FunctorType -> Constr $ctoConstr :: FunctorType -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunctorType $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunctorType gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctorType -> c FunctorType $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctorType -> c FunctorType $cp1Data :: Typeable FunctorType Data, Typeable) data PredicateType = PredicateType FOF_arguments deriving (Int -> PredicateType -> ShowS [PredicateType] -> ShowS PredicateType -> String (Int -> PredicateType -> ShowS) -> (PredicateType -> String) -> ([PredicateType] -> ShowS) -> Show PredicateType forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [PredicateType] -> ShowS $cshowList :: [PredicateType] -> ShowS show :: PredicateType -> String $cshow :: PredicateType -> String showsPrec :: Int -> PredicateType -> ShowS $cshowsPrec :: Int -> PredicateType -> ShowS Show, PredicateType -> PredicateType -> Bool (PredicateType -> PredicateType -> Bool) -> (PredicateType -> PredicateType -> Bool) -> Eq PredicateType forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: PredicateType -> PredicateType -> Bool $c/= :: PredicateType -> PredicateType -> Bool == :: PredicateType -> PredicateType -> Bool $c== :: PredicateType -> PredicateType -> Bool Eq, Eq PredicateType Eq PredicateType => (PredicateType -> PredicateType -> Ordering) -> (PredicateType -> PredicateType -> Bool) -> (PredicateType -> PredicateType -> Bool) -> (PredicateType -> PredicateType -> Bool) -> (PredicateType -> PredicateType -> Bool) -> (PredicateType -> PredicateType -> PredicateType) -> (PredicateType -> PredicateType -> PredicateType) -> Ord PredicateType PredicateType -> PredicateType -> Bool PredicateType -> PredicateType -> Ordering PredicateType -> PredicateType -> PredicateType forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: PredicateType -> PredicateType -> PredicateType $cmin :: PredicateType -> PredicateType -> PredicateType max :: PredicateType -> PredicateType -> PredicateType $cmax :: PredicateType -> PredicateType -> PredicateType >= :: PredicateType -> PredicateType -> Bool $c>= :: PredicateType -> PredicateType -> Bool > :: PredicateType -> PredicateType -> Bool $c> :: PredicateType -> PredicateType -> Bool <= :: PredicateType -> PredicateType -> Bool $c<= :: PredicateType -> PredicateType -> Bool < :: PredicateType -> PredicateType -> Bool $c< :: PredicateType -> PredicateType -> Bool compare :: PredicateType -> PredicateType -> Ordering $ccompare :: PredicateType -> PredicateType -> Ordering $cp1Ord :: Eq PredicateType Ord, Typeable PredicateType Constr DataType Typeable PredicateType => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PredicateType -> c PredicateType) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PredicateType) -> (PredicateType -> Constr) -> (PredicateType -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PredicateType)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredicateType)) -> ((forall b. Data b => b -> b) -> PredicateType -> PredicateType) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PredicateType -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PredicateType -> r) -> (forall u. (forall d. Data d => d -> u) -> PredicateType -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> PredicateType -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType) -> Data PredicateType PredicateType -> Constr PredicateType -> DataType (forall b. Data b => b -> b) -> PredicateType -> PredicateType (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PredicateType -> c PredicateType (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PredicateType forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> PredicateType -> u forall u. (forall d. Data d => d -> u) -> PredicateType -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PredicateType -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PredicateType -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PredicateType forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PredicateType -> c PredicateType forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PredicateType) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredicateType) $cPredicateType :: Constr $tPredicateType :: DataType gmapMo :: (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType gmapMp :: (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType gmapM :: (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> PredicateType -> m PredicateType gmapQi :: Int -> (forall d. Data d => d -> u) -> PredicateType -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PredicateType -> u gmapQ :: (forall d. Data d => d -> u) -> PredicateType -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> PredicateType -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PredicateType -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PredicateType -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PredicateType -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PredicateType -> r gmapT :: (forall b. Data b => b -> b) -> PredicateType -> PredicateType $cgmapT :: (forall b. Data b => b -> b) -> PredicateType -> PredicateType dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredicateType) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredicateType) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PredicateType) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PredicateType) dataTypeOf :: PredicateType -> DataType $cdataTypeOf :: PredicateType -> DataType toConstr :: PredicateType -> Constr $ctoConstr :: PredicateType -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PredicateType $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PredicateType gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PredicateType -> c PredicateType $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PredicateType -> c PredicateType $cp1Data :: Typeable PredicateType Data, Typeable) data Type_functorType = Type_functorType TFF_type_arguments deriving (Int -> Type_functorType -> ShowS [Type_functorType] -> ShowS Type_functorType -> String (Int -> Type_functorType -> ShowS) -> (Type_functorType -> String) -> ([Type_functorType] -> ShowS) -> Show Type_functorType forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Type_functorType] -> ShowS $cshowList :: [Type_functorType] -> ShowS show :: Type_functorType -> String $cshow :: Type_functorType -> String showsPrec :: Int -> Type_functorType -> ShowS $cshowsPrec :: Int -> Type_functorType -> ShowS Show, Type_functorType -> Type_functorType -> Bool (Type_functorType -> Type_functorType -> Bool) -> (Type_functorType -> Type_functorType -> Bool) -> Eq Type_functorType forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Type_functorType -> Type_functorType -> Bool $c/= :: Type_functorType -> Type_functorType -> Bool == :: Type_functorType -> Type_functorType -> Bool $c== :: Type_functorType -> Type_functorType -> Bool Eq, Eq Type_functorType Eq Type_functorType => (Type_functorType -> Type_functorType -> Ordering) -> (Type_functorType -> Type_functorType -> Bool) -> (Type_functorType -> Type_functorType -> Bool) -> (Type_functorType -> Type_functorType -> Bool) -> (Type_functorType -> Type_functorType -> Bool) -> (Type_functorType -> Type_functorType -> Type_functorType) -> (Type_functorType -> Type_functorType -> Type_functorType) -> Ord Type_functorType Type_functorType -> Type_functorType -> Bool Type_functorType -> Type_functorType -> Ordering Type_functorType -> Type_functorType -> Type_functorType forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Type_functorType -> Type_functorType -> Type_functorType $cmin :: Type_functorType -> Type_functorType -> Type_functorType max :: Type_functorType -> Type_functorType -> Type_functorType $cmax :: Type_functorType -> Type_functorType -> Type_functorType >= :: Type_functorType -> Type_functorType -> Bool $c>= :: Type_functorType -> Type_functorType -> Bool > :: Type_functorType -> Type_functorType -> Bool $c> :: Type_functorType -> Type_functorType -> Bool <= :: Type_functorType -> Type_functorType -> Bool $c<= :: Type_functorType -> Type_functorType -> Bool < :: Type_functorType -> Type_functorType -> Bool $c< :: Type_functorType -> Type_functorType -> Bool compare :: Type_functorType -> Type_functorType -> Ordering $ccompare :: Type_functorType -> Type_functorType -> Ordering $cp1Ord :: Eq Type_functorType Ord, Typeable Type_functorType Constr DataType Typeable Type_functorType => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type_functorType -> c Type_functorType) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type_functorType) -> (Type_functorType -> Constr) -> (Type_functorType -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type_functorType)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type_functorType)) -> ((forall b. Data b => b -> b) -> Type_functorType -> Type_functorType) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type_functorType -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type_functorType -> r) -> (forall u. (forall d. Data d => d -> u) -> Type_functorType -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> Type_functorType -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType) -> Data Type_functorType Type_functorType -> Constr Type_functorType -> DataType (forall b. Data b => b -> b) -> Type_functorType -> Type_functorType (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type_functorType -> c Type_functorType (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type_functorType forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> Type_functorType -> u forall u. (forall d. Data d => d -> u) -> Type_functorType -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type_functorType -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type_functorType -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type_functorType forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type_functorType -> c Type_functorType forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type_functorType) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type_functorType) $cType_functorType :: Constr $tType_functorType :: DataType gmapMo :: (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType gmapMp :: (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType gmapM :: (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Type_functorType -> m Type_functorType gmapQi :: Int -> (forall d. Data d => d -> u) -> Type_functorType -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type_functorType -> u gmapQ :: (forall d. Data d => d -> u) -> Type_functorType -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type_functorType -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type_functorType -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type_functorType -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type_functorType -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type_functorType -> r gmapT :: (forall b. Data b => b -> b) -> Type_functorType -> Type_functorType $cgmapT :: (forall b. Data b => b -> b) -> Type_functorType -> Type_functorType dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type_functorType) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type_functorType) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Type_functorType) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type_functorType) dataTypeOf :: Type_functorType -> DataType $cdataTypeOf :: Type_functorType -> DataType toConstr :: Type_functorType -> Constr $ctoConstr :: Type_functorType -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type_functorType $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type_functorType gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type_functorType -> c Type_functorType $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type_functorType -> c Type_functorType $cp1Data :: Typeable Type_functorType Data, Typeable) data Sign = Sign { Sign -> ConstantSet constantSet :: ConstantSet , Sign -> NumberSet numberSet :: NumberSet , Sign -> ConstantSet propositionSet :: PropositionSet , Sign -> THFSubTypeMap thfSubtypeMap :: THFSubTypeMap , Sign -> TFFSubTypeMap tffSubtypeMap :: TFFSubTypeMap , Sign -> THFPredicateMap thfPredicateMap :: THFPredicateMap , Sign -> TFFPredicateMap tffPredicateMap :: TFFPredicateMap , Sign -> FOFPredicateMap fofPredicateMap :: FOFPredicateMap , Sign -> FOFPredicateMap fofFunctorMap :: FOFFunctorMap , Sign -> THFPredicateMap thfTypeConstantMap :: THFTypeConstantMap , Sign -> TFFPredicateMap tffTypeConstantMap :: TFFTypeConstantMap , Sign -> THFPredicateMap thfTypeFunctorMap :: THFTypeFunctorMap , Sign -> TFFPredicateMap tffTypeFunctorMap :: TFFTypeFunctorMap -- The following maps are just temporary and ignored after -- static analysis in favor of thfPreficateMap, thfTypeFunctorMap, -- tffPredicateMap and tffTypeFunctorMap , Sign -> THFPredicateMap thfTypeDeclarationMap :: THFTypeDeclarationMap , Sign -> TFFPredicateMap tffTypeDeclarationMap :: TFFTypeDeclarationMap } deriving (Int -> Sign -> ShowS [Sign] -> ShowS Sign -> String (Int -> Sign -> ShowS) -> (Sign -> String) -> ([Sign] -> ShowS) -> Show Sign forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Sign] -> ShowS $cshowList :: [Sign] -> ShowS show :: Sign -> String $cshow :: Sign -> String showsPrec :: Int -> Sign -> ShowS $cshowsPrec :: Int -> Sign -> ShowS Show, Sign -> Sign -> Bool (Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> Eq Sign forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Sign -> Sign -> Bool $c/= :: Sign -> Sign -> Bool == :: Sign -> Sign -> Bool $c== :: Sign -> Sign -> Bool Eq, Eq Sign Eq Sign => (Sign -> Sign -> Ordering) -> (Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> (Sign -> Sign -> Sign) -> (Sign -> Sign -> Sign) -> Ord Sign Sign -> Sign -> Bool Sign -> Sign -> Ordering Sign -> Sign -> Sign forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Sign -> Sign -> Sign $cmin :: Sign -> Sign -> Sign max :: Sign -> Sign -> Sign $cmax :: Sign -> Sign -> Sign >= :: Sign -> Sign -> Bool $c>= :: Sign -> Sign -> Bool > :: Sign -> Sign -> Bool $c> :: Sign -> Sign -> Bool <= :: Sign -> Sign -> Bool $c<= :: Sign -> Sign -> Bool < :: Sign -> Sign -> Bool $c< :: Sign -> Sign -> Bool compare :: Sign -> Sign -> Ordering $ccompare :: Sign -> Sign -> Ordering $cp1Ord :: Eq Sign Ord, Typeable Sign Constr DataType Typeable Sign => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign -> c Sign) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sign) -> (Sign -> Constr) -> (Sign -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sign)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)) -> ((forall b. Data b => b -> b) -> Sign -> Sign) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r) -> (forall u. (forall d. Data d => d -> u) -> Sign -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> Sign -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Sign -> m Sign) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign) -> Data Sign Sign -> Constr Sign -> DataType (forall b. Data b => b -> b) -> Sign -> Sign (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign -> c Sign (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sign forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> Sign -> u forall u. (forall d. Data d => d -> u) -> Sign -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Sign -> m Sign forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sign forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign -> c Sign forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sign) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign) $cSign :: Constr $tSign :: DataType gmapMo :: (forall d. Data d => d -> m d) -> Sign -> m Sign $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign gmapMp :: (forall d. Data d => d -> m d) -> Sign -> m Sign $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign gmapM :: (forall d. Data d => d -> m d) -> Sign -> m Sign $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Sign -> m Sign gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sign -> u gmapQ :: (forall d. Data d => d -> u) -> Sign -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sign -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r gmapT :: (forall b. Data b => b -> b) -> Sign -> Sign $cgmapT :: (forall b. Data b => b -> b) -> Sign -> Sign dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sign) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sign) dataTypeOf :: Sign -> DataType $cdataTypeOf :: Sign -> DataType toConstr :: Sign -> Constr $ctoConstr :: Sign -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sign $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign -> c Sign $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign -> c Sign $cp1Data :: Typeable Sign Data, Typeable) emptySign :: Sign emptySign :: Sign emptySign = Sign :: ConstantSet -> NumberSet -> ConstantSet -> THFSubTypeMap -> TFFSubTypeMap -> THFPredicateMap -> TFFPredicateMap -> FOFPredicateMap -> FOFPredicateMap -> THFPredicateMap -> TFFPredicateMap -> THFPredicateMap -> TFFPredicateMap -> THFPredicateMap -> TFFPredicateMap -> Sign Sign { constantSet :: ConstantSet constantSet = ConstantSet forall a. Set a Set.empty , numberSet :: NumberSet numberSet = NumberSet forall a. Set a Set.empty , propositionSet :: ConstantSet propositionSet = ConstantSet forall a. Set a Set.empty , thfSubtypeMap :: THFSubTypeMap thfSubtypeMap = THFSubTypeMap forall k a. Map k a Map.empty , tffSubtypeMap :: TFFSubTypeMap tffSubtypeMap = TFFSubTypeMap forall k a. Map k a Map.empty , thfPredicateMap :: THFPredicateMap thfPredicateMap = THFPredicateMap forall k a. Map k a Map.empty , tffPredicateMap :: TFFPredicateMap tffPredicateMap = TFFPredicateMap forall k a. Map k a Map.empty , fofPredicateMap :: FOFPredicateMap fofPredicateMap = FOFPredicateMap forall k a. Map k a Map.empty , fofFunctorMap :: FOFPredicateMap fofFunctorMap = FOFPredicateMap forall k a. Map k a Map.empty , thfTypeConstantMap :: THFPredicateMap thfTypeConstantMap = THFPredicateMap forall k a. Map k a Map.empty , tffTypeConstantMap :: TFFPredicateMap tffTypeConstantMap = TFFPredicateMap forall k a. Map k a Map.empty , thfTypeFunctorMap :: THFPredicateMap thfTypeFunctorMap = THFPredicateMap forall k a. Map k a Map.empty , tffTypeFunctorMap :: TFFPredicateMap tffTypeFunctorMap = TFFPredicateMap forall k a. Map k a Map.empty , thfTypeDeclarationMap :: THFPredicateMap thfTypeDeclarationMap = THFPredicateMap forall k a. Map k a Map.empty , tffTypeDeclarationMap :: TFFPredicateMap tffTypeDeclarationMap = TFFPredicateMap forall k a. Map k a Map.empty } negateSentence :: Sentence -> Maybe Sentence negateSentence :: Sentence -> Maybe Sentence negateSentence sen :: Sentence sen = case Sentence sen of AF_THF_Annotated (THF_annotated n :: Name n r :: Formula_role r f :: THF_formula f a :: Annotations a) -> case THF_formula -> Maybe THF_formula negate_thf THF_formula f of Nothing -> Maybe Sentence forall a. Maybe a Nothing Just f' :: THF_formula f' -> Sentence -> Maybe Sentence forall a. a -> Maybe a Just (Sentence -> Maybe Sentence) -> Sentence -> Maybe Sentence forall a b. (a -> b) -> a -> b $ THF_annotated -> Sentence AF_THF_Annotated (THF_annotated -> Sentence) -> THF_annotated -> Sentence forall a b. (a -> b) -> a -> b $ Name -> Formula_role -> THF_formula -> Annotations -> THF_annotated THF_annotated Name n Formula_role r THF_formula f' Annotations a AF_TFX_Annotated (TFX_annotated _ _ _ _) -> Maybe Sentence forall a. Maybe a Nothing -- Todo: Check if this is possible somehow AF_TFF_Annotated (TFF_annotated n :: Name n r :: Formula_role r f :: TFF_formula f a :: Annotations a) -> case TFF_formula -> Maybe TFF_formula negate_tff TFF_formula f of Nothing -> Maybe Sentence forall a. Maybe a Nothing Just f' :: TFF_formula f' -> Sentence -> Maybe Sentence forall a. a -> Maybe a Just (Sentence -> Maybe Sentence) -> Sentence -> Maybe Sentence forall a b. (a -> b) -> a -> b $ TFF_annotated -> Sentence AF_TFF_Annotated (TFF_annotated -> Sentence) -> TFF_annotated -> Sentence forall a b. (a -> b) -> a -> b $ Name -> Formula_role -> TFF_formula -> Annotations -> TFF_annotated TFF_annotated Name n Formula_role r TFF_formula f' Annotations a AF_TCF_Annotated (TCF_annotated _ _ _ _) -> Maybe Sentence forall a. Maybe a Nothing -- Todo: break out of TCF AF_FOF_Annotated (FOF_annotated n :: Name n r :: Formula_role r f :: FOF_formula f a :: Annotations a) -> case FOF_formula -> Maybe FOF_formula negate_fof FOF_formula f of Nothing -> Maybe Sentence forall a. Maybe a Nothing Just f' :: FOF_formula f' -> Sentence -> Maybe Sentence forall a. a -> Maybe a Just (Sentence -> Maybe Sentence) -> Sentence -> Maybe Sentence forall a b. (a -> b) -> a -> b $ FOF_annotated -> Sentence AF_FOF_Annotated (FOF_annotated -> Sentence) -> FOF_annotated -> Sentence forall a b. (a -> b) -> a -> b $ Name -> Formula_role -> FOF_formula -> Annotations -> FOF_annotated FOF_annotated Name n Formula_role r FOF_formula f' Annotations a AF_CNF_Annotated (CNF_annotated _ _ _ _) -> Maybe Sentence forall a. Maybe a Nothing -- Todo: break out of CNF AF_TPI_Annotated (TPI_annotated n :: Name n r :: Formula_role r f :: FOF_formula f a :: Annotations a) -> case FOF_formula -> Maybe FOF_formula negate_fof FOF_formula f of Nothing -> Maybe Sentence forall a. Maybe a Nothing Just f' :: FOF_formula f' -> Sentence -> Maybe Sentence forall a. a -> Maybe a Just (Sentence -> Maybe Sentence) -> Sentence -> Maybe Sentence forall a b. (a -> b) -> a -> b $ TPI_annotated -> Sentence AF_TPI_Annotated (TPI_annotated -> Sentence) -> TPI_annotated -> Sentence forall a b. (a -> b) -> a -> b $ Name -> Formula_role -> FOF_formula -> Annotations -> TPI_annotated TPI_annotated Name n Formula_role r FOF_formula f' Annotations a where negate_thf :: THF_formula -> Maybe THF_formula negate_thf :: THF_formula -> Maybe THF_formula negate_thf formula :: THF_formula formula = case THF_formula formula of THFF_logic lf :: THF_logic_formula lf -> THF_formula -> Maybe THF_formula forall a. a -> Maybe a Just (THF_formula -> Maybe THF_formula) -> THF_formula -> Maybe THF_formula forall a b. (a -> b) -> a -> b $ THF_logic_formula -> THF_formula THFF_logic (THF_logic_formula -> THF_formula) -> THF_logic_formula -> THF_formula forall a b. (a -> b) -> a -> b $ THF_unitary_formula -> THF_logic_formula THFLF_unitary (THF_unitary_formula -> THF_logic_formula) -> THF_unitary_formula -> THF_logic_formula forall a b. (a -> b) -> a -> b $ THF_unary_formula -> THF_unitary_formula THFUF_unary (THF_unary_formula -> THF_unitary_formula) -> THF_unary_formula -> THF_unitary_formula forall a b. (a -> b) -> a -> b $ THF_unary_connective -> THF_logic_formula -> THF_unary_formula THF_unary_formula (Unary_connective -> THF_unary_connective THFUC_unary Unary_connective NOT) THF_logic_formula lf _ -> Maybe THF_formula forall a. Maybe a Nothing negate_tff :: TFF_formula -> Maybe TFF_formula negate_tff :: TFF_formula -> Maybe TFF_formula negate_tff formula :: TFF_formula formula = case TFF_formula formula of TFFF_logic lf :: TFF_logic_formula lf -> TFF_formula -> Maybe TFF_formula forall a. a -> Maybe a Just (TFF_formula -> Maybe TFF_formula) -> TFF_formula -> Maybe TFF_formula forall a b. (a -> b) -> a -> b $ TFF_logic_formula -> TFF_formula TFFF_logic (TFF_logic_formula -> TFF_formula) -> TFF_logic_formula -> TFF_formula forall a b. (a -> b) -> a -> b $ TFF_unitary_formula -> TFF_logic_formula TFFLF_unitary (TFF_unitary_formula -> TFF_logic_formula) -> TFF_unitary_formula -> TFF_logic_formula forall a b. (a -> b) -> a -> b $ TFF_unary_formula -> TFF_unitary_formula TFFUF_unary (TFF_unary_formula -> TFF_unitary_formula) -> TFF_unary_formula -> TFF_unitary_formula forall a b. (a -> b) -> a -> b $ Unary_connective -> TFF_unitary_formula -> TFF_unary_formula TFFUF_connective Unary_connective NOT (TFF_unitary_formula -> TFF_unary_formula) -> TFF_unitary_formula -> TFF_unary_formula forall a b. (a -> b) -> a -> b $ TFF_logic_formula -> TFF_unitary_formula TFFUF_logic TFF_logic_formula lf _ -> Maybe TFF_formula forall a. Maybe a Nothing negate_fof :: FOF_formula -> Maybe FOF_formula negate_fof :: FOF_formula -> Maybe FOF_formula negate_fof formula :: FOF_formula formula = case FOF_formula formula of FOFF_logic lf :: FOF_logic_formula lf -> FOF_formula -> Maybe FOF_formula forall a. a -> Maybe a Just (FOF_formula -> Maybe FOF_formula) -> FOF_formula -> Maybe FOF_formula forall a b. (a -> b) -> a -> b $ FOF_logic_formula -> FOF_formula FOFF_logic (FOF_logic_formula -> FOF_formula) -> FOF_logic_formula -> FOF_formula forall a b. (a -> b) -> a -> b $ FOF_unitary_formula -> FOF_logic_formula FOFLF_unitary (FOF_unitary_formula -> FOF_logic_formula) -> FOF_unitary_formula -> FOF_logic_formula forall a b. (a -> b) -> a -> b $ FOF_unary_formula -> FOF_unitary_formula FOFUF_unary (FOF_unary_formula -> FOF_unitary_formula) -> FOF_unary_formula -> FOF_unitary_formula forall a b. (a -> b) -> a -> b $ Unary_connective -> FOF_unitary_formula -> FOF_unary_formula FOFUF_connective Unary_connective NOT (FOF_unitary_formula -> FOF_unary_formula) -> FOF_unitary_formula -> FOF_unary_formula forall a b. (a -> b) -> a -> b $ FOF_logic_formula -> FOF_unitary_formula FOFUF_logic FOF_logic_formula lf _ -> Maybe FOF_formula forall a. Maybe a Nothing