2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Proofs/TriangleCons.hs

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 Codescu

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuMaintainer : Christian.Maeder@dfki.de

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuStability : provisional

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuPortability : non-portable(Logic)

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu-}

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescumodule Proofs.TriangleCons where

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Static.DevGraph

c208973c890b8f993297720fd0247bc7481d4304Christian Maederimport Static.DgUtils

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Static.History

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Common.Consistency

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Common.Result

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Common.LibName

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport qualified Data.Map as Map

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport qualified Data.Set as Set

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Data.Graph.Inductive.Graph

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Control.Monad

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescutriangleConsRule :: DGRule

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescutriangleConsRule = DGRule "TriangleCons"

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu

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

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu )

a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder $ labEdgesDG dg

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu return $ Map.insert ln

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu (groupHistory dg triangleConsRule newDg) le

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu

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 ConsStatus

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu Cons

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu Cons

a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder $ Proven triangleConsRule $

a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder ProofBasis $ Set.fromList $

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu map dgl_id [l1, l2]

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu dt -> dt}

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

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu _ -> False

a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder oThm = filter (\ (_, _, ll) -> let e = getRealDGLinkType ll in

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu checkThm (edgeTypeModInc e)

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu ) $ out g t

a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder case oThm of

92f658e1afe40c499c1a59b7d1b82079ad9ed5b5mcodescu [] -> return dg -- no outgoing thm link found

2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu _ -> do

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 oThm

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