content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./OWL2/Profiles.hs
  Copyright   :  (c) Felix Gabriel Mance
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  f.mance@jacobs-university.de
  Stability   :  provisional
  Portability :  portable
  
  OWL2 Profiles (EL, QL and RL)
  
  References  :  <http://www.w3.org/TR/owl2-profiles/>
  -}
  
  module OWL2.Profiles
      ( Profiles(..)
      , bottomProfile
      , topProfile
      , allProfiles
  
      , profileMax
      , printProfile
  
      , axiom
      , ontologyProfiles
      ) where
  
  import OWL2.AS
  
  import Data.Data
  import qualified Data.Set as Set
  
  import Common.IRI(setPrefix, mkIRI)
  
  data Profiles = Profiles
      { outsideEL :: Bool
      , outsideQL :: Bool
      , outsideRL :: Bool
      } deriving (Show, Eq, Ord, Typeable, Data)
  
  allProfiles :: [[Profiles]]
  allProfiles = [[bottomProfile]
              , [elProfile, qlProfile, rlProfile]
              , [elqlProfile, elrlProfile, qlrlProfile]
              , [topProfile]]
  
  bottomProfile :: Profiles
  bottomProfile = Profiles False False False
  
  topProfile :: Profiles
  topProfile = Profiles True True True
  
  elProfile :: Profiles
  elProfile = Profiles False True True
  
  qlProfile :: Profiles
  qlProfile = Profiles True False True
  
  rlProfile :: Profiles
  rlProfile = Profiles True True False
  
  elqlProfile :: Profiles
  elqlProfile = Profiles False False True
  
  elrlProfile :: Profiles
  elrlProfile = Profiles False True False
  
  qlrlProfile :: Profiles
  qlrlProfile = Profiles True False False
  
  printProfile :: Profiles -> String
  printProfile p@(Profiles e q r) = case p of
      (Profiles True True True) -> "NP"
      _ -> (if not e then "EL" else "")
              ++ (if not q then "QL" else "")
              ++ (if not r then "RL" else "")
  
  profileMax :: [Profiles] -> Profiles
  profileMax pl = Profiles
      { outsideEL = any outsideEL pl
      , outsideQL = any outsideQL pl
      , outsideRL = any outsideRL pl }
  
  profileMaxWith :: (a -> Profiles) -> [a] -> Profiles
  profileMaxWith f cel = profileMax (map f cel)
  
  maximalCovering :: Profiles -> [Profiles] -> Profiles
  maximalCovering c pl = profileMax [c, profileMax pl]
  
  
  owlELQLForbiddenDatatypes :: Set.Set Datatype
  owlELQLForbiddenDatatypes = Set.fromList . map (setPrefix "xsd" . mkIRI) $
   [ "double", "float", "nonPositiveInteger", "positiveInteger"
   , "negativeInteger", "long", "int", "short", "byte", "unsignedLong"
   , "unsignedInt", "unsignedShort", "unsignedByte", "language", "boolean"]
  
  datatype :: Datatype -> Profiles
  datatype dt = if dt `Set.member` owlELQLForbiddenDatatypes then rlProfile else bottomProfile 
  
  literal :: Literal -> Profiles
  literal l = case l of
      Literal _ (Typed dt) -> datatype dt
      NumberLit f -> datatype . setPrefix "xsd" . mkIRI . numberName $ f
      _ -> bottomProfile
  
  individual :: Individual -> Profiles
  individual i = if isAnonymous i then rlProfile else bottomProfile
  
  objProp :: ObjectPropertyExpression -> Profiles
  objProp ope = case ope of
      ObjectInverseOf _ -> qlrlProfile
      _ -> bottomProfile
  
  -- TODO: verify
  dataRange :: DataRange -> Profiles
  dataRange dr = case dr of
      DataType dt cfl ->
          if null cfl then datatype dt
           else topProfile
      DataJunction IntersectionOf drl -> profileMax $ map dataRange drl
      DataOneOf ll -> topProfile {
                          outsideEL = length ll /= 1 || outsideEL (profileMaxWith literal ll)
                      }
      _ -> topProfile
  
  subClass :: ClassExpression -> Profiles
  subClass cex = case cex of
      Expression c -> if isThing c then elqlProfile else bottomProfile
      ObjectJunction jt cel -> maximalCovering (case jt of
          IntersectionOf -> elrlProfile
          UnionOf -> rlProfile) $ map subClass cel
      ObjectOneOf il -> bottomProfile {
                      outsideEL = length il /= 1 || outsideEL (profileMaxWith individual il),
                      outsideRL = outsideRL $ profileMaxWith individual il
                  }
      ObjectValuesFrom SomeValuesFrom ope ce -> profileMax [objProp ope,
          case ce of
              Expression c -> if isThing c then bottomProfile
                               else elrlProfile
              _ -> maximalCovering elrlProfile [subClass ce]]
      ObjectHasValue ope i -> maximalCovering elrlProfile
         [objProp ope, individual i]
      ObjectHasSelf ope -> maximalCovering elProfile [objProp ope]
      DataValuesFrom SomeValuesFrom _ dr -> dataRange dr
      DataHasValue _ l -> literal l
      _ -> bottomProfile
  
  superClass :: ClassExpression -> Profiles
  superClass cex = case cex of
      Expression c -> if isThing c then elqlProfile else bottomProfile
      ObjectJunction IntersectionOf cel -> profileMaxWith superClass cel
      ObjectComplementOf ce -> maximalCovering qlrlProfile [subClass ce]
      ObjectOneOf il -> bottomProfile {
                      outsideEL = length il /= 1 || outsideEL (profileMaxWith individual il),
                      outsideRL = outsideRL $ profileMaxWith individual il
                  }
      ObjectValuesFrom qt ope ce -> case qt of
          SomeValuesFrom -> profileMax [objProp ope, case ce of
              Expression _ -> elqlProfile
              _ -> elProfile]
          AllValuesFrom -> profileMax [superClass ce, rlProfile]
      ObjectHasValue ope i -> profileMax [elrlProfile, objProp ope,
          individual i]
      ObjectHasSelf ope -> profileMax [elProfile, objProp ope]
      ObjectCardinality (Cardinality MaxCardinality i _ mce) ->
          if elem i [0, 1] then profileMax [rlProfile, case mce of
              Nothing -> bottomProfile
              Just ce -> case ce of
                  Expression _ -> bottomProfile
                  _ -> subClass ce]
           else bottomProfile
      DataValuesFrom qt _ dr -> profileMax [dataRange dr, case qt of
          SomeValuesFrom -> elqlProfile
          AllValuesFrom -> rlProfile]
      DataHasValue _ l -> profileMax [elrlProfile, literal l]
      DataCardinality (Cardinality MaxCardinality i _ mdr) ->
          if elem i [0, 1] then profileMax [rlProfile, case mdr of
              Nothing -> topProfile
              Just dr -> dataRange dr]
           else bottomProfile
      _ -> bottomProfile
  
  equivClassRL :: ClassExpression -> Bool
  equivClassRL cex = case cex of
      Expression c -> (not . isThing) c
      ObjectJunction IntersectionOf cel -> any equivClassRL cel
      ObjectHasValue _ i -> outsideRL $ individual i
      DataHasValue _ l -> outsideRL $ literal l
      _ -> False
  
  annotation :: Annotation -> Profiles
  annotation (Annotation as _ av) = profileMax [annotations as, case av of
      AnnValLit l -> literal l
      _ -> topProfile]
  
  annotations :: [Annotation] -> Profiles
  annotations = profileMax . map annotation
  
  classAxiomClassExpressions :: [Annotation] -> [ClassExpression] -> Profiles
  classAxiomClassExpressions anns clExprs = profileMax [annotations anns, bottomProfile {
                  outsideEL = outsideEL $ profileMaxWith subClass $ clExprs,
                  outsideQL = outsideQL $ profileMaxWith subClass $ clExprs,
                  outsideRL = any equivClassRL $ clExprs
              }]
  
  axiom :: Axiom -> Profiles
  axiom ax = case ax of
      Declaration _ _ -> bottomProfile
      ClassAxiom cax -> case cax of
          SubClassOf anns sub sup -> profileMax [annotations anns, subClass sub, superClass sup]
          EquivalentClasses anns cExprs -> classAxiomClassExpressions anns cExprs
          DisjointClasses anns cExprs -> classAxiomClassExpressions anns cExprs
          DisjointUnion anns c cExprs -> classAxiomClassExpressions anns (Expression c : cExprs)
      ObjectPropertyAxiom opax -> case opax of
          SubObjectPropertyOf anns subOpExpr supOpExpr -> case subOpExpr of
              SubObjPropExpr_obj oExpr ->
                  profileMax [annotations anns, profileMax $ map objProp [oExpr, supOpExpr]]
              SubObjPropExpr_exprchain oExprs -> 
                  maximalCovering elrlProfile [annotations anns, profileMax $ map objProp (supOpExpr : oExprs)]
          EquivalentObjectProperties anns oExprs -> maximalCovering (annotations anns) $ map objProp oExprs
          DisjointObjectProperties anns oExprs -> maximalCovering qlrlProfile $ (annotations anns) : map objProp oExprs
          InverseObjectProperties anns o1 o2 -> maximalCovering qlrlProfile $ (annotations anns) : map objProp [o1, o2]
          ObjectPropertyDomain anns oe ce -> profileMax [annotations anns, objProp oe, superClass ce] 
          ObjectPropertyRange anns oe ce -> profileMax [annotations anns, objProp oe, superClass ce] -- previously no check on ce was deon
          FunctionalObjectProperty _ oe -> maximalCovering rlProfile [objProp oe]
          InverseFunctionalObjectProperty _ oe -> maximalCovering rlProfile [objProp oe]
          ReflexiveObjectProperty _ oe -> maximalCovering elqlProfile [objProp oe]
          IrreflexiveObjectProperty _ oe -> maximalCovering qlrlProfile [objProp oe]
          SymmetricObjectProperty _ oe -> maximalCovering qlrlProfile [objProp oe]
          AsymmetricObjectProperty _ oe -> maximalCovering qlrlProfile [objProp oe]
          TransitiveObjectProperty _ oe -> maximalCovering elrlProfile [objProp oe]
      DataPropertyAxiom a -> case a of
          SubDataPropertyOf anns _ _ -> annotations anns
          EquivalentDataProperties anns _ -> annotations anns
          DisjointDataProperties anns _ -> maximalCovering qlrlProfile [annotations anns]
          DataPropertyDomain anns _ classExpr -> profileMax [annotations anns, superClass classExpr]
          DataPropertyRange anns _ dr -> profileMax [annotations anns, dataRange dr]
          FunctionalDataProperty anns _ -> maximalCovering elrlProfile [annotations anns]
      DatatypeDefinition anns dt dr -> profileMax [annotations anns, datatype dt, dataRange dr]
      HasKey anns classExpr oExprs _ -> maximalCovering elrlProfile
          [annotations anns, subClass classExpr, profileMax $ map objProp oExprs]
      Assertion a -> case a of
          SameIndividual anns inds -> maximalCovering elrlProfile
              [annotations anns, profileMax $ map individual inds]
          DifferentIndividuals anns inds -> maximalCovering elrlProfile
              [annotations anns, profileMax $ map individual inds]
          ClassAssertion anns ce ind -> profileMax [annotations anns, subClass ce, individual ind] 
          ObjectPropertyAssertion anns oExpr i1 i2 -> profileMax $
              [annotations anns, objProp oExpr] ++ map individual [i1, i2]
          NegativeObjectPropertyAssertion anns oExpr i1 i2 -> maximalCovering elrlProfile $
              [annotations anns, objProp oExpr] ++ map individual [i1, i2]
          DataPropertyAssertion anns _ ind lit -> profileMax $
              [annotations anns, individual ind, literal lit]
          NegativeDataPropertyAssertion anns _ ind lit -> maximalCovering elrlProfile $
              [annotations anns, individual ind, literal lit]
      AnnotationAxiom a -> case a of
          AnnotationAssertion anns prop _ val -> annotation $ Annotation anns prop val
          SubAnnotationPropertyOf anns _ _ -> annotations anns
          AnnotationPropertyDomain anns _ _ -> annotations anns
          AnnotationPropertyRange anns _ _ -> annotations anns
      Rule _ -> topProfile
      DGAxiom _ _ _ _ _ -> topProfile
  
  ontologyP :: Ontology -> Profiles
  ontologyP ont =
      let anns = ontologyAnnotation ont
          ax = axioms ont
      in profileMax [profileMaxWith axiom ax, profileMaxWith annotation anns]
  
  ontologyProfiles :: OntologyDocument -> Profiles
  ontologyProfiles odoc = ontologyP $ ontology odoc
  