- 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 (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
- data Term0 term
- = Var V
- | NumberLitTerm Double
- | DistinctObjectTerm String
- | FunApp AtomicWord [term]

- newtype F c = F {}
- newtype T c = T {}
- 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]

- data Role = Role {}
- data GData
- = GWord AtomicWord
- | GApp AtomicWord [GTerm]
- | GVar V
- | GNumber Double
- | GDistinctObject String
- | GFormulaData String Formula

- data GTerm
- class FreeVars a where
- 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

# Formulae and terms decoreated with state

(.=>.) :: 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))) => 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

fApp :: Pointed (Term0 (T c)) (c (Term0 (T c))) => AtomicWord -> [T c] -> T cSource

Function symbol application (constants are encoded as nullary functions)

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.

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 |

Typeable2 Formula0 | |

(Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty (WithEnclosing (Formula0 t f)) | |

(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.

Var V | Variable |

NumberLitTerm Double | Number literal |

DistinctObjectTerm String | Double-quoted item |

FunApp AtomicWord [term] | Function symbol application (constants are encoded as nullary functions) |

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) | |

Pretty (WithEnclosing t) => Pretty (WithEnclosing (Term0 t)) | |

ToTPTP t => ToTPTP (Term0 t) |

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

.

For example:

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)) | |

ToTPTP (F Identity) |

Terms whose subterms are wrapped in the given type constructor `c`

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 (WithEnclosing (T DiffResult)) | |

ToTPTP (T Identity) |

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 decoreated with comments

data TPTP_Input_ c Source

generalized TPTP_Input

AFormula | Annotated formulae |

- name :: AtomicWord
- role :: Role
- formula :: F c
- annotations :: Annotations
| |

Comment String | |

Include FilePath [AtomicWord] |

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) |

data Annotations Source

Annotations about the formulas origin

data UsefulInfo Source

Misc annotations

Formula roles -- why isn't this newtype??

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 -> 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_word*s).

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

# Utility functions

unwrapF :: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t))) => F t -> Formula0 (T t) (F 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

:: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F 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