StaticAnalysis.hs revision d9afc6f8ffafb5297b4cdf5d3c97efba3d24b7fa
640b2adac05bb7f5e9fba064434c91852c3a72e6ndModule : $Header$
640b2adac05bb7f5e9fba064434c91852c3a72e6ndCopyright : Felix Gabriel Mance
640b2adac05bb7f5e9fba064434c91852c3a72e6ndLicense : GPLv2 or higher, see LICENSE.txt
640b2adac05bb7f5e9fba064434c91852c3a72e6ndMaintainer : f.mance@jacobs-university.de
640b2adac05bb7f5e9fba064434c91852c3a72e6ndStability : provisional
640b2adac05bb7f5e9fba064434c91852c3a72e6ndPortability : portable
640b2adac05bb7f5e9fba064434c91852c3a72e6ndStatic analysis for OWL 2
640b2adac05bb7f5e9fba064434c91852c3a72e6ndimport qualified Data.Set as Set
ef685e00a47967e27d89709461728a229d762172nd-- | Error messages for static analysis
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivefailMsg :: Entity -> ClassExpression -> Result a
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivefailMsg (Entity ty e) desc =
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive fatal_error
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars ("undeclared `" ++ showEntityType ty
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars ++ " " ++ showQN e ++ "` in the following ClassExpression:\n"
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive ++ showDoc desc "") $ iriPos e
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- | takes an entity and modifies the sign according to the given function
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivemodEntity :: (IRI -> Set.Set IRI -> Set.Set IRI) -> Entity -> State Sign ()
b44815871de48215476ad1d4cc46d3f99da532a5erikabelemodEntity f (Entity ty u) = do
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive let chg = f u
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive unless (isDatatypeKey u || isThing u) $ put $ case ty of
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Datatype -> s { datatypes = chg $ datatypes s }
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive Class -> s { concepts = chg $ concepts s }
51853aa2ebfdf9903a094467e1d02099f143639daaron ObjectProperty -> s { objectProperties = chg $ objectProperties s }
51853aa2ebfdf9903a094467e1d02099f143639daaron DataProperty -> s { dataProperties = chg $ dataProperties s }
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive NamedIndividual -> if isAnonymous u then s
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive else s { individuals = chg $ individuals s }
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive AnnotationProperty -> s {annotationRoles = chg $ annotationRoles s}
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- | adding entities to the signature
a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveaddEntity :: Entity -> State Sign ()
a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveaddEntity = modEntity Set.insert
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- | checks if an entity is in the signature
ef685e00a47967e27d89709461728a229d762172ndcheckEntity :: Sign -> Entity -> Result ()
ef685e00a47967e27d89709461728a229d762172ndcheckEntity s (Entity ty e) =
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive let errMsg = mkError ("unknown " ++ showEntityType ty) e
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive in case ty of
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars Datatype -> unless (Set.member e (datatypes s) || isDatatypeKey e) errMsg
4a7e911a2df39170655de6ea32debfcf7e376bfaslive Class -> unless (Set.member e (concepts s) || isThing e) errMsg
4a7e911a2df39170655de6ea32debfcf7e376bfaslive ObjectProperty -> unless (Set.member e $ objectProperties s) errMsg
4a7e911a2df39170655de6ea32debfcf7e376bfaslive DataProperty -> unless (Set.member e $ dataProperties s) errMsg
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars AnnotationProperty -> unless (Set.member e $ annotationRoles s) errMsg
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars _ -> return ()
b44815871de48215476ad1d4cc46d3f99da532a5erikabele-- | takes an iri and finds out what entities it belongs to
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larscorrectEntity :: Sign -> IRI -> [Entity]
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivecorrectEntity s iri =
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive [Entity AnnotationProperty iri | Set.member iri (annotationRoles s)] ++
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive [Entity Class iri | Set.member iri (concepts s)] ++
4a7e911a2df39170655de6ea32debfcf7e376bfaslive [Entity ObjectProperty iri | Set.member iri (objectProperties s)] ++
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive [Entity DataProperty iri | Set.member iri (dataProperties s)] ++
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive [Entity Datatype iri | Set.member iri (datatypes s)] ++
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive [Entity NamedIndividual iri | Set.member iri (individuals s)]
a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveobjPropToIRI :: ObjectPropertyExpression -> Individual
a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveobjPropToIRI opExp = case opExp of
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive ObjectProp u -> u
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive ObjectInverseOf objProp -> objPropToIRI objProp
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivemaybeObjProp :: Sign -> ObjectPropertyExpression
ef685e00a47967e27d89709461728a229d762172nd -> Maybe ObjectPropertyExpression
cd6092a248c4da4842a6e9b306d94e72708a68eendmaybeObjProp s op = if Set.member (objPropToIRI op) (objectProperties s)
ef685e00a47967e27d89709461728a229d762172nd then Just op else Nothing
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive{- | takes a list of object properties and discards the ones
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars which are not in the signature -}
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larssortObjDataList :: Sign -> [ObjectPropertyExpression]
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars -> [ObjectPropertyExpression]
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larssortObjDataList = mapMaybe . maybeObjProp
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larscheckObjPropList :: Sign -> a -> [ObjectPropertyExpression] -> Result a
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivecheckObjPropList s fb ol = do
b44815871de48215476ad1d4cc46d3f99da532a5erikabele let ls = map (\ u -> Set.member (objPropToIRI u)
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars (objectProperties s) ) ol
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive if elem False ls then
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive fail $ "Static analysis found that not all properties" ++
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive " in the following list are ObjectProperties\n\n"
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive else return fb
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivecheckDataPropList :: Sign -> a -> [DataPropertyExpression] -> Result a
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivecheckDataPropList s fb dl = do
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive let ls = map (\ u -> Set.member u (dataProperties s) ) dl
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive if elem False ls then
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive fail $ "Static analysis found that not all properties" ++
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive " in the following list are DataProperties\n\n"
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive else return fb
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- | checks if a DataRange is valid
ef685e00a47967e27d89709461728a229d762172ndcheckDataRange :: Sign -> DataRange -> Result DataRange
ef685e00a47967e27d89709461728a229d762172ndcheckDataRange s dr = case dr of
ef685e00a47967e27d89709461728a229d762172nd DataType dt _ -> checkEntity s (Entity Datatype dt) >> return dr
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive DataJunction _ drl -> mapM_ (checkDataRange s) drl >> return dr
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive DataComplementOf r -> checkDataRange s r
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars _ -> return dr
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars{- | converts ClassExpression to DataRanges because some
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars DataProperties may be parsed as ObjectProperties -}
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larsclassExpressionToDataRange :: Sign -> ClassExpression -> Result DataRange
f6d0bff0e95a7e6dd97f871582a1f091477c45c9larsclassExpressionToDataRange s ce = case ce of
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive Expression u -> checkEntity s (Entity Datatype u)
b44815871de48215476ad1d4cc46d3f99da532a5erikabele >> return (DataType u [])
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars ObjectJunction jt cel -> fmap (DataJunction jt)
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive $ mapM (classExpressionToDataRange s) cel
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive ObjectComplementOf c -> fmap DataComplementOf
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars $ classExpressionToDataRange s c
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars _ -> fail $ "cannot convert ClassExpression to DataRange\n"
f6d0bff0e95a7e6dd97f871582a1f091477c45c9lars ++ showDoc ce ""
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive{- | checks a ClassExpression and recursively converts the
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive (maybe inappropriately) parsed syntax to a one satisfying the signature -}
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivecheckClassExpression :: Sign -> ClassExpression -> Result ClassExpression
a27e9e05958bc51ea09edb8d8d862fe8b125313bslivecheckClassExpression s desc =
a27e9e05958bc51ea09edb8d8d862fe8b125313bslive let errMsg i = failMsg i desc
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive objErr i = errMsg $ Entity ObjectProperty i
17efa6b5344b7574597eec03f02ef28103e19265nd datErr i = errMsg $ Entity DataProperty i
d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele in case desc of
17efa6b5344b7574597eec03f02ef28103e19265nd Expression u ->
17efa6b5344b7574597eec03f02ef28103e19265nd if isThing u then
17efa6b5344b7574597eec03f02ef28103e19265nd return $ Expression u { namePrefix = "owl", iriType = Abbreviated }
ef685e00a47967e27d89709461728a229d762172nd else checkEntity s (Entity Class u) >> return desc
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx ObjectJunction a ds -> fmap (ObjectJunction a)
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx $ mapM (checkClassExpression s) ds
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx ObjectComplementOf d -> fmap ObjectComplementOf
17efa6b5344b7574597eec03f02ef28103e19265nd $ checkClassExpression s d
17efa6b5344b7574597eec03f02ef28103e19265nd ObjectOneOf _ -> return desc
17efa6b5344b7574597eec03f02ef28103e19265nd ObjectValuesFrom a opExpr d -> do
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx let iri = objPropToIRI opExpr
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx mbrOP = Set.member iri (objectProperties s)
17efa6b5344b7574597eec03f02ef28103e19265nd mbrDP = Set.member iri (dataProperties s)
b44815871de48215476ad1d4cc46d3f99da532a5erikabele if mbrOP then fmap (ObjectValuesFrom a opExpr) $ checkClassExpression s d
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx else if mbrDP then do
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx ndr <- classExpressionToDataRange s d
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx _ <- checkDataRange s ndr
17efa6b5344b7574597eec03f02ef28103e19265nd return $ DataValuesFrom a iri ndr
17efa6b5344b7574597eec03f02ef28103e19265nd else objErr iri
17efa6b5344b7574597eec03f02ef28103e19265nd ObjectHasSelf opExpr -> do
17efa6b5344b7574597eec03f02ef28103e19265nd let iri = objPropToIRI opExpr
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx if Set.member iri (objectProperties s) then return desc
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx else objErr iri
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx ObjectHasValue opExpr _ -> do
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx let iri = objPropToIRI opExpr
17efa6b5344b7574597eec03f02ef28103e19265nd if Set.member iri (objectProperties s) then return desc else objErr iri
cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx ObjectCardinality (Cardinality a b opExpr md) -> do
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai let iri = objPropToIRI opExpr
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai let mbrOP = Set.member iri (objectProperties s)
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai let mbrDP = Set.member iri (dataProperties s)
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai Nothing -> if mbrOP then return desc else objErr iri
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai if mbrOP then do
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai n <- checkClassExpression s d
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai return $ ObjectCardinality (Cardinality a b opExpr (Just n))
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai dr <- classExpressionToDataRange s d
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai _ <- checkDataRange s dr
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai if mbrDP then return $ DataCardinality
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai (Cardinality a b iri (Just dr))
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai else datErr iri
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai DataValuesFrom _ dExp r -> do
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai _ <- checkDataRange s r
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai if Set.member dExp (dataProperties s) then return desc else datErr dExp
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai DataHasValue dExp _ ->
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai if Set.member dExp (dataProperties s) then return desc else datErr dExp
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai DataCardinality (Cardinality _ _ dExp mr) ->
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai if Set.member dExp (dataProperties s) then case mr of
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai Nothing -> return desc
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai Just d -> checkDataRange s d >> return desc
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawai else datErr dExp
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawaicheckFactList :: Sign -> ListFrameBit -> [Fact] -> Result ListFrameBit
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawaicheckFactList s fb fl = mapM_ (checkFact s fb) fl >> return fb
86bb9693d63dfc1be14519a5b444467e4b0cdaf8kawaicheckFact :: Sign -> ListFrameBit -> Fact -> Result ListFrameBit
17efa6b5344b7574597eec03f02ef28103e19265ndcheckFact s fb f = case f of
17efa6b5344b7574597eec03f02ef28103e19265nd ObjectPropertyFact _ op _ ->
17efa6b5344b7574597eec03f02ef28103e19265nd if Set.member (objPropToIRI op) (objectProperties s) then return fb
17efa6b5344b7574597eec03f02ef28103e19265nd else fail "Static analysis. ObjectPropertyFact failed"
17efa6b5344b7574597eec03f02ef28103e19265nd DataPropertyFact _ dp _ ->
17efa6b5344b7574597eec03f02ef28103e19265nd if Set.member dp (dataProperties s) then return fb
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick else fail "Static analysis. DataProperty fact failed"
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickcheckHasKeyAll :: Sign -> AnnFrameBit -> Result AnnFrameBit
17efa6b5344b7574597eec03f02ef28103e19265ndcheckHasKeyAll s k = case k of
17efa6b5344b7574597eec03f02ef28103e19265nd ClassHasKey ol dl -> do
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick let l1 = map (\ u -> Set.member (objPropToIRI u) (objectProperties s) ) ol
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick l2 = map (`Set.member` dataProperties s) dl
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick if elem False (l1 ++ l2) then
17efa6b5344b7574597eec03f02ef28103e19265nd fail "Static analysis. Keys failed, undeclared Data or Object Properties"
17efa6b5344b7574597eec03f02ef28103e19265nd else return k
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick _ -> return k
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick-- | sorts the data and object properties
17efa6b5344b7574597eec03f02ef28103e19265ndcheckHasKey :: Sign -> AnnFrameBit -> Result AnnFrameBit
17efa6b5344b7574597eec03f02ef28103e19265ndcheckHasKey s k = case k of
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick ClassHasKey ol dl -> do
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick let sl = sortObjDataList s ol
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick let k2 = ClassHasKey sl (map objPropToIRI (ol \\ sl) ++ dl)
b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick checkHasKeyAll s k2
17efa6b5344b7574597eec03f02ef28103e19265nd _ -> return k
17efa6b5344b7574597eec03f02ef28103e19265ndcheckListBit :: Sign -> Maybe Relation -> ListFrameBit -> Result ListFrameBit
d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabelecheckListBit s r fb = case fb of
17efa6b5344b7574597eec03f02ef28103e19265nd AnnotationBit anl -> case r of
17efa6b5344b7574597eec03f02ef28103e19265nd Just (DRRelation _) -> return fb
17efa6b5344b7574597eec03f02ef28103e19265nd _ -> mapM_ (checkEntity s . Entity AnnotationProperty
ef685e00a47967e27d89709461728a229d762172nd . snd) anl >> return fb
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive ExpressionBit anl -> do
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive n <- mapM (checkClassExpression s . snd) anl
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive return $ ExpressionBit $ zip (map fst anl) n
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive ObjectBit anl -> do
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive let ol = map snd anl
17efa6b5344b7574597eec03f02ef28103e19265nd let sorted = sortObjDataList s ol
b44815871de48215476ad1d4cc46d3f99da532a5erikabele if null sorted then do
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive let dpl = map objPropToIRI ol
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive let nb = DataBit $ zip (map fst anl) dpl
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive checkDataPropList s nb dpl
17efa6b5344b7574597eec03f02ef28103e19265nd if length sorted == length ol then return fb
17efa6b5344b7574597eec03f02ef28103e19265nd else fail $ "Static analysis found that there are" ++
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive " multiple types of properties in\n\n" ++
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive show sorted ++ show
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive (map objPropToIRI (ol \\ sorted))
222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive ObjectCharacteristics _ -> return fb
17efa6b5344b7574597eec03f02ef28103e19265nd DataBit anl -> checkDataPropList s fb $ map snd anl
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele DataPropRange anl -> mapM_ (checkDataRange s . snd) anl >> return fb
17efa6b5344b7574597eec03f02ef28103e19265nd IndividualFacts anl -> checkFactList s fb $ map snd anl
17efa6b5344b7574597eec03f02ef28103e19265nd IndividualSameOrDifferent _ -> return fb
17efa6b5344b7574597eec03f02ef28103e19265ndcheckAnnBit :: Sign -> AnnFrameBit -> Result AnnFrameBit
17efa6b5344b7574597eec03f02ef28103e19265ndcheckAnnBit s fb = case fb of
17efa6b5344b7574597eec03f02ef28103e19265nd DatatypeBit dr -> checkDataRange s dr >> return fb
ef685e00a47967e27d89709461728a229d762172nd ClassDisjointUnion cel -> fmap ClassDisjointUnion
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele $ mapM (checkClassExpression s) cel
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele ClassHasKey _ _ -> checkHasKey s fb
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele ObjectSubPropertyChain ol -> checkObjPropList s fb ol
17efa6b5344b7574597eec03f02ef28103e19265nd _ -> return fb
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelecheckAssertion :: Sign -> IRI -> Annotations -> Result [Axiom]
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelecheckAssertion s iri ans = do
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele let entList = correctEntity s iri
17efa6b5344b7574597eec03f02ef28103e19265nd ab = AnnFrameBit ans $ AnnotationFrameBit Assertion
b44815871de48215476ad1d4cc46d3f99da532a5erikabele if null entList then
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele let misc = Misc [Annotation [] iri $ AnnValue iri]
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele in return [PlainAxiom misc ab]
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele else return $ map (\ x -> PlainAxiom (SimpleEntity x) ab) entList
17efa6b5344b7574597eec03f02ef28103e19265nd-- | corrects the axiom according to the signature
17efa6b5344b7574597eec03f02ef28103e19265ndcheckAxiom :: Sign -> Axiom -> Result [Axiom]
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelecheckAxiom s ax@(PlainAxiom ext fb) = case fb of
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele ListFrameBit mr lfb -> do
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele next <- checkExtended s ext
1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele nfb <- fmap (ListFrameBit mr) $ checkListBit s mr lfb
17efa6b5344b7574597eec03f02ef28103e19265nd return [PlainAxiom next nfb]
81622596373177e079337e956f7a5800895443b3erikabele ab@(AnnFrameBit ans afb) -> case afb of
81622596373177e079337e956f7a5800895443b3erikabele AnnotationFrameBit ty -> case ty of
81622596373177e079337e956f7a5800895443b3erikabele Assertion -> case ext of
81622596373177e079337e956f7a5800895443b3erikabele Misc [Annotation _ iri _] -> checkAssertion s iri ans
ef685e00a47967e27d89709461728a229d762172nd SimpleEntity (Entity _ iri) -> checkAssertion s iri ans
ef685e00a47967e27d89709461728a229d762172nd _ -> do next <- checkExtended s ext
ef685e00a47967e27d89709461728a229d762172nd return [PlainAxiom next ab]
81622596373177e079337e956f7a5800895443b3erikabele Declaration -> return [ax]
81622596373177e079337e956f7a5800895443b3erikabele next <- checkExtended s ext
81622596373177e079337e956f7a5800895443b3erikabele nfb <- fmap (AnnFrameBit ans) $ checkAnnBit s afb
81622596373177e079337e956f7a5800895443b3erikabele return [PlainAxiom next nfb]
81622596373177e079337e956f7a5800895443b3erikabelecheckExtended :: Sign -> Extended -> Result Extended
81622596373177e079337e956f7a5800895443b3erikabelecheckExtended s e = case e of
81622596373177e079337e956f7a5800895443b3erikabele ClassEntity ce -> fmap ClassEntity $ checkClassExpression s ce
81622596373177e079337e956f7a5800895443b3erikabele ObjectEntity oe -> case oe of
81622596373177e079337e956f7a5800895443b3erikabele ObjectInverseOf op -> let i = objPropToIRI op in
81622596373177e079337e956f7a5800895443b3erikabele if Set.member i (objectProperties s)
81622596373177e079337e956f7a5800895443b3erikabele then return e else mkError "unknown object property" i
81622596373177e079337e956f7a5800895443b3erikabele _ -> return e
81622596373177e079337e956f7a5800895443b3erikabele _ -> return e
81622596373177e079337e956f7a5800895443b3erikabele-- | checks a frame and applies desired changes
81622596373177e079337e956f7a5800895443b3erikabelecheckFrame :: Sign -> Frame -> Result [Frame]
81622596373177e079337e956f7a5800895443b3erikabelecheckFrame s (Frame eith fbl) = fmap (map axToFrame . concat)
81622596373177e079337e956f7a5800895443b3erikabele $ mapM (checkAxiom s . PlainAxiom eith) fbl
81622596373177e079337e956f7a5800895443b3erikabelecorrectFrames :: Sign -> [Frame] -> Result [Frame]
ef685e00a47967e27d89709461728a229d762172ndcorrectFrames s fl = fmap concat $ mapM (checkFrame s) fl
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelegetEntityFromFrame :: Frame -> State Sign ()
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelegetEntityFromFrame f = case f of
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele Frame (SimpleEntity e) _ -> addEntity e
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele Frame (ClassEntity (Expression e)) _ -> addEntity $ Entity Class e
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele Frame (ObjectEntity (ObjectProp e)) _ ->
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele addEntity $ Entity ObjectProperty e
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele _ -> return ()
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele-- | collects all entites from the frames
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelecreateSign :: [Frame] -> State Sign ()
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelecreateSign f = do
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele pm <- gets prefixMap
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele mapM_ (getEntityFromFrame . function Expand pm) f
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele-- | corrects the axioms according to the signature
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelecreateAxioms :: Sign -> [Frame] -> Result ([Named Axiom], [Frame])
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelecreateAxioms s fl = do
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele cf <- correctFrames s $ map (function Expand $ prefixMap s) fl
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele return (map anaAxiom $ concatMap getAxioms cf, cf)
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelemodifyOntologyDocument :: OntologyDocument -> [Frame] -> OntologyDocument
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelemodifyOntologyDocument
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele OntologyDocument {ontology = mo, prefixDeclaration = pd} fl =
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele OntologyDocument { ontology = mo {ontFrames = fl},
f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele prefixDeclaration = pd}
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki-- | static analysis of ontology with incoming sign.
17efa6b5344b7574597eec03f02ef28103e19265ndbasicOWL2Analysis ::
17efa6b5344b7574597eec03f02ef28103e19265nd (OntologyDocument, Sign, GlobalAnnos) ->
17efa6b5344b7574597eec03f02ef28103e19265nd Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom])
17efa6b5344b7574597eec03f02ef28103e19265ndbasicOWL2Analysis (odoc, inSign, _) = do
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki let pd = prefixDeclaration odoc
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki fs = ontFrames $ ontology odoc
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki let syms = Set.difference (symOf accSign) $ symOf inSign
17efa6b5344b7574597eec03f02ef28103e19265nd accSign = execState
17efa6b5344b7574597eec03f02ef28103e19265nd (createSign fs)
17efa6b5344b7574597eec03f02ef28103e19265nd inSign {prefixMap = pd}
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki (axl, nfl) <- createAxioms accSign fs
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki let newdoc = modifyOntologyDocument odoc nfl
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki return (newdoc , ExtSign accSign syms, axl)
17efa6b5344b7574597eec03f02ef28103e19265nd-- | adding annotations for theorems
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshikianaAxiom :: Axiom -> Named Axiom
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshikianaAxiom ax = findImplied ax $ makeNamed "" ax
17efa6b5344b7574597eec03f02ef28103e19265ndfindImplied :: Axiom -> Named Axiom -> Named Axiom
17efa6b5344b7574597eec03f02ef28103e19265ndfindImplied ax sent =
17efa6b5344b7574597eec03f02ef28103e19265nd if prove ax then sent
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki { isAxiom = False
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki , isDef = False
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki , wasTheorem = False }
4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki else sent { isAxiom = True }