Data.TPTP.Parse.Combinators

Whitespace

whitespace :: Parser ()

Consume white space and trailing comments.

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)

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

literal :: Parser Literal

Parse a literal.

clause :: Parser Clause

Parse a clause.

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.

Annotations

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.