Safe Haskell	None
Language	Haskell98

Codec.TPTP.Base

Contents

Basic undecorated formulae and terms
Formulae and terms decorated with state
General decorated formulae and terms
Formula Metadata
Gathering free Variables
Fixed-point style decorated formulae and terms
Utility functions

Synopsis

Basic undecorated formulae and terms

type Formula = F Identity Source #

Basic (undecorated) first-order formulae

type Term = T Identity Source #

Basic (undecorated) terms

Formulae and terms decorated with state

type FormulaST s = F (State s) Source #

First-order formulae decorated with state

type TermST s = T (State s) Source #

Terms decorated with state

type FormulaC = FormulaST [String] Source #

First-order formulae decorated with comments

type TermC = TermST [String] Source #

Terms decorated with comments

forgetFC :: FormulaC -> Formula Source #

Forget comments in formulae decorated with comments

forgetTC :: TermC -> Term Source #

Forget comments in terms decorated with comments

(.<=>.) :: Pointed c => F c -> F c -> F c infixl 2 Source #

Equivalence

Important special case:

\(\.\<\=\>\.\) :: Formula -> Formula -> Formula

(.=>.) :: Pointed c => F c -> F c -> F c infixl 2 Source #

Implication

(.<=.) :: Pointed c => F c -> F c -> F c infixl 2 Source #

Reverse implication

(.|.) :: Pointed c => F c -> F c -> F c infixl 3 Source #

Disjunction/OR

(.&.) :: Pointed c => F c -> F c -> F c infixl 4 Source #

Conjunction/AND

(.<~>.) :: Pointed c => F c -> F c -> F c infixl 2 Source #

XOR

(.~|.) :: Pointed c => F c -> F c -> F c infixl 3 Source #

NOR

(.~&.) :: Pointed c => F c -> F c -> F c infixl 4 Source #

NAND

(.~.) :: Pointed c => F c -> F c Source #

Negation

(.=.) :: Pointed c => T c -> T c -> F c infixl 5 Source #

Equality

(.!=.) :: Pointed c => T c -> T c -> F c infixl 5 Source #

Inequality

for_all :: Pointed c => [V] -> F c -> F c Source #

Universal quantification

exists :: Pointed c => [V] -> F c -> F c Source #

Existential quantification

pApp :: Pointed c => AtomicWord -> [T c] -> F c Source #

Predicate symbol application

var :: Pointed c => V -> T c Source #

Variable

fApp :: Pointed c => AtomicWord -> [T c] -> T c Source #

Function symbol application (constants are encoded as nullary functions)

numberLitTerm :: Pointed c => Rational -> T c Source #

Number literal

distinctObjectTerm :: Pointed c => String -> T c Source #

Double-quoted string literal, called Distinct Object in TPTP's grammar

General decorated formulae and terms

data Formula0 term formula Source #

See http://haskell.org/haskellwiki/Indirect_composite for the point of the type parameters (they allow for future decorations, e.g. monadic subformulae). If you don't need decorations, you can just use Formula and the wrapped constructors above.

Constructors

BinOp formula BinOp formula	Binary connective application
InfixPred term InfixPred term	Infix predicate application (equalities, inequalities)
PredApp AtomicWord [term]	Predicate application
Quant Quant [V] formula	Quantified formula
(:~:) formula	Negation

Instances

Pretty F0Diff #
Methods pretty :: F0Diff -> Doc # prettyList :: [F0Diff] -> Doc #
(Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty (WithEnclosing (Formula0 t f)) #
Methods pretty :: WithEnclosing (Formula0 t f) -> Doc # prettyList :: [WithEnclosing (Formula0 t f)] -> Doc #
Pretty (WithEnclosing F0Diff) #
Methods pretty :: WithEnclosing F0Diff -> Doc # prettyList :: [WithEnclosing F0Diff] -> Doc #
(Eq term, Eq formula) => Eq (Formula0 term formula) Source #
Methods (==) :: Formula0 term formula -> Formula0 term formula -> Bool # (/=) :: Formula0 term formula -> Formula0 term formula -> Bool #
(Data formula, Data term) => Data (Formula0 term formula) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Formula0 term formula -> c (Formula0 term formula) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Formula0 term formula) # toConstr :: Formula0 term formula -> Constr # dataTypeOf :: Formula0 term formula -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (Formula0 term formula)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Formula0 term formula)) # gmapT :: (forall b. Data b => b -> b) -> Formula0 term formula -> Formula0 term formula # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Formula0 term formula -> r # gmapQ :: (forall d. Data d => d -> u) -> Formula0 term formula -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Formula0 term formula -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Formula0 term formula -> m (Formula0 term formula) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula0 term formula -> m (Formula0 term formula) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula0 term formula -> m (Formula0 term formula) #
(Ord term, Ord formula) => Ord (Formula0 term formula) Source #
Methods compare :: Formula0 term formula -> Formula0 term formula -> Ordering # (<) :: Formula0 term formula -> Formula0 term formula -> Bool # (<=) :: Formula0 term formula -> Formula0 term formula -> Bool # (>) :: Formula0 term formula -> Formula0 term formula -> Bool # (>=) :: Formula0 term formula -> Formula0 term formula -> Bool # max :: Formula0 term formula -> Formula0 term formula -> Formula0 term formula # min :: Formula0 term formula -> Formula0 term formula -> Formula0 term formula #
(Read term, Read formula) => Read (Formula0 term formula) Source #
Methods readsPrec :: Int -> ReadS (Formula0 term formula) # readList :: ReadS [Formula0 term formula] # readPrec :: ReadPrec (Formula0 term formula) # readListPrec :: ReadPrec [Formula0 term formula] #
(Show term, Show formula) => Show (Formula0 term formula) Source #
Methods showsPrec :: Int -> Formula0 term formula -> ShowS # show :: Formula0 term formula -> String # showList :: [Formula0 term formula] -> ShowS #
(Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b) Source #
Methods arbitrary :: Gen (Formula0 a b) # shrink :: Formula0 a b -> [Formula0 a b] #
(ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f) Source #
Methods toTPTP :: Formula0 t f -> ShowS Source #

data Term0 term Source #

See http://haskell.org/haskellwiki/Indirect_composite for the point of the type parameters (they allow for future decorations). If you don't need decorations, you can just use Term and the wrapped constructors above.

Constructors

Var V	Variable
NumberLitTerm Rational	Number literal
DistinctObjectTerm String	Double-quoted item
FunApp AtomicWord [term]	Function symbol application (constants are encoded as nullary functions)

Instances

Pretty T0Diff #
Methods pretty :: T0Diff -> Doc # prettyList :: [T0Diff] -> Doc #
Eq term => Eq (Term0 term) Source #
Methods (==) :: Term0 term -> Term0 term -> Bool # (/=) :: Term0 term -> Term0 term -> Bool #
Data term => Data (Term0 term) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term0 term -> c (Term0 term) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Term0 term) # toConstr :: Term0 term -> Constr # dataTypeOf :: Term0 term -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (Term0 term)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Term0 term)) # gmapT :: (forall b. Data b => b -> b) -> Term0 term -> Term0 term # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term0 term -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term0 term -> r # gmapQ :: (forall d. Data d => d -> u) -> Term0 term -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Term0 term -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term) #
Ord term => Ord (Term0 term) Source #
Methods compare :: Term0 term -> Term0 term -> Ordering # (<) :: Term0 term -> Term0 term -> Bool # (<=) :: Term0 term -> Term0 term -> Bool # (>) :: Term0 term -> Term0 term -> Bool # (>=) :: Term0 term -> Term0 term -> Bool # max :: Term0 term -> Term0 term -> Term0 term # min :: Term0 term -> Term0 term -> Term0 term #
Read term => Read (Term0 term) Source #
Methods readsPrec :: Int -> ReadS (Term0 term) # readList :: ReadS [Term0 term] # readPrec :: ReadPrec (Term0 term) # readListPrec :: ReadPrec [Term0 term] #
Show term => Show (Term0 term) Source #
Methods showsPrec :: Int -> Term0 term -> ShowS # show :: Term0 term -> String # showList :: [Term0 term] -> ShowS #
Arbitrary a => Arbitrary (Term0 a) Source #
Methods arbitrary :: Gen (Term0 a) # shrink :: Term0 a -> [Term0 a] #
Pretty (WithEnclosing t) => Pretty (WithEnclosing (Term0 t)) #
Methods pretty :: WithEnclosing (Term0 t) -> Doc # prettyList :: [WithEnclosing (Term0 t)] -> Doc #
Pretty (WithEnclosing T0Diff) #
Methods pretty :: WithEnclosing T0Diff -> Doc # prettyList :: [WithEnclosing T0Diff] -> Doc #
ToTPTP t => ToTPTP (Term0 t) Source #
Methods toTPTP :: Term0 t -> ShowS Source #

data BinOp Source #

Binary formula connectives

Constructors

(:<=>:)	Equivalence
(:=>:)	Implication
(:<=:)	Reverse Implication
(:&:)	AND
(:\|:)	OR
(:~&:)	NAND
(:~\|:)	NOR
(:<~>:)	XOR

Instances

Bounded BinOp Source #
Methods minBound :: BinOp # maxBound :: BinOp #
Enum BinOp Source #
Methods succ :: BinOp -> BinOp # pred :: BinOp -> BinOp # toEnum :: Int -> BinOp # fromEnum :: BinOp -> Int # enumFrom :: BinOp -> [BinOp] # enumFromThen :: BinOp -> BinOp -> [BinOp] # enumFromTo :: BinOp -> BinOp -> [BinOp] # enumFromThenTo :: BinOp -> BinOp -> BinOp -> [BinOp] #
Eq BinOp Source #
Methods (==) :: BinOp -> BinOp -> Bool # (/=) :: BinOp -> BinOp -> Bool #
Data BinOp Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BinOp -> c BinOp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BinOp # toConstr :: BinOp -> Constr # dataTypeOf :: BinOp -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c BinOp) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp) # gmapT :: (forall b. Data b => b -> b) -> BinOp -> BinOp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r # gmapQ :: (forall d. Data d => d -> u) -> BinOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BinOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp #
Ord BinOp Source #
Methods compare :: BinOp -> BinOp -> Ordering # (<) :: BinOp -> BinOp -> Bool # (<=) :: BinOp -> BinOp -> Bool # (>) :: BinOp -> BinOp -> Bool # (>=) :: BinOp -> BinOp -> Bool # max :: BinOp -> BinOp -> BinOp # min :: BinOp -> BinOp -> BinOp #
Read BinOp Source #
Methods readsPrec :: Int -> ReadS BinOp # readList :: ReadS [BinOp] # readPrec :: ReadPrec BinOp # readListPrec :: ReadPrec [BinOp] #
Show BinOp Source #
Methods showsPrec :: Int -> BinOp -> ShowS # show :: BinOp -> String # showList :: [BinOp] -> ShowS #
Arbitrary BinOp Source #
Methods arbitrary :: Gen BinOp # shrink :: BinOp -> [BinOp] #
ToTPTP BinOp Source #
Methods toTPTP :: BinOp -> ShowS Source #

data InfixPred Source #

Term -> Term -> Formula infix connectives

Constructors

(:=:)
(:!=:)

Instances

Bounded InfixPred Source #
Methods minBound :: InfixPred # maxBound :: InfixPred #
Enum InfixPred Source #
Methods succ :: InfixPred -> InfixPred # pred :: InfixPred -> InfixPred # toEnum :: Int -> InfixPred # fromEnum :: InfixPred -> Int # enumFrom :: InfixPred -> [InfixPred] # enumFromThen :: InfixPred -> InfixPred -> [InfixPred] # enumFromTo :: InfixPred -> InfixPred -> [InfixPred] # enumFromThenTo :: InfixPred -> InfixPred -> InfixPred -> [InfixPred] #
Eq InfixPred Source #
Methods (==) :: InfixPred -> InfixPred -> Bool # (/=) :: InfixPred -> InfixPred -> Bool #
Data InfixPred Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InfixPred -> c InfixPred # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InfixPred # toConstr :: InfixPred -> Constr # dataTypeOf :: InfixPred -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c InfixPred) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfixPred) # gmapT :: (forall b. Data b => b -> b) -> InfixPred -> InfixPred # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InfixPred -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InfixPred -> r # gmapQ :: (forall d. Data d => d -> u) -> InfixPred -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> InfixPred -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred #
Ord InfixPred Source #
Methods compare :: InfixPred -> InfixPred -> Ordering # (<) :: InfixPred -> InfixPred -> Bool # (<=) :: InfixPred -> InfixPred -> Bool # (>) :: InfixPred -> InfixPred -> Bool # (>=) :: InfixPred -> InfixPred -> Bool # max :: InfixPred -> InfixPred -> InfixPred # min :: InfixPred -> InfixPred -> InfixPred #
Read InfixPred Source #
Methods readsPrec :: Int -> ReadS InfixPred # readList :: ReadS [InfixPred] # readPrec :: ReadPrec InfixPred # readListPrec :: ReadPrec [InfixPred] #
Show InfixPred Source #
Methods showsPrec :: Int -> InfixPred -> ShowS # show :: InfixPred -> String # showList :: [InfixPred] -> ShowS #
Arbitrary InfixPred Source #
Methods arbitrary :: Gen InfixPred # shrink :: InfixPred -> [InfixPred] #
ToTPTP InfixPred Source #
Methods toTPTP :: InfixPred -> ShowS Source #

data Quant Source #

Quantifier specification

Constructors

All
Exists

Instances

Bounded Quant Source #
Methods minBound :: Quant # maxBound :: Quant #
Enum Quant Source #
Methods succ :: Quant -> Quant # pred :: Quant -> Quant # toEnum :: Int -> Quant # fromEnum :: Quant -> Int # enumFrom :: Quant -> [Quant] # enumFromThen :: Quant -> Quant -> [Quant] # enumFromTo :: Quant -> Quant -> [Quant] # enumFromThenTo :: Quant -> Quant -> Quant -> [Quant] #
Eq Quant Source #
Methods (==) :: Quant -> Quant -> Bool # (/=) :: Quant -> Quant -> Bool #
Data Quant Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quant -> c Quant # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quant # toConstr :: Quant -> Constr # dataTypeOf :: Quant -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Quant) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant) # gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r # gmapQ :: (forall d. Data d => d -> u) -> Quant -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Quant -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quant -> m Quant # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant #
Ord Quant Source #
Methods compare :: Quant -> Quant -> Ordering # (<) :: Quant -> Quant -> Bool # (<=) :: Quant -> Quant -> Bool # (>) :: Quant -> Quant -> Bool # (>=) :: Quant -> Quant -> Bool # max :: Quant -> Quant -> Quant # min :: Quant -> Quant -> Quant #
Read Quant Source #
Methods readsPrec :: Int -> ReadS Quant # readList :: ReadS [Quant] # readPrec :: ReadPrec Quant # readListPrec :: ReadPrec [Quant] #
Show Quant Source #
Methods showsPrec :: Int -> Quant -> ShowS # show :: Quant -> String # showList :: [Quant] -> ShowS #
Arbitrary Quant Source #
Methods arbitrary :: Gen Quant # shrink :: Quant -> [Quant] #
ToTPTP Quant Source #
Methods toTPTP :: Quant -> ShowS Source #

Formula Metadata

type TPTP_Input = TPTP_Input_ Identity Source #

A line of a TPTP file: Annotated formula, comment or include statement.

type TPTP_Input_C = TPTP_Input_ (State [String]) Source #

A line of a TPTP file: Annotated formula (with the comment string embbeded in the State monad ), comment or include statement

forgetTIC :: TPTP_Input_C -> TPTP_Input Source #

Forget comments in a line of a TPTP file decorated with comments

data TPTP_Input_ c Source #

Generalized TPTP_Input

Constructors

AFormula	Annotated formulae
Fields name :: AtomicWord role :: Role formula :: F c annotations :: Annotations
Comment String
Include FilePath [AtomicWord]

Instances

Arbitrary TPTP_Input Source #
Methods arbitrary :: Gen TPTP_Input # shrink :: TPTP_Input -> [TPTP_Input] #
ToTPTP TPTP_Input Source #
Methods toTPTP :: TPTP_Input -> ShowS Source #
Eq (c (Formula0 (T c) (F c))) => Eq (TPTP_Input_ c) Source #
Methods (==) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool # (/=) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool #
(Typeable (* -> *) c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TPTP_Input_ c -> c (TPTP_Input_ c) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TPTP_Input_ c) # toConstr :: TPTP_Input_ c -> Constr # dataTypeOf :: TPTP_Input_ c -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (TPTP_Input_ c)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TPTP_Input_ c)) # gmapT :: (forall b. Data b => b -> b) -> TPTP_Input_ c -> TPTP_Input_ c # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPTP_Input_ c -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPTP_Input_ c -> r # gmapQ :: (forall d. Data d => d -> u) -> TPTP_Input_ c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TPTP_Input_ c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TPTP_Input_ c -> m (TPTP_Input_ c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP_Input_ c -> m (TPTP_Input_ c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP_Input_ c -> m (TPTP_Input_ c) #
Ord (c (Formula0 (T c) (F c))) => Ord (TPTP_Input_ c) Source #
Methods compare :: TPTP_Input_ c -> TPTP_Input_ c -> Ordering # (<) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool # (<=) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool # (>) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool # (>=) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool # max :: TPTP_Input_ c -> TPTP_Input_ c -> TPTP_Input_ c # min :: TPTP_Input_ c -> TPTP_Input_ c -> TPTP_Input_ c #
Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c) Source #
Methods readsPrec :: Int -> ReadS (TPTP_Input_ c) # readList :: ReadS [TPTP_Input_ c] # readPrec :: ReadPrec (TPTP_Input_ c) # readListPrec :: ReadPrec [TPTP_Input_ c] #
Show (c (Formula0 (T c) (F c))) => Show (TPTP_Input_ c) Source #
Methods showsPrec :: Int -> TPTP_Input_ c -> ShowS # show :: TPTP_Input_ c -> String # showList :: [TPTP_Input_ c] -> ShowS #
ToTPTP [TPTP_Input] Source #
Methods toTPTP :: [TPTP_Input] -> ShowS Source #

data Annotations Source #

Annotations about the formulas origin

Constructors

NoAnnotations
Annotations GTerm UsefulInfo

Instances

Eq Annotations Source #
Methods (==) :: Annotations -> Annotations -> Bool # (/=) :: Annotations -> Annotations -> Bool #
Data Annotations Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annotations -> c Annotations # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Annotations # toConstr :: Annotations -> Constr # dataTypeOf :: Annotations -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Annotations) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annotations) # gmapT :: (forall b. Data b => b -> b) -> Annotations -> Annotations # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annotations -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annotations -> r # gmapQ :: (forall d. Data d => d -> u) -> Annotations -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Annotations -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations #
Ord Annotations Source #
Methods compare :: Annotations -> Annotations -> Ordering # (<) :: Annotations -> Annotations -> Bool # (<=) :: Annotations -> Annotations -> Bool # (>) :: Annotations -> Annotations -> Bool # (>=) :: Annotations -> Annotations -> Bool # max :: Annotations -> Annotations -> Annotations # min :: Annotations -> Annotations -> Annotations #
Read Annotations Source #
Methods readsPrec :: Int -> ReadS Annotations # readList :: ReadS [Annotations] # readPrec :: ReadPrec Annotations # readListPrec :: ReadPrec [Annotations] #
Show Annotations Source #
Methods showsPrec :: Int -> Annotations -> ShowS # show :: Annotations -> String # showList :: [Annotations] -> ShowS #
Arbitrary Annotations Source #
Methods arbitrary :: Gen Annotations # shrink :: Annotations -> [Annotations] #
ToTPTP Annotations Source #
Methods toTPTP :: Annotations -> ShowS Source #

data UsefulInfo Source #

Misc annotations

Constructors

NoUsefulInfo
UsefulInfo [GTerm]

Instances

Eq UsefulInfo Source #
Methods (==) :: UsefulInfo -> UsefulInfo -> Bool # (/=) :: UsefulInfo -> UsefulInfo -> Bool #
Data UsefulInfo Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UsefulInfo -> c UsefulInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UsefulInfo # toConstr :: UsefulInfo -> Constr # dataTypeOf :: UsefulInfo -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c UsefulInfo) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UsefulInfo) # gmapT :: (forall b. Data b => b -> b) -> UsefulInfo -> UsefulInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> UsefulInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UsefulInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo #
Ord UsefulInfo Source #
Methods compare :: UsefulInfo -> UsefulInfo -> Ordering # (<) :: UsefulInfo -> UsefulInfo -> Bool # (<=) :: UsefulInfo -> UsefulInfo -> Bool # (>) :: UsefulInfo -> UsefulInfo -> Bool # (>=) :: UsefulInfo -> UsefulInfo -> Bool # max :: UsefulInfo -> UsefulInfo -> UsefulInfo # min :: UsefulInfo -> UsefulInfo -> UsefulInfo #
Read UsefulInfo Source #
Methods readsPrec :: Int -> ReadS UsefulInfo # readList :: ReadS [UsefulInfo] # readPrec :: ReadPrec UsefulInfo # readListPrec :: ReadPrec [UsefulInfo] #
Show UsefulInfo Source #
Methods showsPrec :: Int -> UsefulInfo -> ShowS # show :: UsefulInfo -> String # showList :: [UsefulInfo] -> ShowS #
Arbitrary UsefulInfo Source #
Methods arbitrary :: Gen UsefulInfo # shrink :: UsefulInfo -> [UsefulInfo] #
ToTPTP UsefulInfo Source #
Methods toTPTP :: UsefulInfo -> ShowS Source #

newtype Role Source #

Formula roles

Constructors

Role
Fields unrole :: String

Instances

Eq Role Source #
Methods (==) :: Role -> Role -> Bool # (/=) :: Role -> Role -> Bool #
Data Role Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role # toConstr :: Role -> Constr # dataTypeOf :: Role -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Role) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role) # gmapT :: (forall b. Data b => b -> b) -> Role -> Role # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r # gmapQ :: (forall d. Data d => d -> u) -> Role -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role #
Ord Role Source #
Methods compare :: Role -> Role -> Ordering # (<) :: Role -> Role -> Bool # (<=) :: Role -> Role -> Bool # (>) :: Role -> Role -> Bool # (>=) :: Role -> Role -> Bool # max :: Role -> Role -> Role # min :: Role -> Role -> Role #
Read Role Source #
Methods readsPrec :: Int -> ReadS Role # readList :: ReadS [Role] # readPrec :: ReadPrec Role # readListPrec :: ReadPrec [Role] #
Show Role Source #
Methods showsPrec :: Int -> Role -> ShowS # show :: Role -> String # showList :: [Role] -> ShowS #
Arbitrary Role Source #
Methods arbitrary :: Gen Role # shrink :: Role -> [Role] #
ToTPTP Role Source #
Methods toTPTP :: Role -> ShowS Source #

data GData Source #

Metadata (the general_data rule in TPTP's grammar)

Constructors

GWord AtomicWord
GApp AtomicWord [GTerm]
GVar V
GNumber Rational
GDistinctObject String
GFormulaData String Formula

Instances

Eq GData Source #
Methods (==) :: GData -> GData -> Bool # (/=) :: GData -> GData -> Bool #
Data GData Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GData -> c GData # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GData # toConstr :: GData -> Constr # dataTypeOf :: GData -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c GData) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GData) # gmapT :: (forall b. Data b => b -> b) -> GData -> GData # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r # gmapQ :: (forall d. Data d => d -> u) -> GData -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> GData -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> GData -> m GData # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GData -> m GData # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GData -> m GData #
Ord GData Source #
Methods compare :: GData -> GData -> Ordering # (<) :: GData -> GData -> Bool # (<=) :: GData -> GData -> Bool # (>) :: GData -> GData -> Bool # (>=) :: GData -> GData -> Bool # max :: GData -> GData -> GData # min :: GData -> GData -> GData #
Read GData Source #
Methods readsPrec :: Int -> ReadS GData # readList :: ReadS [GData] # readPrec :: ReadPrec GData # readListPrec :: ReadPrec [GData] #
Show GData Source #
Methods showsPrec :: Int -> GData -> ShowS # show :: GData -> String # showList :: [GData] -> ShowS #
Arbitrary GData Source #
Methods arbitrary :: Gen GData # shrink :: GData -> [GData] #
ToTPTP GData Source #
Methods toTPTP :: GData -> ShowS Source #

data GTerm Source #

Metadata (the general_term rule in TPTP's grammar)

Constructors

ColonSep GData GTerm
GTerm GData
GList [GTerm]

Instances

Eq GTerm Source #
Methods (==) :: GTerm -> GTerm -> Bool # (/=) :: GTerm -> GTerm -> Bool #
Data GTerm Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GTerm -> c GTerm # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GTerm # toConstr :: GTerm -> Constr # dataTypeOf :: GTerm -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c GTerm) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GTerm) # gmapT :: (forall b. Data b => b -> b) -> GTerm -> GTerm # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r # gmapQ :: (forall d. Data d => d -> u) -> GTerm -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> GTerm -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> GTerm -> m GTerm # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GTerm -> m GTerm # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GTerm -> m GTerm #
Ord GTerm Source #
Methods compare :: GTerm -> GTerm -> Ordering # (<) :: GTerm -> GTerm -> Bool # (<=) :: GTerm -> GTerm -> Bool # (>) :: GTerm -> GTerm -> Bool # (>=) :: GTerm -> GTerm -> Bool # max :: GTerm -> GTerm -> GTerm # min :: GTerm -> GTerm -> GTerm #
Read GTerm Source #
Methods readsPrec :: Int -> ReadS GTerm # readList :: ReadS [GTerm] # readPrec :: ReadPrec GTerm # readListPrec :: ReadPrec [GTerm] #
Show GTerm Source #
Methods showsPrec :: Int -> GTerm -> ShowS # show :: GTerm -> String # showList :: [GTerm] -> ShowS #
Arbitrary GTerm Source #
Methods arbitrary :: Gen GTerm # shrink :: GTerm -> [GTerm] #
ToTPTP GTerm Source #
Methods toTPTP :: GTerm -> ShowS Source #

Gathering free Variables

class FreeVars a where Source #

Minimal complete definition

freeVars

Methods

freeVars :: a -> Set V Source #

Obtain the free variables from a formula or term

Instances

FreeVars Term Source #
Methods freeVars :: Term -> Set V Source #
FreeVars Formula Source #
Methods freeVars :: Formula -> Set V Source #

univquant_free_vars :: Formula -> Formula Source #

Universally quantify all free variables in the formula

newtype AtomicWord Source #

TPTP constant symbol/predicate symbol/function symbol identifiers (they are output in single quotes unless they are lower_words).

Tip: Use the -XOverloadedStrings compiler flag if you don't want to have to type AtomicWord to construct an AtomicWord

Constructors

AtomicWord String

Instances

Eq AtomicWord Source #
Methods (==) :: AtomicWord -> AtomicWord -> Bool # (/=) :: AtomicWord -> AtomicWord -> Bool #
Data AtomicWord Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AtomicWord -> c AtomicWord # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AtomicWord # toConstr :: AtomicWord -> Constr # dataTypeOf :: AtomicWord -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c AtomicWord) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AtomicWord) # gmapT :: (forall b. Data b => b -> b) -> AtomicWord -> AtomicWord # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AtomicWord -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AtomicWord -> r # gmapQ :: (forall d. Data d => d -> u) -> AtomicWord -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AtomicWord -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord #
Ord AtomicWord Source #
Methods compare :: AtomicWord -> AtomicWord -> Ordering # (<) :: AtomicWord -> AtomicWord -> Bool # (<=) :: AtomicWord -> AtomicWord -> Bool # (>) :: AtomicWord -> AtomicWord -> Bool # (>=) :: AtomicWord -> AtomicWord -> Bool # max :: AtomicWord -> AtomicWord -> AtomicWord # min :: AtomicWord -> AtomicWord -> AtomicWord #
Read AtomicWord Source #
Methods readsPrec :: Int -> ReadS AtomicWord # readList :: ReadS [AtomicWord] # readPrec :: ReadPrec AtomicWord # readListPrec :: ReadPrec [AtomicWord] #
Show AtomicWord Source #
Methods showsPrec :: Int -> AtomicWord -> ShowS # show :: AtomicWord -> String # showList :: [AtomicWord] -> ShowS #
IsString AtomicWord Source #
Methods fromString :: String -> AtomicWord #
Monoid AtomicWord Source #
Methods mempty :: AtomicWord # mappend :: AtomicWord -> AtomicWord -> AtomicWord # mconcat :: [AtomicWord] -> AtomicWord #
Arbitrary AtomicWord Source #
Methods arbitrary :: Gen AtomicWord # shrink :: AtomicWord -> [AtomicWord] #
ToTPTP AtomicWord Source #
Methods toTPTP :: AtomicWord -> ShowS Source #

newtype V Source #

Variable names

Constructors

V String

Instances

Eq V Source #
Methods (==) :: V -> V -> Bool # (/=) :: V -> V -> Bool #
Data V Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> V -> c V # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c V # toConstr :: V -> Constr # dataTypeOf :: V -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c V) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V) # gmapT :: (forall b. Data b => b -> b) -> V -> V # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r # gmapQ :: (forall d. Data d => d -> u) -> V -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> V -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> V -> m V # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> V -> m V # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> V -> m V #
Ord V Source #
Methods compare :: V -> V -> Ordering # (<) :: V -> V -> Bool # (<=) :: V -> V -> Bool # (>) :: V -> V -> Bool # (>=) :: V -> V -> Bool # max :: V -> V -> V # min :: V -> V -> V #
Read V Source #
Methods readsPrec :: Int -> ReadS V # readList :: ReadS [V] # readPrec :: ReadPrec V # readListPrec :: ReadPrec [V] #
Show V Source #
Methods showsPrec :: Int -> V -> ShowS # show :: V -> String # showList :: [V] -> ShowS #
IsString V Source #
Methods fromString :: String -> V #
Monoid V Source #
Methods mempty :: V # mappend :: V -> V -> V # mconcat :: [V] -> V #
Arbitrary V Source #
Methods arbitrary :: Gen V # shrink :: V -> [V] #
ToTPTP V Source #
Methods toTPTP :: V -> ShowS Source #

Fixed-point style decorated formulae and terms

newtype F c Source #

Formulae whose subexpressions are wrapped in the given type constructor c.

For example:

c = Identity: Plain formulae
c = Maybe: Formulae that may contain "holes"
c = IORef: (Mutable) formulae with mutable subexpressions

Constructors

F
Fields runF :: c (Formula0 (T c) (F c))

Instances

Arbitrary Formula Source #
Methods arbitrary :: Gen Formula # shrink :: Formula -> [Formula] #
Pretty F0Diff #
Methods pretty :: F0Diff -> Doc # prettyList :: [F0Diff] -> Doc #
FreeVars Formula Source #
Methods freeVars :: Formula -> Set V Source #
Diffable Formula (F DiffResult) Source #
Methods diff :: Formula -> Formula -> F DiffResult Source #
Eq (c (Formula0 (T c) (F c))) => Eq (F c) Source #
Methods (==) :: F c -> F c -> Bool # (/=) :: F c -> F c -> Bool #
(Typeable (* -> *) c, Data (c (Formula0 (T c) (F c)))) => Data (F c) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> F c -> c (F c) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (F c) # toConstr :: F c -> Constr # dataTypeOf :: F c -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (F c)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (F c)) # gmapT :: (forall b. Data b => b -> b) -> F c -> F c # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> F c -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> F c -> r # gmapQ :: (forall d. Data d => d -> u) -> F c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> F c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> F c -> m (F c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> F c -> m (F c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> F c -> m (F c) #
Ord (c (Formula0 (T c) (F c))) => Ord (F c) Source #
Methods compare :: F c -> F c -> Ordering # (<) :: F c -> F c -> Bool # (<=) :: F c -> F c -> Bool # (>) :: F c -> F c -> Bool # (>=) :: F c -> F c -> Bool # max :: F c -> F c -> F c # min :: F c -> F c -> F c #
Read (c (Formula0 (T c) (F c))) => Read (F c) Source #
Methods readsPrec :: Int -> ReadS (F c) # readList :: ReadS [F c] # readPrec :: ReadPrec (F c) # readListPrec :: ReadPrec [F c] #
Show (c (Formula0 (T c) (F c))) => Show (F c) Source #
Methods showsPrec :: Int -> F c -> ShowS # show :: F c -> String # showList :: [F c] -> ShowS #
Show (F DiffResult) #
Methods showsPrec :: Int -> F DiffResult -> ShowS # show :: F DiffResult -> String # showList :: [F DiffResult] -> ShowS #
Pretty (F DiffResult) #
Methods pretty :: F DiffResult -> Doc # prettyList :: [F DiffResult] -> Doc #
Pretty (WithEnclosing (F DiffResult)) #
Methods pretty :: WithEnclosing (F DiffResult) -> Doc # prettyList :: [WithEnclosing (F DiffResult)] -> Doc #
Pretty (WithEnclosing Formula) #
Methods pretty :: WithEnclosing Formula -> Doc # prettyList :: [WithEnclosing Formula] -> Doc #
Pretty (WithEnclosing F0Diff) #
Methods pretty :: WithEnclosing F0Diff -> Doc # prettyList :: [WithEnclosing F0Diff] -> Doc #
ToTPTP (F Identity) Source #
Methods toTPTP :: F Identity -> ShowS Source #

newtype T c Source #

Terms whose subterms are wrapped in the given type constructor c

Constructors

T
Fields runT :: c (Term0 (T c))

Instances

Arbitrary Term Source #
Methods arbitrary :: Gen Term # shrink :: Term -> [Term] #
Pretty F0Diff #
Methods pretty :: F0Diff -> Doc # prettyList :: [F0Diff] -> Doc #
Pretty T0Diff #
Methods pretty :: T0Diff -> Doc # prettyList :: [T0Diff] -> Doc #
FreeVars Term Source #
Methods freeVars :: Term -> Set V Source #
Diffable Term (T DiffResult) Source #
Methods diff :: Term -> Term -> T DiffResult Source #
Eq (c (Term0 (T c))) => Eq (T c) Source #
Methods (==) :: T c -> T c -> Bool # (/=) :: T c -> T c -> Bool #
(Typeable (* -> *) c, Data (c (Term0 (T c)))) => Data (T c) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> T c -> c (T c) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (T c) # toConstr :: T c -> Constr # dataTypeOf :: T c -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (T c)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (T c)) # gmapT :: (forall b. Data b => b -> b) -> T c -> T c # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> T c -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T c -> r # gmapQ :: (forall d. Data d => d -> u) -> T c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> T c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> T c -> m (T c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> T c -> m (T c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> T c -> m (T c) #
Ord (c (Term0 (T c))) => Ord (T c) Source #
Methods compare :: T c -> T c -> Ordering # (<) :: T c -> T c -> Bool # (<=) :: T c -> T c -> Bool # (>) :: T c -> T c -> Bool # (>=) :: T c -> T c -> Bool # max :: T c -> T c -> T c # min :: T c -> T c -> T c #
Read (c (Term0 (T c))) => Read (T c) Source #
Methods readsPrec :: Int -> ReadS (T c) # readList :: ReadS [T c] # readPrec :: ReadPrec (T c) # readListPrec :: ReadPrec [T c] #
Show (c (Term0 (T c))) => Show (T c) Source #
Methods showsPrec :: Int -> T c -> ShowS # show :: T c -> String # showList :: [T c] -> ShowS #
Show (T DiffResult) #
Methods showsPrec :: Int -> T DiffResult -> ShowS # show :: T DiffResult -> String # showList :: [T DiffResult] -> ShowS #
Pretty (T DiffResult) #
Methods pretty :: T DiffResult -> Doc # prettyList :: [T DiffResult] -> Doc #
Pretty (WithEnclosing (T DiffResult)) #
Methods pretty :: WithEnclosing (T DiffResult) -> Doc # prettyList :: [WithEnclosing (T DiffResult)] -> Doc #
Pretty (WithEnclosing Term) #
Methods pretty :: WithEnclosing Term -> Doc # prettyList :: [WithEnclosing Term] -> Doc #
Pretty (WithEnclosing F0Diff) #
Methods pretty :: WithEnclosing F0Diff -> Doc # prettyList :: [WithEnclosing F0Diff] -> Doc #
Pretty (WithEnclosing T0Diff) #
Methods pretty :: WithEnclosing T0Diff -> Doc # prettyList :: [WithEnclosing T0Diff] -> Doc #
ToTPTP (T Identity) Source #
Methods toTPTP :: T Identity -> ShowS Source #

Utility functions

unwrapF :: Copointed t => F t -> Formula0 (T t) (F t) Source #

unwrapT :: Copointed t => T t -> Term0 (T t) Source #

foldFormula0 :: (f -> r) -> (Quant -> [V] -> f -> r) -> (f -> BinOp -> f -> r) -> (t -> InfixPred -> t -> r) -> (AtomicWord -> [t] -> r) -> Formula0 t f -> r Source #

foldTerm0 :: (String -> r) -> (Rational -> r) -> (V -> r) -> (AtomicWord -> [t] -> r) -> Term0 t -> r Source #

foldF Source #

Arguments

:: Copointed t
=> (F t -> r)	Handle negation
-> (Quant -> [V] -> F t -> r)	Handle quantification
-> (F t -> BinOp -> F t -> r)	Handle binary op
-> (T t -> InfixPred -> T t -> r)	Handle equality/inequality
-> (AtomicWord -> [T t] -> r)	Handle predicate symbol application
-> F t -> r	Handle formula

Eliminate formulae

foldT Source #

Arguments

:: Copointed t
=> (String -> r)	Handle string literal
-> (Rational -> r)	Handle number literal
-> (V -> r)	Handle variable
-> (AtomicWord -> [T t] -> r)	Handle function symbol application
-> T t -> r	Handle term

Eliminate terms