Copyright	(c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable(Logic)
Safe Haskell	None

Proofs.EdgeUtils

Contents

other methods on edges
methods that calculate paths of certain types
methods to check and select proof basis

Description

utility functions for edges of development graphs

Synopsis

other methods on edges

eqLEdge :: (DGLinkLab -> DGLinkLab -> Bool) -> LEdge DGLinkLab -> LEdge DGLinkLab -> Bool

noPath :: LEdge DGLinkLab -> [LEdge DGLinkLab] -> Bool

tryToGetEdge :: LEdge DGLinkLab -> DGraph -> Maybe (LEdge DGLinkLab)

try to get the given edge from the given DGraph or the given list of DGChange to advoid duplicate inserting of an edge.

insertDGLEdge :: LEdge DGLinkLab -> DGraph -> DGraph

try to insert an edge into the given dgraph, if the edge exists, the edge's id should match, too.

getEdgeId :: LEdge DGLinkLab -> EdgeId

get the edge id out of a given edge

methods that calculate paths of certain types

getAllPathsOfTypeFromGoalList :: DGraph -> (DGLinkType -> Bool) -> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]

getAllPathsOfType :: DGraph -> (DGLinkType -> Bool) -> [[LEdge DGLinkLab]]

returns all paths consisting of edges of the given type in the given development graph

realMorphism :: DGLinkLab -> Maybe GMorphism

morphisms of (co)free definitions are identities

calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism

determines the morphism of a given path

filterPathsByMorphism :: GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]

returns all paths from the given list whose morphism is equal to the given one

getAllLocGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]

returns all paths consisting of global edges only or of one local edge followed by any number of global edges

getAllGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]

returns all paths of globalDef edges or globalThm edges between the given source and target node

getAllPathsOfTypeBetween :: DGraph -> (DGLinkType -> Bool) -> Node -> Node -> [[LEdge DGLinkLab]]

returns all cyclic paths consisting of edges of the given type between the given two nodes

getAllPathsOfTypeFrom :: DGraph -> Node -> [[LEdge DGLinkLab]]

return all non-cyclic paths starting from the given node

methods to check and select proof basis

checkEdgeIds :: DGraph -> Maybe [EdgeId]

selectProofBasis :: DGraph -> LEdge DGLinkLab -> [[LEdge DGLinkLab]] -> ProofBasis

determines all proven paths in the given list and tries to select a proof basis from these (s. selectProofBasisAux); if this fails the same is done for the rest of the given paths, i.e. for the unproven ones

selectProofBasisAux :: Map EdgeId (Set EdgeId) -> LEdge DGLinkLab -> [[LEdge DGLinkLab]] -> ProofBasis

selects the first path that does not form a proof cycle with the given label (if such a path exits) and returns the labels of its edges

calculateProofBasis :: Map EdgeId (Set EdgeId) -> [LEdge DGLinkLab] -> ProofBasis

calculates the proofBasis of the given path, i.e. (recursively) close the list of DGLinkLabs under the relation 'is proved using'. If a DGLinkLab has proof status LeftOpen, look up in the development graph for its current status

invalidateProof :: DGLinkType -> DGLinkType

adoptEdges :: DGraph -> Node -> Node -> DGraph

adopts the edges of the old node to the new node

adoptEdgesAux :: Node -> Bool -> LEdge DGLinkLab -> LEdge DGLinkLab

auxiliary method for adoptEdges

getAllOpenNodeGoals :: [DGNodeLab] -> [DGNodeLab]

hidingLabelWarning :: DGNodeLab -> String

return a warning text if the given label has incoming hiding edge, otherwise just an empty string.

addHasInHidingWarning :: DGraph -> Node -> String

return a warning text if the given node has incoming hiding edge, otherwise just an empty string.

hidingWarning :: [String]