content: {- |
  Module      :  ./SoftFOL/ProverState.hs
  Description :  Help functions for all automatic theorem provers.
  Copyright   :  (c) Rainer Grabbe
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  needs POSIX
  
  Data structures and initialising functions for Prover state and configurations.
  
  -}
  
  module SoftFOL.ProverState where
  
  import Logic.Prover
  
  import SoftFOL.Sign
  import SoftFOL.Conversions
  import SoftFOL.Translate
  import SoftFOL.PrintTPTP
  import SoftFOL.Print ()
  
  import qualified Common.AS_Annotation as AS_Anno
  import Common.ProofUtils
  import Common.Utils (splitOn)
  import Common.DocUtils
  
  -- * Data structures
  
  data SoftFOLProverState = SoftFOLProverState
      { initialLogicalPart :: SPLogicalPart}
  
  -- * SoftFOL specific functions for prover GUI
  
  {- |
    Creates an initial SoftFOL prover state with logical part.
  -}
  spassProverState
      :: Sign -- ^ SoftFOL signature
      -> [AS_Anno.Named SPTerm]
         -- ^ list of named SoftFOL terms containing axioms
      -> [FreeDefMorphism SPTerm SoftFOLMorphism]  -- ^ freeness constraints
      -> SoftFOLProverState
  spassProverState sign oSens' _ = SoftFOLProverState {
      initialLogicalPart = foldl insertSentence
                                 (signToSPLogicalPart sign)
                                 (reverse axiomList)}
    where nSens = prepareSenNames transSenName oSens'
          axiomList = filter AS_Anno.isAxiom nSens
  
  {- |
    Inserts a named SoftFOL term into SoftFOL prover state.
  -}
  insertSentenceGen
      :: SoftFOLProverState
         -- ^ prover state containing initial logical part
      -> AS_Anno.Named SPTerm -- ^ goal to add
      -> SoftFOLProverState
  insertSentenceGen pst s = pst {initialLogicalPart =
                                  insertSentence (initialLogicalPart pst) s}
  
  {- |
    Pretty printing SoftFOL goal in DFG format.
  -}
  showDFGProblem
      :: String -- ^ theory name
      -> SoftFOLProverState
         -- ^ prover state containing initial logical part
      -> AS_Anno.Named SPTerm -- ^ goal to print
      -> [String] -- ^ extra options
      -> IO String -- ^ formatted output of the goal
  showDFGProblem thName pst nGoal opts = do
    prob <- genSoftFOLProblem thName (initialLogicalPart pst) $ Just nGoal
    -- add SPASS command line settings and extra options
    let prob' = prob { settings = settings prob ++ parseSPASSCommands opts }
    return $ showDoc prob' ""
  
  {- |
    Pretty printing SoftFOL-model-finding-problem in TPTP format.
  -}
  showTPTPProblemM
      :: String -- ^ theory name
      -> SoftFOLProverState -- ^ prover state containing initial logical part
      -> [String] -- ^ extra options
      -> IO String -- ^ formatted output of the goal
  showTPTPProblemM thName pst = showTPTPProblemAux thName pst Nothing
  
  {- |
    Pretty printing SoftFOL goal in TPTP format.
  -}
  showTPTPProblem
      :: String -- ^ theory name
      -> SoftFOLProverState -- ^ prover state containing initial logical part
      -> AS_Anno.Named SPTerm -- ^ goal to print
      -> [String] -- ^ extra options
      -> IO String -- ^ formatted output of the goal
  showTPTPProblem thName pst = showTPTPProblemAux thName pst . Just
  
  showTPTPProblemAux
      :: String -- ^ theory name
      -> SoftFOLProverState -- ^ prover state containing initial logical part
      -> Maybe (AS_Anno.Named SPTerm) -- ^ possible goal to print
      -> [String] -- ^ extra options
      -> IO String -- ^ formatted output of the goal
  showTPTPProblemAux thName pst mGoal opts = do
    prob <- genSoftFOLProblem thName (initialLogicalPart pst) mGoal
    -- add extra options as SPSettings with only one field filled
    let prob' = prob { settings = settings prob
                                  ++ [SPSettings SPASS
                                       $ map (\ opt ->
                                             SPFlag "set_flag" [opt]) opts] }
    return $ show $ printTPTP prob'
  
  -- | Translates SPASS command line into [SPSetting]
  parseSPASSCommands :: [String] -- ^ SPASS command line options
                     -> [SPSetting] -- ^ parsed parameters and options
  parseSPASSCommands comLine =
      [SPSettings SPASS $
              map (\ opt -> case splitOn '=' $ dropWhile (== '-') opt of
                   [] -> error "parseSPASSCommands"
                   [h] -> SPFlag "set_flag" [h, "1"]
                     -- if multiple '=', texts are concatenated
                   h : r -> SPFlag "set_flag" [h, concat r]
                  ) comLine ]
  
  -- | get all axioms possibly used in a proof
  getAxioms :: SoftFOLProverState -> [String]
  getAxioms = map AS_Anno.senAttr . concatMap formulae . filter isAxiomFormula
    . formulaLists . initialLogicalPart
  