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