Safe Haskell	Safe-Inferred
Language	Haskell2010

Codec.TPTP.Base

Contents

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

Synopsis

type Formula = F Identity
type Term = T Identity
type FormulaW s = F (Writer s)
type TermW s = T (Writer s)
type FormulaC = FormulaW [String]
type TermC = TermW [String]
forgetFC :: FormulaC -> Formula
forgetTC :: TermC -> Term
(.<=>.) :: Pointed c => F c -> F c -> F c
(.=>.) :: Pointed c => F c -> F c -> F c
(.<=.) :: Pointed c => F c -> F c -> F c
(.|.) :: Pointed c => F c -> F c -> F c
(.&.) :: Pointed c => F c -> F c -> F c
(.<~>.) :: Pointed c => F c -> F c -> F c
(.~|.) :: Pointed c => F c -> F c -> F c
(.~&.) :: Pointed c => F c -> F c -> F c
(.~.) :: Pointed c => F c -> F c
(.=.) :: Pointed c => T c -> T c -> F c
(.!=.) :: Pointed c => T c -> T c -> F c
for_all :: Pointed c => [V] -> F c -> F c
exists :: Pointed c => [V] -> F c -> F c
pApp :: Pointed c => AtomicWord -> [T c] -> F c
var :: Pointed c => V -> T c
fApp :: Pointed c => AtomicWord -> [T c] -> T c
numberLitTerm :: Pointed c => Rational -> T c
distinctObjectTerm :: Pointed c => String -> T c
data Formula0 term formula
- = BinOp formula BinOp formula
- | InfixPred term InfixPred term
- | PredApp AtomicWord [term]
- | Quant Quant [V] formula
- | (:~:) formula
data Term0 term
- = Var V
- | NumberLitTerm Rational
- | DistinctObjectTerm String
- | FunApp AtomicWord [term]
data BinOp
- = (:<=>:)
- | (:=>:)
- | (:<=:)
- | (:&:)
- | (:|:)
- | (:~&:)
- | (:~|:)
- | (:<~>:)
data InfixPred
- = (:=:)
- | (:!=:)
data Quant
- = All
- | Exists
type TPTP_Input = TPTP_Input_ Identity
type TPTP_Input_C = TPTP_Input_ (Writer [String])
forgetTIC :: TPTP_Input_C -> TPTP_Input
data TPTP_Input_ c
- = AFormula {
  - name :: AtomicWord
  - role :: Role
  - formula :: F c
  - annotations :: Annotations
  }
- | Comment String
- | Include FilePath [AtomicWord]
data Annotations
- = NoAnnotations
- | Annotations GTerm UsefulInfo
data UsefulInfo
- = NoUsefulInfo
- | UsefulInfo [GTerm]
newtype Role = Role {
- unrole :: String
}
data GData
- = GWord AtomicWord
- | GApp AtomicWord [GTerm]
- | GVar V
- | GNumber Rational
- | GDistinctObject String
- | GFormulaData String Formula
- | GFormulaTerm String Term
data GTerm
- = ColonSep GData GTerm
- | GTerm GData
- | GList [GTerm]
class FreeVars a where
- freeVars :: a -> Set V
univquant_free_vars :: Formula -> Formula
univquant_free_vars_FC :: FormulaC -> FormulaC
arbCNF :: Gen Formula
arbLiteral :: Gen Formula
arbAtomicFormula :: Gen Formula
newtype AtomicWord = AtomicWord String
newtype V = V String
newtype F c = F {
- runF :: c (Formula0 (T c) (F c))
}
newtype T c = T {
- runT :: c (Term0 (T c))
}
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 :: Copointed t => (F t -> r) -> (Quant -> [V] -> F t -> r) -> (F t -> BinOp -> F t -> r) -> (T t -> InfixPred -> T t -> r) -> (AtomicWord -> [T t] -> r) -> F t -> r
foldT :: Copointed t => (String -> r) -> (Rational -> r) -> (V -> r) -> (AtomicWord -> [T t] -> r) -> T t -> r

Basic undecorated formulae and terms

type Formula = F Identity Source #

Basic (undecorated) first-order formulae

type Term = T Identity Source #

Basic (undecorated) terms

Formulae and terms decorated with state

type FormulaW s = F (Writer s) Source #

First-order formulae decorated with state

type TermW s = T (Writer s) Source #

Terms decorated with state

type FormulaC = FormulaW [String] Source #

First-order formulae decorated with comments

type TermC = TermW [String] Source #

Terms decorated with comments

forgetFC :: FormulaC -> Formula Source #

Forget comments in formulae decorated with comments

forgetTC :: TermC -> Term Source #

Forget comments in terms decorated with comments

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

Equivalence

Important special case:

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

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

Implication

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

Reverse implication

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

Disjunction/OR

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

Conjunction/AND

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

XOR

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

NOR

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

NAND

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

Negation

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

Equality

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

Inequality

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

Universal quantification

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

Existential quantification

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

Predicate symbol application

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

Variable

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

Function symbol application (constants are encoded as nullary functions)

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

Number literal

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

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

General decorated formulae and terms

data Formula0 term formula Source #

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

Constructors

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

Instances

Instances details

PrettyAnsi F0Diff Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: F0Diff -> Doc AnsiStyle Source # prettyAnsiList :: [F0Diff] -> Doc AnsiStyle Source #
(PrettyAnsi (WithEnclosing t), PrettyAnsi (WithEnclosing f)) => PrettyAnsi (WithEnclosing (Formula0 t f)) Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: WithEnclosing (Formula0 t f) -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing (Formula0 t f)] -> Doc AnsiStyle Source #
PrettyAnsi (WithEnclosing F0Diff) Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: WithEnclosing F0Diff -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing F0Diff] -> Doc AnsiStyle Source #
(Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b) Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen (Formula0 a b) # shrink :: Formula0 a b -> [Formula0 a b] #
(Data term, Data formula) => Data (Formula0 term formula) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Formula0 t f -> ShowS Source #
PrettyAnsi (Formula0 Term Formula) Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: Formula0 Term Formula -> Doc AnsiStyle Source # prettyAnsiList :: [Formula0 Term Formula] -> Doc AnsiStyle Source #

data Term0 term Source #

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

Constructors

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

Instances

Instances details

PrettyAnsi T0Diff Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: T0Diff -> Doc AnsiStyle Source # prettyAnsiList :: [T0Diff] -> Doc AnsiStyle Source #
Arbitrary a => Arbitrary (Term0 a) Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen (Term0 a) # shrink :: Term0 a -> [Term0 a] #
Data term => Data (Term0 term) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> Term0 term -> ShowS # show :: Term0 term -> String # showList :: [Term0 term] -> ShowS #
Eq term => Eq (Term0 term) Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: Term0 term -> Term0 term -> Bool # (/=) :: Term0 term -> Term0 term -> Bool #
Ord term => Ord (Term0 term) Source #
Instance details 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) Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Term0 t -> ShowS Source #
PrettyAnsi (Term0 Term) Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: Term0 Term -> Doc AnsiStyle Source # prettyAnsiList :: [Term0 Term] -> Doc AnsiStyle Source #
PrettyAnsi (WithEnclosing t) => PrettyAnsi (WithEnclosing (Term0 t)) Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: WithEnclosing (Term0 t) -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing (Term0 t)] -> Doc AnsiStyle Source #
PrettyAnsi (WithEnclosing T0Diff) Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: WithEnclosing T0Diff -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing T0Diff] -> Doc AnsiStyle Source #

data BinOp Source #

Binary formula connectives

Constructors

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

Instances

Instances details

Arbitrary BinOp Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen BinOp # shrink :: BinOp -> [BinOp] #
Data BinOp Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods minBound :: BinOp # maxBound :: BinOp #
Enum BinOp Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods readsPrec :: Int -> ReadS BinOp # readList :: ReadS [BinOp] # readPrec :: ReadPrec BinOp # readListPrec :: ReadPrec [BinOp] #
Show BinOp Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> BinOp -> ShowS # show :: BinOp -> String # showList :: [BinOp] -> ShowS #
Eq BinOp Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: BinOp -> BinOp -> Bool # (/=) :: BinOp -> BinOp -> Bool #
Ord BinOp Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: BinOp -> ShowS Source #
PrettyAnsi BinOp Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: BinOp -> Doc AnsiStyle Source # prettyAnsiList :: [BinOp] -> Doc AnsiStyle Source #

data InfixPred Source #

Term -> Term -> Formula infix connectives

Constructors

(:=:)
(:!=:)

Instances

Instances details

Arbitrary InfixPred Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen InfixPred # shrink :: InfixPred -> [InfixPred] #
Data InfixPred Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods minBound :: InfixPred # maxBound :: InfixPred #
Enum InfixPred Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods readsPrec :: Int -> ReadS InfixPred # readList :: ReadS [InfixPred] # readPrec :: ReadPrec InfixPred # readListPrec :: ReadPrec [InfixPred] #
Show InfixPred Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> InfixPred -> ShowS # show :: InfixPred -> String # showList :: [InfixPred] -> ShowS #
Eq InfixPred Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: InfixPred -> InfixPred -> Bool # (/=) :: InfixPred -> InfixPred -> Bool #
Ord InfixPred Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: InfixPred -> ShowS Source #
PrettyAnsi InfixPred Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: InfixPred -> Doc AnsiStyle Source # prettyAnsiList :: [InfixPred] -> Doc AnsiStyle Source #

data Quant Source #

Quantifier specification

Constructors

All
Exists

Instances

Instances details

Arbitrary Quant Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen Quant # shrink :: Quant -> [Quant] #
Data Quant Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods minBound :: Quant # maxBound :: Quant #
Enum Quant Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods readsPrec :: Int -> ReadS Quant # readList :: ReadS [Quant] # readPrec :: ReadPrec Quant # readListPrec :: ReadPrec [Quant] #
Show Quant Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> Quant -> ShowS # show :: Quant -> String # showList :: [Quant] -> ShowS #
Eq Quant Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: Quant -> Quant -> Bool # (/=) :: Quant -> Quant -> Bool #
Ord Quant Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Quant -> ShowS Source #
PrettyAnsi Quant Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: Quant -> Doc AnsiStyle Source # prettyAnsiList :: [Quant] -> Doc AnsiStyle Source #

Formula Metadata

type TPTP_Input = TPTP_Input_ Identity Source #

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

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

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

forgetTIC :: TPTP_Input_C -> TPTP_Input Source #

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

data TPTP_Input_ c Source #

Generalized TPTP_Input

Constructors

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

Instances

Instances details

Arbitrary TPTP_Input Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen TPTP_Input # shrink :: TPTP_Input -> [TPTP_Input] #
ToTPTP TPTP_Input Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: TPTP_Input -> ShowS Source #
PrettyAnsi TPTP_Input Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: TPTP_Input -> Doc AnsiStyle Source # prettyAnsiList :: [TPTP_Input] -> Doc AnsiStyle Source #
(Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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] Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: [TPTP_Input] -> ShowS Source #

data Annotations Source #

Annotations about the formulas origin

Constructors

NoAnnotations
Annotations GTerm UsefulInfo

Instances

Instances details

Arbitrary Annotations Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen Annotations # shrink :: Annotations -> [Annotations] #
Data Annotations Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods readsPrec :: Int -> ReadS Annotations # readList :: ReadS [Annotations] # readPrec :: ReadPrec Annotations # readListPrec :: ReadPrec [Annotations] #
Show Annotations Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> Annotations -> ShowS # show :: Annotations -> String # showList :: [Annotations] -> ShowS #
Eq Annotations Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: Annotations -> Annotations -> Bool # (/=) :: Annotations -> Annotations -> Bool #
Ord Annotations Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Annotations -> ShowS Source #
PrettyAnsi Annotations Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: Annotations -> Doc AnsiStyle Source # prettyAnsiList :: [Annotations] -> Doc AnsiStyle Source #

data UsefulInfo Source #

Misc annotations

Constructors

NoUsefulInfo
UsefulInfo [GTerm]

Instances

Instances details

Arbitrary UsefulInfo Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen UsefulInfo # shrink :: UsefulInfo -> [UsefulInfo] #
Data UsefulInfo Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods readsPrec :: Int -> ReadS UsefulInfo # readList :: ReadS [UsefulInfo] # readPrec :: ReadPrec UsefulInfo # readListPrec :: ReadPrec [UsefulInfo] #
Show UsefulInfo Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> UsefulInfo -> ShowS # show :: UsefulInfo -> String # showList :: [UsefulInfo] -> ShowS #
Eq UsefulInfo Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: UsefulInfo -> UsefulInfo -> Bool # (/=) :: UsefulInfo -> UsefulInfo -> Bool #
Ord UsefulInfo Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: UsefulInfo -> ShowS Source #
PrettyAnsi UsefulInfo Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: UsefulInfo -> Doc AnsiStyle Source # prettyAnsiList :: [UsefulInfo] -> Doc AnsiStyle Source #

newtype Role Source #

Formula roles

Constructors

Role
Fields unrole :: String

Instances

Instances details

Arbitrary Role Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen Role # shrink :: Role -> [Role] #
Data Role Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods readsPrec :: Int -> ReadS Role # readList :: ReadS [Role] # readPrec :: ReadPrec Role # readListPrec :: ReadPrec [Role] #
Show Role Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> Role -> ShowS # show :: Role -> String # showList :: [Role] -> ShowS #
Eq Role Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: Role -> Role -> Bool # (/=) :: Role -> Role -> Bool #
Ord Role Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Role -> ShowS Source #

data GData Source #

Metadata (the general_data rule in TPTP's grammar)

Constructors

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

Instances

Instances details

Arbitrary GData Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen GData # shrink :: GData -> [GData] #
Data GData Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods readsPrec :: Int -> ReadS GData # readList :: ReadS [GData] # readPrec :: ReadPrec GData # readListPrec :: ReadPrec [GData] #
Show GData Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> GData -> ShowS # show :: GData -> String # showList :: [GData] -> ShowS #
Eq GData Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: GData -> GData -> Bool # (/=) :: GData -> GData -> Bool #
Ord GData Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: GData -> ShowS Source #
PrettyAnsi GData Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: GData -> Doc AnsiStyle Source # prettyAnsiList :: [GData] -> Doc AnsiStyle Source #

data GTerm Source #

Metadata (the general_term rule in TPTP's grammar)

Constructors

ColonSep GData GTerm
GTerm GData
GList [GTerm]

Instances

Instances details

Arbitrary GTerm Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen GTerm # shrink :: GTerm -> [GTerm] #
Data GTerm Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods readsPrec :: Int -> ReadS GTerm # readList :: ReadS [GTerm] # readPrec :: ReadPrec GTerm # readListPrec :: ReadPrec [GTerm] #
Show GTerm Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> GTerm -> ShowS # show :: GTerm -> String # showList :: [GTerm] -> ShowS #
Eq GTerm Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: GTerm -> GTerm -> Bool # (/=) :: GTerm -> GTerm -> Bool #
Ord GTerm Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: GTerm -> ShowS Source #
PrettyAnsi GTerm Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: GTerm -> Doc AnsiStyle Source # prettyAnsiList :: [GTerm] -> Doc AnsiStyle Source #

Gathering free Variables

class FreeVars a where Source #

Methods

freeVars :: a -> Set V Source #

Obtain the free variables from a formula or term

Instances

Instances details

FreeVars Formula Source #
Instance details Defined in Codec.TPTP.Base Methods freeVars :: Formula -> Set V Source #
FreeVars Term Source #
Instance details Defined in Codec.TPTP.Base Methods freeVars :: Term -> Set V Source #

univquant_free_vars :: Formula -> Formula Source #

Universally quantify all free variables in the formula

univquant_free_vars_FC :: FormulaC -> FormulaC Source #

Universally quantify all free variables in the formula

arbCNF :: Gen Formula Source #

arbLiteral :: Gen Formula Source #

arbAtomicFormula :: Gen Formula Source #

newtype AtomicWord Source #

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

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

Constructors

AtomicWord String

Instances

Instances details

Arbitrary AtomicWord Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen AtomicWord # shrink :: AtomicWord -> [AtomicWord] #
Data AtomicWord Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods fromString :: String -> AtomicWord #
Monoid AtomicWord Source #
Instance details Defined in Codec.TPTP.Base Methods mempty :: AtomicWord # mappend :: AtomicWord -> AtomicWord -> AtomicWord # mconcat :: [AtomicWord] -> AtomicWord #
Semigroup AtomicWord Source #
Instance details Defined in Codec.TPTP.Base Methods (<>) :: AtomicWord -> AtomicWord -> AtomicWord # sconcat :: NonEmpty AtomicWord -> AtomicWord # stimes :: Integral b => b -> AtomicWord -> AtomicWord #
Read AtomicWord Source #
Instance details Defined in Codec.TPTP.Base Methods readsPrec :: Int -> ReadS AtomicWord # readList :: ReadS [AtomicWord] # readPrec :: ReadPrec AtomicWord # readListPrec :: ReadPrec [AtomicWord] #
Show AtomicWord Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> AtomicWord -> ShowS # show :: AtomicWord -> String # showList :: [AtomicWord] -> ShowS #
Eq AtomicWord Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: AtomicWord -> AtomicWord -> Bool # (/=) :: AtomicWord -> AtomicWord -> Bool #
Ord AtomicWord Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: AtomicWord -> ShowS Source #
Pretty AtomicWord Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: AtomicWord -> Doc ann # prettyList :: [AtomicWord] -> Doc ann #

newtype V Source #

Variable names

Constructors

V String

Instances

Instances details

Arbitrary V Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen V # shrink :: V -> [V] #
Data V Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Base Methods fromString :: String -> V #
Monoid V Source #
Instance details Defined in Codec.TPTP.Base Methods mempty :: V # mappend :: V -> V -> V # mconcat :: [V] -> V #
Semigroup V Source #
Instance details Defined in Codec.TPTP.Base Methods (<>) :: V -> V -> V # sconcat :: NonEmpty V -> V # stimes :: Integral b => b -> V -> V #
Read V Source #
Instance details Defined in Codec.TPTP.Base Methods readsPrec :: Int -> ReadS V # readList :: ReadS [V] # readPrec :: ReadPrec V # readListPrec :: ReadPrec [V] #
Show V Source #
Instance details Defined in Codec.TPTP.Base Methods showsPrec :: Int -> V -> ShowS # show :: V -> String # showList :: [V] -> ShowS #
Eq V Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: V -> V -> Bool # (/=) :: V -> V -> Bool #
Ord V Source #
Instance details 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 Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: V -> ShowS Source #
PrettyAnsi V Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: V -> Doc AnsiStyle Source # prettyAnsiList :: [V] -> Doc AnsiStyle Source #

Fixed-point style decorated formulae and terms

newtype F c Source #

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

For example:

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

Constructors

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

Instances

Instances details

Arbitrary Formula Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen Formula # shrink :: Formula -> [Formula] #
FreeVars Formula Source #
Instance details Defined in Codec.TPTP.Base Methods freeVars :: Formula -> Set V Source #
ToTPTP Formula Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Formula -> ShowS Source #
PrettyAnsi Formula Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: Formula -> Doc AnsiStyle Source # prettyAnsiList :: [Formula] -> Doc AnsiStyle Source #
PrettyAnsi F0Diff Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: F0Diff -> Doc AnsiStyle Source # prettyAnsiList :: [F0Diff] -> Doc AnsiStyle Source #
Diffable Formula (F DiffResult) Source #
Instance details Defined in Codec.TPTP.Diff Methods diff :: Formula -> Formula -> F DiffResult Source #
(Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (F c) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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 #
PrettyAnsi (F DiffResult) Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: F DiffResult -> Doc AnsiStyle Source # prettyAnsiList :: [F DiffResult] -> Doc AnsiStyle Source #
PrettyAnsi (WithEnclosing (F DiffResult)) Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: WithEnclosing (F DiffResult) -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing (F DiffResult)] -> Doc AnsiStyle Source #
PrettyAnsi (WithEnclosing Formula) Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: WithEnclosing Formula -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing Formula] -> Doc AnsiStyle Source #
PrettyAnsi (WithEnclosing F0Diff) Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: WithEnclosing F0Diff -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing F0Diff] -> Doc AnsiStyle Source #
PrettyAnsi (Formula0 Term Formula) Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: Formula0 Term Formula -> Doc AnsiStyle Source # prettyAnsiList :: [Formula0 Term Formula] -> Doc AnsiStyle Source #

newtype T c Source #

Terms whose subterms are wrapped in the given type constructor c

Constructors

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

Instances

Instances details

Arbitrary Term Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen Term # shrink :: Term -> [Term] #
FreeVars Term Source #
Instance details Defined in Codec.TPTP.Base Methods freeVars :: Term -> Set V Source #
ToTPTP Term Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Term -> ShowS Source #
PrettyAnsi Term Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: Term -> Doc AnsiStyle Source # prettyAnsiList :: [Term] -> Doc AnsiStyle Source #
PrettyAnsi F0Diff Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: F0Diff -> Doc AnsiStyle Source # prettyAnsiList :: [F0Diff] -> Doc AnsiStyle Source #
PrettyAnsi T0Diff Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: T0Diff -> Doc AnsiStyle Source # prettyAnsiList :: [T0Diff] -> Doc AnsiStyle Source #
Diffable Term (T DiffResult) Source #
Instance details Defined in Codec.TPTP.Diff Methods diff :: Term -> Term -> T DiffResult Source #
(Typeable c, Data (c (Term0 (T c)))) => Data (T c) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: T c -> T c -> Bool # (/=) :: T c -> T c -> Bool #
Ord (c (Term0 (T c))) => Ord (T c) Source #
Instance details 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 #
PrettyAnsi (T DiffResult) Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: T DiffResult -> Doc AnsiStyle Source # prettyAnsiList :: [T DiffResult] -> Doc AnsiStyle Source #
PrettyAnsi (Term0 Term) Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: Term0 Term -> Doc AnsiStyle Source # prettyAnsiList :: [Term0 Term] -> Doc AnsiStyle Source #
PrettyAnsi (WithEnclosing (T DiffResult)) Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: WithEnclosing (T DiffResult) -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing (T DiffResult)] -> Doc AnsiStyle Source #
PrettyAnsi (WithEnclosing Term) Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: WithEnclosing Term -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing Term] -> Doc AnsiStyle Source #
PrettyAnsi (WithEnclosing F0Diff) Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: WithEnclosing F0Diff -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing F0Diff] -> Doc AnsiStyle Source #
PrettyAnsi (WithEnclosing T0Diff) Source #
Instance details Defined in Codec.TPTP.Diff Methods prettyAnsi :: WithEnclosing T0Diff -> Doc AnsiStyle Source # prettyAnsiList :: [WithEnclosing T0Diff] -> Doc AnsiStyle Source #
PrettyAnsi (Formula0 Term Formula) Source #
Instance details Defined in Codec.TPTP.Pretty Methods prettyAnsi :: Formula0 Term Formula -> Doc AnsiStyle Source # prettyAnsiList :: [Formula0 Term Formula] -> Doc AnsiStyle Source #

Utility functions

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

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

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

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

foldF Source #

Arguments

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

Eliminate formulae

foldT Source #

Arguments

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

Eliminate terms