StaticAnalysis.hs revision e5636f167d8113960d320407cbbd7cd3580241d4
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederModule : $Header$
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederDescription : Static Analysis for DL
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2008
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederLicense : similar to LGPL, see Hets/LICENSE.txt or LIZENZ.txt
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederMaintainer : luecke@informatik.uni-bremen.de
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederStability : experimental
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederPortability : non-portable (imports Logic.Logic)
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederThe static analysis of DL basic specs is implemented here.
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ( basic_DL_analysis
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , sign2basic_spec
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Data.Set as Set
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Common.Lib.Rel as Rel()
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederbasic_DL_analysis :: (DLBasic, Sign,GlobalAnnos) ->
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Result (DLBasic, ExtSign Sign DLSymbol,[Named DLBasicItem])
67869d63d1725c79e4c07b51acd466a31932b275Christian Maederbasic_DL_analysis (spec, sig, _) =
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sens = case spec of
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder DLBasic x -> x
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder [cCls, cObjProps, cDtProps, cIndi, cMIndi] = splitSentences sens
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder oCls = uniteClasses cCls
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder oObjProps = uniteObjProps cObjProps
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder oDtProps = uniteDataProps cDtProps
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder oIndi = uniteIndividuals (cIndi ++ splitUpMIndis cMIndi)
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder cls = getClasses $ map item $ oCls
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder dtPp = getDataProps (map item oDtProps) (cls)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder obPp = getObjProps (map item oObjProps) (cls)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ind = getIndivs (map item oIndi) (cls)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder outSig = emptyDLSig
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder classes = cls
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , dataProps = dtPp
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder , objectProps = obPp
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder , individuals = ind
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder outImpSig <- addImplicitDeclarations outSig (oCls ++ oObjProps ++ oDtProps ++ oIndi)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder case Set.intersection (Set.map nameD $ dataProps outImpSig) (Set.map nameO $ objectProps outImpSig) == Set.empty of
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return (spec, ExtSign{
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder plainSign = outImpSig `uniteSigOK` sig
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ,nonImportedSymbols = generateSignSymbols outImpSig
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , map (makeNamedSen) $ concat [oCls, oObjProps, oDtProps, oIndi])
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let doubles = Set.toList $ Set.intersection (Set.map nameD $ dataProps outImpSig) (Set.map nameO $ objectProps outImpSig)
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder fatal_error ("Sets of Object and Data Properties are not disjoint: " ++ show doubles) nullRange
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder-- | Generation of symbols out of a signature
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedergenerateSignSymbols :: Sign -> Set.Set DLSymbol
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedergenerateSignSymbols inSig =
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder cls = Set.map (\x -> DLSymbol
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , symType = ClassSym
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder }) $ classes inSig
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder dtP = Set.map (\x -> DLSymbol
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder , symType = DataProp
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder }) $ Set.map nameD $ dataProps inSig
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder obP = Set.map (\x -> DLSymbol
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , symType = ObjProp
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder }) $ Set.map nameO $ objectProps inSig
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder inD = Set.map (\x -> DLSymbol
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , symType = Indiv
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder }) $ Set.map iid $ individuals inSig
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder cls `Set.union` dtP `Set.union` obP `Set.union` inD
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederisLegalSuperProperty :: Id -> DLPropertyComp -> Bool
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederisLegalSuperProperty cId cProps =
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder case cProps of
False -> fatal_error ((show b) ++ " does not fulfill the SROIQ restrictions for " ++ (show nt)) nullRange
False -> fatal_error ((show b) ++ " does not fulfill the SROIQ restrictions for " ++ (show nt)) nullRange
case Set.member (QualDataProp oP) (dataProps inSig) of
case Set.member (QualDataProp oP) (dataProps inSig) of
case Set.member y dlDefData of
uniteSig emptyDLSig{objectProps=Set.singleton $ QualObjProp r} recSig
uniteSig emptyDLSig{dataProps=Set.singleton $ QualDataProp r} recSig
uniteSig emptyDLSig{classes=Set.singleton r} recSig
uniteSig emptyDLSig{individuals=Set.singleton $ QualIndiv r [topSort]} recSig
idSet = Set.fromList idDs
dom = bucketDomRn $ map fromJust $ Set.toList $ Set.fromList $ filter (/= Nothing) $ map (\x -> case item x of
rn = bucketDomRn $ map fromJust $ Set.toList $ Set.fromList $ filter (/=Nothing) $ map (\x -> case item x of
(x:xs) -> case length (map fromJust (x:xs)) == length (filter (== DLFunctional) $ map fromJust (x:xs)) of
_ -> error ("Wrong characteristics " ++ (concatComma $ map show (filter (/=DLFunctional) $ map fromJust (x:xs)))
dom = bucketDomRn $ map fromJust $ Set.toList $ Set.fromList $ filter (/= Nothing) $ map (\x -> case item x of
rn = bucketDomRn $ map fromJust $ Set.toList $ Set.fromList $ filter (/=Nothing) $ map (\x -> case item x of
DLDataProperty _ _ _ _ (Just DLInvFuntional) _ _-> error "InvFunctional not available for data properties"
DLDataProperty _ _ _ _ (Just DLTransitive) _ _-> error "Transitive not available for data properties"
getClasses :: [DLBasicItem] -> Set.Set Id
bucketIndiv $ map (\z -> case (z `Set.member` cls) of
examineDataProp :: DLBasicItem -> Set.Set Id -> QualDataProp
examineObjProp :: DLBasicItem -> Set.Set Id -> QualObjProp