{- |

Module : $Header$

Description : Gtk GUI for the consistency checker

Copyright : (c) Thiemo Wiedemeyer, Uni Bremen 2009

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : raider@informatik.uni-bremen.de

Stability : provisional

Portability : portable

This module provides a GUI for the consistency checker.

-}

module GUI.GtkConsistencyChecker

(showConsistencyChecker)

where

import Graphics.UI.Gtk

import Graphics.UI.Gtk.Glade

import Graphics.UI.Gtk.ModelView as MV

import GUI.GtkUtils

import qualified GUI.Glade.ConsistencyChecker as ConsistencyChecker

import GUI.GraphTypes

import Static.DevGraph

import Static.GTheory

import Interfaces.DataTypes

import Interfaces.GenericATPState (guiDefaultTimeLimit)

import Logic.Logic (Language(language_name))

import Logic.Grothendieck

import Logic.Comorphism (AnyComorphism(..))

import Comorphisms.LogicGraph (logicGraph)

import Common.LibName (LibName)

import Control.Concurrent (forkIO, killThread)

import Control.Concurrent.MVar

import Control.Monad (foldM_, join, mapM_, when)

import Proofs.AbstractState

import Proofs.InferBasic (consistencyCheck, ConsistencyStatus (..))

import Data.IORef

import Data.Graph.Inductive.Graph (LNode)

import qualified Data.Map as Map

import Data.List (findIndex)

import Data.Maybe

data Finder = Finder { fName :: String

, finder :: G_cons_checker

, comorphism :: [AnyComorphism]

, selected :: Int }

data FNode = FNode { name :: String

, node :: LNode DGNodeLab

, sublogic :: G_sublogics

, status :: ConsistencyStatus }

instance Eq Finder where

(==) (Finder { fName = n1, comorphism = c1 })

(Finder { fName = n2, comorphism = c2 })= n1 == n2 && c1 == c2

-- | Get a markup string containing name and color

instance Show FNode where

show FNode { name = n, status = s } =

"<span color=\"" ++ statusToColor s ++ "\">" ++ statusToPrefix s ++ n ++

"</span>"

statusToColor :: ConsistencyStatus -> String

statusToColor s = case s of

CSUnchecked -> "black"

CSConsistent _ -> "green"

CSInconsistent _ -> "red"

CSTimeout _ -> "blue"

CSError _ -> "darkred"

statusToPrefix :: ConsistencyStatus -> String

statusToPrefix s = case s of

CSUnchecked -> "[ ] "

CSConsistent _ -> "[+] "

CSInconsistent _ -> "[-] "

CSTimeout _ -> "[t] "

CSError _ -> "[f] "

instance Show ConsistencyStatus where

show CSUnchecked = "Unchecked"

show (CSConsistent s) = s

show (CSInconsistent s) = s

show (CSTimeout s) = s

show (CSError s) = s

instance Eq ConsistencyStatus where

(==) CSUnchecked CSUnchecked = True

(==) (CSConsistent _) (CSConsistent _) = True

(==) (CSInconsistent _) (CSInconsistent _) = True

(==) (CSTimeout _) (CSTimeout _) = True

(==) (CSError _) (CSError _) = True

(==) _ _ = False

-- | Displays the consistency checker window

showConsistencyChecker :: GInfo -> IO ()

showConsistencyChecker gInfo@(GInfo { libName = ln }) = postGUIAsync $ do

xml <- getGladeXML ConsistencyChecker.get

-- get objects

window <- xmlGetWidget xml castToWindow "ConsistencyChecker"

btnClose <- xmlGetWidget xml castToButton "btnClose"

btnResults <- xmlGetWidget xml castToButton "btnResults"

-- get nodes view and buttons

trvNodes <- xmlGetWidget xml castToTreeView "trvNodes"

btnNodesAll <- xmlGetWidget xml castToButton "btnNodesAll"

btnNodesNone <- xmlGetWidget xml castToButton "btnNodesNone"

btnNodesInvert <- xmlGetWidget xml castToButton "btnNodesInvert"

btnNodesUnchecked <- xmlGetWidget xml castToButton "btnNodesUnchecked"

btnNodesTimeout <- xmlGetWidget xml castToButton "btnNodesTimeout"

-- get checker view and buttons

lblComorphism <- xmlGetWidget xml castToLabel "lblComorphism"

lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"

sbTimeout <- xmlGetWidget xml castToSpinButton "sbTimeout"

btnCheck <- xmlGetWidget xml castToButton "btnCheck"

btnStop <- xmlGetWidget xml castToButton "btnStop"

btnFineGrained <- xmlGetWidget xml castToButton "btnFineGrained"

trvFinder <- xmlGetWidget xml castToTreeView "trvFinder"

windowSetTitle window "Consistency Checker"

spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit

let widgets = [ toWidget btnFineGrained

, toWidget sbTimeout

, toWidget lblComorphism

, toWidget lblSublogic ]

checkWidgets = widgets ++ [ toWidget btnClose

, toWidget btnNodesAll

, toWidget btnNodesNone

, toWidget btnNodesInvert

, toWidget btnNodesUnchecked

, toWidget btnNodesTimeout

, toWidget btnResults ]

switch b = do

widgetSetSensitive btnStop $ not b

widgetSetSensitive btnCheck b

widgetSetSensitive btnStop False

widgetSetSensitive btnCheck False

widgetSetSensitive btnResults False

threadId <- newEmptyMVar

wait <- newEmptyMVar

mView <- newEmptyMVar

-- get nodes

(le, dg, nodes) <- do

ost <- readIORef $ intState gInfo

case i_state ost of

Nothing -> error "No state given."

Just ist -> do

let le = i_libEnv ist

dg = lookupDGraph ln le

return (le, dg, labNodesDG dg)

let sls = map sublogicOfTh $ mapMaybe (globalTheory . snd) nodes

-- setup data

listNodes <- setListData trvNodes show

$ map (\ (n@(_,l),s) -> FNode (getDGNodeName l) n s CSUnchecked)

$ zip nodes sls

listFinder <- setListData trvFinder fName []

-- setup view selection actions

let update = do

mf <- getSelectedSingle trvFinder listFinder

case mf of

Just (_,f) -> do

case comorphism f !! selected f of

Comorphism cid ->let cN = language_name cid

dN = drop 1 $ dropWhile (/= ';') cN in

labelSetLabel lblComorphism $ if null dN then "identity" else dN

widgetSetSensitive btnCheck True

Nothing -> do

labelSetLabel lblComorphism "No path selected"

widgetSetSensitive btnCheck False

setListSelectorSingle trvFinder update

setListSelectorMultiple trvNodes btnNodesAll btnNodesNone btnNodesInvert

$ updateNodes trvNodes listNodes

(\ s -> do labelSetLabel lblSublogic $ show s

updateFinder trvFinder listFinder s)

(do labelSetLabel lblSublogic "No sublogic"

listStoreClear listFinder

activate widgets False

widgetSetSensitive btnCheck False)

(do activate widgets True; widgetSetSensitive btnCheck False)

-- bindings

let selectWith f = do

model <- treeViewGetModel trvNodes

sel <- treeViewGetSelection trvNodes

treeModelForeach (fromJust model) $ \ i -> do

(row:[]) <- treeModelGetPath (fromJust model) i

(FNode { status = s }) <- listStoreGetValue listNodes row

(if f s then treeSelectionSelectIter else treeSelectionUnselectIter)

sel i

return False

onClicked btnNodesUnchecked $ selectWith (== CSUnchecked)

onClicked btnNodesTimeout $ selectWith (== CSTimeout "")

onClicked btnResults $ showModelView mView "Models" listNodes

onClicked btnClose $ widgetDestroy window

onClicked btnFineGrained $ fineGrainedSelection trvFinder listFinder update

onClicked btnStop $ takeMVar threadId >>= killThread >>= putMVar wait

onClicked btnCheck $ do

activate checkWidgets False

timeout <- spinButtonGetValueAsInt sbTimeout

(updat, exit) <- progressBar "Checking consistency" "please wait..."

nodes' <- getSelectedMultiple trvNodes listNodes

mf <- getSelectedSingle trvFinder listFinder

f <- case mf of

Nothing -> error "Consistency checker: internal error"

Just (_,f) -> return f

switch False

tid <- forkIO $ do

check ln le dg f timeout listNodes updat nodes'

putMVar wait ()

putMVar threadId tid

forkIO_ $ do

takeMVar wait

postGUIAsync $ do

switch True

tryTakeMVar threadId

showModelView mView "Results of consistency check" listNodes

activate checkWidgets True

exit

widgetShow window

-- | Called when node selection is changed. Updates finder list

updateNodes :: TreeView -> ListStore FNode -> (G_sublogics -> IO ())

-> IO () -> IO () -> IO ()

updateNodes view listNodes update lock unlock = do

nodes <- getSelectedMultiple view listNodes

if null nodes then lock

else let sls = map (sublogic . snd) nodes in

maybe lock (\ sl -> do unlock; update sl)

$ foldl (\ ma b -> case ma of

Just a -> joinSublogics b a

Nothing -> Nothing) (Just $ head sls) $ tail sls

-- | Update the list of finder

updateFinder :: TreeView -> ListStore Finder -> G_sublogics -> IO ()

updateFinder view list sl = do

old <- listStoreToList list

let new = Map.elems $ foldr (\ (cc, c) m ->

let n = getPName cc

f = Map.findWithDefault (Finder n cc [] 0) n m

in Map.insert n (f { comorphism = c : comorphism f}) m) Map.empty

$ getConsCheckers $ findComorphismPaths logicGraph sl

when (old /= new) $ do

-- update list and try to select previos finder

selected' <- getSelectedSingle view list

sel <- treeViewGetSelection view

listStoreClear list

mapM_ (listStoreAppend list) $ mergeFinder old new

maybe (selectFirst view)

(\ (_,f) -> let i = findIndex ((fName f ==) . fName) new in

maybe (selectFirst view) (treeSelectionSelectPath sel . (:[])) i

) selected'

-- | Try to select previos selected comorphism if possible

mergeFinder :: [Finder] -> [Finder] -> [Finder]

mergeFinder old new = let m' = Map.fromList $ map (\ f -> (fName f, f)) new in

Map.elems $ foldl (\ m (Finder { fName = n, comorphism = cc, selected = i}) ->

case Map.lookup n m of

Nothing -> m

Just f@(Finder { comorphism = cc' }) -> let c = cc !! i in

Map.insert n (f { selected = fromMaybe 0 $ findIndex (== c) cc' }) m

) m' old

check :: LibName -> LibEnv -> DGraph -> Finder -> Int -> ListStore FNode

-> (Double -> String -> IO ()) -> [(Int,FNode)] -> IO ()

check ln le dg (Finder { finder = cc, comorphism = cs, selected = i}) timeout

listNodes update nodes = let count' = fromIntegral $ length nodes

c = cs !! i in

foldM_ (\ count (row, fn@(FNode { name = n', node = n })) -> do

postGUISync $ update (count / count') n'

res <- consistencyCheck cc c ln le dg n timeout

postGUISync $ listStoreSetValue listNodes row fn { status = res }

return $ count + 1) 0 nodes

fineGrainedSelection :: TreeView -> ListStore Finder -> IO () -> IO ()

fineGrainedSelection view list unlock = do

paths <- listStoreToList list

selector <- treeViewGetSelection view

if null paths then error "Cant make selection without sublogic!"

else do

ret <- listChoiceAux "Choose a translation"

(\ (n,_,c) -> n ++ ": " ++ show c) $ concatMap expand paths

case ret of

Just (_,(n,_,c)) -> case findIndex ((n ==) . fName) paths of

Just i -> let f = paths !! i in

case findIndex (c ==) $ comorphism f of

Just i' -> do

listStoreSetValue list i $ f { selected = i' }

treeSelectionSelectPath selector [i]

unlock

Nothing -> return ()

Nothing -> return ()

Nothing -> return ()

expand :: Finder -> [(String, G_cons_checker, AnyComorphism)]

expand (Finder { fName = n, finder = cc, comorphism = cs }) =

map (\ c -> (n,cc,c)) cs

-- | Displays the model view window

showModelViewAux :: MVar (IO ()) -> String -> ListStore FNode -> IO ()

showModelViewAux lock title list = do

xml <- getGladeXML ConsistencyChecker.get

-- get objects

window <- xmlGetWidget xml castToWindow "ModelView"

btnClose <- xmlGetWidget xml castToButton "btnResClose"

frNodes <- xmlGetWidget xml castToFrame "frResNodes"

trvNodes <- xmlGetWidget xml castToTreeView "trvResNodes"

tvModel <- xmlGetWidget xml castToTextView "tvResModel"

windowSetTitle window title

-- setup text view

buffer <- textViewGetBuffer tvModel

textBufferInsertAtCursor buffer ""

tagTable <- textBufferGetTagTable buffer

font <- textTagNew Nothing

set font [ textTagFont := "FreeMono" ]

textTagTableAdd tagTable font

start <- textBufferGetStartIter buffer

end <- textBufferGetEndIter buffer

textBufferApplyTag buffer font start end

-- setup list view

let filterNodes = filter ((/= CSUnchecked) . status)

nodes <- listStoreToList list

listNodes <- setListData trvNodes show $ filterNodes nodes

setListSelectorSingle trvNodes $ do

mn <- getSelectedSingle trvNodes listNodes

case mn of

Nothing -> textBufferSetText buffer ""

Just (_,n) -> textBufferSetText buffer $ show $ status n

-- setup actions

onClicked btnClose $ widgetDestroy window

onDestroy window $ do takeMVar lock; return ()

putMVar lock $ do

sel' <- getSelectedSingle trvNodes listNodes

sel <- treeViewGetSelection trvNodes

nodes'' <- listStoreToList list

let nodes' = filterNodes nodes''

updateListData listNodes nodes'

maybe (selectFirst trvNodes) (treeSelectionSelectPath sel . (:[]))

$ maybe Nothing (\ (_,n) -> findIndex ((name n ==) . name) nodes') sel'

widgetSetSizeRequest window 800 600

widgetSetSizeRequest frNodes 250 (-1)

widgetShow window

-- | Displays the model view window

showModelView :: MVar (IO ()) -> String -> ListStore FNode -> IO ()

showModelView lock title list = do

isNotOpen <- isEmptyMVar lock

if isNotOpen then showModelViewAux lock title list

else join (readMVar lock)