{-|

Module : $Header$

Copyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2004

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : jfgerken@tzi.de

Stability : provisional

Portability : non-portable(Logic)

utility functions for edges of a development graphs.

-}

module Proofs.EdgeUtils where

import Data.List(nub)

import Logic.Logic

import Logic.Grothendieck

import Static.DevGraph

import Static.DGToSpec

import Data.Graph.Inductive.Graph

import qualified Common.Lib.Map as Map

import Proofs.Proofs

delLEdge :: LEdge DGLinkLab -> DGraph -> DGraph

delLEdge (v, w, l) g = case match v g of

(Just(p, v', l', s), g') -> (p, v', l', filter (/= (l, w)) s) & g'

_ -> g

-- -------------------------------------

-- methods to check the type of an edge

-- -------------------------------------

isProven :: LEdge DGLinkLab -> Bool

isProven edge = isGlobalDef edge || isLocalDef edge

|| isProvenGlobalThm edge || isProvenLocalThm edge

|| isProvenHidingThm edge

isGlobalEdge :: LEdge DGLinkLab -> Bool

isGlobalEdge edge = isGlobalDef edge || isGlobalThm edge

isLocalEdge :: LEdge DGLinkLab -> Bool

isLocalEdge edge = isLocalDef edge || isLocalThm edge

isGlobalThm :: LEdge DGLinkLab -> Bool

isGlobalThm edge = isProvenGlobalThm edge || isUnprovenGlobalThm edge

isLocalThm :: LEdge DGLinkLab -> Bool

isLocalThm edge = isProvenLocalThm edge || isUnprovenLocalThm edge

isProvenGlobalThm :: LEdge DGLinkLab -> Bool

isProvenGlobalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(GlobalThm (Proven _ _) _ _) -> True

_ -> False

isUnprovenGlobalThm :: LEdge DGLinkLab -> Bool

isUnprovenGlobalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(GlobalThm Static.DevGraph.Open _ _) -> True

_ -> False

isProvenLocalThm :: LEdge DGLinkLab -> Bool

isProvenLocalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(LocalThm (Proven _ _) _ _) -> True

_ -> False

isUnprovenLocalThm :: LEdge DGLinkLab -> Bool

isUnprovenLocalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(LocalThm (Static.DevGraph.Open) _ _) -> True

_ -> False

isHidingEdge :: LEdge DGLinkLab -> Bool

isHidingEdge edge = isHidingDef edge || isHidingThm edge

isHidingDef :: LEdge DGLinkLab -> Bool

isHidingDef (_,_,edgeLab) =

case dgl_type edgeLab of

HidingDef -> True

_ -> False

isHidingThm :: LEdge DGLinkLab -> Bool

isHidingThm edge = isProvenHidingThm edge || isUnprovenHidingThm edge

isProvenHidingThm :: LEdge DGLinkLab -> Bool

isProvenHidingThm (_,_,edgeLab) =

case dgl_type edgeLab of

(HidingThm _ (Proven _ _)) -> True

_ -> False

isUnprovenHidingThm :: LEdge DGLinkLab -> Bool

isUnprovenHidingThm (_,_,edgeLab) =

case dgl_type edgeLab of

(HidingThm _ Static.DevGraph.Open) -> True

_ -> False

-- ----------------------------------------------------------------------------

-- other methods on edges

-- ----------------------------------------------------------------------------

{- returns true, if an identical edge is already in the graph or marked to be inserted,

false otherwise-}

isDuplicate :: LEdge DGLinkLab -> DGraph -> [DGChange] -> Bool

isDuplicate newEdge dgraph changes =

elem (InsertEdge newEdge) changes || elem newEdge (labEdges dgraph)

{- returns true, if the given edge is duplicate or

if there already exists a parallel path,

which starts with a localThmEdge to one of the startnodes in 'otherNewEdge'

and has the same morphism as the given edge,

false otherwise -}

isRedundant :: LEdge DGLinkLab -> DGraph -> [DGChange]

->[(Node, [LEdge DGLinkLab])] -> Bool

isRedundant newEdge@(src,_,label) dgraph changes otherNewEdges =

isDuplicate newEdge dgraph changes

|| elem (Just (dgl_morphism label)) morphismsOfParallelPaths

where

localThmEdgesToOtherSources =

[outEdge|outEdge@(_,tgt,_) <- out dgraph src,

elem tgt (map fst otherNewEdges)

&& isLocalThm outEdge]

parallelPaths

= concat (map (combineSucceedingEdges otherNewEdges)

localThmEdgesToOtherSources)

morphismsOfParallelPaths = map calculateMorphismOfPath parallelPaths

{- combines the given edge with each of those given paths that start

with the target node of the edge-}

combineSucceedingEdges :: [(Node,[LEdge DGLinkLab])] -> LEdge DGLinkLab

-> [[LEdge DGLinkLab]]

combineSucceedingEdges [] _ = []

combineSucceedingEdges ((src,path):paths) edge@(_,tgt,_) =

if tgt == src

then ((edge:path)):(combineSucceedingEdges paths edge)

else combineSucceedingEdges paths edge

isIdentityEdge :: LEdge DGLinkLab -> LibEnv -> DGraph -> Bool

isIdentityEdge (src,tgt,edgeLab) libEnv dgraph =

if isDGRef nodeLab then

case Map.lookup (dgn_libname nodeLab) libEnv of

Just (_,_,refDgraph) -> isIdentityEdge (dgn_node nodeLab,tgt,edgeLab) libEnv refDgraph

Nothing -> False

else if src == tgt && (dgl_morphism edgeLab) == (ide Grothendieck (dgn_sign nodeLab)) then True else False

where nodeLab = lab' (context dgraph src)

{- returns the DGLinkLab of the given LEdge -}

getLabelOfEdge :: (LEdge b) -> b

getLabelOfEdge (_,_,label) = label

-- ----------------------------------------------

-- methods that calculate paths of certain types

-- ----------------------------------------------

{- returns a list of all proven global paths of the given morphism between

the given source and target node-}

getAllGlobPathsOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node

-> [[LEdge DGLinkLab]]

getAllGlobPathsOfMorphismBetween dgraph morphism src tgt =

filterPathsByMorphism morphism allPaths

where

allPaths = getAllGlobPathsBetween dgraph src tgt

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

given one-}

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

-> [[LEdge DGLinkLab]]

filterPathsByMorphism morphism paths =

[path| path <- paths, (calculateMorphismOfPath path) == (Just morphism)]

{- returns a list of all paths to the given node

that consist of globalDef edge only

or

that consist of a localDef or hidingDef edge

followed by any number of globalDef edges -}

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

-> [(Node, [LEdge DGLinkLab])]

getAllLocOrHideGlobDefPathsTo =

getAllGlobDefPathsBeginningWithTypesTo

([isLocalDef, isHidingDef]::[LEdge DGLinkLab -> Bool])

{- returns a list of all paths to the given node

that consist of globalDef edges only

or

that consist of a localDef edge followed by any number of globalDef edges -}

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

-> [(Node, [LEdge DGLinkLab])]

getAllLocGlobDefPathsTo = getAllGlobDefPathsBeginningWithTypesTo

([isLocalDef]::[LEdge DGLinkLab -> Bool])

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

-> [(Node, [LEdge DGLinkLab])]

getAllPathsBeginningWithHidingDefTo dgraph node path =

resultPath ++

(concat ( [getAllPathsBeginningWithHidingDefTo

dgraph (getSourceNode edge) (edge:path) |

edge <- nextEdges]))

where

inEdges = inn dgraph node

nextEdges = [edge| edge <- inEdges, not (elem edge path)]

resultPath =

if ((not (null path)) && (isHidingDef (head path)))

then [(node,path)] else []

{- returns all paths consisting of global edges only

or

of one local edge followed by any number of global edges-}

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

getAllLocGlobPathsBetween dgraph src tgt =

locGlobPaths ++ globPaths

where

outEdges = out dgraph src

locEdges = [(edge,target)|edge@(_,target,_) <-

(filterByTypes [isLocalEdge] outEdges)]

locGlobPaths = (concat [map ([edge]++)

(getAllPathsOfTypesBetween dgraph [isGlobalEdge] node tgt [])|

(edge,node) <- locEdges])

globPaths = getAllPathsOfTypesBetween dgraph [isGlobalEdge] src tgt []

{- returns all paths of globalDef edges or globalThm edges

between the given source and target node -}

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

getAllGlobPathsBetween dgraph src tgt =

getAllPathsOfTypesBetween dgraph [isGlobalDef,isGlobalThm] src tgt []

{- gets all paths consisting of local/global thm/def edges

of the given morphism -}

getAllThmDefPathsOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node

-> [[LEdge DGLinkLab]]

getAllThmDefPathsOfMorphismBetween dgraph morphism src tgt =

filterPathsByMorphism morphism allPaths

where

allPaths = getAllPathsOfTypesBetween dgraph types src tgt []

types =

[isGlobalThm,

isProvenLocalThm,

isProvenLocalThm,

isUnprovenLocalThm,

isGlobalDef,

isLocalDef]

{- returns all paths of globalDef edges between the given source and

target node -}

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

getAllGlobDefPathsBetween dgraph src tgt =

getAllPathsOfTypeBetween dgraph isGlobalDef src tgt

{- returns all paths consiting of edges of the given type between the

given node -}

getAllPathsOfTypeBetween :: DGraph -> (LEdge DGLinkLab -> Bool) -> Node

-> Node -> [[LEdge DGLinkLab]]

getAllPathsOfTypeBetween dgraph isType src tgt =

getAllPathsOfTypesBetween dgraph (isType:[]) src tgt []

{- returns all paths consisting of edges of the given types between

the given nodes -}

getAllPathsOfTypesBetween :: DGraph -> [LEdge DGLinkLab -> Bool] -> Node

-> Node -> [LEdge DGLinkLab]

-> [[LEdge DGLinkLab]]

getAllPathsOfTypesBetween dgraph types src tgt path =

[edge:path| edge <- edgesFromSrc]

++ (concat

[getAllPathsOfTypesBetween dgraph types src nextTgt (edge:path)|

(edge,nextTgt) <- nextStep] )

where

inGoingEdges = inn dgraph tgt

edgesOfTypes =

[edge| edge <- filterByTypes types inGoingEdges, notElem edge path]

edgesFromSrc =

[edge| edge@(source,_,_) <- edgesOfTypes, source == src]

nextStep =

[(edge, source)| edge@(source,_,_) <- edgesOfTypes, source /= src]

{-

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

getAllPathsFrom = getAllPathsFromAux []

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

-> [[LEdge DGLinkLab]]

getAllPathsFromAux path dgraph src =

[path ++ [edge]| edge <- edgesFromSrc, notElem edge path]

++(concat

[getAllPathsFromAux (path ++ [edge]) dgraph nextSrc|

(edge,nextSrc) <- nextStep])

where

edgesFromSrc = out dgraph src

nextStep = [(edge,tgt)| edge@(_,tgt,_) <- edgesFromSrc,

tgt /= src && notElem edge path] -}

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

getAllPathsOfTypeFrom = getAllPathsOfTypeFromAux []

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

-> (LEdge DGLinkLab -> Bool) -> [[LEdge DGLinkLab]]

getAllPathsOfTypeFromAux path dgraph src isType =

[path ++ [edge]| edge <- edgesFromSrc, notElem edge path && isType edge]

++(concat

[getAllPathsOfTypeFromAux (path ++ [edge]) dgraph nextSrc isType|

(edge,nextSrc) <- nextStep])

where

edgesFromSrc = out dgraph src

nextStep = [(edge,tgt)| edge@(_,tgt,_) <- edgesFromSrc,

tgt /= src && notElem edge path && isType edge]

-- ----------------------------------------------------------------------------

-- methods to determine the labels of the inserted edges in the given dgchange

-- ----------------------------------------------------------------------------

{- filters the list of changes for insertions of edges and returns the label

of one of these; or Nothing if no insertion was found -}

getLabelsOfInsertedEdges :: [DGChange] -> [DGLinkLab]

getLabelsOfInsertedEdges changes =

[label | (_,_,label) <- getInsertedEdges changes]

{- returns all insertions of edges from the given list of changes -}

getInsertedEdges :: [DGChange] -> [LEdge DGLinkLab]

getInsertedEdges [] = []

getInsertedEdges (change:list) =

case change of

(InsertEdge edge) -> edge:(getInsertedEdges list)

_ -> getInsertedEdges list

-- ----------------------------------------

-- methods to check and select proof basis

-- ----------------------------------------

{- determines all proven paths in the given list and tries to selet 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 -}

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

selectProofBasis label paths =

if null provenProofBasis then selectProofBasisAux label unprovenPaths

else provenProofBasis

where

provenPaths = filterProvenPaths paths

provenProofBasis = selectProofBasisAux label provenPaths

unprovenPaths = [path | path <- paths, notElem path provenPaths]

{- 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 -}

selectProofBasisAux :: DGLinkLab -> [[LEdge DGLinkLab]] -> [DGLinkLab]

selectProofBasisAux _ [] = []

selectProofBasisAux label (path:list) =

if notProofCycle label path then nub (calculateProofBasis path)

else selectProofBasisAux label list

{- calculates the proofBasis of the given path,

i.e. the list of all DGLinkLabs the proofs of the edges contained in the path

are based on, plus the DGLinkLabs of the edges themselves;

duplicates are not removed here, but in the calling method

selectProofBasisAux -}

calculateProofBasis :: [LEdge DGLinkLab] -> [DGLinkLab]

calculateProofBasis [] = []

calculateProofBasis ((_,_,label):edges) =

label:((getProofBasis label)++(calculateProofBasis edges))

{- returns the proofBasis contained in the given DGLinkLab -}

getProofBasis :: DGLinkLab -> [DGLinkLab]

getProofBasis label =

case dgl_type label of

(GlobalThm (Proven _ proofBasis) _ _) -> proofBasis

(LocalThm (Proven _ proofBasis) _ _) -> proofBasis

_ -> []

{- returns all proven paths from the given list -}

filterProvenPaths :: [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]

filterProvenPaths [] = []

filterProvenPaths (path:list) =

if (and [isProven edge| edge <- path]) then path:(filterProvenPaths list)

else filterProvenPaths list

{- opposite of isProofCycle -}

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

notProofCycle label = not.(isProofCycle label)

{- checks if the given label is contained in the ProofBasis of one of the

edges of the given path -}

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

isProofCycle _ [] = False

isProofCycle label (edge:path) =

if (elemOfProofBasis label edge) then True else (isProofCycle label path)

{- checks if the given label is contained in the ProofBasis of the given

edge -}

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

elemOfProofBasis label (_,_,dglink) =

case dgl_type dglink of

(GlobalThm (Proven _ proofBasis) _ _) -> elem label proofBasis

(LocalThm (Proven _ proofBasis) _ _) -> elem label proofBasis

_ -> False