Prop2CASL.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
{- |
Module : $Header$
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
-- | lid of the morphism
data Prop2CASL = Prop2CASL deriving Show
instance Language Prop2CASL where
language_name Prop2CASL = "Propositional2CASL"
instance Comorphism Prop2CASL
ProofTree
ProofTree
where
sourceLogic Prop2CASL = PLogic.Propositional
sourceSublogic Prop2CASL = PSL.top
targetLogic Prop2CASL = CLogic.CASL
mapSublogic Prop2CASL = Just . mapSub
map_theory Prop2CASL = mapTheory
is_model_transportable Prop2CASL = True
map_symbol Prop2CASL _ = mapSym
map_sentence Prop2CASL = mapSentence
map_morphism Prop2CASL = mapMor
has_model_expansion Prop2CASL = True
is_weakly_amalgamable Prop2CASL = True
isInclusionComorphism Prop2CASL = True