content: {-# LANGUAGE MultiParamTypeClasses #-}
  {- |
  Module      :  ./Comorphisms/QBF2Prop.hs
  Description :  Comorphism from QBF to Propositional
  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.QBF2Prop (QBF2Prop (..)) 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 QBF.Tools
  
  import qualified Data.Set as Set
  import Common.AS_Annotation
  import Common.Id
  import Common.Result
  
  -- | lid of the morphism
  data QBF2Prop = QBF2Prop deriving Show
  
  instance Language QBF2Prop where
    language_name QBF2Prop = "QBF2Propositional"
  
  instance Comorphism QBF2Prop
      QLogic.QBF
      QSL.QBFSL
      QBasic.BASICSPEC
      QBasic.FORMULA
      QBasic.SYMBITEMS
      QBasic.SYMBMAPITEMS
      PSign.Sign
      QMor.Morphism
      QSymbol.Symbol
      QSymbol.Symbol
      ProofTree
      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
      where
        sourceLogic QBF2Prop = QLogic.QBF
        sourceSublogic QBF2Prop = QSL.top
        targetLogic QBF2Prop = PLogic.Propositional
        mapSublogic QBF2Prop _ = Just PSL.top
        map_theory QBF2Prop = mapTheory
        is_model_transportable QBF2Prop = True
        map_symbol QBF2Prop _ = mapSym
        map_sentence QBF2Prop _ = trForm
        map_morphism QBF2Prop = mapMor
        has_model_expansion QBF2Prop = True
        is_weakly_amalgamable QBF2Prop = True
        isInclusionComorphism QBF2Prop = True
  
  -- | Translation of the signature
  mapSig :: PSign.Sign -> PSign.Sign
  mapSig = id
  
  -- | Translation of morphisms
  mapMor :: QMor.Morphism -> Result PMor.Morphism
  mapMor mor = return PMor.Morphism
    { PMor.source = QMor.source mor
    , PMor.target = QMor.target mor
    , PMor.propMap = QMor.propMap mor }
  
  -- | Mapping of a theory
  mapTheory :: (PSign.Sign, [Named QBasic.FORMULA])
    -> Result (PSign.Sign, [Named PBasic.FORMULA])
  mapTheory (sig, form) = do
                            form_ <- mapM (mapNamedM trForm) form
                            return (mapSig sig, form_)
  
  -- | Translation of symbols
  mapSym :: QSymbol.Symbol -> Set.Set PSymbol.Symbol
  mapSym = Set.singleton . PSymbol.idToRaw . QSymbol.getSymbolName
  
  -- | Helper for map sentence and map theory
  trForm :: QBasic.FORMULA -> Result PBasic.FORMULA
  trForm = return . trForm_
  
  trForm_ :: QBasic.FORMULA -> PBasic.FORMULA
  trForm_ form = case form of
    QBasic.Negation f r -> PBasic.Negation (trForm_ f) r
    QBasic.Conjunction fs r -> PBasic.Conjunction (map trForm_ fs) r
    QBasic.Disjunction fs r -> PBasic.Disjunction (map trForm_ fs) r
    QBasic.Implication f1 f2 r -> PBasic.Implication (trForm_ f1) (trForm_ f2) r
    QBasic.Equivalence f1 f2 r -> PBasic.Equivalence (trForm_ f1) (trForm_ f2) r
    QBasic.TrueAtom r -> PBasic.True_atom r
    QBasic.FalseAtom r -> PBasic.False_atom r
    QBasic.Predication t -> PBasic.Predication t
    QBasic.ForAll [] f _ -> trForm_ f
    QBasic.ForAll (t : ts) f r -> PBasic.Conjunction
      (map (trForm_ . replacePred (QBasic.ForAll ts f r) t)
      [QBasic.TrueAtom r, QBasic.FalseAtom r]) r
    QBasic.Exists [] f _ -> trForm_ f
    QBasic.Exists (t : ts) f r -> PBasic.Disjunction
      (map (trForm_ . replacePred (QBasic.Exists ts f r) t)
      [QBasic.TrueAtom r, QBasic.FalseAtom r]) r
  
  -- | Helper for trForm
  replacePred :: QBasic.FORMULA -> Token -> QBasic.FORMULA -> QBasic.FORMULA
  replacePred f s r = foldFormula mapRecord {
    foldPredication = \ t -> if t == s then r else
      QBasic.Predication t } f
  