Jukebox.TPTP.Lexer

Documentation

scan :: String -> TokenStream

data Pos

Constructors

Pos !Word !Word

Instances

Show Pos

Defined in Jukebox.TPTP.Lexer

Methods

showsPrec :: Int -> Pos -> ShowS

show :: Pos -> String

showList :: [Pos] -> ShowS

data Token

Constructors

Atom

Fields

• keyword :: !Keyword
• tokenName :: !String

Defined

Fields

• defined :: !Defined

Var

Fields

• tokenName :: !String

DistinctObject

Fields

• tokenName :: !String

Number

Fields

• value :: !Integer

Rational

Fields

• ratValue :: !Rational

Real

Fields

• ratValue :: !Rational

Punct

Fields

• kind :: !Punct

Eof

Error

Instances

Show Token

Defined in Jukebox.TPTP.Print

Methods

showsPrec :: Int -> Token -> ShowS

show :: Token -> String

showList :: [Token] -> ShowS

Stream TokenStream Token

Defined in Jukebox.TPTP.Parse.Core

Associated Types

type Position TokenStream :: Type

Methods

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

position :: TokenStream -> Position TokenStream

data Punct

Constructors

LParen

RParen

LBrack

RBrack

Comma

Dot

Or

And

Not

Iff

Implies

Follows

Xor

Nor

Nand

Eq

Neq

ForAll

Exists

Let

LetTerm

Colon

Times

Plus

FunArrow

Lambda

Apply

ForAllLam

ExistsLam

DependentProduct

DependentSum

Some

The

Subtype

SequentArrow

Instances

Eq Punct

Defined in Jukebox.TPTP.Lexer

Methods

(==) :: Punct -> Punct -> Bool

(/=) :: Punct -> Punct -> Bool

Ord Punct

Defined in Jukebox.TPTP.Lexer

Methods

compare :: Punct -> Punct -> Ordering

(<) :: Punct -> Punct -> Bool

(<=) :: Punct -> Punct -> Bool

(>) :: Punct -> Punct -> Bool

(>=) :: Punct -> Punct -> Bool

max :: Punct -> Punct -> Punct

min :: Punct -> Punct -> Punct

Show Punct

Defined in Jukebox.TPTP.Lexer

Methods

showsPrec :: Int -> Punct -> ShowS

show :: Punct -> String

showList :: [Punct] -> ShowS

data Defined

Constructors

DTrue

DFalse

DDistinct

DItef

DItet

DO

DI

DTType

Instances

Eq Defined

Defined in Jukebox.TPTP.Lexer

Methods

(==) :: Defined -> Defined -> Bool

(/=) :: Defined -> Defined -> Bool

Ord Defined

Defined in Jukebox.TPTP.Lexer

Methods

compare :: Defined -> Defined -> Ordering

(<) :: Defined -> Defined -> Bool

(<=) :: Defined -> Defined -> Bool

(>) :: Defined -> Defined -> Bool

(>=) :: Defined -> Defined -> Bool

max :: Defined -> Defined -> Defined

min :: Defined -> Defined -> Defined

Show Defined

Defined in Jukebox.TPTP.Lexer

Methods

showsPrec :: Int -> Defined -> ShowS

show :: Defined -> String

showList :: [Defined] -> ShowS

data Keyword

Constructors

Normal

Thf

Tff

Fof

Tcf

Cnf

Axiom

Hypothesis

Definition

Assumption

Lemma

Theorem

Conjecture

NegatedConjecture

Question

Plain

FiDomain

FiHypothesis

FiPredicates

Type

Unknown

Include

Instances

Eq Keyword

Defined in Jukebox.TPTP.Lexer

Methods

(==) :: Keyword -> Keyword -> Bool

(/=) :: Keyword -> Keyword -> Bool

Ord Keyword

Defined in Jukebox.TPTP.Lexer

Methods

compare :: Keyword -> Keyword -> Ordering

(<) :: Keyword -> Keyword -> Bool

(<=) :: Keyword -> Keyword -> Bool

(>) :: Keyword -> Keyword -> Bool

(>=) :: Keyword -> Keyword -> Bool

max :: Keyword -> Keyword -> Keyword

min :: Keyword -> Keyword -> Keyword

Show Keyword

Defined in Jukebox.TPTP.Lexer

Methods

showsPrec :: Int -> Keyword -> ShowS

show :: Keyword -> String

showList :: [Keyword] -> ShowS

data TokenStream

Constructors

At !Pos !Contents

Instances

Stream TokenStream Token

Defined in Jukebox.TPTP.Parse.Core

Associated Types

type Position TokenStream :: Type

Methods

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

position :: TokenStream -> Position TokenStream

type Position TokenStream

Defined in Jukebox.TPTP.Parse.Core

type Position TokenStream = TokenStream

data Contents

Constructors

Cons !Token TokenStream