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

instance Language QBF2Prop where
  language_name :: QBF2Prop -> String
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 -> QBF
sourceLogic QBF2Prop = QBF
QLogic.QBF
      sourceSublogic :: QBF2Prop -> QBFSL
sourceSublogic QBF2Prop = QBFSL
QSL.top
      targetLogic :: QBF2Prop -> Propositional
targetLogic QBF2Prop = Propositional
PLogic.Propositional
      mapSublogic :: QBF2Prop -> QBFSL -> Maybe PropSL
mapSublogic QBF2Prop _ = PropSL -> Maybe PropSL
forall a. a -> Maybe a
Just PropSL
PSL.top
      map_theory :: QBF2Prop
-> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA])
map_theory QBF2Prop = (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA])
mapTheory
      is_model_transportable :: QBF2Prop -> Bool
is_model_transportable QBF2Prop = Bool
True
      map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol
map_symbol QBF2Prop _ = Symbol -> Set Symbol
mapSym
      map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA
map_sentence QBF2Prop _ = FORMULA -> Result FORMULA
trForm
      map_morphism :: QBF2Prop -> Morphism -> Result Morphism
map_morphism QBF2Prop = Morphism -> Result Morphism
mapMor
      has_model_expansion :: QBF2Prop -> Bool
has_model_expansion QBF2Prop = Bool
True
      is_weakly_amalgamable :: QBF2Prop -> Bool
is_weakly_amalgamable QBF2Prop = Bool
True
      isInclusionComorphism :: QBF2Prop -> Bool
isInclusionComorphism QBF2Prop = 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 :: QMor.Morphism -> Result PMor.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
PMor.Morphism
  { source :: Sign
PMor.source = Morphism -> Sign
QMor.source Morphism
mor
  , target :: Sign
PMor.target = Morphism -> Sign
QMor.target Morphism
mor
  , propMap :: Map Id Id
PMor.propMap = Morphism -> Map Id Id
QMor.propMap Morphism
mor }

-- | Mapping of a theory
mapTheory :: (PSign.Sign, [Named QBasic.FORMULA])
  -> Result (PSign.Sign, [Named PBasic.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 :: QSymbol.Symbol -> Set.Set PSymbol.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
PSymbol.idToRaw (Id -> Symbol) -> (Symbol -> Id) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Id
QSymbol.getSymbolName

-- | Helper for map sentence and map theory
trForm :: QBasic.FORMULA -> Result PBasic.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_ :: QBasic.FORMULA -> PBasic.FORMULA
trForm_ :: FORMULA -> FORMULA
trForm_ form :: FORMULA
form = case FORMULA
form of
  QBasic.Negation f :: FORMULA
f r :: Range
r -> FORMULA -> Range -> FORMULA
PBasic.Negation (FORMULA -> FORMULA
trForm_ FORMULA
f) Range
r
  QBasic.Conjunction fs :: [FORMULA]
fs r :: Range
r -> [FORMULA] -> Range -> FORMULA
PBasic.Conjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
trForm_ [FORMULA]
fs) Range
r
  QBasic.Disjunction fs :: [FORMULA]
fs r :: Range
r -> [FORMULA] -> Range -> FORMULA
PBasic.Disjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
trForm_ [FORMULA]
fs) Range
r
  QBasic.Implication f1 :: FORMULA
f1 f2 :: FORMULA
f2 r :: Range
r -> FORMULA -> FORMULA -> Range -> FORMULA
PBasic.Implication (FORMULA -> FORMULA
trForm_ FORMULA
f1) (FORMULA -> FORMULA
trForm_ FORMULA
f2) Range
r
  QBasic.Equivalence f1 :: FORMULA
f1 f2 :: FORMULA
f2 r :: Range
r -> FORMULA -> FORMULA -> Range -> FORMULA
PBasic.Equivalence (FORMULA -> FORMULA
trForm_ FORMULA
f1) (FORMULA -> FORMULA
trForm_ FORMULA
f2) Range
r
  QBasic.TrueAtom r :: Range
r -> Range -> FORMULA
PBasic.True_atom Range
r
  QBasic.FalseAtom r :: Range
r -> Range -> FORMULA
PBasic.False_atom Range
r
  QBasic.Predication t :: Token
t -> Token -> FORMULA
PBasic.Predication Token
t
  QBasic.ForAll [] f :: FORMULA
f _ -> FORMULA -> FORMULA
trForm_ FORMULA
f
  QBasic.ForAll (t :: Token
t : ts :: [Token]
ts) f :: FORMULA
f r :: Range
r -> [FORMULA] -> Range -> FORMULA
PBasic.Conjunction
    ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA -> FORMULA
trForm_ (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> Token -> FORMULA -> FORMULA
replacePred ([Token] -> FORMULA -> Range -> FORMULA
QBasic.ForAll [Token]
ts FORMULA
f Range
r) Token
t)
    [Range -> FORMULA
QBasic.TrueAtom Range
r, Range -> FORMULA
QBasic.FalseAtom Range
r]) Range
r
  QBasic.Exists [] f :: FORMULA
f _ -> FORMULA -> FORMULA
trForm_ FORMULA
f
  QBasic.Exists (t :: Token
t : ts :: [Token]
ts) f :: FORMULA
f r :: Range
r -> [FORMULA] -> Range -> FORMULA
PBasic.Disjunction
    ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA -> FORMULA
trForm_ (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> Token -> FORMULA -> FORMULA
replacePred ([Token] -> FORMULA -> Range -> FORMULA
QBasic.Exists [Token]
ts FORMULA
f Range
r) Token
t)
    [Range -> FORMULA
QBasic.TrueAtom Range
r, Range -> FORMULA
QBasic.FalseAtom Range
r]) Range
r

-- | Helper for trForm
replacePred :: QBasic.FORMULA -> Token -> QBasic.FORMULA -> QBasic.FORMULA
replacePred :: FORMULA -> Token -> FORMULA -> FORMULA
replacePred f :: FORMULA
f s :: Token
s r :: FORMULA
r = FoldRecord FORMULA -> FORMULA -> FORMULA
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord FORMULA
mapRecord {
  foldPredication :: Token -> FORMULA
foldPredication = \ t :: Token
t -> if Token
t Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
s then FORMULA
r else
    Token -> FORMULA
QBasic.Predication Token
t } FORMULA
f