FromXml.hs revision 4bf72807172000becf65e11bd225efc1dfd99713
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht{- |
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtModule : $Header$
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtDescription : xml input for Hets development graphs
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtCopyright : (c) Simon Ulbricht, DFKI GmbH 2011
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtLicense : GPLv2 or higher, see LICENSE.txt
da4b55f4795a4b585f513eaceb67cda10485febfChristian MaederMaintainer : tekknix@informatik.uni-bremen.de
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtStability : provisional
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtPortability : non-portable (DevGraph)
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbrichtcreate new or extend a Development Graph in accordance with an XML input
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht-}
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbrichtmodule Static.FromXml where
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbrichtimport Static.ComputeTheory (computeLibEnvTheories)
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbrichtimport Static.DevGraph
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbrichtimport Static.GTheory
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Common.AnalyseAnnos (getGlobalAnnos)
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Common.Consistency (Conservativity (..))
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Common.GlobalAnnotations (GlobalAnnos, emptyGlobalAnnos)
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbrichtimport Common.LibName
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maederimport Common.Result
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maederimport Common.ResultT
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Common.Utils (readMaybe)
8600e22385bce13c5d1048f7b955f9394a5d94d6Simon Ulbrichtimport Common.XUpdate (getAttrVal)
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht
8600e22385bce13c5d1048f7b955f9394a5d94d6Simon Ulbrichtimport Comorphisms.LogicGraph (logicGraph)
79eb29c05606f195fe9c6fdca02bcaa458dde17dSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Control.Monad.Trans (lift)
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbrichtimport Control.Monad (foldM)
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht
804459c3af78eeee3fd3c940c74594febd030dacSimon Ulbrichtimport Data.List (partition, intercalate, isInfixOf)
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maederimport Data.Maybe (fromMaybe)
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbrichtimport qualified Data.Graph.Inductive.Graph as Graph (Node)
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbrichtimport qualified Data.Map as Map (lookup, insert, empty, union)
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Driver.Options
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbrichtimport Driver.ReadFn (findFileOfLibNameAux)
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maeder
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Logic.ExtSign (ext_empty_signature)
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Logic.Grothendieck
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Logic.Logic (AnyLogic (..), cod, composeMorphisms)
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Logic.Prover (noSens)
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Text.XML.Light
024d83266148fc53f9d6f82bedd0b8cb4a6213a9Simon Ulbricht
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbrichtimport Debug.Trace
024d83266148fc53f9d6f82bedd0b8cb4a6213a9Simon Ulbricht-- * Data Types
024d83266148fc53f9d6f82bedd0b8cb4a6213a9Simon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | for faster access, some elements attributes are stored alongside
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtas a String -}
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichttype NamedNode = (String, Element)
5212c904eb65bed7c08f5c6e54df9618125d2939Simon Ulbricht
21f01439b3d87ccc385d3bce73afb2d187d14d05Simon Ulbrichtdata NamedLink = Link { src :: String
21f01439b3d87ccc385d3bce73afb2d187d14d05Simon Ulbricht , trg :: String
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht , lType :: DGLinkType
21f01439b3d87ccc385d3bce73afb2d187d14d05Simon Ulbricht , element :: Element }
3ff10b5930bbec5d888826a65828397795877213Simon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | returns a String representation of a list of links showing their
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtsource and target nodes (used for error messages). -}
765f0ff34c8f2354a4e8a4fbb4467ec5e788c55fSimon UlbrichtprintLinks :: [NamedLink] -> String
765f0ff34c8f2354a4e8a4fbb4467ec5e788c55fSimon UlbrichtprintLinks = let show' l = src l ++ " -> " ++ trg l in
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maeder unlines . map show'
3ff10b5930bbec5d888826a65828397795877213Simon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht-- * Top-Level functions
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | main function; receives a FilePath and calls fromXml upon that path,
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtusing an empty DGraph and initial LogicGraph. -}
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian MaederreadDGXmlR :: HetcatsOpts -> FilePath -> ResultT IO (LibName, LibEnv)
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian MaederreadDGXmlR opts path = do
e90b8ee3fac5c932d83af2061579c6b57d528885Christian Maeder lift $ putIfVerbose opts 2 $ "Reading " ++ path
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maeder xml' <- lift $ readFile path
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht liftR $ case parseXMLDoc xml' of
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maeder Nothing ->
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht fail $ "failed to parse XML file: " ++ path
c25b3ec03906317eabc06bb4dd48bc9cf3841332Simon Ulbricht Just xml -> case getAttrVal "filename" xml of
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maeder Nothing ->
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht fail $ "missing DGraph name attribute\n" ++
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht unlines (take 5 $ lines xml')
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht Just nm -> do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht let ln = setFilePath nm noTime $ emptyLibName nm
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht an <- extractGlobalAnnos xml
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht dg <- fromXml logicGraph emptyDG {globalAnnos = an} xml
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht trace (show ln) $ return (ln, Map.insert ln dg Map.empty)
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht
8600e22385bce13c5d1048f7b955f9394a5d94d6Simon Ulbricht
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maeder-- | top-level function
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian MaederreadDGXml :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian MaederreadDGXml opts path = do
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maeder Result ds res <- runResultT $ readDGXmlR opts path
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maeder showDiags opts ds
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht case res of
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht Just (ln, lv) -> do
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht let dg = lookupDGraph ln lv
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht lv' <- loadRefLibs opts (map snd (lookupNodeWith (isDGRef . snd) dg)) lv
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht return $ Just (ln, computeLibEnvTheories lv')
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht _ -> return res
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht
4bf72807172000becf65e11bd225efc1dfd99713Simon UlbrichtloadRefLibs :: HetcatsOpts -> [DGNodeLab] -> LibEnv -> IO LibEnv
4bf72807172000becf65e11bd225efc1dfd99713Simon UlbrichtloadRefLibs _ [] lv = return lv
4bf72807172000becf65e11bd225efc1dfd99713Simon UlbrichtloadRefLibs opts (x:xs) lv = case nodeInfo x of
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht DGRef ln _ -> trace (getFilePath ln) $ do
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht mPath <- findFileOfLibNameAux opts { intype = DgXml } (getFilePath ln)
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht case mPath of
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht Just path -> do
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht Result _ res <- runResultT $ readDGXmlR opts path
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht case res of
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht Just (_, lv') -> loadRefLibs opts xs $ Map.union lv lv'
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht _ -> loadRefLibs opts xs lv
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht _ -> loadRefLibs opts xs lv
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht _ -> loadRefLibs opts xs lv
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht
8600e22385bce13c5d1048f7b955f9394a5d94d6Simon Ulbricht
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht-- | creates an entirely empty theory
5b93337fb97e848522fcc277e384f694595bc42cSimon UlbrichtemptyTheory :: AnyLogic -> G_theory
5b93337fb97e848522fcc277e384f694595bc42cSimon UlbrichtemptyTheory (Logic lid) =
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht G_theory lid (ext_empty_signature lid) startSigId noSens startThId
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | main function; receives a logicGraph, an initial DGraph and an xml
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtelement, then adds all nodes and edges from the element into the DGraph -}
1c258a97f602cf389ed2aed3924108889dbef512Simon UlbrichtfromXml :: LogicGraph -> DGraph -> Element -> Result DGraph
403c7e517cea70c01c7dd15695867fe4f8820ab4Simon UlbrichtfromXml lg dg el = case Map.lookup (currentLogic lg) (logics lg) of
403c7e517cea70c01c7dd15695867fe4f8820ab4Simon Ulbricht Nothing ->
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht fail "current logic was not found in logicMap"
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht Just lo -> do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht nodes <- extractNodeElements el
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht (defLinks, thmLinks) <- extractLinkElements el
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht (dg', depNodes) <- initialiseNodes (emptyTheory lo) nodes defLinks dg
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht dg1 <- insertNodesAndDefLinks lg depNodes defLinks dg'
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht insertThmLinks lg thmLinks dg1
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht
5ea7ec7c1a5dead365687d6b0270837522c0e6feSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht-- * reconstructing the development graph
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht{- | All nodes that do not have dependencies via the links are processed at the
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtbeginning and written into the DGraph. Returns the resulting DGraph and the
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtlist of nodes that have not been stored (i.e. have dependencies). -}
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon UlbrichtinitialiseNodes :: G_theory -> [NamedNode] -> [NamedLink] -> DGraph
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht -> Result (DGraph, [NamedNode])
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtinitialiseNodes gt nodes links dg = do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht let targets = map trg links
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht -- all nodes that are not target of any link are considered independent
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht (dep, indep) = partition ((`elem` targets) . fst) nodes
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht dg' <- foldM (insertNode gt) dg indep
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht return (dg', dep)
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | main loop: in every step, all links are collected of which the source node
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichthas been written into DGraph already. Upon these, further nodes are written
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtin each step until the list of remaining links reaches null. -}
403c7e517cea70c01c7dd15695867fe4f8820ab4Simon UlbrichtinsertNodesAndDefLinks :: LogicGraph -> [NamedNode] -> [NamedLink] -> DGraph
04641e4ea004e422b32d3e6359f68a3326b4aa8bSimon Ulbricht -> Result DGraph
04641e4ea004e422b32d3e6359f68a3326b4aa8bSimon UlbrichtinsertNodesAndDefLinks _ _ [] dg = return dg
403c7e517cea70c01c7dd15695867fe4f8820ab4Simon UlbrichtinsertNodesAndDefLinks lg nodes links dg = let
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht (cur, lftL) = splitLinks dg links
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht in if (not . null) cur
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht then do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht (dg', lftN) <- iterateNodes lg nodes cur dg
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht insertNodesAndDefLinks lg lftN lftL dg'
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht else fail $
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht "some elements cannot be reached!\n" ++ printLinks lftL
c51cb4bddcd39a87711e238c0c562d67451476dbSimon Ulbricht
94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | Help function for insertNodesAndDefLinks. Given a list of links, it
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtpartitions the links depending on if they can be processed in one step. -}
fe6a19b07759bc4190e88dda76a211d86bf32062Simon UlbrichtsplitLinks :: DGraph -> [NamedLink] -> ([NamedLink], [NamedLink])
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtsplitLinks dg = killMultTrg . partition hasSource where
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht hasSource l = case lookupNodeByName (src l) dg of
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht [] -> False
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht _ -> True
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht killMultTrg (hasSrc, noSrc) = let noSrcTrgs = map trg noSrc in
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht foldr (\ l (r, r') -> if elem (trg l) noSrcTrgs
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht then (r, l : r') else (l : r, r')) ([], noSrc) hasSrc
804459c3af78eeee3fd3c940c74594febd030dacSimon Ulbricht
804459c3af78eeee3fd3c940c74594febd030dacSimon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | Help function for insertNodesAndDefLinks. Given the currently processable
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtlinks and the total of remaining nodes, it stores all processable elements
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtinto the DGraph. Returns the updated DGraph and the list of remaining nodes. -}
403c7e517cea70c01c7dd15695867fe4f8820ab4Simon UlbrichtiterateNodes :: LogicGraph -> [NamedNode] -> [NamedLink] -> DGraph
04641e4ea004e422b32d3e6359f68a3326b4aa8bSimon Ulbricht -> Result (DGraph, [NamedNode])
04641e4ea004e422b32d3e6359f68a3326b4aa8bSimon UlbrichtiterateNodes _ nodes [] dg = return (dg, nodes)
04641e4ea004e422b32d3e6359f68a3326b4aa8bSimon UlbrichtiterateNodes _ [] links _ = fail $
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht "some links are missing their target nodes!\n" ++ printLinks links
fe6a19b07759bc4190e88dda76a211d86bf32062Simon UlbrichtiterateNodes lg (x@(name, _) : xs) links dg =
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht case partitionWith trg name links of
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht ([], _) -> do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht (dg', xs') <- iterateNodes lg xs links dg
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht return (dg', x : xs')
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht (lCur, lLft) -> do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht dg' <- insNdAndDefLinks lg x lCur dg
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht iterateNodes lg xs lLft dg'
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon UlbrichtpartitionWith :: Eq a => (NamedLink -> a) -> a -> [NamedLink]
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht -> ([NamedLink], [NamedLink])
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon UlbrichtpartitionWith f v = partition ((== v) . f)
5917663ca76c8f8b60b767f7fb959f1d1609576bSimon Ulbricht
5917663ca76c8f8b60b767f7fb959f1d1609576bSimon Ulbricht
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht-- | inserts all theorem link into the previously constructed dgraph
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtinsertThmLinks :: LogicGraph -> [NamedLink] -> DGraph -> Result DGraph
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtinsertThmLinks lg links dg' = foldM ins' dg' links where
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht ins' dg l = do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht (i, mr) <- extractMorphism lg dg l
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht (j, gsig) <- signOfNode (trg l) dg
96a17035df49356b70d7ac14bd9f4d52a5f0308dSimon Ulbricht morph <- finalizeMorphism lg mr gsig
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht insertLink i j morph (lType l) dg
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | inserts a new node into the dgraph as well as all deflinks that target
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtthis particular node -}
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtinsNdAndDefLinks :: LogicGraph -> NamedNode -> [NamedLink] -> DGraph
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht -> Result DGraph
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon UlbrichtinsNdAndDefLinks lg trgNd links dg = do
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht mrs <- mapM (extractMorphism lg dg) links
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht (dg', isHiding) <- case partition (isHidingDef . lType) links of
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht -- case #1: none hiding def links
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht ([], _) -> do
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht gsig1 <- gsigManyUnion lg $ map (cod . snd) mrs
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht let gt = case gsig1 of
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht G_sign lid sg sId -> noSensGTheory lid sg sId
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht dg' <- insertNode gt dg trgNd
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht return (dg', False)
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht -- case #2: only hiding def links
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht (_, []) -> case Map.lookup (currentLogic lg) (logics lg) of
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht Nothing ->
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht fail "current logic was not found in logicMap"
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht Just lo -> do
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht dg' <- insertNode (emptyTheory lo) dg trgNd
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht return (dg', True)
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht -- case #3: mixture. not implemented!
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht _ -> fail "mix of HidingDefLinks and other links pointing at a single node"
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht (j, gsig2) <- signOfNode (fst trgNd) dg'
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht let ins' dgR ((i, mr), l) = do
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht morph <- if isHiding then ginclusion lg gsig2 (cod mr)
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht else finalizeMorphism lg mr gsig2
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht insertLink i j morph (lType l) dgR
55be4caff6a01e4c32ec47ee27fe00b67dfd3db5Simon Ulbricht foldM ins' dg' $ zip mrs links
9458e270eb4d18c8e76fdaa569023931ca7ca8dfSimon Ulbricht
5917663ca76c8f8b60b767f7fb959f1d1609576bSimon Ulbricht
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht-- | inserts a new link into the dgraph
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon UlbrichtinsertLink :: Graph.Node -> Graph.Node -> GMorphism -> DGLinkType -> DGraph
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht -> Result DGraph
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtinsertLink i j mr tp = return . snd
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht . insLEdgeDG (i, j, defDGLink mr tp SeeTarget)
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht-- | inserts a new node into the dgraph
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtinsertNode :: G_theory -> DGraph -> NamedNode -> Result DGraph
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtinsertNode gt dg x = do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht let an = globalAnnos dg
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht n = getNewNodeDG dg
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht lbl <- mkDGNodeLab gt an x
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht return $ insLNodeDG (n, lbl) dg
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht-- * logic calculations
5917663ca76c8f8b60b767f7fb959f1d1609576bSimon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | given a links intermediate morphism and its target nodes signature,
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtthis function calculates the final morphism for this link -}
96a17035df49356b70d7ac14bd9f4d52a5f0308dSimon UlbrichtfinalizeMorphism :: LogicGraph -> GMorphism -> G_sign -> Result GMorphism
96a17035df49356b70d7ac14bd9f4d52a5f0308dSimon UlbrichtfinalizeMorphism lg mr sg = do
30b3567d60173c99ef8db1f0a1d8bda73a4225fdSimon Ulbricht mr1 <- ginclusion lg (cod mr) sg
30b3567d60173c99ef8db1f0a1d8bda73a4225fdSimon Ulbricht composeMorphisms mr mr1
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht-- * Utils
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht{- | A Node is looked up via its name in the DGraph. Returns the nodes
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbrichtsignature, but only if one single node is found for the respective name.
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtOtherwise an error is thrown. -}
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtsignOfNode :: String -> DGraph -> Result (Graph.Node, G_sign)
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtsignOfNode nd dg = case lookupNodeByName nd dg of
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht [] -> fail $ "required node [" ++ nd ++ "] was not found in DGraph!"
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder [(j, lbl)] ->
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht return (j, signOf (dgn_theory lbl))
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht _ -> fail $ "ambiguous occurence for node [" ++ nd ++ "]!"
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht-- * Element extraction
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | extracts the intermediate morphism for a link, using the xml data and the
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtsignature of the (previously inserted) source node -}
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtextractMorphism :: LogicGraph -> DGraph -> NamedLink
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht -> Result (Graph.Node, GMorphism)
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtextractMorphism lg dg l = do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht (i, sgn) <- signOfNode (src l) dg
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht case findChild (unqual "GMorphism") (element l) of
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht Nothing -> fail $
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht "Links morphism description is missing!\n" ++ printLinks [l]
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht Just mor -> do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht nm <- getAttrVal "name" mor
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht let symbs = parseSymbolMap mor
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht mor' <- getGMorphism lg sgn nm symbs
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht return (i, mor')
192498961d079b4a31585f9f63148233804cc1c9Simon Ulbricht
3c606bbc21a488c9eaebbfcd833b0b31af25341aSimon UlbrichtparseSymbolMap :: Element -> String
67c57fe89afed0947d5ff8fc8b04c4ace0b9595eSimon UlbrichtparseSymbolMap = intercalate ", "
3c606bbc21a488c9eaebbfcd833b0b31af25341aSimon Ulbricht . map ( intercalate " |-> "
3c606bbc21a488c9eaebbfcd833b0b31af25341aSimon Ulbricht . map strContent . elChildren )
67c57fe89afed0947d5ff8fc8b04c4ace0b9595eSimon Ulbricht . deepSearch ["map"]
3c606bbc21a488c9eaebbfcd833b0b31af25341aSimon Ulbricht
5917663ca76c8f8b60b767f7fb959f1d1609576bSimon Ulbricht
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht-- TODO: when inserting RefNodes, call addToRefNodesDG (DevGraph)!!
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht{- | Generates a new DGNodeLab with a startoff-G_theory, an Element and the
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtthe DGraphs Global Annotations -}
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtmkDGNodeLab :: G_theory -> GlobalAnnos -> NamedNode -> Result DGNodeLab
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon UlbrichtmkDGNodeLab gt annos (name, el) = let
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht parseSpecs specElems = let
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht specs = unlines $ map strContent specElems
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht (response, msg) = extendByBasicSpec annos specs gt
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht in case response of
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht Success gt' _ symbs _ -> return (gt', symbs)
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht Failure _ -> fail
972f1416b11d73d3e98597538cd6d96c13caf992Simon Ulbricht $ "[ " ++ name ++ " ]\n" ++ msg
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht in case findChild (unqual "Reference") el of
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht -- Case #1: regular node
e3d7fd1b63d824960b1c17b6c7009d52d7528c1eChristian Maeder Nothing -> let ch1 = case findChild (unqual "Declarations") el of
e3d7fd1b63d824960b1c17b6c7009d52d7528c1eChristian Maeder Just ch -> deepSearch ["Symbol"] ch
149252aa10a12adce1929d98f5fcfe9c2e88167dSimon Ulbricht Nothing -> findChildren (unqual "Signature") el
5b93337fb97e848522fcc277e384f694595bc42cSimon Ulbricht ch2 = deepSearch ["Axiom", "Theorem"] el
149252aa10a12adce1929d98f5fcfe9c2e88167dSimon Ulbricht in do
149252aa10a12adce1929d98f5fcfe9c2e88167dSimon Ulbricht (gt', symbs) <- parseSpecs $ ch1 ++ ch2
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder diffSig <- homGsigDiff (signOf gt') $ signOf gt
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder return $ newNodeLab (parseNodeName name)
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder (DGBasicSpec Nothing diffSig symbs) gt'
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht -- Case #2: reference node
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht Just rf -> do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht (gt', _) <- parseSpecs $ findChildren (unqual "Signature") rf
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht refLib <- case getAttrVal "library" rf of
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht Nothing -> fail $ "no library name for reference node " ++ name
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht Just ln -> return $ setFilePath ln noTime $ emptyLibName ln
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht return $ newInfoNodeLab (parseNodeName name) (newRefInfo refLib (-1)) gt'
67c57fe89afed0947d5ff8fc8b04c4ace0b9595eSimon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | All nodes are taken from the xml-element. Then, the name-attribute is
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtlooked up and stored alongside the node for easy access. Nodes with no names
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtare ignored. -}
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtextractNodeElements :: Element -> Result [NamedNode]
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtextractNodeElements = foldM labelNode [] . findChildren (unqual "DGNode") where
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht labelNode r e = do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht nm <- getAttrVal "name" e
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht return $ (nm, e) : r
765f0ff34c8f2354a4e8a4fbb4467ec5e788c55fSimon Ulbricht
765f0ff34c8f2354a4e8a4fbb4467ec5e788c55fSimon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | All links are taken from the xml-element and stored alongside their source
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtand target information. The links are then partitioned depending on if they
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtare theorem or definition links. -}
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtextractLinkElements :: Element -> Result ([NamedLink], [NamedLink])
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtextractLinkElements el = do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht l1 <- foldM labelLink [] $ findChildren (unqual "DGLink") el
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht return $ partition isDef l1 where
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht isDef = isDefEdge . lType
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht labelLink r e = do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht sr <- getAttrVal "source" e
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht tr <- getAttrVal "target" e
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht tp <- extractLinkType e
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht return $ Link sr tr tp e : r
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht-- | reads the type of a link from the xml data
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtextractLinkType :: Element -> Result DGLinkType
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtextractLinkType l = do
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht tp <- case findChild (unqual "Type") l of
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht Nothing -> fail "Links type description is missing!"
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht Just xy -> return $ strContent xy
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht if tp == "HidingDefInc" then return HidingDefLink else do
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht let sc = if isInfixOf "Global" tp then Global else Local
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht if isInfixOf "Def" tp
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht -- Case #1: DefinitionLink, global or local
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht then return $ localOrGlobalDef sc None
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht else if not $ isInfixOf "Thm" tp
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht then fail $ "unknown link type!\n" ++ tp
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht else case findChild (unqual "Status") l of
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht -- Case #2: Unproven theorem link, global or local
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht Nothing -> return $ localOrGlobalThm sc None
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht Just st -> if strContent st /= "Proven"
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht then fail $ "unknown links status!\n" ++ strContent st
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht -- Case #3: Proven theorem link, global or local
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht else let
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht rl = case findChild (unqual "Rule") l of
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht Nothing -> "no rule"
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht Just r' -> strContent r'
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht cc = case findChild (unqual "ConsStatus") l of
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht Nothing -> None
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder Just c' -> fromMaybe None $ readMaybe $ strContent c'
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht lkind = ThmLink $ Proven (DGRule rl) emptyProofBasis
7577ca4229962db6f297853d160c2e0214bd2034Simon Ulbricht in return $ ScopedLink sc lkind $ mkConsStatus cc
67c57fe89afed0947d5ff8fc8b04c4ace0b9595eSimon Ulbricht
765f0ff34c8f2354a4e8a4fbb4467ec5e788c55fSimon Ulbricht
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht-- | extracts the global annotations from the xml-graph
8fa27254f463e2c958a10dc513450b992f80137bSimon UlbrichtextractGlobalAnnos :: Element -> Result GlobalAnnos
c3b1c9fa0aa53167405eb9a004137fb5e327fd4fSimon UlbrichtextractGlobalAnnos dgEle = case findChild (unqual "Global") dgEle of
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht Nothing -> return emptyGlobalAnnos
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht Just gl -> getGlobalAnnos $ unlines $ map strContent
8fa27254f463e2c958a10dc513450b992f80137bSimon Ulbricht $ findChildren (unqual "Annotation") gl
c3b1c9fa0aa53167405eb9a004137fb5e327fd4fSimon Ulbricht
c3b1c9fa0aa53167405eb9a004137fb5e327fd4fSimon Ulbricht
21f01439b3d87ccc385d3bce73afb2d187d14d05Simon Ulbricht-- | custom xml-search for not only immediate children
9458e270eb4d18c8e76fdaa569023931ca7ca8dfSimon UlbrichtdeepSearch :: [String] -> Element -> [Element]
689c36560d1509e6f040c096b719a31b31d2d84cSimon UlbrichtdeepSearch tags' ele = rekSearch ele where
9458e270eb4d18c8e76fdaa569023931ca7ca8dfSimon Ulbricht tags = map unqual tags'
846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maeder rekSearch e = filtr e ++ concatMap filtr (elChildren e)
9458e270eb4d18c8e76fdaa569023931ca7ca8dfSimon Ulbricht filtr = filterChildrenName (`elem` tags)