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

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

Complexity analysis of OWL2

-}

module OWL2.Sublogic where

import OWL2.AS
import OWL2.Sign
import OWL2.Morphism

import Data.List
import Data.Graph (stronglyConnComp, SCC(..))
import Data.Tree
import Data.Data
import Data.Maybe (mapMaybe)
import qualified Data.Map as Map
import qualified Data.Set as Set

import Common.IRI (expandIRI')

data NumberRestrictions = None | Unqualified | Qualified
    deriving (Int -> NumberRestrictions -> ShowS
[NumberRestrictions] -> ShowS
NumberRestrictions -> String
(Int -> NumberRestrictions -> ShowS)
-> (NumberRestrictions -> String)
-> ([NumberRestrictions] -> ShowS)
-> Show NumberRestrictions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NumberRestrictions] -> ShowS
$cshowList :: [NumberRestrictions] -> ShowS
show :: NumberRestrictions -> String
$cshow :: NumberRestrictions -> String
showsPrec :: Int -> NumberRestrictions -> ShowS
$cshowsPrec :: Int -> NumberRestrictions -> ShowS
Show, NumberRestrictions -> NumberRestrictions -> Bool
(NumberRestrictions -> NumberRestrictions -> Bool)
-> (NumberRestrictions -> NumberRestrictions -> Bool)
-> Eq NumberRestrictions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NumberRestrictions -> NumberRestrictions -> Bool
$c/= :: NumberRestrictions -> NumberRestrictions -> Bool
== :: NumberRestrictions -> NumberRestrictions -> Bool
$c== :: NumberRestrictions -> NumberRestrictions -> Bool
Eq, Eq NumberRestrictions
Eq NumberRestrictions =>
(NumberRestrictions -> NumberRestrictions -> Ordering)
-> (NumberRestrictions -> NumberRestrictions -> Bool)
-> (NumberRestrictions -> NumberRestrictions -> Bool)
-> (NumberRestrictions -> NumberRestrictions -> Bool)
-> (NumberRestrictions -> NumberRestrictions -> Bool)
-> (NumberRestrictions -> NumberRestrictions -> NumberRestrictions)
-> (NumberRestrictions -> NumberRestrictions -> NumberRestrictions)
-> Ord NumberRestrictions
NumberRestrictions -> NumberRestrictions -> Bool
NumberRestrictions -> NumberRestrictions -> Ordering
NumberRestrictions -> NumberRestrictions -> NumberRestrictions
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 :: NumberRestrictions -> NumberRestrictions -> NumberRestrictions
$cmin :: NumberRestrictions -> NumberRestrictions -> NumberRestrictions
max :: NumberRestrictions -> NumberRestrictions -> NumberRestrictions
$cmax :: NumberRestrictions -> NumberRestrictions -> NumberRestrictions
>= :: NumberRestrictions -> NumberRestrictions -> Bool
$c>= :: NumberRestrictions -> NumberRestrictions -> Bool
> :: NumberRestrictions -> NumberRestrictions -> Bool
$c> :: NumberRestrictions -> NumberRestrictions -> Bool
<= :: NumberRestrictions -> NumberRestrictions -> Bool
$c<= :: NumberRestrictions -> NumberRestrictions -> Bool
< :: NumberRestrictions -> NumberRestrictions -> Bool
$c< :: NumberRestrictions -> NumberRestrictions -> Bool
compare :: NumberRestrictions -> NumberRestrictions -> Ordering
$ccompare :: NumberRestrictions -> NumberRestrictions -> Ordering
$cp1Ord :: Eq NumberRestrictions
Ord, Typeable, Typeable NumberRestrictions
Constr
DataType
Typeable NumberRestrictions =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> NumberRestrictions
 -> c NumberRestrictions)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c NumberRestrictions)
-> (NumberRestrictions -> Constr)
-> (NumberRestrictions -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c NumberRestrictions))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c NumberRestrictions))
-> ((forall b. Data b => b -> b)
    -> NumberRestrictions -> NumberRestrictions)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NumberRestrictions -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NumberRestrictions -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> NumberRestrictions -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> NumberRestrictions -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> NumberRestrictions -> m NumberRestrictions)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NumberRestrictions -> m NumberRestrictions)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NumberRestrictions -> m NumberRestrictions)
-> Data NumberRestrictions
NumberRestrictions -> Constr
NumberRestrictions -> DataType
(forall b. Data b => b -> b)
-> NumberRestrictions -> NumberRestrictions
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> NumberRestrictions
-> c NumberRestrictions
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NumberRestrictions
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) -> NumberRestrictions -> u
forall u. (forall d. Data d => d -> u) -> NumberRestrictions -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NumberRestrictions -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NumberRestrictions -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NumberRestrictions -> m NumberRestrictions
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NumberRestrictions -> m NumberRestrictions
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NumberRestrictions
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> NumberRestrictions
-> c NumberRestrictions
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NumberRestrictions)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NumberRestrictions)
$cQualified :: Constr
$cUnqualified :: Constr
$cNone :: Constr
$tNumberRestrictions :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> NumberRestrictions -> m NumberRestrictions
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NumberRestrictions -> m NumberRestrictions
gmapMp :: (forall d. Data d => d -> m d)
-> NumberRestrictions -> m NumberRestrictions
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NumberRestrictions -> m NumberRestrictions
gmapM :: (forall d. Data d => d -> m d)
-> NumberRestrictions -> m NumberRestrictions
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NumberRestrictions -> m NumberRestrictions
gmapQi :: Int -> (forall d. Data d => d -> u) -> NumberRestrictions -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> NumberRestrictions -> u
gmapQ :: (forall d. Data d => d -> u) -> NumberRestrictions -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> NumberRestrictions -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NumberRestrictions -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NumberRestrictions -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NumberRestrictions -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NumberRestrictions -> r
gmapT :: (forall b. Data b => b -> b)
-> NumberRestrictions -> NumberRestrictions
$cgmapT :: (forall b. Data b => b -> b)
-> NumberRestrictions -> NumberRestrictions
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NumberRestrictions)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NumberRestrictions)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c NumberRestrictions)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NumberRestrictions)
dataTypeOf :: NumberRestrictions -> DataType
$cdataTypeOf :: NumberRestrictions -> DataType
toConstr :: NumberRestrictions -> Constr
$ctoConstr :: NumberRestrictions -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NumberRestrictions
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NumberRestrictions
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> NumberRestrictions
-> c NumberRestrictions
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> NumberRestrictions
-> c NumberRestrictions
$cp1Data :: Typeable NumberRestrictions
Data)

owlDatatypes :: Set.Set Datatype
owlDatatypes :: Set Datatype
owlDatatypes = (Datatype -> Datatype) -> Set Datatype -> Set Datatype
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map String String -> Datatype -> Datatype
expandIRI' Map String String
predefPrefixes) Set Datatype
predefIRIs

data OWLSub = OWLSub
    { OWLSub -> NumberRestrictions
numberRestrictions :: NumberRestrictions -- ^ Cardinaly restrictions the can be used
    , OWLSub -> Bool
nominals :: Bool              -- ^ Enumerated classes can be used
    , OWLSub -> Bool
inverseRoles :: Bool          -- ^ Inverse roles can be used
    , OWLSub -> Bool
roleTransitivity :: Bool      -- ^ Roles can be transitive
    , OWLSub -> Bool
roleHierarchy :: Bool         -- ^ Role hierachy (subproperties) can be used
    , OWLSub -> Bool
complexRoleInclusions :: Bool -- ^ Complex role inclusions can be used
    , OWLSub -> Bool
addFeatures :: Bool           -- ^ Additional features can be used
    , OWLSub -> Set Datatype
datatype :: Set.Set Datatype  -- ^ Set of datatypes that can be used
    , OWLSub -> Bool
rules :: Bool                 -- ^ SWRL Rules can be used
    , OWLSub -> Bool
unrestrictedDL :: Bool        -- ^ OWL2 DL restriction can be ignored
    } deriving (Int -> OWLSub -> ShowS
[OWLSub] -> ShowS
OWLSub -> String
(Int -> OWLSub -> ShowS)
-> (OWLSub -> String) -> ([OWLSub] -> ShowS) -> Show OWLSub
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OWLSub] -> ShowS
$cshowList :: [OWLSub] -> ShowS
show :: OWLSub -> String
$cshow :: OWLSub -> String
showsPrec :: Int -> OWLSub -> ShowS
$cshowsPrec :: Int -> OWLSub -> ShowS
Show, OWLSub -> OWLSub -> Bool
(OWLSub -> OWLSub -> Bool)
-> (OWLSub -> OWLSub -> Bool) -> Eq OWLSub
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OWLSub -> OWLSub -> Bool
$c/= :: OWLSub -> OWLSub -> Bool
== :: OWLSub -> OWLSub -> Bool
$c== :: OWLSub -> OWLSub -> Bool
Eq, Eq OWLSub
Eq OWLSub =>
(OWLSub -> OWLSub -> Ordering)
-> (OWLSub -> OWLSub -> Bool)
-> (OWLSub -> OWLSub -> Bool)
-> (OWLSub -> OWLSub -> Bool)
-> (OWLSub -> OWLSub -> Bool)
-> (OWLSub -> OWLSub -> OWLSub)
-> (OWLSub -> OWLSub -> OWLSub)
-> Ord OWLSub
OWLSub -> OWLSub -> Bool
OWLSub -> OWLSub -> Ordering
OWLSub -> OWLSub -> OWLSub
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 :: OWLSub -> OWLSub -> OWLSub
$cmin :: OWLSub -> OWLSub -> OWLSub
max :: OWLSub -> OWLSub -> OWLSub
$cmax :: OWLSub -> OWLSub -> OWLSub
>= :: OWLSub -> OWLSub -> Bool
$c>= :: OWLSub -> OWLSub -> Bool
> :: OWLSub -> OWLSub -> Bool
$c> :: OWLSub -> OWLSub -> Bool
<= :: OWLSub -> OWLSub -> Bool
$c<= :: OWLSub -> OWLSub -> Bool
< :: OWLSub -> OWLSub -> Bool
$c< :: OWLSub -> OWLSub -> Bool
compare :: OWLSub -> OWLSub -> Ordering
$ccompare :: OWLSub -> OWLSub -> Ordering
$cp1Ord :: Eq OWLSub
Ord, Typeable, Typeable OWLSub
Constr
DataType
Typeable OWLSub =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> OWLSub -> c OWLSub)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c OWLSub)
-> (OWLSub -> Constr)
-> (OWLSub -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c OWLSub))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OWLSub))
-> ((forall b. Data b => b -> b) -> OWLSub -> OWLSub)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> OWLSub -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> OWLSub -> r)
-> (forall u. (forall d. Data d => d -> u) -> OWLSub -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> OWLSub -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> OWLSub -> m OWLSub)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OWLSub -> m OWLSub)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OWLSub -> m OWLSub)
-> Data OWLSub
OWLSub -> Constr
OWLSub -> DataType
(forall b. Data b => b -> b) -> OWLSub -> OWLSub
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OWLSub -> c OWLSub
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OWLSub
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) -> OWLSub -> u
forall u. (forall d. Data d => d -> u) -> OWLSub -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OWLSub -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OWLSub -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OWLSub -> m OWLSub
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OWLSub -> m OWLSub
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OWLSub
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OWLSub -> c OWLSub
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OWLSub)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OWLSub)
$cOWLSub :: Constr
$tOWLSub :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> OWLSub -> m OWLSub
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OWLSub -> m OWLSub
gmapMp :: (forall d. Data d => d -> m d) -> OWLSub -> m OWLSub
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> OWLSub -> m OWLSub
gmapM :: (forall d. Data d => d -> m d) -> OWLSub -> m OWLSub
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> OWLSub -> m OWLSub
gmapQi :: Int -> (forall d. Data d => d -> u) -> OWLSub -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> OWLSub -> u
gmapQ :: (forall d. Data d => d -> u) -> OWLSub -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> OWLSub -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OWLSub -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OWLSub -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OWLSub -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OWLSub -> r
gmapT :: (forall b. Data b => b -> b) -> OWLSub -> OWLSub
$cgmapT :: (forall b. Data b => b -> b) -> OWLSub -> OWLSub
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OWLSub)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OWLSub)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c OWLSub)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c OWLSub)
dataTypeOf :: OWLSub -> DataType
$cdataTypeOf :: OWLSub -> DataType
toConstr :: OWLSub -> Constr
$ctoConstr :: OWLSub -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OWLSub
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c OWLSub
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OWLSub -> c OWLSub
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> OWLSub -> c OWLSub
$cp1Data :: Typeable OWLSub
Data)

allSublogics :: [[OWLSub]]
allSublogics :: [[OWLSub]]
allSublogics = let
  t :: Bool
t = Bool
True
  b :: OWLSub
b = OWLSub
slBottom
  in
  [ [ OWLSub
b { numberRestrictions :: NumberRestrictions
numberRestrictions = NumberRestrictions
Unqualified }
    , OWLSub
b { numberRestrictions :: NumberRestrictions
numberRestrictions = NumberRestrictions
Qualified } ]
  , [OWLSub
b { nominals :: Bool
nominals = Bool
t } ]
  , [OWLSub
b { inverseRoles :: Bool
inverseRoles = Bool
t } ]
  , [OWLSub
b { roleTransitivity :: Bool
roleTransitivity = Bool
t } ]
  , [OWLSub
b { roleHierarchy :: Bool
roleHierarchy = Bool
t } ]
  , [OWLSub
b { complexRoleInclusions :: Bool
complexRoleInclusions = Bool
t } ]
  , [OWLSub
b { addFeatures :: Bool
addFeatures = Bool
t } ]
  , [OWLSub
b { rules :: Bool
rules = Bool
t} ]
  , [OWLSub
b { unrestrictedDL :: Bool
unrestrictedDL = Bool
t} ]
  , (Datatype -> OWLSub) -> [Datatype] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map (\ d :: Datatype
d -> OWLSub
b { datatype :: Set Datatype
datatype = Datatype -> Set Datatype
forall a. a -> Set a
Set.singleton Datatype
d }) ([Datatype] -> [OWLSub]) -> [Datatype] -> [OWLSub]
forall a b. (a -> b) -> a -> b
$ Set Datatype -> [Datatype]
forall a. Set a -> [a]
Set.toList Set Datatype
owlDatatypes ]

-- | sROIQ(D)
slTop :: OWLSub
slTop :: OWLSub
slTop = OWLSub :: NumberRestrictions
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Set Datatype
-> Bool
-> Bool
-> OWLSub
OWLSub
    { numberRestrictions :: NumberRestrictions
numberRestrictions = NumberRestrictions
Qualified
    , nominals :: Bool
nominals = Bool
True
    , inverseRoles :: Bool
inverseRoles = Bool
True
    , roleTransitivity :: Bool
roleTransitivity = Bool
True
    , roleHierarchy :: Bool
roleHierarchy = Bool
True
    , complexRoleInclusions :: Bool
complexRoleInclusions = Bool
True
    , addFeatures :: Bool
addFeatures = Bool
True
    , datatype :: Set Datatype
datatype = Set Datatype
owlDatatypes
    , rules :: Bool
rules = Bool
True
    , unrestrictedDL :: Bool
unrestrictedDL = Bool
True
    }

-- | ALC
slBottom :: OWLSub
slBottom :: OWLSub
slBottom = OWLSub :: NumberRestrictions
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Set Datatype
-> Bool
-> Bool
-> OWLSub
OWLSub
    { numberRestrictions :: NumberRestrictions
numberRestrictions = NumberRestrictions
None
    , nominals :: Bool
nominals = Bool
False
    , inverseRoles :: Bool
inverseRoles = Bool
False
    , roleTransitivity :: Bool
roleTransitivity = Bool
False
    , roleHierarchy :: Bool
roleHierarchy = Bool
False
    , complexRoleInclusions :: Bool
complexRoleInclusions = Bool
False
    , addFeatures :: Bool
addFeatures = Bool
False
    , datatype :: Set Datatype
datatype = Set Datatype
forall a. Set a
Set.empty
    , rules :: Bool
rules = Bool
False
    , unrestrictedDL :: Bool
unrestrictedDL = Bool
False
    }

slDL :: OWLSub
slDL :: OWLSub
slDL = OWLSub
slTop { unrestrictedDL :: Bool
unrestrictedDL = Bool
False }


slMax :: OWLSub -> OWLSub -> OWLSub
slMax :: OWLSub -> OWLSub -> OWLSub
slMax sl1 :: OWLSub
sl1 sl2 :: OWLSub
sl2 = OWLSub :: NumberRestrictions
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Set Datatype
-> Bool
-> Bool
-> OWLSub
OWLSub
    { numberRestrictions :: NumberRestrictions
numberRestrictions = NumberRestrictions -> NumberRestrictions -> NumberRestrictions
forall a. Ord a => a -> a -> a
max (OWLSub -> NumberRestrictions
numberRestrictions OWLSub
sl1) (OWLSub -> NumberRestrictions
numberRestrictions OWLSub
sl2)
    , nominals :: Bool
nominals = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max (OWLSub -> Bool
nominals OWLSub
sl1) (OWLSub -> Bool
nominals OWLSub
sl2)
    , inverseRoles :: Bool
inverseRoles = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max (OWLSub -> Bool
inverseRoles OWLSub
sl1) (OWLSub -> Bool
inverseRoles OWLSub
sl2)
    , roleTransitivity :: Bool
roleTransitivity = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max (OWLSub -> Bool
roleTransitivity OWLSub
sl1) (OWLSub -> Bool
roleTransitivity OWLSub
sl2)
    , roleHierarchy :: Bool
roleHierarchy = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max (OWLSub -> Bool
roleHierarchy OWLSub
sl1) (OWLSub -> Bool
roleHierarchy OWLSub
sl2)
    , complexRoleInclusions :: Bool
complexRoleInclusions = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max (OWLSub -> Bool
complexRoleInclusions OWLSub
sl1)
            (OWLSub -> Bool
complexRoleInclusions OWLSub
sl2)
    , addFeatures :: Bool
addFeatures = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max (OWLSub -> Bool
addFeatures OWLSub
sl1) (OWLSub -> Bool
addFeatures OWLSub
sl2)
    , datatype :: Set Datatype
datatype = Set Datatype -> Set Datatype -> Set Datatype
forall a. Ord a => Set a -> Set a -> Set a
Set.union (OWLSub -> Set Datatype
datatype OWLSub
sl1) (OWLSub -> Set Datatype
datatype OWLSub
sl2)
    , rules :: Bool
rules = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max (OWLSub -> Bool
rules OWLSub
sl1) (OWLSub -> Bool
rules OWLSub
sl2)
    , unrestrictedDL :: Bool
unrestrictedDL = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max (OWLSub -> Bool
unrestrictedDL OWLSub
sl1) (OWLSub -> Bool
unrestrictedDL OWLSub
sl2) 
    }

slMaxs :: Foldable t => t OWLSub -> OWLSub
slMaxs :: t OWLSub -> OWLSub
slMaxs = (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> t OWLSub -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom

-- | Naming for Description Logics
slName :: OWLSub -> String
slName :: OWLSub -> String
slName sl :: OWLSub
sl =
    (if OWLSub -> Bool
complexRoleInclusions OWLSub
sl Bool -> Bool -> Bool
|| OWLSub -> Bool
addFeatures OWLSub
sl
       then (if OWLSub -> Bool
addFeatures OWLSub
sl then "s" else "") String -> ShowS
forall a. [a] -> [a] -> [a]
++ "R"
       else (if OWLSub -> Bool
roleTransitivity OWLSub
sl then "S" else "ALC")
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ if OWLSub -> Bool
roleHierarchy OWLSub
sl then "H" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if OWLSub -> Bool
nominals OWLSub
sl then "O" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if OWLSub -> Bool
inverseRoles OWLSub
sl then "I" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (case OWLSub -> NumberRestrictions
numberRestrictions OWLSub
sl of
        Qualified -> "Q"
        Unqualified -> "N"
        None -> "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if OWLSub -> Bool
rules OWLSub
sl then "u" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if OWLSub -> Bool
unrestrictedDL OWLSub
sl then "x" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ let ds :: Set Datatype
ds = OWLSub -> Set Datatype
datatype OWLSub
sl in if Set Datatype -> Bool
forall a. Set a -> Bool
Set.null Set Datatype
ds then "" else
           "-D|" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Set Datatype
ds Set Datatype -> Set Datatype -> Bool
forall a. Eq a => a -> a -> Bool
== Set Datatype
owlDatatypes then "-|" else
                String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "|" ((Datatype -> String) -> [Datatype] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Datatype -> String
printDatatype ([Datatype] -> [String]) -> [Datatype] -> [String]
forall a b. (a -> b) -> a -> b
$ Set Datatype -> [Datatype]
forall a. Set a -> [a]
Set.toList Set Datatype
ds) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "|")

requireQualNumberRestrictions :: OWLSub -> OWLSub
requireQualNumberRestrictions :: OWLSub -> OWLSub
requireQualNumberRestrictions sl :: OWLSub
sl = OWLSub
sl {numberRestrictions :: NumberRestrictions
numberRestrictions = NumberRestrictions
Qualified}

requireNumberRestrictions :: OWLSub -> OWLSub
requireNumberRestrictions :: OWLSub -> OWLSub
requireNumberRestrictions sl :: OWLSub
sl = let nr :: NumberRestrictions
nr = OWLSub -> NumberRestrictions
numberRestrictions OWLSub
sl in
    OWLSub
sl {numberRestrictions :: NumberRestrictions
numberRestrictions = if NumberRestrictions
nr NumberRestrictions -> NumberRestrictions -> Bool
forall a. Eq a => a -> a -> Bool
/= NumberRestrictions
Qualified then NumberRestrictions
Unqualified else NumberRestrictions
nr}

requireRoleTransitivity :: OWLSub -> OWLSub
requireRoleTransitivity :: OWLSub -> OWLSub
requireRoleTransitivity sl :: OWLSub
sl = OWLSub
sl {roleTransitivity :: Bool
roleTransitivity = Bool
True}

requireRoleHierarchy :: OWLSub -> OWLSub
requireRoleHierarchy :: OWLSub -> OWLSub
requireRoleHierarchy sl :: OWLSub
sl = OWLSub
sl {roleHierarchy :: Bool
roleHierarchy = Bool
True}

requireComplexRoleInclusions :: OWLSub -> OWLSub
requireComplexRoleInclusions :: OWLSub -> OWLSub
requireComplexRoleInclusions sl :: OWLSub
sl = (OWLSub -> OWLSub
requireRoleHierarchy
    (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireRoleTransitivity OWLSub
sl) {complexRoleInclusions :: Bool
complexRoleInclusions = Bool
True}

requireAddFeatures :: OWLSub -> OWLSub
requireAddFeatures :: OWLSub -> OWLSub
requireAddFeatures sl :: OWLSub
sl = (OWLSub -> OWLSub
requireComplexRoleInclusions OWLSub
sl) {addFeatures :: Bool
addFeatures = Bool
True}

requireNominals :: OWLSub -> OWLSub
requireNominals :: OWLSub -> OWLSub
requireNominals sl :: OWLSub
sl = OWLSub
sl {nominals :: Bool
nominals = Bool
True}

requireInverseRoles :: OWLSub -> OWLSub
requireInverseRoles :: OWLSub -> OWLSub
requireInverseRoles sl :: OWLSub
sl = OWLSub
sl {inverseRoles :: Bool
inverseRoles = Bool
True}

requireRules :: OWLSub -> OWLSub
requireRules :: OWLSub -> OWLSub
requireRules sl :: OWLSub
sl = OWLSub
sl {rules :: Bool
rules = Bool
True}

requireUnrestrictedDL :: OWLSub -> OWLSub
requireUnrestrictedDL :: OWLSub -> OWLSub
requireUnrestrictedDL sl :: OWLSub
sl = OWLSub
sl {unrestrictedDL :: Bool
unrestrictedDL = Bool
True}

slDatatype :: Datatype -> OWLSub
slDatatype :: Datatype -> OWLSub
slDatatype dt :: Datatype
dt = OWLSub
slBottom {datatype :: Set Datatype
datatype = if Datatype -> Bool
isDatatypeKey Datatype
dt then
    Datatype -> Set Datatype
forall a. a -> Set a
Set.singleton (Datatype -> Set Datatype) -> Datatype -> Set Datatype
forall a b. (a -> b) -> a -> b
$ Datatype -> Datatype
setDatatypePrefix Datatype
dt else Set Datatype
forall a. Set a
Set.empty}

slObjProp :: ObjectPropertyExpression -> OWLSub
slObjProp :: ObjectPropertyExpression -> OWLSub
slObjProp o :: ObjectPropertyExpression
o = case ObjectPropertyExpression
o of
    ObjectProp _ -> OWLSub
slBottom
    ObjectInverseOf _ -> OWLSub -> OWLSub
requireInverseRoles OWLSub
slBottom

slEntity :: Entity -> OWLSub
slEntity :: Entity -> OWLSub
slEntity (Entity _ et :: EntityType
et iri :: Datatype
iri) = case EntityType
et of
    Datatype -> Datatype -> OWLSub
slDatatype Datatype
iri
    _ -> OWLSub
slBottom

slAnnotation :: Annotation -> OWLSub
slAnnotation :: Annotation -> OWLSub
slAnnotation (Annotation annos :: [Annotation]
annos _ val :: AnnotationValue
val) = OWLSub -> OWLSub -> OWLSub
slMax ([Annotation] -> OWLSub
slAnnos [Annotation]
annos) (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ case AnnotationValue
val of
    AnnAnInd i :: Datatype
i -> [Datatype] -> OWLSub
slIndividuals [Datatype
i]
    AnnValLit l :: Literal
l -> Literal -> OWLSub
slLiteral Literal
l
    _ -> OWLSub
slBottom

slAnnos :: [Annotation] -> OWLSub
slAnnos :: [Annotation] -> OWLSub
slAnnos = (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub)
-> ([Annotation] -> [OWLSub]) -> [Annotation] -> OWLSub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Annotation -> OWLSub) -> [Annotation] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map Annotation -> OWLSub
slAnnotation

slAnnosAnd :: [Annotation] -> OWLSub  -> OWLSub
slAnnosAnd :: [Annotation] -> OWLSub -> OWLSub
slAnnosAnd annos :: [Annotation]
annos = OWLSub -> OWLSub -> OWLSub
slMax ([Annotation] -> OWLSub
slAnnos [Annotation]
annos)

slLiteral :: Literal -> OWLSub
slLiteral :: Literal -> OWLSub
slLiteral = OWLSub -> (Datatype -> OWLSub) -> Maybe Datatype -> OWLSub
forall b a. b -> (a -> b) -> Maybe a -> b
maybe OWLSub
slBottom Datatype -> OWLSub
slDatatype (Maybe Datatype -> OWLSub)
-> (Literal -> Maybe Datatype) -> Literal -> OWLSub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Maybe Datatype
litType

slDataRange :: DataRange -> OWLSub
slDataRange :: DataRange -> OWLSub
slDataRange rn :: DataRange
rn = case DataRange
rn of
    DataType ur :: Datatype
ur fs :: [(Datatype, Literal)]
fs -> (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax (Datatype -> OWLSub
slDatatype Datatype
ur) (Literal -> OWLSub
slLiteral (Literal -> OWLSub)
-> ((Datatype, Literal) -> Literal)
-> (Datatype, Literal)
-> OWLSub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Datatype, Literal) -> Literal
forall a b. (a, b) -> b
snd ((Datatype, Literal) -> OWLSub)
-> [(Datatype, Literal)] -> [OWLSub]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Datatype, Literal)]
fs)
    DataComplementOf c :: DataRange
c -> DataRange -> OWLSub
slDataRange DataRange
c
    DataOneOf lits :: [Literal]
lits -> OWLSub -> OWLSub
requireNominals ((OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom (Literal -> OWLSub
slLiteral (Literal -> OWLSub) -> [Literal] -> [OWLSub]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Literal]
lits))
    DataJunction _ drl :: [DataRange]
drl -> (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ (DataRange -> OWLSub) -> [DataRange] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map DataRange -> OWLSub
slDataRange [DataRange]
drl

-- | Checks anonymous individuals
--   Anonymous individuals are not allowed in some place in OWL2 DL
slIndividuals :: [Individual] -> OWLSub
slIndividuals :: [Datatype] -> OWLSub
slIndividuals is :: [Datatype]
is = if (Datatype -> Bool) -> [Datatype] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Datatype -> Bool
isAnonymous [Datatype]
is then OWLSub -> OWLSub
requireUnrestrictedDL OWLSub
slBottom else OWLSub
slBottom

slClassExpression :: COPs -> ClassExpression -> OWLSub
slClassExpression :: COPs -> ClassExpression -> OWLSub
slClassExpression cops :: COPs
cops des :: ClassExpression
des = case ClassExpression
des of
    ObjectJunction _ dec :: [ClassExpression]
dec -> (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ (ClassExpression -> OWLSub) -> [ClassExpression] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops) [ClassExpression]
dec
    ObjectComplementOf dec :: ClassExpression
dec -> COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
dec
    ObjectOneOf is :: [Datatype]
is -> OWLSub -> OWLSub
requireNominals (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ [Datatype] -> OWLSub
slIndividuals [Datatype]
is
    ObjectValuesFrom _ o :: ObjectPropertyExpression
o d :: ClassExpression
d -> OWLSub -> OWLSub -> OWLSub
slMax (ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
o) (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
d)
    ObjectHasSelf o :: ObjectPropertyExpression
o -> OWLSub -> OWLSub
requireAddFeatures (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ COPs -> ObjectPropertyExpression -> OWLSub
slSimpleObjectProp COPs
cops ObjectPropertyExpression
o
    ObjectHasValue o :: ObjectPropertyExpression
o i :: Datatype
i -> (if Datatype -> Bool
isAnonymous Datatype
i then OWLSub -> OWLSub
requireUnrestrictedDL else OWLSub -> OWLSub
forall a. a -> a
id) (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
o
    ObjectCardinality c :: Cardinality ObjectPropertyExpression ClassExpression
c -> COPs
-> Cardinality ObjectPropertyExpression ClassExpression -> OWLSub
slObjCard COPs
cops Cardinality ObjectPropertyExpression ClassExpression
c
    DataValuesFrom _ _ dr :: DataRange
dr -> DataRange -> OWLSub
slDataRange DataRange
dr
    DataCardinality c :: Cardinality Datatype DataRange
c -> Cardinality Datatype DataRange -> OWLSub
slDataCard Cardinality Datatype DataRange
c
    DataHasValue _ l :: Literal
l -> Literal -> OWLSub
slLiteral Literal
l
    _ -> OWLSub
slBottom

slDataCard :: Cardinality DataPropertyExpression DataRange -> OWLSub
slDataCard :: Cardinality Datatype DataRange -> OWLSub
slDataCard (Cardinality _ _ _ x :: Maybe DataRange
x) = OWLSub -> OWLSub
requireNumberRestrictions (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ case Maybe DataRange
x of
    Nothing -> OWLSub
slBottom
    Just y :: DataRange
y -> DataRange -> OWLSub
slDataRange DataRange
y

slObjCard :: COPs -> Cardinality ObjectPropertyExpression ClassExpression -> OWLSub
slObjCard :: COPs
-> Cardinality ObjectPropertyExpression ClassExpression -> OWLSub
slObjCard cops :: COPs
cops (Cardinality _ _ op :: ObjectPropertyExpression
op x :: Maybe ClassExpression
x) = OWLSub -> OWLSub
requireNumberRestrictions (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$
    case Maybe ClassExpression
x of
        Nothing -> COPs -> ObjectPropertyExpression -> OWLSub
slSimpleObjectProp COPs
cops ObjectPropertyExpression
op
        Just y :: ClassExpression
y -> (if ClassExpression
y ClassExpression -> ClassExpression -> Bool
forall a. Eq a => a -> a -> Bool
== Datatype -> ClassExpression
Expression Datatype
owlThing then OWLSub -> OWLSub
forall a. a -> a
id else OWLSub -> OWLSub
requireQualNumberRestrictions) (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ 
            OWLSub -> OWLSub -> OWLSub
slMax (COPs -> ObjectPropertyExpression -> OWLSub
slSimpleObjectProp COPs
cops ObjectPropertyExpression
op) (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
y)

slSimpleObjectProp :: COPs -> ObjectPropertyExpression  -> OWLSub
slSimpleObjectProp :: COPs -> ObjectPropertyExpression -> OWLSub
slSimpleObjectProp cops :: COPs
cops ope :: ObjectPropertyExpression
ope = let sl :: OWLSub
sl = ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
ope in
    if ObjectPropertyExpression
ope ObjectPropertyExpression -> COPs -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` COPs
cops then OWLSub -> OWLSub
requireUnrestrictedDL OWLSub
sl else OWLSub
sl

slIArg :: IndividualArg -> OWLSub
slIArg :: IndividualArg -> OWLSub
slIArg arg :: IndividualArg
arg = case IndividualArg
arg of
    IArg i :: Datatype
i -> [Datatype] -> OWLSub
slIndividuals [Datatype
i]
    _ -> OWLSub
slBottom

slDArg :: DataArg -> OWLSub
slDArg :: DataArg -> OWLSub
slDArg arg :: DataArg
arg = case DataArg
arg of
    DArg l :: Literal
l -> Literal -> OWLSub
slLiteral Literal
l
    _ -> OWLSub
slBottom

slAtom :: COPs -> Atom -> OWLSub
slAtom :: COPs -> Atom -> OWLSub
slAtom cops :: COPs
cops atom :: Atom
atom = case Atom
atom of
    ClassAtom clExpr :: ClassExpression
clExpr iArg :: IndividualArg
iArg -> OWLSub -> OWLSub -> OWLSub
slMax (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
clExpr) (IndividualArg -> OWLSub
slIArg IndividualArg
iArg)
    DataRangeAtom dr :: DataRange
dr dArg :: DataArg
dArg -> OWLSub -> OWLSub -> OWLSub
slMax (DataRange -> OWLSub
slDataRange DataRange
dr) (DataArg -> OWLSub
slDArg DataArg
dArg)
    ObjectPropertyAtom opExpr :: ObjectPropertyExpression
opExpr iArg1 :: IndividualArg
iArg1 iArg2 :: IndividualArg
iArg2 -> [OWLSub] -> OWLSub
forall (t :: * -> *). Foldable t => t OWLSub -> OWLSub
slMaxs ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ [ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
opExpr, IndividualArg -> OWLSub
slIArg IndividualArg
iArg1, IndividualArg -> OWLSub
slIArg IndividualArg
iArg2]
    DataPropertyAtom _ iArg :: IndividualArg
iArg dArg :: DataArg
dArg -> OWLSub -> OWLSub -> OWLSub
slMax (IndividualArg -> OWLSub
slIArg IndividualArg
iArg) (DataArg -> OWLSub
slDArg DataArg
dArg)
    BuiltInAtom _ dArgs :: [DataArg]
dArgs -> [OWLSub] -> OWLSub
forall (t :: * -> *). Foldable t => t OWLSub -> OWLSub
slMaxs ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ DataArg -> OWLSub
slDArg (DataArg -> OWLSub) -> [DataArg] -> [OWLSub]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataArg]
dArgs
    SameIndividualAtom iArg1 :: IndividualArg
iArg1 iArg2 :: IndividualArg
iArg2 -> [OWLSub] -> OWLSub
forall (t :: * -> *). Foldable t => t OWLSub -> OWLSub
slMaxs ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ IndividualArg -> OWLSub
slIArg (IndividualArg -> OWLSub) -> [IndividualArg] -> [OWLSub]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [IndividualArg
iArg1, IndividualArg
iArg2]
    DifferentIndividualsAtom iArg1 :: IndividualArg
iArg1 iArg2 :: IndividualArg
iArg2 -> [OWLSub] -> OWLSub
forall (t :: * -> *). Foldable t => t OWLSub -> OWLSub
slMaxs ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ IndividualArg -> OWLSub
slIArg (IndividualArg -> OWLSub) -> [IndividualArg] -> [OWLSub]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [IndividualArg
iArg1, IndividualArg
iArg2]
    _ -> OWLSub
slBottom

slAxiom :: COPs -> Axiom -> OWLSub
slAxiom :: COPs -> Axiom -> OWLSub
slAxiom cops :: COPs
cops ax :: Axiom
ax = case Axiom
ax of
    Declaration annos :: [Annotation]
annos e :: Entity
e -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ Entity -> OWLSub
slEntity Entity
e 
    ClassAxiom cax :: ClassAxiom
cax -> case ClassAxiom
cax of
        SubClassOf annos :: [Annotation]
annos sub :: ClassExpression
sub sup :: ClassExpression
sup -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub -> OWLSub
slMax (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
sub) (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
sup)
        EquivalentClasses annos :: [Annotation]
annos clExprs :: [ClassExpression]
clExprs -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ (ClassExpression -> OWLSub) -> [ClassExpression] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops) [ClassExpression]
clExprs 
        DisjointClasses annos :: [Annotation]
annos clExprs :: [ClassExpression]
clExprs -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ (ClassExpression -> OWLSub) -> [ClassExpression] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops) [ClassExpression]
clExprs 
        DisjointUnion annos :: [Annotation]
annos _ clExprs :: [ClassExpression]
clExprs -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ (ClassExpression -> OWLSub) -> [ClassExpression] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops) [ClassExpression]
clExprs 
    ObjectPropertyAxiom opax :: ObjectPropertyAxiom
opax -> case ObjectPropertyAxiom
opax of
        SubObjectPropertyOf annos :: [Annotation]
annos subOpExpr :: SubObjectPropertyExpression
subOpExpr supOpExpr :: ObjectPropertyExpression
supOpExpr ->
            let oExprs :: [ObjectPropertyExpression]
oExprs = case SubObjectPropertyExpression
subOpExpr of
                    SubObjPropExpr_obj oExpr :: ObjectPropertyExpression
oExpr -> [ObjectPropertyExpression
oExpr]
                    SubObjPropExpr_exprchain e :: [ObjectPropertyExpression]
e -> [ObjectPropertyExpression]
e
            in [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireRoleHierarchy (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ (ObjectPropertyExpression -> OWLSub)
-> [ObjectPropertyExpression] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map ObjectPropertyExpression -> OWLSub
slObjProp (ObjectPropertyExpression
supOpExpr ObjectPropertyExpression
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. a -> [a] -> [a]
: [ObjectPropertyExpression]
oExprs) 
        EquivalentObjectProperties annos :: [Annotation]
annos oExprs :: [ObjectPropertyExpression]
oExprs -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ (ObjectPropertyExpression -> OWLSub)
-> [ObjectPropertyExpression] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map ObjectPropertyExpression -> OWLSub
slObjProp [ObjectPropertyExpression]
oExprs 
        DisjointObjectProperties annos :: [Annotation]
annos oExprs :: [ObjectPropertyExpression]
oExprs -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax (OWLSub -> OWLSub
requireAddFeatures OWLSub
slBottom) ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ (ObjectPropertyExpression -> OWLSub)
-> [ObjectPropertyExpression] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map (COPs -> ObjectPropertyExpression -> OWLSub
slSimpleObjectProp COPs
cops) [ObjectPropertyExpression]
oExprs 
        InverseObjectProperties annos :: [Annotation]
annos e1 :: ObjectPropertyExpression
e1 e2 :: ObjectPropertyExpression
e2 -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireInverseRoles (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub -> OWLSub
slMax (ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
e1) (ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
e2)
        ObjectPropertyDomain annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr cExpr :: ClassExpression
cExpr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub -> OWLSub
slMax (ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
oExpr) (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
cExpr)
        ObjectPropertyRange annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr cExpr :: ClassExpression
cExpr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub -> OWLSub
slMax (ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
oExpr) (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
cExpr)
        FunctionalObjectProperty annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ COPs -> ObjectPropertyExpression -> OWLSub
slSimpleObjectProp COPs
cops ObjectPropertyExpression
oExpr
        InverseFunctionalObjectProperty annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireInverseRoles (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ COPs -> ObjectPropertyExpression -> OWLSub
slSimpleObjectProp COPs
cops ObjectPropertyExpression
oExpr
        ReflexiveObjectProperty annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireAddFeatures (ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
oExpr)
        IrreflexiveObjectProperty annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireAddFeatures (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ COPs -> ObjectPropertyExpression -> OWLSub
slSimpleObjectProp COPs
cops ObjectPropertyExpression
oExpr
        SymmetricObjectProperty annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
oExpr
        AsymmetricObjectProperty annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireAddFeatures (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ COPs -> ObjectPropertyExpression -> OWLSub
slSimpleObjectProp COPs
cops ObjectPropertyExpression
oExpr
        TransitiveObjectProperty annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireRoleTransitivity (ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
oExpr)
    DataPropertyAxiom a :: DataPropertyAxiom
a -> case DataPropertyAxiom
a of
        SubDataPropertyOf annos :: [Annotation]
annos sub :: Datatype
sub _ -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireRoleHierarchy (OWLSub -> OWLSub) -> (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            (if Datatype
topDataProperty Datatype -> Datatype -> Bool
forall a. Eq a => a -> a -> Bool
== Datatype
sub then OWLSub -> OWLSub
requireUnrestrictedDL else OWLSub -> OWLSub
forall a. a -> a
id) (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$
            OWLSub
slBottom
        EquivalentDataProperties annos :: [Annotation]
annos _ -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub
slBottom
        DisjointDataProperties annos :: [Annotation]
annos _ -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireAddFeatures OWLSub
slBottom
        DataPropertyDomain annos :: [Annotation]
annos _ cExpr :: ClassExpression
cExpr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
cExpr
        DataPropertyRange annos :: [Annotation]
annos _ r :: DataRange
r -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ DataRange -> OWLSub
slDataRange DataRange
r
        FunctionalDataProperty annos :: [Annotation]
annos _ -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub
slBottom
    DatatypeDefinition annos :: [Annotation]
annos dt :: Datatype
dt dr :: DataRange
dr -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub -> OWLSub
slMax (Datatype -> OWLSub
slDatatype Datatype
dt) (DataRange -> OWLSub
slDataRange DataRange
dr)
    HasKey annos :: [Annotation]
annos cExpr :: ClassExpression
cExpr oExprs :: [ObjectPropertyExpression]
oExprs _ -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax (COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
cExpr)
        ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ (ObjectPropertyExpression -> OWLSub)
-> [ObjectPropertyExpression] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map ObjectPropertyExpression -> OWLSub
slObjProp [ObjectPropertyExpression]
oExprs 
    Assertion a :: Assertion
a -> case Assertion
a of
        SameIndividual annos :: [Annotation]
annos is :: [Datatype]
is -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireNominals (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ [Datatype] -> OWLSub
slIndividuals [Datatype]
is
        DifferentIndividuals annos :: [Annotation]
annos is :: [Datatype]
is -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireNominals  (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ [Datatype] -> OWLSub
slIndividuals [Datatype]
is
        ClassAssertion annos :: [Annotation]
annos clExpr :: ClassExpression
clExpr _ -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ COPs -> ClassExpression -> OWLSub
slClassExpression COPs
cops ClassExpression
clExpr
        ObjectPropertyAssertion annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr si :: Datatype
si ti :: Datatype
ti -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub -> OWLSub
slMax (ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
oExpr) ([Datatype] -> OWLSub
slIndividuals [Datatype
si, Datatype
ti])
        NegativeObjectPropertyAssertion annos :: [Annotation]
annos oExpr :: ObjectPropertyExpression
oExpr si :: Datatype
si ti :: Datatype
ti -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub -> OWLSub
slMax (ObjectPropertyExpression -> OWLSub
slObjProp ObjectPropertyExpression
oExpr) ([Datatype] -> OWLSub
slIndividuals [Datatype
si, Datatype
ti])
        DataPropertyAssertion annos :: [Annotation]
annos _ _ l :: Literal
l -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ Literal -> OWLSub
slLiteral Literal
l
        NegativeDataPropertyAssertion annos :: [Annotation]
annos _ _ l :: Literal
l -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ Literal -> OWLSub
slLiteral Literal
l
    AnnotationAxiom a :: AnnotationAxiom
a -> case AnnotationAxiom
a of
        AnnotationAssertion annos :: [Annotation]
annos _ _ _ -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub
slBottom 
        SubAnnotationPropertyOf annos :: [Annotation]
annos _ _ -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub -> OWLSub
requireRoleHierarchy OWLSub
slBottom
        AnnotationPropertyDomain annos :: [Annotation]
annos _ _ -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub
slBottom
        AnnotationPropertyRange annos :: [Annotation]
annos _ _ -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLSub
slBottom
    Rule r :: Rule
r -> OWLSub -> OWLSub
requireRules (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ case Rule
r of
        DLSafeRule annos :: [Annotation]
annos b :: Body
b h :: Body
h -> [Annotation] -> OWLSub -> OWLSub
slAnnosAnd [Annotation]
annos (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ COPs -> Atom -> OWLSub
slAtom COPs
cops (Atom -> OWLSub) -> Body -> [OWLSub]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Body
b Body -> Body -> Body
forall a. [a] -> [a] -> [a]
++ Body
h)
        _ -> OWLSub
slBottom
    _ -> OWLSub
slBottom


-- | Checks only for general restrictions 
slGeneralRestrictions :: [Axiom] -> OWLSub
slGeneralRestrictions :: [Axiom] -> OWLSub
slGeneralRestrictions axs :: [Axiom]
axs = 
    let dts :: [(Datatype, DataRange)]
dts = (Axiom -> Maybe (Datatype, DataRange))
-> [Axiom] -> [(Datatype, DataRange)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ax :: Axiom
ax -> case Axiom
ax of
            DatatypeDefinition _ dt :: Datatype
dt dr :: DataRange
dr -> (Datatype, DataRange) -> Maybe (Datatype, DataRange)
forall a. a -> Maybe a
Just (Datatype
dt, DataRange
dr)
            _ -> Maybe (Datatype, DataRange)
forall a. Maybe a
Nothing) [Axiom]
axs
        is :: [(Datatype, Datatype)]
is = (Axiom -> Maybe (Datatype, Datatype))
-> [Axiom] -> [(Datatype, Datatype)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ax :: Axiom
ax -> case Axiom
ax of
            Assertion (ObjectPropertyAssertion _ _ s :: Datatype
s t :: Datatype
t) -> (Datatype, Datatype) -> Maybe (Datatype, Datatype)
forall a. a -> Maybe a
Just (Datatype
s, Datatype
t)
            _ -> Maybe (Datatype, Datatype)
forall a. Maybe a
Nothing) [Axiom]
axs
        es :: [Entity]
es = (Axiom -> Maybe Entity) -> [Axiom] -> [Entity]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ax :: Axiom
ax -> case Axiom
ax of
            Declaration _ e :: Entity
e -> Entity -> Maybe Entity
forall a. a -> Maybe a
Just Entity
e
            _ -> Maybe Entity
forall a. Maybe a
Nothing) [Axiom]
axs
    in
    (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$
        [ [(Datatype, DataRange)] -> OWLSub
slGDatatypes [(Datatype, DataRange)]
dts
        , [Axiom] -> OWLSub
slGPropertyHierachy [Axiom]
axs
        , [(Datatype, Datatype)] -> OWLSub
slGAnonymousIndividuals [(Datatype, Datatype)]
is
        , [Entity] -> OWLSub
slGTypingConstraints [Entity]
es
        ]

slGTypingConstraints :: [Entity] -> OWLSub
slGTypingConstraints :: [Entity] -> OWLSub
slGTypingConstraints declared :: [Entity]
declared = 
    if (Set EntityType -> Bool) -> [Set EntityType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Set EntityType -> Bool
obeysRestriction ([Set EntityType] -> Bool) -> [Set EntityType] -> Bool
forall a b. (a -> b) -> a -> b
$ Map Datatype (Set EntityType) -> [Set EntityType]
forall k a. Map k a -> [a]
Map.elems Map Datatype (Set EntityType)
entityMap then OWLSub
slBottom else OWLSub -> OWLSub
requireUnrestrictedDL OWLSub
slBottom where
    entityMap :: Map Datatype (Set EntityType)
entityMap = (Map Datatype (Set EntityType)
 -> Entity -> Map Datatype (Set EntityType))
-> Map Datatype (Set EntityType)
-> [Entity]
-> Map Datatype (Set EntityType)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\m :: Map Datatype (Set EntityType)
m (Entity _ k :: EntityType
k i :: Datatype
i) -> (Set EntityType -> Set EntityType -> Set EntityType)
-> Datatype
-> Set EntityType
-> Map Datatype (Set EntityType)
-> Map Datatype (Set EntityType)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set EntityType -> Set EntityType -> Set EntityType
forall a. Ord a => Set a -> Set a -> Set a
Set.union Datatype
i (EntityType -> Set EntityType
forall a. a -> Set a
Set.singleton EntityType
k) Map Datatype (Set EntityType)
m) Map Datatype (Set EntityType)
forall k a. Map k a
Map.empty [Entity]
declared
    obeysRestriction :: Set EntityType -> Bool
obeysRestriction ks :: Set EntityType
ks = (Set EntityType -> Bool) -> [Set EntityType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(>=) 1 (Int -> Bool) -> (Set EntityType -> Int) -> Set EntityType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set EntityType -> Int
forall a. Set a -> Int
Set.size (Set EntityType -> Int)
-> (Set EntityType -> Set EntityType) -> Set EntityType -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set EntityType -> Set EntityType -> Set EntityType
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set EntityType
ks) ([Set EntityType] -> Bool) -> [Set EntityType] -> Bool
forall a b. (a -> b) -> a -> b
$ [EntityType] -> Set EntityType
forall a. Ord a => [a] -> Set a
Set.fromList ([EntityType] -> Set EntityType)
-> [[EntityType]] -> [Set EntityType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [
        [EntityType
ObjectProperty, EntityType
DataProperty, EntityType
AnnotationProperty],
        [EntityType
Datatype, EntityType
Class]]


-- | Analyses the datatypes for a circle in their definition
slGDatatypes :: [(Datatype, DataRange)] -> OWLSub 
slGDatatypes :: [(Datatype, DataRange)] -> OWLSub
slGDatatypes ax :: [(Datatype, DataRange)]
ax = if [SCC (Datatype, DataRange)] -> Bool
forall a. [SCC a] -> Bool
isCyclic [SCC (Datatype, DataRange)]
comps then
        OWLSub -> OWLSub
requireUnrestrictedDL OWLSub
slBottom
    else OWLSub
slBottom where
    comps :: [SCC (Datatype, DataRange)]
comps = [((Datatype, DataRange), Datatype, [Datatype])]
-> [SCC (Datatype, DataRange)]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp ([((Datatype, DataRange), Datatype, [Datatype])]
 -> [SCC (Datatype, DataRange)])
-> [((Datatype, DataRange), Datatype, [Datatype])]
-> [SCC (Datatype, DataRange)]
forall a b. (a -> b) -> a -> b
$ ((Datatype, DataRange)
 -> ((Datatype, DataRange), Datatype, [Datatype]))
-> [(Datatype, DataRange)]
-> [((Datatype, DataRange), Datatype, [Datatype])]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: (Datatype, DataRange)
x -> ((Datatype, DataRange)
x, (Datatype, DataRange) -> Datatype
forall a b. (a, b) -> a
fst (Datatype, DataRange)
x, DataRange -> [Datatype]
basedOn (DataRange -> [Datatype])
-> ((Datatype, DataRange) -> DataRange)
-> (Datatype, DataRange)
-> [Datatype]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Datatype, DataRange) -> DataRange
forall a b. (a, b) -> b
snd ((Datatype, DataRange) -> [Datatype])
-> (Datatype, DataRange) -> [Datatype]
forall a b. (a -> b) -> a -> b
$ (Datatype, DataRange)
x)) [(Datatype, DataRange)]
ax

type Graph a = Map.Map a (Set.Set a)

addEdge :: Ord a => a -> a -> Graph a -> Graph a
addEdge :: a -> a -> Graph a -> Graph a
addEdge from :: a
from to :: a
to = (Set a -> Set a -> Set a) -> a -> Set a -> Graph a -> Graph a
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union a
from (a -> Set a
forall a. a -> Set a
Set.singleton a
to) (Graph a -> Graph a) -> (Graph a -> Graph a) -> Graph a -> Graph a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (Set a -> Set a -> Set a) -> a -> Set a -> Graph a -> Graph a
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union a
to Set a
forall a. Set a
Set.empty

-- | @connected x g@ yields all nodes connected to x with an edge in g
connected :: Ord a => a -> Graph a -> Set.Set a
connected :: a -> Graph a -> Set a
connected = Set a -> a -> Graph a -> Set a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set a
forall a. Set a
Set.empty

-- | Checks whether an undirected graph is cyclic
isCyclicU :: Ord a => Graph a -> Bool
isCyclicU :: Graph a -> Bool
isCyclicU g :: Graph a
g = case Graph a -> [a]
forall k a. Map k a -> [k]
Map.keys Graph a
g of
    [] -> Bool
False
    (h :: a
h:_) -> (Bool, Set a) -> Bool
forall a b. (a, b) -> a
fst ((Bool, Set a) -> Bool) -> (Bool, Set a) -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Graph a -> a -> Maybe a -> Set a -> (Bool, Set a)
forall a.
Ord a =>
Bool -> Graph a -> a -> Maybe a -> Set a -> (Bool, Set a)
isCyclic' Bool
False Graph a
g a
h Maybe a
forall a. Maybe a
Nothing (Graph a -> Set a
forall k a. Map k a -> Set k
Map.keysSet Graph a
g)

isCyclicD :: Ord a => Graph a -> Bool
isCyclicD :: Graph a -> Bool
isCyclicD g :: Graph a
g = case Graph a -> [a]
forall k a. Map k a -> [k]
Map.keys Graph a
g of
    [] -> Bool
False
    (h :: a
h:_) -> (Bool, Set a) -> Bool
forall a b. (a, b) -> a
fst ((Bool, Set a) -> Bool) -> (Bool, Set a) -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Graph a -> a -> Maybe a -> Set a -> (Bool, Set a)
forall a.
Ord a =>
Bool -> Graph a -> a -> Maybe a -> Set a -> (Bool, Set a)
isCyclic' Bool
True Graph a
g a
h Maybe a
forall a. Maybe a
Nothing (Graph a -> Set a
forall k a. Map k a -> Set k
Map.keysSet Graph a
g)


-- | @isCyclic' directed g v p r@ checks if a cycle can be found in @g@ starting at vertex @v@ with parent @p@ and not visited vertices @r@
isCyclic' :: Ord a => Bool -> Graph a -> a -> Maybe a -> Set.Set a -> (Bool, Set.Set a)
isCyclic' :: Bool -> Graph a -> a -> Maybe a -> Set a -> (Bool, Set a)
isCyclic' directed :: Bool
directed g :: Graph a
g v :: a
v p :: Maybe a
p remaining :: Set a
remaining = let remaining' :: Set a
remaining' = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.delete a
v Set a
remaining in
    ((Bool, Set a) -> a -> (Bool, Set a))
-> (Bool, Set a) -> Set a -> (Bool, Set a)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(b :: Bool
b, r :: Set a
r) c :: a
c -> if Bool
b then (Bool
b, Set a
r) else if a
c a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set a
r then 
            Bool -> Graph a -> a -> Maybe a -> Set a -> (Bool, Set a)
forall a.
Ord a =>
Bool -> Graph a -> a -> Maybe a -> Set a -> (Bool, Set a)
isCyclic' Bool
directed Graph a
g a
c (a -> Maybe a
forall a. a -> Maybe a
Just a
v) Set a
r
        else (Bool
directed Bool -> Bool -> Bool
|| a -> Maybe a
forall a. a -> Maybe a
Just a
c Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe a
p, Set a
r)) (Bool
False, Set a
remaining') (Set a -> a -> Graph a -> Set a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set a
forall a. Set a
Set.empty a
v Graph a
g)

-- | @forest g@ Given that @g@ is acyclic, transforms @g@ to a forest
forest :: Ord a => Graph a -> Forest a
forest :: Graph a -> Forest a
forest g :: Graph a
g = case Graph a -> [a]
forall k a. Map k a -> [k]
Map.keys Graph a
g of
    [] -> []
    (h :: a
h:_) -> let (t :: Tree a
t, g' :: Graph a
g') = Graph a -> a -> (Tree a, Graph a)
forall a. Ord a => Graph a -> a -> (Tree a, Graph a)
buildTree Graph a
g a
h in Tree a
t Tree a -> Forest a -> Forest a
forall a. a -> [a] -> [a]
: Graph a -> Forest a
forall a. Ord a => Graph a -> Forest a
forest Graph a
g'

-- | @reachable r g@ returns all reachable nodes from @r@ in @g@
reachable :: Ord a => a -> Graph a -> Set.Set a
reachable :: a -> Graph a -> Set a
reachable r :: a
r g :: Graph a
g = Graph a -> Set a -> a -> Set a
forall a. Ord a => Graph a -> Set a -> a -> Set a
reachable' Graph a
g (a -> Set a
forall a. a -> Set a
Set.singleton a
r) a
r

-- | @reachable' g visited r@ returns all reachable unvisited nodes from @r@ in @g@ 
reachable' :: Ord a => Graph a -> Set.Set a -> a -> Set.Set a
reachable' :: Graph a -> Set a -> a -> Set a
reachable' g :: Graph a
g visited :: Set a
visited r :: a
r = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set a
c (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ [Set a] -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set a] -> Set a)
-> (Set (Set a) -> [Set a]) -> Set (Set a) -> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set a) -> [Set a]
forall a. Set a -> [a]
Set.toList (Set (Set a) -> Set a) -> Set (Set a) -> Set a
forall a b. (a -> b) -> a -> b
$ (a -> Set a) -> Set a -> Set (Set a)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Graph a -> Set a -> a -> Set a
forall a. Ord a => Graph a -> Set a -> a -> Set a
reachable' Graph a
g (Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set a
visited Set a
c)) Set a
c where
    c :: Set a
c = (a -> Graph a -> Set a
forall a. Ord a => a -> Graph a -> Set a
connected a
r Graph a
g) Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set a
visited

inverse :: Ord a => Graph a -> Graph a
inverse :: Graph a -> Graph a
inverse g :: Graph a
g = ((a, Set a) -> Graph a -> Graph a)
-> Graph a -> [(a, Set a)] -> Graph a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(n :: a
n, outs :: Set a
outs) g' :: Graph a
g' -> (a -> Graph a -> Graph a) -> Graph a -> Set a -> Graph a
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr (\o :: a
o g'' :: Graph a
g''  -> a -> a -> Graph a -> Graph a
forall a. Ord a => a -> a -> Graph a -> Graph a
addEdge a
o a
n Graph a
g'') Graph a
g' Set a
outs) Graph a
forall k a. Map k a
Map.empty (Graph a -> [(a, Set a)]
forall k a. Map k a -> [(k, a)]
Map.toList Graph a
g)

-- | @components  g@ gets the components of @g@
components :: Ord a => Graph a -> [Graph a]
components :: Graph a -> [Graph a]
components graph :: Graph a
graph = case Graph a -> [a]
forall k a. Map k a -> [k]
Map.keys Graph a
graph of
    [] -> []
    (h :: a
h:_) -> let (c :: Graph a
c, g' :: Graph a
g') = Graph a -> a -> (Graph a, Graph a)
forall a. Ord a => Graph a -> a -> (Graph a, Graph a)
compsOf Graph a
graph a
h in Graph a
c Graph a -> [Graph a] -> [Graph a]
forall a. a -> [a] -> [a]
: Graph a -> [Graph a]
forall a. Ord a => Graph a -> [Graph a]
components Graph a
g'
    where
    compsOf :: Graph a -> a -> (Graph a, Graph a)
compsOf graph' :: Graph a
graph' r :: a
r = (a -> Set a -> Bool) -> Graph a -> (Graph a, Graph a)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\k :: a
k _ -> a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
k Bool -> Bool -> Bool
|| a
k a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` (a -> Graph a -> Set a
forall a. Ord a => a -> Graph a -> Set a
reachable a
r Graph a
graph')) Graph a
graph'

-- | @buildTree g r@ given that @g@ is acyclic, transforms @g@ into a tree with @r@ as root node and returns the remaining graph
buildTree :: Ord a => Graph a -> a -> (Tree a, Graph a)
buildTree :: Graph a -> a -> (Tree a, Graph a)
buildTree graph :: Graph a
graph r :: a
r = (a -> Forest a -> Tree a
forall a. a -> Forest a -> Tree a
Node a
r Forest a
f, Graph a
g') where
    g :: Graph a
g = a -> Graph a -> Graph a
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete a
r Graph a
graph
    (f :: Forest a
f, g' :: Graph a
g') = ((Forest a, Graph a) -> a -> (Forest a, Graph a))
-> (Forest a, Graph a) -> Set a -> (Forest a, Graph a)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(f' :: Forest a
f', g'' :: Graph a
g'') v :: a
v ->
        let (tree :: Tree a
tree, g''' :: Graph a
g''') = Graph a -> a -> (Tree a, Graph a)
forall a. Ord a => Graph a -> a -> (Tree a, Graph a)
buildTree Graph a
g'' a
v in 
            (Tree a
tree Tree a -> Forest a -> Forest a
forall a. a -> [a] -> [a]
: Forest a
f', Graph a
g''')) ([] :: [Tree a], Graph a
g) (Set a -> (Forest a, Graph a)) -> Set a -> (Forest a, Graph a)
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> Set a -> Set a
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
r) (Set a -> a -> Graph a -> Set a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set a
forall a. Set a
Set.empty a
r Graph a
graph)

slGAnonymousIndividuals :: [(Individual, Individual)] -> OWLSub
slGAnonymousIndividuals :: [(Datatype, Datatype)] -> OWLSub
slGAnonymousIndividuals edges :: [(Datatype, Datatype)]
edges = if (Graph Datatype -> Bool) -> [Graph Datatype] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Graph Datatype -> Bool
forall a. Ord a => Graph a -> Bool
isCyclicU [Graph Datatype]
comps Bool -> Bool -> Bool
|| Bool -> Bool
not ((Tree Datatype -> Bool) -> [Tree Datatype] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\t :: Tree Datatype
t -> (Datatype -> Bool) -> Tree Datatype -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\x :: Datatype
x -> Set Datatype -> Int
forall a. Set a -> Int
Set.size ((Datatype -> Bool) -> Set Datatype -> Set Datatype
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Datatype -> Bool) -> Datatype -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Datatype -> Bool
isAnonymous) (Datatype -> Graph Datatype -> Set Datatype
forall a. Ord a => a -> Graph a -> Set a
connected Datatype
x Graph Datatype
g')) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 1) Tree Datatype
t) [Tree Datatype]
f) then
        OWLSub -> OWLSub
requireUnrestrictedDL OWLSub
slBottom
    else OWLSub
slBottom where
    edges' :: [(Datatype, Datatype)]
edges' = [(Datatype, Datatype)]
edges [(Datatype, Datatype)]
-> [(Datatype, Datatype)] -> [(Datatype, Datatype)]
forall a. [a] -> [a] -> [a]
++ [(Datatype
y,Datatype
x) | (x :: Datatype
x,y :: Datatype
y) <- [(Datatype, Datatype)]
edges]
    g :: Graph Datatype
g = (Graph Datatype -> (Datatype, Datatype) -> Graph Datatype)
-> Graph Datatype -> [(Datatype, Datatype)] -> Graph Datatype
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\m :: Graph Datatype
m (x :: Datatype
x,y :: Datatype
y) -> (Set Datatype -> Set Datatype -> Set Datatype)
-> Datatype -> Set Datatype -> Graph Datatype -> Graph Datatype
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set Datatype -> Set Datatype -> Set Datatype
forall a. Ord a => Set a -> Set a -> Set a
Set.union Datatype
x (if Datatype -> Bool
isAnonymous Datatype
y then Datatype -> Set Datatype
forall a. a -> Set a
Set.singleton Datatype
y else Set Datatype
forall a. Set a
Set.empty) Graph Datatype
m) Graph Datatype
forall k a. Map k a
Map.empty (((Datatype, Datatype) -> Bool)
-> [(Datatype, Datatype)] -> [(Datatype, Datatype)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Datatype -> Bool
isAnonymous (Datatype -> Bool)
-> ((Datatype, Datatype) -> Datatype)
-> (Datatype, Datatype)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Datatype, Datatype) -> Datatype
forall a b. (a, b) -> a
fst) [(Datatype, Datatype)]
edges')
    g' :: Graph Datatype
g' = (Graph Datatype -> (Datatype, Datatype) -> Graph Datatype)
-> Graph Datatype -> [(Datatype, Datatype)] -> Graph Datatype
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\m :: Graph Datatype
m (x :: Datatype
x,y :: Datatype
y) -> (Set Datatype -> Set Datatype -> Set Datatype)
-> Datatype -> Set Datatype -> Graph Datatype -> Graph Datatype
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set Datatype -> Set Datatype -> Set Datatype
forall a. Ord a => Set a -> Set a -> Set a
Set.union Datatype
x (Datatype -> Set Datatype
forall a. a -> Set a
Set.singleton Datatype
y) Graph Datatype
m) Graph Datatype
forall k a. Map k a
Map.empty [(Datatype, Datatype)]
edges'
    comps :: [Graph Datatype]
comps = Graph Datatype -> [Graph Datatype]
forall a. Ord a => Graph a -> [Graph a]
components Graph Datatype
g
    f :: [Tree Datatype]
f = Graph Datatype -> [Tree Datatype]
forall a. Ord a => Graph a -> Forest a
forest Graph Datatype
g


slGPropertyHierachy :: [Axiom] -> OWLSub
slGPropertyHierachy :: [Axiom] -> OWLSub
slGPropertyHierachy axs :: [Axiom]
axs = if Bool
verify then OWLSub
slBottom else OWLSub -> OWLSub
requireUnrestrictedDL OWLSub
slBottom where
    ops :: [([ObjectPropertyExpression], ObjectPropertyExpression)]
ops = (Axiom
 -> Maybe ([ObjectPropertyExpression], ObjectPropertyExpression))
-> [Axiom]
-> [([ObjectPropertyExpression], ObjectPropertyExpression)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ax :: Axiom
ax -> case Axiom
ax of
            ObjectPropertyAxiom (SubObjectPropertyOf _ (SubObjPropExpr_exprchain ch :: [ObjectPropertyExpression]
ch) ope :: ObjectPropertyExpression
ope) -> ([ObjectPropertyExpression], ObjectPropertyExpression)
-> Maybe ([ObjectPropertyExpression], ObjectPropertyExpression)
forall a. a -> Maybe a
Just ([ObjectPropertyExpression]
ch, ObjectPropertyExpression
ope)
            _ -> Maybe ([ObjectPropertyExpression], ObjectPropertyExpression)
forall a. Maybe a
Nothing) [Axiom]
axs
    hierachy :: Graph ObjectPropertyExpression
hierachy = [Axiom] -> Graph ObjectPropertyExpression
objectPropertyHierachy [Axiom]
axs
    ord :: Graph Datatype
ord = [([ObjectPropertyExpression], ObjectPropertyExpression)]
-> Graph Datatype
objectPropertyOrder [([ObjectPropertyExpression], ObjectPropertyExpression)]
ops
    verify :: Bool
verify = Bool -> Bool
not (Graph Datatype -> Bool
forall a. Ord a => Graph a -> Bool
isCyclicD Graph Datatype
ord) Bool -> Bool -> Bool
&& (Datatype -> Bool) -> [Datatype] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\v :: Datatype
v -> (Datatype -> Bool) -> [Datatype] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\v' :: Datatype
v' -> Datatype -> ObjectPropertyExpression
ObjectProp Datatype
v ObjectPropertyExpression -> COPs -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` ObjectPropertyExpression -> Graph ObjectPropertyExpression -> COPs
forall a. Ord a => a -> Graph a -> Set a
reachable (Datatype -> ObjectPropertyExpression
ObjectProp Datatype
v') Graph ObjectPropertyExpression
hierachy) ([Datatype] -> Bool) -> [Datatype] -> Bool
forall a b. (a -> b) -> a -> b
$ Set Datatype -> [Datatype]
forall a. Set a -> [a]
Set.toList (Set Datatype -> [Datatype]) -> Set Datatype -> [Datatype]
forall a b. (a -> b) -> a -> b
$ Set Datatype -> Datatype -> Graph Datatype -> Set Datatype
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set Datatype
forall a. Set a
Set.empty Datatype
v Graph Datatype
ord) (Graph Datatype -> [Datatype]
forall k a. Map k a -> [k]
Map.keys Graph Datatype
ord)

-- | Whether a direct graph is cyclic
isCyclic :: [SCC a] -> Bool
isCyclic :: [SCC a] -> Bool
isCyclic = Int -> [SCC a] -> Bool
forall a. Int -> [SCC a] -> Bool
containsCircle 1

-- | @containsCircle len comps@ Checks whether @comps@ contain a circle of min length @len@
containsCircle :: Int -> [SCC a] -> Bool
containsCircle :: Int -> [SCC a] -> Bool
containsCircle len :: Int
len comps :: [SCC a]
comps = (SCC a -> Bool) -> [SCC a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SCC a -> Bool
forall a. SCC a -> Bool
cyclic [SCC a]
comps where
    cyclic :: SCC a -> Bool
cyclic s :: SCC a
s = case SCC a
s of
        CyclicSCC circle :: [a]
circle | [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
circle Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
len -> Bool
True
        _ -> Bool
False

type COPs = Set.Set ObjectPropertyExpression

compositeObjectProperties :: [Axiom] -> Set.Set ObjectPropertyExpression
compositeObjectProperties :: [Axiom] -> COPs
compositeObjectProperties axs :: [Axiom]
axs = [ObjectPropertyExpression] -> COPs
forall a. Ord a => [a] -> Set a
Set.fromList ([ObjectPropertyExpression] -> COPs)
-> [ObjectPropertyExpression] -> COPs
forall a b. (a -> b) -> a -> b
$
    Datatype -> ObjectPropertyExpression
ObjectProp Datatype
topObjectProperty ObjectPropertyExpression
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. a -> [a] -> [a]
:
    Datatype -> ObjectPropertyExpression
ObjectProp Datatype
bottomObjectProperty ObjectPropertyExpression
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. a -> [a] -> [a]
:
    (Axiom -> Maybe ObjectPropertyExpression)
-> [Axiom] -> [ObjectPropertyExpression]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ax :: Axiom
ax -> case Axiom
ax of
        ObjectPropertyAxiom (SubObjectPropertyOf _ (SubObjPropExpr_exprchain c :: [ObjectPropertyExpression]
c) ope :: ObjectPropertyExpression
ope)
            | [ObjectPropertyExpression] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ObjectPropertyExpression]
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 -> ObjectPropertyExpression -> Maybe ObjectPropertyExpression
forall a. a -> Maybe a
Just ObjectPropertyExpression
ope
        ObjectPropertyAxiom (TransitiveObjectProperty _ ope :: ObjectPropertyExpression
ope) -> ObjectPropertyExpression -> Maybe ObjectPropertyExpression
forall a. a -> Maybe a
Just ObjectPropertyExpression
ope
        _ -> Maybe ObjectPropertyExpression
forall a. Maybe a
Nothing
        ) [Axiom]
axs

-- | Extracts the object property hierachy as an adjacency list.
--
--   Each object property expression has an edge according to https://www.w3.org/TR/2012/REC-owl2-syntax-20121211/#Property_Hierarchy_and_Simple_Object_Property_Expressions
objectPropertyHierachy :: [Axiom] -> Graph ObjectPropertyExpression
objectPropertyHierachy :: [Axiom] -> Graph ObjectPropertyExpression
objectPropertyHierachy = (Axiom
 -> Graph ObjectPropertyExpression
 -> Graph ObjectPropertyExpression)
-> Graph ObjectPropertyExpression
-> [Axiom]
-> Graph ObjectPropertyExpression
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ax :: Axiom
ax m :: Graph ObjectPropertyExpression
m -> case Axiom
ax of
        ObjectPropertyAxiom (SubObjectPropertyOf _ (SubObjPropExpr_obj o1 :: ObjectPropertyExpression
o1) o2 :: ObjectPropertyExpression
o2) ->
            ObjectPropertyExpression
-> ObjectPropertyExpression
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
ins ObjectPropertyExpression
o2 ObjectPropertyExpression
o1 Graph ObjectPropertyExpression
m
        ObjectPropertyAxiom (EquivalentObjectProperties _ ops :: [ObjectPropertyExpression]
ops) ->
            (ObjectPropertyExpression
 -> Graph ObjectPropertyExpression
 -> Graph ObjectPropertyExpression)
-> Graph ObjectPropertyExpression
-> [ObjectPropertyExpression]
-> Graph ObjectPropertyExpression
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\o2 :: ObjectPropertyExpression
o2 -> ObjectPropertyExpression
-> [ObjectPropertyExpression]
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
insl ObjectPropertyExpression
o2 [ObjectPropertyExpression
o1 | ObjectPropertyExpression
o1 <- [ObjectPropertyExpression]
ops, ObjectPropertyExpression
o1 ObjectPropertyExpression -> ObjectPropertyExpression -> Bool
forall a. Eq a => a -> a -> Bool
/= ObjectPropertyExpression
o2]) Graph ObjectPropertyExpression
m [ObjectPropertyExpression]
ops
        ObjectPropertyAxiom (InverseObjectProperties _ o1 :: ObjectPropertyExpression
o1 o2 :: ObjectPropertyExpression
o2) ->
            ObjectPropertyExpression
-> ObjectPropertyExpression
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
ins (ObjectPropertyExpression -> ObjectPropertyExpression
inverseOf ObjectPropertyExpression
o2) ObjectPropertyExpression
o1 (Graph ObjectPropertyExpression -> Graph ObjectPropertyExpression)
-> Graph ObjectPropertyExpression -> Graph ObjectPropertyExpression
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression
-> ObjectPropertyExpression
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
ins ObjectPropertyExpression
o1 (ObjectPropertyExpression -> ObjectPropertyExpression
inverseOf ObjectPropertyExpression
o2) Graph ObjectPropertyExpression
m
        ObjectPropertyAxiom (SymmetricObjectProperty _ o :: ObjectPropertyExpression
o) ->
            ObjectPropertyExpression
-> ObjectPropertyExpression
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
ins (ObjectPropertyExpression -> ObjectPropertyExpression
inverseOf ObjectPropertyExpression
o) ObjectPropertyExpression
o (Graph ObjectPropertyExpression -> Graph ObjectPropertyExpression)
-> Graph ObjectPropertyExpression -> Graph ObjectPropertyExpression
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression
-> ObjectPropertyExpression
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
ins ObjectPropertyExpression
o (ObjectPropertyExpression -> ObjectPropertyExpression
inverseOf ObjectPropertyExpression
o) Graph ObjectPropertyExpression
m
        _ -> Graph ObjectPropertyExpression
m) Graph ObjectPropertyExpression
forall k a. Map k a
Map.empty
    where
        ins :: ObjectPropertyExpression
-> ObjectPropertyExpression
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
ins k :: ObjectPropertyExpression
k v :: ObjectPropertyExpression
v m :: Graph ObjectPropertyExpression
m = ObjectPropertyExpression
-> [ObjectPropertyExpression]
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
insl ObjectPropertyExpression
k [ObjectPropertyExpression
k, ObjectPropertyExpression
v] Graph ObjectPropertyExpression
m -- also add self for reflexive closure
        insl :: ObjectPropertyExpression
-> [ObjectPropertyExpression]
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
insl k :: ObjectPropertyExpression
k v :: [ObjectPropertyExpression]
v m :: Graph ObjectPropertyExpression
m = (COPs -> COPs -> COPs)
-> ObjectPropertyExpression
-> COPs
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (COPs -> COPs -> COPs
forall a. Ord a => Set a -> Set a -> Set a
Set.union) ObjectPropertyExpression
k ([ObjectPropertyExpression] -> COPs
forall a. Ord a => [a] -> Set a
Set.fromList [ObjectPropertyExpression]
v) (Graph ObjectPropertyExpression -> Graph ObjectPropertyExpression)
-> Graph ObjectPropertyExpression -> Graph ObjectPropertyExpression
forall a b. (a -> b) -> a -> b
$
            (COPs -> COPs -> COPs)
-> ObjectPropertyExpression
-> COPs
-> Graph ObjectPropertyExpression
-> Graph ObjectPropertyExpression
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (COPs -> COPs -> COPs
forall a. Ord a => Set a -> Set a -> Set a
Set.union) (ObjectPropertyExpression -> ObjectPropertyExpression
inverseOf ObjectPropertyExpression
k) ([ObjectPropertyExpression] -> COPs
forall a. Ord a => [a] -> Set a
Set.fromList (ObjectPropertyExpression -> ObjectPropertyExpression
inverseOf (ObjectPropertyExpression -> ObjectPropertyExpression)
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ObjectPropertyExpression]
v)) Graph ObjectPropertyExpression
m
        -- also add hierachy for inverse

objectPropertyOrder :: [(PropertyExpressionChain, ObjectPropertyExpression)] -> Graph ObjectProperty
objectPropertyOrder :: [([ObjectPropertyExpression], ObjectPropertyExpression)]
-> Graph Datatype
objectPropertyOrder = (Graph Datatype
 -> ([ObjectPropertyExpression], ObjectPropertyExpression)
 -> Graph Datatype)
-> Graph Datatype
-> [([ObjectPropertyExpression], ObjectPropertyExpression)]
-> Graph Datatype
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((\g :: Graph Datatype
g c :: ([ObjectPropertyExpression], ObjectPropertyExpression)
c -> case ([ObjectPropertyExpression], ObjectPropertyExpression)
c of
    (_,ope :: ObjectPropertyExpression
ope) | ObjectPropertyExpression
ope ObjectPropertyExpression -> ObjectPropertyExpression -> Bool
forall a. Eq a => a -> a -> Bool
== Datatype -> ObjectPropertyExpression
ObjectProp Datatype
topObjectProperty -> Graph Datatype
g
    ((ope1 :: ObjectPropertyExpression
ope1 : ope2 :: ObjectPropertyExpression
ope2 : _), ope :: ObjectPropertyExpression
ope) | ObjectPropertyExpression
ope1 ObjectPropertyExpression -> ObjectPropertyExpression -> Bool
forall a. Eq a => a -> a -> Bool
== ObjectPropertyExpression
ope2 Bool -> Bool -> Bool
&& ObjectPropertyExpression
ope2 ObjectPropertyExpression -> ObjectPropertyExpression -> Bool
forall a. Eq a => a -> a -> Bool
== ObjectPropertyExpression
ope -> Graph Datatype
g

    (ch :: [ObjectPropertyExpression]
ch@(_:_:_), ope :: ObjectPropertyExpression
ope) -> (Graph Datatype -> ObjectPropertyExpression -> Graph Datatype)
-> Graph Datatype -> [ObjectPropertyExpression] -> Graph Datatype
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\g' :: Graph Datatype
g' o :: ObjectPropertyExpression
o -> Datatype -> Datatype -> Graph Datatype -> Graph Datatype
forall a. Ord a => a -> a -> Graph a -> Graph a
addEdge (ObjectPropertyExpression -> Datatype
objPropToIRI ObjectPropertyExpression
ope) (ObjectPropertyExpression -> Datatype
objPropToIRI ObjectPropertyExpression
o) Graph Datatype
g') Graph Datatype
g ([ObjectPropertyExpression] -> Graph Datatype)
-> [ObjectPropertyExpression] -> Graph Datatype
forall a b. (a -> b) -> a -> b
$
        if [ObjectPropertyExpression] -> ObjectPropertyExpression
forall a. [a] -> a
head [ObjectPropertyExpression]
ch ObjectPropertyExpression -> ObjectPropertyExpression -> Bool
forall a. Eq a => a -> a -> Bool
== ObjectPropertyExpression
ope then [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. [a] -> [a]
tail [ObjectPropertyExpression]
ch
        else if [ObjectPropertyExpression] -> ObjectPropertyExpression
forall a. [a] -> a
last [ObjectPropertyExpression]
ch ObjectPropertyExpression -> ObjectPropertyExpression -> Bool
forall a. Eq a => a -> a -> Bool
== ObjectPropertyExpression
ope then [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. [a] -> [a]
init [ObjectPropertyExpression]
ch
        else [ObjectPropertyExpression]
ch
    _ -> Graph Datatype
g
    )) Graph Datatype
forall k a. Map k a
Map.empty

-- | All object properties in a set of axioms that are not simple
complexObjectProperties :: [Axiom] -> Set.Set ObjectPropertyExpression
complexObjectProperties :: [Axiom] -> COPs
complexObjectProperties axs :: [Axiom]
axs = (Axiom -> COPs -> COPs) -> COPs -> [Axiom] -> COPs
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Axiom -> COPs -> COPs
cop COPs
forall a. Set a
Set.empty [Axiom]
axs where
    compOPE :: COPs
compOPE = [Axiom] -> COPs
compositeObjectProperties [Axiom]
axs
    h :: Graph ObjectPropertyExpression
h = Graph ObjectPropertyExpression -> Graph ObjectPropertyExpression
forall a. Ord a => Graph a -> Graph a
inverse (Graph ObjectPropertyExpression -> Graph ObjectPropertyExpression)
-> Graph ObjectPropertyExpression -> Graph ObjectPropertyExpression
forall a b. (a -> b) -> a -> b
$ [Axiom] -> Graph ObjectPropertyExpression
objectPropertyHierachy [Axiom]
axs
    -- cop :: Axiom -> Set.Set ObjectProperty -> Set.Set.ObjectProperty
    cop :: Axiom -> COPs -> COPs
cop (ObjectPropertyAxiom (SubObjectPropertyOf _ sub :: SubObjectPropertyExpression
sub super :: ObjectPropertyExpression
super)) = case SubObjectPropertyExpression
sub of
        SubObjPropExpr_obj o :: ObjectPropertyExpression
o -- @o -> super@ holds
            | ObjectPropertyExpression -> Bool
isComposite ObjectPropertyExpression
o -> ObjectPropertyExpression -> COPs -> COPs
forall a. Ord a => a -> Set a -> Set a
Set.insert ObjectPropertyExpression
super -- If any sub property is composite
        SubObjPropExpr_exprchain ch :: [ObjectPropertyExpression]
ch  -- @super ->* super@ holds, super is composite
            | [ObjectPropertyExpression] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ObjectPropertyExpression]
ch Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 -> ObjectPropertyExpression -> COPs -> COPs
forall a. Ord a => a -> Set a -> Set a
Set.insert ObjectPropertyExpression
super
        _ -> COPs -> COPs
forall a. a -> a
id
    cop (ObjectPropertyAxiom (TransitiveObjectProperty _ o :: ObjectPropertyExpression
o))
        | ObjectPropertyExpression -> Bool
isComposite ObjectPropertyExpression
o = ObjectPropertyExpression -> COPs -> COPs
forall a. Ord a => a -> Set a -> Set a
Set.insert ObjectPropertyExpression
o
    cop _ = COPs -> COPs
forall a. a -> a
id

    -- Checks if object property expression has any composite object property
    -- expression in their hierachy
    isComposite :: ObjectPropertyExpression -> Bool
isComposite ope :: ObjectPropertyExpression
ope = (ObjectPropertyExpression -> Bool) -> COPs -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (ObjectPropertyExpression -> COPs -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` COPs
compOPE) (COPs -> Bool) -> COPs -> Bool
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression -> COPs -> COPs
forall a. Ord a => a -> Set a -> Set a
Set.insert ObjectPropertyExpression
ope (COPs -> COPs) -> COPs -> COPs
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression -> Graph ObjectPropertyExpression -> COPs
forall a. Ord a => a -> Graph a -> Set a
reachable ObjectPropertyExpression
ope Graph ObjectPropertyExpression
h


slODoc :: OntologyDocument -> OWLSub
slODoc :: OntologyDocument -> OWLSub
slODoc odoc :: OntologyDocument
odoc =
    let axs :: [Axiom]
axs = Ontology -> [Axiom]
axioms (Ontology -> [Axiom])
-> (OntologyDocument -> Ontology) -> OntologyDocument -> [Axiom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OntologyDocument -> Ontology
ontology (OntologyDocument -> [Axiom]) -> OntologyDocument -> [Axiom]
forall a b. (a -> b) -> a -> b
$ OntologyDocument
odoc
        cops :: COPs
cops = [Axiom] -> COPs
complexObjectProperties [Axiom]
axs
    in OWLSub -> OWLSub -> OWLSub
slMax ([Axiom] -> OWLSub
slGeneralRestrictions [Axiom]
axs) ((OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> ([Axiom] -> [OWLSub]) -> [Axiom] -> OWLSub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Axiom -> OWLSub) -> [Axiom] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map (COPs -> Axiom -> OWLSub
slAxiom COPs
cops) ([Axiom] -> OWLSub) -> [Axiom] -> OWLSub
forall a b. (a -> b) -> a -> b
$ [Axiom]
axs)

slSig :: Sign -> OWLSub
slSig :: Sign -> OWLSub
slSig sig :: Sign
sig = let dts :: [Datatype]
dts = Set Datatype -> [Datatype]
forall a. Set a -> [a]
Set.toList (Set Datatype -> [Datatype]) -> Set Datatype -> [Datatype]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Datatype
datatypes Sign
sig in
    if Set Datatype -> Int
forall a. Set a -> Int
Set.size (Sign -> Set Datatype
dataProperties Sign
sig) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 Bool -> Bool -> Bool
&& [Datatype] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Datatype]
dts
    then OWLSub
slBottom else (OWLSub -> OWLSub -> OWLSub) -> OWLSub -> [OWLSub] -> OWLSub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OWLSub -> OWLSub -> OWLSub
slMax OWLSub
slBottom ([OWLSub] -> OWLSub) -> [OWLSub] -> OWLSub
forall a b. (a -> b) -> a -> b
$ (Datatype -> OWLSub) -> [Datatype] -> [OWLSub]
forall a b. (a -> b) -> [a] -> [b]
map Datatype -> OWLSub
slDatatype [Datatype]
dts

slMor :: OWLMorphism -> OWLSub
slMor :: OWLMorphism -> OWLSub
slMor mor :: OWLMorphism
mor = OWLSub -> OWLSub -> OWLSub
slMax (Sign -> OWLSub
slSig (Sign -> OWLSub) -> Sign -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
osource OWLMorphism
mor) (OWLSub -> OWLSub) -> OWLSub -> OWLSub
forall a b. (a -> b) -> a -> b
$ Sign -> OWLSub
slSig (Sign -> OWLSub) -> Sign -> OWLSub
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
otarget OWLMorphism
mor

-- projections along sublogics
prMor :: OWLSub -> OWLMorphism -> OWLMorphism
prMor :: OWLSub -> OWLMorphism -> OWLMorphism
prMor s :: OWLSub
s a :: OWLMorphism
a = OWLMorphism
a
    { osource :: Sign
osource = OWLSub -> Sign -> Sign
prSig OWLSub
s (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
osource OWLMorphism
a
    , otarget :: Sign
otarget = OWLSub -> Sign -> Sign
prSig OWLSub
s (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ OWLMorphism -> Sign
otarget OWLMorphism
a }

prSig :: OWLSub -> Sign -> Sign
prSig :: OWLSub -> Sign -> Sign
prSig s :: OWLSub
s a :: Sign
a = if OWLSub -> Set Datatype
datatype OWLSub
s Set Datatype -> Set Datatype -> Bool
forall a. Eq a => a -> a -> Bool
== Set Datatype
forall a. Set a
Set.empty
    then Sign
a {datatypes :: Set Datatype
datatypes = Set Datatype
forall a. Set a
Set.empty, dataProperties :: Set Datatype
dataProperties = Set Datatype
forall a. Set a
Set.empty}
    else Sign
a

prODoc :: OWLSub -> OntologyDocument -> OntologyDocument
prODoc :: OWLSub -> OntologyDocument -> OntologyDocument
prODoc s :: OWLSub
s a :: OntologyDocument
a =
    let cops :: COPs
cops = [Axiom] -> COPs
compositeObjectProperties ([Axiom] -> COPs)
-> (OntologyDocument -> [Axiom]) -> OntologyDocument -> COPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ontology -> [Axiom]
axioms (Ontology -> [Axiom])
-> (OntologyDocument -> Ontology) -> OntologyDocument -> [Axiom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OntologyDocument -> Ontology
ontology (OntologyDocument -> COPs) -> OntologyDocument -> COPs
forall a b. (a -> b) -> a -> b
$ OntologyDocument
a
        o :: Ontology
o = (OntologyDocument -> Ontology
ontology OntologyDocument
a) {axioms :: [Axiom]
axioms = (Axiom -> Bool) -> [Axiom] -> [Axiom]
forall a. (a -> Bool) -> [a] -> [a]
filter ((OWLSub
s OWLSub -> OWLSub -> Bool
forall a. Ord a => a -> a -> Bool
>=) (OWLSub -> Bool) -> (Axiom -> OWLSub) -> Axiom -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. COPs -> Axiom -> OWLSub
slAxiom COPs
cops) ([Axiom] -> [Axiom]) -> [Axiom] -> [Axiom]
forall a b. (a -> b) -> a -> b
$ Ontology -> [Axiom]
axioms (Ontology -> [Axiom]) -> Ontology -> [Axiom]
forall a b. (a -> b) -> a -> b
$
            OntologyDocument -> Ontology
ontology OntologyDocument
a }
    in OntologyDocument
a {ontology :: Ontology
ontology = Ontology
o}