e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : hide theorem shift proof rule for development graphs
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
cfbd735270fe52115cef0508d265785efcb99cd7Christian MaederMaintainer : Christian.Maeder@dfki.de
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederStability : provisional
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederPortability : non-portable(Logic)
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskihide theorem shift proof rule for development graphs
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Follows Sect. IV:4.4 of the CASL Reference Manual.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder T. Mossakowski, S. Autexier and D. Hutter:
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Extending Development Graphs With Hiding.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Lecture Notes in Computer Science 2029, p. 269-283,
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Springer-Verlag 2001.
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder ( interactiveHideTheoremShift
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , automaticHideTheoremShift
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu , automaticHideTheoremShiftFromList
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maederimport qualified Data.Map as Map
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maedertype ListSelector m a = [a] -> m (Maybe a)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maedertype PathTuple = ([LEdge DGLinkLab], [LEdge DGLinkLab])
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maedertype ProofBaseSelector m = DGraph -> ListSelector m PathTuple
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian MaederhideThmShiftRule :: EdgeId -> DGRule
c4df2219ea6f47a5e510503e475c38362e8464ebChristian MaederhideThmShiftRule = DGRuleWithEdge "HideTheoremShift"
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederinteractiveHideTheoremShift :: LibName -> LibEnv -> IO LibEnv
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian MaederinteractiveHideTheoremShift =
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maeder hideTheoremShift hideTheoremShift_selectProofBase
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederautomaticHideTheoremShift :: LibName -> LibEnv -> LibEnv
6948b7295a0521212803f15cf919395d2073e2c9Christian MaederautomaticHideTheoremShift ln libEnv =
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder let dgraph = lookupDGraph ln libEnv
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian ls = filter (liftE isUnprovenHidingThm) $ labEdgesDG dgraph
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder in automaticHideTheoremShiftFromList ln ls libEnv
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederautomaticHideTheoremShiftFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederautomaticHideTheoremShiftFromList ln ls = runIdentity . hideTheoremShiftFromList
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu (const $ \ l -> return $ case l of
2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu [a] -> Just a -- maybe take the first one always ?
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> Nothing) ln ls
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederhideTheoremShiftFromList :: Monad m => ProofBaseSelector m -> LibName
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> [LEdge DGLinkLab] -> LibEnv -> m LibEnv
6948b7295a0521212803f15cf919395d2073e2c9Christian MaederhideTheoremShiftFromList proofBaseSel ln hidingThmEdges proofStatus = do
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder let dgraph = lookupDGraph ln proofStatus
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder finalHidingThmEdges = filter (liftE isUnprovenHidingThm) hidingThmEdges
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder nextDGraph <- foldM
afe76697dd6888856a066934a1112a38809b27faChristian Maeder (hideTheoremShiftAux proofBaseSel) dgraph finalHidingThmEdges
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder return $ Map.insert ln nextDGraph proofStatus
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederhideTheoremShift :: Monad m => ProofBaseSelector m -> LibName
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian Maeder -> LibEnv -> m LibEnv
6948b7295a0521212803f15cf919395d2073e2c9Christian MaederhideTheoremShift proofBaseSel ln proofStatus =
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder let dgraph = lookupDGraph ln proofStatus
afe76697dd6888856a066934a1112a38809b27faChristian Maeder hidingThmEdges = labEdgesDG dgraph
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder in hideTheoremShiftFromList proofBaseSel ln hidingThmEdges proofStatus
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian{- | auxiliary method for hideTheoremShift.
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian it contains three steps: inserting of the proof basis, deleting of the
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian current edge and inserting of the new proven edge.
afe76697dd6888856a066934a1112a38809b27faChristian MaederhideTheoremShiftAux :: Monad m => ProofBaseSelector m -> DGraph
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder -> LEdge DGLinkLab -> m DGraph
afe76697dd6888856a066934a1112a38809b27faChristian MaederhideTheoremShiftAux proofBaseSel dgraph ledge =
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder do proofbasis <- findProofBaseForHideTheoremShift dgraph ledge proofBaseSel
afe76697dd6888856a066934a1112a38809b27faChristian Maeder return $ if null proofbasis
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder let (auxDGraph, finalProofBasis) =
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder foldl insertNewEdges (dgraph, emptyProofBasis) proofbasis
64325303fc09fc4d88ced49be11ff2d29966422aCui Jian newEdge = makeProvenHidingThmEdge finalProofBasis ledge
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder newDGraph2 = changeDGH auxDGraph $ DeleteEdge ledge
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder newDGraph = insertDGLEdge newEdge newDGraph2
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder newRules = hideThmShiftRule $ getEdgeId ledge
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder in groupHistory dgraph newRules newDGraph
da955132262baab309a50fdffe228c9efe68251dCui Jian{- | inserts the given edges into the development graph and adds a
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian corresponding entry to the changes, while getting the proofbasis.
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder Notice that EdgeId is enough to represent an edge and can therefore
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian be used as proof basis.
afe76697dd6888856a066934a1112a38809b27faChristian MaederinsertNewEdges :: (DGraph, ProofBasis) -> LEdge DGLinkLab
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder -> (DGraph, ProofBasis)
afe76697dd6888856a066934a1112a38809b27faChristian MaederinsertNewEdges (dgraph, proofbasis) edge =
afe76697dd6888856a066934a1112a38809b27faChristian Maeder case tryToGetEdge edge dgraph of
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder Just e -> (dgraph, addEdgeId proofbasis $ getEdgeId e)
5ff3af2a00b2663a7aaeffa820338a895dc38b82Cui Jian Nothing -> let
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder tempDGraph = changeDGH dgraph $ InsertEdge edge
da955132262baab309a50fdffe228c9efe68251dCui Jian -- checks if the edge is actually inserted
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder tempProofBasis = case getLastChange tempDGraph of
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder InsertEdge tempE ->
afe76697dd6888856a066934a1112a38809b27faChristian Maeder addEdgeId proofbasis $ getEdgeId tempE
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> error ("Proofs" ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ".HideTheoremShift" ++
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder ".insertNewEdges")
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder in (tempDGraph, tempProofBasis)
da955132262baab309a50fdffe228c9efe68251dCui Jian{- | creates a new proven HidingThm edge from the given
3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder HidingThm edge using the edge list as the proofbasis
3fe83d4c932a8266edcf0304a97814c59821d91fChristian MaedermakeProvenHidingThmEdge :: ProofBasis -> LEdge DGLinkLab -> LEdge DGLinkLab
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeProvenHidingThmEdge proofBasisEdges ledge@(src, tgt, edgeLab) =
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder (src, tgt, edgeLab
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder { dgl_type = setProof (Proven (hideThmShiftRule $ getEdgeId ledge)
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder proofBasisEdges)
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder $ dgl_type edgeLab
afe76697dd6888856a066934a1112a38809b27faChristian Maeder , dgl_origin = DGLinkProof })
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | selects a proof basis for 'hide theorem shift' if there is one
afe76697dd6888856a066934a1112a38809b27faChristian MaederfindProofBaseForHideTheoremShift :: Monad m => DGraph -> LEdge DGLinkLab
afe76697dd6888856a066934a1112a38809b27faChristian Maeder -> ProofBaseSelector m -> m [LEdge DGLinkLab]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfindProofBaseForHideTheoremShift dgraph (ledge@(src, tgt, lb)) proofBaseSel = do
afe76697dd6888856a066934a1112a38809b27faChristian Maeder let dgraph2 = delLEdgeDG ledge dgraph
afe76697dd6888856a066934a1112a38809b27faChristian Maeder pathsFromSrc = getAllPathsOfTypeFrom dgraph2 src
afe76697dd6888856a066934a1112a38809b27faChristian Maeder pathsFromTgt = getAllPathsOfTypeFrom dgraph2 tgt
afe76697dd6888856a066934a1112a38809b27faChristian Maeder possiblePathPairs = selectPathPairs pathsFromSrc pathsFromTgt
d24317c8197e565e60c8f41309de246249c1e57eChristian Maeder HidingFreeOrCofreeThm Nothing _ hidingMorphism _ = dgl_type lb
afe76697dd6888856a066934a1112a38809b27faChristian Maeder morphism = dgl_morphism lb
afe76697dd6888856a066934a1112a38809b27faChristian Maeder pathPairsFilteredByMorphism
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder = filterPairsByResultingMorphisms possiblePathPairs
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder hidingMorphism morphism
afe76697dd6888856a066934a1112a38809b27faChristian Maeder pathPairsFilteredByConservativity
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder = filterPairsByConservativityOfSecondPath pathPairsFilteredByMorphism
afe76697dd6888856a066934a1112a38809b27faChristian Maeder -- advoiding duplicate to be selected proofbasis.
afe76697dd6888856a066934a1112a38809b27faChristian Maeder pathPairsFilteredByProveStatus
49d8e1a419ee5658d23762335af121179a68669fCui Jian = filterPairsByGlobalProveStatus pathPairsFilteredByConservativity
afe76697dd6888856a066934a1112a38809b27faChristian Maeder pb <- proofBaseSel dgraph pathPairsFilteredByProveStatus
afe76697dd6888856a066934a1112a38809b27faChristian Maeder return $ case pb of
afe76697dd6888856a066934a1112a38809b27faChristian Maeder Nothing -> []
afe76697dd6888856a066934a1112a38809b27faChristian Maeder Just (fstPath, sndPath) -> map createEdgeForPath [fstPath, sndPath]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | advoiding duplicate to be selected proofbasis.
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian MaederfilterPairsByGlobalProveStatus :: [([LEdge DGLinkLab], [LEdge DGLinkLab])]
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian Maeder -> [([LEdge DGLinkLab], [LEdge DGLinkLab])]
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian MaederfilterPairsByGlobalProveStatus = filter bothAreProven where
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian Maeder bothAreProven (pb1, pb2) = allAreProven pb1 && allAreProven pb2
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian Maeder allAreProven = all $ liftE (\ l -> isProven l && isGlobalEdge l)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder{- removes all pairs from the given list whose second path does not have a
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder conservativity greater than or equal to Cons -}
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian MaederfilterPairsByConservativityOfSecondPath
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder :: [([LEdge DGLinkLab], [LEdge DGLinkLab])]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> [([LEdge DGLinkLab], [LEdge DGLinkLab])]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederfilterPairsByConservativityOfSecondPath [] = []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfilterPairsByConservativityOfSecondPath (([], _) : list) =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder filterPairsByConservativityOfSecondPath list
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfilterPairsByConservativityOfSecondPath ((_, []) : list) =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder filterPairsByConservativityOfSecondPath list
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfilterPairsByConservativityOfSecondPath (pair : list) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if and [cons >= Cons | cons <- map getConservativity (snd pair)]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then pair : filterPairsByConservativityOfSecondPath list
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder else filterPairsByConservativityOfSecondPath list
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian{- | selects a proofBasis (i.e. a path tuple) from the list of possible ones:
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian If there is exaclty one proofBasis in the list, this is returned.
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian If there are more than one and the method is called in automatic mode
da955132262baab309a50fdffe228c9efe68251dCui Jian Nothing is returned.
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian In non-automatic mode the user is asked to select a proofBasis via
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian listBox, then the selected one will be returned.
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian MaederhideTheoremShift_selectProofBase
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian Maeder :: DGraph -> [([LEdge DGLinkLab], [LEdge DGLinkLab])]
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian Maeder -> IO (Maybe ([LEdge DGLinkLab], [LEdge DGLinkLab]))
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaederhideTheoremShift_selectProofBase dgraph basisList =
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder case basisList of
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder [] -> return Nothing
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder [basis] -> return $ Just basis
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder sel <- listBox
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder "Choose a path tuple as the proof basis"
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder (map (prettyPrintPathTuple dgraph) basisList)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder Just j -> return $ Just (basisList !! j)
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian Maeder _ -> return Nothing
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder{- returns a string representation of the given paths: for each path a
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder tuple of the names of its nodes is shown, the two are combined by
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder an \'and\' -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprettyPrintPathTuple :: DGraph -> ([LEdge DGLinkLab], [LEdge DGLinkLab])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprettyPrintPathTuple dgraph (p1, p2) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder prettyPrintPath dgraph p1 ++ " and " ++ prettyPrintPath dgraph p2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- returns the names of the nodes of the path, separated by commas
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintNodesOfPath :: DGraph -> [LEdge DGLinkLab] -> String
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintNodesOfPath _ [] = ""
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprettyPrintNodesOfPath dgraph (edge : path) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder prettyPrintSourceNode dgraph edge ++ ", "
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ prettyPrintNodesOfPath dgraph path
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder end = case path of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder [] -> prettyPrintTargetNode dgraph edge
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- returns a string reprentation of the path: showing a tuple of its nodes
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintPath :: DGraph -> [LEdge DGLinkLab] -> String
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya GerkenprettyPrintPath _ [] = "<empty path>"
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintPath dgraph path =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "(" ++ prettyPrintNodesOfPath dgraph path ++ ")"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- returns the name of the source node of the given edge
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintSourceNode :: DGraph -> LEdge DGLinkLab -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprettyPrintSourceNode dgraph (src, _, _) =
5efed683fd173e9d53bd5f1929ba5b0c8a228710Christian Maeder getDGNodeName $ labDG dgraph src
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- returns the name of the target node of the given edge
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintTargetNode :: DGraph -> LEdge DGLinkLab -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprettyPrintTargetNode dgraph (_, tgt, _) =
5efed683fd173e9d53bd5f1929ba5b0c8a228710Christian Maeder getDGNodeName $ labDG dgraph tgt
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder{- creates a unproven global thm edge for the given path, i.e. with
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maederthe same source and target nodes and the same morphism as the path -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedercreateEdgeForPath :: [LEdge DGLinkLab] -> LEdge DGLinkLab
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian MaedercreateEdgeForPath path =
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder case (calculateMorphismOfPath path, path) of
da955132262baab309a50fdffe228c9efe68251dCui Jian (Just morphism, (s, _, _) : _) ->
da955132262baab309a50fdffe228c9efe68251dCui Jian let (_, t, _) = last path
d11391a2447a2005329a95b5d770f24e62bf5b63Christian Maeder in (s, t, defDGLink morphism globalThm DGLinkProof)
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder _ -> error "createEdgeForPath"
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maeder{- returns a list of path pairs, as shorthand the pairs are not
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maederreturned as path-path tuples but as path-<list of path> tuples. Every
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maederpath in the list is a pair of the single path. The path pairs are
90a0050cf7979b2ca1fde7991462851abcbcf3a3Christian Maederselected by having the same target node. -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederselectPathPairs :: [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederselectPathPairs [] _ = []
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederselectPathPairs _ [] = []
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederselectPathPairs paths1 paths2 =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [(p1, [p2 | p2 <- paths2, haveSameTgt (last p1) (last p2) ] ) | p1 <- paths1]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder haveSameTgt :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder haveSameTgt (_, tgt1, _) (_, tgt2, _) = tgt1 == tgt2
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian Maeder{- returns a list of path pairs by keeping those pairs, whose first
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian Maederpath composed with the first given morphism and whose second path
e44a4fd691fbfb3a1ac9f3f31aae7d5245055760Christian Maedercomposed with the second given morphism result in the same morphism,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederand dropping all other pairs. -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfilterPairsByResultingMorphisms :: [([LEdge DGLinkLab], [[LEdge DGLinkLab]])]
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -> GMorphism -> GMorphism
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> [([LEdge DGLinkLab], [LEdge DGLinkLab])]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederfilterPairsByResultingMorphisms [] _ _ = []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfilterPairsByResultingMorphisms (pair : pairs) morph1 morph2 =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [(fst pair, path) | path <- suitingPaths]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ filterPairsByResultingMorphisms pairs morph1 morph2
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder = compMaybeMorphisms (Just morph1) (calculateMorphismOfPath (fst pair))
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder suitingPaths :: [[LEdge DGLinkLab]]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder suitingPaths = if isJust compMorph1 then
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [path | path <- snd pair,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder compMaybeMorphisms (Just morph2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (calculateMorphismOfPath path)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder == compMorph1]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- if the given maybe morphisms are both not Nothing,
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder this method composes their GMorphisms -
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder returns Nothing otherwise -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedercompMaybeMorphisms :: Maybe GMorphism -> Maybe GMorphism -> Maybe GMorphism
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedercompMaybeMorphisms morph1 morph2 =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder case (morph1, morph2) of
bf4226899034bddcfe81c870cbedf28c2890370eChristian Maeder (Just m1, Just m2) -> resultToMaybe $ compInclusion logicGraph m1 m2
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski -- This should be compInclusion, but this would need the logic graph