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

Codec.TPTP.Base

Synopsis

# Basic undecorated formulae and terms

Basic (undecorated) first-order formulae

type Term = T IdentitySource

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 TermC = TermST [String]Source

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

 :=: :!=:

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

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

 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)

Constructors

 NoAnnotations Annotations GTerm UsefulInfo

data UsefulInfo Source

Misc annotations

Constructors

 NoUsefulInfo UsefulInfo [GTerm]

data Role Source

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

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

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

 Ord a => Pointed a (Set a) 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

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

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