| 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.
Synopsis
- 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 Source #
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.
Arguments
| :: String | Prover name from MathServResponse |
| -> String | name without version number or unknown |
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.