{- |
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
    {
      PropProverState -> [Named FORMULA]
initialAxioms :: [AS_Anno.Named AS.FORMULA]
    , PropProverState -> Sign
initialSignature :: Sign.Sign
    , PropProverState -> [FreeDefMorphism FORMULA Morphism]
freeDefs :: [LP.FreeDefMorphism AS.FORMULA PMorphism.Morphism]
    } deriving (Int -> PropProverState -> ShowS
[PropProverState] -> ShowS
PropProverState -> String
(Int -> PropProverState -> ShowS)
-> (PropProverState -> String)
-> ([PropProverState] -> ShowS)
-> Show PropProverState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PropProverState] -> ShowS
$cshowList :: [PropProverState] -> ShowS
show :: PropProverState -> String
$cshow :: PropProverState -> String
showsPrec :: Int -> PropProverState -> ShowS
$cshowsPrec :: Int -> PropProverState -> ShowS
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
-> [Named FORMULA]
-> [FreeDefMorphism FORMULA Morphism]
-> PropProverState
propProverState sign :: Sign
sign aSens :: [Named FORMULA]
aSens freedefs :: [FreeDefMorphism FORMULA Morphism]
freedefs =
    let
        axioms :: [Named FORMULA]
axioms = ShowS -> [Named FORMULA] -> [Named FORMULA]
forall a. ShowS -> [Named a] -> [Named a]
PUtil.prepareSenNames ShowS
transSenName
                                       ([Named FORMULA] -> [Named FORMULA])
-> [Named FORMULA] -> [Named FORMULA]
forall a b. (a -> b) -> a -> b
$ (Named FORMULA -> Bool) -> [Named FORMULA] -> [Named FORMULA]
forall a. (a -> Bool) -> [a] -> [a]
filter Named FORMULA -> Bool
forall s a. SenAttr s a -> Bool
AS_Anno.isAxiom [Named FORMULA]
aSens
    in
      (PropProverState -> Named FORMULA -> PropProverState)
-> PropProverState -> [Named FORMULA] -> PropProverState
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl PropProverState -> Named FORMULA -> PropProverState
insertSentence
      PropProverState :: [Named FORMULA]
-> Sign -> [FreeDefMorphism FORMULA Morphism] -> PropProverState
PropProverState
      {
        initialAxioms :: [Named FORMULA]
initialAxioms = []
      , initialSignature :: Sign
initialSignature = Sign
sign
      , freeDefs :: [FreeDefMorphism FORMULA Morphism]
freeDefs = [FreeDefMorphism FORMULA Morphism]
freedefs
      } [Named FORMULA]
axioms

insertSentence :: PropProverState
               -> AS_Anno.Named AS.FORMULA
               -> PropProverState
insertSentence :: PropProverState -> Named FORMULA -> PropProverState
insertSentence pState :: PropProverState
pState frm :: Named FORMULA
frm =
    let
        sign :: Sign
sign = PropProverState -> Sign
initialSignature PropProverState
pState
        axs :: [Named FORMULA]
axs = PropProverState -> [Named FORMULA]
initialAxioms PropProverState
pState
        freedefs :: [FreeDefMorphism FORMULA Morphism]
freedefs = PropProverState -> [FreeDefMorphism FORMULA Morphism]
freeDefs PropProverState
pState
    in
      PropProverState :: [Named FORMULA]
-> Sign -> [FreeDefMorphism FORMULA Morphism] -> PropProverState
PropProverState
      {
        initialAxioms :: [Named FORMULA]
initialAxioms = [Named FORMULA]
axs [Named FORMULA] -> [Named FORMULA] -> [Named FORMULA]
forall a. [a] -> [a] -> [a]
++ [Named FORMULA
frm]
      , initialSignature :: Sign
initialSignature = Sign
sign
      , freeDefs :: [FreeDefMorphism FORMULA Morphism]
freeDefs = [FreeDefMorphism FORMULA Morphism]
freedefs
      }


-- | Translation of Sentence names
transSenName :: String -> String
transSenName :: ShowS
transSenName str :: String
str = String
str