| Copyright | (c) Evgenii Kotelnikov 2019-2021 |
|---|---|
| License | GPL-3 |
| Maintainer | evgeny.kotelnikov@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.TPTP.Parse.Combinators
Description
Synopsis
- skipWhitespace :: Parser ()
- input :: Parser a -> Parser a
- atom :: Parser Atom
- var :: Parser Var
- distinctObject :: Parser DistinctObject
- function :: Parser (Name Function)
- predicate :: Parser (Name Predicate)
- sort :: Parser (Name Sort)
- tff1Sort :: Parser TFF1Sort
- type_ :: Parser Type
- number :: Parser Number
- term :: Parser Term
- literal :: Parser Literal
- clause :: Parser Clause
- unsortedFirstOrder :: Parser UnsortedFirstOrder
- sortedFirstOrder :: Parser SortedFirstOrder
- monomorphicFirstOrder :: Parser MonomorphicFirstOrder
- polymorphicFirstOrder :: Parser PolymorphicFirstOrder
- unit :: Parser Unit
- tptp :: Parser TPTP
- tstp :: Parser TSTP
- szs :: Parser SZS
- intro :: Parser Intro
- parent :: Parser Parent
- source :: Parser Source
- info :: Parser Info
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
Parse an atomic word. Single-quoted atoms are parsed without the single
quotes and with the characters ' and \ unescaped.
distinctObject :: Parser DistinctObject Source #
Parse a distinct object. Double quotes are not preserved and the characters
' and \ are unescaped.
Sorts and types
First-order logic
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 Source #
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 Source #
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 Source #
Parse a formula in unsorted first-order logic.
sortedFirstOrder :: Parser SortedFirstOrder Source #
An alias for monomorphicFirstOrder.
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.