content: {- |
  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 = "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 axs eMsr cfg nGoal prName =
      either (\ errStr -> (ATPError errStr, cfg))
             (\ msr ->
              either
                (\ failure ->
                   (ATPError ("MathServe Error: " ++ case lines failure of
                     [] -> ""
                     h : _ -> h),
                   cfg { proofStatus = defaultProofStatus nGoal
                           (prName ++ " [via MathServe]") (configTimeLimit cfg)
                           (extraOpts cfg) "",
                         resultOutput = lines failure,
                         timeUsed = cpuTime $ timeResource msr }))
                (\ res -> mapProverResult axs res (timeResource msr)
                          cfg nGoal prName)
                (foAtpResult msr))
             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 axs atpResult timeRes cfg nGoal prName =
      let sStat = systemStatus atpResult
          res = mapToGoalStatus sStat
          prf = proof atpResult
          output = (lines . show) $
            (if prName == brokerName then
                text "Used prover  " <+> colon <+> text
                             (usedProverName $ systemStr atpResult)
              else empty)
            $+$ text "Calculus     " <+> colon <+>
                text (show $ calculus prf)
            $+$ text "Spent time   " <+> colon <+> (
                text "CPU time       " <+> equals <+>
                text (show $ cpuTime timeRes)
                $+$ text "Wall clock time" <+> equals <+>
                text (show $ wallClockTime timeRes) )
            $+$ text "Prover output" <+> colon $+$
                vcat (map (fsep . map text . words) (lines $ outputStr atpResult))
            $+$ text (replicate 75 '-')
          timeout = foAtpStatus sStat == Unsolved Timeout
  
          -- get real prover name if Broker was used
          prName' = if prName == brokerName
                       then usedProverName (systemStr atpResult)
                            ++ " [via " ++ brokerName ++ "]"
                       else prName ++ " [via MathServe]"
          usedAxs = case axioms prf of
            [] -> [AS_Anno.senAttr nGoal]
            as -> words as
          (atpErr, retval) = proofStat axs nGoal res usedAxs timeout $
              defaultProofStatus nGoal prName'
                             (configTimeLimit cfg)
                             (extraOpts cfg)
                             (formalProof prf)
      in (atpErr,
           cfg { proofStatus = retval,
                 resultOutput = output,
                 timeUsed = cpuTime timeRes })
  
  {- |
    Maps the status message from MathServ results to GoalStatus.
  -}
  mapToGoalStatus :: MWStatus -- ^ goal status
                  -> GoalStatus -- ^ final parsed goal status
  mapToGoalStatus stat = case foAtpStatus stat of
          Solved Theorem -> Proved True
          Solved CounterSatisfiable -> Disproved
          s -> Open $ Reason [show 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 pn =
      if null pn then "unknown"
        else takeWhile (/= '_') 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 nGoal prName tl opts pt =
    (openProofStatus (AS_Anno.senAttr nGoal)
                      prName (ProofTree pt))
    {tacticScript = TacticScript $ show ATPTacticScript
      {tsTimeLimit = tl,
       tsExtraOpts = 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 axs nGoal res usedAxs timeOut defaultPrStat = case res of
    Proved _ -> let nName = AS_Anno.senAttr nGoal in
        (ATPSuccess, defaultPrStat
         { goalStatus = Proved $ elem nName usedAxs
         , usedAxioms = case filter (/= nName) usedAxs of
            [] -> axs
            rs -> rs })
    _ -> (if timeOut then ATPTLimitExceeded else ATPSuccess
         , defaultPrStat { goalStatus = res })
  