6133N/A{- |

6133N/AModule : $Header$

6133N/ACopyright : Heng Jiang, Uni Bremen 2004-2006

6133N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

6133N/A

6133N/AMaintainer : jiang@tzi.de

6133N/AStability : provisional

6133N/APortability : non-portable (inports Logic.Logic)

6133N/A

6133N/Aanalyse owl files

6133N/A-}

6133N/A

6133N/Amodule OWL_DL.OWLAnalysis where

6133N/A

6133N/Aimport OWL_DL.AS

6133N/Aimport OWL_DL.Namespace

6133N/Aimport OWL_DL.Logic_OWL_DL

6133N/Aimport OWL_DL.StaticAna

6133N/Aimport OWL_DL.Sign

6133N/Aimport OWL_DL.StructureAna

6133N/A

6133N/Aimport Common.ATerm.ReadWrite

6133N/Aimport Common.ATerm.Unshared

6133N/Aimport System(system)

6133N/Aimport System.Exit

6133N/Aimport System.Environment(getEnv)

6133N/Aimport qualified Common.Lib.Map as Map

6133N/Aimport qualified List as List

6133N/Aimport Data.Graph.Inductive.Graph

6133N/Aimport Static.DevGraph

6147N/Aimport Common.GlobalAnnotations

6147N/Aimport Common.Result

6147N/Aimport Common.AS_Annotation hiding (isAxiom,isDef)

6147N/Aimport Syntax.AS_Library

6147N/Aimport Driver.Options

6147N/Aimport Common.Id

6133N/Aimport Logic.Logic

6147N/Aimport Logic.Grothendieck

6147N/Aimport Logic.Prover

6147N/Aimport Data.Graph.Inductive.Query.DFS

6147N/Aimport Data.Graph.Inductive.Query.BFS

6147N/Aimport Maybe(fromJust)

6147N/Aimport List

6133N/A

6147N/A-- | call for owl parser (env. variable $HETS_OWL_PARSER muss be defined)

6147N/AparseOWL :: FilePath -- ^ local filepath or uri

6147N/A -> IO OntologyMap -- ^ map: uri -> Ontology

6133N/AparseOWL filename =

6147N/A do

6147N/A pwd <- getEnv "PWD"

6147N/A if null filename

6147N/A then

6133N/A error "empty file name!"

6133N/A else if checkUri $ filename

6133N/A then

6133N/A do exitCode <-

system ("$HETS_OWL_PARSER/owl_parser " ++ filename)

-- system ("./OWL_DL/owl_parser " ++ filename)

run exitCode

else if (head filename) == '/'

then

do exitCode <-

system ("$HETS_OWL_PARSER/owl_parser file://"

++ filename)

-- system ("./OWL_DL/owl_parser file://"

-- ++ filename)

run exitCode

else do exitCode <-

system ("$HETS_OWL_PARSER/owl_parser file://"

++ pwd ++ "/" ++ filename)

-- system ("./OWL_DL/owl_parser file://"

-- ++ pwd ++ "/" ++ filename)

run exitCode

where run :: ExitCode -> IO OntologyMap

run exitCode

| exitCode == ExitSuccess =

parseProc "./OWL_DL/output.term"

| otherwise = error ("process stop! " ++ (show exitCode))

-- | parse the file "output.term" from java-owl-parser

parseProc :: FilePath -> IO OntologyMap

parseProc filename =

do d <- readFile filename

let aterm = getATermFull $ readATerm d

case aterm of

AList paarList _ ->

return $ Map.fromList $ parsingAll paarList

_ -> error ("false file: " ++ show filename ++ ".")

-- | parse an ontology with all imported ontologies

parsingAll :: [ATerm] -> [(String, Ontology)]

parsingAll [] = []

parsingAll (aterm:res) =

(ontologyParse aterm):(parsingAll res)

-- | ontology parser, this version ignore validation, massages of java-parser.

ontologyParse :: ATerm -> (String, Ontology)

ontologyParse

(AAppl "UOPaar"

[AAppl uri _ _,

AAppl "OWLParserOutput" [_, _, _, onto] _] _)

= case ontology of

Ontology _ _ namespace ->

(if head uri == '"' then read uri::String else uri,

propagateNspaces namespace $ createAndReduceClassAxiom ontology)

where ontology = fromATerm onto::Ontology

ontologyParse _ = error "false ontology file."

-- | remove equivalent disjoint class axiom, create equivalentClasses,

-- | subClassOf axioms, and sort directives (definitions of classes and

-- | properties muss be moved to begin of directives)

createAndReduceClassAxiom :: Ontology -> Ontology

createAndReduceClassAxiom (Ontology oid directives ns) =

let (definition, axiom, other) =

findAndCreate (List.nub directives) ([], [], [])

directives' = reverse definition ++ reverse axiom ++ reverse other

in Ontology oid directives' ns

where -- search directives list, sort the define concept and role,

-- axioms, and rest

findAndCreate :: [Directive]

-> ([Directive], [Directive], [Directive])

-> ([Directive], [Directive], [Directive])

findAndCreate [] res = res

findAndCreate (h:r) (def, axiom, rest) =

case h of

Ax (Class cid _ Complete _ desps) ->

-- the original directive must also be saved.

findAndCreate r

(h:def,(Ax (EquivalentClasses (DC cid) desps)):axiom,rest)

Ax (Class cid _ Partial _ desps) ->

if null desps then

findAndCreate r (h:def, axiom, rest)

else

findAndCreate r (h:def,

(appendSubClassAxiom cid desps) ++ axiom,

rest)

Ax (EnumeratedClass _ _ _ _) ->

findAndCreate r (h:def, axiom, rest)

Ax (DisjointClasses _ _ _) ->

if any (eqClass h) r then

findAndCreate r (def, axiom, rest)

else findAndCreate r (def,h:axiom, rest)

Ax (DatatypeProperty _ _ _ _ _ _ _) ->

findAndCreate r (h:def, axiom, rest)

Ax (ObjectProperty _ _ _ _ _ _ _ _ _) ->

findAndCreate r (h:def, axiom, rest)

_ -> findAndCreate r (def, axiom, h:rest)

-- append single subClassOf axioms from an derective of ontology

appendSubClassAxiom :: ClassID -> [Description] -> [Directive]

appendSubClassAxiom _ [] = []

appendSubClassAxiom cid (hd:rd) =

(Ax (SubClassOf (DC cid) hd)):(appendSubClassAxiom cid rd)

-- check if two disjointClasses axiom are equivalent

-- (a disjointOf b == b disjointOf a)

eqClass :: Directive -> Directive -> Bool

eqClass dj1 dj2 =

case dj1 of

Ax (DisjointClasses c1 c2 _) ->

case dj2 of

Ax (DisjointClasses c3 c4 _) ->

if (c1 == c4 && c2 == c3)

then True

else False

_ -> False

_ -> False

-- | structure analysis bases of ontologyMap from owl parser

structureAna :: FilePath

-> HetcatsOpts

-> OntologyMap

-> IO (Maybe (LIB_NAME, -- filename

LibEnv -- DGraphs for imported modules

))

structureAna file opt ontoMap =

do

let (newOntoMap, dg) = buildDevGraph ontoMap

case analysis opt of

Structured -> do -- only structure analysis

printMsg $ labNodes dg

putStrLn $ show dg

return (Just (simpleLibName file,

simpleLibEnv file $ reverseGraph dg))

Skip -> return $ fail "" -- Nothing is ambiguous

_ -> staticAna file opt (newOntoMap, dg)

where -- output Analyzing messages for structured anaylsis

printMsg :: [LNode DGNodeLab] -> IO()

printMsg [] = putStrLn ""

printMsg ((_, node):rest) =

do putStrLn ("Analyzing ontology " ++

(showName $ dgn_name node))

printMsg rest

-- simpleLibEnv and simpleLibName builded two simple lib-entities for

-- showGraph

simpleLibEnv :: FilePath -> DGraph -> LibEnv

simpleLibEnv filename dg =

Map.singleton (simpleLibName filename) emptyGlobalContext

{ globalEnv = Map.singleton (mkSimpleId "")

(SpecEntry ((JustNode nodeSig), [], g_sign, nodeSig))

, devGraph = dg }

where nodeSig = NodeSig 0 g_sign

g_sign = G_sign OWL_DL emptySign 0

simpleLibName :: FilePath -> LIB_NAME

simpleLibName s = Lib_id (Direct_link ("library_" ++ s) (Range []))

-- | static analysis if the HetcatesOpts is not only Structured.

-- | sequence call for nodesStaticAna on the basis of topologically

-- | sort of all nodes

staticAna :: FilePath

-> HetcatsOpts

-> (OntologyMap, DGraph)

-> IO (Maybe (LIB_NAME, -- filename

LibEnv -- DGraphs for imported modules

))

staticAna file opt (ontoMap, dg) =

do let topNodes = topsort dg

Result diagnoses res <-

nodesStaticAna (reverse topNodes) Map.empty ontoMap Map.empty dg []

case res of

Just (_, dg', _) -> do

showDiags opt $ List.nub diagnoses

let dg'' = insEdges (reverseLinks $ labEdges dg')

(delEdges (edges dg') dg')

-- putStrLn $ show dg''

return (Just (simpleLibName file,

simpleLibEnv file dg''))

_ -> error "no devGraph..."

-- | a map to save which node has been analysed.

type SignMap = Map.Map Node (Sign, [Named Sentence])

-- | call to static analyse of all nodes

nodesStaticAna :: [Node] -- ^ topologically sort of graph

-> SignMap -- ^ an map of analyzed nodes

-> OntologyMap -- ^ an map of parsed ontology

-> Namespace -- ^ global namespaces

-> DGraph -- ^ current graph

-> [Diagnosis] -- ^ diagnosis of result

-> IO (Result (SignMap, DGraph, Namespace))

-- ^ result is tuple of new map of signs and sentences,

-- ^ new grpah, and new global namespace map.

nodesStaticAna [] signMap _ ns dg diag =

return $ Result diag (Just (signMap, dg, ns))

nodesStaticAna (h:r) signMap ontoMap globalNs dg diag = do

Result digs res <-

-- Each node must be analyzed with the associated imported nodes.

-- Those search for imported nodes is by bfs accomplished.

nodeStaticAna (reverse $ map (matchNode dg) (bfs h dg))

(emptySign, diag)

signMap ontoMap globalNs dg

case res of

Just (newSignMap, newDg, newGlobalNs) ->

nodesStaticAna r newSignMap ontoMap newGlobalNs newDg (diag++digs)

Prelude.Nothing ->

-- Warning or Error message

nodesStaticAna r signMap ontoMap globalNs dg (diag++digs)

-- | call to static analyse of single nodes

nodeStaticAna :: [LNode DGNodeLab] -- ^ imported nodes of one node

-- ^ (incl. itself)

-> (Sign, [Diagnosis]) -- ^ here saved incoming sign, diagnoses

-> SignMap -- ^ an map of analyzed nodes

-> OntologyMap -- ^ an map of parsed ontology

-> Namespace -- ^ global namespaces

-> DGraph -- ^ current graph

-> IO (Result (SignMap, DGraph, Namespace))

nodeStaticAna [] _ _ _ _ _ =

do return initResult -- remove warning

-- the last node in list is current top node.

nodeStaticAna

((n,topNode):[]) (inSig, oldDiags) signMap ontoMap globalNs dg =

do

let nn@(nodeName, _, _) = dgn_name topNode

putStrLn ("Analyzing ontology " ++ (show nodeName))

case Map.lookup n signMap of

Just _ ->

return $ Result oldDiags (Just (signMap, dg, globalNs))

_ ->

do

let ontology@(Ontology mid _ _) = fromJust $

Map.lookup (getNameFromNode nn) ontoMap

Result diag res =

-- static analysis of current ontology with all sign of

-- imported ontology.

basicOWL_DLAnalysis (ontology, inSig, emptyGlobalAnnos)

case res of

Just (_, accSig, sent) ->

do

let (newGlobalNs, tMap) =

integrateNamespaces globalNs (namespaceMap accSig)

newSent = map (renameNamespace tMap) sent

difSig = diffSig accSig inSig

newDifSig = renameNamespace tMap difSig

newSig = renameNamespace tMap accSig

-- the new node (with sign and sentence) has the sign of

-- accumulated sign with imported signs, but the sentences

-- is only of current ontology, because all sentences of

-- imported ontoloies can be automatically outputed by

-- showTheory (see GUI)

newLNode =

(n, topNode {dgn_theory =

G_theory OWL_DL newSig 0 (toThSens newSent)

0})

-- by remove of an node all associated edges are also deleted

-- so the deges must be saved before remove the node, then

-- appended again.

-- The out edges (after reverse are inn edges) must

-- also with new signature be changed.

ledges = (inn dg n) ++ (map (changeGMorOfEdges newSig) (out dg n))

newG = insEdges ledges (insNode newLNode (delNode n dg))

return $ Result (oldDiags ++ diag)

(Just ((Map.insert n (newDifSig, newSent) signMap),

newG, newGlobalNs))

_ -> do let actDiag = mkDiag Error

("error by analysing of " ++ (show mid)) ()

return $ Result (actDiag:oldDiags) Prelude.Nothing

-- The GMorphism of edge should also with new Signature be changed,

-- since with "show theory" the edges also with Sign one links

-- (see Static.DevGraph.joinG_sentences).

where changeGMorOfEdges :: Sign -> LEdge DGLinkLab -> LEdge DGLinkLab

changeGMorOfEdges newSign (n1, n2, edge) =

let newCMor = idComorphism (Logic OWL_DL)

Result _ newGMor = gEmbedComorphism newCMor

(G_sign OWL_DL newSign 0)

in (n1, n2, edge {dgl_morphism = fromJust newGMor})

-- The other nodes in list are examined whether they were already analyzed.

-- if yes then signs of it for further analysis are taken out; otherwise they

-- are first analyzed (with complete part tree of this node).

nodeStaticAna ((n, _):r) (inSig, oldDiags) signMap ontoMap globalNs dg

=

do

case Map.lookup n signMap of

Just (sig, _) ->

nodeStaticAna r ((integSign sig inSig), oldDiags)

signMap ontoMap globalNs dg

Prelude.Nothing ->

do

Result digs' res' <-

nodeStaticAna (reverse $ map (matchNode dg) (bfs n dg))

(emptySign, [])

signMap ontoMap globalNs dg

case res' of

Just (signMap', dg', globalNs') ->

do

let (sig', _) = fromJust $ Map.lookup n signMap'

nodeStaticAna r

((integSign sig' inSig), (oldDiags ++ digs'))

signMap' ontoMap globalNs' dg'

_ -> do error "Error by analysis : nodeStaticAna"

nodeStaticAna r (inSig, oldDiags)

signMap ontoMap globalNs dg

-- | build up two sign

integSign :: Sign -> Sign -> Sign

integSign inSig totalSig =

let (newNamespace, transMap) =

integrateNamespaces (namespaceMap totalSig) (namespaceMap inSig)

in addSign (renameNamespace transMap inSig)

(totalSig {namespaceMap = newNamespace})

-- | turn edges over

reverseLinks :: [LEdge DGLinkLab] -> [LEdge DGLinkLab]

reverseLinks [] = []

reverseLinks ((source, target, edge):r) =

(target, source, edge):(reverseLinks r)

-- | turn all edges over of graph

reverseGraph :: DGraph -> DGraph

reverseGraph dg =

let newLinks = reverseLinks $ labEdges dg

in insEdges newLinks (delEdges (edges dg) dg)

-- | find a node in DevGraph

matchNode :: DGraph -> Node -> LNode DGNodeLab

matchNode dgraph node =

let (mcontext, _ ) = match node dgraph

(_, _, dgNode, _) = fromJust mcontext

in (node, dgNode)