Safe Haskell	None
Language	Haskell98

Jukebox.TPTP.ClauseParser

Documentation

data ParseState Source

Constructors

MkState ![Input Form] !(Map ByteString Type) !(Map ByteString (Name ::: FunType)) !(Map ByteString (Name ::: Type)) Type !(Closed ())

type Parser = Parsec ParsecState Source

type ParsecState = UserState ParseState TokenStream Source

data IncludeStatement Source

Constructors

Include ByteString (Maybe [Tag])

Instances

Show IncludeStatement Source

initialState :: ParseState Source

testParser :: Parser a -> String -> Either [String] a Source

getProblem :: Parser [Input Form] Source

keyword' :: Stream a Token => (Keyword -> Bool) -> Parsec a Token Source

keyword :: Stream a Token => Keyword -> Parsec a Token Source

punct' :: Stream a Token => (Punct -> Bool) -> Parsec a Token Source

punct :: Stream a Token => Punct -> Parsec a Token Source

defined' :: Stream a Token => (Defined -> Bool) -> Parsec a Defined Source

defined :: Stream a Token => Defined -> Parsec a Defined Source

variable :: Parsec ParsecState ByteString Source

number :: Parsec ParsecState Integer Source

atom :: Parsec ParsecState ByteString Source

parens :: Parser a -> Parser a Source

bracks :: Parser a -> Parser a Source

binExpr :: Parser a -> Parser (a -> a -> Parser a) -> Parser a Source

section :: (Tag -> Bool) -> Parser (Maybe IncludeStatement) Source

input :: (Tag -> Bool) -> Parser () Source

kind :: Parser (Tag -> Form -> Input Form) Source

tag :: Parser Tag Source

include :: Parser IncludeStatement Source

newFormula :: Input Form -> Parser () Source

newNameFrom :: Named a => Closed () -> a -> (Closed (), Name) Source

findType :: ByteString -> Parser Type Source

newFunction :: ByteString -> FunType -> Parser (Name ::: FunType) Source

applyFunction :: ByteString -> [Term] -> Type -> Parser Term Source

typeError :: Stream a c => (:::) Name FunType -> [Term] -> Parsec a b Source

lookupFunction :: FunType -> ByteString -> Parser (Name ::: FunType) Source

individual :: Parser Type Source

cnf :: Parser Form Source

tff :: Parser Form Source

fof :: Parser Form Source

data Thing Source

Constructors

Apply !ByteString ![Term]
Term !Term
Formula !Form

Instances

Show Thing Source
FormulaLike Thing Source
TermLike Thing Source

class TermLike a where Source

Methods

fromThing :: Thing -> Parser a Source

var :: (?ctx :: Maybe (Map ByteString Variable)) => Parser a Source

parser :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable)) => Parser a Source

Instances

TermLike Form Source
TermLike Term Source
TermLike Thing Source

class TermLike a => FormulaLike a where Source

Methods

fromFormula :: Form -> a Source

Instances

FormulaLike Form Source
FormulaLike Thing Source

term :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), TermLike a) => Parser a Source

literal :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a Source

unitary :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a Source

quantified :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a Source

formula :: (?binder :: Parser Variable, ?ctx :: Maybe (Map ByteString Variable), FormulaLike a) => Parser a Source

varDecl :: Bool -> Parser Variable Source

type_ :: Parser Type Source

data Type_ Source

Constructors

TType
Fun [Type] Type
Prod [Type]

prod :: Type_ -> Type_ -> Parser Type_ Source

arrow :: Type_ -> Type_ -> Parser Type_ Source

leaf :: Parser Type_ Source

compoundType :: Parser Type_ Source

typeDeclaration :: Parser () Source