1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- |

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederModule : $Header$

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederCopyright : Felix Gabriel Mance

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederMaintainer : f.mance@jacobs-university.de

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederStability : provisional

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederPortability : portable

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederContains : static analysis for OWL 2

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedermodule OWL2.StaticAnalysis where

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport OWL2.Sign

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport OWL2.AS

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport OWL2.MS

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maederimport OWL2.Theorem

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport qualified Data.Map as Map

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederimport qualified Data.Set as Set

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Data.List

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Data.Maybe

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.AS_Annotation

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Result

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederimport Common.GlobalAnnotations

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.ExtSign

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Lib.State

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport Control.Monad

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-- | Error messages for static analysis

64e1905404e5135e98a26d2ab4150b6764956576Christian MaederfailMsg :: Maybe Entity -> String -> String

64e1905404e5135e98a26d2ab4150b6764956576Christian MaederfailMsg ent s = case ent of

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder Just (Entity ty e) -> "Static analysis cannot find " ++ showEntityType ty

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ++ " " ++ showQN e ++ s

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder Nothing -> s

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaedergetObjRoleFromExpression :: ObjectPropertyExpression -> IndividualRoleIRI

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedergetObjRoleFromExpression opExp =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder case opExp of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ObjectProp u -> u

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ObjectInverseOf objProp -> getObjRoleFromExpression objProp

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedergetObjRoleFromSubExpression :: SubObjectPropertyExpression

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> [IndividualRoleIRI]

64e1905404e5135e98a26d2ab4150b6764956576Christian MaedergetObjRoleFromSubExpression sopExp =

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder case sopExp of

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder OPExpression opExp -> [getObjRoleFromExpression opExp]

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder SubObjectPropertyChain expList ->

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder map getObjRoleFromExpression expList

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

65dce48b81f69e11a36bf1051314a845299446e1Christian MaedersortObjData :: Sign -> ObjectPropertyExpression

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder -> Maybe ObjectPropertyExpression

64e1905404e5135e98a26d2ab4150b6764956576Christian MaedersortObjData s op =

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder let p = getObjRoleFromExpression op in

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder if Set.member p (objectProperties s) then Just op

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else Nothing

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian MaedersortObjDataList :: Sign -> [ObjectPropertyExpression]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> [ObjectPropertyExpression]

64e1905404e5135e98a26d2ab4150b6764956576Christian MaedersortObjDataList s = mapMaybe $ sortObjData s

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian MaedermodEntity :: (IRI -> Set.Set IRI -> Set.Set IRI) -> Entity -> State Sign ()

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian MaedermodEntity f (Entity ty u) = do

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder s <- get

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let chg = f u

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder put $ case ty of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Datatype -> s { datatypes = chg $ datatypes s }

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Class -> s { concepts = chg $ concepts s }

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder ObjectProperty -> s { objectProperties = chg $ objectProperties s }

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder DataProperty -> s { dataProperties = chg $ dataProperties s }

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder NamedIndividual -> s { individuals = chg $ individuals s }

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder AnnotationProperty -> s {annotationRoles = chg $ annotationRoles s}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | adding entities to the signature

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederaddEntity :: Entity -> State Sign ()

67869d63d1725c79e4c07b51acd466a31932b275Christian MaederaddEntity = modEntity Set.insert

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-- | adding annotations for theorems

64e1905404e5135e98a26d2ab4150b6764956576Christian MaederanaAxiom :: Axiom -> Named Axiom

64e1905404e5135e98a26d2ab4150b6764956576Christian MaederanaAxiom x = findImplied x $ makeNamed "" x

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-- | checks if an entity is in the signature

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedercheckEntity :: Sign -> a -> Entity -> Result a

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedercheckEntity s a ent = let Entity ty e = ent in case ty of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Datatype -> if Set.member e (datatypes s) then return a

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else fail $ failMsg (Just ent) ""

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder Class -> if Set.member e (concepts s) then return a

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else fail $ failMsg (Just ent) ""

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ObjectProperty -> if Set.member e (objectProperties s) then return a

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else fail $ failMsg (Just ent) ""

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder DataProperty -> if Set.member e (dataProperties s) then return a

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else fail $ failMsg (Just ent) ""

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder NamedIndividual -> if Set.member e (individuals s) then return a

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder else fail $ failMsg (Just ent) ""

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder AnnotationProperty -> if Set.member e (annotationRoles s) then return a

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else fail $ failMsg (Just ent) ""

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | checks if a DataRange is valid

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedercheckDataRange :: Sign -> DataRange -> Result DataRange

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedercheckDataRange s dr =

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder case dr of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder DataType dt _ -> do

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder checkEntity s dr (Entity Datatype dt)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return dr

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder DataJunction _ drl -> do

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder mapM_ (checkDataRange s) drl

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return dr

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder DataComplementOf r -> checkDataRange s r

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder _ -> return dr

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder{- | converts ClassExpression to DataRanges because some

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder DataProperties may be parsed as ObjectProperties -}

ecf557c0b4f953106755a239da2c0b168064d3f4Christian MaederclassExpressionToDataRange :: Sign -> ClassExpression -> Result DataRange

ecf557c0b4f953106755a239da2c0b168064d3f4Christian MaederclassExpressionToDataRange s ce = case ce of

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder Expression u -> do

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder checkEntity s ce (Entity Datatype u)

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder return $ DataType u []

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder ObjectJunction jt cel -> do

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder nrl <- mapM (classExpressionToDataRange s) cel

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder return $ DataJunction jt nrl

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder ObjectComplementOf c -> do

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder nr <- classExpressionToDataRange s c

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder return $ DataComplementOf nr

65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder _ -> fail $ failMsg Nothing

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder "Static analysis cannot correct so parsed ClassExpression\n\n"

65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder ++ show ce ++ "\n\nto a DataRange"

65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder{- | checks a ClassExpression and recursively converts the

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder (maybe inappropriately) parsed syntax to a one satisfying the signature -}

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian MaedercheckClassExpression :: Sign -> ClassExpression -> Result ClassExpression

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian MaedercheckClassExpression s desc = case desc of

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder Expression u -> case u of

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder QN _ "Thing" _ _ -> return $ Expression $ QN "owl" "Thing" False ""

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder QN _ "Nothing" _ _ -> return $ Expression $ QN "owl" "Nothing" False ""

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder _ -> checkEntity s desc (Entity Class u)

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ObjectJunction a ds -> do

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder nl <- mapM (checkClassExpression s) ds

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return $ ObjectJunction a nl

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ObjectComplementOf d -> do

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder n <- checkClassExpression s d

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return $ ObjectComplementOf n

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ObjectOneOf is -> do

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder mapM_ (checkEntity s desc . Entity NamedIndividual) is

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return desc

ObjectValuesFrom a opExpr d -> do

let iri = getObjRoleFromExpression opExpr

x = Set.member iri (objectProperties s)

z = Set.member iri (dataProperties s)

if x then do

n <- checkClassExpression s d

return $ ObjectValuesFrom a opExpr n

else if z then do

ndr <- classExpressionToDataRange s d

checkDataRange s ndr

return $ DataValuesFrom a iri [] ndr

else fail $ failMsg (Just $ Entity ObjectProperty iri)

" in the following ClassExpression\n\n" ++ show desc

ObjectHasSelf opExpr -> do

let iri = getObjRoleFromExpression opExpr

if Set.member iri (objectProperties s) then return desc

else fail $ failMsg (Just $ Entity ObjectProperty iri)

" in the following ClassExpression\n\n" ++ show desc

ObjectHasValue opExpr i -> do

let iri = getObjRoleFromExpression opExpr

x = Set.member iri (objectProperties s)

if x then do

checkEntity s desc (Entity NamedIndividual i)

return desc

else fail $ failMsg (Just $ Entity ObjectProperty iri)

" in the following ClassExpression\n\n" ++ show desc

ObjectCardinality (Cardinality a b opExpr md) -> do

let iri = getObjRoleFromExpression opExpr

let x = Set.member iri (objectProperties s)

let z = Set.member iri (dataProperties s)

case md of

Nothing ->

if x then return desc

else fail $ failMsg (Just $ Entity ObjectProperty iri)

" in the following ClassExpression\n\n" ++ show desc

Just d ->

if x then do

n <- checkClassExpression s d

return $ ObjectCardinality (Cardinality a b opExpr (Just n))

else do

dr <- classExpressionToDataRange s d

checkDataRange s dr

if z then return $ DataCardinality (Cardinality a b iri (Just dr))

else fail $ failMsg (Just $ Entity DataProperty iri)

" in the following ClassExpression\n\n" ++ show desc

DataValuesFrom _ dExp ds r -> do

checkDataRange s r

let x = Set.isSubsetOf (Set.fromList (dExp : ds)) (dataProperties s)

if x then return desc

else fail $ failMsg (Just $ Entity DataProperty dExp)

" in the following ClassExpression\n\n" ++ show desc

DataHasValue dExp _ -> do

let x = Set.member dExp (dataProperties s)

if x then return desc

else fail $ failMsg (Just $ Entity DataProperty dExp)

" in the following ClassExpression\n\n" ++ show desc

DataCardinality (Cardinality _ _ dExp mr) -> do

let x = Set.member dExp (dataProperties s)

if x then

case mr of

Nothing -> return desc

Just d -> do

checkDataRange s d

return desc

else fail $ failMsg (Just $ Entity DataProperty dExp)

" in the following ClassExpression\n\n" ++ show desc

-- corrects the frame bits according to the signature

checkAnnBit :: Sign -> AnnFrameBit -> Result AnnFrameBit

checkAnnBit s fb = case fb of

DatatypeBit dr -> do

checkDataRange s dr

return fb

ClassDisjointUnion cel -> do

n <- mapM (checkClassExpression s) cel

return $ ClassDisjointUnion n

ClassHasKey _ _ -> checkHasKey s fb

ObjectSubPropertyChain ol -> checkObjPropList s fb ol

_ -> return fb

checkListBit :: Sign -> (Maybe Relation) -> ListFrameBit -> Result ListFrameBit

checkListBit s r fb = case fb of

AnnotationBit anl -> case r of

Just (DRRelation _) -> return fb

_ -> do

let apl = map snd anl

mapM_ (checkEntity s fb . Entity AnnotationProperty) apl

return fb

ExpressionBit anl -> do

let ans = map fst anl

let ce = map snd anl

n <- mapM (checkClassExpression s) ce

return $ ExpressionBit $ zip ans n

ObjectBit anl -> do

let ans = map fst anl

let ol = map snd anl

--checkObjPropList s fb ol

let x = sortObjDataList s ol

if null x then do

let dpl = map getObjRoleFromExpression ol

let nb = DataBit $ zip ans dpl

checkDataPropList s nb dpl

else

if length x == length ol then return fb

else fail $ "Static analysis found that there are" ++

" multiple types of properties in\n\n" ++

show x ++ show

(map getObjRoleFromExpression (ol \\ x))

ObjectCharacteristics _ -> return fb

DataBit anl -> do

let dl = map snd anl

checkDataPropList s fb dl

DataPropRange anl -> do

let dr = map snd anl

mapM_ (checkDataRange s) dr

return fb

IndividualFacts anl -> do

let f = map snd anl

checkFactList s fb f

IndividualSameOrDifferent anl -> do

let i = map snd anl

mapM_ (checkEntity s fb . Entity NamedIndividual) i

return fb

checkBit :: Sign -> FrameBit -> Result FrameBit

checkBit s fb = case fb of

ListFrameBit mr lfb -> do

nf <- checkListBit s mr lfb

return $ ListFrameBit mr nf

AnnFrameBit ans afb -> do

nf <- checkAnnBit s afb

return $ AnnFrameBit ans nf

checkFactList :: Sign -> ListFrameBit -> [Fact] -> Result ListFrameBit

checkFactList s fb fl = do

mapM_ (checkFact s fb) fl

return fb

checkFact :: Sign -> ListFrameBit -> Fact -> Result ListFrameBit

checkFact s fb f =

case f of

ObjectPropertyFact _ op _ ->

if Set.member (getObjRoleFromExpression op) (objectProperties s) then

return fb

else fail "Static analysis. ObjectPropertyFact failed"

DataPropertyFact _ dp _ ->

if Set.member dp (dataProperties s) then return fb

else fail "Static analysis. DataProperty fact failed"

checkObjPropList :: Sign -> a -> [ObjectPropertyExpression] -> Result a

checkObjPropList s fb ol = do

let x = map (\ u -> Set.member (getObjRoleFromExpression u)

(objectProperties s) ) ol

if elem False x then

fail $ "Static analysis found that not all properties" ++

" in the following list are ObjectProperties\n\n"

++ show ol

else return fb

checkDataPropList :: Sign -> a -> [DataPropertyExpression] -> Result a

checkDataPropList s fb dl = do

let x = map (\ u -> Set.member u (dataProperties s) ) dl

if elem False x then

fail $ "Static analysis found that not all properties" ++

" in the following list are DataProperties\n\n"

++ show dl

else return fb

checkHasKeyAll :: Sign -> AnnFrameBit -> Result AnnFrameBit

checkHasKeyAll s k = case k of

ClassHasKey ol dl -> do

let x = map (\ u -> Set.member (getObjRoleFromExpression u)

(objectProperties s) ) ol

y = map (\ u -> Set.member u (dataProperties s) ) dl

if elem False (x ++ y) then

fail "Static analysis. Keys failed, undeclared Data or Object Properties"

else return $ ClassHasKey ol dl

_ -> return k

checkHasKey :: Sign -> AnnFrameBit -> Result AnnFrameBit

checkHasKey s k = case k of

ClassHasKey ol _ -> do

let x = sortObjDataList s ol

let k2 = ClassHasKey x (map getObjRoleFromExpression (ol \\ x))

checkHasKeyAll s k2

_ -> return k

-- | checks a frame and applies desired changes

checkFrame :: Sign -> Frame -> Result Frame

checkFrame s (Frame eith fbl) = do

nl <- mapM (checkBit s) fbl

return $ Frame eith nl

correctFrames :: Sign -> [Frame] -> Result [Frame]

correctFrames s = mapM (checkFrame s)

getEntityFromFrame :: Frame -> State Sign ()

getEntityFromFrame f = case f of

Frame (SimpleEntity e) _ -> addEntity e

_ -> return ()

createSign :: [Frame] -> State Sign ()

createSign = mapM_ getEntityFromFrame

createAxioms :: Sign -> [Frame] -> Result ([Named Axiom], [Frame])

createAxioms s fl = do

x <- correctFrames s fl

return (map anaAxiom $ concatMap getAxioms x, x)

modifyOntologyDocument :: OntologyDocument -> [Frame] -> OntologyDocument

modifyOntologyDocument

OntologyDocument {mOntology = mo, prefixDeclaration = pd} fl =

OntologyDocument { mOntology = mo {ontologyFrame = fl},

prefixDeclaration = pd}

-- | static analysis of ontology with incoming sign.

basicOWL2Analysis ::

(OntologyDocument, Sign, GlobalAnnos) ->

Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom])

basicOWL2Analysis (odoc, inSign, _) = do

let ns = prefixDeclaration odoc

fs = ontologyFrame $ mOntology odoc

integNamespace <- integrateNamespaces (prefixMap inSign) ns

let syms = Set.difference (symOf accSign) $ symOf inSign

accSign = execState

(createSign fs)

inSign {prefixMap = integNamespace}

(axl, nfl) <- createAxioms accSign fs

let newdoc = modifyOntologyDocument odoc nfl

return (newdoc , ExtSign accSign syms, axl)

testAndInteg :: PrefixMap -> (String, String) -> Result PrefixMap

testAndInteg old (pre, ouri) =

case Map.lookup pre old of

Just iri -> if ouri == iri then return old else

fail $ "Static analysis found a prefix clash " ++ pre

Nothing -> return $ Map.insert pre ouri old

uniteSign :: Sign -> Sign -> Result Sign

uniteSign s1 s2 = do

pm <- integrateNamespaces (prefixMap s1) (prefixMap s2)

return $ (addSign s1 s2) {prefixMap = pm}

integrateNamespaces :: PrefixMap -> PrefixMap

-> Result PrefixMap

integrateNamespaces oldNsMap testNsMap =

foldM testAndInteg oldNsMap (Map.toList testNsMap)

findImplied :: Axiom -> Named Axiom -> Named Axiom

findImplied ax sent =

if isToProve ax then sent

{ isAxiom = False

, isDef = False

, wasTheorem = False }

else sent { isAxiom = True }