tptp-0.1.1.0: A parser and a pretty printer for the TPTP language

Copyright(c) Evgenii Kotelnikov 2019
LicenseGPL-3
Maintainerevgeny.kotelnikov@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.TPTP.Parse.Combinators

Contents

Description

 
Synopsis

Whitespace

skipWhitespace :: Parser () Source #

Consume white space and trailing comments.

input :: Parser a -> Parser a Source #

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

Names

atom :: Parser Atom Source #

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

var :: Parser Var Source #

Parse a variable.

distinctObject :: Parser DistinctObject Source #

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

function :: Parser (Name Function) Source #

Parse a function name.

predicate :: Parser (Name Predicate) Source #

Parse a predicate name.

Sorts and types

sort :: Parser (Name Sort) Source #

Parse a sort.

tff1Sort :: Parser TFF1Sort Source #

Parse a sort in sorted polymorphic logic.

type_ :: Parser Type Source #

Parse a type.

First-order logic

number :: Parser Number Source #

Parse a number.

term :: Parser Term Source #

Parse a term.

literal :: Parser Literal Source #

Parse a literal.

clause :: Parser Clause Source #

Parse a clause.

unsortedFirstOrder :: Parser UnsortedFirstOrder Source #

Parse a formula in unsorted first-order logic.

monomorphicFirstOrder :: Parser MonomorphicFirstOrder Source #

Parse a formula in sorted monomorphic first-order logic.

polymorphicFirstOrder :: Parser PolymorphicFirstOrder Source #

Parse a formula in sorted polymorphic first-order logic.

Units

unit :: Parser Unit Source #

Parse a TPTP unit.

tptp :: Parser TPTP Source #

Parse a TPTP input.

tstp :: Parser TSTP Source #

Parse a TSTP input.

Annotations

szs :: Parser SZS Source #

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

intro :: Parser Intro Source #

Parse an introduction marking.

parent :: Parser Parent Source #

Parse a parent.

source :: Parser Source Source #

Parse the source of a unit.

info :: Parser Info Source #

Parse a unit of information about a formula.

Orphan instances

Semigroup SZS Source # 
Instance details

Methods

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

sconcat :: NonEmpty SZS -> SZS #

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

Monoid SZS Source # 
Instance details

Methods

mempty :: SZS #

mappend :: SZS -> SZS -> SZS #

mconcat :: [SZS] -> SZS #