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

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

Defined in Codec.TPTP.Base

Methods

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

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

(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 :: (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 formula, Ord term) => 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

(Read formula, Read term) => 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 formula, Show term) => 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

(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

(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

Eq term => Eq (Term0 term)

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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)

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

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

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

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

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]

Eq BinOp

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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

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

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

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

ToTPTP BinOp

Defined in Codec.TPTP.Export

Methods

toTPTP :: BinOp -> ShowS

data InfixPred

Term -> Term -> Formula infix connectives

Constructors

(:=:)

(:!=:)

Instances

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]

Eq InfixPred

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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

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

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

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

ToTPTP InfixPred

Defined in Codec.TPTP.Export

Methods

toTPTP :: InfixPred -> ShowS

data Quant

Quantifier specification

Constructors

All

Exists

Instances

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]

Eq Quant

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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

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

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

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

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

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

(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 :: (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)

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

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

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

Eq Annotations

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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

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

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

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

ToTPTP Annotations

Defined in Codec.TPTP.Export

Methods

toTPTP :: Annotations -> ShowS

data UsefulInfo

Misc annotations

Constructors

NoUsefulInfo

UsefulInfo [GTerm]

Instances

Eq UsefulInfo

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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

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

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

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

ToTPTP UsefulInfo

Defined in Codec.TPTP.Export

Methods

toTPTP :: UsefulInfo -> ShowS

newtype Role

Formula roles

Constructors

Role

Fields

• unrole :: String

Instances

Eq Role

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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

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

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

Arbitrary Role

Defined in Codec.TPTP.Base

Methods

arbitrary :: Gen Role

shrink :: 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

Eq GData

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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

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

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

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

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

Eq GTerm

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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

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

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

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

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 Term

Defined in Codec.TPTP.Base

Methods

freeVars :: Term -> Set V

FreeVars Formula

Defined in Codec.TPTP.Base

Methods

freeVars :: Formula -> 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

Eq AtomicWord

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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

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

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

IsString AtomicWord

Defined in Codec.TPTP.Base

Methods

fromString :: String -> AtomicWord

Semigroup AtomicWord

Defined in Codec.TPTP.Base

Methods

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

sconcat :: NonEmpty AtomicWord -> AtomicWord

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

Monoid AtomicWord

Defined in Codec.TPTP.Base

Methods

mempty :: AtomicWord

mappend :: AtomicWord -> AtomicWord -> AtomicWord

mconcat :: [AtomicWord] -> AtomicWord

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

ToTPTP AtomicWord

Defined in Codec.TPTP.Export

Methods

toTPTP :: AtomicWord -> ShowS

newtype V

Variable names

Constructors

V String

Instances

Eq V

Defined in Codec.TPTP.Base

Methods

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

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

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 :: (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

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

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

IsString V

Defined in Codec.TPTP.Base

Methods

fromString :: String -> V

Semigroup V

Defined in Codec.TPTP.Base

Methods

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

sconcat :: NonEmpty V -> V

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

Monoid V

Defined in Codec.TPTP.Base

Methods

mempty :: V

mappend :: V -> V -> V

mconcat :: [V] -> V

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

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

Diffable Formula (F DiffResult)

Defined in Codec.TPTP.Diff

Methods

diff :: Formula -> Formula -> F DiffResult

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

(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 :: (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)

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

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 (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

Show (F DiffResult)

Defined in Codec.TPTP.Diff

Methods

showsPrec :: Int -> F DiffResult -> ShowS

show :: F DiffResult -> String

showList :: [F DiffResult] -> ShowS

Pretty (F Identity)

Defined in Codec.TPTP.Pretty

Methods

pretty :: F Identity -> Doc

prettyList :: [F Identity] -> Doc

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

ToTPTP (F Identity)

Defined in Codec.TPTP.Export

Methods

toTPTP :: F Identity -> ShowS

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

Diffable Term (T DiffResult)

Defined in Codec.TPTP.Diff

Methods

diff :: Term -> Term -> T DiffResult

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

Defined in Codec.TPTP.Base

Methods

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

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

(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 :: (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)

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

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 (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

Show (T DiffResult)

Defined in Codec.TPTP.Diff

Methods

showsPrec :: Int -> T DiffResult -> ShowS

show :: T DiffResult -> String

showList :: [T DiffResult] -> ShowS

Pretty (T Identity)

Defined in Codec.TPTP.Pretty

Methods

pretty :: T Identity -> Doc

prettyList :: [T Identity] -> Doc

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

ToTPTP (T Identity)

Defined in Codec.TPTP.Export

Methods

toTPTP :: T Identity -> ShowS

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