Data.TPTP.Parse.Combinators

Whitespace

skipWhitespace :: Parser ()

Consume white space and trailing comments.

input :: Parser a -> Parser a

input runs a given parser skipping leading whitespace. The function succeeds if the parser consumes the entire input.

Names

atom :: Parser Atom

Parse an atomic word. Single-quoted atoms are parsed without the single quotes and with the characters ' and \ unescaped.

var :: Parser Var

Parse a variable.

distinctObject :: Parser DistinctObject

Parse a distinct object. Double quotes are not preserved and the characters ' and \ are unescaped.

function :: Parser (Name Function)

Parse a function name.

predicate :: Parser (Name Predicate)

Parse a predicate name.

Sorts and types

sort :: Parser (Name Sort)

Parse a sort.

tff1Sort :: Parser TFF1Sort

Parse a sort in sorted polymorphic logic.

type_ :: Parser Type

Parse a type.

First-order logic

number :: Parser Number

Parse a number.

term :: Parser Term

Parse a term.

term supports parsing superfluous parenthesis around arguments of the function application, which are not present in the TPTP grammar.

literal :: Parser Literal

Parse a literal.

literal supports parsing superfluous parenthesis around arguments of the predicate application, which are not present in the TPTP grammar.

clause :: Parser Clause

Parse a clause.

clause supports parsing superfluous parenthesis around any of the subclauses of the clause, which are not present in the TPTP grammar.

unsortedFirstOrder :: Parser UnsortedFirstOrder

Parse a formula in unsorted first-order logic.

sortedFirstOrder :: Parser SortedFirstOrder

An alias for monomorphicFirstOrder.

monomorphicFirstOrder :: Parser MonomorphicFirstOrder

Parse a formula in sorted monomorphic first-order logic.

polymorphicFirstOrder :: Parser PolymorphicFirstOrder

Parse a formula in sorted polymorphic first-order logic.

Units

unit :: Parser Unit

Parse a TPTP unit.

tptp :: Parser TPTP

Parse a TPTP input.

tstp :: Parser TSTP

Parse a TSTP input.

Annotations

szs :: Parser SZS

Parse the SZS ontology information of a TSTP output inside a comment.

intro :: Parser Intro

Parse an introduction marking.

parent :: Parser Parent

Parse a parent.

source :: Parser Source

Parse the source of a unit.

info :: Parser Info

Parse a unit of information about a formula.

Orphan instances

Semigroup SZS

Methods

(<>) :: SZS -> SZS -> SZS

sconcat :: NonEmpty SZS -> SZS

stimes :: Integral b => b -> SZS -> SZS

Monoid SZS

Methods

mempty :: SZS

mappend :: SZS -> SZS -> SZS

mconcat :: [SZS] -> SZS