HideTheoremShift.hs revision 04d04d19fdd5320953c78ad5b6d2d11f85bc4bcf
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederModule : $Header$
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederMaintainer : jfgerken@tzi.de
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederStability : provisional
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederPortability : non-portable(Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederhide theorem shift proof in 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.
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski todo: use compInclusion instead of compHomInclusion
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder ( interactiveHideTheoremShift
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder , automaticHideTheoremShift
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-- ----------------------------------------------
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-- hide theorem shift
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-- ----------------------------------------------
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maedertype ListSelector m a = [a] -> m (Maybe a)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maedertype PathTuple = ([LEdge DGLinkLab], [LEdge DGLinkLab])
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maedertype ProofBaseSelector m = DGraph -> ListSelector m PathTuple
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian MaederinteractiveHideTheoremShift :: LIB_NAME -> LibEnv -> IO LibEnv
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian MaederinteractiveHideTheoremShift =
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maeder hideTheoremShift hideTheoremShift_selectProofBase
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian MaederautomaticHideTheoremShift :: LIB_NAME -> LibEnv -> LibEnv
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian MaederautomaticHideTheoremShift ln = runIdentity . hideTheoremShift
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder (const $ \ l -> return $ case l of
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder [a] -> Just a -- may be take the first one always?
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maeder _ -> Nothing) ln
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian MaederhideTheoremShift :: Monad m => ProofBaseSelector m -> LIB_NAME
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian Maeder -> LibEnv -> m LibEnv
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian MaederhideTheoremShift proofBaseSel ln proofStatus = do
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder let dgraph = lookupDGraph ln proofStatus
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder hidingThmEdges = filter isUnprovenHidingThm (labEdges dgraph)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder result <- hideTheoremShiftAux dgraph ([],[]) hidingThmEdges proofBaseSel
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder let nextDGraph = fst result
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder nextHistoryElem = snd result
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder newProofStatus
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maeder = mkResultProofStatus ln proofStatus nextDGraph nextHistoryElem
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return newProofStatus
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- auxiliary method for hideTheoremShift -}
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaederhideTheoremShiftAux :: Monad m => DGraph -> ([DGRule],[DGChange])
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder -> [LEdge DGLinkLab] -> ProofBaseSelector m
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder -> m (DGraph,([DGRule],[DGChange]))
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederhideTheoremShiftAux dgraph historyElement [] _ =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return (dgraph, historyElement)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederhideTheoremShiftAux dgraph (rules,changes) (ledge:list) proofBaseSel =
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder do proofBasis <- findProofBaseForHideTheoremShift dgraph ledge proofBaseSel
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder if (null proofBasis)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder then hideTheoremShiftAux dgraph (rules,changes) list proofBaseSel
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder let newEdge = makeProvenHidingThmEdge proofBasis ledge
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder auxDGraph = insEdge newEdge (delLEdge ledge dgraph)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder auxChanges = (DeleteEdge ledge):((InsertEdge newEdge):changes)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder (newDGraph,newChanges) =
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder insertNewEdges auxDGraph auxChanges proofBasis
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder newRules = (HideTheoremShift ledge):rules
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder hideTheoremShiftAux newDGraph (newRules,newChanges) list proofBaseSel
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- inserts the given edges into the development graph and adds a corresponding entry to the changes -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsertNewEdges :: DGraph -> [DGChange] -> [LEdge DGLinkLab] -> (DGraph,[DGChange])
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinsertNewEdges dgraph changes [] = (dgraph,changes)
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya GerkeninsertNewEdges dgraph changes (edge:list) =
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken if isDuplicate edge dgraph changes then insertNewEdges dgraph changes list
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya Gerken else insertNewEdges (insEdge edge dgraph) ((InsertEdge edge):changes) list
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- creates a new proven HidingThm edge from the given HidingThm edge using the edge list as the proofBasis -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedermakeProvenHidingThmEdge :: [LEdge DGLinkLab] -> LEdge DGLinkLab -> LEdge DGLinkLab
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya GerkenmakeProvenHidingThmEdge proofBasisEdges ledge@(src,tgt,edgeLab) =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder DGLink {dgl_morphism = morphism,
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder dgl_type = (HidingThm hidingMorphism
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder (Proven (HideTheoremShift ledge) proofBasisEdges)),
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgl_origin = DGProof}
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder morphism = dgl_morphism edgeLab
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (HidingThm hidingMorphism _) = (dgl_type edgeLab)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- selects a proof basis for 'hide theorem shift' if there is one-}
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaederfindProofBaseForHideTheoremShift
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder :: Monad m => DGraph -> LEdge DGLinkLab
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder -> ProofBaseSelector m -> m [LEdge DGLinkLab]
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederfindProofBaseForHideTheoremShift dgraph (ledge@(src,tgt,edgelab))
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder proofBaseSel =
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder do pb <- proofBaseSel dgraph pathPairsFilteredByConservativity
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Nothing -> return []
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Just proofBasis -> do let fstPath = fst proofBasis
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder sndPath = snd proofBasis
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder return [createEdgeForPath fstPath,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder createEdgeForPath sndPath]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder pathsFromSrc = getAllPathsOfTypeFrom dgraph src (ledge /=)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder pathsFromTgt = getAllPathsOfTypeFrom dgraph tgt (ledge /=)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder possiblePathPairs = selectPathPairs pathsFromSrc pathsFromTgt
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (HidingThm hidingMorphism _) = (dgl_type edgelab)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder morphism = dgl_morphism edgelab
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder pathPairsFilteredByMorphism
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder = filterPairsByResultingMorphisms possiblePathPairs
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder hidingMorphism morphism
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder pathPairsFilteredByConservativity
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder = filterPairsByConservativityOfSecondPath pathPairsFilteredByMorphism
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 -}
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederfilterPairsByConservativityOfSecondPath ::
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder [([LEdge DGLinkLab],[LEdge DGLinkLab])]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -> [([LEdge DGLinkLab],[LEdge DGLinkLab])]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederfilterPairsByConservativityOfSecondPath [] = []
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederfilterPairsByConservativityOfSecondPath (([],_):list) =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder filterPairsByConservativityOfSecondPath list
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederfilterPairsByConservativityOfSecondPath ((_,[]):list) =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder filterPairsByConservativityOfSecondPath list
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederfilterPairsByConservativityOfSecondPath (pair:list) =
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder if (and [cons >= Cons | cons <- map getConservativity (snd pair)])
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder then pair:(filterPairsByConservativityOfSecondPath list)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder else filterPairsByConservativityOfSecondPath list
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- selects a proofBasis (i.e. a path tuple) from the list of possible ones:
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder If there is exaclty one proofBasis in the list, this is returned.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder If there are more than one and the method is called in automatic mode Nothing is returned. In non-automatic mode the user is asked to select a proofBasis via listBox. -}
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederhideTheoremShift_selectProofBase ::
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder DGraph -> [([LEdge DGLinkLab], [LEdge DGLinkLab])]
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian 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)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder _ -> return Nothing -- error ("Proofs.Proofs: " ++
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder -- "selection of proof basis failed")
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder -- failing or outputting something here may be a bad idea
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- returns a string representation of the given paths:
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder for each path a tuple of the names of its nodes is shown, the two are combined by an 'and' -}
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederprettyPrintPathTuple :: DGraph -> ([LEdge DGLinkLab],[LEdge DGLinkLab])
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintPathTuple dgraph (p1,p2) =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (prettyPrintPath dgraph p1) ++ " and " ++ (prettyPrintPath dgraph p2)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- returns the names of the nodes of the path, separated by commas-}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintNodesOfPath :: DGraph -> [LEdge DGLinkLab] -> String
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintNodesOfPath _ [] = ""
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintNodesOfPath dgraph (edge:path) =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (prettyPrintSourceNode dgraph edge) ++ ", "
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder ++ (prettyPrintNodesOfPath dgraph path)
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder end = case path of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder [] -> prettyPrintTargetNode dgraph edge
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- 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 =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder "(" ++ (prettyPrintNodesOfPath dgraph path) ++ ")"
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- returns the name of the source node of the given edge-}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintSourceNode :: DGraph -> LEdge DGLinkLab -> String
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintSourceNode dgraph (src,_,_) =
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder getDGNodeName $ lab' $
e509b6f97f98f96ef258c1c3f7968241da8bde5dTill Mossakowski safeContext "Proofs.HideTheoremShift.prettyPrintSourceNode" dgraph src
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- returns the name of the target node of the given edge-}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintTargetNode :: DGraph -> LEdge DGLinkLab -> String
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederprettyPrintTargetNode dgraph (_,tgt,_) =
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder getDGNodeName $ lab' $
e509b6f97f98f96ef258c1c3f7968241da8bde5dTill Mossakowski safeContext "Proofs.HideTheoremShift.prettyPrintTargetNode" dgraph tgt
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- creates a unproven global thm edge for the given path, i.e. with the same source and target nodes and the same morphism as the path -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedercreateEdgeForPath :: [LEdge DGLinkLab] -> LEdge DGLinkLab
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedercreateEdgeForPath path =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder case (calculateMorphismOfPath path) of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Just morphism -> (getSourceNode (head path),
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder getTargetNode (last path),
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder DGLink {dgl_morphism = morphism,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgl_type = (GlobalThm LeftOpen None
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgl_origin = DGProof}
878d0086bd0aae2d7ad64451035c4e78047b1cffChristian Maeder Nothing -> error "createEdgeForPath"
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- returns a list of path pairs, as shorthand the pairs are not returned as path-path tuples but as path-<list of path> tuples. Every path in the list is a pair of the single path.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederThe path pairs are selected by having the same target node. -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederselectPathPairs :: [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -> [([LEdge DGLinkLab],[[LEdge DGLinkLab]])]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederselectPathPairs [] _ = []
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederselectPathPairs _ [] = []
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederselectPathPairs paths1 paths2 =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder [(p1, [p2| p2 <- paths2, haveSameTgt (last p1) (last p2) ] )| p1 <- paths1]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder haveSameTgt :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder haveSameTgt (_,tgt1,_) (_,tgt2,_) = tgt1 == tgt2
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski{- returns a list of path pairs by keeping those pairs, whose first path composed with the first given morphism and whose second path composed with the second given morphism result in the same morphism, and dropping all other pairs.-}
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederfilterPairsByResultingMorphisms :: [([LEdge DGLinkLab],[[LEdge DGLinkLab]])]
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -> GMorphism -> GMorphism
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -> [([LEdge DGLinkLab],[LEdge DGLinkLab])]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederfilterPairsByResultingMorphisms [] _ _ = []
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederfilterPairsByResultingMorphisms (pair:pairs) morph1 morph2 =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder [((fst pair),path)| path <- suitingPaths]
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder ++ (filterPairsByResultingMorphisms pairs morph1 morph2)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder = compMaybeMorphisms (Just morph1) (calculateMorphismOfPath (fst pair))
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder suitingPaths :: [[LEdge DGLinkLab]]
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder suitingPaths = if (compMorph1 /= Nothing) then
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder [path |path <- (snd pair),
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder (compMaybeMorphisms (Just morph2)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder (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
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder (Just m1, Just m2) -> resultToMaybe $ compHomInclusion m1 m2
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski -- This should be compInclusion, but this would need the logic graph
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{- returns the Conservativity if the given edge has one,
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder otherwise an error is raised -}
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedergetConservativity :: LEdge DGLinkLab -> Conservativity
e220b2051a2342a9291721e6c7f408860bed01b7Jorina Freya GerkengetConservativity (_,_,edgeLab) =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder case dgl_type edgeLab of
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (LocalThm _ cons _) -> cons
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (GlobalThm _ cons _) -> cons