da9cd70c94407d05ad340bdcf620adb579b21e36sin{- |

da9cd70c94407d05ad340bdcf620adb579b21e36sinModule : $Header$

da9cd70c94407d05ad340bdcf620adb579b21e36sinCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006

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

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sinMaintainer : jfgerken@tzi.de

da9cd70c94407d05ad340bdcf620adb579b21e36sinStability : provisional

da9cd70c94407d05ad340bdcf620adb579b21e36sinPortability : non-portable(DevGraph)

8cf870d281dc8c242f083d14dfef05f24aa5fceeJnRouvignac

8cf870d281dc8c242f083d14dfef05f24aa5fceeJnRouvignacglobal proofs in development graphs.

da9cd70c94407d05ad340bdcf620adb579b21e36sin Follows Sect. IV:4.4 of the CASL Reference Manual.

da9cd70c94407d05ad340bdcf620adb579b21e36sin-}

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sin{-

8cf870d281dc8c242f083d14dfef05f24aa5fceeJnRouvignactodo for Jorina:

8cf870d281dc8c242f083d14dfef05f24aa5fceeJnRouvignac

8cf870d281dc8c242f083d14dfef05f24aa5fceeJnRouvignac - bei GlobDecomp hinzuf�gen:

8cf870d281dc8c242f083d14dfef05f24aa5fceeJnRouvignac zus�tzlich alle Pfade K<--theta-- M --sigma-->N in den aktuellen

da9cd70c94407d05ad340bdcf620adb579b21e36sin Knoten N, die mit einem HidingDef anfangen, und danach nur GlobalDef

da9cd70c94407d05ad340bdcf620adb579b21e36sin theta ist der Signaturmorphismus des HidingDef's (geht "falsch rum")

da9cd70c94407d05ad340bdcf620adb579b21e36sin sigma ist die Komposition der Signaturmorphismen auf dem restl. Pfad

da9cd70c94407d05ad340bdcf620adb579b21e36sin f�r jeden solchen Pfad: einen HidingThm theta einf�gen. sigma ist

da9cd70c94407d05ad340bdcf620adb579b21e36sin der normale Morphismus (wie bei jedem anderen Link)

da9cd70c94407d05ad340bdcf620adb579b21e36sin siehe auch Seite 302 des CASL Reference Manual

da9cd70c94407d05ad340bdcf620adb579b21e36sin-}

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sinmodule Proofs.Global (globSubsume, globDecomp, globDecompAux, globDecompFromList, globSubsumeFromList) where

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sinimport Data.Graph.Inductive.Graph

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sinimport Logic.Grothendieck

da9cd70c94407d05ad340bdcf620adb579b21e36sinimport Static.DevGraph

da9cd70c94407d05ad340bdcf620adb579b21e36sinimport Static.DGToSpec

da9cd70c94407d05ad340bdcf620adb579b21e36sinimport Syntax.AS_Library

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sinimport Proofs.EdgeUtils

da9cd70c94407d05ad340bdcf620adb579b21e36sinimport Proofs.StatusUtils

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sin-- ---------------------

da9cd70c94407d05ad340bdcf620adb579b21e36sin-- global decomposition

da9cd70c94407d05ad340bdcf620adb579b21e36sin-- ---------------------

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sin{- apply rule GlobDecomp to all global theorem links in the current DG

da9cd70c94407d05ad340bdcf620adb579b21e36sin current DG = DGm

da9cd70c94407d05ad340bdcf620adb579b21e36sin add to proof status the pair ([GlobDecomp e1,...,GlobDecomp en],DGm+1)

da9cd70c94407d05ad340bdcf620adb579b21e36sin where e1...en are the global theorem links in DGm

da9cd70c94407d05ad340bdcf620adb579b21e36sin DGm+1 results from DGm by application of GlobDecomp e1,...,GlobDecomp en -}

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sin{- applies global decomposition to the list of edges given (global theorem edges)

da9cd70c94407d05ad340bdcf620adb579b21e36sin if possible, if empty list is given then to all unproven global theorems -}

da9cd70c94407d05ad340bdcf620adb579b21e36singlobDecompFromList :: LIB_NAME -> [LEdge DGLinkLab] -> LibEnv -> LibEnv

da9cd70c94407d05ad340bdcf620adb579b21e36singlobDecompFromList ln globalThmEdges proofStatus =

da9cd70c94407d05ad340bdcf620adb579b21e36sin let dgraph = lookupDGraph ln proofStatus

da9cd70c94407d05ad340bdcf620adb579b21e36sin finalGlobalThmEdges = filter isUnprovenGlobalThm globalThmEdges

da9cd70c94407d05ad340bdcf620adb579b21e36sin (newDGraph, newHistoryElem)= globDecompAux dgraph finalGlobalThmEdges ([],[])

da9cd70c94407d05ad340bdcf620adb579b21e36sin in mkResultProofStatus ln proofStatus newDGraph newHistoryElem

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sin{- applies global decomposition to all unproven global theorem edges

da9cd70c94407d05ad340bdcf620adb579b21e36sin if possible -}

da9cd70c94407d05ad340bdcf620adb579b21e36singlobDecomp ::LIB_NAME -> LibEnv -> LibEnv

da9cd70c94407d05ad340bdcf620adb579b21e36singlobDecomp ln proofStatus =

da9cd70c94407d05ad340bdcf620adb579b21e36sin let dgraph = lookupDGraph ln proofStatus

da9cd70c94407d05ad340bdcf620adb579b21e36sin globalThmEdges = filter isUnprovenGlobalThm (labEdges dgraph)

da9cd70c94407d05ad340bdcf620adb579b21e36sin in globDecompFromList ln globalThmEdges proofStatus

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sin

da9cd70c94407d05ad340bdcf620adb579b21e36sin

{- applies global decomposition to all unproven global theorem edges

if possible -}

--globDecomp :: LIB_NAME -> LibEnv -> LibEnv

--globDecomp ln proofStatus =

-- let dgraph = lookupDGraph ln proofStatus

-- globalThmEdges = filter isUnprovenGlobalThm (labEdges dgraph)

-- (newDGraph, newHistoryElem) = globDecompAux dgraph globalThmEdges ([],[])

-- (finalDGraph, finalHistoryElem)

-- = removeSuperfluousInsertions newDGraph newHistoryElem

-- in mkResultProofStatus ln proofStatus newDGraph newHistoryElem

--finalDGraph finalHistoryElem

{- removes all superfluous insertions from the list of changes as well as

from the development graph (i.e. insertions of edges that are

equivalent to edges or paths resulting from the other insertions) -}

removeSuperfluousInsertions :: DGraph -> ([DGRule],[DGChange])

-> (DGraph,([DGRule],[DGChange]))

removeSuperfluousInsertions dgraph (rules,changes)

= (newDGraph,(rules,newChanges))

where

localThms = [edge | (InsertEdge edge)

<- filter isLocalThmInsertion changes]

(newDGraph, localThmsToInsert)

= removeSuperfluousEdges dgraph localThms

newChanges = (filter (not.isLocalThmInsertion) changes)

++ [InsertEdge edge | edge <- localThmsToInsert]

{- auxiliary function for globDecomp (above)

actual implementation -}

globDecompAux :: DGraph -> [LEdge DGLinkLab] -> ([DGRule],[DGChange])

-> (DGraph,([DGRule],[DGChange]))

globDecompAux dgraph [] historyElem = (dgraph, historyElem)

globDecompAux dgraph (edge:list) historyElem =

globDecompAux newDGraph list newHistoryElem

where

(newDGraph, newChanges) = globDecompForOneEdge dgraph edge

newHistoryElem = (((GlobDecomp edge):(fst historyElem)),

(newChanges++(snd historyElem)))

-- applies global decomposition to a single edge

globDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> (DGraph,[DGChange])

globDecompForOneEdge dgraph edge =

globDecompForOneEdgeAux dgraph edge [] paths

where

source = getSourceNode edge

defEdgesToSource = [e | e <- labEdges dgraph,

isDefEdge e && (getTargetNode e) == source]

paths = map (\e -> [e,edge]) defEdgesToSource ++ [[edge]]

--getAllLocOrHideGlobDefPathsTo dgraph (getSourceNode edge) []

-- paths = [(node, path++(edge:[]))| (node,path) <- pathsToSource]

{- auxiliary funktion for globDecompForOneEdge (above)

actual implementation -}

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

[[LEdge DGLinkLab]] -> (DGraph,[DGChange])

{- if the list of paths is empty from the beginning, nothing is done

otherwise the unprovenThm edge is replaced by a proven one -}

globDecompForOneEdgeAux dgraph edge@(source,target,edgeLab) changes [] =

-- if null changes then (dgraph, changes)

-- else

if isDuplicate provenEdge dgraph changes

then (deLLEdge edge dgraph,

((DeleteEdge edge):changes))

else ((insEdge provenEdge (deLLEdge edge dgraph)),

((DeleteEdge edge):((InsertEdge provenEdge):changes)))

where

(GlobalThm _ conservativity conservStatus) = (dgl_type edgeLab)

proofBasis = getInsertedEdges changes

provenEdge = (source,

target,

DGLink {dgl_morphism = dgl_morphism edgeLab,

dgl_type =

(GlobalThm (Proven (GlobDecomp edge) proofBasis)

conservativity conservStatus),

dgl_origin = DGProof}

)

-- for each path an unproven localThm edge is inserted

globDecompForOneEdgeAux dgraph edge@(_,target,_) changes

(path:list) =

if isDuplicate newEdge dgraph changes-- list

then globDecompForOneEdgeAux dgraph edge changes list

else globDecompForOneEdgeAux newGraph edge newChanges list

where

hd = head path

isHiding = not (null path) && isHidingDef hd

morphismPath = if isHiding then tail path else path

morphism = case calculateMorphismOfPath morphismPath of

Just morph -> morph

Nothing ->

error "globDecomp: could not determine morphism of new edge"

newEdge = if isHiding then hidingEdge

else if isGlobalDef hd then globalEdge else localEdge

node = getSourceNode hd

hidingEdge =

(node,

target,

DGLink {dgl_morphism = morphism,

dgl_type = HidingThm (dgl_morphism $

getLabelOfEdge hd) LeftOpen,

dgl_origin = DGProof})

globalEdge = (node,

target,

DGLink {dgl_morphism = morphism,

dgl_type = (GlobalThm LeftOpen

None LeftOpen),

dgl_origin = DGProof}

)

localEdge = (node,

target,

DGLink {dgl_morphism = morphism,

dgl_type = (LocalThm LeftOpen

None LeftOpen),

dgl_origin = DGProof}

)

newGraph = insEdge newEdge dgraph

newChanges = ((InsertEdge newEdge):changes)

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

-- global subsumption

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

globSubsumeFromList :: LIB_NAME -> [LEdge DGLinkLab] -> LibEnv -> LibEnv

globSubsumeFromList ln globalThmEdges libEnv=

let dgraph = lookupDGraph ln libEnv

finalGlobalThmEdges = filter isUnprovenGlobalThm globalThmEdges

(nextDGraph, nextHistoryElem) =

globSubsumeAux libEnv dgraph ([],[]) finalGlobalThmEdges

in mkResultProofStatus ln libEnv nextDGraph nextHistoryElem

globSubsume :: LIB_NAME -> LibEnv -> LibEnv

globSubsume ln libEnv =

let dgraph = lookupDGraph ln libEnv

globalThmEdges = filter isUnprovenGlobalThm (labEdges dgraph)

in globSubsumeFromList ln globalThmEdges libEnv

-- applies global subsumption to all unproven global theorem edges if possible

--globSubsume :: LIB_NAME -> LibEnv -> LibEnv

--globSubsume ln libEnv =

-- let dgraph = lookupDGraph ln libEnv

-- globalThmEdges = filter isUnprovenGlobalThm (labEdges dgraph)

-- {- the previous 'nub' is (probably) not needed, because it is

-- (or should be) checked for duplicate edge insertions -}

-- (nextDGraph, nextHistoryElem) =

-- globSubsumeAux libEnv dgraph ([],[]) globalThmEdges

-- in mkResultProofStatus ln libEnv nextDGraph nextHistoryElem

{- auxiliary function for globSubsume (above)

the actual implementation -}

globSubsumeAux :: LibEnv -> DGraph -> ([DGRule],[DGChange]) ->

[LEdge DGLinkLab] -> (DGraph,([DGRule],[DGChange]))

globSubsumeAux _ dgraph historyElement [] = (dgraph, historyElement)

globSubsumeAux libEnv dgraph (rules,changes) ((ledge@(src,tgt,edgeLab)):list) =

if not (null proofBasis) || isIdentityEdge ledge libEnv dgraph

then

if isDuplicate newEdge dgraph changes then

globSubsumeAux libEnv (deLLEdge ledge dgraph)

(newRules,(DeleteEdge ledge):changes) list

else

globSubsumeAux libEnv (insEdge newEdge (deLLEdge ledge dgraph))

(newRules,(DeleteEdge ledge):((InsertEdge newEdge):changes)) list

else

globSubsumeAux libEnv dgraph (rules,changes) list

where

morphism = dgl_morphism edgeLab

allPaths = getAllGlobPathsOfMorphismBetween dgraph morphism src tgt

filteredPaths = [path| path <- allPaths, notElem ledge path]

proofBasis = selectProofBasis dgraph ledge filteredPaths

(GlobalThm _ conservativity conservStatus) = dgl_type edgeLab

newEdge = (src,

tgt,

DGLink {dgl_morphism = morphism,

dgl_type = (GlobalThm (Proven (GlobSubsumption ledge)

proofBasis)

conservativity conservStatus),

dgl_origin = DGProof}

)

newRules = (GlobSubsumption ledge):rules

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

-- methods for the extension of globDecomp (avoid insertion ofredundant edges)

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

{- returns all paths consisting of local theorem links whose src and tgt nodes

are contained in the given list of nodes -}

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

localThmPathsBetweenNodes _ [] = []

localThmPathsBetweenNodes dgraph ns = localThmPathsBetweenNodesAux dgraph ns ns

{- auxiliary method for localThmPathsBetweenNodes -}

localThmPathsBetweenNodesAux :: DGraph -> [Node] -> [Node]

-> [[LEdge DGLinkLab]]

localThmPathsBetweenNodesAux _ [] _ = []

localThmPathsBetweenNodesAux dgraph (node:srcNodes) tgtNodes =

concatMap (getAllPathsOfTypeBetween dgraph isUnprovenLocalThm node) tgtNodes

++ localThmPathsBetweenNodesAux dgraph srcNodes tgtNodes

{- combines each of the given paths with matching edges from the given list

(i.e. every edge that has as its source node the tgt node of the path)-}

combinePathsWithEdges :: [[LEdge DGLinkLab]] -> [LEdge DGLinkLab]

-> [[LEdge DGLinkLab]]

combinePathsWithEdges paths = concatMap (combinePathsWithEdge paths)

{- combines the given path with each matching edge from the given list

(i.e. every edge that has as its source node the tgt node of the path)-}

combinePathsWithEdge :: [[LEdge DGLinkLab]] -> LEdge DGLinkLab

-> [[LEdge DGLinkLab]]

combinePathsWithEdge [] _ = []

combinePathsWithEdge (path:paths) edge@(src,_,_) =

case path of

[] -> combinePathsWithEdge paths edge

_ :_ -> if getTargetNode (last path) == src

then (path ++ [edge]) : combinePathsWithEdge paths edge

else combinePathsWithEdge paths edge

{- todo: choose a better name for this method...

returns for each of the given paths a pair consisting of the last edge

contained in the path and - as a triple - the src, tgt and morphism of the

complete path

if there is an empty path in the given list or the morphsim cannot be

calculated, it is simply ignored -}

calculateResultingEdges :: [[LEdge DGLinkLab]]

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

calculateResultingEdges [] = []

calculateResultingEdges (path : paths) =

case path of

[] -> calculateResultingEdges paths

hd : _ ->

case calculateMorphismOfPath path of

Nothing -> calculateResultingEdges paths

Just morphism -> (lst, (src, tgt, morphism)) :

calculateResultingEdges paths

where lst = last path

src = getSourceNode hd

tgt = getTargetNode lst

{- removes from the given list every edge for which there is already an

equivalent edge or path (i.e. an edge or path with the same src, tgt and

morphsim) -}

removeSuperfluousEdges :: DGraph -> [LEdge DGLinkLab]

-> (DGraph,[LEdge DGLinkLab])

removeSuperfluousEdges dgraph [] = (dgraph,[])

removeSuperfluousEdges dgraph es

= removeSuperfluousEdgesAux dgraph es

(calculateResultingEdges combinedPaths) []

where

localThmPaths

= localThmPathsBetweenNodes dgraph (map (getSourceNode) es)

combinedPaths = combinePathsWithEdges localThmPaths es

{- auxiliary method for removeSuperfluousEdges -}

removeSuperfluousEdgesAux :: DGraph -> [LEdge DGLinkLab]

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

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

removeSuperfluousEdgesAux dgraph [] _ edgesToInsert= (dgraph,edgesToInsert)

removeSuperfluousEdgesAux dgraph ((edge@(src,tgt,edgeLab)):list)

resultingEdges edgesToInsert =

if not (null equivalentEdges)

then removeSuperfluousEdgesAux

newDGraph list newResultingEdges edgesToInsert

else removeSuperfluousEdgesAux

dgraph list resultingEdges (edge:edgesToInsert)

where

equivalentEdges

= [e | e <- resultingEdges,(snd e) == (src,tgt,dgl_morphism edgeLab)]

newResultingEdges = [e | e <- resultingEdges,(fst e) /= edge]

newDGraph = deLLEdge edge dgraph

{- returns true, if the given change is an insertion of an local theorem edge,

false otherwise -}

isLocalThmInsertion :: DGChange -> Bool

isLocalThmInsertion change

= case change of

InsertEdge edge -> isLocalThm edge

_ -> False