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 Ulbrichtcreate new or extend a Development Graph in accordance with an XML input
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbrichtimport Static.ComputeTheory (computeLibEnvTheories)
fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbrichtimport Common.Result (Result (..))
8600e22385bce13c5d1048f7b955f9394a5d94d6Simon Ulbrichtimport Comorphisms.LogicGraph (logicGraph)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbrichtimport Control.Monad (foldM, unless)
4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbrichtimport qualified Data.Graph.Inductive.Graph as Graph (Node)
0223b75560eead55b7bbf11d18117a6819540983Christian Maederimport qualified Data.Map as Map
1a088ae6e5ab1e717d720da7b517233286665073Christian Maederimport qualified Data.Set as Set
4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbrichtimport Driver.ReadFn (findFileOfLibNameAux)
e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Logic.ExtSign (ext_empty_signature)
1a088ae6e5ab1e717d720da7b517233286665073Christian Maederimport Logic.Logic (AnyLogic (..), cod, composeMorphisms)
036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon Ulbrichtimport Text.XML.Light (Element)
fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht-- | top-level function
fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon UlbrichtreadDGXml :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon UlbrichtreadDGXml opts path = do
59fa2ed5a4936e7e56f7164d8a274df68dd4160cSimon Ulbricht Result ds res <- runResultT $ readDGXmlR opts path Map.empty
fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht showDiags opts ds
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | main function; receives a FilePath and calls fromXml upon that path,
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbrichtusing an initial LogicGraph. -}
59fa2ed5a4936e7e56f7164d8a274df68dd4160cSimon UlbrichtreadDGXmlR :: HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (LibName, LibEnv)
59fa2ed5a4936e7e56f7164d8a274df68dd4160cSimon UlbrichtreadDGXmlR opts path lv = do
e90b8ee3fac5c932d83af2061579c6b57d528885Christian Maeder lift $ putIfVerbose opts 2 $ "Reading " ++ path
ce07f3639c04fc3457da387c0dfd9ec01dbf05c4Christian Maeder xml' <- lift $ readXmlFile path
da5b7a9907d7e4f3bed31ae76dff8bbe562ef8b3Christian Maeder res <- lift $ parseXml xml'
036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon Ulbricht Right xml -> rebuiltDgXml opts lv xml
036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon Ulbricht Left err -> fail $ "failed to parse XML file: " ++ path ++ "\n" ++ err
5d75e163c4134d97bba0ced346c3095d7150685cSimon Ulbricht-- | call rebuiltDG with only a LibEnv and an Xml-Element
036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon UlbrichtrebuiltDgXml :: HetcatsOpts -> LibEnv -> Element -> ResultT IO (LibName, LibEnv)
036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon UlbrichtrebuiltDgXml opts lv xml = do
8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht xg <- liftR $ xGraph xml
8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht res <- rebuiltDG opts logicGraph xg lv
8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht let ln = libName xg
8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht return (ln, computeLibEnvTheories $ uncurry (Map.insert ln) res)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht{- | reconstructs the Development Graph via a previously created XGraph-
8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon UlbrichtrebuiltDG :: HetcatsOpts -> LogicGraph -> XGraph -> LibEnv
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht -> ResultT IO (DGraph, LibEnv)
9b59de1ee08232aa26d9d21d3bf99f8d1f68c45dChristian MaederrebuiltDG opts lg (XGraph _ ga i thmLk nds body) lv = do
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder (dg, lv') <- rebuiltBody body lv
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder dg' <- insertThmLinks lg dg $ mkEdgeMap thmLk
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder return (dg', lv') where
8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht rebuiltBody bd lv' = case bd of
857ab542e0b0bdf90e5a484ffe8df5a9c9c3e38fChristian Maeder foldM (flip $ insertFirstNode opts lg)
3413b54d5439b4a66d6423cc134e1b9abb5bbe2fChristian Maeder (emptyDG { globalAnnos = ga, getNewEdgeId = i }, lv') nds
9b59de1ee08232aa26d9d21d3bf99f8d1f68c45dChristian Maeder bs : bd' -> do
8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht res0 <- rebuiltBody bd' lv'
a9ad67574dd71144680f8dedc285f6c4498a79f8Christian Maeder foldM (\ dl (lKs, nd) ->
a9ad67574dd71144680f8dedc285f6c4498a79f8Christian Maeder insertStep opts lg nd lKs dl)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht-- | inserts a new node as well as all definition links pointing at that node
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtinsertStep :: HetcatsOpts -> LogicGraph -> XNode -> [XLink] -> (DGraph, LibEnv)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht -> ResultT IO (DGraph, LibEnv)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtinsertStep opts lg xNd lks (dg, lv) = do
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht mrs <- mapM (getTypeAndMorphism lg dg) lks
2fa75b8879de8c878475f16ab43161e0580f5430Simon Ulbricht G_sign lid sg sId <- getSigForXNode lg dg mrs
627e304eb081ce411768e08d3554d8efd52d4187Simon Ulbricht let j = getNewNodeDG dg
5d75e163c4134d97bba0ced346c3095d7150685cSimon Ulbricht (gt2, dg', lv') <-
5d75e163c4134d97bba0ced346c3095d7150685cSimon Ulbricht insertNode opts lg (Just $ noSensGTheory lid sg sId) xNd j (dg, lv)
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht dg'' <- foldM (insertLink lg j (signOf gt2)) dg' mrs
fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht return (dg'', lv')
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon UlbrichtinsertLink :: LogicGraph -> Graph.Node -> G_sign -> DGraph
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht -> (Graph.Node, GMorphism, DGLinkType, XLink) -> ResultT IO DGraph
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon UlbrichtinsertLink lg j gs dg (i, mr, tp, lk) = do
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht lkLab <- finalizeLink lg lk mr gs tp
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht return $ insEdgeAsIs (i, j, lkLab) dg
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder-- | inserts theorem links
0223b75560eead55b7bbf11d18117a6819540983Christian MaederinsertThmLinks :: LogicGraph -> DGraph -> EdgeMap -> ResultT IO DGraph
0223b75560eead55b7bbf11d18117a6819540983Christian MaederinsertThmLinks lg p = foldM (\ dg (tgt, sm) -> do
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder (j, gsig) <- signOfNode tgt dg
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder insertTarThmLinks lg j gsig dg sm) p . Map.toList
0223b75560eead55b7bbf11d18117a6819540983Christian MaederinsertTarThmLinks :: LogicGraph -> Graph.Node -> G_sign
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder -> DGraph -> Map.Map String [XLink] -> ResultT IO DGraph
0223b75560eead55b7bbf11d18117a6819540983Christian MaederinsertTarThmLinks lg j tgt p = foldM (\ dg (src, ls) -> do
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder (i, gsig) <- signOfNode src dg
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder foldM (\ dg' xLk -> do
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder (mr, tp) <- getTypeAndMorphism1 lg dg gsig xLk
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht insertLink lg j tgt dg' (i, mr, tp, xLk)) dg ls) p . Map.toList
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbricht{- | given a links intermediate morphism and its target nodes signature,
fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtthis function calculates the final morphism for this link -}
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtfinalizeLink :: LogicGraph -> XLink -> GMorphism -> G_sign -> DGLinkType
f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbricht -> ResultT IO DGLinkLab
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtfinalizeLink lg xLk mr sg tp = do
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht mr' <- liftR $ case edgeTypeModInc $ lType xLk of
f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbricht HidingDef -> ginclusion lg sg (cod mr)
f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbricht mr1 <- ginclusion lg (cod mr) sg
f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbricht composeMorphisms mr mr1
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht return $ defDGLinkId mr' tp SeeTarget $ edgeId xLk
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht{- | based upon the morphisms of ingoing deflinks, calculate the initial
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbrichtsignature to be used for node insertion -}
2fa75b8879de8c878475f16ab43161e0580f5430Simon UlbrichtgetSigForXNode :: LogicGraph -> DGraph
2fa75b8879de8c878475f16ab43161e0580f5430Simon Ulbricht -> [(Graph.Node, GMorphism, DGLinkType, XLink)]
2fa75b8879de8c878475f16ab43161e0580f5430Simon Ulbricht -> ResultT IO G_sign
2fa75b8879de8c878475f16ab43161e0580f5430Simon UlbrichtgetSigForXNode lg dg mrs = case mrs of
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht [] -> fail "insertStep: empty link list"
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht (_, _, FreeOrCofreeDefLink _ _, xLk) : rt -> do
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht unless (null rt)
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht $ fail "unexpected non-singleton free or cofree def link"
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht fmap snd $ signOfNode (source xLk) dg
0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht _ -> liftR $ gsigManyUnion lg $ map (\ (_, m, _, _) -> cod m) mrs
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht-- | gathers information for an XLink using its source nodes signature
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtgetTypeAndMorphism :: LogicGraph -> DGraph -> XLink
9575d8e9e9211ccd22dbc9b86fa3e8941ee1d021Simon Ulbricht -> ResultT IO (Graph.Node, GMorphism, DGLinkType, XLink)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtgetTypeAndMorphism lg dg xLk = do
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht (i, sg1) <- signOfNode (source xLk) dg
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder (mr', lTp) <- getTypeAndMorphism1 lg dg sg1 xLk
9575d8e9e9211ccd22dbc9b86fa3e8941ee1d021Simon Ulbricht return (i, mr', lTp, xLk)
0223b75560eead55b7bbf11d18117a6819540983Christian MaedergetTypeAndMorphism1 :: LogicGraph -> DGraph -> G_sign -> XLink
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder -> ResultT IO (GMorphism, DGLinkType)
0223b75560eead55b7bbf11d18117a6819540983Christian MaedergetTypeAndMorphism1 lg dg sg1 xLk = do
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder (sg2, lTp) <- getTypeAndMorAux lg dg sg1 xLk
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder mr' <- liftR $ getGMorphism lg sg2 (mr_name xLk) (mapping xLk)
0223b75560eead55b7bbf11d18117a6819540983Christian Maeder return (mr', lTp)
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht{- depending on the type of the link, the correct DGLinkType and the signature
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbrichtfor the (external) morphism are extracted here -}
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtgetTypeAndMorAux :: LogicGraph -> DGraph -> G_sign -> XLink
f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbricht -> ResultT IO (G_sign, DGLinkType)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtgetTypeAndMorAux lg dg sg@(G_sign slid _ _) xLk = let
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht emptySig = G_sign slid (ext_empty_signature slid) startSigId
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht mkRtVAL sg' tp = return (sg', tp)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht cc = cons xLk
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht in case edgeTypeModInc $ lType xLk of
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht HidingDef -> mkRtVAL sg HidingDefLink
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht GlobalDef -> mkRtVAL sg $ localOrGlobalDef Global cc
c044cefcba5a9db7f8948b3778266971742b3dc6Simon Ulbricht HetDef -> mkRtVAL sg $ localOrGlobalDef Global cc
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht LocalDef -> mkRtVAL sg $ localOrGlobalDef Local cc
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht FreeOrCofreeDef fc -> do
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht (sg', mNd) <- case mr_source xLk of
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht Nothing -> return (emptySig, EmptyNode $ Logic slid)
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht Just ms -> do
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht (j, sg') <- signOfNode ms dg
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht return (sg', JustNode $ NodeSig j sg')
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht mkRtVAL sg' $ FreeOrCofreeDefLink fc mNd
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht ThmType thTp prv _ _ -> let
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht lStat = if not prv then LeftOpen
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht else Proven (rule xLk) $ prBasis xLk in
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht HidingThm -> do
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht (i', sg') <- case mr_source xLk of
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht Just ms -> signOfNode ms dg
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht Nothing -> fail "no morphism source declaration for HidingThmLink"
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht mr' <- liftR $ ginclusion lg sg' sg
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht mkRtVAL sg' $ HidingFreeOrCofreeThm Nothing i' mr' lStat
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht FreeOrCofreeThm fc -> do
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht (i', sg') <- case mr_source xLk of
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht Just ms -> signOfNode ms dg
a9ad67574dd71144680f8dedc285f6c4498a79f8Christian Maeder Nothing -> return (-1, emptySig)
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht mr' <- liftR $ ginclusion lg sg' sg
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht mkRtVAL sg' $ HidingFreeOrCofreeThm (Just fc) i' mr' lStat
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht GlobalOrLocalThm sc _ -> mkRtVAL sg
776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht $ ScopedLink sc (ThmLink lStat) $ mkConsStatus cc
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht{- | Generates and inserts a new DGNodeLab with a startoff-G_theory, an Element
7dc84ca1f3a253bcf947bd870f0303fffd37d3afSimon Ulbrichtand the the DGraphs Global Annotations. The caller has to ensure that the
7dc84ca1f3a253bcf947bd870f0303fffd37d3afSimon Ulbrichtchosen nodeId is not used in dgraph. -}
627e304eb081ce411768e08d3554d8efd52d4187Simon UlbrichtinsertNode :: HetcatsOpts -> LogicGraph -> Maybe G_theory -> XNode -> Graph.Node
627e304eb081ce411768e08d3554d8efd52d4187Simon Ulbricht -> (DGraph, LibEnv) -> ResultT IO (G_theory, DGraph, LibEnv)
19988126590a72905215aef1d7a67c646d99bdadSimon UlbrichtinsertNode opts lg mGt xNd n (dg, lv) = do
19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht (lbl, lv') <- generateNodeLab opts lg mGt xNd (dg, lv)
19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht return (dgn_theory lbl, insNodeDG (n, lbl) dg, lv')
19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht{- | generate nodelab with startoff-gtheory and xnode information (a new libenv
19988126590a72905215aef1d7a67c646d99bdadSimon Ulbrichtis returned in case it was extended due to reference node insertion) -}
19988126590a72905215aef1d7a67c646d99bdadSimon UlbrichtgenerateNodeLab :: HetcatsOpts -> LogicGraph -> Maybe G_theory -> XNode
19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht -> (DGraph, LibEnv) -> ResultT IO (DGNodeLab, LibEnv)
19988126590a72905215aef1d7a67c646d99bdadSimon UlbrichtgenerateNodeLab opts lg mGt xNd (dg, lv) = case xNd of
8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht -- Case #1: Reference Node
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht XRef nm rfNd rfLb spc -> do
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht (dg', lv') <- case Map.lookup (emptyLibName rfLb) lv of
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Just dg' -> return (dg', lv)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Nothing -> loadRefLib opts rfLb lv
5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian Maeder (i, gt) <- case lookupUniqueNodeByName rfNd dg' of
5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian Maeder Just (i, lbl) -> case signOf $ dgn_theory lbl of
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht G_sign lid sign sId -> return (i, noSensGTheory lid sign sId)
5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian Maeder Nothing -> fail $ "reference node " ++ rfNd ++ " was not found"
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht (gt', _) <- parseSpecs gt nm dg spc
857ab542e0b0bdf90e5a484ffe8df5a9c9c3e38fChristian Maeder let nInf = newRefInfo (emptyLibName rfLb) i
19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht return (newInfoNodeLab nm nInf gt', lv')
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht -- Case #2: Regular Node
01bf5a978a5dd7aecf7dea0ee2e1046922c64fd2Simon Ulbricht XNode nm lN (hid, syb) spc cc -> do
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht -- StartOff-Theory. Taken from LogicGraph for initial Nodes
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht gt0 <- case mGt of
7aa4fd41783d419ff516a23b767555d29ccda29fChristian Maeder Nothing -> fmap emptyTheory $ lookupLogic "generateNodeLab " lN lg
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Just gt -> return gt
454e349ad409df6c5fa9ba2b485243b8222dec41Simon Ulbricht -- hidden symbols use a different parser
d3d09eed06d615a26a9c930966f29cf2c149b876Simon Ulbricht gt1 <- if hid then parseHidden gt0 syb
d3d09eed06d615a26a9c930966f29cf2c149b876Simon Ulbricht else fmap fst $ parseSpecs gt0 nm dg syb
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht (gt2, syb') <- parseSpecs gt1 nm dg spc
454e349ad409df6c5fa9ba2b485243b8222dec41Simon Ulbricht -- the DGOrigin is also different for nodes with hidden symbols
1a088ae6e5ab1e717d720da7b517233286665073Christian Maeder lOrig <- if hid then let
1a088ae6e5ab1e717d720da7b517233286665073Christian Maeder syms = Set.difference (symsOfGsign $ signOf gt0)
1a088ae6e5ab1e717d720da7b517233286665073Christian Maeder $ symsOfGsign $ signOf gt2
454e349ad409df6c5fa9ba2b485243b8222dec41Simon Ulbricht in return $ DGRestriction NoRestriction syms
454e349ad409df6c5fa9ba2b485243b8222dec41Simon Ulbricht diffSig <- liftR $ homGsigDiff (signOf gt2) $ signOf gt0
454e349ad409df6c5fa9ba2b485243b8222dec41Simon Ulbricht return $ DGBasicSpec Nothing diffSig syb'
01bf5a978a5dd7aecf7dea0ee2e1046922c64fd2Simon Ulbricht return (newInfoNodeLab nm (newConsNodeInfo lOrig cc) gt2, lv)
857ab542e0b0bdf90e5a484ffe8df5a9c9c3e38fChristian MaederinsertFirstNode :: HetcatsOpts -> LogicGraph -> XNode -> (DGraph, LibEnv)
857ab542e0b0bdf90e5a484ffe8df5a9c9c3e38fChristian Maeder -> ResultT IO (DGraph, LibEnv)
627e304eb081ce411768e08d3554d8efd52d4187Simon UlbrichtinsertFirstNode opts lg xNd p@(dg', _) = let n = getNewNodeDG dg' in do
627e304eb081ce411768e08d3554d8efd52d4187Simon Ulbricht (_, dg, lv) <- insertNode opts lg Nothing xNd n p
857ab542e0b0bdf90e5a484ffe8df5a9c9c3e38fChristian Maeder return (dg, lv)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtparseHidden :: G_theory -> String -> ResultT IO G_theory
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtparseHidden gt s' = do
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht gs <- liftR $ deleteHiddenSymbols s' $ signOf gt
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht return $ case gs of
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht G_sign lid sg sId -> noSensGTheory lid sg sId
9deba6a2981f6b73fc57f27d525cabbb4f8bf484Simon UlbrichtparseSpecs :: G_theory -> NodeName -> DGraph -> String
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht -> ResultT IO (G_theory, Set G_symbol)
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtparseSpecs gt' nm dg spec = let
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht (response, msg) = extendByBasicSpec (globalAnnos dg) spec gt'
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht in case response of
042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Success gt'' _ smbs _ -> return (gt'', smbs)
9deba6a2981f6b73fc57f27d525cabbb4f8bf484Simon Ulbricht Failure _ -> fail $ "[ " ++ showName nm ++ " ]\n" ++ msg
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon UlbrichtloadRefLib :: HetcatsOpts -> String -> LibEnv -> ResultT IO (DGraph, LibEnv)
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon UlbrichtloadRefLib opts ln lv = do
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht mPath <- lift $ findFileOfLibNameAux opts { intype = DgXml } ln
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht case mPath of
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht Just path -> do
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht (ln', lv') <- readDGXmlR opts path lv
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht return (lookupDGraph ln' lv', lv')
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht _ -> fail $ "no file exists for reference library " ++ ln
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht-- | creates an entirely empty theory
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon UlbrichtemptyTheory :: AnyLogic -> G_theory
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon UlbrichtemptyTheory (Logic lid) =
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder G_theory lid Nothing (ext_empty_signature lid) startSigId noSens startThId
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht{- | A Node is looked up via its name in the DGraph. Returns the nodes
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbrichtsignature, but only if one single node is found for the respective name.
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon UlbrichtOtherwise an error is thrown. -}
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon UlbrichtsignOfNode :: String -> DGraph -> ResultT IO (Graph.Node, G_sign)
5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian MaedersignOfNode nd dg = case lookupUniqueNodeByName nd dg of
5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian Maeder Nothing -> fail $ "required node [" ++ nd ++ "] was not found in DGraph!"
5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian Maeder Just (j, lbl) ->
bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht return (j, signOf (dgn_theory lbl))