{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/ExtModal2OWL.hs
Description :  Comorphism from ExtModal to OWL2
Copyright   :  (c) C. Maeder, DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

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

module Comorphisms.ExtModal2OWL where

import Logic.Logic as Logic
import Logic.Comorphism

import Common.ProofTree

-- OWL = codomain
import OWL2.Logic_OWL2
import OWL2.AS
import OWL2.ProfilesAndSublogics
import OWL2.ManchesterPrint ()
import OWL2.Morphism
import OWL2.Symbols
import OWL2.Sign as OS
import OWL2.CASL2OWL

-- ExtModal = domain
import ExtModal.Logic_ExtModal
import ExtModal.AS_ExtModal
import ExtModal.Sublogic

import CASL.Sign
import CASL.Morphism
import CASL.AS_Basic_CASL
import CASL.Sublogic

data ExtModal2OWL = ExtModal2OWL deriving Int -> ExtModal2OWL -> ShowS
[ExtModal2OWL] -> ShowS
ExtModal2OWL -> String
(Int -> ExtModal2OWL -> ShowS)
-> (ExtModal2OWL -> String)
-> ([ExtModal2OWL] -> ShowS)
-> Show ExtModal2OWL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExtModal2OWL] -> ShowS
$cshowList :: [ExtModal2OWL] -> ShowS
show :: ExtModal2OWL -> String
$cshow :: ExtModal2OWL -> String
showsPrec :: Int -> ExtModal2OWL -> ShowS
$cshowsPrec :: Int -> ExtModal2OWL -> ShowS
Show

instance Language ExtModal2OWL

instance Comorphism
    ExtModal2OWL        -- comorphism
    ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
    SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol ()
    OWL2            -- lid codomain
    ProfSub         -- sublogics codomain
    OntologyDocument -- Basic spec codomain
    Axiom           -- sentence codomain
    SymbItems       -- symbol items codomain
    SymbMapItems    -- symbol map items codomain
    OS.Sign         -- signature codomain
    OWLMorphism     -- morphism codomain
    Entity          -- symbol codomain
    RawSymb         -- rawsymbol codomain
    ProofTree       -- proof tree codomain
    where
      sourceLogic :: ExtModal2OWL -> ExtModal
sourceLogic ExtModal2OWL = ExtModal
ExtModal
      sourceSublogic :: ExtModal2OWL -> ExtModalSL
sourceSublogic ExtModal2OWL = Sublogic -> ExtModalSL
forall a. a -> CASL_SL a
mkTop Sublogic
maxSublogic
      targetLogic :: ExtModal2OWL -> OWL2
targetLogic ExtModal2OWL = OWL2
OWL2
      mapSublogic :: ExtModal2OWL -> ExtModalSL -> Maybe ProfSub
mapSublogic ExtModal2OWL _ = ProfSub -> Maybe ProfSub
forall a. a -> Maybe a
Just ProfSub
topS
      map_theory :: ExtModal2OWL
-> (ExtModalSign, [Named ExtModalFORMULA])
-> Result (Sign, [Named Axiom])
map_theory ExtModal2OWL = (ExtModalSign, [Named ExtModalFORMULA])
-> Result (Sign, [Named Axiom])
forall f e.
(FormExtension f, TermExtension f) =>
(Sign f e, [Named (FORMULA f)]) -> Result (Sign, [Named Axiom])
mapTheory