{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2CspCASL.hs
Copyright   :  (c) Till Mossakowski and Uni Bremen 2003
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  M.Roggenbach@swansea.ac.uk
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from CASL to CspCASL.
-}

module Comorphisms.CASL2CspCASL where

import Logic.Logic
import Logic.Comorphism
import Common.ProofTree

-- CASL
import CASL.AS_Basic_CASL
import CASL.Logic_CASL
import CASL.Morphism
import CASL.Sign
import CASL.Sublogic as SL

-- CspCASL
import CspCASL.Logic_CspCASL
import CspCASL.StatAnaCSP (CspBasicSpec)
import CspCASL.SignCSP
import CspCASL.Morphism (CspCASLMorphism, emptyCspAddMorphism)
import CspCASL.SymbItems
import CspCASL.Symbol

import qualified Data.Set as Set

-- | The identity of the comorphism
data CASL2CspCASL = CASL2CspCASL deriving (Int -> CASL2CspCASL -> ShowS
[CASL2CspCASL] -> ShowS
CASL2CspCASL -> String
(Int -> CASL2CspCASL -> ShowS)
-> (CASL2CspCASL -> String)
-> ([CASL2CspCASL] -> ShowS)
-> Show CASL2CspCASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2CspCASL] -> ShowS
$cshowList :: [CASL2CspCASL] -> ShowS
show :: CASL2CspCASL -> String
$cshow :: CASL2CspCASL -> String
showsPrec :: Int -> CASL2CspCASL -> ShowS
$cshowsPrec :: Int -> CASL2CspCASL -> ShowS
Show)

instance Language CASL2CspCASL -- default definition is okay

instance Comorphism CASL2CspCASL
    CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
        CASLSign CASLMor Symbol RawSymbol ProofTree
    CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems
        CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () where
    sourceLogic :: CASL2CspCASL -> CASL
sourceLogic CASL2CspCASL = CASL
CASL
    sourceSublogic :: CASL2CspCASL -> CASL_Sublogics
sourceSublogic CASL2CspCASL = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.top
    targetLogic :: CASL2CspCASL -> CspCASL
targetLogic CASL2CspCASL = CspCASL
cspCASL
    mapSublogic :: CASL2CspCASL -> CASL_Sublogics -> Maybe ()
mapSublogic CASL2CspCASL _ = () -> Maybe ()
forall a. a -> Maybe a
Just ()
    map_theory :: CASL2CspCASL
-> (CASLSign, [Named CASLFORMULA])
-> Result (CspCASLSign, [Named CspCASLSen])
map_theory CASL2CspCASL =
      (CspCASLSign, [Named CspCASLSen])
-> Result (CspCASLSign, [Named CspCASLSen])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CspCASLSign, [Named CspCASLSen])
 -> Result (CspCASLSign, [Named CspCASLSen]))
-> ((CASLSign, [Named CASLFORMULA])
    -> (CspCASLSign, [Named CspCASLSen]))
-> (CASLSign, [Named CASLFORMULA])
-> Result (CspCASLSign, [Named CspCASLSen])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CspSign
-> (CASLSign, [Named CASLFORMULA])
-> (CspCASLSign, [Named CspCASLSen])
forall e f1 e1 f.
e
-> (Sign f1 e1, [Named (FORMULA f1)])
-> (Sign f e, [Named (FORMULA f)])
embedCASLTheory CspSign
emptyCspSign
    map_symbol :: CASL2CspCASL -> CASLSign -> Symbol -> Set CspSymbol
map_symbol CASL2CspCASL _ = CspSymbol -> Set CspSymbol
forall a. a -> Set a
Set.singleton (CspSymbol -> Set CspSymbol)
-> (Symbol -> CspSymbol) -> Symbol -> Set CspSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> CspSymbol
caslToCspSymbol
    map_morphism :: CASL2CspCASL -> CASLMor -> Result CspCASLMorphism
map_morphism CASL2CspCASL =
      CspCASLMorphism -> Result CspCASLMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (CspCASLMorphism -> Result CspCASLMorphism)
-> (CASLMor -> CspCASLMorphism)
-> CASLMor
-> Result CspCASLMorphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CspSign -> CspAddMorphism -> CASLMor -> CspCASLMorphism
forall e m f1 e1 m1 f.
e -> m -> Morphism f1 e1 m1 -> Morphism f e m
mapCASLMor CspSign
emptyCspSign CspAddMorphism
emptyCspAddMorphism
    map_sentence :: CASL2CspCASL -> CASLSign -> CASLFORMULA -> Result CspCASLSen
map_sentence CASL2CspCASL _sig :: CASLSign
_sig = CspCASLSen -> Result CspCASLSen
forall (m :: * -> *) a. Monad m => a -> m a
return (CspCASLSen -> Result CspCASLSen)
-> (CASLFORMULA -> CspCASLSen) -> CASLFORMULA -> Result CspCASLSen
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> CspCASLSen
forall f1 f. FORMULA f1 -> FORMULA f
mapFORMULA
    has_model_expansion :: CASL2CspCASL -> Bool
has_model_expansion CASL2CspCASL = Bool
True
    is_weakly_amalgamable :: CASL2CspCASL -> Bool
is_weakly_amalgamable CASL2CspCASL = Bool
True
    isInclusionComorphism :: CASL2CspCASL -> Bool
isInclusionComorphism CASL2CspCASL = Bool
True