FromXml.hs revision c52c301fb104b784a899ab237a0e1887a0246b97
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@informatik.uni-bremen.de
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian 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 (computeLibEnvTheories)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Common.AnalyseAnnos (getGlobalAnnos)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Common.Consistency (Conservativity (..))
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Common.GlobalAnnotations (GlobalAnnos, emptyGlobalAnnos)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Common.Result (Result (..))
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederimport Common.Utils (readMaybe)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maederimport Common.XUpdate (getAttrVal)
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanuimport Comorphisms.LogicGraph (logicGraph)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Data.List (partition, intercalate, isInfixOf)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Data.Maybe (fromMaybe)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport qualified Data.Graph.Inductive.Graph as Graph (Node)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport qualified Data.Map as Map (lookup, insert, empty)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport qualified Data.Set as Set (Set)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Driver.ReadFn (findFileOfLibNameAux)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maederimport Logic.ExtSign (ext_empty_signature)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport Logic.Logic (AnyLogic (..), cod, composeMorphisms)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder{- -------------
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian Maeder{- | for faster access, some elements attributes are stored alongside
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maederas a String -}
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maedertype NamedNode = (String, Element)
6948b7295a0521212803f15cf919395d2073e2c9Christian Maederdata NamedLink = Link { src :: String
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder , trg :: String
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian , lType :: LType
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder , element :: Element }
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanudata LType = DefL { scope :: Scope
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu , isHiding :: Bool }
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu | ThmL { scope :: Scope
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu , isHiding :: Bool }
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan PascanugetLType :: Element -> ResultT IO LType
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan PascanugetLType el = case findChild (unqual "Type") el of
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu Just tp -> let
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder scp = if isInfixOf "Global" $ strContent tp then Global else Local
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder def = isInfixOf "Def" $ strContent tp
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder hid = isInfixOf "Hiding" $ strContent tp
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder in return $ if def then DefL scp hid else ThmL scp hid
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder Nothing -> fail "links type description is missing"
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder{- ----------------------
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan PascanuTop-Level Functions -}
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 Map.empty
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder showDiags opts ds
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu{- | main function; receives a FilePath and calls fromXml upon that path,
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanuusing an initial LogicGraph. -}
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan PascanureadDGXmlR :: HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (LibName, LibEnv)
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan PascanureadDGXmlR opts path lv = do
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu lift $ putIfVerbose opts 2 $ "Reading " ++ path
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu xml' <- lift $ readFile path
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu case parseXMLDoc xml' of
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu fail $ "failed to parse XML file: " ++ path
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu Just xml -> case getAttrVal "libname" xml of
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu fail $ "missing DGraph name attribute\n" ++
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder unlines (take 5 $ lines xml')
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian Just nm -> do
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian let ln = setFilePath nm noTime $ emptyLibName nm
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian fromXml opts logicGraph ln lv xml
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder{- | main function; receives a logicGraph, an initial LibEnv and an Xml
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maederelement, then adds all nodes and edges from this element into a DGraph -}
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaederfromXml :: HetcatsOpts -> LogicGraph -> LibName -> LibEnv -> Element
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> ResultT IO (LibName, LibEnv)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederfromXml opts lg ln lv xml = case Map.lookup (currentLogic lg) (logics lg) of
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder fail "current logic was not found in logicMap"
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder Just lo -> do
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder an <- extractGlobalAnnos xml
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder let dg = emptyDG { globalAnnos = an }
5ff3af2a00b2663a7aaeffa820338a895dc38b82Cui Jian nodes <- extractNodeElements xml
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder (defLk, thmLk) <- extractLinkElements xml
64325303fc09fc4d88ced49be11ff2d29966422aCui Jian (res0, depNd) <- initialise opts (emptyTheory lo) nodes defLk (dg, lv)
da955132262baab309a50fdffe228c9efe68251dCui Jian res1 <- insertNodesAndDefLinks opts lg depNd defLk res0
da955132262baab309a50fdffe228c9efe68251dCui Jian res2 <- insertThmLinks lg thmLk res1
64325303fc09fc4d88ced49be11ff2d29966422aCui Jian return (ln, computeLibEnvTheories $ uncurry (Map.insert ln) res2)
64325303fc09fc4d88ced49be11ff2d29966422aCui Jian{- ------------------------------------------------
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederReconstruct the Development Graph, high level -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | All nodes that do not have dependencies via the links are processed at the
da955132262baab309a50fdffe228c9efe68251dCui Jianbeginning and written into the DGraph. Returns the resulting DGraph and the
37e30366abd83c00a5d5447b45694627fd783de8Cui Jianlist of nodes that have not been stored (i.e. have dependencies). -}
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maederinitialise :: HetcatsOpts -> G_theory -> [NamedNode] -> [NamedLink]
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian -> (DGraph, LibEnv) -> ResultT IO ((DGraph, LibEnv), [NamedNode])
37e30366abd83c00a5d5447b45694627fd783de8Cui Jianinitialise opts gt nodes links dglv = do
544b866d340cdef36332f59ecd899daa1807f6c7Cui Jian let targets = map trg links
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder -- all nodes that are not target of any link are considered independent
5ff3af2a00b2663a7aaeffa820338a895dc38b82Cui Jian (dep, indep) = partition ((`elem` targets) . fst) nodes
5ff3af2a00b2663a7aaeffa820338a895dc38b82Cui Jian (dglv') <- foldM (flip $ insertNode opts gt) dglv indep
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder return (dglv', dep)
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder-- | inserts all theorem link into the previously constructed dgraph
5ff3af2a00b2663a7aaeffa820338a895dc38b82Cui JianinsertThmLinks :: LogicGraph -> [NamedLink] -> (DGraph, LibEnv)
64325303fc09fc4d88ced49be11ff2d29966422aCui Jian -> ResultT IO (DGraph, LibEnv)
64325303fc09fc4d88ced49be11ff2d29966422aCui JianinsertThmLinks lg links (dg, lv) = do
da955132262baab309a50fdffe228c9efe68251dCui Jian dg' <- foldM ins' dg links
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder return (dg', lv) where
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder ins' dgR l = do
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder (i, mr, tp) <- extractMorphism lg dgR l
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder (j, gsig) <- signOfNode (trg l) dgR
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder morph <- finalizeMorphism lg mr gsig
64325303fc09fc4d88ced49be11ff2d29966422aCui Jian insertLink i j morph tp dgR
64325303fc09fc4d88ced49be11ff2d29966422aCui Jian{- | main loop: in every step, all links are collected of which the source node
64325303fc09fc4d88ced49be11ff2d29966422aCui Jianhas been written into DGraph already. Upon these, further nodes are written in
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maedereach step until the list of remaining links reaches null. -}
da955132262baab309a50fdffe228c9efe68251dCui JianinsertNodesAndDefLinks :: HetcatsOpts -> LogicGraph -> [NamedNode]
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder -> [NamedLink] -> (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv)
37e30366abd83c00a5d5447b45694627fd783de8Cui JianinsertNodesAndDefLinks _ _ _ [] dglv = return dglv
3fe83d4c932a8266edcf0304a97814c59821d91fChristian MaederinsertNodesAndDefLinks opts lg nodes links (dg, lv) = let
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken (cur, lftL) = splitLinks dg links
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder in if (not . null) cur
b5a5755f7d034f5ebc9f7f45e878c68695e139c4Thiemo Wiedemeyer (dglv', lftN) <- iterateNodes opts lg nodes cur (dg, lv)
b5a5755f7d034f5ebc9f7f45e878c68695e139c4Thiemo Wiedemeyer insertNodesAndDefLinks opts lg lftN lftL dglv'
b5a5755f7d034f5ebc9f7f45e878c68695e139c4Thiemo Wiedemeyer "some elements cannot be reached!\n" ++ printLinks lftL
b5a5755f7d034f5ebc9f7f45e878c68695e139c4Thiemo Wiedemeyer{- | Help function for insertNodesAndDefLinks. Given the currently processable
120eec9ff1748e1ae786e2ab073234198bc0f701Christian 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. -}
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederiterateNodes :: HetcatsOpts -> LogicGraph -> [NamedNode] -> [NamedLink]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> (DGraph, LibEnv) -> ResultT IO ((DGraph, LibEnv), [NamedNode])
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederiterateNodes _ _ nodes [] dglv = return (dglv, nodes)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederiterateNodes _ _ [] links _ = fail $
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian "some links are missing their target nodes!\n" ++ printLinks links
37e30366abd83c00a5d5447b45694627fd783de8Cui JianiterateNodes opts lg (x@(name, _) : xs) links dglv =
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder case partition ((== name) . trg) links of
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder ([], _) -> do
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder (dglv', xs') <- iterateNodes opts lg xs links dglv
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder return (dglv', x : xs')
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder (lCur, lLft) -> do
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian dglv' <- insertNodeAndLinks opts lg x lCur dglv
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder iterateNodes opts lg xs lLft dglv'
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder{- | inserts a new node into the dgraph as well as all definition links that
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maedertarget this particular node -}
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederinsertNodeAndLinks :: HetcatsOpts -> LogicGraph -> NamedNode -> [NamedLink]
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -> (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsertNodeAndLinks opts lg trgNd links (dg, lv) = do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder mrs <- mapM (extractMorphism lg dg) links
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder ((dg', lv'), hid) <- case partition (isHiding . lType) links of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -- case #1: none hiding def links
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder ([], _) -> do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder gsig1 <- liftR $ gsigManyUnion lg $ map (\(_, m, _) -> cod m) mrs
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder let gt = case gsig1 of
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder G_sign lid sg sId -> noSensGTheory lid sg sId
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dglv <- insertNode opts gt trgNd (dg, lv)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder return (dglv, False)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -- case #2: only hiding def links
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (_, []) -> case Map.lookup (currentLogic lg) (logics lg) of
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian fail "current logic was not found in logicMap"
49d8e1a419ee5658d23762335af121179a68669fCui Jian Just lo -> do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder dglv <- insertNode opts (emptyTheory lo) trgNd (dg, lv)
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian return (dglv, True)
da955132262baab309a50fdffe228c9efe68251dCui Jian -- case #3: mixture. not implemented!
49d8e1a419ee5658d23762335af121179a68669fCui Jian _ -> fail "mix of HidingDefLinks and other links pointing at a single node"
49d8e1a419ee5658d23762335af121179a68669fCui Jian (j, gsig2) <- signOfNode (fst trgNd) dg'
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian let ins' dgR (i, mr, tp) = do
64325303fc09fc4d88ced49be11ff2d29966422aCui Jian morph <- if hid then liftR $ ginclusion lg gsig2 (cod mr)
64325303fc09fc4d88ced49be11ff2d29966422aCui Jian else finalizeMorphism lg mr gsig2
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian insertLink i j morph tp dgR
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder dg'' <- foldM ins' dg' mrs
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return (dg'', lv')
b03274844ecd270f9e9331f51cc4236a33e2e671Christian 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 -> ResultT IO GMorphism
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederfinalizeMorphism lg mr sg = liftR $ do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder mr1 <- ginclusion lg (cod mr) sg
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder composeMorphisms mr mr1
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- -----------------------------------------------
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederReconstruct the Development Graph, low level -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-- | inserts a new link into the dgraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsertLink :: Graph.Node -> Graph.Node -> GMorphism -> DGLinkType -> DGraph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> ResultT IO DGraph
37e30366abd83c00a5d5447b45694627fd783de8Cui JianinsertLink i j mr tp = return .
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian insLEdgeNubDG (i, j, defDGLink mr tp SeeTarget)
da955132262baab309a50fdffe228c9efe68251dCui Jian{- | Generates and inserts a new DGNodeLab with a startoff-G_theory, an Element
37e30366abd83c00a5d5447b45694627fd783de8Cui Jianand the the DGraphs Global Annotations -}
37e30366abd83c00a5d5447b45694627fd783de8Cui JianinsertNode :: HetcatsOpts -> G_theory -> NamedNode -> (DGraph, LibEnv)
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian -> ResultT IO (DGraph, LibEnv)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederinsertNode opts gt (name, el) (dg, lv) =
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder case findChild (unqual "Reference") el of
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder Just rf -> insertRefNode opts rf (name, el) (dg, lv)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder Nothing -> let
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder n = getNewNodeDG dg
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder ch1 = case findChild (unqual "Declarations") el of
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder Just ch -> deepSearch ["Symbol"] ch
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder Nothing -> findChildren (unqual "Signature") el
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder ch2 = deepSearch ["Axiom", "Theorem"] el
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder (gt', symbs) <- parseSpecs gt name dg $ ch1 ++ ch2
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder diffSig <- liftR $ homGsigDiff (signOf gt') $ signOf gt
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder let lbl = newNodeLab (parseNodeName name)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder (DGBasicSpec Nothing diffSig symbs) gt'
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder return (insLNodeDG (n, lbl) dg, lv)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsertRefNode :: HetcatsOpts -> Element -> NamedNode -> (DGraph, LibEnv)
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian -> ResultT IO (DGraph, LibEnv)
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui JianinsertRefNode opts rf (name, el) (dg, lv) = do
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian refLib <- case getAttrVal "library" rf of
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian Nothing -> fail $ "no library name for reference node " ++ name
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian Just ln -> return ln
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian refNod <- case getAttrVal "node" rf of
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian Nothing -> fail $ "no reference node name for node " ++ name
da955132262baab309a50fdffe228c9efe68251dCui Jian Just nm -> return nm
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian (dg', lv') <- case Map.lookup (emptyLibName refLib) lv of
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian Just dg' -> return (dg', lv)
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian Nothing -> loadRefLib opts refLib lv
da955132262baab309a50fdffe228c9efe68251dCui Jian (i, gt) <- case lookupNodeByName refNod dg' of
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian [(i, lbl)] -> case signOf $ dgn_theory lbl of
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian G_sign lid sign sId -> return (i, noSensGTheory lid sign sId)
da955132262baab309a50fdffe228c9efe68251dCui Jian _ -> fail $ "reference node " ++ refNod ++ " was not found"
da955132262baab309a50fdffe228c9efe68251dCui Jian (gt', _) <- parseSpecs gt name dg
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian $ deepSearch ["Axiom", "Theorem"] el
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian let n = getNewNodeDG dg
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian nInf = newRefInfo (emptyLibName refLib) i
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian lbl = newInfoNodeLab (parseNodeName name) nInf gt'
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui Jian return (addToRefNodesDG n nInf $ insLNodeDG (n, lbl) dg, lv')
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui JianloadRefLib :: HetcatsOpts -> String -> LibEnv -> ResultT IO (DGraph, LibEnv)
e04726af1ef4af2f172f6ce2a075a4f004ea98f1Cui JianloadRefLib opts ln lv = do
f4ae50539e67874b6162f8334f6782a0d66acefaCui Jian mPath <- lift $ findFileOfLibNameAux opts { intype = DgXml } ln
f4ae50539e67874b6162f8334f6782a0d66acefaCui Jian case mPath of
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder Just path -> do
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder (ln', lv') <- readDGXmlR opts path lv
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder return (lookupDGraph ln' lv', lv')
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder _ -> fail $ "no file exists for reference library " ++ ln
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederparseSpecs :: G_theory -> String -> DGraph -> [Element]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> ResultT IO (G_theory, Set.Set G_symbol)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederparseSpecs gt' name dg specElems = let
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder specs = unlines $ map strContent specElems
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (response, msg) = extendByBasicSpec (globalAnnos dg) specs gt'
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder in case response of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Success gt'' _ symbs _ -> return (gt'', symbs)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Failure _ -> fail $ "[ " ++ name ++ " ]\n" ++ msg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- ---------------------
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederElement extraction -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | extracts the intermediate morphism for a link, using the xml data and the
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maedersignature of the (previously inserted) source node -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractMorphism :: LogicGraph -> DGraph -> NamedLink
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> ResultT IO (Graph.Node, GMorphism, DGLinkType)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractMorphism lg dg (Link srN _ tp l) =
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken case findChild (unqual "GMorphism") l of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Nothing -> fail "Links morphism description is missing!"
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Just mor -> let
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder symbs = parseSymbolMap mor
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder rl = case findChild (unqual "Rule") l of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Nothing -> "no rule"
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Just r' -> strContent r'
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder cc = case findChild (unqual "ConsStatus") l of
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder Nothing -> None
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian Just c' -> fromMaybe None $ readMaybe $ strContent c'
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (i, sgn) <- signOfNode srN dg
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder nm <- getAttrVal "name" mor
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (sgn', lTp) <- case tp of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder DefL sc hid -> return $ if hid then (sgn, HidingDefLink)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder else (sgn, localOrGlobalDef sc cc)
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian ThmL sc hid -> do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder lStat <- case findChild (unqual "Status") l of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Nothing -> return LeftOpen
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder Just st -> if strContent st /= "Proven"
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder then fail $ "unknown links status!\n" ++ strContent st
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder else return $ Proven (DGRule rl) emptyProofBasis
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder if hid then do
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder mSrc <- getAttrVal "morphismsource" mor
da955132262baab309a50fdffe228c9efe68251dCui Jian (i', sgn') <- signOfNode mSrc dg
da955132262baab309a50fdffe228c9efe68251dCui Jian mr' <- liftR $ ginclusion lg sgn' sgn
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder return (sgn', HidingFreeOrCofreeThm Nothing i' mr' lStat)
b5a5755f7d034f5ebc9f7f45e878c68695e139c4Thiemo Wiedemeyer else return (sgn, ScopedLink sc (ThmLink lStat) $ mkConsStatus cc)
b5a5755f7d034f5ebc9f7f45e878c68695e139c4Thiemo Wiedemeyer mor' <- liftR $ getGMorphism lg sgn' nm symbs
b5a5755f7d034f5ebc9f7f45e878c68695e139c4Thiemo Wiedemeyer return (i, mor', lTp)
b5a5755f7d034f5ebc9f7f45e878c68695e139c4Thiemo Wiedemeyer-- | reads the type of a link from the xml data
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaedergetDGLinkTyp :: NamedLink -> GMorphism -> ResultT IO DGLinkType
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian MaedergetDGLinkTyp (Link _ _ tp l) mor = let
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder rl = case findChild (unqual "Rule") l of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Nothing -> "no rule"
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder Just r' -> strContent r'
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder cc = case findChild (unqual "ConsStatus") l of
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder Nothing -> None
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder Just c' -> fromMaybe None $ readMaybe $ strContent c'
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder in case tp of
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder DefL sc hid -> return $ if hid then HidingDefLink
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder else localOrGlobalDef sc cc
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder ThmL sc hid -> do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder lStat <- case findChild (unqual "Status") l of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Nothing -> return LeftOpen
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder Just st -> if strContent st /= "Proven"
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder then fail $ "unknown links status!\n" ++ strContent st
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder else return $ Proven (DGRule rl) emptyProofBasis
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return $ if hid then HidingFreeOrCofreeThm Nothing (-1) mor lStat
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder else ScopedLink sc (ThmLink lStat) $ mkConsStatus cc
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederparseSymbolMap :: Element -> String
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederparseSymbolMap = intercalate ", "
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder . map ( intercalate " |-> "
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder . map strContent . elChildren )
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder . deepSearch ["map"]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- | All nodes are taken from the xml-element. Then, the name-attribute is
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederlooked up and stored alongside the node for easy access. Nodes with no names
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederare ignored. -}
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederextractNodeElements :: Element -> ResultT IO [NamedNode]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractNodeElements = foldM labelNode [] . findChildren (unqual "DGNode") where
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder labelNode r e = do
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder nm <- getAttrVal "name" e
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder return $ (nm, e) : r
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian 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 -> ResultT IO ([NamedLink], [NamedLink])
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractLinkElements el = do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder l1 <- foldM labelLink [] $ findChildren (unqual "DGLink") el
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return $ partition (\ l -> case lType l of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder DefL _ _ -> True
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder _ -> False) l1 where
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski labelLink r e = do
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken sr <- getAttrVal "source" e
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder tr <- getAttrVal "target" e
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder tp <- getLType e
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return $ Link sr tr tp e : r
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken-- | extracts the global annotations from the xml-graph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractGlobalAnnos :: Element -> ResultT IO GlobalAnnos
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederextractGlobalAnnos dgEle = case findChild (unqual "Global") dgEle of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Nothing -> return emptyGlobalAnnos
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken Just gl -> liftR $ getGlobalAnnos $ unlines $ map strContent
signOfNode :: String -> DGraph -> ResultT IO (Graph.Node, G_sign)