{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2VSE.hs
Description :  embedding from CASL to VSE
Copyright   :  (c) C. Maeder, DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from CASL to VSE.
-}

module Comorphisms.CASL2VSE (CASL2VSE (..)) where

import qualified Data.Set as Set

import Logic.Logic
import Logic.Comorphism

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

import VSE.Logic_VSE
import VSE.As
import VSE.Ana

import Common.ProofTree

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

instance Language CASL2VSE -- default definition is okay

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