Safe Haskell	None
Language	Haskell98

Codec.TPTP.Base

Contents

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

Synopsis

type Formula = F Identity
type Term = T Identity
type FormulaST s = F (State s)
type TermST s = T (State s)
type FormulaC = FormulaST [String]
type TermC = TermST [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_ (State [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 FormulaST s = F (State s) Source #

First-order formulae decorated with state

type TermST s = T (State s) Source #

Terms decorated with state

type FormulaC = FormulaST [String] Source #

First-order formulae decorated with comments

type TermC = TermST [String] Source #

Terms decorated with comments

forgetFC :: FormulaC -> Formula Source #

Forget comments in formulae decorated with comments

forgetTC :: TermC -> Term Source #

Forget comments in terms decorated with comments

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

Equivalence

Important special case:

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

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

Implication

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

Reverse implication

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

Disjunction/OR

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

Conjunction/AND

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

XOR

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

NOR

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

NAND

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

Negation

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

Equality

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

Inequality

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

Universal quantification

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

Existential quantification

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

Predicate symbol application

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

Variable

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

Function symbol application (constants are encoded as nullary functions)

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

Number literal

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

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

General decorated formulae and terms

data Formula0 term formula Source #

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

Constructors

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

Instances

Pretty F0Diff Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: F0Diff -> Doc # prettyList :: [F0Diff] -> Doc #
(Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty (WithEnclosing (Formula0 t f)) Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: WithEnclosing (Formula0 t f) -> Doc # prettyList :: [WithEnclosing (Formula0 t f)] -> Doc #
Pretty (WithEnclosing F0Diff) Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: WithEnclosing F0Diff -> Doc # prettyList :: [WithEnclosing F0Diff] -> Doc #
(Eq formula, Eq term) => 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 #
(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 :: (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) 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 #
(Read formula, Read term) => 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 formula, Show term) => 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 #
(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] #
Pretty (Formula0 Term Formula) Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: Formula0 Term Formula -> Doc # prettyList :: [Formula0 Term Formula] -> Doc #
(ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f) Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Formula0 t f -> ShowS Source #

data Term0 term Source #

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

Constructors

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

Instances

Pretty T0Diff Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: T0Diff -> Doc # prettyList :: [T0Diff] -> Doc #
Eq term => Eq (Term0 term) Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: Term0 term -> Term0 term -> Bool # (/=) :: Term0 term -> Term0 term -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term0 term -> r # gmapQ :: (forall d. Data d => d -> u) -> Term0 term -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Term0 term -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term0 term -> m (Term0 term) #
Ord term => Ord (Term0 term) Source #
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 #
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 #
Arbitrary a => Arbitrary (Term0 a) Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen (Term0 a) # shrink :: Term0 a -> [Term0 a] #
Pretty (Term0 Term) Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: Term0 Term -> Doc # prettyList :: [Term0 Term] -> Doc #
Pretty (WithEnclosing t) => Pretty (WithEnclosing (Term0 t)) Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: WithEnclosing (Term0 t) -> Doc # prettyList :: [WithEnclosing (Term0 t)] -> Doc #
Pretty (WithEnclosing T0Diff) Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: WithEnclosing T0Diff -> Doc # prettyList :: [WithEnclosing T0Diff] -> Doc #
ToTPTP t => ToTPTP (Term0 t) Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Term0 t -> ShowS Source #

data BinOp Source #

Binary formula connectives

Constructors

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

Instances

Bounded BinOp Source #
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] #
Eq BinOp Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: BinOp -> BinOp -> Bool # (/=) :: BinOp -> BinOp -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r # gmapQ :: (forall d. Data d => d -> u) -> BinOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BinOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp #
Ord BinOp Source #
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 #
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 #
Arbitrary BinOp Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen BinOp # shrink :: BinOp -> [BinOp] #
Pretty BinOp Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: BinOp -> Doc # prettyList :: [BinOp] -> Doc #
ToTPTP BinOp Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: BinOp -> ShowS Source #

data InfixPred Source #

Term -> Term -> Formula infix connectives

Constructors

(:=:)
(:!=:)

Instances

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] #
Eq InfixPred Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: InfixPred -> InfixPred -> Bool # (/=) :: InfixPred -> InfixPred -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InfixPred -> r # gmapQ :: (forall d. Data d => d -> u) -> InfixPred -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> InfixPred -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InfixPred -> m InfixPred #
Ord InfixPred Source #
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 #
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 #
Arbitrary InfixPred Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen InfixPred # shrink :: InfixPred -> [InfixPred] #
Pretty InfixPred Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: InfixPred -> Doc # prettyList :: [InfixPred] -> Doc #
ToTPTP InfixPred Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: InfixPred -> ShowS Source #

data Quant Source #

Quantifier specification

Constructors

All
Exists

Instances

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] #
Eq Quant Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: Quant -> Quant -> Bool # (/=) :: Quant -> Quant -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r # gmapQ :: (forall d. Data d => d -> u) -> Quant -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Quant -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quant -> m Quant # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant #
Ord Quant Source #
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 #
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 #
Arbitrary Quant Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen Quant # shrink :: Quant -> [Quant] #
Pretty Quant Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: Quant -> Doc # prettyList :: [Quant] -> Doc #
ToTPTP Quant Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Quant -> ShowS Source #

Formula Metadata

type TPTP_Input = TPTP_Input_ Identity Source #

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

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

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

forgetTIC :: TPTP_Input_C -> TPTP_Input Source #

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

data TPTP_Input_ c Source #

Generalized TPTP_Input

Constructors

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

Instances

Arbitrary TPTP_Input Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen TPTP_Input # shrink :: TPTP_Input -> [TPTP_Input] #
Pretty TPTP_Input Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: TPTP_Input -> Doc # prettyList :: [TPTP_Input] -> Doc #
ToTPTP TPTP_Input Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: TPTP_Input -> ShowS Source #
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 #
(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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPTP_Input_ c -> r # gmapQ :: (forall d. Data d => d -> u) -> TPTP_Input_ c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TPTP_Input_ c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TPTP_Input_ c -> m (TPTP_Input_ c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP_Input_ c -> m (TPTP_Input_ c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP_Input_ c -> m (TPTP_Input_ c) #
Ord (c (Formula0 (T c) (F c))) => Ord (TPTP_Input_ c) Source #
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 #
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 #
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

Eq Annotations Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: Annotations -> Annotations -> Bool # (/=) :: Annotations -> Annotations -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annotations -> r # gmapQ :: (forall d. Data d => d -> u) -> Annotations -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Annotations -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations #
Ord Annotations Source #
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 #
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 #
Arbitrary Annotations Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen Annotations # shrink :: Annotations -> [Annotations] #
Pretty Annotations Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: Annotations -> Doc # prettyList :: [Annotations] -> Doc #
ToTPTP Annotations Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: Annotations -> ShowS Source #

data UsefulInfo Source #

Misc annotations

Constructors

NoUsefulInfo
UsefulInfo [GTerm]

Instances

Eq UsefulInfo Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: UsefulInfo -> UsefulInfo -> Bool # (/=) :: UsefulInfo -> UsefulInfo -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UsefulInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> UsefulInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UsefulInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UsefulInfo -> m UsefulInfo #
Ord UsefulInfo Source #
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 #
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 #
Arbitrary UsefulInfo Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen UsefulInfo # shrink :: UsefulInfo -> [UsefulInfo] #
Pretty UsefulInfo Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: UsefulInfo -> Doc # prettyList :: [UsefulInfo] -> Doc #
ToTPTP UsefulInfo Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: UsefulInfo -> ShowS Source #

newtype Role Source #

Formula roles

Constructors

Role
Fields unrole :: String

Instances

Eq Role Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: Role -> Role -> Bool # (/=) :: Role -> Role -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r # gmapQ :: (forall d. Data d => d -> u) -> Role -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role #
Ord Role Source #
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 #
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 #
Arbitrary Role Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen Role # shrink :: 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

Eq GData Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: GData -> GData -> Bool # (/=) :: GData -> GData -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GData -> r # gmapQ :: (forall d. Data d => d -> u) -> GData -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> GData -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> GData -> m GData # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GData -> m GData # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GData -> m GData #
Ord GData Source #
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 #
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 #
Arbitrary GData Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen GData # shrink :: GData -> [GData] #
Pretty GData Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: GData -> Doc # prettyList :: [GData] -> Doc #
ToTPTP GData Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: GData -> ShowS Source #

data GTerm Source #

Metadata (the general_term rule in TPTP's grammar)

Constructors

ColonSep GData GTerm
GTerm GData
GList [GTerm]

Instances

Eq GTerm Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: GTerm -> GTerm -> Bool # (/=) :: GTerm -> GTerm -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GTerm -> r # gmapQ :: (forall d. Data d => d -> u) -> GTerm -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> GTerm -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> GTerm -> m GTerm # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GTerm -> m GTerm # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GTerm -> m GTerm #
Ord GTerm Source #
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 #
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 #
Arbitrary GTerm Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen GTerm # shrink :: GTerm -> [GTerm] #
Pretty GTerm Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: GTerm -> Doc # prettyList :: [GTerm] -> Doc #
ToTPTP GTerm Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: GTerm -> ShowS 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

FreeVars Term Source #
Instance details Defined in Codec.TPTP.Base Methods freeVars :: Term -> Set V Source #
FreeVars Formula Source #
Instance details Defined in Codec.TPTP.Base Methods freeVars :: Formula -> 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

Eq AtomicWord Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: AtomicWord -> AtomicWord -> Bool # (/=) :: AtomicWord -> AtomicWord -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AtomicWord -> r # gmapQ :: (forall d. Data d => d -> u) -> AtomicWord -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AtomicWord -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord #
Ord AtomicWord Source #
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 #
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 #
IsString AtomicWord Source #
Instance details Defined in Codec.TPTP.Base Methods fromString :: String -> 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 #
Monoid AtomicWord Source #
Instance details Defined in Codec.TPTP.Base Methods mempty :: AtomicWord # mappend :: AtomicWord -> AtomicWord -> AtomicWord # mconcat :: [AtomicWord] -> AtomicWord #
Arbitrary AtomicWord Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen AtomicWord # shrink :: AtomicWord -> [AtomicWord] #
Pretty AtomicWord Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: AtomicWord -> Doc # prettyList :: [AtomicWord] -> Doc #
ToTPTP AtomicWord Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: AtomicWord -> ShowS Source #

newtype V Source #

Variable names

Constructors

V String

Instances

Eq V Source #
Instance details Defined in Codec.TPTP.Base Methods (==) :: V -> V -> Bool # (/=) :: V -> V -> Bool #
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r # gmapQ :: (forall d. Data d => d -> u) -> V -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> V -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> V -> m V # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> V -> m V # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> V -> m V #
Ord V Source #
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 #
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 #
IsString V Source #
Instance details Defined in Codec.TPTP.Base Methods fromString :: String -> 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 #
Monoid V Source #
Instance details Defined in Codec.TPTP.Base Methods mempty :: V # mappend :: V -> V -> V # mconcat :: [V] -> V #
Arbitrary V Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen V # shrink :: V -> [V] #
Pretty V Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: V -> Doc # prettyList :: [V] -> Doc #
ToTPTP V Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: V -> ShowS Source #

Fixed-point style decorated formulae and terms

newtype F c Source #

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

For example:

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

Constructors

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

Instances

Arbitrary Formula Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen Formula # shrink :: Formula -> [Formula] #
Pretty F0Diff Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: F0Diff -> Doc # prettyList :: [F0Diff] -> Doc #
FreeVars Formula Source #
Instance details Defined in Codec.TPTP.Base Methods freeVars :: Formula -> Set V Source #
Diffable Formula (F DiffResult) Source #
Instance details Defined in Codec.TPTP.Diff Methods diff :: Formula -> Formula -> F DiffResult Source #
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 #
(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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> F c -> r # gmapQ :: (forall d. Data d => d -> u) -> F c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> F c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> F c -> m (F c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> F c -> m (F c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> F c -> m (F c) #
Ord (c (Formula0 (T c) (F c))) => Ord (F c) Source #
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 #
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 (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 #
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 #
Pretty (F Identity) Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: F Identity -> Doc # prettyList :: [F Identity] -> Doc #
Pretty (F DiffResult) Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: F DiffResult -> Doc # prettyList :: [F DiffResult] -> Doc #
Pretty (WithEnclosing (F DiffResult)) Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: WithEnclosing (F DiffResult) -> Doc # prettyList :: [WithEnclosing (F DiffResult)] -> Doc #
Pretty (WithEnclosing Formula) Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: WithEnclosing Formula -> Doc # prettyList :: [WithEnclosing Formula] -> Doc #
Pretty (WithEnclosing F0Diff) Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: WithEnclosing F0Diff -> Doc # prettyList :: [WithEnclosing F0Diff] -> Doc #
ToTPTP (F Identity) Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: F Identity -> ShowS Source #
Pretty (Formula0 Term Formula) Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: Formula0 Term Formula -> Doc # prettyList :: [Formula0 Term Formula] -> Doc #

newtype T c Source #

Terms whose subterms are wrapped in the given type constructor c

Constructors

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

Instances

Arbitrary Term Source #
Instance details Defined in Codec.TPTP.Base Methods arbitrary :: Gen Term # shrink :: Term -> [Term] #
Pretty F0Diff Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: F0Diff -> Doc # prettyList :: [F0Diff] -> Doc #
Pretty T0Diff Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: T0Diff -> Doc # prettyList :: [T0Diff] -> Doc #
FreeVars Term Source #
Instance details Defined in Codec.TPTP.Base Methods freeVars :: Term -> Set V Source #
Diffable Term (T DiffResult) Source #
Instance details Defined in Codec.TPTP.Diff Methods diff :: Term -> Term -> T DiffResult Source #
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 #
(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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T c -> r # gmapQ :: (forall d. Data d => d -> u) -> T c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> T c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> T c -> m (T c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> T c -> m (T c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> T c -> m (T c) #
Ord (c (Term0 (T c))) => Ord (T c) Source #
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 #
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 (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 #
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 #
Pretty (T Identity) Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: T Identity -> Doc # prettyList :: [T Identity] -> Doc #
Pretty (T DiffResult) Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: T DiffResult -> Doc # prettyList :: [T DiffResult] -> Doc #
Pretty (Term0 Term) Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: Term0 Term -> Doc # prettyList :: [Term0 Term] -> Doc #
Pretty (WithEnclosing (T DiffResult)) Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: WithEnclosing (T DiffResult) -> Doc # prettyList :: [WithEnclosing (T DiffResult)] -> Doc #
Pretty (WithEnclosing Term) Source #
Instance details Defined in Codec.TPTP.Pretty Methods pretty :: WithEnclosing Term -> Doc # prettyList :: [WithEnclosing Term] -> Doc #
Pretty (WithEnclosing F0Diff) Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: WithEnclosing F0Diff -> Doc # prettyList :: [WithEnclosing F0Diff] -> Doc #
Pretty (WithEnclosing T0Diff) Source #
Instance details Defined in Codec.TPTP.Diff Methods pretty :: WithEnclosing T0Diff -> Doc # prettyList :: [WithEnclosing T0Diff] -> Doc #
ToTPTP (T Identity) Source #
Instance details Defined in Codec.TPTP.Export Methods toTPTP :: T Identity -> ShowS Source #
Pretty (Formula0 Term Formula) Source #
Instance details 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) 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