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