{-# 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 Int -> Prop2QBF -> ShowS
[Prop2QBF] -> ShowS
Prop2QBF -> String
(Int -> Prop2QBF -> ShowS)
-> (Prop2QBF -> String) -> ([Prop2QBF] -> ShowS) -> Show Prop2QBF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Prop2QBF] -> ShowS
$cshowList :: [Prop2QBF] -> ShowS
show :: Prop2QBF -> String
$cshow :: Prop2QBF -> String
showsPrec :: Int -> Prop2QBF -> ShowS
$cshowsPrec :: Int -> Prop2QBF -> ShowS
Show

instance Language Prop2QBF where
  language_name :: Prop2QBF -> String
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 -> Propositional
sourceLogic Prop2QBF = Propositional
PLogic.Propositional
      sourceSublogic :: Prop2QBF -> PropSL
sourceSublogic Prop2QBF = PropSL
PSL.top
      targetLogic :: Prop2QBF -> QBF
targetLogic Prop2QBF = QBF
QLogic.QBF
      mapSublogic :: Prop2QBF -> PropSL -> Maybe QBFSL
mapSublogic Prop2QBF _ = Maybe QBFSL
forall a. Maybe a
Nothing
      map_theory :: Prop2QBF
-> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA])
map_theory Prop2QBF = (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA])
mapTheory
      is_model_transportable :: Prop2QBF -> Bool
is_model_transportable Prop2QBF = Bool
True
      map_symbol :: Prop2QBF -> Sign -> Symbol -> Set Symbol
map_symbol Prop2QBF _ = Symbol -> Set Symbol
mapSym
      map_sentence :: Prop2QBF -> Sign -> FORMULA -> Result FORMULA
map_sentence Prop2QBF _ = FORMULA -> Result FORMULA
trForm
      map_morphism :: Prop2QBF -> Morphism -> Result Morphism
map_morphism Prop2QBF = Morphism -> Result Morphism
mapMor
      has_model_expansion :: Prop2QBF -> Bool
has_model_expansion Prop2QBF = Bool
True
      is_weakly_amalgamable :: Prop2QBF -> Bool
is_weakly_amalgamable Prop2QBF = Bool
True
      isInclusionComorphism :: Prop2QBF -> Bool
isInclusionComorphism Prop2QBF = Bool
True

-- | Translation of the signature
mapSig :: PSign.Sign -> PSign.Sign
mapSig :: Sign -> Sign
mapSig = Sign -> Sign
forall a. a -> a
id

-- | Translation of morphisms
mapMor :: PMor.Morphism -> Result QMor.Morphism
mapMor :: Morphism -> Result Morphism
mapMor mor :: Morphism
mor = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism :: Sign -> Sign -> Map Id Id -> Morphism
QMor.Morphism
  { source :: Sign
QMor.source = Morphism -> Sign
PMor.source Morphism
mor
  , target :: Sign
QMor.target = Morphism -> Sign
PMor.target Morphism
mor
  , propMap :: Map Id Id
QMor.propMap = Morphism -> Map Id Id
PMor.propMap Morphism
mor }

-- | Mapping of a theory
mapTheory :: (PSign.Sign, [Named PBasic.FORMULA])
  -> Result (PSign.Sign, [Named QBasic.FORMULA])
mapTheory :: (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA])
mapTheory (sig :: Sign
sig, form :: [Named FORMULA]
form) = do
                          [Named FORMULA]
form_ <- (Named FORMULA -> Result (Named FORMULA))
-> [Named FORMULA] -> Result [Named FORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((FORMULA -> Result FORMULA)
-> Named FORMULA -> Result (Named FORMULA)
forall (m :: * -> *) s t.
Monad m =>
(s -> m t) -> Named s -> m (Named t)
mapNamedM FORMULA -> Result FORMULA
trForm) [Named FORMULA]
form
                          (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Sign
mapSig Sign
sig, [Named FORMULA]
form_)

-- | Translation of symbols
mapSym :: PSymbol.Symbol -> Set.Set QSymbol.Symbol
mapSym :: Symbol -> Set Symbol
mapSym = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Symbol
QSymbol.idToRaw (Id -> Symbol) -> (Symbol -> Id) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Id
PSymbol.getSymbolName

-- | Helper for map sentence and map theory
trForm :: PBasic.FORMULA -> Result QBasic.FORMULA
trForm :: FORMULA -> Result FORMULA
trForm = FORMULA -> Result FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> Result FORMULA)
-> (FORMULA -> FORMULA) -> FORMULA -> Result FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
trForm_

trForm_ :: PBasic.FORMULA -> QBasic.FORMULA
trForm_ :: FORMULA -> FORMULA
trForm_ form :: FORMULA
form = case FORMULA
form of
  PBasic.Negation f :: FORMULA
f r :: Range
r -> FORMULA -> Range -> FORMULA
QBasic.Negation (FORMULA -> FORMULA
trForm_ FORMULA
f) Range
r
  PBasic.Conjunction fs :: [FORMULA]
fs r :: Range
r -> [FORMULA] -> Range -> FORMULA
QBasic.Conjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
trForm_ [FORMULA]
fs) Range
r
  PBasic.Disjunction fs :: [FORMULA]
fs r :: Range
r -> [FORMULA] -> Range -> FORMULA
QBasic.Disjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
trForm_ [FORMULA]
fs) Range
r
  PBasic.Implication f1 :: FORMULA
f1 f2 :: FORMULA
f2 r :: Range
r -> FORMULA -> FORMULA -> Range -> FORMULA
QBasic.Implication (FORMULA -> FORMULA
trForm_ FORMULA
f1) (FORMULA -> FORMULA
trForm_ FORMULA
f2) Range
r
  PBasic.Equivalence f1 :: FORMULA
f1 f2 :: FORMULA
f2 r :: Range
r -> FORMULA -> FORMULA -> Range -> FORMULA
QBasic.Equivalence (FORMULA -> FORMULA
trForm_ FORMULA
f1) (FORMULA -> FORMULA
trForm_ FORMULA
f2) Range
r
  PBasic.True_atom r :: Range
r -> Range -> FORMULA
QBasic.TrueAtom Range
r
  PBasic.False_atom r :: Range
r -> Range -> FORMULA
QBasic.FalseAtom Range
r
  PBasic.Predication t :: Token
t -> Token -> FORMULA
QBasic.Predication Token
t