content: {- |
  Module      :  ./Propositional/ProverState.hs
  Description :  ProverState for propositional logic
  Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  luecke@informatik.uni-bremen.de
  Stability   :  experimental
  Portability :  portable
  
  Prover state for propositional logic
  -}
  
  module Propositional.ProverState
      where
  
  import qualified Common.AS_Annotation as AS_Anno
  import qualified Propositional.AS_BASIC_Propositional as AS
  import qualified Propositional.Sign as Sign
  import qualified Propositional.Morphism as PMorphism
  import qualified Common.ProofUtils as PUtil
  import qualified Logic.Prover as LP
  
  -- | Datatype for the prover state for propositional logic
  data PropProverState = PropProverState
      {
        initialAxioms :: [AS_Anno.Named AS.FORMULA]
      , initialSignature :: Sign.Sign
      , freeDefs :: [LP.FreeDefMorphism AS.FORMULA PMorphism.Morphism]
      } deriving (Show)
  
  -- | function to create prover state
  propProverState :: Sign.Sign                  -- Input Signature
                  -> [AS_Anno.Named AS.FORMULA] -- Input Formulae
                  -> [LP.FreeDefMorphism AS.FORMULA PMorphism.Morphism]
                  -- ^ free definitions
                  -> PropProverState
  propProverState sign aSens freedefs =
      let
          axioms = PUtil.prepareSenNames transSenName
                                         $ filter AS_Anno.isAxiom aSens
      in
        foldl insertSentence
        PropProverState
        {
          initialAxioms = []
        , initialSignature = sign
        , freeDefs = freedefs
        } axioms
  
  insertSentence :: PropProverState
                 -> AS_Anno.Named AS.FORMULA
                 -> PropProverState
  insertSentence pState frm =
      let
          sign = initialSignature pState
          axs = initialAxioms pState
          freedefs = freeDefs pState
      in
        PropProverState
        {
          initialAxioms = axs ++ [frm]
        , initialSignature = sign
        , freeDefs = freedefs
        }
  
  
  -- | Translation of Sentence names
  transSenName :: String -> String
  transSenName str = str
  