EdgeUtils.hs revision 294e24edea598311fa5af82e2f6a9cdaa531f5e7
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder{- |
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederModule : $Header$
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian MaederCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
34bff097c14521b5e57ce37279a34256e1f78aa5Klaus LuettichMaintainer : jfgerken@tzi.de
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederStability : provisional
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederPortability : non-portable(Logic)
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederutility functions for edges of a development graphs.
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder-}
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
c29fabd288a7c6c0b46e134f70b48138aae9214aChristian Maeder{- todo: also treat conservativity proof status in computation of proof basis
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder-}
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maedermodule Proofs.EdgeUtils where
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Logic.Grothendieck
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Static.DevGraph
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Static.DGToSpec
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Data.Graph.Inductive.Graph
02a2037f53b925617df45eb62ca743d777672265Klaus Luettichimport Data.List
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaederdeLLEdge :: LEdge DGLinkLab -> DGraph -> DGraph
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederdeLLEdge e@(v, _, _) g = case match v g of
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder (Just(p, v', l', s), g') ->
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let (ls, rs) = partition (\ (k, n) -> e == (v, n, k)) s in
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder case ls of
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maeder [] -> error $ "deLLEdge no edge: " ++ show e
41076bb5f87e3dbebb53d762ccb9795801b4a27aChristian Maeder [_] -> (p, v', l', rs) & g'
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder _ -> error $ "deLLEdge multiple edges: " ++ show e
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder _ -> error $ "deLLEdge no node for edge: " ++ show e
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederinsLEdge :: LEdge DGLinkLab -> DGraph -> DGraph
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederinsLEdge e@(v, w, l) g = case match v g of
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder (Just(p, v', l', s), g') ->
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder let ls = filter (\ (k, n) -> e == (v, n, k)) s in
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder case ls of
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder [] -> (p, v', l', (l, w) : s) & g'
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder _ -> error $ "insLEdge multiple edge: " ++ show e
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder _ -> error $ "insLEdge no node for edge: " ++ show e
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian MaederdelLNode :: LNode DGNodeLab -> DGraph -> DGraph
9f29e77d1b758a260223874ac6956e290134cb9dChristian MaederdelLNode n@(v, l) g = case match v g of
eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder (Just(p, _, l', s), g') ->
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder if l' == l then
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder if null p && null s then g'
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder else error $ "delLNode remaining edges: " ++ show (p ++ s)
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder else error $ "delLNode wrong label: " ++ show n
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder _ -> error $ "delLNode no such node: " ++ show n
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian MaederinsLNode :: LNode DGNodeLab -> DGraph -> DGraph
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian MaederinsLNode n@(v, _) g =
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder if gelem v g then error $ "insLNode " ++ show n else insNode n g
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederchangeDG :: DGraph -> DGChange -> DGraph
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederchangeDG g c = case c of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder InsertNode n -> insLNode n g
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder DeleteNode n -> delLNode n g
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder InsertEdge e -> insLEdge e g
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder DeleteEdge e -> deLLEdge e g
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaederchangesDG :: DGraph -> [DGChange] -> DGraph
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederchangesDG = foldl' changeDG
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaederapplyProofHistory :: ProofHistory -> GlobalContext -> GlobalContext
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaederapplyProofHistory h c = c { devGraph = changesDG (devGraph c) $ concatMap snd
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder $ reverse h
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder , proofHistory = h }
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder-- -------------------------------------
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder-- methods to check the type of an edge
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder-- -------------------------------------
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian MaederisProven :: LEdge DGLinkLab -> Bool
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian MaederisProven edge = isGlobalDef edge || isLocalDef edge
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder || isProvenGlobalThm edge || isProvenLocalThm edge
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder || isProvenHidingThm edge
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian MaederisDefEdge :: LEdge DGLinkLab -> Bool
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian MaederisDefEdge edge = isGlobalDef edge || isLocalDef edge || isHidingDef edge
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisGlobalEdge :: LEdge DGLinkLab -> Bool
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisGlobalEdge edge = isGlobalDef edge || isGlobalThm edge
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian MaederisLocalEdge :: LEdge DGLinkLab -> Bool
a255351561838b3743d03c1629d335cfb8b83804Christian MaederisLocalEdge edge = isLocalDef edge || isLocalThm edge
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisGlobalThm :: LEdge DGLinkLab -> Bool
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisGlobalThm edge = isProvenGlobalThm edge || isUnprovenGlobalThm edge
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaederisLocalThm :: LEdge DGLinkLab -> Bool
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian MaederisLocalThm edge = isProvenLocalThm edge || isUnprovenLocalThm edge
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich
02a2037f53b925617df45eb62ca743d777672265Klaus LuettichisProvenGlobalThm :: LEdge DGLinkLab -> Bool
02a2037f53b925617df45eb62ca743d777672265Klaus LuettichisProvenGlobalThm (_,_,edgeLab) =
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich case dgl_type edgeLab of
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich (GlobalThm (Proven _ _) _ _) -> True
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder _ -> False
5908cc06d7a3f4dd46d2d7c7fe0fad43b6cd921fChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederisUnprovenGlobalThm :: LEdge DGLinkLab -> Bool
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisUnprovenGlobalThm (_,_,edgeLab) =
5908cc06d7a3f4dd46d2d7c7fe0fad43b6cd921fChristian Maeder case dgl_type edgeLab of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (GlobalThm LeftOpen _ _) -> True
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder _ -> False
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisProvenLocalThm :: LEdge DGLinkLab -> Bool
6a50fa6b0d93a521d8e52c61a3ceb71d9f878cebChristian MaederisProvenLocalThm (_,_,edgeLab) =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case dgl_type edgeLab of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder (LocalThm (Proven _ _) _ _) -> True
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder _ -> False
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederisUnprovenLocalThm :: LEdge DGLinkLab -> Bool
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederisUnprovenLocalThm (_,_,edgeLab) =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case dgl_type edgeLab of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (LocalThm LeftOpen _ _) -> True
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder _ -> False
41076bb5f87e3dbebb53d762ccb9795801b4a27aChristian Maeder
41076bb5f87e3dbebb53d762ccb9795801b4a27aChristian MaederisHidingEdge :: LEdge DGLinkLab -> Bool
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederisHidingEdge edge = isHidingDef edge || isHidingThm edge
41076bb5f87e3dbebb53d762ccb9795801b4a27aChristian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederisHidingDef :: LEdge DGLinkLab -> Bool
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederisHidingDef (_,_,edgeLab) =
ee1ceac4345bc824210b2f7c6d6b182cb1902547Christian Maeder case dgl_type edgeLab of
ee1ceac4345bc824210b2f7c6d6b182cb1902547Christian Maeder HidingDef -> True
ee1ceac4345bc824210b2f7c6d6b182cb1902547Christian Maeder _ -> False
ee1ceac4345bc824210b2f7c6d6b182cb1902547Christian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederisHidingThm :: LEdge DGLinkLab -> Bool
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederisHidingThm edge = isProvenHidingThm edge || isUnprovenHidingThm edge
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederisProvenHidingThm :: LEdge DGLinkLab -> Bool
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisProvenHidingThm (_,_,edgeLab) =
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder case dgl_type edgeLab of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder (HidingThm _ (Proven _ _)) -> True
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder _ -> False
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisUnprovenHidingThm :: LEdge DGLinkLab -> Bool
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisUnprovenHidingThm (_,_,edgeLab) =
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder case dgl_type edgeLab of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (HidingThm _ LeftOpen) -> True
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder _ -> False
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder-- ----------------------------------------------------------------------------
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder-- other methods on edges
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder-- ----------------------------------------------------------------------------
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder{- | returns true, if an identical edge is already in the graph or
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder marked to be inserted, false otherwise -}
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisDuplicate :: LEdge DGLinkLab -> DGraph -> [DGChange] -> Bool
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederisDuplicate newEdge dgraph changes =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder elem (InsertEdge newEdge) changes || elem newEdge (labEdges dgraph)
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder{- | returns the DGLinkLab of the given LEdge -}
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedergetLabelOfEdge :: (LEdge b) -> b
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaedergetLabelOfEdge (_,_,label) = label
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder-- ----------------------------------------------
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder-- methods that calculate paths of certain types
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder-- ----------------------------------------------
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedergetAllPathsOfTypeFromGoalList :: DGraph -> (LEdge DGLinkLab -> Bool) ->[LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaedergetAllPathsOfTypeFromGoalList dgraph isType ls =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder concat
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder [concat (map (getAllPathsOfTypeBetween dgraph isType source) targets) |
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder source <- sources]
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder where
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder edgesOfType = [edge | edge <- ls]
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder sources = nub (map getSourceNode edgesOfType)
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder targets = nub (map getTargetNode edgesOfType)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder{- | returns all paths consisting of edges of the given type in the given
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder development graph-}
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllPathsOfType :: DGraph -> (LEdge DGLinkLab -> Bool) -> [[LEdge DGLinkLab]]
c29fabd288a7c6c0b46e134f70b48138aae9214aChristian MaedergetAllPathsOfType dgraph isType =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder concat
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder [concat (map (getAllPathsOfTypeBetween dgraph isType source) targets) |
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder source <- sources]
0678d323bee844db79af13113ae252546629a594Christian Maeder where
0678d323bee844db79af13113ae252546629a594Christian Maeder edgesOfType = [edge | edge <- filter isType (labEdges dgraph)]
c29fabd288a7c6c0b46e134f70b48138aae9214aChristian Maeder sources = nub (map getSourceNode edgesOfType)
0678d323bee844db79af13113ae252546629a594Christian Maeder targets = nub (map getTargetNode edgesOfType)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder{- | returns a list of all proven global paths of the given morphism between
0678d323bee844db79af13113ae252546629a594Christian Maeder the given source and target node-}
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaedergetAllGlobPathsOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder -> [[LEdge DGLinkLab]]
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaedergetAllGlobPathsOfMorphismBetween dgraph morphism src tgt =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder filterPathsByMorphism morphism allPaths
0678d323bee844db79af13113ae252546629a594Christian Maeder where
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder allPaths = getAllGlobPathsBetween dgraph src tgt
0678d323bee844db79af13113ae252546629a594Christian Maeder
0678d323bee844db79af13113ae252546629a594Christian Maeder{- | returns all paths from the given list whose morphism is equal to the
0678d323bee844db79af13113ae252546629a594Christian Maeder given one-}
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederfilterPathsByMorphism :: GMorphism -> [[LEdge DGLinkLab]]
0678d323bee844db79af13113ae252546629a594Christian Maeder -> [[LEdge DGLinkLab]]
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederfilterPathsByMorphism morphism paths =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder [path| path <- paths, (calculateMorphismOfPath path) == (Just morphism)]
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder{- | returns all paths consisting of global edges only
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder or
0678d323bee844db79af13113ae252546629a594Christian Maeder of one local edge followed by any number of global edges-}
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllLocGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllLocGlobPathsBetween dgraph src tgt =
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder locGlobPaths ++ globPaths
0678d323bee844db79af13113ae252546629a594Christian Maeder where
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder outEdges = out dgraph src
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder locEdges = [(edge,target)|edge@(_,target,_) <-
c29fabd288a7c6c0b46e134f70b48138aae9214aChristian Maeder (filter isLocalEdge outEdges)]
c29fabd288a7c6c0b46e134f70b48138aae9214aChristian Maeder locGlobPaths = concat
0678d323bee844db79af13113ae252546629a594Christian Maeder [map ([edge]++)
0678d323bee844db79af13113ae252546629a594Christian Maeder $ getAllPathsOfTypesBetween dgraph isGlobalEdge node tgt []
a625226f55956c1dccb72888417d1f25db3cf173Christian Maeder | (edge, node) <- locEdges]
18c1d987ce5818ecf0bfc8af3f43aed2ce86e1eaChristian Maeder globPaths = getAllPathsOfTypesBetween dgraph isGlobalEdge src tgt []
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder{- | returns all paths of globalDef edges or globalThm edges
0678d323bee844db79af13113ae252546629a594Christian Maeder between the given source and target node -}
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaedergetAllGlobPathsBetween dgraph src tgt =
0678d323bee844db79af13113ae252546629a594Christian Maeder getAllPathsOfTypesBetween dgraph (liftOr isGlobalDef isGlobalThm) src tgt []
4fc4ac78b045c631bc979f849582d9e161568aacChristian Maeder
4fc4ac78b045c631bc979f849582d9e161568aacChristian Maeder{- | returns all paths consiting of edges of the given type between the
0678d323bee844db79af13113ae252546629a594Christian Maeder given node -}
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllPathsOfTypeBetween :: DGraph -> (LEdge DGLinkLab -> Bool) -> Node
0678d323bee844db79af13113ae252546629a594Christian Maeder -> Node -> [[LEdge DGLinkLab]]
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllPathsOfTypeBetween dgraph isType src tgt =
0678d323bee844db79af13113ae252546629a594Christian Maeder getAllPathsOfTypesBetween dgraph isType src tgt []
0678d323bee844db79af13113ae252546629a594Christian Maeder
0678d323bee844db79af13113ae252546629a594Christian Maeder{- | returns all paths consisting of edges of the given types between
0678d323bee844db79af13113ae252546629a594Christian Maeder the given nodes -}
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllPathsOfTypesBetween :: DGraph -> (LEdge DGLinkLab -> Bool) -> Node
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder -> Node -> [LEdge DGLinkLab]
0678d323bee844db79af13113ae252546629a594Christian Maeder -> [[LEdge DGLinkLab]]
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaedergetAllPathsOfTypesBetween dgraph types src tgt path =
0678d323bee844db79af13113ae252546629a594Christian Maeder [edge:path| edge <- edgesFromSrc]
0678d323bee844db79af13113ae252546629a594Christian Maeder ++ (concat
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder [getAllPathsOfTypesBetween dgraph types src nextTgt (edge:path)|
0678d323bee844db79af13113ae252546629a594Christian Maeder (edge,nextTgt) <- nextStep] )
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder where
0678d323bee844db79af13113ae252546629a594Christian Maeder inGoingEdges = inn dgraph tgt
0678d323bee844db79af13113ae252546629a594Christian Maeder edgesOfTypes =
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder [edge| edge <- filter types inGoingEdges, notElem edge path]
0678d323bee844db79af13113ae252546629a594Christian Maeder edgesFromSrc =
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder [edge| edge@(source,_,_) <- edgesOfTypes, source == src]
0678d323bee844db79af13113ae252546629a594Christian Maeder nextStep =
0678d323bee844db79af13113ae252546629a594Christian Maeder [(edge, source)| edge@(source,_,_) <- edgesOfTypes, source /= src]
0678d323bee844db79af13113ae252546629a594Christian Maeder
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllPathsOfTypeFrom :: DGraph -> Node -> (LEdge DGLinkLab -> Bool)
0678d323bee844db79af13113ae252546629a594Christian Maeder -> [[LEdge DGLinkLab]]
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllPathsOfTypeFrom = getAllPathsOfTypeFromAux []
0678d323bee844db79af13113ae252546629a594Christian Maeder
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllPathsOfTypeFromAux :: [LEdge DGLinkLab] -> DGraph -> Node
0678d323bee844db79af13113ae252546629a594Christian Maeder -> (LEdge DGLinkLab -> Bool) -> [[LEdge DGLinkLab]]
0678d323bee844db79af13113ae252546629a594Christian MaedergetAllPathsOfTypeFromAux path dgraph src isType =
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder [path ++ [edge]| edge <- edgesFromSrc, notElem edge path && isType edge]
0678d323bee844db79af13113ae252546629a594Christian Maeder ++(concat
0678d323bee844db79af13113ae252546629a594Christian Maeder [getAllPathsOfTypeFromAux (path ++ [edge]) dgraph nextSrc isType|
0678d323bee844db79af13113ae252546629a594Christian Maeder (edge,nextSrc) <- nextStep])
0678d323bee844db79af13113ae252546629a594Christian Maeder where
0678d323bee844db79af13113ae252546629a594Christian Maeder edgesFromSrc = out dgraph src
nextStep = [(edge,tgt)| edge@(_,tgt,_) <- edgesFromSrc,
tgt /= src && notElem edge path && isType edge]
-- --------------------------------------------------------------
-- methods to determine the inserted edges in the given dgchange
-- --------------------------------------------------------------
{- | returns all insertions of edges from the given list of changes -}
getInsertedEdges :: [DGChange] -> [LEdge DGLinkLab]
getInsertedEdges [] = []
getInsertedEdges (change:list) =
case change of
(InsertEdge edge) -> edge:(getInsertedEdges list)
_ -> getInsertedEdges list
-- ----------------------------------------
-- methods to check and select proof basis
-- ----------------------------------------
{- | determines all proven paths in the given list and tries to select a
proof basis from these (s. selectProofBasisAux);
if this fails the same is done for the rest of the given paths, i.e.
for the unproven ones -}
selectProofBasis :: DGraph -> LEdge DGLinkLab -> [[LEdge DGLinkLab]]
-> [LEdge DGLinkLab]
selectProofBasis dg ledge paths =
if null provenProofBasis then selectProofBasisAux dg ledge unprovenPaths
else provenProofBasis
where
provenPaths = filterProvenPaths paths
provenProofBasis = selectProofBasisAux dg ledge provenPaths
unprovenPaths = filter (`notElem` provenPaths) paths
{- | selects the first path that does not form a proof cycle with the given
label (if such a path exits) and returns the labels of its edges -}
selectProofBasisAux :: DGraph -> LEdge DGLinkLab -> [[LEdge DGLinkLab]]
-> [LEdge DGLinkLab]
selectProofBasisAux _ _ [] = []
selectProofBasisAux dg ledge (path:list) =
if not (roughElem ledge b) then {- OK, no cyclic proof -} b
else selectProofBasisAux dg ledge list
where b = calculateProofBasis dg path []
{- | calculates the proofBasis of the given path,
i.e. (recursively) close the list of DGLinkLabs under the relation
'is proved using'. If a DGLinkLab has proof status LeftOpen,
look up in the development graph for its current status -}
calculateProofBasis :: DGraph -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
-> [LEdge DGLinkLab]
calculateProofBasis _ [] acc = acc
calculateProofBasis dg (ledge@(src,tgt,label):list) acc =
if roughElem ledge acc
then calculateProofBasis dg list acc
else
case oneStepProofBasis label of
Left proofBasis -> calculateProofBasis dg (proofBasis++list) (ledge:acc)
Right True -> calculateProofBasis dg (curProofBasis++list) (ledge:acc)
Right False -> calculateProofBasis dg list (ledge:acc)
where curProofBasis =
case lookup tgt (lsuc dg src) >>= (thmLinkStatus . dgl_type) of
Just (Proven _ proofBasis) -> proofBasis
_ -> []
oneStepProofBasis :: DGLinkLab -> Either [LEdge DGLinkLab] Bool
oneStepProofBasis label =
case dgl_type label of
(GlobalThm (Proven _ proofBasis) _ _) -> Left proofBasis
(LocalThm (Proven _ proofBasis) _ _) -> Left proofBasis
(HidingThm _ (Proven _ proofBasis)) -> Left proofBasis
(GlobalThm LeftOpen _ _) -> Right True
(LocalThm LeftOpen _ _) -> Right True
(HidingThm _ LeftOpen) -> Right True
_ -> Right False -- todo: also treat conservativity proof status
{- | returns all proven paths from the given list -}
filterProvenPaths :: [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
filterProvenPaths = filter (all isProven)
{- | adopts the edges of the old node to the new node -}
adoptEdges :: DGraph -> Node -> Node -> (DGraph, [DGChange])
adoptEdges dgraph oldNode newNode =
if oldNode == newNode then (dgraph, []) else
let inEdges = inn dgraph oldNode
outEdges = out dgraph oldNode
newIn = map (adoptEdgesAux newNode True) inEdges
newOut = map (adoptEdgesAux newNode False) outEdges
allChanges = map DeleteEdge (inEdges ++ outEdges)
++ map InsertEdge (newIn ++ newOut)
in (changesDG dgraph allChanges, allChanges)
{- | auxiliary method for adoptEdges -}
adoptEdgesAux :: Node -> Bool -> LEdge DGLinkLab -> LEdge DGLinkLab
adoptEdgesAux node areIngoingEdges (src,tgt,edgelab) =
let (newSrc,newTgt) = if src == tgt then (node, node) else (src, tgt)
in if areIngoingEdges then (newSrc, node, edgelab)
else (node, newTgt, edgelab)
{- | adjusts a node whose label is changed -}
adjustNode :: DGraph -> (Node, DGNodeLab) -> DGNodeLab -> (DGraph, [DGChange])
adjustNode dgraph (node,oldLab) newLab =
let es = inn dgraph node ++ out dgraph node
changes = map DeleteEdge es ++ [DeleteNode (node, oldLab),
InsertNode (node, newLab)] ++ map InsertEdge es
in (changesDG dgraph changes, changes)
--getAllNodeGoals :: LIB_NAME -> LibEnv -> [DGNodeLab]
--getAllNodeGoals ln libEnv =
-- let dgraph = lookupDgraph ln libEnv
-- in nodes dgraph
getAllOpenNodeGoals :: [DGNodeLab] -> [DGNodeLab]
getAllOpenNodeGoals nodes =
filter hasOpenGoals nodes