Hets - the Heterogeneous Tool Set

Copyright(c) Rainer Grabbe, DFKI GmbH
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityunknown
Safe HaskellNone

SoftFOL.MathServParsing

Description

Functions for parsing MathServ output into a MathServResponse structure.

Synopsis

Documentation

callMathServ

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

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

MathServ services to select.

Constructors

Broker

Broker service

VampireService

Vampire service

data MathServOperationTypes

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

data MathServCall

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

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

data MWStatus

Constructors

MWStatus