Safe Haskell	None
Language	Haskell98

Jukebox.TPTP.Parse.Core

Documentation

data ParseState Source

Constructors

MkState ![Input Form] !(Map String Type) !(Map String Function) !(Map String Variable) !Int64

type Parser = Parsec ParsecState Source

type ParsecState = UserState ParseState TokenStream Source

data IncludeStatement Source

Constructors

Include String (Maybe [Tag])

Instances

Show IncludeStatement Source

initialState :: ParseState Source

initialStateFrom :: [Name] -> Map String Type -> Map String (Name ::: FunType) -> ParseState Source

data ParseResult a Source

Constructors

ParseFailed Location [String]
ParseSucceeded a
ParseStalled Location FilePath (String -> ParseResult a)

Instances

Monad ParseResult Source
Functor ParseResult Source
Applicative ParseResult Source

data Location Source

Constructors

Location FilePath Integer Integer

Instances

Show Location Source

makeLocation :: FilePath -> Pos -> Location Source

parseProblem :: FilePath -> String -> ParseResult [Input Form] Source

parseProblemFrom :: ParseState -> FilePath -> String -> ParseResult [Input Form] Source

testParser :: Parser a -> String -> Either [String] a 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 String Source

number :: Parsec ParsecState Integer Source

atom :: Parsec ParsecState String 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

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

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

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

lookupType :: String -> Parser Type Source

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

individual :: Type Source

cnf :: Parser Form Source

tff :: Parser Form Source

fof :: Parser Form Source

data Thing Source

Constructors

Apply !String ![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 :: Mode -> Map String Variable -> Parser a Source

parser :: Mode -> Map String Variable -> Parser a Source

Instances

TermLike Form Source
TermLike Term Source
TermLike Thing Source

data Mode Source

Constructors

Typed
Untyped
NoQuantification

class TermLike a => FormulaLike a where Source

Methods

fromFormula :: Form -> a Source

Instances

FormulaLike Form Source
FormulaLike Thing Source

term :: TermLike a => Mode -> Map String Variable -> Parser a Source

literal :: FormulaLike a => Mode -> Map String Variable -> Parser a Source

unitary :: FormulaLike a => Mode -> Map String Variable -> Parser a Source

quantified :: FormulaLike a => Mode -> Map String Variable -> Parser a Source

formula :: FormulaLike a => Mode -> Map String Variable -> Parser a Source

binder :: Mode -> 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