{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  $Header$
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.MS
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 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
      sourceSublogic ExtModal2OWL = mkTop maxSublogic
      targetLogic ExtModal2OWL = OWL2
      mapSublogic ExtModal2OWL _ = Just topS
      map_theory ExtModal2OWL = mapTheory
