{- |
Module      :  ./SoftFOL/MathServMapping.hs
Description :  Maps a MathServResponse into a prover configuration.
Copyright   :  (c) Rainer Grabbe
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  needs POSIX

Maps a MathServResponse into a GenericConfig structure.

-}

module SoftFOL.MathServMapping where

import Common.Doc -- as Pretty
import qualified Common.AS_Annotation as AS_Anno
import Common.ProofTree

import Logic.Prover

import SoftFOL.MathServParsing
import SoftFOL.Sign hiding (Theorem)

import Interfaces.GenericATPState

{- |
  Name of the prover if MathServ was called via Broker.
-}
brokerName :: String
brokerName :: String
brokerName = "MathServe Broker"

{- |
  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.
-}
mapMathServResponse :: [String] -- ^ all axiom names
                    -> Either String MathServResponse
                    -- ^ SOAP faultstring or Parsed MathServ data
                    -> GenericConfig ProofTree -- ^ configuration to use
                    -> AS_Anno.Named SPTerm -- ^ goal to prove
                    -> String -- ^ prover name
                    -> (ATPRetval, GenericConfig ProofTree)
                    {- ^ (retval, configuration with proof status and
                    complete output) -}
mapMathServResponse :: [String]
-> Either String MathServResponse
-> GenericConfig ProofTree
-> Named SPTerm
-> String
-> (ATPRetval, GenericConfig ProofTree)
mapMathServResponse axs :: [String]
axs eMsr :: Either String MathServResponse
eMsr cfg :: GenericConfig ProofTree
cfg nGoal :: Named SPTerm
nGoal prName :: String
prName =
    (String -> (ATPRetval, GenericConfig ProofTree))
-> (MathServResponse -> (ATPRetval, GenericConfig ProofTree))
-> Either String MathServResponse
-> (ATPRetval, GenericConfig ProofTree)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\ errStr :: String
errStr -> (String -> ATPRetval
ATPError String
errStr, GenericConfig ProofTree
cfg))
           (\ msr :: MathServResponse
msr ->
            (String -> (ATPRetval, GenericConfig ProofTree))
-> (MWFoAtpResult -> (ATPRetval, GenericConfig ProofTree))
-> Either String MWFoAtpResult
-> (ATPRetval, GenericConfig ProofTree)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
              (\ failure :: String
failure ->
                 (String -> ATPRetval
ATPError ("MathServe Error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ case String -> [String]
lines String
failure of
                   [] -> ""
                   h :: String
h : _ -> String
h),
                 GenericConfig ProofTree
cfg { proofStatus :: ProofStatus ProofTree
proofStatus = Named SPTerm
-> String -> Int -> [String] -> String -> ProofStatus ProofTree
defaultProofStatus Named SPTerm
nGoal
                         (String
prName String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [via MathServe]") (GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg)
                         (GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg) "",
                       resultOutput :: [String]
resultOutput = String -> [String]
lines String
failure,
                       timeUsed :: TimeOfDay
timeUsed = MWTimeResource -> TimeOfDay
cpuTime (MWTimeResource -> TimeOfDay) -> MWTimeResource -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ MathServResponse -> MWTimeResource
timeResource MathServResponse
msr }))
              (\ res :: MWFoAtpResult
res -> [String]
-> MWFoAtpResult
-> MWTimeResource
-> GenericConfig ProofTree
-> Named SPTerm
-> String
-> (ATPRetval, GenericConfig ProofTree)
mapProverResult [String]
axs MWFoAtpResult
res (MathServResponse -> MWTimeResource
timeResource MathServResponse
msr)
                        GenericConfig ProofTree
cfg Named SPTerm
nGoal String
prName)
              (MathServResponse -> Either String MWFoAtpResult
foAtpResult MathServResponse
msr))
           Either String MathServResponse
eMsr

{- |
  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.
-}
mapProverResult :: [String] -- ^ all axiom names
                -> MWFoAtpResult -- ^ parsed FoATPResult data
                -> MWTimeResource -- ^ global time spent
                -> GenericConfig ProofTree -- ^ configuration to use
                -> AS_Anno.Named SPTerm -- ^ goal to prove
                -> String -- ^ prover name
                -> (ATPRetval, GenericConfig ProofTree)
                -- ^ (retval, configuration with proof status, complete output)
mapProverResult :: [String]
-> MWFoAtpResult
-> MWTimeResource
-> GenericConfig ProofTree
-> Named SPTerm
-> String
-> (ATPRetval, GenericConfig ProofTree)
mapProverResult axs :: [String]
axs atpResult :: MWFoAtpResult
atpResult timeRes :: MWTimeResource
timeRes cfg :: GenericConfig ProofTree
cfg nGoal :: Named SPTerm
nGoal prName :: String
prName =
    let sStat :: MWStatus
sStat = MWFoAtpResult -> MWStatus
systemStatus MWFoAtpResult
atpResult
        res :: GoalStatus
res = MWStatus -> GoalStatus
mapToGoalStatus MWStatus
sStat
        prf :: MWFormalProof
prf = MWFoAtpResult -> MWFormalProof
proof MWFoAtpResult
atpResult
        output :: [String]
output = (String -> [String]
lines (String -> [String]) -> (Doc -> String) -> Doc -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show) (Doc -> [String]) -> Doc -> [String]
forall a b. (a -> b) -> a -> b
$
          (if String
prName String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
brokerName then
              String -> Doc
text "Used prover  " Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> String -> Doc
text
                           (String -> String
usedProverName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ MWFoAtpResult -> String
systemStr MWFoAtpResult
atpResult)
            else Doc
empty)
          Doc -> Doc -> Doc
$+$ String -> Doc
text "Calculus     " Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+>
              String -> Doc
text (MWCalculus -> String
forall a. Show a => a -> String
show (MWCalculus -> String) -> MWCalculus -> String
forall a b. (a -> b) -> a -> b
$ MWFormalProof -> MWCalculus
calculus MWFormalProof
prf)
          Doc -> Doc -> Doc
$+$ String -> Doc
text "Spent time   " Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> (
              String -> Doc
text "CPU time       " Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+>
              String -> Doc
text (TimeOfDay -> String
forall a. Show a => a -> String
show (TimeOfDay -> String) -> TimeOfDay -> String
forall a b. (a -> b) -> a -> b
$ MWTimeResource -> TimeOfDay
cpuTime MWTimeResource
timeRes)
              Doc -> Doc -> Doc
$+$ String -> Doc
text "Wall clock time" Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+>
              String -> Doc
text (TimeOfDay -> String
forall a. Show a => a -> String
show (TimeOfDay -> String) -> TimeOfDay -> String
forall a b. (a -> b) -> a -> b
$ MWTimeResource -> TimeOfDay
wallClockTime MWTimeResource
timeRes) )
          Doc -> Doc -> Doc
$+$ String -> Doc
text "Prover output" Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
$+$
              [Doc] -> Doc
vcat ((String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Doc] -> Doc
fsep ([Doc] -> Doc) -> (String -> [Doc]) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text ([String] -> [Doc]) -> (String -> [String]) -> String -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words) (String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ MWFoAtpResult -> String
outputStr MWFoAtpResult
atpResult))
          Doc -> Doc -> Doc
$+$ String -> Doc
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate 75 '-')
        timeout :: Bool
timeout = MWStatus -> FoAtpStatus
foAtpStatus MWStatus
sStat FoAtpStatus -> FoAtpStatus -> Bool
forall a. Eq a => a -> a -> Bool
== UnsolvedStatus -> FoAtpStatus
Unsolved UnsolvedStatus
Timeout

        -- get real prover name if Broker was used
        prName' :: String
prName' = if String
prName String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
brokerName
                     then String -> String
usedProverName (MWFoAtpResult -> String
systemStr MWFoAtpResult
atpResult)
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [via " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
brokerName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"
                     else String
prName String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [via MathServe]"
        usedAxs :: [String]
usedAxs = case MWFormalProof -> String
axioms MWFormalProof
prf of
          [] -> [Named SPTerm -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named SPTerm
nGoal]
          as :: String
as -> String -> [String]
words String
as
        (atpErr :: ATPRetval
atpErr, retval :: ProofStatus ProofTree
retval) = [String]
-> Named SPTerm
-> GoalStatus
-> [String]
-> Bool
-> ProofStatus ProofTree
-> (ATPRetval, ProofStatus ProofTree)
proofStat [String]
axs Named SPTerm
nGoal GoalStatus
res [String]
usedAxs Bool
timeout (ProofStatus ProofTree -> (ATPRetval, ProofStatus ProofTree))
-> ProofStatus ProofTree -> (ATPRetval, ProofStatus ProofTree)
forall a b. (a -> b) -> a -> b
$
            Named SPTerm
-> String -> Int -> [String] -> String -> ProofStatus ProofTree
defaultProofStatus Named SPTerm
nGoal String
prName'
                           (GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg)
                           (GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg)
                           (MWFormalProof -> String
formalProof MWFormalProof
prf)
    in (ATPRetval
atpErr,
         GenericConfig ProofTree
cfg { proofStatus :: ProofStatus ProofTree
proofStatus = ProofStatus ProofTree
retval,
               resultOutput :: [String]
resultOutput = [String]
output,
               timeUsed :: TimeOfDay
timeUsed = MWTimeResource -> TimeOfDay
cpuTime MWTimeResource
timeRes })

{- |
  Maps the status message from MathServ results to GoalStatus.
-}
mapToGoalStatus :: MWStatus -- ^ goal status
                -> GoalStatus -- ^ final parsed goal status
mapToGoalStatus :: MWStatus -> GoalStatus
mapToGoalStatus stat :: MWStatus
stat = case MWStatus -> FoAtpStatus
foAtpStatus MWStatus
stat of
        Solved Theorem -> Bool -> GoalStatus
Proved Bool
True
        Solved CounterSatisfiable -> GoalStatus
Disproved
        s :: FoAtpStatus
s -> Reason -> GoalStatus
Open (Reason -> GoalStatus) -> Reason -> GoalStatus
forall a b. (a -> b) -> a -> b
$ [String] -> Reason
Reason [FoAtpStatus -> String
forall a. Show a => a -> String
show FoAtpStatus
s]

{- |
  Gets the prover name from MathServResponse and extracts the name only
  (without version number). If the name's empty, prover name is "unknown".
-}
usedProverName :: String -- ^ Prover name from MathServResponse
               -> String -- ^ name without version number or unknown
usedProverName :: String -> String
usedProverName pn :: String
pn =
    if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
pn then "unknown"
      else (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '_') String
pn

{- |
  Default proof status. Contains the goal name, prover name
  and the time limit option used by MathServ.
-}
defaultProofStatus :: AS_Anno.Named SPTerm -- ^ goal to prove
                    -> String -- ^ prover name
                    -> Int -- ^ time limit
                    -> [String] -- ^ list of used options
                    -> String -- ^ proof tree (simple text)
                    -> ProofStatus ProofTree
defaultProofStatus :: Named SPTerm
-> String -> Int -> [String] -> String -> ProofStatus ProofTree
defaultProofStatus nGoal :: Named SPTerm
nGoal prName :: String
prName tl :: Int
tl opts :: [String]
opts pt :: String
pt =
  (String -> String -> ProofTree -> ProofStatus ProofTree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus (Named SPTerm -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named SPTerm
nGoal)
                    String
prName (String -> ProofTree
ProofTree String
pt))
  {tacticScript :: TacticScript
tacticScript = String -> TacticScript
TacticScript (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> String
forall a. Show a => a -> String
show ATPTacticScript :: Int -> [String] -> ATPTacticScript
ATPTacticScript
    {tsTimeLimit :: Int
tsTimeLimit = Int
tl,
     tsExtraOpts :: [String]
tsExtraOpts = [String]
opts} }

{- |
  Returns the value of a prover run used in GUI (Success or
  TLimitExceeded), and the proofStatus containing all prove
  information available.
-}
proofStat :: [String] -- ^ all axiom names
           -> AS_Anno.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. -}
proofStat :: [String]
-> Named SPTerm
-> GoalStatus
-> [String]
-> Bool
-> ProofStatus ProofTree
-> (ATPRetval, ProofStatus ProofTree)
proofStat axs :: [String]
axs nGoal :: Named SPTerm
nGoal res :: GoalStatus
res usedAxs :: [String]
usedAxs timeOut :: Bool
timeOut defaultPrStat :: ProofStatus ProofTree
defaultPrStat = case GoalStatus
res of
  Proved _ -> let nName :: String
nName = Named SPTerm -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named SPTerm
nGoal in
      (ATPRetval
ATPSuccess, ProofStatus ProofTree
defaultPrStat
       { goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved (Bool -> GoalStatus) -> Bool -> GoalStatus
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
nName [String]
usedAxs
       , usedAxioms :: [String]
usedAxioms = case (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
nName) [String]
usedAxs of
          [] -> [String]
axs
          rs :: [String]
rs -> [String]
rs })
  _ -> (if Bool
timeOut then ATPRetval
ATPTLimitExceeded else ATPRetval
ATPSuccess
       , ProofStatus ProofTree
defaultPrStat { goalStatus :: GoalStatus
goalStatus = GoalStatus
res })