3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./GUI/ShowRefTree.hs

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Mihai Codescu, DFKI GmbH 2010

3520f6893da8b7397046dfd3dbdae21293647e6fChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

3520f6893da8b7397046dfd3dbdae21293647e6fChristian MaederMaintainer : mihai.codescu@dfki.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

3520f6893da8b7397046dfd3dbdae21293647e6fChristian MaederPortability : non-portable (Logic)

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maederdisplay the logic graph

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski-}

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maedermodule GUI.ShowRefTree (showRefTree) where

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maederimport Control.Monad

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maederimport Data.Graph.Inductive.Graph as Tree

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maederimport Data.IORef

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maederimport GUI.GraphTypes

819ef30d291cb3d17790271f901b0ca03f2b783fChristian Maederimport GUI.UDGUtils as UDG

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport GUI.Utils

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederimport GUI.GraphLogic

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder

ad4da9d870c666f00992431e3badbbe9cc4f19aaChristian Maederimport Interfaces.DataTypes

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederimport Interfaces.Command

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport Common.Consistency

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport Common.DocUtils

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederimport Driver.Options (doDump)

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maederimport Static.DevGraph

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maederimport Static.DgUtils

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maederimport Static.PrintDevGraph

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maederimport Static.History

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport qualified Data.Map as Map

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski

ad4da9d870c666f00992431e3badbbe9cc4f19aaChristian MaedershowRefTree :: LibFunc

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskishowRefTree gInfo = do

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski graph <- newIORef daVinciSort

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder nodesEdges <- newIORef (([], []) :: NodeEdgeListRef)

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder let

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder globalMenu =

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski GlobalMenu (UDG.Menu Nothing

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski [])

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski graphParms = globalMenu $$

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski GraphTitle "Refinement Tree" $$

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski OptimiseLayout True $$

6e538f8086fb560f0b88d49581f0006d6323bdc0Christian Maeder AllowClose (return True) $$

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder emptyGraphParms

734e27bb95c8331c9c262fdd24381b9b9c9d7c28Christian Maeder graph' <- newGraph daVinciSort graphParms

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder addNodesAndEdgesRef gInfo graph' nodesEdges

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder writeIORef graph graph'

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder redraw graph'

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedertype NodeEdgeListRef = ([DaVinciNode Int], [DaVinciArc (IO RTLinkLab)])

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maedertype NodeEdgeListDep = ([DaVinciNode DiagNodeLab], [DaVinciArc (IO String)])

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder

e92e93922166c81167de83cc7400403c5d9bb26cChristian MaederaddNodesAndEdgesRef :: GInfo -> DaVinciGraphTypeSyn ->

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder IORef NodeEdgeListRef -> IO ()

94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederaddNodesAndEdgesRef gInfo@(GInfo { hetcatsOpts = opts}) graph nodesEdges = do

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder ost <- readIORef $ intState gInfo

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder case i_state ost of

eae727f2a1203f1e3c86e40667fe6dfb1173abcbcmaeder Nothing -> return ()

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder Just ist -> do

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder let

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder le = i_libEnv ist

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder lookup' x y = Map.findWithDefault (error "lookup': node not found") y x

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder dg = lookup' le $ i_ln ist

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder rTree = refTree dg

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder vertexes = map fst $ Tree.labNodes rTree

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder isRoot n = any (\ (_, _, llab) -> rtl_type llab == RTComp) $

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder out rTree n

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder -- look for outgoing component links

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder arcs = Tree.labEdges rTree

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder subNodeMenuRoots = LocalMenu (UDG.Menu Nothing [

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder Button "Show dependency diagram" $ showDiagram gInfo dg,

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder Button "Show spec" $ showSpec dg,

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder Button "Check consistency" $ checkCons gInfo])

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder subNodeMenu = LocalMenu (UDG.Menu Nothing [

6e538f8086fb560f0b88d49581f0006d6323bdc0Christian Maeder Button "Show spec" $ showSpec dg,

734e27bb95c8331c9c262fdd24381b9b9c9d7c28Christian Maeder Button "Check consistency" $ checkCons gInfo])

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder subNodeTypeParmsR = subNodeMenuRoots $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich Ellipse $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich ValueTitle (return . rtn_name . labRT dg) $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich Color (getColor opts Green True True) $$$

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder emptyNodeTypeParms

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder subNodeTypeParms = subNodeMenu $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich Ellipse $$$

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder ValueTitle (return . rtn_name . labRT dg) $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich Color (getColor opts Green True True) $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich emptyNodeTypeParms

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder subNodeType <- newNodeType graph subNodeTypeParms

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich -- subNodeListI <- mapM (newNode graph subNodeType) internal

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich subNodeTypeR <- newNodeType graph subNodeTypeParmsR

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich subNodeList <- mapM (\ x -> if isRoot x then

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder newNode graph subNodeTypeR x

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder else newNode graph subNodeType x) vertexes

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder -- let subNodeList = subNodeListI ++ subNodeListR

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich let

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich nodes' = Map.fromList $ zip (Tree.nodes rTree) subNodeList

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich subArcMenu = LocalMenu (UDG.Menu Nothing [])

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich subArcTypeParms = subArcMenu $$$

819ef30d291cb3d17790271f901b0ca03f2b783fChristian Maeder ValueTitle (return $ return "") $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich Color (getColor opts Black False False) $$$

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder emptyArcTypeParms

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich subArcTypeParmsT = subArcMenu $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich ValueTitle (return $ return "") $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich Color (getColor opts Blue False False) $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich emptyArcTypeParms

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich subArcTypeParmsR = subArcMenu $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich ValueTitle (return $ return "") $$$

6e538f8086fb560f0b88d49581f0006d6323bdc0Christian Maeder Color (getColor opts Coral False False) $$$

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich emptyArcTypeParms

e444c9b47fae2490b64e6a465d3706a07b2f6d84Klaus Luettich subArcType <- newArcType graph subArcTypeParms

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder let insertSubArc (n1, n2, e) = newArc graph subArcType

819ef30d291cb3d17790271f901b0ca03f2b783fChristian Maeder (return e)

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder (lookup' nodes' n1)

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (lookup' nodes' n2)

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder subArcList <- mapM insertSubArc $

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder filter (\ (_, _, e) -> rtl_type e == RTComp) arcs

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder subArcTypeT <- newArcType graph subArcTypeParmsT

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let insertSubArcT (n1, n2, e) = newArc graph subArcTypeT

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder (return e)

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder (lookup' nodes' n1)

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (lookup' nodes' n2)

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder subArcListT <- mapM insertSubArcT $

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder filter (\ (_, _, _e) -> False) -- TODO: it was easier

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder arcs

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder subArcTypeR <- newArcType graph subArcTypeParmsR

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder let insertSubArcR (n1, n2, e) = newArc graph subArcTypeR

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder (return e)

e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder (lookup' nodes' n1)

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder (lookup' nodes' n2)

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder subArcListR <- mapM insertSubArcR $

5f0d686f35e3cf510a32517fe5a2788d591964aeChristian Maeder filter (\ (_, _, e) -> rtl_type e == RTRefine) arcs

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder writeIORef nodesEdges (subNodeList, subArcList ++ subArcListT

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder ++ subArcListR)

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder

819ef30d291cb3d17790271f901b0ca03f2b783fChristian MaedercheckCons :: GInfo -> Int -> IO ()

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian MaedercheckCons gInfo n = do

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder lockGlobal gInfo

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder checkConsAux gInfo [n]

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian MaedercheckConsAux :: GInfo -> [Int] -> IO ()

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian MaedercheckConsAux gInfo [] = unlockGlobal gInfo

3520f6893da8b7397046dfd3dbdae21293647e6fChristian MaedercheckConsAux gInfo (n : ns) = do

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder ost <- readIORef $ intState gInfo

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder case i_state ost of

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder Nothing -> return ()

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder Just ist -> do

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder let

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder le = i_libEnv ist

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder lookup' x y = Map.findWithDefault (error "lookup': node not found") y x

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder dg = lookup' le $ i_ln ist

3520f6893da8b7397046dfd3dbdae21293647e6fChristian Maeder rtlab = labRT dg n

6a245e3ef6baa0923c02062da35d035dfd2c82a4Christian Maeder rt = refTree dg

6e538f8086fb560f0b88d49581f0006d6323bdc0Christian Maeder changeConsStatus x = let

oldLab = labDG dg x

oldNInfo = nodeInfo oldLab

newLab = oldLab {nodeInfo = case oldNInfo of

DGNode o _ -> DGNode o $ mkConsStatus Cons

_ -> oldNInfo}

in [SetNodeLab oldLab (x, newLab)]

consLinks (s, t, l) = let

l' = l {dgl_type = case dgl_type l of

ScopedLink a b _ ->

ScopedLink a b $ mkConsStatus Cons

dt -> dt}

in [DeleteEdge (s, t, l), InsertEdge (s, t, l')]

updateDG changes = do

let dg' = changesDGH dg changes

history = snd $ splitHistory dg dg'

le' = Map.insert (i_ln ist) dg' le

lln = map DgCommandChange $ calcGlobalHistory le le'

nst = add2history HelpCmd ost lln

nwst = nst { i_state = Just ist { i_libEnv = le'}}

doDump (hetcatsOpts gInfo) "PrintHistory" $ do

putStrLn "History"

print $ prettyHistory history

writeIORef (intState gInfo) nwst

updateGraph gInfo (reverse $ flatHistory history)

case rtn_type rtlab of

RTRef n' -> checkConsAux gInfo $ n' : ns

RTPlain usig ->

let units = map (\ (_, x, _) -> x) $

filter (\ (_ss, _tt, ll) -> rtl_type ll == RTComp) $ out rt n

in case units of

[] -> -- n is itself a unit, insert obligation

case usig of

UnitSig [] nsig _ -> do -- non-parametric unit, change node

let gn = getNode nsig

changes = changeConsStatus gn

updateDG changes

checkConsAux gInfo ns

UnitSig _ _ Nothing -> error "consCheck2"

UnitSig _nsigs nsig (Just usig') -> do

let ss = getNode usig'

tt = getNode nsig

lEdges = filter (\ (x, y, _) -> x == ss && y == tt)

$ labEdges $ dgBody dg

ll = if null lEdges then

error "consCheck1"

else head lEdges -- parametric unit, change edge

changes = consLinks ll

updateDG changes

checkConsAux gInfo ns

_ -> checkConsAux gInfo $ units ++ ns

showSpec :: DGraph -> Int -> IO ()

showSpec dg n =

createTextDisplay "" (showDoc (labRT dg n) "")

showDiagram :: GInfo -> DGraph -> Int -> IO ()

showDiagram gInfo dg n = do

let asDiags = archSpecDiags dg

rtlab = labRT dg n

name = rtn_diag rtlab

when (name `elem` Map.keys asDiags) $ do

graph <- newIORef daVinciSort

nodesEdges <- newIORef (([], []) :: NodeEdgeListDep)

let

globalMenu =

GlobalMenu (UDG.Menu Nothing

[])

graphParms = globalMenu $$

GraphTitle ("Dependency Diagram for " ++ name) $$

OptimiseLayout True $$

AllowClose (return True) $$

emptyGraphParms

graph' <- newGraph daVinciSort graphParms

addNodesAndEdgesDeps dg (Map.findWithDefault (error "showDiagram")

name asDiags)

graph' gInfo nodesEdges

writeIORef graph graph'

redraw graph'

showDiagSpec :: DGraph -> DiagNodeLab -> IO ()

showDiagSpec dg l = do

let NodeSig n _ = dn_sig l

nlab = labDG dg n

g1 = globOrLocTh nlab

createTextDisplay ""

$ "Desc:\n" ++ dn_desc l ++ "\n" ++

"Sig:\n" ++ showDoc g1 ""

addNodesAndEdgesDeps :: DGraph -> Diag -> DaVinciGraphTypeSyn -> GInfo ->

IORef NodeEdgeListDep -> IO ()

addNodesAndEdgesDeps dg diag graph gi nodesEdges = do

let

opts = hetcatsOpts gi

lookup' x y = Map.findWithDefault (error "lookup': node not found") y x

vertexes = map snd $ Tree.labNodes $ diagGraph diag

arcs = Tree.labEdges $ diagGraph diag

subNodeMenu = LocalMenu (UDG.Menu Nothing [Button "Show desc and sig" $

showDiagSpec dg ])

subNodeTypeParms = subNodeMenu $$$

Ellipse $$$

ValueTitle (return . (\ x ->

take 20 (dn_desc x) ++ "..." )) $$$

Color (getColor opts Green True True) $$$

emptyNodeTypeParms

subNodeType <- newNodeType graph subNodeTypeParms

subNodeList <- mapM (newNode graph subNodeType) vertexes

let

nodes' = Map.fromList $ zip (Tree.nodes $ diagGraph diag) subNodeList

subArcMenu = LocalMenu (UDG.Menu Nothing [])

subArcTypeParms = subArcMenu $$$

ValueTitle (return $ return "") $$$

Color (getColor opts Black False False) $$$

emptyArcTypeParms

subArcType <- newArcType graph subArcTypeParms

let insertSubArc (n1, n2, _e) = newArc graph subArcType

(return "")

(lookup' nodes' n1)

(lookup' nodes' n2)

subArcList <- mapM insertSubArc arcs

writeIORef nodesEdges (subNodeList, subArcList)