Copyright	(c) Simon Ulbricht, DFKI GmbH 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	tekknix@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable (DevGraph)
Safe Haskell	None

Static.FromXml

Description

create new or extend a Development Graph in accordance with an XML input

Synopsis

Documentation

readDGXml :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))

top-level function

readDGXmlR :: HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (LibName, LibEnv)

main function; receives a FilePath and calls fromXml upon that path, using an initial LogicGraph.

rebuiltDgXml :: HetcatsOpts -> LibEnv -> Element -> ResultT IO (LibName, LibEnv)

call rebuiltDG with only a LibEnv and an Xml-Element

rebuiltDG :: HetcatsOpts -> LogicGraph -> XGraph -> LibEnv -> ResultT IO (DGraph, LibEnv)

reconstructs the Development Graph via a previously created XGraph- structure.

insertStep :: HetcatsOpts -> LogicGraph -> XNode -> [XLink] -> (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv)

inserts a new node as well as all definition links pointing at that node

insertLink :: LogicGraph -> Node -> G_sign -> DGraph -> (Node, GMorphism, DGLinkType, XLink) -> ResultT IO DGraph

insertThmLinks :: LogicGraph -> DGraph -> EdgeMap -> ResultT IO DGraph

inserts theorem links

insertTarThmLinks :: LogicGraph -> Node -> G_sign -> DGraph -> Map String [XLink] -> ResultT IO DGraph

finalizeLink :: LogicGraph -> XLink -> GMorphism -> G_sign -> DGLinkType -> ResultT IO DGLinkLab

given a links intermediate morphism and its target nodes signature, this function calculates the final morphism for this link

getSigForXNode :: LogicGraph -> DGraph -> [(Node, GMorphism, DGLinkType, XLink)] -> ResultT IO G_sign

based upon the morphisms of ingoing deflinks, calculate the initial signature to be used for node insertion

getTypeAndMorphism :: LogicGraph -> DGraph -> XLink -> ResultT IO (Node, GMorphism, DGLinkType, XLink)

gathers information for an XLink using its source nodes signature

getTypeAndMorphism1 :: LogicGraph -> DGraph -> G_sign -> XLink -> ResultT IO (GMorphism, DGLinkType)

getTypeAndMorAux :: LogicGraph -> DGraph -> G_sign -> XLink -> ResultT IO (G_sign, DGLinkType)

insertNode :: HetcatsOpts -> LogicGraph -> Maybe G_theory -> XNode -> Node -> (DGraph, LibEnv) -> ResultT IO (G_theory, DGraph, LibEnv)

Generates and inserts a new DGNodeLab with a startoff-G_theory, an Element and the the DGraphs Global Annotations. The caller has to ensure that the chosen nodeId is not used in dgraph.

generateNodeLab :: HetcatsOpts -> LogicGraph -> Maybe G_theory -> XNode -> (DGraph, LibEnv) -> ResultT IO (DGNodeLab, LibEnv)

generate nodelab with startoff-gtheory and xnode information (a new libenv is returned in case it was extended due to reference node insertion)

insertFirstNode :: HetcatsOpts -> LogicGraph -> XNode -> (DGraph, LibEnv) -> ResultT IO (DGraph, LibEnv)

parseHidden :: G_theory -> String -> ResultT IO G_theory

parseSpecs :: G_theory -> NodeName -> DGraph -> String -> ResultT IO (G_theory, Set G_symbol)

loadRefLib :: HetcatsOpts -> String -> LibEnv -> ResultT IO (DGraph, LibEnv)

emptyTheory :: AnyLogic -> G_theory

creates an entirely empty theory

signOfNode :: String -> DGraph -> ResultT IO (Node, G_sign)

A Node is looked up via its name in the DGraph. Returns the nodes signature, but only if one single node is found for the respective name. Otherwise an error is thrown.