{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
License     :  GPLv2 or higher, see LICENSE.txt

Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from CASL to HybridCASL.

-}

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

-- HybridCASL
import Hybrid.Logic_Hybrid
import Hybrid.AS_Hybrid
import Hybrid.HybridSign

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

instance Language CASL2Hybrid -- default definition is okay

instance Comorphism CASL2Hybrid
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               Hybrid ()
               H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               HSign
               HybridMor
               Symbol RawSymbol () where
    sourceLogic :: CASL2Hybrid -> CASL
sourceLogic CASL2Hybrid = CASL
CASL
    sourceSublogic :: CASL2Hybrid -> CASL_Sublogics
sourceSublogic CASL2Hybrid = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.top
    targetLogic :: CASL2Hybrid -> Hybrid
targetLogic CASL2Hybrid = Hybrid
Hybrid
    mapSublogic :: CASL2Hybrid -> CASL_Sublogics -> Maybe ()
mapSublogic CASL2Hybrid _ = () -> Maybe ()
forall a. a -> Maybe a
Just ()
    map_theory :: CASL2Hybrid
-> (CASLSign, [Named CASLFORMULA])
-> Result (HSign, [Named HybridFORMULA])
map_theory CASL2Hybrid = (HSign, [Named HybridFORMULA])
-> Result (HSign, [Named HybridFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return ((HSign, [Named HybridFORMULA])
 -> Result (HSign, [Named HybridFORMULA]))
-> ((CASLSign, [Named CASLFORMULA])
    -> (HSign, [Named HybridFORMULA]))
-> (CASLSign, [Named CASLFORMULA])
-> Result (HSign, [Named HybridFORMULA])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HybridSign
-> (CASLSign, [Named CASLFORMULA])
-> (HSign, [Named HybridFORMULA])
forall e f1 e1 f.
e
-> (Sign f1 e1, [Named (FORMULA f1)])
-> (Sign f e, [Named (FORMULA f)])
embedCASLTheory HybridSign
emptyHybridSign
    map_morphism :: CASL2Hybrid -> CASLMor -> Result HybridMor
map_morphism CASL2Hybrid = HybridMor -> Result HybridMor
forall (m :: * -> *) a. Monad m => a -> m a
return (HybridMor -> Result HybridMor)
-> (CASLMor -> HybridMor) -> CASLMor -> Result HybridMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HybridSign -> DefMorExt HybridSign -> CASLMor -> HybridMor
forall e m f1 e1 m1 f.
e -> m -> Morphism f1 e1 m1 -> Morphism f e m
mapCASLMor HybridSign
emptyHybridSign DefMorExt HybridSign
forall e. DefMorExt e
emptyMorExt
    map_sentence :: CASL2Hybrid -> CASLSign -> CASLFORMULA -> Result HybridFORMULA
map_sentence CASL2Hybrid _ = HybridFORMULA -> Result HybridFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (HybridFORMULA -> Result HybridFORMULA)
-> (CASLFORMULA -> HybridFORMULA)
-> CASLFORMULA
-> Result HybridFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> HybridFORMULA
forall f1 f. FORMULA f1 -> FORMULA f
mapFORMULA
    map_symbol :: CASL2Hybrid -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2Hybrid _ = 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 :: CASL2Hybrid -> Bool
has_model_expansion CASL2Hybrid = Bool
True
    is_weakly_amalgamable :: CASL2Hybrid -> Bool
is_weakly_amalgamable CASL2Hybrid = Bool
True
    isInclusionComorphism :: CASL2Hybrid -> Bool
isInclusionComorphism CASL2Hybrid = Bool
True