tptp-0.1.0.3: 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

whitespace :: Parser () Source #

Consume white space and trailing comments.

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 #

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

Annotations

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.