{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2CoCASL.hs
Description :  embedding from CASL to CoCASL
Copyright   :  (c) Till Mossakowski and Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

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

The embedding comorphism from CASL to CoCASL.

-}

module Comorphisms.CASL2CoCASL where

import Logic.Logic
import Logic.Comorphism
import qualified Data.Set as Set
import Common.ProofTree

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

-- CoCASLCASL
import CoCASL.Logic_CoCASL
import CoCASL.AS_CoCASL
import CoCASL.CoCASLSign
import CoCASL.StatAna (CSign)
import CoCASL.Sublogic

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

instance Language CASL2CoCASL -- default definition is okay

instance Comorphism CASL2CoCASL
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               CoCASL CoCASL_Sublogics
               C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CSign
               CoCASLMor
               Symbol RawSymbol () where
    sourceLogic :: CASL2CoCASL -> CASL
sourceLogic CASL2CoCASL = CASL
CASL
    sourceSublogic :: CASL2CoCASL -> CASL_Sublogics
sourceSublogic CASL2CoCASL = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.top
    targetLogic :: CASL2CoCASL -> CoCASL
targetLogic CASL2CoCASL = CoCASL
CoCASL
    mapSublogic :: CASL2CoCASL -> CASL_Sublogics -> Maybe CoCASL_Sublogics
mapSublogic CASL2CoCASL s :: CASL_Sublogics
s = CoCASL_Sublogics -> Maybe CoCASL_Sublogics
forall a. a -> Maybe a
Just (CoCASL_Sublogics -> Maybe CoCASL_Sublogics)
-> CoCASL_Sublogics -> Maybe CoCASL_Sublogics
forall a b. (a -> b) -> a -> b
$ CASL_Sublogics
s { ext_features :: Bool
ext_features = Bool
False }

    map_theory :: CASL2CoCASL
-> (CASLSign, [Named CASLFORMULA])
-> Result (CSign, [Named CoCASLFORMULA])
map_theory CASL2CoCASL = (CSign, [Named CoCASLFORMULA])
-> Result (CSign, [Named CoCASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CSign, [Named CoCASLFORMULA])
 -> Result (CSign, [Named CoCASLFORMULA]))
-> ((CASLSign, [Named CASLFORMULA])
    -> (CSign, [Named CoCASLFORMULA]))
-> (CASLSign, [Named CASLFORMULA])
-> Result (CSign, [Named CoCASLFORMULA])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoCASLSign
-> (CASLSign, [Named CASLFORMULA])
-> (CSign, [Named CoCASLFORMULA])
forall e f1 e1 f.
e
-> (Sign f1 e1, [Named (FORMULA f1)])
-> (Sign f e, [Named (FORMULA f)])
embedCASLTheory CoCASLSign
emptyCoCASLSign
    map_morphism :: CASL2CoCASL -> CASLMor -> Result CoCASLMor
map_morphism CASL2CoCASL = CoCASLMor -> Result CoCASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return (CoCASLMor -> Result CoCASLMor)
-> (CASLMor -> CoCASLMor) -> CASLMor -> Result CoCASLMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoCASLSign -> DefMorExt CoCASLSign -> CASLMor -> CoCASLMor
forall e m f1 e1 m1 f.
e -> m -> Morphism f1 e1 m1 -> Morphism f e m
mapCASLMor CoCASLSign
emptyCoCASLSign DefMorExt CoCASLSign
forall e. DefMorExt e
emptyMorExt
    map_sentence :: CASL2CoCASL -> CASLSign -> CASLFORMULA -> Result CoCASLFORMULA
map_sentence CASL2CoCASL _ = CoCASLFORMULA -> Result CoCASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CoCASLFORMULA -> Result CoCASLFORMULA)
-> (CASLFORMULA -> CoCASLFORMULA)
-> CASLFORMULA
-> Result CoCASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> CoCASLFORMULA
forall f1 f. FORMULA f1 -> FORMULA f
mapFORMULA
    map_symbol :: CASL2CoCASL -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2CoCASL _ = 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
. Symbol -> Symbol
forall a. a -> a
id
    has_model_expansion :: CASL2CoCASL -> Bool
has_model_expansion CASL2CoCASL = Bool
True
    is_weakly_amalgamable :: CASL2CoCASL -> Bool
is_weakly_amalgamable CASL2CoCASL = Bool
True
    isInclusionComorphism :: CASL2CoCASL -> Bool
isInclusionComorphism CASL2CoCASL = Bool
True