{-# 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