{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/Prop2CASL.hs
Description :  Coding of Propositional into CASL
Copyright   :  (c) Dominik Luecke and Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

The translating comorphism from Propositional to CASL.
-}

module Comorphisms.Prop2CASL
    (
     Prop2CASL (..)
    )
    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

-- CASL
import qualified CASL.Logic_CASL as CLogic
import qualified CASL.AS_Basic_CASL as CBasic
import qualified CASL.Sublogic as CSL
import qualified CASL.Sign as CSign
import qualified CASL.Morphism as CMor
import Propositional.Prop2CASLHelpers

-- | lid of the morphism
data Prop2CASL = Prop2CASL deriving Int -> Prop2CASL -> ShowS
[Prop2CASL] -> ShowS
Prop2CASL -> String
(Int -> Prop2CASL -> ShowS)
-> (Prop2CASL -> String)
-> ([Prop2CASL] -> ShowS)
-> Show Prop2CASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Prop2CASL] -> ShowS
$cshowList :: [Prop2CASL] -> ShowS
show :: Prop2CASL -> String
$cshow :: Prop2CASL -> String
showsPrec :: Int -> Prop2CASL -> ShowS
$cshowsPrec :: Int -> Prop2CASL -> ShowS
Show

instance Language Prop2CASL where
  language_name :: Prop2CASL -> String
language_name Prop2CASL = "Propositional2CASL"

instance Comorphism Prop2CASL
    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
    CLogic.CASL
    CSL.CASL_Sublogics
    CLogic.CASLBasicSpec
    CBasic.CASLFORMULA
    CBasic.SYMB_ITEMS
    CBasic.SYMB_MAP_ITEMS
    CSign.CASLSign
    CMor.CASLMor
    CSign.Symbol
    CMor.RawSymbol
    ProofTree
    where
      sourceLogic :: Prop2CASL -> Propositional
sourceLogic Prop2CASL = Propositional
PLogic.Propositional
      sourceSublogic :: Prop2CASL -> PropSL
sourceSublogic Prop2CASL = PropSL
PSL.top
      targetLogic :: Prop2CASL -> CASL
targetLogic Prop2CASL = CASL
CLogic.CASL
      mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics
mapSublogic Prop2CASL = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just (CASL_Sublogics -> Maybe CASL_Sublogics)
-> (PropSL -> CASL_Sublogics) -> PropSL -> Maybe CASL_Sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropSL -> CASL_Sublogics
mapSub
      map_theory :: Prop2CASL
-> (Sign, [Named FORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory Prop2CASL = (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory
      is_model_transportable :: Prop2CASL -> Bool
is_model_transportable Prop2CASL = Bool
True
      map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol
map_symbol Prop2CASL _ = Symbol -> Set Symbol
mapSym
      map_sentence :: Prop2CASL -> Sign -> FORMULA -> Result CASLFORMULA
map_sentence Prop2CASL = Sign -> FORMULA -> Result CASLFORMULA
mapSentence
      map_morphism :: Prop2CASL -> Morphism -> Result CASLMor
map_morphism Prop2CASL = Morphism -> Result CASLMor
mapMor
      has_model_expansion :: Prop2CASL -> Bool
has_model_expansion Prop2CASL = Bool
True
      is_weakly_amalgamable :: Prop2CASL -> Bool
is_weakly_amalgamable Prop2CASL = Bool
True
      isInclusionComorphism :: Prop2CASL -> Bool
isInclusionComorphism Prop2CASL = Bool
True