{- |
Module      :  ./OWL2/StaticAnalysis.hs
Copyright   :  Felix Gabriel Mance
License     :  GPLv2 or higher, see LICENSE.txt

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

Static analysis for OWL 2
-}

module OWL2.StaticAnalysis where

import OWL2.Sign
import OWL2.Morphism
import qualified OWL2.AS as AS
import OWL2.MS
import OWL2.Print ()
import OWL2.Theorem
import OWL2.Function
import OWL2.Symbols

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List

import Common.AS_Annotation hiding (Annotation)
import Common.DocUtils
import Common.Result
import Common.GlobalAnnotations as GA
import Common.ExtSign
import Common.Lib.State
import Common.IRI --(iriToStringUnsecure, setAngles)
import Common.SetColimit

import Control.Monad
import qualified Control.Monad.Fail as Fail

import Logic.Logic

-- | Error messages for static analysis
failMsg :: AS.Entity -> AS.ClassExpression -> Result a
failMsg :: Entity -> ClassExpression -> Result a
failMsg (AS.Entity _ ty :: EntityType
ty e :: IRI
e) desc :: ClassExpression
desc =
  String -> Range -> Result a
forall a. String -> Range -> Result a
fatal_error
    ("undeclared `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ EntityType -> String
AS.showEntityType EntityType
ty
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String
showIRI IRI
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ "` in the following ClassExpression:\n"
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ ClassExpression -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ClassExpression
desc "") (Range -> Result a) -> Range -> Result a
forall a b. (a -> b) -> a -> b
$ IRI -> Range
iriPos IRI
e

-- | checks if an entity is in the signature
checkEntity :: Sign -> AS.Entity -> Result ()
checkEntity :: Sign -> Entity -> Result ()
checkEntity s :: Sign
s t :: Entity
t@(AS.Entity _ ty :: EntityType
ty e :: IRI
e) =
  let errMsg :: Result b
errMsg = String -> IRI -> Result b
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("unknown " String -> String -> String
forall a. [a] -> [a] -> [a]
++ EntityType -> String
AS.showEntityType EntityType
ty) IRI
e
  in case EntityType
ty of
   AS.Datatype -> Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
e (Sign -> Set IRI
datatypes Sign
s) Bool -> Bool -> Bool
|| IRI -> Bool
AS.isDatatypeKey IRI
e) Result ()
forall b. Result b
errMsg
   AS.Class -> Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
e (Sign -> Set IRI
concepts Sign
s) Bool -> Bool -> Bool
|| IRI -> Bool
AS.isThing IRI
e) Result ()
forall b. Result b
errMsg
   AS.ObjectProperty -> Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sign -> ObjectPropertyExpression -> Bool
isDeclObjProp Sign
s (ObjectPropertyExpression -> Bool)
-> ObjectPropertyExpression -> Bool
forall a b. (a -> b) -> a -> b
$ IRI -> ObjectPropertyExpression
AS.ObjectProp IRI
e) Result ()
forall b. Result b
errMsg
   AS.DataProperty -> Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sign -> IRI -> Bool
isDeclDataProp Sign
s IRI
e) Result ()
forall b. Result b
errMsg
   AS.AnnotationProperty -> Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
e (Sign -> Set IRI
annotationRoles Sign
s)
        Bool -> Bool -> Bool
|| IRI -> Bool
AS.isPredefAnnoProp IRI
e) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> String -> Result ()
forall a. a -> String -> Result a
justWarn () (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ Entity -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Entity
t " unknown"
   _ -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | takes an iri and finds out what entities it belongs to
correctEntity :: Sign -> IRI -> [AS.Entity]
correctEntity :: Sign -> IRI -> [Entity]
correctEntity s :: Sign
s iri :: IRI
iri =
    [EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.AnnotationProperty IRI
iri | IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
iri (Sign -> Set IRI
annotationRoles Sign
s)] [Entity] -> [Entity] -> [Entity]
forall a. [a] -> [a] -> [a]
++
    [EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.Class IRI
iri | IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
iri (Sign -> Set IRI
concepts Sign
s)] [Entity] -> [Entity] -> [Entity]
forall a. [a] -> [a] -> [a]
++
    [EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.ObjectProperty IRI
iri | IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
iri (Sign -> Set IRI
objectProperties Sign
s)] [Entity] -> [Entity] -> [Entity]
forall a. [a] -> [a] -> [a]
++
    [EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.DataProperty IRI
iri | IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
iri (Sign -> Set IRI
dataProperties Sign
s)] [Entity] -> [Entity] -> [Entity]
forall a. [a] -> [a] -> [a]
++
    [EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.Datatype IRI
iri | IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
iri (Sign -> Set IRI
datatypes Sign
s)] [Entity] -> [Entity] -> [Entity]
forall a. [a] -> [a] -> [a]
++
    [EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.NamedIndividual IRI
iri | IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
iri (Sign -> Set IRI
individuals Sign
s)]

checkLiteral :: Sign -> AS.Literal -> Result ()
checkLiteral :: Sign -> Literal -> Result ()
checkLiteral s :: Sign
s l :: Literal
l = case Literal
l of
    AS.Literal _ (AS.Typed dt :: IRI
dt) -> Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> Entity -> Result ()
forall a b. (a -> b) -> a -> b
$ EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.Datatype IRI
dt
    _ -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

isDeclInd :: Sign -> AS.Individual -> Bool
isDeclInd :: Sign -> IRI -> Bool
isDeclInd s :: Sign
s ind :: IRI
ind = IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
ind (Set IRI -> Bool) -> Set IRI -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
individuals Sign
s

isDeclObjProp :: Sign -> AS.ObjectPropertyExpression -> Bool
isDeclObjProp :: Sign -> ObjectPropertyExpression -> Bool
isDeclObjProp s :: Sign
s ope :: ObjectPropertyExpression
ope = let op :: IRI
op = ObjectPropertyExpression -> IRI
AS.objPropToIRI ObjectPropertyExpression
ope in
    IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
op (Sign -> Set IRI
objectProperties Sign
s) Bool -> Bool -> Bool
|| IRI -> Bool
AS.isPredefObjProp IRI
op

isDeclDataProp :: Sign -> AS.DataPropertyExpression -> Bool
isDeclDataProp :: Sign -> IRI -> Bool
isDeclDataProp s :: Sign
s dp :: IRI
dp = IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
dp (Sign -> Set IRI
dataProperties Sign
s) Bool -> Bool -> Bool
|| IRI -> Bool
AS.isPredefDataProp IRI
dp

{- | takes a list of object properties and discards the ones
    which are not in the signature -}
filterObjProp :: Sign -> [AS.ObjectPropertyExpression]
    -> [AS.ObjectPropertyExpression]
filterObjProp :: Sign -> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
filterObjProp = (ObjectPropertyExpression -> Bool)
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. (a -> Bool) -> [a] -> [a]
filter ((ObjectPropertyExpression -> Bool)
 -> [ObjectPropertyExpression] -> [ObjectPropertyExpression])
-> (Sign -> ObjectPropertyExpression -> Bool)
-> Sign
-> [ObjectPropertyExpression]
-> [ObjectPropertyExpression]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> ObjectPropertyExpression -> Bool
isDeclObjProp

checkHasKey :: Sign -> [AS.ObjectPropertyExpression] -> [AS.DataPropertyExpression]
    -> Result ([AS.ObjectPropertyExpression], [AS.DataPropertyExpression])
checkHasKey :: Sign
-> [ObjectPropertyExpression]
-> [IRI]
-> Result ([ObjectPropertyExpression], [IRI])
checkHasKey s :: Sign
s ol :: [ObjectPropertyExpression]
ol dl :: [IRI]
dl = do
    let (declaredObjProps :: [ObjectPropertyExpression]
declaredObjProps, undeclaredObjs :: [ObjectPropertyExpression]
undeclaredObjs) = (ObjectPropertyExpression -> Bool)
-> [ObjectPropertyExpression]
-> ([ObjectPropertyExpression], [ObjectPropertyExpression])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Sign -> ObjectPropertyExpression -> Bool
isDeclObjProp Sign
s) [ObjectPropertyExpression]
ol
    let (declaredDProps :: [IRI]
declaredDProps, undeclaredDProps :: [IRI]
undeclaredDProps) = (IRI -> Bool) -> [IRI] -> ([IRI], [IRI])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Sign -> IRI -> Bool
isDeclDataProp Sign
s) [IRI]
dl

    let newDProps :: [IRI]
newDProps = (ObjectPropertyExpression -> IRI)
-> [ObjectPropertyExpression] -> [IRI]
forall a b. (a -> b) -> [a] -> [b]
map (ObjectPropertyExpression -> IRI
AS.objPropToIRI) ([ObjectPropertyExpression] -> [IRI])
-> [ObjectPropertyExpression] -> [IRI]
forall a b. (a -> b) -> a -> b
$ (ObjectPropertyExpression -> Bool)
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. (a -> Bool) -> [a] -> [a]
filter ObjectPropertyExpression -> Bool
AS.isObjectProperty [ObjectPropertyExpression]
undeclaredObjs
    let newObjProps :: [ObjectPropertyExpression]
newObjProps = (IRI -> ObjectPropertyExpression)
-> [IRI] -> [ObjectPropertyExpression]
forall a b. (a -> b) -> [a] -> [b]
map (IRI -> ObjectPropertyExpression
AS.ObjectProp) [IRI]
undeclaredDProps

    Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression]
newObjProps
    Sign -> [IRI] -> Result ()
checkDataPropList Sign
s [IRI]
newDProps

    ([ObjectPropertyExpression], [IRI])
-> Result ([ObjectPropertyExpression], [IRI])
forall (m :: * -> *) a. Monad m => a -> m a
return ([ObjectPropertyExpression]
declaredObjProps [ObjectPropertyExpression]
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. [a] -> [a] -> [a]
++ [ObjectPropertyExpression]
newObjProps, [IRI]
declaredDProps [IRI] -> [IRI] -> [IRI]
forall a. [a] -> [a] -> [a]
++ [IRI]
newDProps)

    

checkObjPropList :: Sign -> [AS.ObjectPropertyExpression] -> Result ()
checkObjPropList :: Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList s :: Sign
s ol :: [ObjectPropertyExpression]
ol = do
    let ls :: [Bool]
ls = (ObjectPropertyExpression -> Bool)
-> [ObjectPropertyExpression] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> ObjectPropertyExpression -> Bool
isDeclObjProp Sign
s) [ObjectPropertyExpression]
ol
    Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
ls) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "undeclared object properties:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                      [ObjectPropertyExpression] -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ((ObjectPropertyExpression -> ObjectPropertyExpression)
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a b. (a -> b) -> [a] -> [b]
map (\o :: ObjectPropertyExpression
o -> case ObjectPropertyExpression
o of
                                     AS.ObjectProp _ -> ObjectPropertyExpression
o
                                     AS.ObjectInverseOf x :: ObjectPropertyExpression
x -> ObjectPropertyExpression
x) ((ObjectPropertyExpression -> Bool)
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (ObjectPropertyExpression -> Bool)
-> ObjectPropertyExpression
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> ObjectPropertyExpression -> Bool
isDeclObjProp Sign
s) [ObjectPropertyExpression]
ol)) ""

checkDataPropList :: Sign -> [AS.DataPropertyExpression] -> Result ()
checkDataPropList :: Sign -> [IRI] -> Result ()
checkDataPropList s :: Sign
s dl :: [IRI]
dl = do
    let ls :: [Bool]
ls = (IRI -> Bool) -> [IRI] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> IRI -> Bool
isDeclDataProp Sign
s) [IRI]
dl
    Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
ls) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "undeclared data properties:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [IRI] -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ((IRI -> Bool) -> [IRI] -> [IRI]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (IRI -> Bool) -> IRI -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> IRI -> Bool
isDeclDataProp Sign
s) [IRI]
dl) ""

-- | checks if a DataRange is valid
checkDataRange :: Sign -> AS.DataRange -> Result ()
checkDataRange :: Sign -> DataRange -> Result ()
checkDataRange s :: Sign
s dr :: DataRange
dr = case DataRange
dr of
    AS.DataType dt :: IRI
dt rl :: [(IRI, Literal)]
rl -> do
        Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> Entity -> Result ()
forall a b. (a -> b) -> a -> b
$ EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.Datatype IRI
dt
        ((IRI, Literal) -> Result ()) -> [(IRI, Literal)] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Sign -> Literal -> Result ()
checkLiteral Sign
s (Literal -> Result ())
-> ((IRI, Literal) -> Literal) -> (IRI, Literal) -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IRI, Literal) -> Literal
forall a b. (a, b) -> b
snd) [(IRI, Literal)]
rl
    AS.DataJunction _ drl :: [DataRange]
drl -> (DataRange -> Result ()) -> [DataRange] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Sign -> DataRange -> Result ()
checkDataRange Sign
s) [DataRange]
drl
    AS.DataComplementOf r :: DataRange
r -> Sign -> DataRange -> Result ()
checkDataRange Sign
s DataRange
r
    AS.DataOneOf ll :: [Literal]
ll -> (Literal -> Result ()) -> [Literal] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Sign -> Literal -> Result ()
checkLiteral Sign
s) [Literal]
ll

{- | converts ClassExpression to DataRanges because some
     DataProperties may be parsed as ObjectProperties -}
classExpressionToDataRange :: Sign -> AS.ClassExpression -> Result AS.DataRange
classExpressionToDataRange :: Sign -> ClassExpression -> Result DataRange
classExpressionToDataRange s :: Sign
s ce :: ClassExpression
ce = case ClassExpression
ce of
    AS.Expression u :: IRI
u -> Sign -> Entity -> Result ()
checkEntity Sign
s (EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.Datatype IRI
u)
        Result () -> Result DataRange -> Result DataRange
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DataRange -> Result DataRange
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI -> [(IRI, Literal)] -> DataRange
AS.DataType IRI
u [])
    AS.ObjectJunction jt :: JunctionType
jt cel :: [ClassExpression]
cel -> ([DataRange] -> DataRange)
-> Result [DataRange] -> Result DataRange
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (JunctionType -> [DataRange] -> DataRange
AS.DataJunction JunctionType
jt)
        (Result [DataRange] -> Result DataRange)
-> Result [DataRange] -> Result DataRange
forall a b. (a -> b) -> a -> b
$ (ClassExpression -> Result DataRange)
-> [ClassExpression] -> Result [DataRange]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> ClassExpression -> Result DataRange
classExpressionToDataRange Sign
s) [ClassExpression]
cel
    AS.ObjectComplementOf c :: ClassExpression
c -> (DataRange -> DataRange) -> Result DataRange -> Result DataRange
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataRange -> DataRange
AS.DataComplementOf
        (Result DataRange -> Result DataRange)
-> Result DataRange -> Result DataRange
forall a b. (a -> b) -> a -> b
$ Sign -> ClassExpression -> Result DataRange
classExpressionToDataRange Sign
s ClassExpression
c
    _ -> String -> Result DataRange
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result DataRange) -> String -> Result DataRange
forall a b. (a -> b) -> a -> b
$ "cannot convert ClassExpression to DataRange\n"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ ClassExpression -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ClassExpression
ce ""

{- | checks a ClassExpression and recursively converts the
     (maybe inappropriately) parsed syntax to a one satisfying the signature -}
checkClassExpression :: Sign -> AS.ClassExpression -> Result AS.ClassExpression
checkClassExpression :: Sign -> ClassExpression -> Result ClassExpression
checkClassExpression s :: Sign
s desc :: ClassExpression
desc =
    let errMsg :: Entity -> Result a
errMsg i :: Entity
i = Entity -> ClassExpression -> Result a
forall a. Entity -> ClassExpression -> Result a
failMsg Entity
i ClassExpression
desc
        objErr :: IRI -> Result a
objErr i :: IRI
i = Entity -> Result a
forall a. Entity -> Result a
errMsg (Entity -> Result a) -> Entity -> Result a
forall a b. (a -> b) -> a -> b
$ EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.ObjectProperty IRI
i
        datErr :: IRI -> Result a
datErr i :: IRI
i = Entity -> Result a
forall a. Entity -> Result a
errMsg (Entity -> Result a) -> Entity -> Result a
forall a b. (a -> b) -> a -> b
$ EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.DataProperty IRI
i
    in case ClassExpression
desc of
    AS.Expression u :: IRI
u -> if IRI -> Bool
AS.isThing IRI
u
        then ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassExpression -> Result ClassExpression)
-> ClassExpression -> Result ClassExpression
forall a b. (a -> b) -> a -> b
$ IRI -> ClassExpression
AS.Expression (IRI -> ClassExpression) -> IRI -> ClassExpression
forall a b. (a -> b) -> a -> b
$ IRI -> IRI
AS.setReservedPrefix IRI
u
        else Sign -> Entity -> Result ()
checkEntity Sign
s (EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.Class IRI
u) Result () -> Result ClassExpression -> Result ClassExpression
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return ClassExpression
desc
    AS.ObjectJunction ty :: JunctionType
ty ds :: [ClassExpression]
ds -> ([ClassExpression] -> ClassExpression)
-> Result [ClassExpression] -> Result ClassExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (JunctionType -> [ClassExpression] -> ClassExpression
AS.ObjectJunction JunctionType
ty)
        (Result [ClassExpression] -> Result ClassExpression)
-> Result [ClassExpression] -> Result ClassExpression
forall a b. (a -> b) -> a -> b
$ (ClassExpression -> Result ClassExpression)
-> [ClassExpression] -> Result [ClassExpression]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s) [ClassExpression]
ds
    AS.ObjectComplementOf d :: ClassExpression
d -> (ClassExpression -> ClassExpression)
-> Result ClassExpression -> Result ClassExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ClassExpression -> ClassExpression
AS.ObjectComplementOf (Result ClassExpression -> Result ClassExpression)
-> Result ClassExpression -> Result ClassExpression
forall a b. (a -> b) -> a -> b
$ Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s ClassExpression
d
    AS.ObjectOneOf _ -> ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return ClassExpression
desc
    AS.ObjectValuesFrom q :: QuantifierType
q opExpr :: ObjectPropertyExpression
opExpr d :: ClassExpression
d -> if Sign -> ObjectPropertyExpression -> Bool
isDeclObjProp Sign
s ObjectPropertyExpression
opExpr
        then (ClassExpression -> ClassExpression)
-> Result ClassExpression -> Result ClassExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QuantifierType
-> ObjectPropertyExpression -> ClassExpression -> ClassExpression
AS.ObjectValuesFrom QuantifierType
q ObjectPropertyExpression
opExpr) (Result ClassExpression -> Result ClassExpression)
-> Result ClassExpression -> Result ClassExpression
forall a b. (a -> b) -> a -> b
$ Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s ClassExpression
d
        else let iri :: IRI
iri = ObjectPropertyExpression -> IRI
AS.objPropToIRI ObjectPropertyExpression
opExpr
             in if Sign -> IRI -> Bool
isDeclDataProp Sign
s IRI
iri then
                    (DataRange -> ClassExpression)
-> Result DataRange -> Result ClassExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QuantifierType -> [IRI] -> DataRange -> ClassExpression
AS.DataValuesFrom QuantifierType
q [IRI
iri])
                      (Result DataRange -> Result ClassExpression)
-> Result DataRange -> Result ClassExpression
forall a b. (a -> b) -> a -> b
$ Sign -> ClassExpression -> Result DataRange
classExpressionToDataRange Sign
s ClassExpression
d
                else IRI -> Result ClassExpression
forall a. IRI -> Result a
objErr IRI
iri
    AS.ObjectHasSelf opExpr :: ObjectPropertyExpression
opExpr -> if Sign -> ObjectPropertyExpression -> Bool
isDeclObjProp Sign
s ObjectPropertyExpression
opExpr then ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return ClassExpression
desc
        else IRI -> Result ClassExpression
forall a. IRI -> Result a
objErr (IRI -> Result ClassExpression) -> IRI -> Result ClassExpression
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression -> IRI
AS.objPropToIRI ObjectPropertyExpression
opExpr
    AS.ObjectHasValue opExpr :: ObjectPropertyExpression
opExpr _ -> if Sign -> ObjectPropertyExpression -> Bool
isDeclObjProp Sign
s ObjectPropertyExpression
opExpr then ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return ClassExpression
desc
        else IRI -> Result ClassExpression
forall a. IRI -> Result a
objErr (IRI -> Result ClassExpression) -> IRI -> Result ClassExpression
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression -> IRI
AS.objPropToIRI ObjectPropertyExpression
opExpr
    AS.ObjectCardinality (AS.Cardinality a :: CardinalityType
a b :: Int
b opExpr :: ObjectPropertyExpression
opExpr md :: Maybe ClassExpression
md) -> do
        let iri :: IRI
iri = ObjectPropertyExpression -> IRI
AS.objPropToIRI ObjectPropertyExpression
opExpr
            mbrOP :: Bool
mbrOP = IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
iri (Set IRI -> Bool) -> Set IRI -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set IRI
objectProperties Sign
s
        case Maybe ClassExpression
md of
            Nothing
                | Bool
mbrOP -> ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return ClassExpression
desc
                | Sign -> IRI -> Bool
isDeclDataProp Sign
s IRI
iri ->
                        ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassExpression -> Result ClassExpression)
-> ClassExpression -> Result ClassExpression
forall a b. (a -> b) -> a -> b
$ Cardinality IRI DataRange -> ClassExpression
AS.DataCardinality (Cardinality IRI DataRange -> ClassExpression)
-> Cardinality IRI DataRange -> ClassExpression
forall a b. (a -> b) -> a -> b
$ CardinalityType
-> Int -> IRI -> Maybe DataRange -> Cardinality IRI DataRange
forall a b.
CardinalityType -> Int -> a -> Maybe b -> Cardinality a b
AS.Cardinality CardinalityType
a Int
b IRI
iri Maybe DataRange
forall a. Maybe a
Nothing
                | Bool
otherwise -> IRI -> Result ClassExpression
forall a. IRI -> Result a
objErr IRI
iri
            Just d :: ClassExpression
d ->
                if Bool
mbrOP then (ClassExpression -> ClassExpression)
-> Result ClassExpression -> Result ClassExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cardinality ObjectPropertyExpression ClassExpression
-> ClassExpression
AS.ObjectCardinality (Cardinality ObjectPropertyExpression ClassExpression
 -> ClassExpression)
-> (ClassExpression
    -> Cardinality ObjectPropertyExpression ClassExpression)
-> ClassExpression
-> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CardinalityType
-> Int
-> ObjectPropertyExpression
-> Maybe ClassExpression
-> Cardinality ObjectPropertyExpression ClassExpression
forall a b.
CardinalityType -> Int -> a -> Maybe b -> Cardinality a b
AS.Cardinality CardinalityType
a Int
b ObjectPropertyExpression
opExpr
                            (Maybe ClassExpression
 -> Cardinality ObjectPropertyExpression ClassExpression)
-> (ClassExpression -> Maybe ClassExpression)
-> ClassExpression
-> Cardinality ObjectPropertyExpression ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClassExpression -> Maybe ClassExpression
forall a. a -> Maybe a
Just) (Result ClassExpression -> Result ClassExpression)
-> Result ClassExpression -> Result ClassExpression
forall a b. (a -> b) -> a -> b
$ Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s ClassExpression
d
                else do
                    DataRange
dr <- Sign -> ClassExpression -> Result DataRange
classExpressionToDataRange Sign
s ClassExpression
d
                    if Sign -> IRI -> Bool
isDeclDataProp Sign
s IRI
iri then
                        ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassExpression -> Result ClassExpression)
-> ClassExpression -> Result ClassExpression
forall a b. (a -> b) -> a -> b
$ Cardinality IRI DataRange -> ClassExpression
AS.DataCardinality
                          (Cardinality IRI DataRange -> ClassExpression)
-> Cardinality IRI DataRange -> ClassExpression
forall a b. (a -> b) -> a -> b
$ CardinalityType
-> Int -> IRI -> Maybe DataRange -> Cardinality IRI DataRange
forall a b.
CardinalityType -> Int -> a -> Maybe b -> Cardinality a b
AS.Cardinality CardinalityType
a Int
b IRI
iri (Maybe DataRange -> Cardinality IRI DataRange)
-> Maybe DataRange -> Cardinality IRI DataRange
forall a b. (a -> b) -> a -> b
$ DataRange -> Maybe DataRange
forall a. a -> Maybe a
Just DataRange
dr
                        else IRI -> Result ClassExpression
forall a. IRI -> Result a
datErr IRI
iri
    AS.DataValuesFrom _ dExps :: [IRI]
dExps r :: DataRange
r -> Sign -> DataRange -> Result ()
checkDataRange Sign
s DataRange
r
        Result () -> Result ClassExpression -> Result ClassExpression
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> if (IRI -> Bool) -> [IRI] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Sign -> IRI -> Bool
isDeclDataProp Sign
s) [IRI]
dExps then ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return ClassExpression
desc else IRI -> Result ClassExpression
forall a. IRI -> Result a
datErr ([IRI] -> IRI
forall a. [a] -> a
head ([IRI] -> IRI) -> [IRI] -> IRI
forall a b. (a -> b) -> a -> b
$ (IRI -> Bool) -> [IRI] -> [IRI]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not(Bool -> Bool) -> (IRI -> Bool) -> IRI -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Sign -> IRI -> Bool
isDeclDataProp Sign
s) [IRI]
dExps)
    AS.DataHasValue dExp :: IRI
dExp l :: Literal
l -> do
        Sign -> Literal -> Result ()
checkLiteral Sign
s Literal
l
        if Sign -> IRI -> Bool
isDeclDataProp Sign
s IRI
dExp then ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return ClassExpression
desc
            else IRI -> Result ClassExpression
forall a. IRI -> Result a
datErr IRI
dExp
    AS.DataCardinality (AS.Cardinality _ _ dExp :: IRI
dExp mr :: Maybe DataRange
mr) -> if Sign -> IRI -> Bool
isDeclDataProp Sign
s IRI
dExp
        then case Maybe DataRange
mr of
            Nothing -> ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return ClassExpression
desc
            Just d :: DataRange
d -> Sign -> DataRange -> Result ()
checkDataRange Sign
s DataRange
d Result () -> Result ClassExpression -> Result ClassExpression
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ClassExpression -> Result ClassExpression
forall (m :: * -> *) a. Monad m => a -> m a
return ClassExpression
desc
        else IRI -> Result ClassExpression
forall a. IRI -> Result a
datErr IRI
dExp


checkAnnotation :: Sign -> AS.Annotation -> Result ()
checkAnnotation :: Sign -> Annotation -> Result ()
checkAnnotation s :: Sign
s (AS.Annotation ans :: [Annotation]
ans apr :: IRI
apr av :: AnnotationValue
av) = do
    Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
ans
    Sign -> Entity -> Result ()
checkEntity Sign
s (EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.AnnotationProperty IRI
apr)
    case AnnotationValue
av of
        AS.AnnValLit lit :: Literal
lit -> Sign -> Literal -> Result ()
checkLiteral Sign
s Literal
lit
        _ -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

checkAnnos :: Sign -> [AS.Annotation] -> Result ()
checkAnnos :: Sign -> [Annotation] -> Result ()
checkAnnos = (Annotation -> Result ()) -> [Annotation] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Annotation -> Result ()) -> [Annotation] -> Result ())
-> (Sign -> Annotation -> Result ())
-> Sign
-> [Annotation]
-> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Annotation -> Result ()
checkAnnotation

checkAssertion :: Sign -> IRI -> Annotations -> Result [Axiom]
checkAssertion :: Sign -> IRI -> [Annotation] -> Result [Axiom]
checkAssertion s :: Sign
s iri :: IRI
iri ans :: [Annotation]
ans = do
    let entList :: [Entity]
entList = Sign -> IRI -> [Entity]
correctEntity Sign
s IRI
iri
        ab :: FrameBit
ab = [Annotation] -> AnnFrameBit -> FrameBit
AnnFrameBit [Annotation]
ans (AnnFrameBit -> FrameBit) -> AnnFrameBit -> FrameBit
forall a b. (a -> b) -> a -> b
$ AnnoType -> AnnFrameBit
AnnotationFrameBit AnnoType
Assertion
    if [Entity] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Entity]
entList
        then let misc :: Extended
misc = [Annotation] -> Extended
Misc [[Annotation] -> IRI -> AnnotationValue -> Annotation
AS.Annotation [] IRI
iri (AnnotationValue -> Annotation) -> AnnotationValue -> Annotation
forall a b. (a -> b) -> a -> b
$ IRI -> AnnotationValue
AS.AnnValue IRI
iri]
             in [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Extended -> FrameBit -> Axiom
PlainAxiom Extended
misc FrameBit
ab] -- only for anonymous individuals
        else [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Axiom] -> Result [Axiom]) -> [Axiom] -> Result [Axiom]
forall a b. (a -> b) -> a -> b
$ (Entity -> Axiom) -> [Entity] -> [Axiom]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: Entity
x -> Extended -> FrameBit -> Axiom
PlainAxiom (Entity -> Extended
SimpleEntity Entity
x) FrameBit
ab) [Entity]
entList

extractDGVariables :: [AS.DGAtom] -> [AS.Variable]
extractDGVariables :: [DGAtom] -> [IRI]
extractDGVariables = 
    let eIArg :: IndividualArg -> [IRI]
eIArg a :: IndividualArg
a = case IndividualArg
a of
            AS.IVar v :: IRI
v -> [IRI
v]
            _ -> []
    in
    
    [[IRI]] -> [IRI]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[IRI]] -> [IRI]) -> ([DGAtom] -> [[IRI]]) -> [DGAtom] -> [IRI]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DGAtom -> [IRI]) -> [DGAtom] -> [[IRI]]
forall a b. (a -> b) -> [a] -> [b]
map (\atom :: DGAtom
atom -> case DGAtom
atom of
        AS.DGClassAtom _ a :: IndividualArg
a -> IndividualArg -> [IRI]
eIArg IndividualArg
a
        AS.DGObjectPropertyAtom _ a1 :: IndividualArg
a1 a2 :: IndividualArg
a2 -> IndividualArg -> [IRI]
eIArg IndividualArg
a1 [IRI] -> [IRI] -> [IRI]
forall a. [a] -> [a] -> [a]
++ IndividualArg -> [IRI]
eIArg IndividualArg
a2
    )

extractVariables :: [AS.Atom] -> [AS.Variable]
extractVariables :: [Atom] -> [IRI]
extractVariables = 
    let eIArg :: IndividualArg -> [IRI]
eIArg a :: IndividualArg
a = case IndividualArg
a of
            AS.IVar v :: IRI
v -> [IRI
v]
            _ -> []
        eDArg :: DataArg -> [IRI]
eDArg a :: DataArg
a = case DataArg
a of
            AS.DVar v :: IRI
v -> [IRI
v]
            _ -> []
        eUArg :: UnknownArg -> [IRI]
eUArg a :: UnknownArg
a = case UnknownArg
a of
            AS.IndividualArg ia :: IndividualArg
ia -> IndividualArg -> [IRI]
eIArg IndividualArg
ia
            AS.DataArg da :: DataArg
da -> DataArg -> [IRI]
eDArg DataArg
da
            AS.Variable v :: IRI
v -> [IRI
v]
    in
    
    [[IRI]] -> [IRI]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[IRI]] -> [IRI]) -> ([Atom] -> [[IRI]]) -> [Atom] -> [IRI]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Atom -> [IRI]) -> [Atom] -> [[IRI]]
forall a b. (a -> b) -> [a] -> [b]
map (\atom :: Atom
atom -> case Atom
atom of
        AS.ClassAtom _ a :: IndividualArg
a -> IndividualArg -> [IRI]
eIArg IndividualArg
a
        AS.DataRangeAtom _ a :: DataArg
a -> DataArg -> [IRI]
eDArg DataArg
a
        AS.ObjectPropertyAtom _ a1 :: IndividualArg
a1 a2 :: IndividualArg
a2 -> IndividualArg -> [IRI]
eIArg IndividualArg
a1 [IRI] -> [IRI] -> [IRI]
forall a. [a] -> [a] -> [a]
++ IndividualArg -> [IRI]
eIArg IndividualArg
a2
        AS.DataPropertyAtom _ a1 :: IndividualArg
a1 a2 :: DataArg
a2 -> IndividualArg -> [IRI]
eIArg IndividualArg
a1 [IRI] -> [IRI] -> [IRI]
forall a. [a] -> [a] -> [a]
++ DataArg -> [IRI]
eDArg DataArg
a2
        AS.BuiltInAtom _ args :: [DataArg]
args -> [[IRI]] -> [IRI]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[IRI]] -> [IRI]) -> [[IRI]] -> [IRI]
forall a b. (a -> b) -> a -> b
$ DataArg -> [IRI]
eDArg (DataArg -> [IRI]) -> [DataArg] -> [[IRI]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataArg]
args
        AS.SameIndividualAtom a1 :: IndividualArg
a1 a2 :: IndividualArg
a2 -> IndividualArg -> [IRI]
eIArg IndividualArg
a1 [IRI] -> [IRI] -> [IRI]
forall a. [a] -> [a] -> [a]
++ IndividualArg -> [IRI]
eIArg IndividualArg
a2
        AS.DifferentIndividualsAtom a1 :: IndividualArg
a1 a2 :: IndividualArg
a2 -> IndividualArg -> [IRI]
eIArg IndividualArg
a1 [IRI] -> [IRI] -> [IRI]
forall a. [a] -> [a] -> [a]
++ IndividualArg -> [IRI]
eIArg IndividualArg
a2
        AS.UnknownUnaryAtom _ a :: UnknownArg
a -> UnknownArg -> [IRI]
eUArg UnknownArg
a
        AS.UnknownBinaryAtom _ a1 :: UnknownArg
a1 a2 :: UnknownArg
a2 -> UnknownArg -> [IRI]
eUArg UnknownArg
a1 [IRI] -> [IRI] -> [IRI]
forall a. [a] -> [a] -> [a]
++ UnknownArg -> [IRI]
eUArg UnknownArg
a2
    )

checkIndividualArg :: Sign -> Maybe [AS.Variable] -> AS.IndividualArg -> Result ()
checkIndividualArg :: Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg s :: Sign
s mVars :: Maybe [IRI]
mVars a :: IndividualArg
a = case IndividualArg
a of
    AS.IArg i :: IRI
i -> Sign -> Entity -> Result ()
checkEntity Sign
s (EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.NamedIndividual IRI
i) Result () -> Result () -> Result ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    AS.IVar v :: IRI
v -> case Maybe [IRI]
mVars of
        Nothing -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just vars :: [IRI]
vars -> Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IRI
v IRI -> [IRI] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [IRI]
vars) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> IRI -> Result ()
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Unknown variable" IRI
v

checkDataArg :: Sign -> Maybe [AS.Variable] -> AS.DataArg -> Result ()
checkDataArg :: Sign -> Maybe [IRI] -> DataArg -> Result ()
checkDataArg s :: Sign
s mVars :: Maybe [IRI]
mVars a :: DataArg
a = case DataArg
a of
    AS.DArg l :: Literal
l -> Sign -> Literal -> Result ()
checkLiteral Sign
s Literal
l Result () -> Result () -> Result ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    AS.DVar v :: IRI
v -> case Maybe [IRI]
mVars of
        Nothing -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just vars :: [IRI]
vars -> Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IRI
v IRI -> [IRI] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [IRI]
vars) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> IRI -> Result ()
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Unknown variable" IRI
v

checkDGAtom :: Sign -> Maybe [AS.Variable] -> AS.DGAtom -> Result AS.DGAtom
checkDGAtom :: Sign -> Maybe [IRI] -> DGAtom -> Result DGAtom
checkDGAtom s :: Sign
s mVars :: Maybe [IRI]
mVars atom :: DGAtom
atom = case DGAtom
atom of
    AS.DGClassAtom c :: ClassExpression
c a :: IndividualArg
a -> do
        ClassExpression
nExpr <- Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s ClassExpression
c
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a
        DGAtom -> Result DGAtom
forall (m :: * -> *) a. Monad m => a -> m a
return (DGAtom -> Result DGAtom) -> DGAtom -> Result DGAtom
forall a b. (a -> b) -> a -> b
$ ClassExpression -> IndividualArg -> DGAtom
AS.DGClassAtom ClassExpression
nExpr IndividualArg
a
    AS.DGObjectPropertyAtom o :: ObjectPropertyExpression
o a1 :: IndividualArg
a1 a2 :: IndividualArg
a2 -> do
        Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
o]
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a1
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a2
        DGAtom -> Result DGAtom
forall (m :: * -> *) a. Monad m => a -> m a
return DGAtom
atom


checkDLAtom :: Sign -> Maybe [AS.Variable] -> AS.Atom -> Result AS.Atom
checkDLAtom :: Sign -> Maybe [IRI] -> Atom -> Result Atom
checkDLAtom s :: Sign
s mVars :: Maybe [IRI]
mVars atom :: Atom
atom = case Atom
atom of
    AS.ClassAtom e :: ClassExpression
e a :: IndividualArg
a -> do
        ClassExpression
newExpr <- Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s ClassExpression
e
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a
        Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ ClassExpression -> IndividualArg -> Atom
AS.ClassAtom ClassExpression
newExpr IndividualArg
a
    AS.DataRangeAtom r :: DataRange
r a :: DataArg
a -> do
        Sign -> DataRange -> Result ()
checkDataRange Sign
s DataRange
r
        Sign -> Maybe [IRI] -> DataArg -> Result ()
checkDataArg Sign
s Maybe [IRI]
mVars DataArg
a
        Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return Atom
atom
    AS.ObjectPropertyAtom o :: ObjectPropertyExpression
o a1 :: IndividualArg
a1 a2 :: IndividualArg
a2 -> do
        Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
o]
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a1
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a2
        Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return Atom
atom
    AS.DataPropertyAtom d :: IRI
d a1 :: IndividualArg
a1 a2 :: DataArg
a2 -> do
        Sign -> [IRI] -> Result ()
checkDataPropList Sign
s [IRI
d]
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a1
        Sign -> Maybe [IRI] -> DataArg -> Result ()
checkDataArg Sign
s Maybe [IRI]
mVars DataArg
a2
        Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return Atom
atom
    AS.BuiltInAtom _ args :: [DataArg]
args -> do
        (DataArg -> Result ()) -> [DataArg] -> Result [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> Maybe [IRI] -> DataArg -> Result ()
checkDataArg Sign
s Maybe [IRI]
mVars) [DataArg]
args
        Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return Atom
atom
    AS.SameIndividualAtom a1 :: IndividualArg
a1 a2 :: IndividualArg
a2 -> do
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a1
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a2
        Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return Atom
atom
    AS.DifferentIndividualsAtom a1 :: IndividualArg
a1 a2 :: IndividualArg
a2 -> do
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a1
        Sign -> Maybe [IRI] -> IndividualArg -> Result ()
checkIndividualArg Sign
s Maybe [IRI]
mVars IndividualArg
a2
        Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return Atom
atom
    AS.UnknownUnaryAtom i :: IRI
i a :: UnknownArg
a -> case UnknownArg
a of
        AS.Variable v :: IRI
v -> if IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
i (Sign -> Set IRI
concepts Sign
s)
            then Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ ClassExpression -> IndividualArg -> Atom
AS.ClassAtom (IRI -> ClassExpression
AS.Expression IRI
i) (IRI -> IndividualArg
AS.IVar IRI
v)
            else Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ IRI -> [DataArg] -> Atom
AS.BuiltInAtom IRI
i [IRI -> DataArg
AS.DVar IRI
v]
        _ -> String -> IRI -> Result Atom
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Unknown unary atom" IRI
i
    AS.UnknownBinaryAtom i :: IRI
i a1 :: UnknownArg
a1 a2 :: UnknownArg
a2 -> case UnknownArg
a1 of
        AS.Variable v :: IRI
v ->
            if IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
i (Sign -> Set IRI
objectProperties Sign
s) then case UnknownArg
a2 of
                AS.Variable v2 :: IRI
v2 -> Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression -> IndividualArg -> IndividualArg -> Atom
AS.ObjectPropertyAtom (IRI -> ObjectPropertyExpression
AS.ObjectProp IRI
i) (IRI -> IndividualArg
AS.IVar IRI
v) (IRI -> IndividualArg
AS.IVar IRI
v2)
                AS.IndividualArg a :: IndividualArg
a -> Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression -> IndividualArg -> IndividualArg -> Atom
AS.ObjectPropertyAtom (IRI -> ObjectPropertyExpression
AS.ObjectProp IRI
i) (IRI -> IndividualArg
AS.IVar IRI
v) IndividualArg
a
                _ -> String -> IRI -> Result Atom
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Unknown binary atom" IRI
i
            else if IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
i (Sign -> Set IRI
dataProperties Sign
s) then case UnknownArg
a2 of
                AS.Variable v2 :: IRI
v2 -> Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ IRI -> IndividualArg -> DataArg -> Atom
AS.DataPropertyAtom IRI
i (IRI -> IndividualArg
AS.IVar IRI
v) (IRI -> DataArg
AS.DVar IRI
v2)
                AS.DataArg a :: DataArg
a -> Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ IRI -> IndividualArg -> DataArg -> Atom
AS.DataPropertyAtom IRI
i (IRI -> IndividualArg
AS.IVar IRI
v) DataArg
a
                _ -> String -> IRI -> Result Atom
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Unknown binary atom" IRI
i
            else case UnknownArg
a2 of
                AS.Variable v' :: IRI
v' -> Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ IRI -> [DataArg] -> Atom
AS.BuiltInAtom IRI
i [IRI -> DataArg
AS.DVar IRI
v']
                AS.DataArg a :: DataArg
a -> Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ IRI -> [DataArg] -> Atom
AS.BuiltInAtom IRI
i [DataArg
a]
                _ -> String -> IRI -> Result Atom
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Unknown binary atom" IRI
i 
        AS.IndividualArg a :: IndividualArg
a@(AS.IArg _) -> case UnknownArg
a2 of
            AS.Variable v :: IRI
v ->
                if IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
i (Sign -> Set IRI
objectProperties Sign
s) then Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ ObjectPropertyExpression -> IndividualArg -> IndividualArg -> Atom
AS.ObjectPropertyAtom (IRI -> ObjectPropertyExpression
AS.ObjectProp IRI
i) IndividualArg
a (IRI -> IndividualArg
AS.IVar IRI
v)
                else if IRI -> Set IRI -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IRI
i (Sign -> Set IRI
dataProperties Sign
s) then Atom -> Result Atom
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> Result Atom) -> Atom -> Result Atom
forall a b. (a -> b) -> a -> b
$ IRI -> IndividualArg -> DataArg -> Atom
AS.DataPropertyAtom IRI
i IndividualArg
a (IRI -> DataArg
AS.DVar IRI
v)
                else String -> IRI -> Result Atom
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Unknown binary atom" IRI
i
            _ -> String -> IRI -> Result Atom
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Unknown binary atom" IRI
i
        _ -> String -> IRI -> Result Atom
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Unknown binary atom" IRI
i


checkDGEdgeAssertion :: Sign -> AS.DGEdgeAssertion -> Result ()
checkDGEdgeAssertion :: Sign -> DGEdgeAssertion -> Result ()
checkDGEdgeAssertion s :: Sign
s (AS.DGEdgeAssertion o :: IRI
o _ _) = do
    Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [IRI -> ObjectPropertyExpression
AS.ObjectProp IRI
o]
    () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | corrects the axiom according to the signature
checkAxiom :: Sign -> AS.Axiom -> Result [AS.Axiom]
checkAxiom :: Sign -> Axiom -> Result [Axiom]
checkAxiom s :: Sign
s a :: Axiom
a = case Axiom
a of
    (AS.Declaration anns :: [Annotation]
anns entity :: Entity
entity) -> do
        Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
        Sign -> Entity -> Result ()
checkEntity Sign
s Entity
entity
        [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

    AS.ClassAxiom clAxiom :: ClassAxiom
clAxiom -> case ClassAxiom
clAxiom of
        AS.SubClassOf anns :: [Annotation]
anns subClExpr :: ClassExpression
subClExpr supClExpr :: ClassExpression
supClExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            ClassExpression
nSubClExpr <- (Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s) ClassExpression
subClExpr
            ClassExpression
nSupClExpr <- (Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s) ClassExpression
supClExpr
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> ClassExpression -> ClassExpression -> ClassAxiom
AS.SubClassOf [Annotation]
anns ClassExpression
nSubClExpr ClassExpression
nSupClExpr]

        AS.EquivalentClasses anns :: [Annotation]
anns clExprs :: [ClassExpression]
clExprs -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            [ClassExpression]
nClExprs <- (ClassExpression -> Result ClassExpression)
-> [ClassExpression] -> Result [ClassExpression]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s) [ClassExpression]
clExprs
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [ClassExpression] -> ClassAxiom
AS.EquivalentClasses [Annotation]
anns [ClassExpression]
nClExprs]
            
        AS.DisjointClasses anns :: [Annotation]
anns clExprs :: [ClassExpression]
clExprs -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            [ClassExpression]
nClExprs <- (ClassExpression -> Result ClassExpression)
-> [ClassExpression] -> Result [ClassExpression]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s) [ClassExpression]
clExprs
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [ClassExpression] -> ClassAxiom
AS.DisjointClasses [Annotation]
anns [ClassExpression]
nClExprs]

        AS.DisjointUnion anns :: [Annotation]
anns clIRI :: IRI
clIRI clExprs :: [ClassExpression]
clExprs -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> Entity -> Result ()
checkEntity Sign
s (EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.Class IRI
clIRI)
            [ClassExpression]
nClExprs <- (ClassExpression -> Result ClassExpression)
-> [ClassExpression] -> Result [ClassExpression]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s) [ClassExpression]
clExprs
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> IRI -> [ClassExpression] -> ClassAxiom
AS.DisjointUnion [Annotation]
anns IRI
clIRI [ClassExpression]
nClExprs]

    AS.ObjectPropertyAxiom opAxiom :: ObjectPropertyAxiom
opAxiom -> case ObjectPropertyAxiom
opAxiom of
        AS.SubObjectPropertyOf anns :: [Annotation]
anns subOpExpr :: SubObjectPropertyExpression
subOpExpr supOpExpr :: ObjectPropertyExpression
supOpExpr -> do
            let subOpExpr2 :: [ObjectPropertyExpression]
subOpExpr2 = case SubObjectPropertyExpression
subOpExpr of
                    AS.SubObjPropExpr_obj o :: ObjectPropertyExpression
o -> [ObjectPropertyExpression
o]
                    AS.SubObjPropExpr_exprchain c :: [ObjectPropertyExpression]
c -> [ObjectPropertyExpression]
c
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s (ObjectPropertyExpression
supOpExpr ObjectPropertyExpression
-> [ObjectPropertyExpression] -> [ObjectPropertyExpression]
forall a. a -> [a] -> [a]
: [ObjectPropertyExpression]
subOpExpr2)
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.EquivalentObjectProperties anns :: [Annotation]
anns opExprs :: [ObjectPropertyExpression]
opExprs -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression]
opExprs
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.DisjointObjectProperties anns :: [Annotation]
anns opExprs :: [ObjectPropertyExpression]
opExprs -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression]
opExprs
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.InverseObjectProperties anns :: [Annotation]
anns opExpr1 :: ObjectPropertyExpression
opExpr1 opExpr2 :: ObjectPropertyExpression
opExpr2 -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr1, ObjectPropertyExpression
opExpr2]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.ObjectPropertyDomain anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr clExpr :: ClassExpression
clExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            ClassExpression
nClExpr <- Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s ClassExpression
clExpr
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom
                (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> ObjectPropertyExpression
-> ClassExpression
-> ObjectPropertyAxiom
AS.ObjectPropertyDomain [Annotation]
anns ObjectPropertyExpression
opExpr ClassExpression
nClExpr]

        AS.ObjectPropertyRange anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr clExpr :: ClassExpression
clExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            ClassExpression
nClExpr <- Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s ClassExpression
clExpr
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom
                (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation]
-> ObjectPropertyExpression
-> ClassExpression
-> ObjectPropertyAxiom
AS.ObjectPropertyRange [Annotation]
anns ObjectPropertyExpression
opExpr ClassExpression
nClExpr]

        AS.FunctionalObjectProperty anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.InverseFunctionalObjectProperty anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.ReflexiveObjectProperty anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.IrreflexiveObjectProperty anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.SymmetricObjectProperty anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.AsymmetricObjectProperty anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.TransitiveObjectProperty anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

    (AS.DataPropertyAxiom dpAxiom :: DataPropertyAxiom
dpAxiom) -> case DataPropertyAxiom
dpAxiom of
        AS.SubDataPropertyOf anns :: [Annotation]
anns subDpExpr :: IRI
subDpExpr supDpExpr :: IRI
supDpExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [IRI] -> Result ()
checkDataPropList Sign
s [IRI
subDpExpr, IRI
supDpExpr]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.EquivalentDataProperties anns :: [Annotation]
anns dpExprs :: [IRI]
dpExprs -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([IRI] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [IRI]
dpExprs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> [IRI] -> Result ()
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Incorrect number of Data Property Expressions (must be >= 2): " [IRI]
dpExprs
            Sign -> [IRI] -> Result ()
checkDataPropList Sign
s [IRI]
dpExprs
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.DisjointDataProperties anns :: [Annotation]
anns dpExprs :: [IRI]
dpExprs -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([IRI] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [IRI]
dpExprs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> [IRI] -> Result ()
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Incorrect number of Data Property Expressions (must be >= 2): " [IRI]
dpExprs
            Sign -> [IRI] -> Result ()
checkDataPropList Sign
s [IRI]
dpExprs
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.DataPropertyDomain anns :: [Annotation]
anns dpExpr :: IRI
dpExpr clExpr :: ClassExpression
clExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [IRI] -> Result ()
checkDataPropList Sign
s [IRI
dpExpr]
            ClassExpression
nClExpr <- Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s ClassExpression
clExpr
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [DataPropertyAxiom -> Axiom
AS.DataPropertyAxiom
                (DataPropertyAxiom -> Axiom) -> DataPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> IRI -> ClassExpression -> DataPropertyAxiom
AS.DataPropertyDomain [Annotation]
anns IRI
dpExpr ClassExpression
nClExpr]

        AS.DataPropertyRange anns :: [Annotation]
anns dpExpr :: IRI
dpExpr dr :: DataRange
dr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [IRI] -> Result ()
checkDataPropList Sign
s [IRI
dpExpr]
            Sign -> DataRange -> Result ()
checkDataRange Sign
s DataRange
dr
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.FunctionalDataProperty anns :: [Annotation]
anns dpExpr :: IRI
dpExpr -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [IRI] -> Result ()
checkDataPropList Sign
s [IRI
dpExpr]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]
            
    AS.DatatypeDefinition anns :: [Annotation]
anns dt :: IRI
dt dr :: DataRange
dr -> do
        Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
        Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> Entity -> Result ()
forall a b. (a -> b) -> a -> b
$ EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.Datatype IRI
dt
        Sign -> DataRange -> Result ()
checkDataRange Sign
s DataRange
dr
        [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

    AS.HasKey anns :: [Annotation]
anns clExpr :: ClassExpression
clExpr opExprs :: [ObjectPropertyExpression]
opExprs dpExprs :: [IRI]
dpExprs -> do
        Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
        ClassExpression
nClExpr <- Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s ClassExpression
clExpr
        (nOpExprs :: [ObjectPropertyExpression]
nOpExprs, nDpExprs :: [IRI]
nDpExprs) <- Sign
-> [ObjectPropertyExpression]
-> [IRI]
-> Result ([ObjectPropertyExpression], [IRI])
checkHasKey Sign
s [ObjectPropertyExpression]
opExprs [IRI]
dpExprs
        [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [[Annotation]
-> ClassExpression -> [ObjectPropertyExpression] -> [IRI] -> Axiom
AS.HasKey [Annotation]
anns ClassExpression
nClExpr [ObjectPropertyExpression]
nOpExprs [IRI]
nDpExprs]

    AS.Assertion assertionAxiom :: Assertion
assertionAxiom -> case Assertion
assertionAxiom of 
        AS.SameIndividual anns :: [Annotation]
anns inds :: [IRI]
inds -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([IRI] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [IRI]
inds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> [IRI] -> Result ()
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Incorrect number of Individuals (must be >= 2): " [IRI]
inds
            (IRI -> Result ()) -> [IRI] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> (IRI -> Entity) -> IRI -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.NamedIndividual) [IRI]
inds 
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]
            
        AS.DifferentIndividuals anns :: [Annotation]
anns inds :: [IRI]
inds -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([IRI] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [IRI]
inds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> [IRI] -> Result ()
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Incorrect number of Individuals (must be >= 2): " [IRI]
inds
            (IRI -> Result ()) -> [IRI] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> (IRI -> Entity) -> IRI -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.NamedIndividual) [IRI]
inds
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.ClassAssertion anns :: [Annotation]
anns clExpr :: ClassExpression
clExpr ind :: IRI
ind -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            ClassExpression
nClExpr <- Sign -> ClassExpression -> Result ClassExpression
checkClassExpression Sign
s ClassExpression
clExpr
            Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> Entity -> Result ()
forall a b. (a -> b) -> a -> b
$ EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.NamedIndividual IRI
ind
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> ClassExpression -> IRI -> Assertion
AS.ClassAssertion [Annotation]
anns ClassExpression
nClExpr IRI
ind]

        AS.ObjectPropertyAssertion anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr sInd :: IRI
sInd tInd :: IRI
tInd -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            (IRI -> Result ()) -> [IRI] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> (IRI -> Entity) -> IRI -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.NamedIndividual) [IRI
sInd, IRI
tInd]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.NegativeObjectPropertyAssertion anns :: [Annotation]
anns opExpr :: ObjectPropertyExpression
opExpr sInd :: IRI
sInd tInd :: IRI
tInd -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [ObjectPropertyExpression] -> Result ()
checkObjPropList Sign
s [ObjectPropertyExpression
opExpr]
            (IRI -> Result ()) -> [IRI] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> (IRI -> Entity) -> IRI -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.NamedIndividual) [IRI
sInd, IRI
tInd]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.DataPropertyAssertion anns :: [Annotation]
anns dpExpr :: IRI
dpExpr sInd :: IRI
sInd tValue :: Literal
tValue -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [IRI] -> Result ()
checkDataPropList Sign
s [IRI
dpExpr]
            Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> Entity -> Result ()
forall a b. (a -> b) -> a -> b
$ EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.NamedIndividual IRI
sInd
            Sign -> Literal -> Result ()
checkLiteral Sign
s Literal
tValue
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.NegativeDataPropertyAssertion anns :: [Annotation]
anns dpExpr :: IRI
dpExpr sInd :: IRI
sInd tValue :: Literal
tValue -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> [IRI] -> Result ()
checkDataPropList Sign
s [IRI
dpExpr]
            Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> Entity -> Result ()
forall a b. (a -> b) -> a -> b
$ EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.NamedIndividual IRI
sInd
            Sign -> Literal -> Result ()
checkLiteral Sign
s Literal
tValue
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

    AS.AnnotationAxiom anAxiom :: AnnotationAxiom
anAxiom -> case AnnotationAxiom
anAxiom of
        AS.AnnotationAssertion anns :: [Annotation]
anns prop :: IRI
prop subj :: AnnotationSubject
subj val :: AnnotationValue
val -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> Entity -> Result ()
checkEntity Sign
s (EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.AnnotationProperty IRI
prop)

            case AnnotationSubject
subj of
                AS.AnnSubIri iri :: IRI
iri -> Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Entity] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Entity] -> Bool) -> [Entity] -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> IRI -> [Entity]
correctEntity Sign
s IRI
iri)
                    (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> String -> Result ()
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Incorrect AnnotationAssertion axiom. Axiom subject is not declared: " (IRI -> String
forall a. Show a => a -> String
show IRI
iri)
                _ -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                
            case AnnotationValue
val of
                AS.AnnValLit lit :: Literal
lit -> Sign -> Literal -> Result ()
checkLiteral Sign
s Literal
lit
                _ -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]
            

        AS.SubAnnotationPropertyOf anns :: [Annotation]
anns subAnProp :: IRI
subAnProp supAnProp :: IRI
supAnProp -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            (IRI -> Result ()) -> [IRI] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Sign -> Entity -> Result ()
checkEntity Sign
s (Entity -> Result ()) -> (IRI -> Entity) -> IRI -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.AnnotationProperty) [IRI
subAnProp, IRI
supAnProp]
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.AnnotationPropertyDomain anns :: [Annotation]
anns prop :: IRI
prop _ -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> Entity -> Result ()
checkEntity Sign
s (EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.AnnotationProperty IRI
prop)
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]

        AS.AnnotationPropertyRange anns :: [Annotation]
anns prop :: IRI
prop _ -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            Sign -> Entity -> Result ()
checkEntity Sign
s (EntityType -> IRI -> Entity
AS.mkEntity EntityType
AS.AnnotationProperty IRI
prop)
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]
        

    (AS.Rule rule :: Rule
rule) -> case Rule
rule of 
        AS.DLSafeRule anns :: [Annotation]
anns body :: [Atom]
body hea :: [Atom]
hea -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            [Atom]
nBody <- (Atom -> Result Atom) -> [Atom] -> Result [Atom]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> Maybe [IRI] -> Atom -> Result Atom
checkDLAtom Sign
s Maybe [IRI]
forall a. Maybe a
Nothing) [Atom]
body
            let vars :: [IRI]
vars = [Atom] -> [IRI]
extractVariables [Atom]
body
            [Atom]
nHead <- (Atom -> Result Atom) -> [Atom] -> Result [Atom]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> Maybe [IRI] -> Atom -> Result Atom
checkDLAtom Sign
s ([IRI] -> Maybe [IRI]
forall a. a -> Maybe a
Just [IRI]
vars)) [Atom]
hea
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Rule -> Axiom
AS.Rule (Rule -> Axiom) -> Rule -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [Atom] -> [Atom] -> Rule
AS.DLSafeRule [Annotation]
anns [Atom]
nBody [Atom]
nHead]
        AS.DGRule anns :: [Annotation]
anns body :: [DGAtom]
body hea :: [DGAtom]
hea -> do
            Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
            (DGAtom -> Result DGAtom) -> [DGAtom] -> Result [DGAtom]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> Maybe [IRI] -> DGAtom -> Result DGAtom
checkDGAtom Sign
s Maybe [IRI]
forall a. Maybe a
Nothing) [DGAtom]
body
            let vars :: [IRI]
vars = [DGAtom] -> [IRI]
extractDGVariables [DGAtom]
body
            (DGAtom -> Result DGAtom) -> [DGAtom] -> Result [DGAtom]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> Maybe [IRI] -> DGAtom -> Result DGAtom
checkDGAtom Sign
s ([IRI] -> Maybe [IRI]
forall a. a -> Maybe a
Just [IRI]
vars)) [DGAtom]
hea
            [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]
    (AS.DGAxiom anns :: [Annotation]
anns _ _ edges :: DGEdges
edges _) -> do
        Sign -> [Annotation] -> Result ()
checkAnnos Sign
s [Annotation]
anns
        (DGEdgeAssertion -> Result ()) -> DGEdges -> Result [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> DGEdgeAssertion -> Result ()
checkDGEdgeAssertion Sign
s) DGEdges
edges
        [Axiom] -> Result [Axiom]
forall (m :: * -> *) a. Monad m => a -> m a
return [Axiom
a]



correctFrames :: Sign -> [AS.Axiom] -> Result [AS.Axiom]
correctFrames :: Sign -> [Axiom] -> Result [Axiom]
correctFrames s :: Sign
s = ([[Axiom]] -> [Axiom]) -> Result [[Axiom]] -> Result [Axiom]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Axiom]] -> [Axiom]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Result [[Axiom]] -> Result [Axiom])
-> ([Axiom] -> Result [[Axiom]]) -> [Axiom] -> Result [Axiom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Axiom -> Result [Axiom]) -> [Axiom] -> Result [[Axiom]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> Axiom -> Result [Axiom]
checkAxiom Sign
s)

collectEntities :: AS.Axiom -> State Sign ()
collectEntities :: Axiom -> State Sign ()
collectEntities f :: Axiom
f = case Axiom
f of
    AS.Declaration _ e :: Entity
e -> Entity -> State Sign ()
addEntity Entity
e
    _ -> () -> State Sign ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | collects all entites from the aximoms
createSign :: [AS.Axiom] -> State Sign ()
createSign :: [Axiom] -> State Sign ()
createSign f :: [Axiom]
f = do
  PrefixMap
pm <- (Sign -> PrefixMap) -> State Sign PrefixMap
forall s a. (s -> a) -> State s a
gets Sign -> PrefixMap
prefixMap
  (Axiom -> State Sign ()) -> [Axiom] -> State Sign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Axiom -> State Sign ()
collectEntities (Axiom -> State Sign ())
-> (Axiom -> Axiom) -> Axiom -> State Sign ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action -> AMap -> Axiom -> Axiom
forall a. Function a => Action -> AMap -> a -> a
function Action
Expand (PrefixMap -> AMap
StringMap PrefixMap
pm)) [Axiom]
f

noDecl :: AS.Axiom -> Bool
noDecl :: Axiom -> Bool
noDecl ax :: Axiom
ax = case Axiom
ax of
  AS.Declaration _ _ -> Bool
False
  _ -> Bool
True

-- | corrects the axioms according to the signature
createAxioms :: Sign -> [AS.Axiom] -> Result ([Named AS.Axiom], [AS.Axiom])
createAxioms :: Sign -> [Axiom] -> Result ([Named Axiom], [Axiom])
createAxioms s :: Sign
s fl :: [Axiom]
fl = do
    [Axiom]
cf <- Sign -> [Axiom] -> Result [Axiom]
correctFrames Sign
s ([Axiom] -> Result [Axiom]) -> [Axiom] -> Result [Axiom]
forall a b. (a -> b) -> a -> b
$ (Axiom -> Axiom) -> [Axiom] -> [Axiom]
forall a b. (a -> b) -> [a] -> [b]
map (Action -> AMap -> Axiom -> Axiom
forall a. Function a => Action -> AMap -> a -> a
function Action
Expand (AMap -> Axiom -> Axiom) -> AMap -> Axiom -> Axiom
forall a b. (a -> b) -> a -> b
$ PrefixMap -> AMap
StringMap (PrefixMap -> AMap) -> PrefixMap -> AMap
forall a b. (a -> b) -> a -> b
$ Sign -> PrefixMap
prefixMap Sign
s) [Axiom]
fl
    ([Named Axiom], [Axiom]) -> Result ([Named Axiom], [Axiom])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Axiom -> Named Axiom) -> [Axiom] -> [Named Axiom]
forall a b. (a -> b) -> [a] -> [b]
map Axiom -> Named Axiom
anaAxiom ([Axiom] -> [Named Axiom])
-> ([Axiom] -> [Axiom]) -> [Axiom] -> [Named Axiom]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Axiom -> Bool) -> [Axiom] -> [Axiom]
forall a. (a -> Bool) -> [a] -> [a]
filter Axiom -> Bool
noDecl ([Axiom] -> [Named Axiom]) -> [Axiom] -> [Named Axiom]
forall a b. (a -> b) -> a -> b
$ [Axiom]
cf, [Axiom]
cf)

check1Prefix :: Maybe IRI -> IRI -> Bool
check1Prefix :: Maybe IRI -> IRI -> Bool
check1Prefix ms :: Maybe IRI
ms s :: IRI
s = case Maybe IRI
ms of
      Nothing -> Bool
True
      Just iri :: IRI
iri -> IRI
iri IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
s

checkPrefixMap :: GA.PrefixMap -> Bool
checkPrefixMap :: PrefixMap -> Bool
checkPrefixMap pm :: PrefixMap
pm =
    let pl :: [Maybe IRI]
pl = (String -> Maybe IRI) -> [String] -> [Maybe IRI]
forall a b. (a -> b) -> [a] -> [b]
map (String -> PrefixMap -> Maybe IRI
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` PrefixMap
pm) ["owl", "rdf", "rdfs", "xsd"]
    in [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Maybe IRI -> IRI -> Bool) -> [Maybe IRI] -> [IRI] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Maybe IRI -> IRI -> Bool
check1Prefix [Maybe IRI]
pl
            (((String, IRI) -> IRI) -> [(String, IRI)] -> [IRI]
forall a b. (a -> b) -> [a] -> [b]
map (String, IRI) -> IRI
forall a b. (a, b) -> b
snd ([(String, IRI)] -> [IRI]) -> [(String, IRI)] -> [IRI]
forall a b. (a -> b) -> a -> b
$ PrefixMap -> [(String, IRI)]
forall k a. Map k a -> [(k, a)]
Map.toList PrefixMap
AS.predefPrefixesGA)

newODoc :: AS.OntologyDocument -> [AS.Axiom] -> Result AS.OntologyDocument
newODoc :: OntologyDocument -> [Axiom] -> Result OntologyDocument
newODoc AS.OntologyDocument {
      ontology :: OntologyDocument -> Ontology
AS.ontology = Ontology
mo
    , ontologyMetadata :: OntologyDocument -> OntologyMetadata
AS.ontologyMetadata = OntologyMetadata
md
    , prefixDeclaration :: OntologyDocument -> PrefixMap
AS.prefixDeclaration = PrefixMap
pd} ax :: [Axiom]
ax =
    if PrefixMap -> Bool
checkPrefixMap PrefixMap
pd
        then OntologyDocument -> Result OntologyDocument
forall (m :: * -> *) a. Monad m => a -> m a
return OntologyDocument :: OntologyMetadata -> PrefixMap -> Ontology -> OntologyDocument
AS.OntologyDocument
                { ontologyMetadata :: OntologyMetadata
AS.ontologyMetadata = OntologyMetadata
md
                , ontology :: Ontology
AS.ontology = Ontology
mo {axioms :: [Axiom]
AS.axioms = [Axiom]
ax}
                , prefixDeclaration :: PrefixMap
AS.prefixDeclaration = PrefixMap
pd
                }
        else String -> Result OntologyDocument
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result OntologyDocument)
-> String -> Result OntologyDocument
forall a b. (a -> b) -> a -> b
$ "Incorrect predefined prefixes " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PrefixMap -> String -> String
forall a. Pretty a => a -> String -> String
showDoc PrefixMap
pd "\n"

-- | static analysis of ontology with incoming sign.
basicOWL2Analysis :: (AS.OntologyDocument, Sign, GlobalAnnos)
    -> Result (AS.OntologyDocument, ExtSign Sign AS.Entity, [Named AS.Axiom])
basicOWL2Analysis :: (OntologyDocument, Sign, GlobalAnnos)
-> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom])
basicOWL2Analysis (inOnt :: OntologyDocument
inOnt, inSign :: Sign
inSign, ga :: GlobalAnnos
ga) = do
    let pm :: PrefixMap
pm = PrefixMap -> PrefixMap -> PrefixMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (OntologyDocument -> PrefixMap
AS.prefixDeclaration OntologyDocument
inOnt)
          (PrefixMap -> PrefixMap)
-> (PrefixMap -> PrefixMap) -> PrefixMap -> PrefixMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> PrefixMap -> PrefixMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete "" (PrefixMap -> PrefixMap) -> PrefixMap -> PrefixMap
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> PrefixMap
prefix_map GlobalAnnos
ga
        odoc :: OntologyDocument
odoc = OntologyDocument
inOnt { prefixDeclaration :: PrefixMap
AS.prefixDeclaration = PrefixMap
pm }
        axs :: [Axiom]
axs = Ontology -> [Axiom]
AS.axioms (Ontology -> [Axiom]) -> Ontology -> [Axiom]
forall a b. (a -> b) -> a -> b
$ OntologyDocument -> Ontology
AS.ontology OntologyDocument
odoc
        accSign :: Sign
accSign = State Sign () -> Sign -> Sign
forall s a. State s a -> s -> s
execState ([Axiom] -> State Sign ()
createSign [Axiom]
axs) Sign
inSign { prefixMap :: PrefixMap
prefixMap = PrefixMap -> PrefixMap
AS.changePrefixMapTypeToString PrefixMap
pm }
        syms :: Set Entity
syms = Set Entity -> Set Entity -> Set Entity
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set Entity
symOf Sign
accSign) (Set Entity -> Set Entity) -> Set Entity -> Set Entity
forall a b. (a -> b) -> a -> b
$ Sign -> Set Entity
symOf Sign
inSign
    (axl :: [Named Axiom]
axl, nfl :: [Axiom]
nfl) <- Sign -> [Axiom] -> Result ([Named Axiom], [Axiom])
createAxioms Sign
accSign [Axiom]
axs
    OntologyDocument
newdoc <- OntologyDocument -> [Axiom] -> Result OntologyDocument
newODoc OntologyDocument
odoc [Axiom]
nfl
    (OntologyDocument, ExtSign Sign Entity, [Named Axiom])
-> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom])
forall (m :: * -> *) a. Monad m => a -> m a
return (OntologyDocument
newdoc
      , Sign -> Set Entity -> ExtSign Sign Entity
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign Sign
accSign {labelMap :: Map IRI String
labelMap = Sign -> [Axiom] -> Map IRI String
generateLabelMap Sign
accSign [Axiom]
nfl} Set Entity
syms, [Named Axiom]
axl)

-- | extract labels from Axiom-List (after processing with correctFrames)
generateLabelMap :: Sign -> [AS.Axiom] -> Map.Map IRI String
generateLabelMap :: Sign -> [Axiom] -> Map IRI String
generateLabelMap sig :: Sign
sig = (Axiom -> Map IRI String -> Map IRI String)
-> Map IRI String -> [Axiom] -> Map IRI String
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ a :: Axiom
a -> case Axiom
a of 
        AS.AnnotationAxiom ax :: AnnotationAxiom
ax -> case AnnotationAxiom
ax of
            AS.AnnotationAssertion _ apr :: IRI
apr sub :: AnnotationSubject
sub (AS.AnnValLit (AS.Literal s' :: String
s' _))
                | IRI -> String
prefixName IRI
apr String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "rdfs" Bool -> Bool -> Bool
&& Id -> String
forall a. Show a => a -> String
show (IRI -> Id
iriPath IRI
apr) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "label"
                -> IRI -> String -> Map IRI String -> Map IRI String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (AnnotationSubject -> IRI
ir AnnotationSubject
sub) String
s'
            _ -> Map IRI String -> Map IRI String
forall a. a -> a
id
        _ -> Map IRI String -> Map IRI String
forall a. a -> a
id) (Sign -> Map IRI String
labelMap Sign
sig)
    where ir :: AnnotationSubject -> IRI
ir sub :: AnnotationSubject
sub = case AnnotationSubject
sub of
            AS.AnnSubIri i :: IRI
i -> IRI
i
            AS.AnnSubAnInd i :: IRI
i -> IRI
i 

-- | adding annotations for theorems
anaAxiom :: AS.Axiom -> Named AS.Axiom
anaAxiom :: Axiom -> Named Axiom
anaAxiom ax :: Axiom
ax = Axiom -> Named Axiom -> Named Axiom
findImplied Axiom
ax (Named Axiom -> Named Axiom) -> Named Axiom -> Named Axiom
forall a b. (a -> b) -> a -> b
$ String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed String
nm Axiom
ax
   where names :: [String]
names = Axiom -> [String]
getNames Axiom
ax
         nm :: String
nm = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse "_" [String]
names
         
findImplied :: AS.Axiom -> Named AS.Axiom -> Named AS.Axiom
findImplied :: Axiom -> Named Axiom -> Named Axiom
findImplied ax :: Axiom
ax sent :: Named Axiom
sent =
  if Axiom -> Bool
prove Axiom
ax then Named Axiom
sent
         { isAxiom :: Bool
isAxiom = Bool
False
         , isDef :: Bool
isDef = Bool
False
         , wasTheorem :: Bool
wasTheorem = Bool
False }
   else Named Axiom
sent { isAxiom :: Bool
isAxiom = Bool
True }

getNamesFromAnnos :: [AS.Annotation] -> [String]
getNamesFromAnnos :: [Annotation] -> [String]
getNamesFromAnnos = [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[String]] -> [String])
-> ([Annotation] -> [[String]]) -> [Annotation] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Annotation -> [String]) -> [Annotation] -> [[String]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\anno :: Annotation
anno -> case Annotation
anno of
      AS.Annotation _ aIRI :: IRI
aIRI (AS.AnnValLit (AS.Literal value :: String
value _)) ->
          if Id -> String
forall a. Show a => a -> String
show (IRI -> Id
iriPath IRI
aIRI) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "label"
             then [String
value]
             else []
      _ -> [])

getNames :: AS.Axiom -> [String]
getNames :: Axiom -> [String]
getNames ax :: Axiom
ax = case Axiom
ax of
    AS.Declaration anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
    AS.ClassAxiom cax :: ClassAxiom
cax -> case ClassAxiom
cax of
        AS.SubClassOf anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.EquivalentClasses anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.DisjointClasses anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.DisjointUnion anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
    AS.ObjectPropertyAxiom opax :: ObjectPropertyAxiom
opax -> case ObjectPropertyAxiom
opax of
        AS.SubObjectPropertyOf anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.EquivalentObjectProperties anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.DisjointObjectProperties anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.InverseObjectProperties anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.ObjectPropertyDomain anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.ObjectPropertyRange anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.FunctionalObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.InverseFunctionalObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.ReflexiveObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.IrreflexiveObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.SymmetricObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.AsymmetricObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.TransitiveObjectProperty anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
    AS.DataPropertyAxiom a :: DataPropertyAxiom
a -> case DataPropertyAxiom
a of
        AS.SubDataPropertyOf anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.EquivalentDataProperties anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.DisjointDataProperties anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.DataPropertyDomain anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.DataPropertyRange anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.FunctionalDataProperty anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
    AS.DatatypeDefinition anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
    AS.HasKey anns :: [Annotation]
anns _ _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
    AS.Assertion a :: Assertion
a -> case Assertion
a of
        AS.SameIndividual anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.DifferentIndividuals anns :: [Annotation]
anns _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.ClassAssertion anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.ObjectPropertyAssertion anns :: [Annotation]
anns _ _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.NegativeObjectPropertyAssertion anns :: [Annotation]
anns _ _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.DataPropertyAssertion anns :: [Annotation]
anns _ _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.NegativeDataPropertyAssertion anns :: [Annotation]
anns _ _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
    AS.AnnotationAxiom a :: AnnotationAxiom
a -> case AnnotationAxiom
a of
        AS.AnnotationAssertion anns :: [Annotation]
anns _ _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.SubAnnotationPropertyOf anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.AnnotationPropertyDomain anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.AnnotationPropertyRange anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
    AS.DGAxiom anns :: [Annotation]
anns _ _ _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
    AS.Rule r :: Rule
r -> case Rule
r of
        AS.DLSafeRule anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns
        AS.DGRule anns :: [Annotation]
anns _ _ -> [Annotation] -> [String]
getNamesFromAnnos [Annotation]
anns


addEquiv :: Sign -> Sign -> [SymbItems] -> [SymbItems] ->
            Result (Sign, Sign, Sign,
                     EndoMap AS.Entity, EndoMap AS.Entity)
addEquiv :: Sign
-> Sign
-> [SymbItems]
-> [SymbItems]
-> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity)
addEquiv ssig :: Sign
ssig tsig :: Sign
tsig l1 :: [SymbItems]
l1 l2 :: [SymbItems]
l2 = do
  let l1' :: [RawSymb]
l1' = Sign -> [SymbItems] -> [RawSymb]
statSymbItems Sign
ssig [SymbItems]
l1
      l2' :: [RawSymb]
l2' = Sign -> [SymbItems] -> [RawSymb]
statSymbItems Sign
tsig [SymbItems]
l2
  case ([RawSymb]
l1', [RawSymb]
l2') of
    ([rs1 :: RawSymb
rs1], [rs2 :: RawSymb
rs2]) -> do
      let match1 :: [Entity]
match1 = (Entity -> Bool) -> [Entity] -> [Entity]
forall a. (a -> Bool) -> [a] -> [a]
filter (Entity -> RawSymb -> Bool
`matchesSym` RawSymb
rs1) ([Entity] -> [Entity]) -> [Entity] -> [Entity]
forall a b. (a -> b) -> a -> b
$ Set Entity -> [Entity]
forall a. Set a -> [a]
Set.toList (Set Entity -> [Entity]) -> Set Entity -> [Entity]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Entity
symOf Sign
ssig
          match2 :: [Entity]
match2 = (Entity -> Bool) -> [Entity] -> [Entity]
forall a. (a -> Bool) -> [a] -> [a]
filter (Entity -> RawSymb -> Bool
`matchesSym` RawSymb
rs2) ([Entity] -> [Entity]) -> [Entity] -> [Entity]
forall a b. (a -> b) -> a -> b
$ Set Entity -> [Entity]
forall a. Set a -> [a]
Set.toList (Set Entity -> [Entity]) -> Set Entity -> [Entity]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Entity
symOf Sign
tsig
      case
       ([Entity]
match1, [Entity]
match2) of
          ([e1 :: Entity
e1], [e2 :: Entity
e2]) ->
           if Entity -> EntityType
AS.entityKind Entity
e1 EntityType -> EntityType -> Bool
forall a. Eq a => a -> a -> Bool
== Entity -> EntityType
AS.entityKind Entity
e2 then do
              Entity
s <- Entity -> Entity -> Result Entity
AS.pairSymbols Entity
e1 Entity
e2
              Sign
sig <- Sign -> Entity -> Result Sign
addSymbToSign Sign
emptySign Entity
s
              Sign
sig1 <- Sign -> Entity -> Result Sign
addSymbToSign Sign
emptySign Entity
e1
              Sign
sig2 <- Sign -> Entity -> Result Sign
addSymbToSign Sign
emptySign Entity
e2
              (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity)
-> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sig, Sign
sig1, Sign
sig2,
                         Entity -> Entity -> EndoMap Entity -> EndoMap Entity
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Entity
e1 Entity
s EndoMap Entity
forall k a. Map k a
Map.empty,
                         Entity -> Entity -> EndoMap Entity -> EndoMap Entity
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Entity
e2 Entity
s EndoMap Entity
forall k a. Map k a
Map.empty)
             else
              String -> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "only symbols of same kind can be equivalent in an alignment"
          _ -> String -> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String
 -> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity))
-> String
-> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity)
forall a b. (a -> b) -> a -> b
$ "non-unique symbol match:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SymbItems] -> String -> String
forall a. Pretty a => a -> String -> String
showDoc [SymbItems]
l1 " "
                                                 String -> String -> String
forall a. [a] -> [a] -> [a]
++  [SymbItems] -> String -> String
forall a. Pretty a => a -> String -> String
showDoc [SymbItems]
l2 " "
    _ -> String -> Result (Sign, Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "terms not yet supported in alignments"

corr2theo :: String -> Bool -> Sign -> Sign -> [SymbItems] -> [SymbItems] ->
             EndoMap AS.Entity -> EndoMap AS.Entity -> REL_REF ->
             Result (Sign, [Named AS.Axiom], Sign, Sign,
                     EndoMap AS.Entity, EndoMap AS.Entity)
corr2theo :: String
-> Bool
-> Sign
-> Sign
-> [SymbItems]
-> [SymbItems]
-> EndoMap Entity
-> EndoMap Entity
-> REL_REF
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
corr2theo _aname :: String
_aname flag :: Bool
flag ssig :: Sign
ssig tsig :: Sign
tsig l1 :: [SymbItems]
l1 l2 :: [SymbItems]
l2 eMap1 :: EndoMap Entity
eMap1 eMap2 :: EndoMap Entity
eMap2 rref :: REL_REF
rref = do
  let l1' :: [RawSymb]
l1' = Sign -> [SymbItems] -> [RawSymb]
statSymbItems Sign
ssig [SymbItems]
l1
      l2' :: [RawSymb]
l2' = Sign -> [SymbItems] -> [RawSymb]
statSymbItems Sign
tsig [SymbItems]
l2
  case ([RawSymb]
l1', [RawSymb]
l2') of
    ([rs1 :: RawSymb
rs1], [rs2 :: RawSymb
rs2]) -> do
      let match1 :: [Entity]
match1 = (Entity -> Bool) -> [Entity] -> [Entity]
forall a. (a -> Bool) -> [a] -> [a]
filter (Entity -> RawSymb -> Bool
`matchesSym` RawSymb
rs1) ([Entity] -> [Entity]) -> [Entity] -> [Entity]
forall a b. (a -> b) -> a -> b
$ Set Entity -> [Entity]
forall a. Set a -> [a]
Set.toList (Set Entity -> [Entity]) -> Set Entity -> [Entity]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Entity
symOf Sign
ssig
          match2 :: [Entity]
match2 = (Entity -> Bool) -> [Entity] -> [Entity]
forall a. (a -> Bool) -> [a] -> [a]
filter (Entity -> RawSymb -> Bool
`matchesSym` RawSymb
rs2) ([Entity] -> [Entity]) -> [Entity] -> [Entity]
forall a b. (a -> b) -> a -> b
$ Set Entity -> [Entity]
forall a. Set a -> [a]
Set.toList (Set Entity -> [Entity]) -> Set Entity -> [Entity]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Entity
symOf Sign
tsig
      case
       ([Entity]
match1, [Entity]
match2) of
          ([e1 :: Entity
e1], [e2 :: Entity
e2]) -> do
           let e1' :: Entity
e1' = if Bool
flag then Entity
e1 {cutIRI :: IRI
AS.cutIRI =  (IRI, String) -> IRI
forall a. SymbolName a => (a, String) -> a
addString (Entity -> IRI
AS.cutIRI Entity
e1, "_source")} else Entity
e1
               e2' :: Entity
e2' = if Bool
flag then Entity
e2 {cutIRI :: IRI
AS.cutIRI =  (IRI, String) -> IRI
forall a. SymbolName a => (a, String) -> a
addString (Entity -> IRI
AS.cutIRI Entity
e2, "_target")} else Entity
e2
               sig :: Sign
sig = Sign
emptySign
               eMap1' :: EndoMap Entity
eMap1' = EndoMap Entity -> EndoMap Entity -> EndoMap Entity
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union EndoMap Entity
eMap1 (EndoMap Entity -> EndoMap Entity)
-> EndoMap Entity -> EndoMap Entity
forall a b. (a -> b) -> a -> b
$ [(Entity, Entity)] -> EndoMap Entity
forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList [(Entity
e1', Entity
e1)]
               eMap2' :: EndoMap Entity
eMap2' = EndoMap Entity -> EndoMap Entity -> EndoMap Entity
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union EndoMap Entity
eMap2 (EndoMap Entity -> EndoMap Entity)
-> EndoMap Entity -> EndoMap Entity
forall a b. (a -> b) -> a -> b
$ [(Entity, Entity)] -> EndoMap Entity
forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList [(Entity
e2', Entity
e2)]
           Sign
sig1 <- Sign -> Entity -> Result Sign
addSymbToSign Sign
sig Entity
e1'
           Sign
sig2 <- Sign -> Entity -> Result Sign
addSymbToSign Sign
sig Entity
e2'
           Sign
sigB <- Sign -> Entity -> Result Sign
addSymbToSign Sign
sig1 Entity
e2'
           case REL_REF
rref of
            Equiv -> do
                let axiom :: Axiom
axiom = case (Entity -> EntityType
AS.entityKind Entity
e1', Entity -> EntityType
AS.entityKind Entity
e2') of
                        (AS.Class, AS.Class) -> ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$
                                [Annotation] -> [ClassExpression] -> ClassAxiom
AS.EquivalentClasses [] (IRI -> ClassExpression
AS.Expression (IRI -> ClassExpression)
-> (Entity -> IRI) -> Entity -> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entity -> IRI
AS.cutIRI (Entity -> ClassExpression) -> [Entity] -> [ClassExpression]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Entity
e1', Entity
e2'])
                        (AS.ObjectProperty, AS.ObjectProperty) -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$
                            [Annotation] -> [ObjectPropertyExpression] -> ObjectPropertyAxiom
AS.EquivalentObjectProperties [] (IRI -> ObjectPropertyExpression
AS.ObjectProp (IRI -> ObjectPropertyExpression)
-> (Entity -> IRI) -> Entity -> ObjectPropertyExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entity -> IRI
AS.cutIRI (Entity -> ObjectPropertyExpression)
-> [Entity] -> [ObjectPropertyExpression]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Entity
e1', Entity
e2'])
                        (AS.NamedIndividual, AS.NamedIndividual) -> Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$
                            [Annotation] -> [IRI] -> Assertion
AS.SameIndividual [] (Entity -> IRI
AS.cutIRI (Entity -> IRI) -> [Entity] -> [IRI]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Entity
e1', Entity
e2'])
                        _ -> String -> Axiom
forall a. HasCallStack => String -> a
error (String -> Axiom) -> String -> Axiom
forall a b. (a -> b) -> a -> b
$ "use subsumption only between"
                                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ "classes or roles:" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                        [SymbItems] -> String
forall a. Show a => a -> String
show [SymbItems]
l1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SymbItems] -> String
forall a. Show a => a -> String
show [SymbItems]
l2
                (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sigB, [String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed "" Axiom
axiom], Sign
sig1, Sign
sig2, EndoMap Entity
eMap1', EndoMap Entity
eMap2')
            Subs -> do
                let axiom :: Axiom
axiom = case (Entity -> EntityType
AS.entityKind Entity
e1', Entity -> EntityType
AS.entityKind Entity
e2') of
                        (AS.Class, AS.Class) -> ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$
                            [Annotation] -> ClassExpression -> ClassExpression -> ClassAxiom
AS.SubClassOf []
                                (IRI -> ClassExpression
AS.Expression (IRI -> ClassExpression)
-> (Entity -> IRI) -> Entity -> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entity -> IRI
AS.cutIRI (Entity -> ClassExpression) -> Entity -> ClassExpression
forall a b. (a -> b) -> a -> b
$ Entity
e1')
                                (IRI -> ClassExpression
AS.Expression (IRI -> ClassExpression)
-> (Entity -> IRI) -> Entity -> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entity -> IRI
AS.cutIRI (Entity -> ClassExpression) -> Entity -> ClassExpression
forall a b. (a -> b) -> a -> b
$ Entity
e2')
                        (AS.ObjectProperty, AS.ObjectProperty) -> ObjectPropertyAxiom -> Axiom
AS.ObjectPropertyAxiom (ObjectPropertyAxiom -> Axiom) -> ObjectPropertyAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$
                            [Annotation]
-> SubObjectPropertyExpression
-> ObjectPropertyExpression
-> ObjectPropertyAxiom
AS.SubObjectPropertyOf []
                                (ObjectPropertyExpression -> SubObjectPropertyExpression
AS.SubObjPropExpr_obj (ObjectPropertyExpression -> SubObjectPropertyExpression)
-> ObjectPropertyExpression -> SubObjectPropertyExpression
forall a b. (a -> b) -> a -> b
$ IRI -> ObjectPropertyExpression
AS.ObjectProp (IRI -> ObjectPropertyExpression)
-> IRI -> ObjectPropertyExpression
forall a b. (a -> b) -> a -> b
$ Entity -> IRI
AS.cutIRI Entity
e1')
                                (IRI -> ObjectPropertyExpression
AS.ObjectProp (IRI -> ObjectPropertyExpression)
-> IRI -> ObjectPropertyExpression
forall a b. (a -> b) -> a -> b
$ Entity -> IRI
AS.cutIRI Entity
e2')
                        _ -> String -> Axiom
forall a. HasCallStack => String -> a
error (String -> Axiom) -> String -> Axiom
forall a b. (a -> b) -> a -> b
$ "use subsumption only between"
                                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ "classes or roles:" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                        [SymbItems] -> String
forall a. Show a => a -> String
show [SymbItems]
l1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SymbItems] -> String
forall a. Show a => a -> String
show [SymbItems]
l2
                (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sigB, [String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed "" Axiom
axiom], Sign
sig1, Sign
sig2, EndoMap Entity
eMap1', EndoMap Entity
eMap2')
            Incomp -> do
                let axiom :: Axiom
axiom = ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> [ClassExpression] -> ClassAxiom
AS.DisjointClasses [] (IRI -> ClassExpression
AS.Expression (IRI -> ClassExpression)
-> (Entity -> IRI) -> Entity -> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entity -> IRI
AS.cutIRI (Entity -> ClassExpression) -> [Entity] -> [ClassExpression]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Entity
e1', Entity
e2'])
                (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sigB, [String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed "" Axiom
axiom], Sign
sig1, Sign
sig2, EndoMap Entity
eMap1', EndoMap Entity
eMap2')
            IsSubs -> do
                let axiom :: Axiom
axiom = ClassAxiom -> Axiom
AS.ClassAxiom (ClassAxiom -> Axiom) -> ClassAxiom -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> ClassExpression -> ClassExpression -> ClassAxiom
AS.SubClassOf []
                        (IRI -> ClassExpression
AS.Expression (IRI -> ClassExpression)
-> (Entity -> IRI) -> Entity -> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entity -> IRI
AS.cutIRI (Entity -> ClassExpression) -> Entity -> ClassExpression
forall a b. (a -> b) -> a -> b
$ Entity
e1')
                        (IRI -> ClassExpression
AS.Expression (IRI -> ClassExpression)
-> (Entity -> IRI) -> Entity -> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entity -> IRI
AS.cutIRI (Entity -> ClassExpression) -> Entity -> ClassExpression
forall a b. (a -> b) -> a -> b
$ Entity
e2')
                (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sigB, [String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed "" Axiom
axiom], Sign
sig1, Sign
sig2, EndoMap Entity
eMap1', EndoMap Entity
eMap2')
            InstOf -> do
                let axiom :: Axiom
axiom = Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> ClassExpression -> IRI -> Assertion
AS.ClassAssertion []
                        (IRI -> ClassExpression
AS.Expression (IRI -> ClassExpression)
-> (Entity -> IRI) -> Entity -> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entity -> IRI
AS.cutIRI (Entity -> ClassExpression) -> Entity -> ClassExpression
forall a b. (a -> b) -> a -> b
$ Entity
e1')
                        (Entity -> IRI
AS.cutIRI (Entity -> IRI) -> Entity -> IRI
forall a b. (a -> b) -> a -> b
$ Entity
e2')
                (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. Monad m => a -> m a
return
                    (Sign
sigB, [String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed "" Axiom
axiom], Sign
sig1, Sign
sig2, EndoMap Entity
eMap1', EndoMap Entity
eMap2')
            HasInst -> do
                let axiom :: Axiom
axiom = Assertion -> Axiom
AS.Assertion (Assertion -> Axiom) -> Assertion -> Axiom
forall a b. (a -> b) -> a -> b
$ [Annotation] -> ClassExpression -> IRI -> Assertion
AS.ClassAssertion []
                        (IRI -> ClassExpression
AS.Expression (IRI -> ClassExpression)
-> (Entity -> IRI) -> Entity -> ClassExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entity -> IRI
AS.cutIRI (Entity -> ClassExpression) -> Entity -> ClassExpression
forall a b. (a -> b) -> a -> b
$ Entity
e2')
                        (Entity -> IRI
AS.cutIRI (Entity -> IRI) -> Entity -> IRI
forall a b. (a -> b) -> a -> b
$ Entity
e1')
                (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. Monad m => a -> m a
return
                    (Sign
sigB, [String -> Axiom -> Named Axiom
forall a s. a -> s -> SenAttr s a
makeNamed "" Axiom
axiom], Sign
sig1, Sign
sig2, EndoMap Entity
eMap1', EndoMap Entity
eMap2')
            RelName _r :: IRI
_r -> String
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall a. HasCallStack => String -> a
error "nyi" {- do
             let extPart = mkExtendedEntity e1'
                 rQName = QN "" (iriToStringUnsecure r)
                             Abbreviated (iriToStringUnsecure r) Id.nullRange
                 sym = mkEntity ObjectProperty rQName
                 rSyms = filter (== sym) $
                            Set.toList $ symOf tsig
             case rSyms of
               [] -> Fail.fail $ "relation " ++ show rQName ++
                                " not in " ++ show tsig
               [rsym] -> do
                 let sym'@(Entity _ ObjectProperty rQName') =
                             Map.findWithDefault rsym rsym eMap2'
                     axiom = PlainAxiom extPart $
                              ListFrameBit (Just SubClass) $
                               ExpressionBit [([],
                                ObjectValuesFrom
                                 SomeValuesFrom
                                 (ObjectProp rQName')
                                 (Expression $ cutIRI e2'))]
                 sigB' <- addSymbToSign sigB sym'
                 sig2' <- addSymbToSign sig2 rsym
                 return
                   (sigB', [makeNamed "" axiom], sig1, sig2', eMap1',
                      Map.union eMap2' $ Map.fromAscList [(rsym, sym')])
               _ -> Fail.fail $ "too many matches for " ++ show rQName -}
            _ -> String
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String
 -> Result
      (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity))
-> String
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall a b. (a -> b) -> a -> b
$ "nyi:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ REL_REF -> String
forall a. Show a => a -> String
show REL_REF
rref
          _ -> String
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String
 -> Result
      (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity))
-> String
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall a b. (a -> b) -> a -> b
$ "non-unique symbol match:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SymbItems] -> String -> String
forall a. Pretty a => a -> String -> String
showDoc [SymbItems]
l1 " "
                                                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SymbItems] -> String -> String
forall a. Pretty a => a -> String -> String
showDoc [SymbItems]
l2 " "
    _ -> String
-> Result
     (Sign, [Named Axiom], Sign, Sign, EndoMap Entity, EndoMap Entity)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "terms not yet supported in alignments"