Codec.TPTP.Base

Basic undecorated formulae and terms

type Formula = F Identity

Basic (undecorated) first-order formulae

type Term = T Identity

Basic (undecorated) terms

Formulae and terms decorated with state

type FormulaST s = F (State s)

First-order formulae decorated with state

type TermST s = T (State s)

Terms decorated with state

type FormulaC = FormulaST [String]

First-order formulae decorated with comments

type TermC = TermST [String]

Terms decorated with comments

forgetFC :: FormulaC -> Formula

Forget comments in formulae decorated with comments

forgetTC :: TermC -> Term

Forget comments in terms decorated with comments

(.<=>.) :: Pointed c => F c -> F c -> F c

Equivalence

Important special case:

(.<=>.) :: Formula -> Formula -> Formula

(.=>.) :: Pointed c => F c -> F c -> F c

Implication

(.<=.) :: Pointed c => F c -> F c -> F c

Reverse implication

(.|.) :: Pointed c => F c -> F c -> F c

Disjunction/OR

(.&.) :: Pointed c => F c -> F c -> F c

Conjunction/AND

(.<~>.) :: Pointed c => F c -> F c -> F c

XOR

(.~|.) :: Pointed c => F c -> F c -> F c

NOR

(.~&.) :: Pointed c => F c -> F c -> F c

NAND

(.~.) :: Pointed c => F c -> F c

Negation

(.=.) :: Pointed c => T c -> T c -> F c

Equality

(.!=.) :: Pointed c => T c -> T c -> F c

Inequality

for_all :: Pointed c => [V] -> F c -> F c

Universal quantification

exists :: Pointed c => [V] -> F c -> F c

Existential quantification

pApp :: Pointed c => AtomicWord -> [T c] -> F c

Predicate symbol application

var :: Pointed c => V -> T c

Variable

fApp :: Pointed c => AtomicWord -> [T c] -> T c

Function symbol application (constants are encoded as nullary functions)

numberLitTerm :: Pointed c => Rational -> T c

Number literal

distinctObjectTerm :: Pointed c => String -> T c

Double-quoted string literal, called Distinct Object in TPTP's grammar

General decorated formulae and terms

data Formula0 term formula

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)

data Term0 term

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)

data BinOp

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

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

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

A line of a TPTP file: Annotated formula, comment or include statement.

type TPTP_Input_C = TPTP_Input_ (State [String])

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

Forget comments in a line of a TPTP file decorated with comments

data TPTP_Input_ c

Generalized TPTP_Input

Constructors

AFormula

Annotated formulae

Fields

name :: AtomicWord

role :: Role

formula :: F c

annotations :: Annotations

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

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

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

newtype Role

Formula roles

Constructors

Role

Fields

unrole :: String

Instances

Eq Role

Data Role

Ord Role

Read Role

Show Role

Typeable Role

Arbitrary Role

ToTPTP Role

data GData

Metadata (the general_data rule in TPTP's grammar)

Constructors

GWord AtomicWord

GApp AtomicWord [GTerm]

GVar V

GNumber Rational

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

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 where

Methods

freeVars :: a -> Set V

Obtain the free variables from a formula or term

Instances

FreeVars Term

FreeVars Formula

univquant_free_vars :: Formula -> Formula

Universally quantify all free variables in the formula

newtype AtomicWord

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

newtype V

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

newtype F c

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

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)

newtype T c

Terms whose subterms are wrapped in the given type constructor c

Constructors

T

Fields

runT :: c (Term0 (T 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

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

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

foldT

Arguments

:: Copointed t

=> (String -> r)

Handle string literal

-> (Rational -> r)

Handle number literal

-> (V -> r)

Handle variable

-> (AtomicWord -> [T t] -> r)

Handle function symbol application

-> T t -> r

Handle term

Eliminate terms