{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./OWL2/ProfilesAndSublogics.hs
Copyright   :  (c) Felix Gabriel Mance
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  f.mance@jacobs-university.de
Stability   :  provisional
Portability :  portable

OWL2 Profiles (EL, QL and RL) + OWL2 complexity analysis

References  :  <http://www.w3.org/TR/owl2-profiles/>
-}

module OWL2.ProfilesAndSublogics where

import OWL2.AS
import OWL2.Profiles
import OWL2.Sublogic
import OWL2.Sign
import OWL2.Morphism

import Data.Data
import Data.Set (empty)

data ProfSub = ProfSub
    { ProfSub -> Profiles
profiles :: Profiles
    , ProfSub -> OWLSub
sublogic :: OWLSub
    } deriving (Int -> ProfSub -> ShowS
[ProfSub] -> ShowS
ProfSub -> String
(Int -> ProfSub -> ShowS)
-> (ProfSub -> String) -> ([ProfSub] -> ShowS) -> Show ProfSub
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProfSub] -> ShowS
$cshowList :: [ProfSub] -> ShowS
show :: ProfSub -> String
$cshow :: ProfSub -> String
showsPrec :: Int -> ProfSub -> ShowS
$cshowsPrec :: Int -> ProfSub -> ShowS
Show, ProfSub -> ProfSub -> Bool
(ProfSub -> ProfSub -> Bool)
-> (ProfSub -> ProfSub -> Bool) -> Eq ProfSub
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProfSub -> ProfSub -> Bool
$c/= :: ProfSub -> ProfSub -> Bool
== :: ProfSub -> ProfSub -> Bool
$c== :: ProfSub -> ProfSub -> Bool
Eq, Eq ProfSub
Eq ProfSub =>
(ProfSub -> ProfSub -> Ordering)
-> (ProfSub -> ProfSub -> Bool)
-> (ProfSub -> ProfSub -> Bool)
-> (ProfSub -> ProfSub -> Bool)
-> (ProfSub -> ProfSub -> Bool)
-> (ProfSub -> ProfSub -> ProfSub)
-> (ProfSub -> ProfSub -> ProfSub)
-> Ord ProfSub
ProfSub -> ProfSub -> Bool
ProfSub -> ProfSub -> Ordering
ProfSub -> ProfSub -> ProfSub
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ProfSub -> ProfSub -> ProfSub
$cmin :: ProfSub -> ProfSub -> ProfSub
max :: ProfSub -> ProfSub -> ProfSub
$cmax :: ProfSub -> ProfSub -> ProfSub
>= :: ProfSub -> ProfSub -> Bool
$c>= :: ProfSub -> ProfSub -> Bool
> :: ProfSub -> ProfSub -> Bool
$c> :: ProfSub -> ProfSub -> Bool
<= :: ProfSub -> ProfSub -> Bool
$c<= :: ProfSub -> ProfSub -> Bool
< :: ProfSub -> ProfSub -> Bool
$c< :: ProfSub -> ProfSub -> Bool
compare :: ProfSub -> ProfSub -> Ordering
$ccompare :: ProfSub -> ProfSub -> Ordering
$cp1Ord :: Eq ProfSub
Ord, Typeable, Typeable ProfSub
Constr
DataType
Typeable ProfSub =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ProfSub -> c ProfSub)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ProfSub)
-> (ProfSub -> Constr)
-> (ProfSub -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ProfSub))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProfSub))
-> ((forall b. Data b => b -> b) -> ProfSub -> ProfSub)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ProfSub -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ProfSub -> r)
-> (forall u. (forall d. Data d => d -> u) -> ProfSub -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> ProfSub -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ProfSub -> m ProfSub)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProfSub -> m ProfSub)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProfSub -> m ProfSub)
-> Data ProfSub
ProfSub -> Constr
ProfSub -> DataType
(forall b. Data b => b -> b) -> ProfSub -> ProfSub
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProfSub -> c ProfSub
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProfSub
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ProfSub -> u
forall u. (forall d. Data d => d -> u) -> ProfSub -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProfSub -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProfSub -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProfSub -> m ProfSub
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProfSub -> m ProfSub
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProfSub
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProfSub -> c ProfSub
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProfSub)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProfSub)
$cProfSub :: Constr
$tProfSub :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ProfSub -> m ProfSub
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProfSub -> m ProfSub
gmapMp :: (forall d. Data d => d -> m d) -> ProfSub -> m ProfSub
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProfSub -> m ProfSub
gmapM :: (forall d. Data d => d -> m d) -> ProfSub -> m ProfSub
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProfSub -> m ProfSub
gmapQi :: Int -> (forall d. Data d => d -> u) -> ProfSub -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ProfSub -> u
gmapQ :: (forall d. Data d => d -> u) -> ProfSub -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ProfSub -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProfSub -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProfSub -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProfSub -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProfSub -> r
gmapT :: (forall b. Data b => b -> b) -> ProfSub -> ProfSub
$cgmapT :: (forall b. Data b => b -> b) -> ProfSub -> ProfSub
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProfSub)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProfSub)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ProfSub)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProfSub)
dataTypeOf :: ProfSub -> DataType
$cdataTypeOf :: ProfSub -> DataType
toConstr :: ProfSub -> Constr
$ctoConstr :: ProfSub -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProfSub
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProfSub
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProfSub -> c ProfSub
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProfSub -> c ProfSub
$cp1Data :: Typeable ProfSub
Data)

allProfSubs :: [[ProfSub]]
allProfSubs :: [[ProfSub]]
allProfSubs = 
    [ [Profiles -> OWLSub -> ProfSub
ProfSub Profiles
p OWLSub
sl | OWLSub
sl <- [OWLSub]
sls, Profiles
p <- [Profiles]
ps]
    | [OWLSub]
sls <- [[OWLSub]]
allSublogics, [Profiles]
ps <- [[Profiles]]
allProfiles ]

bottomS :: ProfSub
bottomS :: ProfSub
bottomS = Profiles -> OWLSub -> ProfSub
ProfSub Profiles
bottomProfile OWLSub
slBottom

topS :: ProfSub
topS :: ProfSub
topS = Profiles -> OWLSub -> ProfSub
ProfSub Profiles
topProfile OWLSub
slTop

-- | OWL2 DL Sublogic
dlS :: ProfSub
dlS :: ProfSub
dlS = Profiles -> OWLSub -> ProfSub
ProfSub Profiles
topProfile OWLSub
slDL

maxS :: ProfSub -> ProfSub -> ProfSub
maxS :: ProfSub -> ProfSub -> ProfSub
maxS ps1 :: ProfSub
ps1 ps2 :: ProfSub
ps2 = Profiles -> OWLSub -> ProfSub
ProfSub ([Profiles] -> Profiles
profileMax [ProfSub -> Profiles
profiles ProfSub
ps1, ProfSub -> Profiles
profiles ProfSub
ps2])
    (OWLSub -> OWLSub -> OWLSub
slMax (ProfSub -> OWLSub
sublogic ProfSub
ps1) (ProfSub -> OWLSub
sublogic ProfSub
ps2))

nameS :: ProfSub -> String
nameS :: ProfSub -> String
nameS ps :: ProfSub
ps = Profiles -> String
printProfile (ProfSub -> Profiles
profiles ProfSub
ps) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ OWLSub -> String
slName (ProfSub -> OWLSub
sublogic ProfSub
ps)

psAxiom :: Axiom -> ProfSub
psAxiom :: Axiom -> ProfSub
psAxiom ax :: Axiom
ax = Profiles -> OWLSub -> ProfSub
ProfSub (Axiom -> Profiles
axiom Axiom
ax) (COPs -> Axiom -> OWLSub
slAxiom COPs
forall a. Set a
empty Axiom
ax)

sSig :: Sign -> ProfSub
sSig :: Sign -> ProfSub
sSig s :: Sign
s = ProfSub
bottomS {sublogic :: OWLSub
sublogic = Sign -> OWLSub
slSig Sign
s}

sMorph :: OWLMorphism -> ProfSub
sMorph :: OWLMorphism -> ProfSub
sMorph m :: OWLMorphism
m = ProfSub
bottomS {sublogic :: OWLSub
sublogic = OWLMorphism -> OWLSub
slMor OWLMorphism
m}

prSign :: ProfSub -> Sign -> Sign
prSign :: ProfSub -> Sign -> Sign
prSign s :: ProfSub
s = OWLSub -> Sign -> Sign
prSig (ProfSub -> OWLSub
sublogic ProfSub
s)

prMorph :: ProfSub -> OWLMorphism -> OWLMorphism
prMorph :: ProfSub -> OWLMorphism -> OWLMorphism
prMorph s :: ProfSub
s a :: OWLMorphism
a = OWLMorphism
a
    { osource :: Sign
osource = ProfSub -> Sign -> Sign
prSign ProfSub
s (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
osource OWLMorphism
a
    , otarget :: Sign
otarget = ProfSub -> Sign -> Sign
prSign ProfSub
s (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
otarget OWLMorphism
a }

prOntDoc :: ProfSub -> OntologyDocument -> OntologyDocument
prOntDoc :: ProfSub -> OntologyDocument -> OntologyDocument
prOntDoc ps :: ProfSub
ps = OWLSub -> OntologyDocument -> OntologyDocument
prODoc (ProfSub -> OWLSub
sublogic ProfSub
ps)

profilesAndSublogic :: OntologyDocument -> ProfSub
profilesAndSublogic :: OntologyDocument -> ProfSub
profilesAndSublogic odoc :: OntologyDocument
odoc = Profiles -> OWLSub -> ProfSub
ProfSub (OntologyDocument -> Profiles
ontologyProfiles OntologyDocument
odoc) (OntologyDocument -> OWLSub
slODoc OntologyDocument
odoc)