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