1caad5414a81bd3593e10ca6d089ebabac2d9ad8Christian MaederDescription : Maps a MathServResponse into a prover configuration.
d5fe06af711a6912ae028ebf873eada4ee8733f8Christian MaederCopyright : (c) Rainer Grabbe
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
acc7fe823b23e829cfbde7464f92557822a2a7d9Christian MaederStability : provisional
acc7fe823b23e829cfbde7464f92557822a2a7d9Christian MaederPortability : needs POSIX
1caad5414a81bd3593e10ca6d089ebabac2d9ad8Christian MaederMaps a MathServResponse into a GenericConfig structure.
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maederimport Common.Doc -- as Pretty
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maederimport qualified Common.AS_Annotation as AS_Anno
3141ac1ae0a0b9f86af05f439bc79316451b94f3Carsten Fischerimport SoftFOL.Sign hiding (Theorem)
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maeder Name of the prover if MathServ was called via Broker.
bccea164bdfc2ddc3d1e20749bb5477a46eab3a6Christian MaederbrokerName :: String
ad270004874ce1d0697fb30d7309f180553bb315Christian MaederbrokerName = "MathServe Broker"
bccea164bdfc2ddc3d1e20749bb5477a46eab3a6Christian Maeder Maps a MathServResponse record into a GenericConfig with ProofStatus.
bccea164bdfc2ddc3d1e20749bb5477a46eab3a6Christian Maeder If an error occured, an ATPError with error message instead of result output
3141ac1ae0a0b9f86af05f439bc79316451b94f3Carsten Fischer will be returned.
f323228f78695312bd7e881484e18df94c1e8f0eChristian MaedermapMathServResponse :: [String] -- ^ all axiom names
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maeder -> Either String MathServResponse
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maeder -- ^ SOAP faultstring or Parsed MathServ data
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maeder -> GenericConfig ProofTree -- ^ configuration to use
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maeder -> AS_Anno.Named SPTerm -- ^ goal to prove
d5a644d593fc653a5476f9b3efffe1d34693f1e4Christian Maeder -> String -- ^ prover name
3141ac1ae0a0b9f86af05f439bc79316451b94f3Carsten Fischer -> (ATPRetval, GenericConfig ProofTree)
8f197d81eada0a49fd7e1afdc5ef401d24bab104Christian Maeder {- ^ (retval, configuration with proof status and
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder complete output) -}
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian MaedermapMathServResponse axs eMsr cfg nGoal prName =
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder either (\ errStr -> (ATPError errStr, cfg))
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (\ failure ->
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (ATPError ("MathServe Error: " ++ case lines failure of
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder cfg { proofStatus = defaultProofStatus nGoal
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (prName ++ " [via MathServe]") (configTimeLimit cfg)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (extraOpts cfg) "",
ea39a854498febb718cbdd6035fb935fd145daacEugen Kuksa resultOutput = lines failure,
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder timeUsed = cpuTime $ timeResource msr }))
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (\ res -> mapProverResult axs res (timeResource msr)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder cfg nGoal prName)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (foAtpResult msr))
acc7fe823b23e829cfbde7464f92557822a2a7d9Christian Maeder Maps a FoAtpResult record into a GenericConfig with ProofStatus.
acc7fe823b23e829cfbde7464f92557822a2a7d9Christian Maeder Result output contains all important informations in a list of Strings.
3141ac1ae0a0b9f86af05f439bc79316451b94f3Carsten Fischer The function should only be called if there is a FoAtpResult available.
bccea164bdfc2ddc3d1e20749bb5477a46eab3a6Christian MaedermapProverResult :: [String] -- ^ all axiom names
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> MWFoAtpResult -- ^ parsed FoATPResult data
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> MWTimeResource -- ^ global time spent
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> GenericConfig ProofTree -- ^ configuration to use
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> AS_Anno.Named SPTerm -- ^ goal to prove
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> String -- ^ prover name
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> (ATPRetval, GenericConfig ProofTree)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -- ^ (retval, configuration with proof status, complete output)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian MaedermapProverResult axs atpResult timeRes cfg nGoal prName =
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder let sStat = systemStatus atpResult
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder res = mapToGoalStatus sStat
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder prf = proof atpResult
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder output = (lines . show) $
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (if prName == brokerName then
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder text "Used prover " <+> colon <+> text
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (usedProverName $ systemStr atpResult)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder $+$ text "Calculus " <+> colon <+>
3141ac1ae0a0b9f86af05f439bc79316451b94f3Carsten Fischer text (show $ calculus prf)
d5a644d593fc653a5476f9b3efffe1d34693f1e4Christian Maeder $+$ text "Spent time " <+> colon <+> (
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maeder text "CPU time " <+> equals <+>
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder text (show $ cpuTime timeRes)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder $+$ text "Wall clock time" <+> equals <+>
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder text (show $ wallClockTime timeRes) )
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder $+$ text "Prover output" <+> colon $+$
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder vcat (map (fsep . map text . words) (lines $ outputStr atpResult))
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder $+$ text (replicate 75 '-')
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder timeout = foAtpStatus sStat == Unsolved Timeout
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -- get real prover name if Broker was used
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder prName' = if prName == brokerName
3141ac1ae0a0b9f86af05f439bc79316451b94f3Carsten Fischer then usedProverName (systemStr atpResult)
d5a644d593fc653a5476f9b3efffe1d34693f1e4Christian Maeder ++ " [via " ++ brokerName ++ "]"
3141ac1ae0a0b9f86af05f439bc79316451b94f3Carsten Fischer else prName ++ " [via MathServe]"
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder usedAxs = case axioms prf of
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder as -> words as
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (atpErr, retval) = proofStat axs nGoal res usedAxs timeout $
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder defaultProofStatus nGoal prName'
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (configTimeLimit cfg)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (extraOpts cfg)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (formalProof prf)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder cfg { proofStatus = retval,
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder resultOutput = output,
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder timeUsed = cpuTime timeRes })
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder Maps the status message from MathServ results to GoalStatus.
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian MaedermapToGoalStatus :: MWStatus -- ^ goal status
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> GoalStatus -- ^ final parsed goal status
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian MaedermapToGoalStatus stat = case foAtpStatus stat of
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder Solved Theorem -> Proved True
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder Solved CounterSatisfiable -> Disproved
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder s -> Open $ Reason [show s]
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maeder Gets the prover name from MathServResponse and extracts the name only
3141ac1ae0a0b9f86af05f439bc79316451b94f3Carsten Fischer (without version number). If the name's empty, prover name is "unknown".
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian MaederusedProverName :: String -- ^ Prover name from MathServResponse
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> String -- ^ name without version number or unknown
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian MaederusedProverName pn =
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder if null pn then "unknown"
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder else takeWhile (/= '_') pn
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder Default proof status. Contains the goal name, prover name
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder and the time limit option used by MathServ.
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian MaederdefaultProofStatus :: AS_Anno.Named SPTerm -- ^ goal to prove
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> String -- ^ prover name
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> Int -- ^ time limit
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> [String] -- ^ list of used options
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> String -- ^ proof tree (simple text)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder -> ProofStatus ProofTree
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian MaederdefaultProofStatus nGoal prName tl opts pt =
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maeder (openProofStatus (AS_Anno.senAttr nGoal)
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder prName (ProofTree pt))
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder {tacticScript = TacticScript $ show ATPTacticScript
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder {tsTimeLimit = tl,
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder tsExtraOpts = opts} }
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder Returns the value of a prover run used in GUI (Success or
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder TLimitExceeded), and the proofStatus containing all prove
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder information available.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederproofStat :: [String] -- ^ all axiom names
ea39a854498febb718cbdd6035fb935fd145daacEugen Kuksa -> AS_Anno.Named SPTerm -- ^ goal to prove
ea39a854498febb718cbdd6035fb935fd145daacEugen Kuksa -> GoalStatus -- ^ Nothing stands for prove error
ea39a854498febb718cbdd6035fb935fd145daacEugen Kuksa -> [String] -- ^ Used axioms in the proof
ea39a854498febb718cbdd6035fb935fd145daacEugen Kuksa -> Bool -- ^ Timeout status
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> ProofStatus ProofTree -- ^ default proof status
ea39a854498febb718cbdd6035fb935fd145daacEugen Kuksa -> (ATPRetval, ProofStatus ProofTree)
ea39a854498febb718cbdd6035fb935fd145daacEugen Kuksa {- ^ General return value of a prover run, used in GUI.
f323228f78695312bd7e881484e18df94c1e8f0eChristian Maeder Detailed proof status if information is available. -}
f323228f78695312bd7e881484e18df94c1e8f0eChristian MaederproofStat axs nGoal res usedAxs timeOut defaultPrStat = case res of
3141ac1ae0a0b9f86af05f439bc79316451b94f3Carsten Fischer Proved _ -> let nName = AS_Anno.senAttr nGoal in
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder (ATPSuccess, defaultPrStat
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder { goalStatus = Proved $ elem nName usedAxs
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder , usedAxioms = case filter (/= nName) usedAxs of
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder _ -> (if timeOut then ATPTLimitExceeded else ATPSuccess
6cc0d8b77759c557e7d9459cd2734625a4db78b9Christian Maeder , defaultPrStat { goalStatus = res })