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

eqLEdge :: (DGLinkLab -> DGLinkLab -> Bool) -> LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
noPath :: LEdge DGLinkLab -> [LEdge DGLinkLab] -> Bool
tryToGetEdge :: LEdge DGLinkLab -> DGraph -> Maybe (LEdge DGLinkLab)
insertDGLEdge :: LEdge DGLinkLab -> DGraph -> DGraph
getEdgeId :: LEdge DGLinkLab -> EdgeId
getAllPathsOfTypeFromGoalList :: DGraph -> (DGLinkType -> Bool) -> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
getAllPathsOfType :: DGraph -> (DGLinkType -> Bool) -> [[LEdge DGLinkLab]]
realMorphism :: DGLinkLab -> Maybe GMorphism
calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism
filterPathsByMorphism :: GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
getAllLocGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeBetween :: DGraph -> (DGLinkType -> Bool) -> Node -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeFrom :: DGraph -> Node -> [[LEdge DGLinkLab]]
checkEdgeIds :: DGraph -> Maybe [EdgeId]
selectProofBasis :: DGraph -> LEdge DGLinkLab -> [[LEdge DGLinkLab]] -> ProofBasis
selectProofBasisAux :: Map EdgeId (Set EdgeId) -> LEdge DGLinkLab -> [[LEdge DGLinkLab]] -> ProofBasis
calculateProofBasis :: Map EdgeId (Set EdgeId) -> [LEdge DGLinkLab] -> ProofBasis
invalidateProof :: DGLinkType -> DGLinkType
adoptEdges :: DGraph -> Node -> Node -> DGraph
adoptEdgesAux :: Node -> Bool -> LEdge DGLinkLab -> LEdge DGLinkLab
getAllOpenNodeGoals :: [DGNodeLab] -> [DGNodeLab]
hidingLabelWarning :: DGNodeLab -> String
addHasInHidingWarning :: DGraph -> Node -> String
hidingWarning :: [String]

other methods on edges

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

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

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

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 Source #

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

getEdgeId :: LEdge DGLinkLab -> EdgeId Source #

get the edge id out of a given edge

methods that calculate paths of certain types

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

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

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

realMorphism :: DGLinkLab -> Maybe GMorphism Source #

morphisms of (co)free definitions are identities

calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism Source #

determines the morphism of a given path

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

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

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

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]] Source #

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

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

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

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

return all non-cyclic paths starting from the given node

methods to check and select proof basis

checkEdgeIds :: DGraph -> Maybe [EdgeId] Source #

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

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 Source #

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 Source #

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 Source #

adoptEdges :: DGraph -> Node -> Node -> DGraph Source #

adopts the edges of the old node to the new node

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

auxiliary method for adoptEdges

getAllOpenNodeGoals :: [DGNodeLab] -> [DGNodeLab] Source #

hidingLabelWarning :: DGNodeLab -> String Source #

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

addHasInHidingWarning :: DGraph -> Node -> String Source #

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

hidingWarning :: [String] Source #