Jukebox.TPTP.Parse.Core

Documentation

data ParseState

Constructors

MkState (Maybe String) ![Input Form] !(Map String Type) !(Map String [Function]) !(Map String 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 String Type -> Map String [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

fail :: String -> 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

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

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

variable :: Parsec ParsecState String

number :: Parsec ParsecState Integer

ratNumber :: Parsec ParsecState Rational

realNumber :: Parsec ParsecState Rational

atom :: Parsec ParsecState String

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 :: String -> FunType -> Parser Function

showTypes :: [FunType] -> String

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

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

lookupType :: String -> Parser Type

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

cnf :: Parser Form

tff :: Parser Form

fof :: Parser Form

data Thing

Constructors

Apply !String ![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

FormulaLike Thing

Defined in Jukebox.TPTP.Parse.Core

Methods

fromFormula :: Form -> Thing

TermLike Thing

Defined in Jukebox.TPTP.Parse.Core

Methods

fromThing :: Thing -> Parser Thing

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

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

class TermLike a where

Methods

fromThing :: Thing -> Parser a

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

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

Instances

TermLike Form

Defined in Jukebox.TPTP.Parse.Core

Methods

fromThing :: Thing -> Parser Form

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

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

TermLike Term

Defined in Jukebox.TPTP.Parse.Core

Methods

fromThing :: Thing -> Parser Term

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

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

TermLike Thing

Defined in Jukebox.TPTP.Parse.Core

Methods

fromThing :: Thing -> Parser Thing

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

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

data Mode

Constructors

Typed

Untyped

NoQuantification

class TermLike a => FormulaLike a where

Methods

fromFormula :: Form -> a

Instances

FormulaLike Form

Defined in Jukebox.TPTP.Parse.Core

Methods

fromFormula :: Form -> Form

FormulaLike Thing

Defined in Jukebox.TPTP.Parse.Core

Methods

fromFormula :: Form -> Thing

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

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

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

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

formula :: FormulaLike a => Mode -> Map String 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 :: Type

Methods

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

position :: TokenStream -> Position TokenStream