Safe Haskell | None |
---|---|
Language | Haskell98 |
- 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 {}
- data GData
- 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 c Source #
Function symbol application (constants are encoded as nullary functions)
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.
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 |
Pretty F0Diff # | |
(Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty (WithEnclosing (Formula0 t f)) # | |
Pretty (WithEnclosing F0Diff) # | |
(Eq term, Eq formula) => Eq (Formula0 term formula) Source # | |
(Data formula, Data term) => Data (Formula0 term formula) Source # | |
(Ord term, Ord formula) => Ord (Formula0 term formula) Source # | |
(Read term, Read formula) => Read (Formula0 term formula) Source # | |
(Show term, Show formula) => Show (Formula0 term formula) Source # | |
(Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b) Source # | |
(ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f) 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.
Var V | Variable |
NumberLitTerm Rational | Number literal |
DistinctObjectTerm String | Double-quoted item |
FunApp AtomicWord [term] | Function symbol application (constants are encoded as nullary functions) |
Pretty T0Diff # | |
Eq term => Eq (Term0 term) Source # | |
Data term => Data (Term0 term) Source # | |
Ord term => Ord (Term0 term) Source # | |
Read term => Read (Term0 term) Source # | |
Show term => Show (Term0 term) Source # | |
Arbitrary a => Arbitrary (Term0 a) Source # | |
Pretty (WithEnclosing t) => Pretty (WithEnclosing (Term0 t)) # | |
Pretty (WithEnclosing T0Diff) # | |
ToTPTP t => ToTPTP (Term0 t) Source # | |
Binary formula connectives
Term -> Term -> Formula infix connectives
Quantifier specification
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
AFormula | Annotated formulae |
| |
Comment String | |
Include FilePath [AtomicWord] |
Arbitrary TPTP_Input Source # | |
ToTPTP TPTP_Input Source # | |
Eq (c (Formula0 (T c) (F c))) => Eq (TPTP_Input_ c) Source # | |
(Typeable (* -> *) c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c) Source # | |
Ord (c (Formula0 (T c) (F c))) => Ord (TPTP_Input_ c) Source # | |
Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c) Source # | |
Show (c (Formula0 (T c) (F c))) => Show (TPTP_Input_ c) Source # | |
ToTPTP [TPTP_Input] Source # | |
data Annotations Source #
Annotations about the formulas origin
data UsefulInfo Source #
Misc annotations
Formula roles
Metadata (the general_data rule in TPTP's grammar)
Metadata (the general_term rule in TPTP's grammar)
Gathering free Variables
univquant_free_vars :: Formula -> Formula Source #
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
Variable names
Fixed-point style decorated formulae and terms
Formulae whose subexpressions are wrapped in the given type constructor c
.
For example:
Arbitrary Formula Source # | |
Pretty F0Diff # | |
FreeVars Formula Source # | |
Diffable Formula (F DiffResult) Source # | |
Eq (c (Formula0 (T c) (F c))) => Eq (F c) Source # | |
(Typeable (* -> *) c, Data (c (Formula0 (T c) (F c)))) => Data (F c) Source # | |
Ord (c (Formula0 (T c) (F c))) => Ord (F c) Source # | |
Read (c (Formula0 (T c) (F c))) => Read (F c) Source # | |
Show (c (Formula0 (T c) (F c))) => Show (F c) Source # | |
Show (F DiffResult) # | |
Pretty (F DiffResult) # | |
Pretty (WithEnclosing (F DiffResult)) # | |
Pretty (WithEnclosing Formula) # | |
Pretty (WithEnclosing F0Diff) # | |
ToTPTP (F Identity) Source # | |
Terms whose subterms are wrapped in the given type constructor c
Arbitrary Term Source # | |
Pretty F0Diff # | |
Pretty T0Diff # | |
FreeVars Term Source # | |
Diffable Term (T DiffResult) Source # | |
Eq (c (Term0 (T c))) => Eq (T c) Source # | |
(Typeable (* -> *) c, Data (c (Term0 (T c)))) => Data (T c) Source # | |
Ord (c (Term0 (T c))) => Ord (T c) Source # | |
Read (c (Term0 (T c))) => Read (T c) Source # | |
Show (c (Term0 (T c))) => Show (T c) Source # | |
Show (T DiffResult) # | |
Pretty (T DiffResult) # | |
Pretty (WithEnclosing (T DiffResult)) # | |
Pretty (WithEnclosing Term) # | |
Pretty (WithEnclosing F0Diff) # | |
Pretty (WithEnclosing T0Diff) # | |
ToTPTP (T Identity) Source # | |
Utility functions
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 #
:: 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