Prop2QBF.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
{-# LANGUAGE MultiParamTypeClasses #-}
{- |
Module : ./Comorphisms/Prop2QBF.hs
Description : Comorphism from Propositional to QBF
Copyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : <jonathan.von_schroeder@dfki.de>
Stability : experimental
Portability : non-portable (imports Logic.Logic)
-}
module Comorphisms.Prop2QBF (Prop2QBF (..)) where
import Common.ProofTree
import Logic.Logic
import Logic.Comorphism
-- Propositional
import qualified Propositional.Logic_Propositional as PLogic
import qualified Propositional.AS_BASIC_Propositional as PBasic
import qualified Propositional.Sublogic as PSL
import qualified Propositional.Sign as PSign
import qualified Propositional.Morphism as PMor
import qualified Propositional.Symbol as PSymbol
-- QBF
import qualified QBF.Logic_QBF as QLogic
import qualified QBF.AS_BASIC_QBF as QBasic
import qualified QBF.Sublogic as QSL
import qualified QBF.Morphism as QMor
import qualified QBF.Symbol as QSymbol
import qualified Data.Set as Set
import Common.AS_Annotation
import Common.Result
-- | lid of the morphism
data Prop2QBF = Prop2QBF deriving Show
instance Language Prop2QBF where
language_name Prop2QBF = "Propositional2QBF"
instance Comorphism Prop2QBF
ProofTree
ProofTree
where
sourceLogic Prop2QBF = PLogic.Propositional
sourceSublogic Prop2QBF = PSL.top
targetLogic Prop2QBF = QLogic.QBF
mapSublogic Prop2QBF _ = Nothing
map_theory Prop2QBF = mapTheory
is_model_transportable Prop2QBF = True
map_symbol Prop2QBF _ = mapSym
map_sentence Prop2QBF _ = trForm
map_morphism Prop2QBF = mapMor
has_model_expansion Prop2QBF = True
is_weakly_amalgamable Prop2QBF = True
isInclusionComorphism Prop2QBF = True
-- | Translation of the signature
mapSig :: PSign.Sign -> PSign.Sign
mapSig = id
-- | Translation of morphisms
mapMor :: PMor.Morphism -> Result QMor.Morphism
mapMor mor = return QMor.Morphism
{ QMor.source = PMor.source mor
, QMor.target = PMor.target mor
, QMor.propMap = PMor.propMap mor }
-- | Mapping of a theory
mapTheory :: (PSign.Sign, [Named PBasic.FORMULA])
-> Result (PSign.Sign, [Named QBasic.FORMULA])
mapTheory (sig, form) = do
form_ <- mapM (mapNamedM trForm) form
return (mapSig sig, form_)
-- | Translation of symbols
-- | Helper for map sentence and map theory
trForm :: PBasic.FORMULA -> Result QBasic.FORMULA
trForm = return . trForm_
trForm_ :: PBasic.FORMULA -> QBasic.FORMULA
trForm_ form = case form of
PBasic.Negation f r -> QBasic.Negation (trForm_ f) r
PBasic.Conjunction fs r -> QBasic.Conjunction (map trForm_ fs) r
PBasic.Disjunction fs r -> QBasic.Disjunction (map trForm_ fs) r
PBasic.Implication f1 f2 r -> QBasic.Implication (trForm_ f1) (trForm_ f2) r
PBasic.Equivalence f1 f2 r -> QBasic.Equivalence (trForm_ f1) (trForm_ f2) r
PBasic.True_atom r -> QBasic.TrueAtom r