Safe Haskell	None

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

initialState :: ParseState Source

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

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 ByteStringSource

number :: Parsec ParsecState IntegerSource

atom :: Parsec ParsecState ByteStringSource

parens :: Parser a -> Parser aSource

bracks :: Parser a -> Parser aSource

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

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 bSource

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

individual :: Parser Type Source

cnf :: Parser Form Source

fof :: Parser Form Source

tff :: Parser Form Source

data Thing Source

Constructors

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

Instances

Show Thing
FormulaLike Thing
TermLike Thing

class TermLike a whereSource

Methods

fromThing :: Thing -> Parser aSource

var :: [ctx :: Maybe (Map ByteString Variable)] => Parser aSource

parser :: ([binder :: Parser Variable], [ctx :: Maybe (Map ByteString Variable)]) => Parser aSource

Instances

TermLike Form
TermLike Term
TermLike Thing

class TermLike a => FormulaLike a whereSource

Methods

fromFormula :: Form -> aSource

Instances

FormulaLike Form
FormulaLike Thing

term :: ([binder :: Parser Variable], [ctx :: Maybe (Map ByteString Variable)], TermLike a) => Parser aSource

literal :: ([binder :: Parser Variable], [ctx :: Maybe (Map ByteString Variable)], FormulaLike a) => Parser aSource

formula :: ([binder :: Parser Variable], [ctx :: Maybe (Map ByteString Variable)], FormulaLike a) => Parser aSource

quantified :: ([binder :: Parser Variable], [ctx :: Maybe (Map ByteString Variable)], FormulaLike a) => Parser aSource

unitary :: ([binder :: Parser Variable], [ctx :: Maybe (Map ByteString Variable)], FormulaLike a) => Parser aSource

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