content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./TPTP/Prover/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 TPTP.Prover.ProverState ( ProverState (..)
                                 , getAxioms
                                 , insertSentenceIntoProverState
                                 , ioShowTPTPProblem
                                 , showTPTPProblemM
                                 , tptpProverState
                                 ) where
  
  import TPTP.AS
  import TPTP.Morphism
  import TPTP.Pretty
  import TPTP.Sign
  
  import Common.AS_Annotation
  import Common.ProofUtils
  import Common.Doc
  import Logic.Prover
  
  import Data.Data
  import Data.List
  
  -- * Data structures
  
  data PProblem = PProblem { identifier :: String
                           , logicalPart :: PLogicalPart
                           } deriving (Show, Eq, Ord, Typeable, Data)
  
  data ProverState = ProverState { psLogicalPart :: PLogicalPart
                                 } deriving (Show, Ord, Eq, Data, Typeable)
  
  tptpProverState :: Sign -- ^ TPTP signature
              -> [Named Sentence]
                 -- ^ list of named TPTP sentences containing axioms
              -> [FreeDefMorphism Sentence Morphism] -- ^ freeness constraints
              -> ProverState
  tptpProverState _ sentences _ = ProverState {
    psLogicalPart = foldr (flip insertSentence) emptyPLogicalPart axiomList}
    where newSentences = prepareSenNames id sentences
          axiomList = filter isAxiom newSentences
  
  -- ** proving Logical Parts
  
  {- |
    A proving logical part consists of a symbol list, a declaration list, and a
    set of formula lists. Support for clause lists and proof lists hasn't
    been implemented yet.
  -}
  data PLogicalPart = PLogicalPart { formulaeList :: [Named Sentence]
                                   } deriving (Show, Eq, Ord, Typeable, Data)
  
  emptyPLogicalPart :: PLogicalPart
  emptyPLogicalPart = PLogicalPart { formulaeList = [] }
  
  -- | gets all axioms possibly used in a proof
  getAxioms :: ProverState -> [String]
  getAxioms = map senAttr . filter isAxiom . formulaeList . psLogicalPart
  
  -- * TPTP specific functions for prover GUI
  
  -- Inserts a named TPTP term into TPTP prover state.
  insertSentenceIntoProverState :: ProverState
                                   -- ^ prover state containing initial logical part
                                -> Named Sentence -- ^ goal to add
                                -> ProverState
  insertSentenceIntoProverState proverState namedSentence =
    proverState { psLogicalPart =
                    insertSentence (psLogicalPart proverState) namedSentence }
  
  {- |
    Inserts a Named Sentence (axiom or goal) into a PLogicalPart.
  -}
  insertSentence :: PLogicalPart -> Named Sentence -> PLogicalPart
  insertSentence pLogicalPart newSentence =
    pLogicalPart { formulaeList = newSentence : formulaeList pLogicalPart }
  
  
  {- |
    Generate a TPTP problem with time stamp while maybe adding a goal.
  -}
  generateTPTPProblem :: PLogicalPart
                      -> Maybe (Named Sentence) -> PProblem
  generateTPTPProblem pLogicalPart mNewGoal = PProblem
      { identifier = "hets_exported"
      , logicalPart = maybe pLogicalPart (insertSentence pLogicalPart) mNewGoal
      }
  
  showTPTPProblemM
      :: String -- ^ theory name
      -> ProverState -- ^ prover state containing initial logical part
      -> [String] -- ^ extra options
      -> IO String -- ^ formatted output of the goal
  showTPTPProblemM thName pst _opts = do
    let problem = generateTPTPProblem
                    (psLogicalPart pst)
                     Nothing
    return $ show $ printTPTPProblem thName problem
  
  {- |
    Pretty printing TPTP goal in TPTP format.
  -}
  ioShowTPTPProblem :: String -- ^ theory name
                    -> ProverState -- ^ prover state containing initial logical part
                    -> Named Sentence -- ^ goal to print
                    -> [String] -- ^ extra options
                    -> IO String -- ^ formatted output of the goal
  ioShowTPTPProblem theoryName proverState newGoal _ = do
    let problem = generateTPTPProblem
                    (psLogicalPart proverState)
                    (Just newGoal)
    return $ show $ printTPTPProblem theoryName problem
  
  -- Print a newline at the end of the document for good style.
  printTPTPProblem :: String -> PProblem -> Doc
  printTPTPProblem theoryName problem =
    text "% Problem: " <> text (identifier problem)
    $+$ text "% generated from the library " <> text theoryName
    $+$ vsep (map printNamedSentence $ sortBy sentenceOrder $ formulaeList $
               logicalPart problem)
    $+$ text ""
    where
      sentenceOrder :: Named Sentence -> Named Sentence -> Ordering
      sentenceOrder s t =
        case (formulaRole $ sentence s, formulaRole $ sentence t) of
          (Unknown, _) -> LT
          (Type, _) -> LT
          (Definition, _) -> LT
          (Conjecture, _) -> GT
          (_, _) -> EQ
  