Codec.TPTP.Base

Contents

Synopsis

Basic undecorated formulae and terms

type Formula = F Identity Source

Basic (undecorated) first-order formulae

type Term = T Identity Source

Basic (undecorated) terms

Formulae and terms decoreated with state

type FormulaST s = F (State s)Source

First-order formulae decorated with state

type TermST s = T (State s)Source

Terms decorated with state

type FormulaC = FormulaST [String]Source

First-order formulae decorated with comments

type TermC = TermST [String]Source

Terms decorated with comments

forgetFC :: FormulaC -> Formula Source

Forget comments in formulae decoreated with comments

forgetTC :: TermC -> Term Source

Forget comments in terms decoreated with comments

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

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 V	Variable
NumberLitTerm Double	Number literal
DistinctObjectTerm String	Double-quoted item
FunApp AtomicWord [term]	Function symbol application (constants are encoded as nullary functions)

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)
Pretty (WithEnclosing t) => Pretty (WithEnclosing (Term0 t))
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
Fields runF :: c (Formula0 (T c) (F c))

Instances

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)

newtype T c Source

Terms whose subterms are wrapped in the given type constructor c

Constructors

T
Fields runT :: c (Term0 (T c))

Instances

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)

data BinOp Source

Binary formula connectives

Constructors

:<=>:	Equivalence
:=>:	Implication
:<=:	Reverse Implication
:&:	AND
:\|:	OR
:~&:	NAND
:~\|:	NOR
:<~>:	XOR

Instances

Bounded BinOp
Enum BinOp
Eq BinOp
Data BinOp
Ord BinOp
Read BinOp
Show BinOp
Typeable BinOp
Arbitrary BinOp
Pretty BinOp
ToTPTP BinOp

data InfixPred Source

Term -> Term -> Formula infix connectives

Constructors

:=:
:!=:

Instances

Bounded InfixPred
Enum InfixPred
Eq InfixPred
Data InfixPred
Ord InfixPred
Read InfixPred
Show InfixPred
Typeable InfixPred
Arbitrary InfixPred
Pretty InfixPred
ToTPTP InfixPred

data Quant Source

Quantifier specification

Constructors

All
Exists

Instances

Bounded Quant
Enum Quant
Eq Quant
Data Quant
Ord Quant
Read Quant
Show Quant
Typeable Quant
Arbitrary Quant
Pretty Quant
ToTPTP Quant

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

data TPTP_Input_ c Source

generalized TPTP_Input -- problem deriving Data and Typable instance TODO other than that backward compatible

Constructors

AFormula	Annotated formulae
Fields name :: AtomicWord role :: Role formula :: F c annotations :: Annotations
Comment String
Include FilePath [AtomicWord]

Instances

Eq (c (Formula0 (T c) (F c))) => Eq (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)

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

data Role Source

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

Constructors

Role
Fields unrole :: String

Instances

Eq Role
Data Role
Ord Role
Read Role
Show Role
Typeable Role
Arbitrary Role
ToTPTP Role

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

Instances

Eq GData
Data GData
Ord GData
Read GData
Show GData
Typeable GData
Arbitrary GData
Pretty GData
ToTPTP GData

data GTerm Source

Metadata (the general_term rule in TPTP's grammar)

Constructors

ColonSep GData GTerm
GTerm GData
GList [GTerm]

Instances

Eq GTerm
Data GTerm
Ord GTerm
Read GTerm
Show GTerm
Typeable GTerm
Arbitrary GTerm
Pretty GTerm
ToTPTP GTerm

Gathering free Variables

class FreeVars a whereSource

Methods

freeVars :: a -> Set V Source

Obtain the free variables from a formula or term

Instances

FreeVars Term
FreeVars Formula

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

Constructors

AtomicWord String

newtype V Source

Variable names

Constructors

V String

Instances

Eq V
Data V
Ord V
Read V
Show V
Typeable V
IsString V
Arbitrary V
Pretty V
Monoid V
ToTPTP V

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

Instances

Monad m => Pointed a (m 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

Instances

Copointed a (Identity a)

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

foldF Source

Arguments

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

foldT Source

Arguments

:: Copointed (Term0 (T t)) (t (Term0 (T t)))
=> (String -> r)	Handle string literal
-> (Double -> r)	Handle number literal
-> (V -> r)	Handle variable
-> (AtomicWord -> [T t] -> r)	Handle function symbol application
-> T t -> r	Handle term

Eliminate terms

Eq AtomicWord
Data AtomicWord
Ord AtomicWord
Read AtomicWord
Show AtomicWord
Typeable AtomicWord
IsString AtomicWord
Arbitrary AtomicWord
Pretty AtomicWord
Monoid AtomicWord
ToTPTP AtomicWord