Codec.TPTP.Base

Basic undecorated formulae and terms

type Formula = F Identity

Basic (undecorated) first-order formulae

type Term = T Identity

Basic (undecorated) terms

Formulae and terms decorated with state

type FormulaST s = F (State s)

First-order formulae decorated with state

type TermST s = T (State s)

Terms decorated with state

type FormulaC = FormulaST [String]

First-order formulae decorated with comments

type TermC = TermST [String]

Terms decorated with comments

forgetFC :: FormulaC -> Formula

Forget comments in formulae decorated with comments

forgetTC :: TermC -> Term

Forget comments in terms decorated with comments

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

Equivalence

Important special case:

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

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

Implication

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

Reverse implication

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

Disjunction/OR

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

Conjunction/AND

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

XOR

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

NOR

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

NAND

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

Negation

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

Equality

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

Inequality

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

Universal quantification

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

Existential quantification

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

Predicate symbol application

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

Variable

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

Function symbol application (constants are encoded as nullary functions)

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

Number literal

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

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

General decorated formulae and terms

data Formula0 term formula

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

Defined in Codec.TPTP.Diff

Methods

pretty :: F0Diff -> Doc

prettyList :: [F0Diff] -> Doc

(Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty (WithEnclosing (Formula0 t f))

Defined in Codec.TPTP.Pretty

Methods

pretty :: WithEnclosing (Formula0 t f) -> Doc

prettyList :: [WithEnclosing (Formula0 t f)] -> Doc

Pretty (WithEnclosing F0Diff)

Defined in Codec.TPTP.Diff

Methods

pretty :: WithEnclosing F0Diff -> Doc

prettyList :: [WithEnclosing F0Diff] -> Doc

(Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b)

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen (Formula0 a b)

shrink :: Formula0 a b -> [Formula0 a b]

Pretty (Formula0 Term Formula)

Defined in Codec.TPTP.Pretty

Methods

pretty :: Formula0 Term Formula -> Doc

prettyList :: [Formula0 Term Formula] -> Doc

(Data term, Data formula) => Data (Formula0 term formula)

Defined in Codec.TPTP.Base

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 :: forall r r'. (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)

(Read term, Read formula) => Read (Formula0 term formula)

Defined in Codec.TPTP.Base

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)

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> Formula0 term formula -> ShowS

show :: Formula0 term formula -> String

showList :: [Formula0 term formula] -> ShowS

(Eq term, Eq formula) => Eq (Formula0 term formula)

Defined in Codec.TPTP.Base

Methods

(==) :: Formula0 term formula -> Formula0 term formula -> Bool

(/=) :: Formula0 term formula -> Formula0 term formula -> Bool

(Ord term, Ord formula) => Ord (Formula0 term formula)

Defined in Codec.TPTP.Base

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

(ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f)

Defined in Codec.TPTP.Export

Methods

toTPTP :: Formula0 t f -> ShowS

data Term0 term

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

Defined in Codec.TPTP.Diff

Methods

pretty :: T0Diff -> Doc

prettyList :: [T0Diff] -> Doc

Arbitrary a => Arbitrary (Term0 a)

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen (Term0 a)

shrink :: Term0 a -> [Term0 a]

Pretty (Term0 Term)

Defined in Codec.TPTP.Pretty

Methods

pretty :: Term0 Term -> Doc

prettyList :: [Term0 Term] -> Doc

Pretty (WithEnclosing t) => Pretty (WithEnclosing (Term0 t))

Defined in Codec.TPTP.Pretty

Methods

pretty :: WithEnclosing (Term0 t) -> Doc

prettyList :: [WithEnclosing (Term0 t)] -> Doc

Pretty (WithEnclosing T0Diff)

Defined in Codec.TPTP.Diff

Methods

pretty :: WithEnclosing T0Diff -> Doc

prettyList :: [WithEnclosing T0Diff] -> Doc

Data term => Data (Term0 term)

Defined in Codec.TPTP.Base

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 :: forall r r'. (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)

Read term => Read (Term0 term)

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS (Term0 term)

readList :: ReadS [Term0 term]

readPrec :: ReadPrec (Term0 term)

readListPrec :: ReadPrec [Term0 term]

Show term => Show (Term0 term)

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> Term0 term -> ShowS

show :: Term0 term -> String

showList :: [Term0 term] -> ShowS

Eq term => Eq (Term0 term)

Defined in Codec.TPTP.Base

Methods

(==) :: Term0 term -> Term0 term -> Bool

(/=) :: Term0 term -> Term0 term -> Bool

Ord term => Ord (Term0 term)

Defined in Codec.TPTP.Base

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

ToTPTP t => ToTPTP (Term0 t)

Defined in Codec.TPTP.Export

Methods

toTPTP :: Term0 t -> ShowS

data BinOp

Binary formula connectives

Constructors

(:<=>:)

Equivalence

(:=>:)

Implication

(:<=:)

Reverse Implication

(:&:)

AND

(:|:)

OR

(:~&:)

NAND

(:~|:)

NOR

(:<~>:)

XOR

Instances

Arbitrary BinOp

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen BinOp

shrink :: BinOp -> [BinOp]

Pretty BinOp

Defined in Codec.TPTP.Pretty

Methods

pretty :: BinOp -> Doc

prettyList :: [BinOp] -> Doc

Data BinOp

Defined in Codec.TPTP.Base

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 :: forall r r'. (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

Bounded BinOp

Defined in Codec.TPTP.Base

Methods

minBound :: BinOp

maxBound :: BinOp

Enum BinOp

Defined in Codec.TPTP.Base

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]

Read BinOp

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS BinOp

readList :: ReadS [BinOp]

readPrec :: ReadPrec BinOp

readListPrec :: ReadPrec [BinOp]

Show BinOp

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> BinOp -> ShowS

show :: BinOp -> String

showList :: [BinOp] -> ShowS

Eq BinOp

Defined in Codec.TPTP.Base

Methods

(==) :: BinOp -> BinOp -> Bool

(/=) :: BinOp -> BinOp -> Bool

Ord BinOp

Defined in Codec.TPTP.Base

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

ToTPTP BinOp

Defined in Codec.TPTP.Export

Methods

toTPTP :: BinOp -> ShowS

data InfixPred

Term -> Term -> Formula infix connectives

Constructors

(:=:)

(:!=:)

Instances

Arbitrary InfixPred

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen InfixPred

shrink :: InfixPred -> [InfixPred]

Pretty InfixPred

Defined in Codec.TPTP.Pretty

Methods

pretty :: InfixPred -> Doc

prettyList :: [InfixPred] -> Doc

Data InfixPred

Defined in Codec.TPTP.Base

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 :: forall r r'. (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

Bounded InfixPred

Defined in Codec.TPTP.Base

Methods

minBound :: InfixPred

maxBound :: InfixPred

Enum InfixPred

Defined in Codec.TPTP.Base

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]

Read InfixPred

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS InfixPred

readList :: ReadS [InfixPred]

readPrec :: ReadPrec InfixPred

readListPrec :: ReadPrec [InfixPred]

Show InfixPred

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> InfixPred -> ShowS

show :: InfixPred -> String

showList :: [InfixPred] -> ShowS

Eq InfixPred

Defined in Codec.TPTP.Base

Methods

(==) :: InfixPred -> InfixPred -> Bool

(/=) :: InfixPred -> InfixPred -> Bool

Ord InfixPred

Defined in Codec.TPTP.Base

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

ToTPTP InfixPred

Defined in Codec.TPTP.Export

Methods

toTPTP :: InfixPred -> ShowS

data Quant

Quantifier specification

Constructors

All

Exists

Instances

Arbitrary Quant

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen Quant

shrink :: Quant -> [Quant]

Pretty Quant

Defined in Codec.TPTP.Pretty

Methods

pretty :: Quant -> Doc

prettyList :: [Quant] -> Doc

Data Quant

Defined in Codec.TPTP.Base

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 :: forall r r'. (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

Bounded Quant

Defined in Codec.TPTP.Base

Methods

minBound :: Quant

maxBound :: Quant

Enum Quant

Defined in Codec.TPTP.Base

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]

Read Quant

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS Quant

readList :: ReadS [Quant]

readPrec :: ReadPrec Quant

readListPrec :: ReadPrec [Quant]

Show Quant

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> Quant -> ShowS

show :: Quant -> String

showList :: [Quant] -> ShowS

Eq Quant

Defined in Codec.TPTP.Base

Methods

(==) :: Quant -> Quant -> Bool

(/=) :: Quant -> Quant -> Bool

Ord Quant

Defined in Codec.TPTP.Base

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

ToTPTP Quant

Defined in Codec.TPTP.Export

Methods

toTPTP :: Quant -> ShowS

Formula Metadata

type TPTP_Input = TPTP_Input_ Identity

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

type TPTP_Input_C = TPTP_Input_ (State [String])

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

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

data TPTP_Input_ c

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

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen TPTP_Input

shrink :: TPTP_Input -> [TPTP_Input]

Pretty TPTP_Input

Defined in Codec.TPTP.Pretty

Methods

pretty :: TPTP_Input -> Doc

prettyList :: [TPTP_Input] -> Doc

ToTPTP TPTP_Input

Defined in Codec.TPTP.Export

Methods

toTPTP :: TPTP_Input -> ShowS

(Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c)

Defined in Codec.TPTP.Base

Methods

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

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

toConstr :: TPTP_Input_ c -> Constr

dataTypeOf :: TPTP_Input_ c -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (TPTP_Input_ c))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (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 :: forall r r'. (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)

Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c)

Defined in Codec.TPTP.Base

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)

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> TPTP_Input_ c -> ShowS

show :: TPTP_Input_ c -> String

showList :: [TPTP_Input_ c] -> ShowS

Eq (c (Formula0 (T c) (F c))) => Eq (TPTP_Input_ c)

Defined in Codec.TPTP.Base

Methods

(==) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool

(/=) :: TPTP_Input_ c -> TPTP_Input_ c -> Bool

Ord (c (Formula0 (T c) (F c))) => Ord (TPTP_Input_ c)

Defined in Codec.TPTP.Base

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

ToTPTP [TPTP_Input]

Defined in Codec.TPTP.Export

Methods

toTPTP :: [TPTP_Input] -> ShowS

data Annotations

Annotations about the formulas origin

Constructors

NoAnnotations

Annotations GTerm UsefulInfo

Instances

Arbitrary Annotations

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen Annotations

shrink :: Annotations -> [Annotations]

Pretty Annotations

Defined in Codec.TPTP.Pretty

Methods

pretty :: Annotations -> Doc

prettyList :: [Annotations] -> Doc

Data Annotations

Defined in Codec.TPTP.Base

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 :: forall r r'. (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

Read Annotations

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS Annotations

readList :: ReadS [Annotations]

readPrec :: ReadPrec Annotations

readListPrec :: ReadPrec [Annotations]

Show Annotations

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> Annotations -> ShowS

show :: Annotations -> String

showList :: [Annotations] -> ShowS

Eq Annotations

Defined in Codec.TPTP.Base

Methods

(==) :: Annotations -> Annotations -> Bool

(/=) :: Annotations -> Annotations -> Bool

Ord Annotations

Defined in Codec.TPTP.Base

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

ToTPTP Annotations

Defined in Codec.TPTP.Export

Methods

toTPTP :: Annotations -> ShowS

data UsefulInfo

Misc annotations

Constructors

NoUsefulInfo

UsefulInfo [GTerm]

Instances

Arbitrary UsefulInfo

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen UsefulInfo

shrink :: UsefulInfo -> [UsefulInfo]

Pretty UsefulInfo

Defined in Codec.TPTP.Pretty

Methods

pretty :: UsefulInfo -> Doc

prettyList :: [UsefulInfo] -> Doc

Data UsefulInfo

Defined in Codec.TPTP.Base

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 :: forall r r'. (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

Read UsefulInfo

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS UsefulInfo

readList :: ReadS [UsefulInfo]

readPrec :: ReadPrec UsefulInfo

readListPrec :: ReadPrec [UsefulInfo]

Show UsefulInfo

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> UsefulInfo -> ShowS

show :: UsefulInfo -> String

showList :: [UsefulInfo] -> ShowS

Eq UsefulInfo

Defined in Codec.TPTP.Base

Methods

(==) :: UsefulInfo -> UsefulInfo -> Bool

(/=) :: UsefulInfo -> UsefulInfo -> Bool

Ord UsefulInfo

Defined in Codec.TPTP.Base

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

ToTPTP UsefulInfo

Defined in Codec.TPTP.Export

Methods

toTPTP :: UsefulInfo -> ShowS

newtype Role

Formula roles

Constructors

Role

Fields

• unrole :: String

Instances

Arbitrary Role

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen Role

shrink :: Role -> [Role]

Data Role

Defined in Codec.TPTP.Base

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 :: forall r r'. (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

Read Role

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS Role

readList :: ReadS [Role]

readPrec :: ReadPrec Role

readListPrec :: ReadPrec [Role]

Show Role

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> Role -> ShowS

show :: Role -> String

showList :: [Role] -> ShowS

Eq Role

Defined in Codec.TPTP.Base

Methods

(==) :: Role -> Role -> Bool

(/=) :: Role -> Role -> Bool

Ord Role

Defined in Codec.TPTP.Base

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

ToTPTP Role

Defined in Codec.TPTP.Export

Methods

toTPTP :: Role -> ShowS

data GData

Metadata (the general_data rule in TPTP's grammar)

Constructors

GWord AtomicWord

GApp AtomicWord [GTerm]

GVar V

GNumber Rational

GDistinctObject String

GFormulaData String Formula

GFormulaTerm String Term

Instances

Arbitrary GData

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen GData

shrink :: GData -> [GData]

Pretty GData

Defined in Codec.TPTP.Pretty

Methods

pretty :: GData -> Doc

prettyList :: [GData] -> Doc

Data GData

Defined in Codec.TPTP.Base

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 :: forall r r'. (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

Read GData

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS GData

readList :: ReadS [GData]

readPrec :: ReadPrec GData

readListPrec :: ReadPrec [GData]

Show GData

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> GData -> ShowS

show :: GData -> String

showList :: [GData] -> ShowS

Eq GData

Defined in Codec.TPTP.Base

Methods

(==) :: GData -> GData -> Bool

(/=) :: GData -> GData -> Bool

Ord GData

Defined in Codec.TPTP.Base

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

ToTPTP GData

Defined in Codec.TPTP.Export

Methods

toTPTP :: GData -> ShowS

data GTerm

Metadata (the general_term rule in TPTP's grammar)

Constructors

ColonSep GData GTerm

GTerm GData

GList [GTerm]

Instances

Arbitrary GTerm

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen GTerm

shrink :: GTerm -> [GTerm]

Pretty GTerm

Defined in Codec.TPTP.Pretty

Methods

pretty :: GTerm -> Doc

prettyList :: [GTerm] -> Doc

Data GTerm

Defined in Codec.TPTP.Base

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 :: forall r r'. (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

Read GTerm

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS GTerm

readList :: ReadS [GTerm]

readPrec :: ReadPrec GTerm

readListPrec :: ReadPrec [GTerm]

Show GTerm

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> GTerm -> ShowS

show :: GTerm -> String

showList :: [GTerm] -> ShowS

Eq GTerm

Defined in Codec.TPTP.Base

Methods

(==) :: GTerm -> GTerm -> Bool

(/=) :: GTerm -> GTerm -> Bool

Ord GTerm

Defined in Codec.TPTP.Base

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

ToTPTP GTerm

Defined in Codec.TPTP.Export

Methods

toTPTP :: GTerm -> ShowS

Gathering free Variables

class FreeVars a where

Methods

freeVars :: a -> Set V

Obtain the free variables from a formula or term

Instances

FreeVars Formula

Defined in Codec.TPTP.Base

Methods

freeVars :: Formula -> Set V

FreeVars Term

Defined in Codec.TPTP.Base

Methods

freeVars :: Term -> Set V

univquant_free_vars :: Formula -> Formula

Universally quantify all free variables in the formula

univquant_free_vars_FC :: FormulaC -> FormulaC

Universally quantify all free variables in the formula

arbCNF :: Gen Formula

arbLiteral :: Gen Formula

arbAtomicFormula :: Gen Formula

newtype AtomicWord

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

Arbitrary AtomicWord

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen AtomicWord

shrink :: AtomicWord -> [AtomicWord]

Pretty AtomicWord

Defined in Codec.TPTP.Pretty

Methods

pretty :: AtomicWord -> Doc

prettyList :: [AtomicWord] -> Doc

Data AtomicWord

Defined in Codec.TPTP.Base

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 :: forall r r'. (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

IsString AtomicWord

Defined in Codec.TPTP.Base

Methods

fromString :: String -> AtomicWord

Monoid AtomicWord

Defined in Codec.TPTP.Base

Methods

mempty :: AtomicWord

mappend :: AtomicWord -> AtomicWord -> AtomicWord

mconcat :: [AtomicWord] -> AtomicWord

Semigroup AtomicWord

Defined in Codec.TPTP.Base

Methods

(<>) :: AtomicWord -> AtomicWord -> AtomicWord

sconcat :: NonEmpty AtomicWord -> AtomicWord

stimes :: Integral b => b -> AtomicWord -> AtomicWord

Read AtomicWord

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS AtomicWord

readList :: ReadS [AtomicWord]

readPrec :: ReadPrec AtomicWord

readListPrec :: ReadPrec [AtomicWord]

Show AtomicWord

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> AtomicWord -> ShowS

show :: AtomicWord -> String

showList :: [AtomicWord] -> ShowS

Eq AtomicWord

Defined in Codec.TPTP.Base

Methods

(==) :: AtomicWord -> AtomicWord -> Bool

(/=) :: AtomicWord -> AtomicWord -> Bool

Ord AtomicWord

Defined in Codec.TPTP.Base

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

ToTPTP AtomicWord

Defined in Codec.TPTP.Export

Methods

toTPTP :: AtomicWord -> ShowS

newtype V

Variable names

Constructors

V String

Instances

Arbitrary V

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen V

shrink :: V -> [V]

Pretty V

Defined in Codec.TPTP.Pretty

Methods

pretty :: V -> Doc

prettyList :: [V] -> Doc

Data V

Defined in Codec.TPTP.Base

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 :: forall r r'. (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

IsString V

Defined in Codec.TPTP.Base

Methods

fromString :: String -> V

Monoid V

Defined in Codec.TPTP.Base

Methods

mempty :: V

mappend :: V -> V -> V

mconcat :: [V] -> V

Semigroup V

Defined in Codec.TPTP.Base

Methods

(<>) :: V -> V -> V

sconcat :: NonEmpty V -> V

stimes :: Integral b => b -> V -> V

Read V

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS V

readList :: ReadS [V]

readPrec :: ReadPrec V

readListPrec :: ReadPrec [V]

Show V

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> V -> ShowS

show :: V -> String

showList :: [V] -> ShowS

Eq V

Defined in Codec.TPTP.Base

Methods

(==) :: V -> V -> Bool

(/=) :: V -> V -> Bool

Ord V

Defined in Codec.TPTP.Base

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

ToTPTP V

Defined in Codec.TPTP.Export

Methods

toTPTP :: V -> ShowS

Fixed-point style decorated formulae and terms

newtype F c

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

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen Formula

shrink :: Formula -> [Formula]

Pretty Formula

Defined in Codec.TPTP.Pretty

Methods

pretty :: Formula -> Doc

prettyList :: [Formula] -> Doc

Pretty F0Diff

Defined in Codec.TPTP.Diff

Methods

pretty :: F0Diff -> Doc

prettyList :: [F0Diff] -> Doc

FreeVars Formula

Defined in Codec.TPTP.Base

Methods

freeVars :: Formula -> Set V

ToTPTP Formula

Defined in Codec.TPTP.Export

Methods

toTPTP :: Formula -> ShowS

Diffable Formula (F DiffResult)

Defined in Codec.TPTP.Diff

Methods

diff :: Formula -> Formula -> F DiffResult

Pretty (F DiffResult)

Defined in Codec.TPTP.Diff

Methods

pretty :: F DiffResult -> Doc

prettyList :: [F DiffResult] -> Doc

Pretty (WithEnclosing (F DiffResult))

Defined in Codec.TPTP.Diff

Methods

pretty :: WithEnclosing (F DiffResult) -> Doc

prettyList :: [WithEnclosing (F DiffResult)] -> Doc

Pretty (WithEnclosing Formula)

Defined in Codec.TPTP.Pretty

Methods

pretty :: WithEnclosing Formula -> Doc

prettyList :: [WithEnclosing Formula] -> Doc

Pretty (WithEnclosing F0Diff)

Defined in Codec.TPTP.Diff

Methods

pretty :: WithEnclosing F0Diff -> Doc

prettyList :: [WithEnclosing F0Diff] -> Doc

(Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (F c)

Defined in Codec.TPTP.Base

Methods

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

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

toConstr :: F c -> Constr

dataTypeOf :: F c -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (F c))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (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 :: forall r r'. (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)

Read (c (Formula0 (T c) (F c))) => Read (F c)

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS (F c)

readList :: ReadS [F c]

readPrec :: ReadPrec (F c)

readListPrec :: ReadPrec [F c]

Show (F DiffResult)

Defined in Codec.TPTP.Diff

Methods

showsPrec :: Int -> F DiffResult -> ShowS

show :: F DiffResult -> String

showList :: [F DiffResult] -> ShowS

Show (c (Formula0 (T c) (F c))) => Show (F c)

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> F c -> ShowS

show :: F c -> String

showList :: [F c] -> ShowS

Eq (c (Formula0 (T c) (F c))) => Eq (F c)

Defined in Codec.TPTP.Base

Methods

(==) :: F c -> F c -> Bool

(/=) :: F c -> F c -> Bool

Ord (c (Formula0 (T c) (F c))) => Ord (F c)

Defined in Codec.TPTP.Base

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

Pretty (Formula0 Term Formula)

Defined in Codec.TPTP.Pretty

Methods

pretty :: Formula0 Term Formula -> Doc

prettyList :: [Formula0 Term Formula] -> Doc

newtype T c

Terms whose subterms are wrapped in the given type constructor c

Constructors

T

Fields

• runT :: c (Term0 (T c))

Instances

Arbitrary Term

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen Term

shrink :: Term -> [Term]

Pretty Term

Defined in Codec.TPTP.Pretty

Methods

pretty :: Term -> Doc

prettyList :: [Term] -> Doc

Pretty F0Diff

Defined in Codec.TPTP.Diff

Methods

pretty :: F0Diff -> Doc

prettyList :: [F0Diff] -> Doc

Pretty T0Diff

Defined in Codec.TPTP.Diff

Methods

pretty :: T0Diff -> Doc

prettyList :: [T0Diff] -> Doc

FreeVars Term

Defined in Codec.TPTP.Base

Methods

freeVars :: Term -> Set V

ToTPTP Term

Defined in Codec.TPTP.Export

Methods

toTPTP :: Term -> ShowS

Diffable Term (T DiffResult)

Defined in Codec.TPTP.Diff

Methods

diff :: Term -> Term -> T DiffResult

Pretty (T DiffResult)

Defined in Codec.TPTP.Diff

Methods

pretty :: T DiffResult -> Doc

prettyList :: [T DiffResult] -> Doc

Pretty (Term0 Term)

Defined in Codec.TPTP.Pretty

Methods

pretty :: Term0 Term -> Doc

prettyList :: [Term0 Term] -> Doc

Pretty (WithEnclosing (T DiffResult))

Defined in Codec.TPTP.Diff

Methods

pretty :: WithEnclosing (T DiffResult) -> Doc

prettyList :: [WithEnclosing (T DiffResult)] -> Doc

Pretty (WithEnclosing Term)

Defined in Codec.TPTP.Pretty

Methods

pretty :: WithEnclosing Term -> Doc

prettyList :: [WithEnclosing Term] -> Doc

Pretty (WithEnclosing F0Diff)

Defined in Codec.TPTP.Diff

Methods

pretty :: WithEnclosing F0Diff -> Doc

prettyList :: [WithEnclosing F0Diff] -> Doc

Pretty (WithEnclosing T0Diff)

Defined in Codec.TPTP.Diff

Methods

pretty :: WithEnclosing T0Diff -> Doc

prettyList :: [WithEnclosing T0Diff] -> Doc

(Typeable c, Data (c (Term0 (T c)))) => Data (T c)

Defined in Codec.TPTP.Base

Methods

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

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

toConstr :: T c -> Constr

dataTypeOf :: T c -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (T c))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (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 :: forall r r'. (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)

Read (c (Term0 (T c))) => Read (T c)

Defined in Codec.TPTP.Base

Methods

readsPrec :: Int -> ReadS (T c)

readList :: ReadS [T c]

readPrec :: ReadPrec (T c)

readListPrec :: ReadPrec [T c]

Show (T DiffResult)

Defined in Codec.TPTP.Diff

Methods

showsPrec :: Int -> T DiffResult -> ShowS

show :: T DiffResult -> String

showList :: [T DiffResult] -> ShowS

Show (c (Term0 (T c))) => Show (T c)

Defined in Codec.TPTP.Base

Methods

showsPrec :: Int -> T c -> ShowS

show :: T c -> String

showList :: [T c] -> ShowS

Eq (c (Term0 (T c))) => Eq (T c)

Defined in Codec.TPTP.Base

Methods

(==) :: T c -> T c -> Bool

(/=) :: T c -> T c -> Bool

Ord (c (Term0 (T c))) => Ord (T c)

Defined in Codec.TPTP.Base

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

Pretty (Formula0 Term Formula)

Defined in Codec.TPTP.Pretty

Methods

pretty :: Formula0 Term Formula -> Doc

prettyList :: [Formula0 Term Formula] -> Doc

Utility functions

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

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

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

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

foldF

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

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