Jukebox.TPTP.Parse.Core

Documentation

data ParseState

Constructors

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

type Parser = Parsec ParsecState

type ParsecState = UserState ParseState TokenStream

data IncludeStatement

Constructors

Include String (Maybe [Tag])

Instances

Show IncludeStatement

Defined in Jukebox.TPTP.Parse.Core

Methods

showsPrec :: Int -> IncludeStatement -> ShowS

show :: IncludeStatement -> String

showList :: [IncludeStatement] -> ShowS

initialState :: Maybe String -> ParseState

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

data ParseResult a

Constructors

ParseFailed Location [String]

ParseSucceeded a

ParseStalled Location FilePath (String -> ParseResult a)

Instances

Monad ParseResult

Defined in Jukebox.TPTP.Parse.Core

Methods

(>>=) :: ParseResult a -> (a -> ParseResult b) -> ParseResult b

(>>) :: ParseResult a -> ParseResult b -> ParseResult b

return :: a -> ParseResult a

Functor ParseResult

Defined in Jukebox.TPTP.Parse.Core

Methods

fmap :: (a -> b) -> ParseResult a -> ParseResult b

(<$) :: a -> ParseResult b -> ParseResult a

Applicative ParseResult

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

Constructors

Location FilePath Integer Integer

Instances

Show Location

Defined in Jukebox.TPTP.Parse.Core

Methods

showsPrec :: Int -> Location -> ShowS

show :: Location -> String

showList :: [Location] -> ShowS

makeLocation :: FilePath -> Pos -> Location

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

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

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

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

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

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

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

operator :: Stream a Token => (Punct -> Bool) -> Parsec a Token

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

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

variable :: Parsec ParsecState Symbol

number :: Parsec ParsecState Integer

ratNumber :: Parsec ParsecState Rational

realNumber :: Parsec ParsecState Rational

atom :: Parsec ParsecState Symbol

parens :: Parser a -> Parser a

bracks :: Parser a -> Parser a

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

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

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

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

tag :: Parser Tag

include :: Parser IncludeStatement

newFormula :: Input Form -> Parser ()

newFunction :: Symbol -> FunType -> Parser Function

showTypes :: [FunType] -> String

applyFunction :: Symbol -> [Term] -> Type -> Parser Term

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

lookupType :: Symbol -> Parser Type

lookupFunction :: FunType -> Symbol -> Parser [Name ::: FunType]

getFunctions :: Parser (Map Symbol [Function])

cnf :: Parser Form

tff :: Parser Form

fof :: Parser Form

data Thing

Constructors

Apply !Symbol ![Term]

Term !Term

Formula !Form

Instances

Show Thing

Defined in Jukebox.TPTP.Parse.Core

Methods

showsPrec :: Int -> Thing -> ShowS

show :: Thing -> String

showList :: [Thing] -> ShowS

TermLike Thing

Defined in Jukebox.TPTP.Parse.Core

Methods

fromThing :: Thing -> Parser Thing

var :: Mode -> Map Symbol Variable -> Parser Thing

parseFormula :: Parser Form -> Parser Thing

parser :: Mode -> Map Symbol Variable -> Parser Thing

class TermLike a where

Methods

fromThing :: Thing -> Parser a

var :: Mode -> Map Symbol Variable -> Parser a

parseFormula :: Parser Form -> Parser a

parser :: Mode -> Map Symbol Variable -> Parser a

Instances

TermLike Form

Defined in Jukebox.TPTP.Parse.Core

Methods

fromThing :: Thing -> Parser Form

var :: Mode -> Map Symbol Variable -> Parser Form

parseFormula :: Parser Form -> Parser Form

parser :: Mode -> Map Symbol Variable -> Parser Form

TermLike Term

Defined in Jukebox.TPTP.Parse.Core

Methods

fromThing :: Thing -> Parser Term

var :: Mode -> Map Symbol Variable -> Parser Term

parseFormula :: Parser Form -> Parser Term

parser :: Mode -> Map Symbol Variable -> Parser Term

TermLike Thing

Defined in Jukebox.TPTP.Parse.Core

Methods

fromThing :: Thing -> Parser Thing

var :: Mode -> Map Symbol Variable -> Parser Thing

parseFormula :: Parser Form -> Parser Thing

parser :: Mode -> Map Symbol Variable -> Parser Thing

data Mode

Constructors

Typed

Untyped

NoQuantification

atomic :: TermLike a => Mode -> Map Symbol Variable -> Parser a

unary :: TermLike a => Mode -> Map Symbol Variable -> Parser a

term :: TermLike a => Mode -> Map Symbol Variable -> Parser a

postfixOperator :: Parser Symbol

prefixOperator :: Parser Symbol

infixOperator :: Parser Symbol

isPostfix :: Map Symbol [Function] -> Punct -> Bool

literal :: TermLike a => Mode -> Map Symbol Variable -> Parser a

unitary :: TermLike a => Mode -> Map Symbol Variable -> Parser a

quantified :: TermLike a => Mode -> Map Symbol Variable -> Parser a

formula :: TermLike a => Mode -> Map Symbol Variable -> Parser a

binder :: Mode -> Parser Variable

type_ :: Parser Type

data Type_

Constructors

TType

Fun [Type] Type

Prod [Type]

prod :: Type_ -> Type_ -> Parser Type_

arrow :: Type_ -> Type_ -> Parser Type_

leaf :: Parser Type_

compoundType :: Parser Type_

typeDeclaration :: Parser ()

Orphan instances

Stream TokenStream Token

Associated Types

type Position TokenStream

Methods

primToken :: TokenStream -> (TokenStream -> Token -> c) -> c -> (String -> c) -> c

position :: TokenStream -> Position TokenStream