XGraph.hs revision fa8878c6145f652f615a04a5e9c15a1d1327bc92
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{-# LANGUAGE DeriveDataTypeable #-}
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederDescription : xml input for Hets development graphs
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Simon Ulbricht, DFKI GmbH 2011
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : tekknix@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable (DevGraph)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederconvert an Xml-Graph into an XGraph-Structure.
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowskiimport Common.AnalyseAnnos (getGlobalAnnos)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederimport Common.Consistency (Conservativity (..))
760ae19a92dde8249679a674f93f58d26a7c5f6bChristian Maederimport Common.GlobalAnnotations (GlobalAnnos, emptyGlobalAnnos)
88c800932dd7053322501ea2039d9f234be6866cKlaus Luettichimport Common.Result (Result (..))
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport Common.Utils (readMaybe)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport Common.XUpdate (getAttrVal, readAttrVal)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichimport Data.Maybe (fromMaybe)
e1f542dcb2f3f33a7a1be5096f5ccf6147d3576cChristian Maederimport qualified Data.Set as Set
e1f542dcb2f3f33a7a1be5096f5ccf6147d3576cChristian Maederimport qualified Data.Map as Map
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maeder{- -------------
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maeder-- represent element information in the order they can be processed later
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederdata XGraph = XGraph { libName :: LibName
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich , globAnnos :: GlobalAnnos
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , nextLinkId :: EdgeId
5d44c8cecd07b47ce537c7e14bf7b41a39f08507Christian Maeder , thmLinks :: [XLink]
5d44c8cecd07b47ce537c7e14bf7b41a39f08507Christian Maeder , startNodes :: [XNode]
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maeder , xg_body :: XTree }
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maeder deriving (Typeable, Data)
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich{- outer list must be executed in order; inner lists represent all def-links
7b2177999334c920c5669621bd3c142fe198a8d7Christian Maeder-node bundles that can be processed in one step -}
9e748851c150e1022fb952bab3315e869aaf0214Christian Maedertype XTree = [[([XLink], XNode)]]
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maedertype EdgeMap = Map.Map String (Map.Map String [XLink])
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettichdata XNode = XNode { nodeName :: NodeName
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , logicName :: String
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , symbs :: (Bool, String) -- ^ hidden?
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , specs :: String -- ^ Sentences
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , nd_cons :: Conservativity }
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder | XRef { nodeName :: NodeName
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , refNode :: String
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , refLib :: String
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , specs :: String }
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder deriving (Typeable, Data)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederdata XLink = XLink { source :: String
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , target :: String
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , edgeId :: EdgeId
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , lType :: DGEdgeType
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder , rule :: DGRule
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder , cons :: Conservativity
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder , prBasis :: ProofBasis
5d44c8cecd07b47ce537c7e14bf7b41a39f08507Christian Maeder , mr_name :: String
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder , mr_source :: Maybe String
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder , mapping :: String }
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder deriving (Typeable, Data)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederinstance Show XNode where
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder show xn = showName (nodeName xn)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederinstance Show XLink where
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder show xl = showEdgeId (edgeId xl) ++ ": " ++ source xl ++ " -> " ++ target xl
549b97cfbe3a6687db74440a550b68b2fc19a272Christian Maederinstance Ord XLink where
549b97cfbe3a6687db74440a550b68b2fc19a272Christian Maeder compare xl1 xl2 = compare (edgeId xl1, source xl1, target xl1)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (edgeId xl2, source xl2, target xl2)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederinstance Eq XLink where
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich a == b = compare a b == EQ
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- ------------
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus LuettichinsertXLink :: XLink -> EdgeMap -> EdgeMap
5d4038657f6a63e131f5804af2f7957b69e15a43Klaus LuettichinsertXLink l = Map.insertWith (Map.unionWith (++)) (target l)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder $ Map.singleton (source l) [l]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermkEdgeMap :: [XLink] -> EdgeMap
77a65251ee036c6aaf09c2775315a4ee24259fbdJorina Freya GerkenmkEdgeMap = foldl (flip insertXLink) Map.empty
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederxGraph :: Element -> Result XGraph
23ab8855c58adfbd03a0730584b917b24c603901Christian MaederxGraph xml = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder allNodes <- extractXNodes xml
97812b7ce9860bf514a8822a63503451795dbc65Klaus Luettich allLinks <- extractXLinks xml
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder _ <- foldM (\ s l -> let e = edgeId l in
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder if Set.member e s then fail $ "duplicate edge id: " ++ show e
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder else return $ Set.insert e s) Set.empty allLinks
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder nodeMap <- foldM (\ m n -> let s = showName $ nodeName n in
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder if Map.member s m then fail $ "duplicate node name: " ++ s
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder else return $ Map.insert s n m) Map.empty allNodes
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let (thmLk, defLk) = partition (\ l -> case edgeTypeModInc $ lType l of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ThmType {} -> True
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder _ -> False) allLinks
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder edgeMap = mkEdgeMap defLk
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (\ n _ -> Set.notMember n $ Map.keysSet edgeMap)
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maeder missingTgts = Set.difference (Map.keysSet edgeMap) tgts
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers srcs = Set.unions $ map Map.keysSet $ Map.elems edgeMap
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maeder missingSrcs = Set.difference srcs tgts
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder unless (Set.null missingTgts)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers $ fail $ "missing nodes for edge targets " ++ show missingTgts
5d4038657f6a63e131f5804af2f7957b69e15a43Klaus Luettich unless (Set.null missingSrcs)
5d4038657f6a63e131f5804af2f7957b69e15a43Klaus Luettich $ fail $ "missing nodes for edge sources " ++ show missingSrcs
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder nm <- getAttrVal "libname" xml
c432483b64662e8db604a58758cd18ea7fa65659Christian Maeder fl <- getAttrVal "filename" xml
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder let ln = setFilePath fl $ emptyLibName nm
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder ga <- extractGlobalAnnos xml
8659594bb40eb5f3da5439692f0908300947191eSonja Gröning i' <- fmap readEdgeId $ getAttrVal "nextlinkid" xml
8c692d0cc44e7df93f58a3eed0d9774ba5908339Jorina Freya Gerken xg <- builtXGraph (Map.keysSet initN) edgeMap restN []
eeb419aa20c97b4af973e97ee6ae77a8eed29e15Till Mossakowski return $ XGraph ln ga i' thmLk (Map.elems initN) xg
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederbuiltXGraph :: Monad m => Set.Set String -> EdgeMap -> Map.Map String XNode
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder -> XTree -> m XTree
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederbuiltXGraph ns xls xns xg = if Map.null xls && Map.null xns then return xg
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder when (Map.null xls) $ fail $ "unprocessed nodes: " ++ show (Map.keysSet xns)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder when (Map.null xns) $ fail $ "unprocessed links: "
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ++ show (map edgeId $ concat $ concatMap Map.elems $ Map.elems xls)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let (sls, rls) = Map.partition ((`Set.isSubsetOf` ns) . Map.keysSet) xls
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder when (Map.null bs) $ fail $ "cannot continue with source nodes:\n "
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ++ show (Set.difference (Set.unions $ map Map.keysSet $ Map.elems rls) ns)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ++ "\nfor given nodes: " ++ show ns
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder builtXGraph (Set.union ns $ Map.keysSet bs) rls
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder map (\ (m, x) -> (concat $ Map.elems m, x)) (Map.elems bs) : xg
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederextractXNodes :: Monad m => Element -> m [XNode]
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederextractXNodes = mapM mkXNode . findChildren (unqual "DGNode")
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix ReckersextractXLinks :: Monad m => Element -> m [XLink]
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederextractXLinks = mapM mkXLink . findChildren (unqual "DGLink")
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedermkXNode :: Monad m => Element -> m XNode
a02a4eb2a2029d27a11fff2ebcc6c460574a74fcKlaus LuettichmkXNode el = let spcs = unlines . map strContent
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder . concatMap (findChildren $ unqual "Text")
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski $ deepSearch ["Axiom", "Theorem"] el
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski get f s = f . map strContent . deepSearch [s]
b70b9c569e477c6a877c93d3ecc17c38c9e047dcChristian Maeder get' = get unlines in do
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maeder nm <- extractNodeName el
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maeder case findChild (unqual "Reference") el of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Just rf -> do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder rfNm <- getAttrVal "node" rf
a348b2eb46eb51f376c910d6dd4415fdab6713bdChristian Maeder rfLib <- getAttrVal "library" rf
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder return $ XRef nm rfNm rfLib spcs
7ea1b24778bb8f58c650f5ae659da720b9f9e109Klaus Luettich Nothing -> let
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder hdSyms = case findChild (unqual "Hidden") el of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Nothing -> case findChild (unqual "Declarations") el of
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder -- Case #1: No declared or hidden symbols
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder Nothing -> (False, "")
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder -- Case #2: Node has declared symbols (DGBasicSpec)
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke Just ch -> (False, get' "Symbol" ch)
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke -- Case #3: Node has hidden symbols (DGRestricted)
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke Just ch -> (True, get (intercalate ", ") "Symbol" ch)
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke lgN <- getAttrVal "logic" el
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder xp0 <- getAttrVal "relxpath" el
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder nm0 <- getAttrVal "refname" el
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder xp1 <- readXPath (nm0 ++ xp0)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder return $ XNode nm { xpath = reverse xp1 } lgN hdSyms spcs $ readCons el
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederextractNodeName :: Monad m => Element -> m NodeName
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederextractNodeName e = liftM parseNodeName $ getAttrVal "name" e
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till MossakowskimkXLink :: Monad m => Element -> m XLink
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermkXLink el = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder sr <- getAttrVal "source" el
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers tr <- getAttrVal "target" el
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder ei <- extractEdgeId el
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder tp <- case findChild (unqual "Type") el of
ed9207cf24e96b0d6f59985822054ae28cb69b2eChristian Maeder Just tp' -> return $ revertDGEdgeTypeName $ strContent tp'
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder Nothing -> fail "links type description is missing"
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder rl <- case findChild (unqual "Rule") el of
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder Nothing -> return $ DGRule "no rule"
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder Just r' -> case findChildren (unqual "MovedTheorems") el of
b10267ae0a6523b73113fc2dee9ea628266fce60Christian Maeder [] -> return $ DGRule $ strContent r'
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder mThs -> liftM DGRuleLocalInference $ mapM (\ e -> do
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder nmOld <- getAttrVal "name" e
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder nmNew <- getAttrVal "renamedTo" e
05a8b581f98b928baca6dab60cd20277659ac760Christian Maeder return (nmOld, nmNew)) mThs
ed9207cf24e96b0d6f59985822054ae28cb69b2eChristian Maeder prB <- mapM (getAttrVal "linkref") $ findChildren (unqual "ProofBasis") el
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder (mrNm, mrSrc) <- case findChild (unqual "GMorphism") el of
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder Nothing -> fail "Links morphism description is missing!"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just mor -> do
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder nm <- getAttrVal "name" mor
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return (nm, findAttr (unqual "morphismsource") mor)
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich let parseSymbMap = intercalate ", " . map ( intercalate " |-> "
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder . map strContent . elChildren ) . deepSearch ["map"]
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder prBs = ProofBasis $ foldr (Set.insert . readEdgeId) Set.empty prB
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder cc = readCons el
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich return $ XLink sr tr ei tp rl cc prBs mrNm mrSrc $ parseSymbMap el
08e5741dd8b6bf9b7419e89298e384e18bc57f64Christian MaederreadCons :: Element -> Conservativity
53818ced114da21321063fff307aa41c1ab31dd3Achim MahnkereadCons el = case findChild (unqual "ConsStatus") el of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> None
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just c' -> fromMaybe None $ readMaybe $ strContent c'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederextractEdgeId :: Monad m => Element -> m EdgeId
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederextractEdgeId = liftM EdgeId . readAttrVal "XGraph.extractEdgeId" "linkid"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederreadEdgeId :: String -> EdgeId
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederreadEdgeId = EdgeId . fromMaybe (-1) . readMaybe
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | custom xml-search for not only immediate children
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederdeepSearch :: [String] -> Element -> [Element]
b905126bab9454b89041f92b3c50bb9efc85e427Klaus LuettichdeepSearch tags e = filtr e ++ concatMap filtr (elChildren e) where
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich filtr = filterChildrenName (`elem` map unqual tags)
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich-- | extracts the global annotations from the xml-graph
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederextractGlobalAnnos :: Element -> Result GlobalAnnos
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian MaederextractGlobalAnnos dgEle = case findChild (unqual "Global") dgEle of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Nothing -> return emptyGlobalAnnos
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder Just gl -> parseAnnotations gl
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian MaederparseAnnotations :: Element -> Result GlobalAnnos
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian MaederparseAnnotations = getGlobalAnnos . unlines . map strContent
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich . findChildren (unqual "Annotation")