{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  $Header$
Description :  Comorphism from Propostional Logic to OWL 2
Copyright   :  (c) Felix Gabriel Mance
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  f.mance@jacobs-university.de
Stability   :  provisional
Portability :  non-portable (via Logic.Logic)
-}

module OWL2.Propositional2OWL2 where

import Common.ProofTree
import Logic.Logic
import Logic.Comorphism

import Common.AS_Annotation
import Common.Id
import Common.Result

import OWL2.AS
import OWL2.Keywords
import OWL2.MS
import qualified OWL2.Morphism as OWLMor
import qualified OWL2.ProfilesAndSublogics as OWLSub
import qualified OWL2.Sign as OWLSign
import qualified OWL2.Logic_OWL2 as OWLLogic
import qualified OWL2.Symbols as OWLSym

import qualified Propositional.Logic_Propositional as PLogic
import Propositional.AS_BASIC_Propositional
import qualified Propositional.Sublogic as PSL
import qualified Propositional.Sign as PSign
import qualified Propositional.Morphism as PMor
import qualified Propositional.Symbol as PSymbol

import qualified Data.Set as Set

data Propositional2OWL2 = Propositional2OWL2 deriving Show

instance Language Propositional2OWL2

instance Comorphism Propositional2OWL2
    PLogic.Propositional
    PSL.PropSL
    BASIC_SPEC
    FORMULA
    SYMB_ITEMS
    SYMB_MAP_ITEMS
    PSign.Sign
    PMor.Morphism
    PSymbol.Symbol
    PSymbol.Symbol
    ProofTree
    OWLLogic.OWL2
    OWLSub.ProfSub
    OntologyDocument
    Axiom
    OWLSym.SymbItems
    OWLSym.SymbMapItems
    OWLSign.Sign
    OWLMor.OWLMorphism
    Entity
    OWLSym.RawSymb
    ProofTree
    where
        sourceLogic Propositional2OWL2 = PLogic.Propositional
        sourceSublogic Propositional2OWL2 = PSL.top
        targetLogic Propositional2OWL2 = OWLLogic.OWL2
        mapSublogic Propositional2OWL2 = Just . mapSub -- TODO
        map_theory Propositional2OWL2 = mapTheory
        -- map_morphism Propositional2OWL2 = mapMorphism
        -- map_symbol Propositional2OWL2 _ = mapSymbol
        isInclusionComorphism Propositional2OWL2 = True
        has_model_expansion Propositional2OWL2 = True

mkOWLDeclaration :: ClassExpression -> Axiom
mkOWLDeclaration ex = PlainAxiom (ClassEntity $ Expression $ setPrefix "owl"
    $ mkQName thingS) $ ListFrameBit (Just SubClass) $ ExpressionBit [([], ex)]

mapFormula :: FORMULA -> ClassExpression
mapFormula f = case f of
    False_atom _ -> Expression $ mkQName nothingS
    True_atom _ -> Expression $ mkQName thingS
    Predication p -> Expression $ mkQName $ tokStr p
    Negation nf _ -> ObjectComplementOf $ mapFormula nf
    Conjunction fl _ -> ObjectJunction IntersectionOf $ map mapFormula fl
    Disjunction fl _ -> ObjectJunction UnionOf $ map mapFormula fl
    Implication a b _ -> ObjectJunction UnionOf [ObjectComplementOf
                $ mapFormula a, mapFormula b]
    Equivalence a b _ -> ObjectJunction IntersectionOf $ map mapFormula
                [Implication a b nullRange, Implication b a nullRange]

mapPredDecl :: PRED_ITEM -> [Axiom]
mapPredDecl (Pred_item il _) = map (mkOWLDeclaration . Expression
    . mkQName . tokStr) il

mapAxiomItems :: Annoted FORMULA -> Axiom
mapAxiomItems = mkOWLDeclaration . mapFormula . item

mapBasicItems :: BASIC_ITEMS -> [Axiom]
mapBasicItems bi = case bi of
    Pred_decl p -> mapPredDecl p
    Axiom_items al -> map mapAxiomItems al

mapBasicSpec :: BASIC_SPEC -> [Axiom]
mapBasicSpec (Basic_spec il) = concatMap (mapBasicItems . item) il

mapSign :: PSign.Sign -> OWLSign.Sign
mapSign ps = OWLSign.emptySign {OWLSign.concepts = Set.fromList
    $ map (mkQName . tokStr . idToSimpleId) $ Set.toList $ PSign.items ps}

mapTheory :: (PSign.Sign, [Named FORMULA])
    -> Result (OWLSign.Sign, [Named Axiom])
mapTheory (psig, fl) = return (mapSign psig, map (makeNamed "")
    $ map (mkOWLDeclaration . mapFormula . sentence) fl)

mapSub :: PSL.PropSL -> OWLSub.ProfSub
mapSub _ = OWLSub.topS



