{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./OWL2/Propositional2OWL2.hs
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 Common.IRI
import OWL2.Keywords
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 Int -> Propositional2OWL2 -> ShowS
[Propositional2OWL2] -> ShowS
Propositional2OWL2 -> String
(Int -> Propositional2OWL2 -> ShowS)
-> (Propositional2OWL2 -> String)
-> ([Propositional2OWL2] -> ShowS)
-> Show Propositional2OWL2
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Propositional2OWL2] -> ShowS
$cshowList :: [Propositional2OWL2] -> ShowS
show :: Propositional2OWL2 -> String
$cshow :: Propositional2OWL2 -> String
showsPrec :: Int -> Propositional2OWL2 -> ShowS
$cshowsPrec :: Int -> Propositional2OWL2 -> ShowS
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 -> Propositional
sourceLogic Propositional2OWL2 = Propositional
PLogic.Propositional
        sourceSublogic :: Propositional2OWL2 -> PropSL
sourceSublogic Propositional2OWL2 = PropSL
PSL.top
        targetLogic :: Propositional2OWL2 -> OWL2
targetLogic Propositional2OWL2 = OWL2
OWLLogic.OWL2
        mapSublogic :: Propositional2OWL2 -> PropSL -> Maybe ProfSub
mapSublogic Propositional2OWL2 = ProfSub -> Maybe ProfSub
forall a. a -> Maybe a
Just (ProfSub -> Maybe ProfSub)
-> (PropSL -> ProfSub) -> PropSL -> Maybe ProfSub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropSL -> ProfSub
mapSub -- TODO
        map_theory :: Propositional2OWL2
-> (Sign, [Named FORMULA]) -> Result (Sign, [Named Axiom])
map_theory Propositional2OWL2 = (Sign, [Named FORMULA]) -> Result (Sign, [Named Axiom])
mapTheory
        isInclusionComorphism :: Propositional2OWL2 -> Bool
isInclusionComorphism Propositional2OWL2 = Bool
True
        has_model_expansion :: Propositional2OWL2 -> Bool
has_model_expansion Propositional2OWL2 = Bool
True

mkOWLDeclaration :: ClassExpression -> Axiom
mkOWLDeclaration :: ClassExpression -> Axiom
mkOWLDeclaration ex :: ClassExpression
ex = ClassAxiom -> Axiom
ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ AxiomAnnotations
-> ClassExpression -> ClassExpression -> ClassAxiom
SubClassOf []
    (Class -> ClassExpression
Expression (Class -> ClassExpression) -> Class -> ClassExpression
forall a b. (a -> b) -> a -> b
$ String -> Class -> Class
setPrefix "owl" (Class -> Class) -> Class -> Class
forall a b. (a -> b) -> a -> b
$ String -> Class
mkIRI String
thingS) ClassExpression
ex

tokToIRI :: Token -> IRI
tokToIRI :: Token -> Class
tokToIRI = Id -> Class
idToIRI (Id -> Class) -> (Token -> Id) -> Token -> Class
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Id
simpleIdToId

mapFormula :: FORMULA -> ClassExpression
mapFormula :: FORMULA -> ClassExpression
mapFormula f :: FORMULA
f = case FORMULA
f of
    False_atom _ -> Class -> ClassExpression
Expression (Class -> ClassExpression) -> Class -> ClassExpression
forall a b. (a -> b) -> a -> b
$ String -> Class
mkIRI String
nothingS
    True_atom _ -> Class -> ClassExpression
Expression (Class -> ClassExpression) -> Class -> ClassExpression
forall a b. (a -> b) -> a -> b
$ String -> Class
mkIRI String
thingS
    Predication p :: Token
p -> Class -> ClassExpression
Expression (Class -> ClassExpression) -> Class -> ClassExpression
forall a b. (a -> b) -> a -> b
$ Token -> Class
tokToIRI Token
p
    Negation nf :: FORMULA
nf _ -> ClassExpression -> ClassExpression
ObjectComplementOf (ClassExpression -> ClassExpression)
-> ClassExpression -> ClassExpression
forall a b. (a -> b) -> a -> b
$ FORMULA -> ClassExpression
mapFormula FORMULA
nf
    Conjunction fl :: [FORMULA]
fl _ -> JunctionType -> [ClassExpression] -> ClassExpression
ObjectJunction JunctionType
IntersectionOf ([ClassExpression] -> ClassExpression)
-> [ClassExpression] -> ClassExpression
forall a b. (a -> b) -> a -> b
$ (FORMULA -> ClassExpression) -> [FORMULA] -> [ClassExpression]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> ClassExpression
mapFormula [FORMULA]
fl
    Disjunction fl :: [FORMULA]
fl _ -> JunctionType -> [ClassExpression] -> ClassExpression
ObjectJunction JunctionType
UnionOf ([ClassExpression] -> ClassExpression)
-> [ClassExpression] -> ClassExpression
forall a b. (a -> b) -> a -> b
$ (FORMULA -> ClassExpression) -> [FORMULA] -> [ClassExpression]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> ClassExpression
mapFormula [FORMULA]
fl
    Implication a :: FORMULA
a b :: FORMULA
b _ -> JunctionType -> [ClassExpression] -> ClassExpression
ObjectJunction JunctionType
UnionOf [ClassExpression -> ClassExpression
ObjectComplementOf
                (ClassExpression -> ClassExpression)
-> ClassExpression -> ClassExpression
forall a b. (a -> b) -> a -> b
$ FORMULA -> ClassExpression
mapFormula FORMULA
a, FORMULA -> ClassExpression
mapFormula FORMULA
b]
    Equivalence a :: FORMULA
a b :: FORMULA
b _ -> JunctionType -> [ClassExpression] -> ClassExpression
ObjectJunction JunctionType
IntersectionOf ([ClassExpression] -> ClassExpression)
-> [ClassExpression] -> ClassExpression
forall a b. (a -> b) -> a -> b
$ (FORMULA -> ClassExpression) -> [FORMULA] -> [ClassExpression]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> ClassExpression
mapFormula
                [FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
a FORMULA
b Range
nullRange, FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
b FORMULA
a Range
nullRange]

mapPredDecl :: PRED_ITEM -> [Axiom]
mapPredDecl :: PRED_ITEM -> [Axiom]
mapPredDecl (Pred_item il :: [Token]
il _) = (Token -> Axiom) -> [Token] -> [Axiom]
forall a b. (a -> b) -> [a] -> [b]
map (ClassExpression -> Axiom
mkOWLDeclaration (ClassExpression -> Axiom)
-> (Token -> ClassExpression) -> Token -> Axiom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Class -> ClassExpression
Expression
    (Class -> ClassExpression)
-> (Token -> Class) -> Token -> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Class
tokToIRI) [Token]
il

mapAxiomItems :: Annoted FORMULA -> Axiom
mapAxiomItems :: Annoted FORMULA -> Axiom
mapAxiomItems = ClassExpression -> Axiom
mkOWLDeclaration (ClassExpression -> Axiom)
-> (Annoted FORMULA -> ClassExpression) -> Annoted FORMULA -> Axiom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> ClassExpression
mapFormula (FORMULA -> ClassExpression)
-> (Annoted FORMULA -> FORMULA)
-> Annoted FORMULA
-> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FORMULA -> FORMULA
forall a. Annoted a -> a
item

mapBasicItems :: BASIC_ITEMS -> [Axiom]
mapBasicItems :: BASIC_ITEMS -> [Axiom]
mapBasicItems bi :: BASIC_ITEMS
bi = case BASIC_ITEMS
bi of
    Pred_decl p :: PRED_ITEM
p -> PRED_ITEM -> [Axiom]
mapPredDecl PRED_ITEM
p
    Axiom_items al :: [Annoted FORMULA]
al -> (Annoted FORMULA -> Axiom) -> [Annoted FORMULA] -> [Axiom]
forall a b. (a -> b) -> [a] -> [b]
map Annoted FORMULA -> Axiom
mapAxiomItems [Annoted FORMULA]
al

mapBasicSpec :: BASIC_SPEC -> [Axiom]
mapBasicSpec :: BASIC_SPEC -> [Axiom]
mapBasicSpec (Basic_spec il :: [Annoted BASIC_ITEMS]
il) = (Annoted BASIC_ITEMS -> [Axiom])
-> [Annoted BASIC_ITEMS] -> [Axiom]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BASIC_ITEMS -> [Axiom]
mapBasicItems (BASIC_ITEMS -> [Axiom])
-> (Annoted BASIC_ITEMS -> BASIC_ITEMS)
-> Annoted BASIC_ITEMS
-> [Axiom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BASIC_ITEMS -> BASIC_ITEMS
forall a. Annoted a -> a
item) [Annoted BASIC_ITEMS]
il

mapSign :: PSign.Sign -> OWLSign.Sign
mapSign :: Sign -> Sign
mapSign ps :: Sign
ps = Sign
OWLSign.emptySign {concepts :: Set Class
OWLSign.concepts = [Class] -> Set Class
forall a. Ord a => [a] -> Set a
Set.fromList
    ([Class] -> Set Class) -> [Class] -> Set Class
forall a b. (a -> b) -> a -> b
$ (Id -> Class) -> [Id] -> [Class]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Class
idToIRI ([Id] -> [Class]) -> [Id] -> [Class]
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
PSign.items Sign
ps}

mapTheory :: (PSign.Sign, [Named FORMULA])
    -> Result (OWLSign.Sign, [Named Axiom])
mapTheory :: (Sign, [Named FORMULA]) -> Result (Sign, [Named Axiom])
mapTheory (psig :: Sign
psig, fl :: [Named FORMULA]
fl) = (Sign, [Named Axiom]) -> Result (Sign, [Named Axiom])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Sign
mapSign Sign
psig, (Named FORMULA -> Named Axiom) -> [Named FORMULA] -> [Named Axiom]
forall a b. (a -> b) -> [a] -> [b]
map
    ((FORMULA -> Axiom) -> Named FORMULA -> Named Axiom
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((FORMULA -> Axiom) -> Named FORMULA -> Named Axiom)
-> (FORMULA -> Axiom) -> Named FORMULA -> Named Axiom
forall a b. (a -> b) -> a -> b
$ ClassExpression -> Axiom
mkOWLDeclaration (ClassExpression -> Axiom)
-> (FORMULA -> ClassExpression) -> FORMULA -> Axiom
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> ClassExpression
mapFormula) [Named FORMULA]
fl)

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