{- |
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 })