hets/Propositional/ProverState.hs

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