content: {-# 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
      PLogic.Propositional
      PSL.PropSL
      PBasic.BASIC_SPEC
      PBasic.FORMULA
      PBasic.SYMB_ITEMS
      PBasic.SYMB_MAP_ITEMS
      PSign.Sign
      PMor.Morphism
      PSymbol.Symbol
      PSymbol.Symbol
      ProofTree
      QLogic.QBF
      QSL.QBFSL
      QBasic.BASICSPEC
      QBasic.FORMULA
      QBasic.SYMBITEMS
      QBasic.SYMBMAPITEMS
      PSign.Sign
      QMor.Morphism
      QSymbol.Symbol
      QSymbol.Symbol
      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
  mapSym :: PSymbol.Symbol -> Set.Set QSymbol.Symbol
  mapSym = Set.singleton . QSymbol.idToRaw . PSymbol.getSymbolName
  
  -- | 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
    PBasic.False_atom r -> QBasic.FalseAtom r
    PBasic.Predication t -> QBasic.Predication t
  