logic-TPTP-0.2.0: Import, export etc. for TPTP, a syntax for first-order logicSource codeContentsIndex
Codec.TPTP.Base
Contents
Basic undecorated formulae and terms
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
(.<=>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F c
(.=>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F c
(.<=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F c
(.|.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F c
(.&.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F c
(.<~>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F c
(.~|.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F c
(.~&.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F c
(.~.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c
(.=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => T c -> T c -> F c
(.!=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => T c -> T c -> F c
for_all :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => [V] -> F c -> F c
exists :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => [V] -> F c -> F c
pApp :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => AtomicWord -> [T c] -> F c
var :: Pointed (Term0 (T c)) (c (Term0 (T c))) => V -> T c
fApp :: Pointed (Term0 (T c)) (c (Term0 (T c))) => AtomicWord -> [T c] -> T c
numberLitTerm :: Pointed (Term0 (T c)) (c (Term0 (T c))) => Double -> T c
distinctObjectTerm :: Pointed (Term0 (T c)) (c (Term0 (T 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 Double
| DistinctObjectTerm String
| FunApp AtomicWord [term]
newtype F c = F {
runF :: c (Formula0 (T c) (F c))
}
newtype T c = T {
runT :: c (Term0 (T c))
}
data BinOp
= :<=>:
| :=>:
| :<=:
| :&:
| :|:
| :~&:
| :~|:
| :<~>:
data InfixPred
= :=:
| :!=:
data Quant
= All
| Exists
data TPTP_Input
= AFormula {
name :: AtomicWord
role :: Role
formula :: Formula
annotations :: Annotations
}
| Comment String
| Include FilePath [AtomicWord]
data Annotations
= NoAnnotations
| Annotations GTerm UsefulInfo
data UsefulInfo
= NoUsefulInfo
| UsefulInfo [GTerm]
data Role = Role {
unrole :: String
}
data GData
= GWord AtomicWord
| GApp AtomicWord [GTerm]
| GVar V
| GNumber Double
| GDistinctObject String
| GFormulaData String Formula
data GTerm
= ColonSep GData GTerm
| GTerm GData
| GList [GTerm]
class FreeVars a where
freeVars :: a -> Set V
univquant_free_vars :: Formula -> Formula
newtype AtomicWord = AtomicWord String
newtype V = V String
class Pointed a b | b -> a where
point :: a -> b
class Copointed a b | b -> a where
copoint :: b -> a
unwrapF :: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t))) => F t -> Formula0 (T t) (F t)
unwrapT :: Copointed (Term0 (T t)) (t (Term0 (T 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) -> (Double -> r) -> (V -> r) -> (AtomicWord -> [t] -> r) -> Term0 t -> r
foldF :: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F 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 (Term0 (T t)) (t (Term0 (T t))) => (String -> r) -> (Double -> r) -> (V -> r) -> (AtomicWord -> [T t] -> r) -> T t -> r
Basic undecorated formulae and terms
type Formula = F IdentitySource
Basic (undecorated) first-order formulae
type Term = T IdentitySource
Basic (undecorated) terms
(.<=>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource

Equivalence

Don't let the type context of these wrapper function confuse you :) -- the important special case is just: 

(.<=>.) :: Formula -> Formula -> Formula
(.=>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource
Implication
(.<=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource
Reverse implication
(.|.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource
Disjunction/OR
(.&.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource
Conjunction/AND
(.<~>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource
XOR
(.~|.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource
NOR
(.~&.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource
NAND
(.~.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F cSource
Negation
(.=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => T c -> T c -> F cSource
Equality
(.!=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => T c -> T c -> F cSource
Inequality
for_all :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => [V] -> F c -> F cSource
Universal quantification
exists :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => [V] -> F c -> F cSource
Existential quantification
pApp :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => AtomicWord -> [T c] -> F cSource
Predicate symbol application
var :: Pointed (Term0 (T c)) (c (Term0 (T c))) => V -> T cSource
Variable
fApp :: Pointed (Term0 (T c)) (c (Term0 (T c))) => AtomicWord -> [T c] -> T cSource
Function symbol application (constants are encoded as nullary functions)
numberLitTerm :: Pointed (Term0 (T c)) (c (Term0 (T c))) => Double -> T cSource
Number literal
distinctObjectTerm :: Pointed (Term0 (T c)) (c (Term0 (T c))) => String -> T cSource
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 formulaBinary connective application
InfixPred term InfixPred termInfix predicate application (equalities, inequalities)
PredApp AtomicWord [term]Predicate application
Quant Quant [V] formulaQuantified formula
:~: formulaNegation
show/hide Instances
Typeable2 Formula0
(Eq term, Eq formula) => Eq (Formula0 term formula)
(Data term, Data formula) => Data (Formula0 term formula)
(Ord term, Ord formula) => Ord (Formula0 term formula)
(Read term, Read formula) => Read (Formula0 term formula)
(Show term, Show formula) => Show (Formula0 term formula)
(Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b)
Pretty (Formula0 Term Formula)
(ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f)
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 VVariable
NumberLitTerm DoubleNumber literal
DistinctObjectTerm StringDouble-quoted item
FunApp AtomicWord [term]Function symbol application (constants are encoded as nullary functions)
show/hide Instances
Typeable1 Term0
Eq term => Eq (Term0 term)
Data term => Data (Term0 term)
Ord term => Ord (Term0 term)
Read term => Read (Term0 term)
Show term => Show (Term0 term)
Arbitrary a => Arbitrary (Term0 a)
Pretty (Term0 Term)
ToTPTP t => ToTPTP (Term0 t)
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
runF :: c (Formula0 (T c) (F c))
show/hide Instances
Arbitrary Formula
FreeVars Formula
Diffable Formula (F DiffResult)
Eq (c (Formula0 (T c) (F c))) => Eq (F c)
(Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (F c)
Ord (c (Formula0 (T c) (F c))) => Ord (F c)
Read (c (Formula0 (T c) (F c))) => Read (F c)
Show (c (Formula0 (T c) (F c))) => Show (F c)
Show (F DiffResult)
Typeable1 c => Typeable (F c)
Pretty (F Identity)
Pretty (F DiffResult)
ToTPTP (F Identity)
newtype T c Source
Terms whose subterms are wrapped in the given type constructor c
Constructors
T
runT :: c (Term0 (T c))
show/hide Instances
Arbitrary Term
FreeVars Term
Diffable Term (T DiffResult)
Eq (c (Term0 (T c))) => Eq (T c)
(Typeable1 c, Data (c (Term0 (T c)))) => Data (T c)
Ord (c (Term0 (T c))) => Ord (T c)
Read (c (Term0 (T c))) => Read (T c)
Show (c (Term0 (T c))) => Show (T c)
Show (T DiffResult)
Typeable1 c => Typeable (T c)
Pretty (T Identity)
Pretty (T DiffResult)
ToTPTP (T Identity)
data BinOp Source
Binary formula connectives
Constructors
:<=>:Equivalence
:=>:Implication
:<=:Reverse Implication
:&:AND
:|:OR
:~&:NAND
:~|:NOR
:<~>:XOR
show/hide Instances
data InfixPred Source
Term -> Term -> Formula infix connectives
Constructors
:=:
:!=:
show/hide Instances
data Quant Source
Quantifier specification
Constructors
All
Exists
show/hide Instances
Formula Metadata
data TPTP_Input Source
A line of a TPTP file: Annotated formula, comment or include statement.
Constructors
AFormulaAnnotated formulae
name :: AtomicWord
role :: Role
formula :: Formula
annotations :: Annotations
Comment String
Include FilePath [AtomicWord]
show/hide Instances
data Annotations Source
Annotations about the formulas origin
Constructors
NoAnnotations
Annotations GTerm UsefulInfo
show/hide Instances
data UsefulInfo Source
Misc annotations
Constructors
NoUsefulInfo
UsefulInfo [GTerm]
show/hide Instances
data Role Source
Formula roles
Constructors
Role
unrole :: String
show/hide Instances
data GData Source
Metadata (the general_data rule in TPTP's grammar)
Constructors
GWord AtomicWord
GApp AtomicWord [GTerm]
GVar V
GNumber Double
GDistinctObject String
GFormulaData String Formula
show/hide Instances
data GTerm Source
Metadata (the general_term rule in TPTP's grammar)
Constructors
ColonSep GData GTerm
GTerm GData
GList [GTerm]
show/hide Instances
Gathering free Variables
class FreeVars a whereSource
Methods
freeVars :: a -> Set VSource
Obtain the free variables from a formula or term
show/hide Instances
univquant_free_vars :: Formula -> FormulaSource
Universally quantify all free variables in the formula
newtype AtomicWord Source

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

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

Constructors
AtomicWord String
show/hide Instances
newtype V Source
Variable names
Constructors
V String
show/hide Instances
Fixed-point style decorated formulae and terms
class Pointed a b | b -> a whereSource

This class is used in several utility functions involving F and T.

Conceptually point should be of type a -> m a, but we need the extra flexibility to make restricted monads like Set instances.

Note: We have instance (Monad m) => Pointed a (m a), but Haddock currently doesn't display this.

Methods
point :: a -> bSource
show/hide Instances
Ord a => Pointed a (Set a)
class Copointed a b | b -> a whereSource

This class is used in several utility functions involving F and T.

Conceptually copoint should be of type w a -> a, but let's keep the extra flexibility.

Methods
copoint :: b -> aSource
show/hide Instances
Utility functions
unwrapF :: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t))) => F t -> Formula0 (T t) (F t)Source
unwrapT :: Copointed (Term0 (T t)) (t (Term0 (T 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 -> rSource
foldTerm0 :: (String -> r) -> (Double -> r) -> (V -> r) -> (AtomicWord -> [t] -> r) -> Term0 t -> rSource
foldFSource
:: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t)))
=> F t -> rHandle negation
-> Quant -> [V] -> F t -> rHandle quantification
-> F t -> BinOp -> F t -> rHandle binary op
-> T t -> InfixPred -> T t -> rHandle equality/inequality
-> AtomicWord -> [T t] -> rHandle predicate symbol application
-> F t -> rHandle formula
Eliminate formulae
foldTSource
:: Copointed (Term0 (T t)) (t (Term0 (T t)))
=> String -> rHandle string literal
-> Double -> rHandle number literal
-> V -> rHandle variable
-> AtomicWord -> [T t] -> rHandle function symbol application
-> T t -> rHandle term
Eliminate terms
Produced by Haddock version 2.4.2