0N/ACopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2004
0N/AMaintainer : jfgerken@tzi.de
0N/AStability : provisional
0N/APortability : non-portable(Logic)
157N/A theorem hide shift proof in development graphs.
0N/A Follows Sect. IV:4.4 of the CASL Reference Manual.
0N/A T. Mossakowski, S. Autexier and D. Hutter:
0N/A Extending Development Graphs With Hiding.
0N/A H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
0N/A Lecture Notes in Computer Science 2029, p. 269-283,
0N/A Springer-Verlag 2001.
0N/A{- returns the sentence list of the given node -}
0N/AgetSignature :: LibEnv -> DGraph -> Node -> Maybe G_sign
0N/AgetSignature libEnv dgraph node =
0N/A Just (_,_,refDgraph) ->
0N/A getSignature libEnv refDgraph (dgn_node nodeLab)
0N/A else Just (dgn_sign nodeLab)
0N/A where nodeLab = lab' (context dgraph node)
0N/A-- ----------------------------------------------
0N/A-- theorem hide shift
0N/A-- ----------------------------------------------
0N/AtheoremHideShift :: ProofStatus -> IO ProofStatus
0N/AtheoremHideShift proofStatus@(ln,_,_) = do
0N/A let (nonLeaves,leaves)
0N/A = partition (hasIngoingHidingDef proofStatus ln) $
0N/A nodes $ lookupDGraph ln proofStatus
0N/A auxProofstatus <- handleLeaves (prepareProofStatus proofStatus) leaves
finalProofstatus <- handleNonLeaves auxProofstatus nonLeaves
return (reviseProofStatus finalProofstatus)
-- bei DGRefs auch ueber lib-Grenze hinaus suchen?
{- returns True, if the given node has at least one directely or
indirectely (ie via an ingoing path of GlobalDef edges)
hasIngoingHidingDef :: ProofStatus -> LIB_NAME -> Node -> Bool
hasIngoingHidingDef proofstatus@(_,libEnv,_) ln node =
not (null hidingDefEdges)
|| or [hasIngoingHidingDef proofstatus ln' node'| (ln',node') <- next]
inGoingEdges = getAllIngoingEdges libEnv (ln,node)
hidingDefEdges = [tuple| tuple <- inGoingEdges, isHidingDef (snd tuple)]
globalDefEdges = [tuple| tuple <- inGoingEdges, isGlobalDef (snd tuple)]
next = [(l,getSourceNode e)| (l,e) <- globalDefEdges]
{- handles all nodes that are leaves
(ie nodes that have no ingoing edges of type HidingDef) -}
handleLeaves :: ProofStatus -> [Node] -> IO ProofStatus
handleLeaves proofstatus [] = return proofstatus
handleLeaves proofstatus (node:list) = do
auxProofstatus <- convertToNf proofstatus node
handleLeaves auxProofstatus list
{- converts the given node to its own normal form -}
convertToNf :: ProofStatus -> Node -> IO ProofStatus
convertToNf proofstatus@(ln,libEnv,history) node = do
let dgraph = lookupDGraph ln proofstatus
nodelab = lab' (context dgraph node)
Just _ -> return proofstatus
let newNode = getNewNode dgraph
proofstatusAux <- mkNfNodeForLeave node newNode proofstatus
let auxGraph = lookupDGraph ln proofstatusAux
(finalGraph,changes) <- adoptEdges auxGraph node newNode
let finalChanges = changes ++ [DeleteNode (node,nodelab)]
return (updateProofStatus ln (delNode node finalGraph)
finalChanges proofstatusAux)
{- creates and inserts a normal form node from the given input -}
mkNfNodeForLeave :: Node -> Node -> ProofStatus -> IO ProofStatus
mkNfNodeForLeave node newNode proofstatus@(ln,_,_) = do
let nodelab = lab' (context (lookupDGraph ln proofstatus) node)
True -> mkDGRefNfNode nodelab newNode True proofstatus
False -> mkDGNodeNfNode nodelab newNode Nothing proofstatus
{- creates and inserts a normal form node of type DGNode:
if the given nonLeaveValues is Nothing, ie the original node is a leave,
the original node is copied and the dgn_sigma is the identity;
if not, dgn_sign and dgn_sigma are taken from the nonLeaveValues and
the remaining values are copied from the original node;
in both cases the normal form node ist its own normal form -}
mkDGNodeNfNode :: DGNodeLab -> Node -> Maybe (G_sign, Maybe GMorphism)
-> ProofStatus -> IO ProofStatus
mkDGNodeNfNode nodelab newNode nonLeaveValues proofstatus = do
let (sign,sigma) = case nonLeaveValues of
Nothing -> (dgn_sign nodelab,
Just (ide Grothendieck (dgn_sign nodelab)))
DGNode {dgn_name = dgn_name nodelab,
dgn_sens = dgn_sens nodelab,
return (insertNfNode proofstatus lnode)
{- creates and inserts a normal form node of type DGRef:
if the given corresponding node is a leave, the normal form node
of the referenced node is referenced and its values copied;
if not, the original node is copied and the dgn_sigma is the identiy;
in both cases the normal form node is its own normal form -}
mkDGRefNfNode :: DGNodeLab -> Node -> Bool -> ProofStatus -> IO ProofStatus
mkDGRefNfNode nodelab newNode isLeave proofstatus@(ln,_,_) = do
auxProofstatus@(_,auxLibEnv,_)
(changeCurrentLibName (dgn_libname nodelab) proofstatus)
let refGraph = lookupDGraph (dgn_libname nodelab) proofstatus
(Just refNf) = dgn_nf $ lab' $ context refGraph $ dgn_node nodelab
refNodelab = lab' (context refGraph refNf)
(renamed, libname, sigma) =
then (dgn_renamed nodelab, dgn_libname nodelab,
case getSignature auxLibEnv refGraph refNf of
Just sign -> Just (ide Grothendieck sign)
else (dgn_renamed refNodelab, dgn_libname refNodelab,
DGRef {dgn_renamed = renamed,
return (insertNfNode (changeCurrentLibName ln auxProofstatus) lnode)
{- inserts the given node into the development graph belonging
to the given library name and updates the proofstatus -}
insertNfNode :: ProofStatus -> LNode DGNodeLab -> ProofStatus
insertNfNode proofstatus@(ln,_,_) dgnode =
(insNode dgnode (lookupDGraph ln proofstatus))
{- adopts the edges of the old node to the new node -}
adoptEdges :: DGraph -> Node -> Node -> IO (DGraph,[DGChange])
adoptEdges dgraph oldNode newNode = do
let ingoingEdges = inn dgraph oldNode
outgoingEdges = [outEdge| outEdge <- out dgraph oldNode,
not (elem outEdge ingoingEdges)]
(auxGraph, changes) = adoptEdgesAux dgraph ingoingEdges newNode True
(finalGraph, furtherChanges)
= adoptEdgesAux auxGraph outgoingEdges newNode False
return (finalGraph, changes ++ furtherChanges)
{- auxiliary method for adoptEdges -}
adoptEdgesAux :: DGraph -> [LEdge DGLinkLab] -> Node -> Bool
adoptEdgesAux dgraph [] _ _ = (dgraph,[])
adoptEdgesAux dgraph (oldEdge@(src,tgt,edgelab):list) node areIngoingEdges =
(finalGraph, [DeleteEdge oldEdge,InsertEdge newEdge]++furtherChanges)
(newSrc,newTgt) = if src == tgt then (node,node) else (src,tgt)
newEdge = if areIngoingEdges then (newSrc,node,edgelab)
else (node,newTgt,edgelab)
auxGraph = insEdge newEdge (delLEdge oldEdge dgraph)
(finalGraph,furtherChanges)
= adoptEdgesAux auxGraph list node areIngoingEdges
{- handles all nodes that are no leaves
(ie nodes that have ingoing edges of type HidingDef) -}
handleNonLeaves :: ProofStatus -> [Node] -> IO ProofStatus
handleNonLeaves proofstatus [] = return proofstatus
handleNonLeaves proofstatus@(ln,_,_) (node:list) = do
let dgraph = lookupDGraph ln proofstatus
nodelab = lab' (context dgraph node)
Just _ -> handleNonLeaves proofstatus list
let nfNode = getNewNode dgraph
auxProofstatus' <- mkDGRefNfNode nodelab nfNode False proofstatus
(auxGraph,changes) <- setNfOfNode dgraph node nfNode
let finalProofstatus = updateProofStatus ln auxGraph changes
handleNonLeaves finalProofstatus list
auxProofstatus <- createNfsForPredecessors proofstatus node
let auxGraph = lookupDGraph ln auxProofstatus
defInEdges = [edge| edge <- inn auxGraph node,
isGlobalDef edge || isHidingDef edge]
predecessors = [src| (src,_,_) <- defInEdges]
diagram = makeDiagram auxGraph (node:predecessors) defInEdges
Result diags res = gWeaklyAmalgamableCocone diagram
Nothing -> do sequence $ map (putStrLn . show) diags
handleNonLeaves auxProofstatus list
let nfNode = getNewNode auxGraph
auxProofstatus'<- mkDGNodeNfNode nodelab nfNode
-- use this line until gWeaklyAmalgamableCocone is defined: (Just (dgn_sign nodelab,sigma))
finalProofstatus <- linkNfNode node nfNode map auxProofstatus'
handleNonLeaves finalProofstatus list
{- creates the normal forms of the predecessors of the given node
note: as this method it is called after the normal forms of the leave nodes
have already been defined, only handleNonLeaves is called here -}
createNfsForPredecessors :: ProofStatus -> Node -> IO ProofStatus
createNfsForPredecessors proofstatus@(ln,_,_) node = do
handleNonLeaves proofstatus predecessors
dgraph = lookupDGraph ln proofstatus
defInEdges = [edge| edge@(src,_,_) <- inn dgraph node,
(isGlobalDef edge || isHidingDef edge)
predecessors = [src| (src,_,_) <- defInEdges]
{- creates an GDiagram with the signatures of the given nodes as nodes
and the morphisms of the given edges as edges -}
makeDiagram :: DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
makeDiagram = makeDiagramAux empty
{- auxiliary method for makeDiagram: first translates all nodes then all edges,
the descriptors of the nodes are kept in order to make retranslation easier
makeDiagramAux :: GDiagram -> DGraph -> [Node] -> [LEdge DGLinkLab] -> GDiagram
makeDiagramAux diagram _ [] [] = diagram
makeDiagramAux diagram dgraph [] (edge@(src,tgt,lab):list) =
makeDiagramAux (insEdge morphEdge diagram) dgraph [] list
where morphEdge = if isHidingDef edge then (tgt,src,dgl_morphism lab)
else (src,tgt,dgl_morphism lab)
makeDiagramAux diagram dgraph (node:list) edges =
makeDiagramAux (insNode sigNode diagram) dgraph list edges
where sigNode = (node, dgn_sign (lab' (context dgraph node)))
{- sets the normal form of the first given node to the second one and
insert the edges to the normal form node according to the given map -}
linkNfNode :: Node -> Node ->
Map.Map Node GMorphism -> ProofStatus
linkNfNode node nfNode map proofstatus@(ln,_,_) = do
setNfOfNode (lookupDGraph ln proofstatus) node nfNode
let (finalGraph,changes') = insertEdgesToNf auxGraph nfNode map
return (updateProofStatus ln finalGraph (changes ++ changes') proofstatus)
{- sets the normal form of the first node to the second one -}
setNfOfNode :: DGraph -> Node -> Node -> IO (DGraph,[DGChange])
setNfOfNode dgraph node nf_node = do
(finalGraph,changes) <- adoptEdges auxGraph node newNode
return (delNode node finalGraph,
((InsertNode newLNode):changes)++[DeleteNode oldLNode])
nodeLab = lab' (context dgraph node)
oldLNode = labNode' (context dgraph node)
newNode = getNewNode dgraph
newLNode = case isDGRef nodeLab of
True -> (newNode, DGRef {dgn_renamed = dgn_renamed nodeLab,
dgn_libname = dgn_libname nodeLab,
dgn_node = dgn_node nodeLab,
dgn_sigma = dgn_sigma nodeLab
False -> (newNode, DGNode {dgn_name = dgn_name nodeLab,
dgn_sign = dgn_sign nodeLab,
dgn_sens = dgn_sens nodeLab,
dgn_sigma = dgn_sigma nodeLab,
auxGraph = insNode newLNode dgraph
{- inserts GlobalDef edges to the given node from each node in the map
with the corresponding morphism -}
insertEdgesToNf :: DGraph -> Node -> (
Map.Map Node GMorphism)
insertEdgesToNf dgraph nfNode map =
{- auxiliary method for insertEdgesToNf -}
insertEdgesToNfAux :: DGraph -> Node -> [(Node,GMorphism)]
insertEdgesToNfAux dgraph _ [] = (dgraph,[])
insertEdgesToNfAux dgraph nfNode ((node,morph):list) =
(finalGraph, (InsertEdge ledge):changes)
ledge = (node, nfNode, DGLink {dgl_morphism = morph,
auxGraph = insEdge ledge dgraph
(finalGraph,changes) = insertEdgesToNfAux auxGraph nfNode list