Safe Haskell	None
Language	Haskell98

Jukebox.TPTP.Parse.Core

Contents

Orphan instances

Documentation

data ParseState Source #

Constructors

MkState (Maybe String) ![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 #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods showsPrec :: Int -> IncludeStatement -> ShowS # show :: IncludeStatement -> String # showList :: [IncludeStatement] -> ShowS #

initialState :: Maybe String -> ParseState Source #

initialStateFrom :: Maybe String -> [Name] -> Map String Type -> Map String [Function] -> ParseState Source #

data ParseResult a Source #

Constructors

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

Instances

Monad ParseResult Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods (>>=) :: ParseResult a -> (a -> ParseResult b) -> ParseResult b # (>>) :: ParseResult a -> ParseResult b -> ParseResult b # return :: a -> ParseResult a # fail :: String -> ParseResult a #
Functor ParseResult Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods fmap :: (a -> b) -> ParseResult a -> ParseResult b # (<$) :: a -> ParseResult b -> ParseResult a #
Applicative ParseResult Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods pure :: a -> ParseResult a # (<>) :: ParseResult (a -> b) -> ParseResult a -> ParseResult b # liftA2 :: (a -> b -> c) -> ParseResult a -> ParseResult b -> ParseResult c # (>) :: ParseResult a -> ParseResult b -> ParseResult b # (<*) :: ParseResult a -> ParseResult b -> ParseResult a #

data Location Source #

Constructors

Location FilePath Integer Integer

Instances

Show Location Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods showsPrec :: Int -> Location -> ShowS # show :: Location -> String # showList :: [Location] -> ShowS #

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 #

ratNumber :: Parsec ParsecState Rational Source #

realNumber :: Parsec ParsecState Rational 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 Function Source #

showTypes :: [FunType] -> String 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 #

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 #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods showsPrec :: Int -> Thing -> ShowS # show :: Thing -> String # showList :: [Thing] -> ShowS #
FormulaLike Thing Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods fromFormula :: Form -> Thing Source #
TermLike Thing Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods fromThing :: Thing -> Parser Thing Source # var :: Mode -> Map String Variable -> Parser Thing Source # parser :: Mode -> Map String Variable -> Parser Thing Source #

class TermLike a where Source #

Minimal complete definition

fromThing, var, parser

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 #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods fromThing :: Thing -> Parser Form Source # var :: Mode -> Map String Variable -> Parser Form Source # parser :: Mode -> Map String Variable -> Parser Form Source #
TermLike Term Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods fromThing :: Thing -> Parser Term Source # var :: Mode -> Map String Variable -> Parser Term Source # parser :: Mode -> Map String Variable -> Parser Term Source #
TermLike Thing Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods fromThing :: Thing -> Parser Thing Source # var :: Mode -> Map String Variable -> Parser Thing Source # parser :: Mode -> Map String Variable -> Parser Thing Source #

data Mode Source #

Constructors

Typed
Untyped
NoQuantification

class TermLike a => FormulaLike a where Source #

Minimal complete definition

fromFormula

Methods

fromFormula :: Form -> a Source #

Instances

FormulaLike Form Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods fromFormula :: Form -> Form Source #
FormulaLike Thing Source #
Instance details Defined in Jukebox.TPTP.Parse.Core Methods fromFormula :: Form -> 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 #

Orphan instances

Stream TokenStream Token Source #
Instance details Associated Types type Position TokenStream :: * Source # Methods primToken :: TokenStream -> (TokenStream -> Token -> c) -> c -> (String -> c) -> c Source # position :: TokenStream -> Position TokenStream Source #