TriangleCons.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuDescription : apply triangle-cons rule for all edges in development graphs
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuCopyright : (c) Christian Maeder, DFKI GmbH 2010
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuLicense : GPLv2 or higher, see LICENSE.txt
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuMaintainer : Christian.Maeder@dfki.de
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuStability : provisional
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuPortability : non-portable(Logic)
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport qualified Data.Map as Map
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport qualified Data.Set as Set
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescutriangleConsRule :: DGRule
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescutriangleConsRule = DGRule "TriangleCons"
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescutriangleCons :: LibName -> LibEnv -> Result LibEnv
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescutriangleCons ln le = do
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu let dg = lookupDGraph ln le
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder newDg <- foldM triangleConsDG dg $
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu filter (\ (_, _, l) -> let e = getRealDGLinkType l in
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu edgeTypeModInc e == GlobalDef
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu && getCons (dgl_type l) == Cons
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder $ labEdgesDG dg
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu (groupHistory dg triangleConsRule newDg) le
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescutriangleConsDG :: DGraph -> LEdge DGLinkLab -> Result DGraph
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian MaedertriangleConsDG dg (s, t, l) = do
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu let g = dgBody dg
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder markCons l1 l2 = let
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder l' = l {dgl_type = case dgl_type l of
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu ScopedLink a b _ ->
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu ScopedLink a b $
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder $ Proven triangleConsRule $
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu map dgl_id [l1, l2]
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder in [DeleteEdge (s, t, l), InsertEdge (s, t, l')]
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder checkThm eType =
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder case eType of
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu ThmType (GlobalOrLocalThm _ _) _ _ _ -> True
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder oThm = filter (\ (_, _, ll) -> let e = getRealDGLinkType ll in
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu checkThm (edgeTypeModInc e)
92f658e1afe40c499c1a59b7d1b82079ad9ed5b5mcodescu [] -> return dg -- no outgoing thm link found
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder let bases = filter (\ ((s', _, _), _) -> s == s')
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder $ concatMap (\ dge@(_, tt, _) ->
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder map (\ x -> (x, dge))
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder $ filter (\ (_, _, lx) ->
a77aecc59cee605ea48e33b65a627e0aa0a245e0Mihai Codescu getCons (dgl_type lx) == Cons
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu ) $ inn g tt)
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu case bases of
92f658e1afe40c499c1a59b7d1b82079ad9ed5b5mcodescu [] -> return dg -- no cons link found
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder ((_, _, cl), (_, _, tl)) : _ -> do
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu let changes = markCons cl tl
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu return $ changesDGH dg changes