logic-TPTP-0.4.0.0: Import, export etc. for TPTP, a syntax for first-order logic

Safe Haskell None

Codec.TPTP.Base

Synopsis

# Basic undecorated formulae and terms

Basic (undecorated) first-order formulae

type Term = T IdentitySource

Basic (undecorated) terms

# Formulae and terms decorated 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

First-order formulae decorated with comments

type TermC = TermST [String]Source

Terms decorated with comments

Forget comments in formulae decorated with comments

Forget comments in terms decorated with comments

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

Equivalence

Important special case:

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

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

Implication

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

Reverse implication

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

Disjunction/OR

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

Conjunction/AND

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

XOR

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

NOR

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

NAND

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

Negation

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

Equality

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

Inequality

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

Universal quantification

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

Existential quantification

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

Predicate symbol application

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

Variable

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

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)

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

 :=: :!=:

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

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

A line of a TPTP file: Annotated formula (with the comment string embbeded in the State monad ), comment or include statement

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

data TPTP_Input_ c Source

Generalized TPTP_Input

Constructors

 AFormula Annotated formulae Fieldsname :: 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]

Annotations about the formulas origin

Constructors

 NoAnnotations Annotations GTerm UsefulInfo

data UsefulInfo Source

Misc annotations

Constructors

 NoUsefulInfo UsefulInfo [GTerm]

newtype Role Source

Formula roles

Constructors

 Role Fieldsunrole :: 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 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 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 VSource

Obtain the free variables from a formula or term

Instances

 FreeVars Term FreeVars Formula

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

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

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

Constructors

 T FieldsrunT :: 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)Source

unwrapT :: Copointed 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) -> (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

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