logic-TPTP-0.1: Import, export and other utilities 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
Internal
Fixed-point style decorated formulae and terms
Synopsis
newtype Formula = FF (Formula0 Term Formula)
newtype Term = TT (Term0 Term)
(.<=>.) :: Formula -> Formula -> Formula
(.<~>.) :: Formula -> Formula -> Formula
(.=>.) :: Formula -> Formula -> Formula
(.<=.) :: Formula -> Formula -> Formula
(.~|.) :: Formula -> Formula -> Formula
(.|.) :: Formula -> Formula -> Formula
(.~&.) :: Formula -> Formula -> Formula
(.&.) :: Formula -> Formula -> Formula
(.~.) :: Formula -> Formula
(.=.) :: Term -> Term -> Formula
(.!=.) :: Term -> Term -> Formula
for_all :: [String] -> Formula -> Formula
exists :: [String] -> Formula -> Formula
pApp :: AtomicWord -> [Term] -> Formula
var :: String -> Term
fApp :: AtomicWord -> [Term] -> Term
numberLitTerm :: Double -> Term
distinctObjectTerm :: String -> Term
data Formula0 term formula
= BinOp formula BinOp formula
| InfixPred term InfixPred term
| PredApp AtomicWord [term]
| Quant Quant [String] formula
| :~: formula
data Term0 term
= Var String
| NumberLitTerm Double
| DistinctObjectTerm String
| FunApp AtomicWord [term]
data BinOp
= :<=>:
| :=>:
| :<=:
| :&:
| :|:
| :~&:
| :~|:
| :<~>:
data InfixPred
= :=:
| :!=:
data Quant
= All
| Exists
data TPTP_Input
= AFormula {
name :: AtomicWord
role :: Role
formula :: Formula
sourceInfo :: SourceInfo
usefulInfo :: UsefulInfo
}
| Comment String
| Include FilePath [AtomicWord]
data SourceInfo
= NoSourceInfo
| SourceInfo GTerm
data UsefulInfo
= NoUsefulInfo
| UsefulInfo [GTerm]
data Role = Role {
unrole :: String
}
data GData
= GWord AtomicWord
| GApp AtomicWord [GTerm]
| GVar String
| GNumber Double
| GDistinctObject String
| GFormulaData String Formula
data GTerm
= ColonSep GData GTerm
| GTerm GData
| GList [GTerm]
class FormulaOrTerm a where
elimFormulaOrTerm :: (Formula -> r) -> (Term -> r) -> a -> r
free_vars :: forall a. FormulaOrTerm a => a -> Set String
univquant_free_vars :: Formula -> Formula
free_vars0 :: Data d => d -> Set String
newtype AtomicWord = AtomicWord String
newtype TermFix f = TermFix {
runTermFix :: f (Term0 (TermFix f))
}
newtype FormulaFix f = FormulaFix {
runFormulaFix :: f (Formula0 (TermFix f) (FormulaFix f))
}
Basic undecorated formulae and terms
newtype Formula Source
Basic (undecorated) first-order formulae
Constructors
FF (Formula0 Term Formula)
show/hide Instances
newtype Term Source
Basic (undecorated) terms
Constructors
TT (Term0 Term)
show/hide Instances
(.<=>.) :: Formula -> Formula -> FormulaSource
(.<~>.) :: Formula -> Formula -> FormulaSource
(.=>.) :: Formula -> Formula -> FormulaSource
(.<=.) :: Formula -> Formula -> FormulaSource
(.~|.) :: Formula -> Formula -> FormulaSource
(.|.) :: Formula -> Formula -> FormulaSource
(.~&.) :: Formula -> Formula -> FormulaSource
(.&.) :: Formula -> Formula -> FormulaSource
(.~.) :: Formula -> FormulaSource
(.=.) :: Term -> Term -> FormulaSource
(.!=.) :: Term -> Term -> FormulaSource
for_all :: [String] -> Formula -> FormulaSource
exists :: [String] -> Formula -> FormulaSource
pApp :: AtomicWord -> [Term] -> FormulaSource
var :: String -> TermSource
fApp :: AtomicWord -> [Term] -> TermSource
numberLitTerm :: Double -> TermSource
distinctObjectTerm :: String -> TermSource
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). 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 [String] 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 StringVariable
NumberLitTerm DoubleNumber literal
DistinctObjectTerm StringDouble-quoted item
FunApp AtomicWord [term]Function symbol application (constants are 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)
data BinOp Source
Binary formula connectives
Constructors
:<=>:Equivalence
:=>:Implication
:<=:Implication (reverse)
:&: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
sourceInfo :: SourceInfo
usefulInfo :: UsefulInfo
Comment String
Include FilePath [AtomicWord]
show/hide Instances
data SourceInfo Source
Annotations about the formulas origin
Constructors
NoSourceInfo
SourceInfo GTerm
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 String
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 FormulaOrTerm a whereSource
Methods
elimFormulaOrTerm :: (Formula -> r) -> (Term -> r) -> a -> rSource
show/hide Instances
free_vars :: forall a. FormulaOrTerm a => a -> Set StringSource
Get the free variables
univquant_free_vars :: Formula -> FormulaSource
Universally quantify all free variables in the formula
Internal
free_vars0 :: Data d => d -> Set StringSource
newtype AtomicWord Source
Tip: Use the -XOverloadedStrings compiler flag if you don't want to type AtomicWord to construct an AtomicWord
Constructors
AtomicWord String
show/hide Instances
Fixed-point style decorated formulae and terms
newtype TermFix f Source

For a given type constructor f, make the fixed point type Y satisfying: 

 Y = f (Term0 Y)

(modulo newtype wrapping). See for example diffFormula.

Constructors
TermFix
runTermFix :: f (Term0 (TermFix f))
show/hide Instances
newtype FormulaFix f Source

For a given type constructor f, make the fixed point type X satisfying: 

 X = f (Formula0 Y X) 
 Y = f (Term0 Y)

(modulo newtype wrapping). See for example diffTerm.

Constructors
FormulaFix
runFormulaFix :: f (Formula0 (TermFix f) (FormulaFix f))
show/hide Instances
Produced by Haddock version 2.4.2