| Copyright | (c) Rainer Grabbe |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | needs POSIX |
| Safe Haskell | None |
SoftFOL.MathServMapping
Description
Maps a MathServResponse into a GenericConfig structure.
- brokerName :: String
- mapMathServResponse :: [String] -> Either String MathServResponse -> GenericConfig ProofTree -> Named SPTerm -> String -> (ATPRetval, GenericConfig ProofTree)
- mapProverResult :: [String] -> MWFoAtpResult -> MWTimeResource -> GenericConfig ProofTree -> Named SPTerm -> String -> (ATPRetval, GenericConfig ProofTree)
- mapToGoalStatus :: MWStatus -> GoalStatus
- usedProverName :: String -> String
- defaultProofStatus :: Named SPTerm -> String -> Int -> [String] -> String -> ProofStatus ProofTree
- proofStat :: [String] -> Named SPTerm -> GoalStatus -> [String] -> Bool -> ProofStatus ProofTree -> (ATPRetval, ProofStatus ProofTree)
Documentation
brokerName :: String
Name of the prover if MathServ was called via Broker.
Arguments
| :: [String] | all axiom names |
| -> Either String MathServResponse | SOAP faultstring or Parsed MathServ data |
| -> GenericConfig ProofTree | configuration to use |
| -> Named SPTerm | goal to prove |
| -> String | prover name |
| -> (ATPRetval, GenericConfig ProofTree) | (retval, configuration with proof status and complete output) |
Maps a MathServResponse record into a GenericConfig with ProofStatus. If an error occured, an ATPError with error message instead of result output will be returned.
Arguments
| :: [String] | all axiom names |
| -> MWFoAtpResult | parsed FoATPResult data |
| -> MWTimeResource | global time spent |
| -> GenericConfig ProofTree | configuration to use |
| -> Named SPTerm | goal to prove |
| -> String | prover name |
| -> (ATPRetval, GenericConfig ProofTree) | (retval, configuration with proof status, complete output) |
Maps a FoAtpResult record into a GenericConfig with ProofStatus. Result output contains all important informations in a list of Strings. The function should only be called if there is a FoAtpResult available.
Arguments
| :: MWStatus | goal status |
| -> GoalStatus | final parsed goal status |
Maps the status message from MathServ results to GoalStatus.
Gets the prover name from MathServResponse and extracts the name only (without version number). If the name's empty, prover name is "unknown".
Arguments
| :: Named SPTerm | goal to prove |
| -> String | prover name |
| -> Int | time limit |
| -> [String] | list of used options |
| -> String | proof tree (simple text) |
| -> ProofStatus ProofTree |
Default proof status. Contains the goal name, prover name and the time limit option used by MathServ.
Arguments
| :: [String] | all axiom names |
| -> Named SPTerm | goal to prove |
| -> GoalStatus | Nothing stands for prove error |
| -> [String] | Used axioms in the proof |
| -> Bool | Timeout status |
| -> ProofStatus ProofTree | default proof status |
| -> (ATPRetval, ProofStatus ProofTree) | General return value of a prover run, used in GUI. Detailed proof status if information is available. |
Returns the value of a prover run used in GUI (Success or TLimitExceeded), and the proofStatus containing all prove information available.