0N/ADescription : the proof status with manipulating functions
0N/ACopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
0N/AMaintainer : ken@tzi.de
0N/AStability : provisional
0N/APortability : non-portable(Logic)
0N/Athe proof status with manipulating functions
0N/A , mkResultProofStatus
0N/A , prepareProofStatus
0N/A proof status = (DG0,[(R1,DG1),...,(Rn,DGn)])
535N/A DG0 is the development graph resulting from the static analysis
535N/A Ri is a list of rules that transforms DGi-1 to DGi
535N/A With the list of intermediate proof states, one can easily implement
0N/A-- -------------------------------
0N/A-- methods used in several proofs
263N/A-- -------------------------------
0N/A{- returns the history that belongs to the given library name-}
0N/AlookupHistory :: LIB_NAME -> LibEnv -> ProofHistory
263N/AlookupHistory ln = proofHistory . lookupDGraph ln
263N/AmkResultProofStatus :: LIB_NAME -> LibEnv -> DGraph
535N/A -> ([DGRule], [DGChange]) -> LibEnv
535N/AmkResultProofStatus ln ps dgraph (dgrules, dgchanges) =
535N/A let historyElem = (dgrules,removeContraryChanges dgchanges)
0N/A $ prepareResultProofHistory ps
263N/AmapProofHistory :: (ProofHistory -> ProofHistory) -> LibEnv -> LibEnv
263N/AmapProofHistory f =
Map.map ( \ c -> setProofHistoryWithDG f c )
535N/AprepareResultProofHistory :: LibEnv -> LibEnv
535N/AprepareResultProofHistory = mapProofHistory (emptyHistory :)
535N/A-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
535N/A-- prepare, revise, lookup, update on proofstatus and its components
0N/A-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
535N/A{- prepares the all histories of the proof history of the given proofstatus -}
263N/AprepareProofStatus :: LibEnv -> LibEnv
0N/AprepareProofStatus = mapProofHistory prepareHistory
0N/A{- prepares the given history for the rule application by appending
0N/A an empty list tuple to the front of it, if there is not already one
0N/A with an empty change list-}
0N/AprepareHistory :: ProofHistory -> ProofHistory
0N/AprepareHistory [] = [emptyHistory]
0N/AprepareHistory history@((_,[]):_) = history
0N/AprepareHistory history = emptyHistory : history
535N/A{- revises the history of the given proofstatus -}
535N/AreviseProofStatus :: LibEnv -> LibEnv
0N/AreviseProofStatus = mapProofHistory reviseHistory
0N/A{- removes the contrary changes form the given history and adds the name
535N/A of the proof method (TheoremHideShift) -}
535N/AreviseHistory :: ProofHistory -> ProofHistory
0N/AreviseHistory ((_,changes) : history) =
263N/A ([TheoremHideShift], removeContraryChanges changes) : history
535N/A{- updates the library environment and the proof history of the given
535N/A proofstatus for the given library name-}
535N/AupdateProofStatus :: LIB_NAME -> DGraph -> [DGChange] -> LibEnv -> LibEnv
263N/AupdateProofStatus ln dgraph changes =
263N/A setProofHistoryWithDG (addChanges changes) dgraph) ln
263N/A{- adds the given changes to the given history -}
0N/AaddChanges :: [DGChange] -> [([DGRule],[DGChange])] -> [([DGRule],[DGChange])]
0N/AaddChanges changes [] = [([],changes)]
0N/AaddChanges changes (hElem:history) = (fst hElem, snd hElem ++ changes):history
263N/A-- - - - - - - - - - - - - - - - - - - - - -
263N/A-- debug methods to print a list of changes
263N/A-- - - - - - - - - - - - - - - - - - - - - -
263N/AshowChanges :: [DGChange] -> String
263N/AshowChanges (change:changes) =
263N/A InsertEdge edge -> "InsertEdge " ++ (showEdgeChange edge)
0N/A ++ (showChanges changes)
0N/A DeleteEdge edge -> "DeleteEdge " ++ (showEdgeChange edge)
263N/A ++ (showChanges changes)
0N/A InsertNode node -> "InsertNode " ++ (showNodeChange node)
0N/A ++ (showChanges changes)
0N/A DeleteNode node -> "DeleteNode " ++ (showNodeChange node)
0N/A ++ (showChanges changes)
0N/A SetNodeLab _ (node, newLab) -> "SetNodeLab of node " ++ show node ++
0N/A " with new lab: " ++ show newLab
0N/AshowEdgeChange :: LEdge DGLinkLab -> String
0N/AshowEdgeChange (src,tgt,edgelab) =
0N/A " from " ++ (show src) ++ " to " ++ (show tgt)
0N/A ++ " and of type " ++ showDoc (dgl_type edgelab) "\n\n"
0N/AshowNodeChange :: LNode DGNodeLab -> String
0N/AshowNodeChange (descr, nodelab) =
0N/A (show descr) ++ " with name " ++ (show (dgn_name nodelab)) ++ "\n\n"
0N/A-- ----------------------------------------------
0N/A-- methods that keep the change list clean
0N/A-- ----------------------------------------------
0N/AremoveContraryChanges :: [DGChange] -> [DGChange]
0N/AremoveContraryChanges [] = []
0N/AremoveContraryChanges (change:changes) =
0N/A case contraryChange of
0N/A Just c -> removeContraryChanges (removeChange c changes)
0N/A Nothing -> change:(removeContraryChanges changes)
0N/A case getContraryChange change of
0N/A Just c -> if c `elem` changes then Just c else Nothing
0N/AgetContraryChange :: DGChange -> Maybe DGChange
1879N/AgetContraryChange change = case change of
1879N/A InsertEdge edge -> Just $ DeleteEdge edge
-- re-insertion of deleted edge may be useful if node has changed
InsertNode node -> Just $ DeleteNode node
-- re-insertion of deleted node may be useful if node has changed
-- ... although this should be recognized ... a bit strange ...
DeleteNode _ -> Nothing -- Just $ InsertNode node
SetNodeLab _ _ -> Nothing
removeChange :: DGChange -> [DGChange] -> [DGChange]
removeChange c1 (c2:rest) | c1==c2 = rest
-- when a node is removed afterwards, throw away all edge operations
-- refering to that node that are encountered on the way
removeChange c1@(DeleteNode (n,_)) (c2:rest) =
InsertEdge (n1,n2,_) -> n==n1 || n==n2
DeleteEdge (n1,n2,_) -> n==n1 || n==n2
then removeChange c1 rest
else c2:removeChange c1 rest
removeChange c1 (c2:rest) = c2:removeChange c1 rest
isIdentityEdge :: LEdge DGLinkLab -> LibEnv -> DGraph -> Bool
isIdentityEdge (src,tgt,edgeLab) ps dgraph =
let dg = lookupDGraph (dgn_libname nodeLab) ps in
isIdentityEdge (dgn_node nodeLab,tgt,edgeLab) ps dg
dgl_morphism edgeLab == ide Grothendieck (dgn_sign nodeLab)