Jukebox.TPTP.Lexer

Documentation

scan :: String -> TokenStream

data Pos

Constructors

Pos !Word !Word

Instances

Show Pos

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

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

Methods

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

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

Ord Punct

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

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

Methods

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

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

Ord Defined

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

Methods

showsPrec :: Int -> Defined -> ShowS

show :: Defined -> String

showList :: [Defined] -> ShowS

data Keyword

Constructors

Normal

Thf

Tff

Fof

Cnf

Axiom

Hypothesis

Definition

Assumption

Lemma

Theorem

Conjecture

NegatedConjecture

Question

Plain

FiDomain

FiHypothesis

FiPredicates

Type

Unknown

Include

Instances

Eq Keyword

Methods

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

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

Ord Keyword

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

Methods

showsPrec :: Int -> Keyword -> ShowS

show :: Keyword -> String

showList :: [Keyword] -> ShowS

data TokenStream

Constructors

At !Pos !Contents

Instances

type Position TokenStream

type Position TokenStream = TokenStream

data Contents

Constructors

Cons !Token TokenStream