Safe Haskell | None |
---|
Codec.TPTP.Base
Contents
- 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
- data Term0 term
- = Var V
- | NumberLitTerm Rational
- | DistinctObjectTerm String
- | FunApp AtomicWord [term]
- data BinOp
- data InfixPred
- data Quant
- 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]
- = AFormula {
- data Annotations
- 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
- data GTerm
- class FreeVars a where
- univquant_free_vars :: Formula -> Formula
- newtype AtomicWord = AtomicWord String
- newtype V = V String
- newtype F c = F {}
- newtype T c = T {}
- 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
Formulae and terms decorated with state
fApp :: Pointed c => AtomicWord -> [T c] -> T cSource
Function symbol application (constants are encoded as nullary functions)
numberLitTerm :: Pointed c => Rational -> T cSource
Number literal
distinctObjectTerm :: Pointed 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 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
Typeable2 Formula0 | |
Pretty F0Diff | |
(Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty (WithEnclosing (Formula0 t f)) | |
Pretty (WithEnclosing F0Diff) | |
(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) |
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
Typeable1 Term0 | |
Pretty T0Diff | |
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) | |
Pretty (WithEnclosing t) => Pretty (WithEnclosing (Term0 t)) | |
Pretty (WithEnclosing T0Diff) | |
ToTPTP t => ToTPTP (Term0 t) |
Binary formula connectives
Term -> Term -> Formula infix connectives
Quantifier specification
Formula Metadata
type TPTP_Input = TPTP_Input_ IdentitySource
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_InputSource
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
| |
Comment String | |
Include FilePath [AtomicWord] |
Instances
Arbitrary TPTP_Input | |
Pretty TPTP_Input | |
ToTPTP TPTP_Input | |
Eq (c (Formula0 (T c) (F c))) => Eq (TPTP_Input_ c) | |
(Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c) | |
Ord (c (Formula0 (T c) (F c))) => Ord (TPTP_Input_ c) | |
Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c) | |
Show (c (Formula0 (T c) (F c))) => Show (TPTP_Input_ c) | |
Typeable1 c => Typeable (TPTP_Input_ c) | |
ToTPTP [TPTP_Input] |
data Annotations Source
Annotations about the formulas origin
Constructors
NoAnnotations | |
Annotations GTerm UsefulInfo |
Instances
Eq Annotations | |
Data Annotations | |
Ord Annotations | |
Read Annotations | |
Show Annotations | |
Typeable Annotations | |
Arbitrary Annotations | |
Pretty Annotations | |
ToTPTP Annotations |
data UsefulInfo Source
Misc annotations
Constructors
NoUsefulInfo | |
UsefulInfo [GTerm] |
Instances
Eq UsefulInfo | |
Data UsefulInfo | |
Ord UsefulInfo | |
Read UsefulInfo | |
Show UsefulInfo | |
Typeable UsefulInfo | |
Arbitrary UsefulInfo | |
Pretty UsefulInfo | |
ToTPTP UsefulInfo |
Formula roles
Metadata (the general_data rule in TPTP's grammar)
Constructors
GWord AtomicWord | |
GApp AtomicWord [GTerm] | |
GVar V | |
GNumber Rational | |
GDistinctObject String | |
GFormulaData String Formula |
Metadata (the general_term rule in TPTP's grammar)
Gathering free Variables
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 |
Instances
Eq AtomicWord | |
Data AtomicWord | |
Ord AtomicWord | |
Read AtomicWord | |
Show AtomicWord | |
Typeable AtomicWord | |
IsString AtomicWord | |
Arbitrary AtomicWord | |
Pretty AtomicWord | |
Monoid AtomicWord | |
ToTPTP AtomicWord |
Variable names
Constructors
V String |
Fixed-point style decorated formulae and terms
Formulae whose subexpressions are wrapped in the given type constructor c
.
For example:
-
c =
: Plain formulaeIdentity
-
c =
: Formulae that may contain "holes"Maybe
-
c =
: (Mutable) formulae with mutable subexpressionsIORef
Instances
Arbitrary Formula | |
Pretty F0Diff | |
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) | |
Pretty (WithEnclosing (F DiffResult)) | |
Pretty (WithEnclosing Formula) | |
Pretty (WithEnclosing F0Diff) | |
ToTPTP (F Identity) | |
Pretty (Formula0 Term Formula) |
Terms whose subterms are wrapped in the given type constructor c
Instances
Arbitrary Term | |
Pretty F0Diff | |
Pretty T0Diff | |
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) | |
Pretty (Term0 Term) | |
Pretty (WithEnclosing (T DiffResult)) | |
Pretty (WithEnclosing Term) | |
Pretty (WithEnclosing F0Diff) | |
Pretty (WithEnclosing T0Diff) | |
ToTPTP (T Identity) | |
Pretty (Formula0 Term Formula) |
Utility functions
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) -> (Rational -> r) -> (V -> r) -> (AtomicWord -> [t] -> r) -> Term0 t -> rSource
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