Copyright	(c) Rainer Grabbe DFKI GmbH
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	unknown
Safe Haskell	None

SoftFOL.MathServParsing

Description

Functions for parsing MathServ output into a MathServResponse structure.

Synopsis

callMathServ :: MathServCall -> IO (Either String String)
parseMathServOut :: Either String String -> IO (Either String MathServResponse)
data MathServServices
- = Broker
- | VampireService
data MathServOperationTypes
- = ProblemOpt
- | ProblemChoice
- | TPTPProblem
- | Problem
data MathServCall = MathServCall {
- mathServService :: MathServServices
- mathServOperation :: MathServOperationTypes
- problem :: String
- proverTimeLimit :: Int
- extraOptions :: Maybe String
}
data MathServResponse = MathServResponse {
- foAtpResult :: Either String MWFoAtpResult
- timeResource :: MWTimeResource
}
data MWFoAtpResult = MWFoAtpResult {
- proof :: MWFormalProof
- outputStr :: String
- systemStatus :: MWStatus
- systemStr :: String
- time :: MWTimeResource
}
data MWFormalProof = TstpCnfRefutation {
- formalProof :: String
- proofOf :: MWProvingProblem
- calculus :: MWCalculus
- axioms :: String
}
data MWStatus = MWStatus {
- solved :: Bool
- foAtpStatus :: FoAtpStatus
}
data FoAtpStatus
- = Solved SolvedStatus
- | Unsolved UnsolvedStatus
data SolvedStatus
- = CounterEquivalent
- | CounterSatisfiable
- | CounterTheorem
- | Equivalent
- | NoConsequence
- | Satisfiable
- | TautologousConclusion
- | Tautology
- | Theorem
- | Unsatisfiable
- | UnsatisfiableConclusion
data UnsolvedStatus
- = Assumed
- | GaveUp
- | InputError
- | MemoryOut
- | ResourceOut
- | Timeout
- | Unknown
- | NoStatus
data MWCalculus
- = AprosNDCalculus
- | OmegaNDCalculus
- | EpResCalc
- | SpassResCalc
- | StandardRes
- | OtterCalc
- | VampireResCalc
- | ZenonCalc
- | UnknownCalc
data MWTimeResource = MWTimeResource {
- cpuTime :: TimeOfDay
- wallClockTime :: TimeOfDay
}

Documentation

callMathServ Source #

Arguments

:: MathServCall	needed data to do a MathServ call
-> IO (Either String String)	Left (SOAP error) or Right (MathServ output or error message)

Sends a problem in TPTP format to MathServ using a given time limit. Either MathServ output is returned or a simple error message (no XML).

parseMathServOut Source #

Arguments

:: Either String String	Left (SOAP error) or Right (MathServ output or error message)
-> IO (Either String MathServResponse)	parsed rdf-objects in record

Full parsing of RDF-objects returned by MathServ and putting the results into a MathServResponse data-structure.

data MathServServices Source #

MathServ services to select.

Constructors

Broker	Broker service
VampireService	Vampire service

Instances

Instances details

Show MathServServices Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> MathServServices -> ShowS show :: MathServServices -> String showList :: [MathServServices] -> ShowS

data MathServOperationTypes Source #

MathServ operation to select. These are only common types and will be translated into correct MathServOperations.

Constructors

ProblemOpt	stands for ProveProblemOpt
ProblemChoice	stands for ProveProblemChoice
TPTPProblem	stands for ProveTPTPProblem or ProveTPTPProblemWithOptions
Problem	stands for ProveProblem

Instances

Instances details

Show MathServOperationTypes Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> MathServOperationTypes -> ShowS show :: MathServOperationTypes -> String showList :: [MathServOperationTypes] -> ShowS

data MathServCall Source #

Record type for all needed data to do a MathServ call.

Constructors

MathServCall
Fields mathServService :: MathServServices Selected MathServ service mathServOperation :: MathServOperationTypes Selected MathServ operation problem :: String Problem to prove in TPTP format proverTimeLimit :: Int Time limit extraOptions :: Maybe String Extra options

data MathServResponse Source #

A MathServ response structure to be filled by parsing all rdf-objects returned by MathServ.

Constructors

MathServResponse
Fields foAtpResult :: Either String MWFoAtpResult timeResource :: MWTimeResource

Instances

Instances details

Eq MathServResponse Source #
Instance details Defined in SoftFOL.MathServParsing Methods (==) :: MathServResponse -> MathServResponse -> Bool (/=) :: MathServResponse -> MathServResponse -> Bool
Ord MathServResponse Source #
Instance details Defined in SoftFOL.MathServParsing Methods compare :: MathServResponse -> MathServResponse -> Ordering (<) :: MathServResponse -> MathServResponse -> Bool (<=) :: MathServResponse -> MathServResponse -> Bool (>) :: MathServResponse -> MathServResponse -> Bool (>=) :: MathServResponse -> MathServResponse -> Bool max :: MathServResponse -> MathServResponse -> MathServResponse min :: MathServResponse -> MathServResponse -> MathServResponse
Show MathServResponse Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> MathServResponse -> ShowS show :: MathServResponse -> String showList :: [MathServResponse] -> ShowS

data MWFoAtpResult Source #

Constructors

MWFoAtpResult
Fields proof :: MWFormalProof outputStr :: String systemStatus :: MWStatus systemStr :: String time :: MWTimeResource

Instances

Instances details

Eq MWFoAtpResult Source #
Instance details Defined in SoftFOL.MathServParsing Methods (==) :: MWFoAtpResult -> MWFoAtpResult -> Bool (/=) :: MWFoAtpResult -> MWFoAtpResult -> Bool
Ord MWFoAtpResult Source #
Instance details Defined in SoftFOL.MathServParsing Methods compare :: MWFoAtpResult -> MWFoAtpResult -> Ordering (<) :: MWFoAtpResult -> MWFoAtpResult -> Bool (<=) :: MWFoAtpResult -> MWFoAtpResult -> Bool (>) :: MWFoAtpResult -> MWFoAtpResult -> Bool (>=) :: MWFoAtpResult -> MWFoAtpResult -> Bool max :: MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult min :: MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult
Show MWFoAtpResult Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> MWFoAtpResult -> ShowS show :: MWFoAtpResult -> String showList :: [MWFoAtpResult] -> ShowS

data MWFormalProof Source #

Constructors

TstpCnfRefutation
Fields formalProof :: String proofOf :: MWProvingProblem calculus :: MWCalculus axioms :: String

Instances

Instances details

Eq MWFormalProof Source #
Instance details Defined in SoftFOL.MathServParsing Methods (==) :: MWFormalProof -> MWFormalProof -> Bool (/=) :: MWFormalProof -> MWFormalProof -> Bool
Ord MWFormalProof Source #
Instance details Defined in SoftFOL.MathServParsing Methods compare :: MWFormalProof -> MWFormalProof -> Ordering (<) :: MWFormalProof -> MWFormalProof -> Bool (<=) :: MWFormalProof -> MWFormalProof -> Bool (>) :: MWFormalProof -> MWFormalProof -> Bool (>=) :: MWFormalProof -> MWFormalProof -> Bool max :: MWFormalProof -> MWFormalProof -> MWFormalProof min :: MWFormalProof -> MWFormalProof -> MWFormalProof
Show MWFormalProof Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> MWFormalProof -> ShowS show :: MWFormalProof -> String showList :: [MWFormalProof] -> ShowS

data MWStatus Source #

Constructors

MWStatus
Fields solved :: Bool foAtpStatus :: FoAtpStatus

Instances

Instances details

Eq MWStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods (==) :: MWStatus -> MWStatus -> Bool (/=) :: MWStatus -> MWStatus -> Bool
Ord MWStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods compare :: MWStatus -> MWStatus -> Ordering (<) :: MWStatus -> MWStatus -> Bool (<=) :: MWStatus -> MWStatus -> Bool (>) :: MWStatus -> MWStatus -> Bool (>=) :: MWStatus -> MWStatus -> Bool max :: MWStatus -> MWStatus -> MWStatus min :: MWStatus -> MWStatus -> MWStatus
Show MWStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> MWStatus -> ShowS show :: MWStatus -> String showList :: [MWStatus] -> ShowS

data FoAtpStatus Source #

Constructors

Solved SolvedStatus
Unsolved UnsolvedStatus

Instances

Instances details

Eq FoAtpStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods (==) :: FoAtpStatus -> FoAtpStatus -> Bool (/=) :: FoAtpStatus -> FoAtpStatus -> Bool
Ord FoAtpStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods compare :: FoAtpStatus -> FoAtpStatus -> Ordering (<) :: FoAtpStatus -> FoAtpStatus -> Bool (<=) :: FoAtpStatus -> FoAtpStatus -> Bool (>) :: FoAtpStatus -> FoAtpStatus -> Bool (>=) :: FoAtpStatus -> FoAtpStatus -> Bool max :: FoAtpStatus -> FoAtpStatus -> FoAtpStatus min :: FoAtpStatus -> FoAtpStatus -> FoAtpStatus
Read FoAtpStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods readsPrec :: Int -> ReadS FoAtpStatus readList :: ReadS [FoAtpStatus] readPrec :: ReadPrec FoAtpStatus readListPrec :: ReadPrec [FoAtpStatus]
Show FoAtpStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> FoAtpStatus -> ShowS show :: FoAtpStatus -> String showList :: [FoAtpStatus] -> ShowS

data SolvedStatus Source #

Constructors

CounterEquivalent
CounterSatisfiable
CounterTheorem
Equivalent
NoConsequence
Satisfiable
TautologousConclusion
Tautology
Theorem
Unsatisfiable
UnsatisfiableConclusion

Instances

Instances details

Eq SolvedStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods (==) :: SolvedStatus -> SolvedStatus -> Bool (/=) :: SolvedStatus -> SolvedStatus -> Bool
Ord SolvedStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods compare :: SolvedStatus -> SolvedStatus -> Ordering (<) :: SolvedStatus -> SolvedStatus -> Bool (<=) :: SolvedStatus -> SolvedStatus -> Bool (>) :: SolvedStatus -> SolvedStatus -> Bool (>=) :: SolvedStatus -> SolvedStatus -> Bool max :: SolvedStatus -> SolvedStatus -> SolvedStatus min :: SolvedStatus -> SolvedStatus -> SolvedStatus
Read SolvedStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods readsPrec :: Int -> ReadS SolvedStatus readList :: ReadS [SolvedStatus] readPrec :: ReadPrec SolvedStatus readListPrec :: ReadPrec [SolvedStatus]
Show SolvedStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> SolvedStatus -> ShowS show :: SolvedStatus -> String showList :: [SolvedStatus] -> ShowS

data UnsolvedStatus Source #

Constructors

Assumed
GaveUp
InputError
MemoryOut
ResourceOut
Timeout
Unknown
NoStatus

Instances

Instances details

Eq UnsolvedStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods (==) :: UnsolvedStatus -> UnsolvedStatus -> Bool (/=) :: UnsolvedStatus -> UnsolvedStatus -> Bool
Ord UnsolvedStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods compare :: UnsolvedStatus -> UnsolvedStatus -> Ordering (<) :: UnsolvedStatus -> UnsolvedStatus -> Bool (<=) :: UnsolvedStatus -> UnsolvedStatus -> Bool (>) :: UnsolvedStatus -> UnsolvedStatus -> Bool (>=) :: UnsolvedStatus -> UnsolvedStatus -> Bool max :: UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus min :: UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus
Read UnsolvedStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods readsPrec :: Int -> ReadS UnsolvedStatus readList :: ReadS [UnsolvedStatus] readPrec :: ReadPrec UnsolvedStatus readListPrec :: ReadPrec [UnsolvedStatus]
Show UnsolvedStatus Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> UnsolvedStatus -> ShowS show :: UnsolvedStatus -> String showList :: [UnsolvedStatus] -> ShowS

data MWCalculus Source #

Constructors

AprosNDCalculus
OmegaNDCalculus
EpResCalc
SpassResCalc
StandardRes
OtterCalc
VampireResCalc
ZenonCalc
UnknownCalc

Instances

Instances details

Eq MWCalculus Source #
Instance details Defined in SoftFOL.MathServParsing Methods (==) :: MWCalculus -> MWCalculus -> Bool (/=) :: MWCalculus -> MWCalculus -> Bool
Ord MWCalculus Source #
Instance details Defined in SoftFOL.MathServParsing Methods compare :: MWCalculus -> MWCalculus -> Ordering (<) :: MWCalculus -> MWCalculus -> Bool (<=) :: MWCalculus -> MWCalculus -> Bool (>) :: MWCalculus -> MWCalculus -> Bool (>=) :: MWCalculus -> MWCalculus -> Bool max :: MWCalculus -> MWCalculus -> MWCalculus min :: MWCalculus -> MWCalculus -> MWCalculus
Read MWCalculus Source #
Instance details Defined in SoftFOL.MathServParsing Methods readsPrec :: Int -> ReadS MWCalculus readList :: ReadS [MWCalculus] readPrec :: ReadPrec MWCalculus readListPrec :: ReadPrec [MWCalculus]
Show MWCalculus Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> MWCalculus -> ShowS show :: MWCalculus -> String showList :: [MWCalculus] -> ShowS

data MWTimeResource Source #

Constructors

MWTimeResource
Fields cpuTime :: TimeOfDay wallClockTime :: TimeOfDay

Instances

Instances details

Eq MWTimeResource Source #
Instance details Defined in SoftFOL.MathServParsing Methods (==) :: MWTimeResource -> MWTimeResource -> Bool (/=) :: MWTimeResource -> MWTimeResource -> Bool
Ord MWTimeResource Source #
Instance details Defined in SoftFOL.MathServParsing Methods compare :: MWTimeResource -> MWTimeResource -> Ordering (<) :: MWTimeResource -> MWTimeResource -> Bool (<=) :: MWTimeResource -> MWTimeResource -> Bool (>) :: MWTimeResource -> MWTimeResource -> Bool (>=) :: MWTimeResource -> MWTimeResource -> Bool max :: MWTimeResource -> MWTimeResource -> MWTimeResource min :: MWTimeResource -> MWTimeResource -> MWTimeResource
Show MWTimeResource Source #
Instance details Defined in SoftFOL.MathServParsing Methods showsPrec :: Int -> MWTimeResource -> ShowS show :: MWTimeResource -> String showList :: [MWTimeResource] -> ShowS