FromXml.hs revision 7577ca4229962db6f297853d160c2e0214bd2034
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : xml input for Hets development graphs
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederCopyright : (c) Simon Ulbricht, DFKI GmbH 2011
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederMaintainer : tekknix@tzi.de
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederStability : provisional
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederPortability : non-portable (DevGraph)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maedercreate new or extend a Development Graph in accordance with an XML input
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederimport Static.ComputeTheory (computeDGraphTheories)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Common.AnalyseAnnos (getGlobalAnnos)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Common.Consistency (Conservativity (..))
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Common.GlobalAnnotations (GlobalAnnos, emptyGlobalAnnos)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Common.LibName (LibName (..), noTime, setFilePath, emptyLibName)
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowskiimport Common.Utils (readMaybe)
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowskiimport Common.XUpdate (getAttrVal)
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowskiimport Comorphisms.LogicGraph (logicGraph)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maederimport Data.List (partition, intercalate, isInfixOf)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport qualified Data.Graph.Inductive.Graph as Graph (Node)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport qualified Data.Map as Map (lookup, insert, empty)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Logic.ExtSign (ext_empty_signature)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Logic.Logic (AnyLogic (..), cod, composeMorphisms)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder-- * Data Types
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | for faster access, some elements attributes are stored alongside
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederas a String -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maedertype NamedNode = (String, Element)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maederdata NamedLink = Link { src :: String
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , trg :: String
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , lType :: DGLinkType
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian Maeder , element :: Element }
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maeder{- | returns a String representation of a list of links showing their
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maedersource and target nodes (used for error messages). -}
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian MaederprintLinks :: [NamedLink] -> String
6948b7295a0521212803f15cf919395d2073e2c9Christian MaederprintLinks = let show' l = src l ++ " -> " ++ trg l in
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder unlines . map show'
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder-- * Top-Level functions
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu{- | main function; receives a FilePath and calls fromXml upon that path,
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanuusing an empty DGraph and initial LogicGraph. -}
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan PascanureadDGXmlR :: HetcatsOpts -> FilePath -> ResultT IO (LibName, LibEnv)
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan PascanureadDGXmlR opts path = do
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu lift $ putIfVerbose opts 2 $ "Reading " ++ path
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu xml' <- lift $ readFile path
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu liftR $ case parseXMLDoc xml' of
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu fail $ "failed to parse XML file: " ++ path
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder Just xml -> case getAttrVal "filename" xml of
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder fail $ "missing DGraph name attribute\n" ++
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder unlines (take 5 $ lines xml')
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder Just nm -> do
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder let ln = setFilePath nm noTime $ emptyLibName nm
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder an <- extractGlobalAnnos xml
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu dg <- fromXml logicGraph emptyDG {globalAnnos = an} xml
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu-- | top-level function
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian MaederreadDGXml :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian MaederreadDGXml opts path = do
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder Result ds res <- runResultT $ readDGXmlR opts path
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder showDiags opts ds
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu{- | main function; receives a logicGraph, an initial DGraph and an xml
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanuelement, then adds all nodes and edges from the element into the DGraph -}
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan PascanufromXml :: LogicGraph -> DGraph -> Element -> Result DGraph
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan PascanufromXml lg dg el = case Map.lookup (currentLogic lg) (logics lg) of
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu fail "current logic was not found in logicMap"
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu Just (Logic lid) -> do
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu let emptyTheory = G_theory lid (ext_empty_signature lid)
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu startSigId noSens startThId
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu nodes <- extractNodeElements el
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu (defLinks, thmLinks) <- extractLinkElements el
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu (dg', depNodes) <- initialiseNodes emptyTheory nodes defLinks dg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder dg1 <- insertNodesAndDefLinks lg depNodes defLinks dg'
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder dg2 <- insertThmLinks lg thmLinks dg1
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder return $ computeDGraphTheories Map.empty dg2
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-- * reconstructing the development graph
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder{- | All nodes that do not have dependencies via the links are processed at the
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maederbeginning and written into the DGraph. Returns the resulting DGraph and the
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederlist of nodes that have not been stored (i.e. have dependencies). -}
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaederinitialiseNodes :: G_theory -> [NamedNode] -> [NamedLink] -> DGraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> Result (DGraph, [NamedNode])
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinitialiseNodes gt nodes links dg = do
294e24edea598311fa5af82e2f6a9cdaa531f5e7Christian Maeder let targets = map trg links
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -- all nodes that are not target of any link are considered independent
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder (dep, indep) = partition ((`elem` targets) . fst) nodes
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dg' <- foldM (insertNode gt) dg indep
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return (dg', dep)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | main loop: in every step, all links are collected of which the source node
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederhas been written into DGraph already. Upon these, further nodes are written
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederin each step until the list of remaining links reaches null. -}
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya GerkeninsertNodesAndDefLinks :: LogicGraph -> [NamedNode] -> [NamedLink] -> DGraph
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken -> Result DGraph
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya GerkeninsertNodesAndDefLinks _ _ [] dg = return dg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsertNodesAndDefLinks lg nodes links dg = let
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (cur, lftL) = splitLinks dg links
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder in if (not . null) cur
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken (dg', lftN) <- iterateNodes lg nodes cur dg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder insertNodesAndDefLinks lg lftN lftL dg'
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder "some elements cannot be reached!\n" ++ printLinks lftL
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder{- | Help function for insertNodesAndDefLinks. Given a list of links, it
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederpartitions the links depending on if they can be processed in one step. -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedersplitLinks :: DGraph -> [NamedLink] -> ([NamedLink], [NamedLink])
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaedersplitLinks dg = killMultTrg . partition hasSource where
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder hasSource l = case lookupNodeByName (src l) dg of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder killMultTrg (hasSrc, noSrc) = let noSrcTrgs = map trg noSrc in
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder foldr (\ l (r, r') -> if elem (trg l) noSrcTrgs
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder then (r, l : r') else (l : r, r')) ([], noSrc) hasSrc
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder{- | Help function for insertNodesAndDefLinks. Given the currently processable
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maederlinks and the total of remaining nodes, it stores all processable elements
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederinto the DGraph. Returns the updated DGraph and the list of remaining nodes. -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederiterateNodes :: LogicGraph -> [NamedNode] -> [NamedLink] -> DGraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> Result (DGraph, [NamedNode])
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederiterateNodes _ nodes [] dg = return (dg, nodes)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederiterateNodes _ [] links _ = fail $
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder "some links are missing their target nodes!\n" ++ printLinks links
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederiterateNodes lg (x@(name, _) : xs) links dg =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder case partitionWith trg name links of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder ([], _) -> do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (dg', xs') <- iterateNodes lg xs links dg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return (dg', x : xs')
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (lCur, lLft) -> do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder dg' <- insNdAndDefLinks lg x lCur dg
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder iterateNodes lg xs lLft dg'
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederpartitionWith :: Eq a => (NamedLink -> a) -> a -> [NamedLink]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> ([NamedLink], [NamedLink])
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederpartitionWith f v = partition ((== v) . f)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder-- | inserts all theorem link into the previously constructed dgraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsertThmLinks :: LogicGraph -> [NamedLink] -> DGraph -> Result DGraph
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederinsertThmLinks lg links dg' = foldM ins' dg' links where
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder ins' dg l = do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (i, mr) <- extractMorphism lg dg l
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (j, gsig) <- signOfNode (trg l) dg
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder morph <- finalizeMorphism lg mr gsig (lType l)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder insertLink i j morph (lType l) dg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | inserts a new node into the dgraph as well as all deflinks that target
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederthis particular node -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsNdAndDefLinks :: LogicGraph -> NamedNode -> [NamedLink] -> DGraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> Result DGraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsNdAndDefLinks lg trgNd links dg = do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder mrs <- mapM (extractMorphism lg dg) links
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder gsig1 <- gsigManyUnion lg $ map (cod . snd) mrs
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder let gt = case gsig1 of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder G_sign lid sg sId -> noSensGTheory lid sg sId
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder dg' <- insertNode gt dg trgNd
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder (j, gsig2) <- signOfNode (fst trgNd) dg'
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder let ins' dgR ((i, mr), l) = do
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder morph <- finalizeMorphism lg mr gsig2 (lType l)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder insertLink i j morph (lType l) dgR
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder foldM ins' dg' $ zip mrs links
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder-- | inserts a new link into the dgraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsertLink :: Graph.Node -> Graph.Node -> GMorphism -> DGLinkType -> DGraph
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -> Result DGraph
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaederinsertLink i j mr tp = return . snd
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder . insLEdgeDG (i, j, defDGLink mr tp SeeTarget)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder-- | inserts a new node into the dgraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsertNode :: G_theory -> DGraph -> NamedNode -> Result DGraph
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian MaederinsertNode gt dg x = do
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder let an = globalAnnos dg
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder n = getNewNodeDG dg
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder lbl <- mkDGNodeLab gt an x
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder return $ insLNodeDG (n, lbl) dg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-- * logic calculations
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | given a links intermediate morphism and its target nodes signature,
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederthis function calculates the final morphism for this link -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederfinalizeMorphism :: LogicGraph -> GMorphism -> G_sign -> DGLinkType
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> Result GMorphism
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederfinalizeMorphism lg mr sg lTp = do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder {- TODO: for HidingDefLinks the inclusion is reversed.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder check if this works right! -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder mr1 <- case lTp of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder HidingDefLink -> ginclusion lg sg (cod mr)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder _ -> ginclusion lg (cod mr) sg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder composeMorphisms mr mr1
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | A Node is looked up via its name in the DGraph. Returns the nodes
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maedersignature, but only if one single node is found for the respective name.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederOtherwise an error is thrown. -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedersignOfNode :: String -> DGraph -> Result (Graph.Node, G_sign)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedersignOfNode nd dg = case lookupNodeByName nd dg of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder [] -> fail $ "required node [" ++ nd ++ "] was not found in DGraph!"
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder [(j, lbl)] -> do
e509b6f97f98f96ef258c1c3f7968241da8bde5dTill Mossakowski return (j, signOf (dgn_theory lbl))
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder _ -> fail $ "ambiguous occurence for node [" ++ nd ++ "]!"
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-- * Element extraction
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder{- | extracts the intermediate morphism for a link, using the xml data and the
e509b6f97f98f96ef258c1c3f7968241da8bde5dTill Mossakowskisignature of the (previously inserted) source node -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractMorphism :: LogicGraph -> DGraph -> NamedLink
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> Result (Graph.Node, GMorphism)
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian MaederextractMorphism lg dg l = do
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder (i, sgn) <- signOfNode (src l) dg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder case findChild (unqual "GMorphism") (element l) of
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder Nothing -> fail $
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder "Links morphism description is missing!\n" ++ printLinks [l]
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder Just mor -> do
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder nm <- getAttrVal "name" mor
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder let symbs = parseSymbolMap mor
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder mor' <- getGMorphism lg sgn nm symbs
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder return (i, mor')
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederparseSymbolMap :: Element -> String
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederparseSymbolMap = intercalate ", "
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder . map ( intercalate " |-> "
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder . map strContent . elChildren )
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder . deepSearch ["map"]
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder{- | Generates a new DGNodeLab with a startoff-G_theory, an Element and the
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maederthe DGraphs Global Annotations -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedermkDGNodeLab :: G_theory -> GlobalAnnos -> NamedNode -> Result DGNodeLab
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaedermkDGNodeLab gt annos (name, el) = let
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder parseSpecs specElems = let
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder specs = unlines $ map strContent specElems
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (response, msg) = extendByBasicSpec annos specs gt
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder in case response of
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder Success gt' _ symbs _ -> return (gt', symbs)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Failure _ -> fail $ "( @node: " ++ name ++ " )\n" ++ msg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder in case findChild (unqual "Reference") el of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -- Case #1: regular node
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Nothing -> do
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski (gt', symbs) <- parseSpecs $ deepSearch ["Axiom", "Theorem", "Symbol"] el
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder return $ newNodeLab (parseNodeName name) (DGBasicSpec Nothing symbs) gt'
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -- Case #2: reference node
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder Just rf -> do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (gt', _) <- parseSpecs $ findChildren (unqual "Signature") rf
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder {- using DGRef currently leads to runtime errors.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder see revision 14911 for such an approach -}
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder return $ newNodeLab (parseNodeName name) DGBasic gt'
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | All nodes are taken from the xml-element. Then, the name-attribute is
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maederlooked up and stored alongside the node for easy access. Nodes with no names
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederare ignored. -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractNodeElements :: Element -> Result [NamedNode]
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederextractNodeElements = foldM labelNode [] . findChildren (unqual "DGNode") where
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder labelNode r e = do
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder nm <- getAttrVal "name" e
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder return $ (nm, e) : r
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | All links are taken from the xml-element and stored alongside their source
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederand target information. The links are then partitioned depending on if they
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederare theorem or definition links. -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractLinkElements :: Element -> Result ([NamedLink], [NamedLink])
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractLinkElements el = do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder l1 <- foldM labelLink [] $ findChildren (unqual "DGLink") el
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder return $ partition isDef l1 where
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski isDef = isDefEdge . lType
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken labelLink r e = do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder sr <- getAttrVal "source" e
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder tr <- getAttrVal "target" e
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder tp <- extractLinkType e
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return $ Link sr tr tp e : r
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-- | reads the type of a link from the xml data
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractLinkType :: Element -> Result DGLinkType
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya GerkenextractLinkType l = do