HyLo.InputFile.Parser

Documentation

parse :: [(Token, FilePos)] -> State ParseState ParseOutput

initParseState :: (Signature n p r, SignatureType)

type ParseState = (StringSignature, SignatureType)

data QueryType

Constructors

Valid

Satisfiable

Retrieve

Counting

Instances

Eq QueryType

Methods

(==) :: QueryType -> QueryType -> Bool

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

Show QueryType

Methods

showsPrec :: Int -> QueryType -> ShowS

show :: QueryType -> String

showList :: [QueryType] -> ShowS

data RelProperty

Constructors

Reflexive

Symmetric

Transitive

Functional

Injective

Universal

Difference

InverseOf String

SubsetOf [String]

Equals [String]

TClosureOf String

TRClosureOf String

Instances

Eq RelProperty

Methods

(==) :: RelProperty -> RelProperty -> Bool

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

Ord RelProperty

Methods

compare :: RelProperty -> RelProperty -> Ordering

(<) :: RelProperty -> RelProperty -> Bool

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

(>) :: RelProperty -> RelProperty -> Bool

(>=) :: RelProperty -> RelProperty -> Bool

max :: RelProperty -> RelProperty -> RelProperty

min :: RelProperty -> RelProperty -> RelProperty

Show RelProperty

Methods

showsPrec :: Int -> RelProperty -> ShowS

show :: RelProperty -> String

showList :: [RelProperty] -> ShowS

data ParseOutput

Constructors

PO

Fields

• relations :: [RelInfo]
• provers :: [ProverInfo]
• theory :: [Formula NomSymbol PropSymbol RelSymbol]
• tasks :: [InferenceTask]

Instances

Show ParseOutput

Methods

showsPrec :: Int -> ParseOutput -> ShowS

show :: ParseOutput -> String

showList :: [ParseOutput] -> ShowS

type RelInfo = (String, [RelProperty])

type ProverInfo = (String, [(String, String)])

type InferenceTask = (QueryType, Maybe String, [Formula NomSymbol PropSymbol RelSymbol])