{- |
Module      :  ./GUI/GtkAutomaticProofs.hs
Description :  Gtk GUI for automatic proving procedure of multiple nodes
Copyright   :  (c) Simon Ulbricht, Uni Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  tekknix@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

This module provides a GUI for the automatic proofs module.
-}

module GUI.GtkAutomaticProofs
  (showAutomaticProofs, Finder (..))
  where

import Graphics.UI.Gtk

import qualified GUI.Glade.NodeChecker as ConsistencyChecker
import GUI.GraphTypes
import GUI.GtkUtils

import Static.DevGraph
import Static.DgUtils
import Static.PrintDevGraph ()
import Static.GTheory
import Static.History
import Static.ComputeTheory

import Interfaces.GenericATPState (guiDefaultTimeLimit)

import Logic.Grothendieck
import Logic.Comorphism (AnyComorphism (..))
import Logic.Prover

import Comorphisms.LogicGraph (logicGraph)

import Common.LibName (LibName)
import Common.AutoProofUtils
import Common.Result
import Common.ResultT

import Control.Concurrent (forkIO, killThread)
import Control.Concurrent.MVar
import Control.Monad (foldM_, join, when)
import Control.Monad.Trans
import qualified Control.Monad.Fail as Fail

import Proofs.AbstractState

import qualified Data.Map as Map
import Data.List
import Data.Maybe

import Interfaces.Utils

-- | Data structure for saving the user-selected prover and comorphism
data Finder = Finder { Finder -> String
fName :: String
                     , Finder -> G_prover
finder :: G_prover
                     , Finder -> [AnyComorphism]
comorphism :: [AnyComorphism]
                     , Finder -> Int
selected :: Int }

instance Eq Finder where
  f1 :: Finder
f1 == :: Finder -> Finder -> Bool
== f2 :: Finder
f2 = Finder -> String
fName Finder
f1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Finder -> String
fName Finder
f2 Bool -> Bool -> Bool
&& Finder -> [AnyComorphism]
comorphism Finder
f1 [AnyComorphism] -> [AnyComorphism] -> Bool
forall a. Eq a => a -> a -> Bool
== Finder -> [AnyComorphism]
comorphism Finder
f2

-- | Displays the consistency checker window
showAutomaticProofs :: GInfo -> LibEnv -> IO (Result LibEnv)
showAutomaticProofs :: GInfo -> LibEnv -> IO (Result LibEnv)
showAutomaticProofs ginf :: GInfo
ginf@(GInfo { libName :: GInfo -> LibName
libName = LibName
ln }) le :: LibEnv
le = do
  MVar LibEnv
wait <- IO (MVar LibEnv)
forall a. IO (MVar a)
newEmptyMVar
  GInfo -> MVar LibEnv -> LibName -> LibEnv -> IO ()
showProverWindow GInfo
ginf MVar LibEnv
wait LibName
ln LibEnv
le
  LibEnv
le' <- MVar LibEnv -> IO LibEnv
forall a. MVar a -> IO a
takeMVar MVar LibEnv
wait
  Result LibEnv -> IO (Result LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result LibEnv -> IO (Result LibEnv))
-> Result LibEnv -> IO (Result LibEnv)
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe LibEnv -> Result LibEnv
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe LibEnv -> Result LibEnv) -> Maybe LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ LibEnv -> Maybe LibEnv
forall a. a -> Maybe a
Just LibEnv
le'

-- | Displays the consistency checker window
showProverWindow :: GInfo -> MVar LibEnv -> LibName -> LibEnv -> IO ()
showProverWindow :: GInfo -> MVar LibEnv -> LibName -> LibEnv -> IO ()
showProverWindow ginf :: GInfo
ginf res :: MVar LibEnv
res ln :: LibName
ln le :: LibEnv
le = IO () -> IO ()
postGUIAsync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  Builder
builder <- (String, String) -> IO Builder
getGTKBuilder (String, String)
ConsistencyChecker.get
  -- get objects
  Window
window <- Builder -> (GObject -> Window) -> String -> IO Window
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Window
forall obj. GObjectClass obj => obj -> Window
castToWindow "NodeChecker"
  Button
btnClose <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnClose"
  Button
btnResults <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnResults"
  -- get nodes view and buttons
  TreeView
trvNodes <- Builder -> (GObject -> TreeView) -> String -> IO TreeView
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> TreeView
forall obj. GObjectClass obj => obj -> TreeView
castToTreeView "trvNodes"
  Button
btnNodesAll <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesAll"
  Button
btnNodesNone <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesNone"
  Button
btnNodesInvert <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesInvert"
  Button
btnNodesUnchecked <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesUnchecked"
  Button
btnNodesTimeout <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesTimeout"
  CheckButton
cbInclThms <- Builder -> (GObject -> CheckButton) -> String -> IO CheckButton
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> CheckButton
forall obj. GObjectClass obj => obj -> CheckButton
castToCheckButton "cbInclThms"
  -- get checker view and buttons
  ComboBox
cbComorphism <- Builder -> (GObject -> ComboBox) -> String -> IO ComboBox
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> ComboBox
forall obj. GObjectClass obj => obj -> ComboBox
castToComboBox "cbComorphism"
  Label
lblSublogic <- Builder -> (GObject -> Label) -> String -> IO Label
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Label
forall obj. GObjectClass obj => obj -> Label
castToLabel "lblSublogic"
  SpinButton
sbTimeout <- Builder -> (GObject -> SpinButton) -> String -> IO SpinButton
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> SpinButton
forall obj. GObjectClass obj => obj -> SpinButton
castToSpinButton "sbTimeout"
  Button
btnCheck <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnCheck"
  Button
btnStop <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnStop"
  -- btnFineGrained    <- builderGetObject builder castToButton "btnFineGrained"
  TreeView
trvFinder <- Builder -> (GObject -> TreeView) -> String -> IO TreeView
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> TreeView
forall obj. GObjectClass obj => obj -> TreeView
castToTreeView "trvFinder"
  Label
toolLabel <- Builder -> (GObject -> Label) -> String -> IO Label
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Label
forall obj. GObjectClass obj => obj -> Label
castToLabel "label1"
  Label -> String -> IO ()
forall self string.
(LabelClass self, GlibString string) =>
self -> string -> IO ()
labelSetLabel Label
toolLabel "Pick prover"
  Window -> String -> IO ()
forall self string.
(WindowClass self, GlibString string) =>
self -> string -> IO ()
windowSetTitle Window
window "AutomaticProofs"
  SpinButton -> Double -> IO ()
forall self. SpinButtonClass self => self -> Double -> IO ()
spinButtonSetValue SpinButton
sbTimeout (Double -> IO ()) -> Double -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
guiDefaultTimeLimit

  let widgets :: [Widget]
widgets = [ SpinButton -> Widget
forall o. WidgetClass o => o -> Widget
toWidget SpinButton
sbTimeout
                , ComboBox -> Widget
forall o. WidgetClass o => o -> Widget
toWidget ComboBox
cbComorphism
                , Label -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Label
lblSublogic ]
      checkWidgets :: [Widget]
checkWidgets = [Widget]
widgets [Widget] -> [Widget] -> [Widget]
forall a. [a] -> [a] -> [a]
++ [ Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnClose
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesAll
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesNone
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesInvert
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesUnchecked
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesTimeout
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnResults ]
      switch :: Bool -> IO ()
switch b :: Bool
b = do
        Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnStop (Bool -> IO ()) -> Bool -> IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b
        Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
b

  CheckButton -> Bool -> IO ()
forall self. ToggleButtonClass self => self -> Bool -> IO ()
toggleButtonSetActive CheckButton
cbInclThms Bool
False

  Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnStop Bool
False
  Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
False

  MVar ThreadId
threadId <- IO (MVar ThreadId)
forall a. IO (MVar a)
newEmptyMVar
  MVar ()
wait <- IO (MVar ())
forall a. IO (MVar a)
newEmptyMVar
  MVar (IO ())
mView <- IO (MVar (IO ()))
forall a. IO (MVar a)
newEmptyMVar

  let dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
      nodes :: [FNode]
nodes = [LNode DGNodeLab] -> [FNode]
initFNodes ([LNode DGNodeLab] -> [FNode]) -> [LNode DGNodeLab] -> [FNode]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dg

  -- setup data
  ListStore FNode
listNodes <- TreeView -> (FNode -> String) -> [FNode] -> IO (ListStore FNode)
forall a. TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData TreeView
trvNodes FNode -> String
forall a. Show a => a -> String
show ([FNode] -> IO (ListStore FNode))
-> [FNode] -> IO (ListStore FNode)
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort [FNode]
nodes
  ListStore Finder
listFinder <- TreeView -> (Finder -> String) -> [Finder] -> IO (ListStore Finder)
forall a. TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData TreeView
trvFinder Finder -> String
fName []

  -- setup comorphism combobox
  ComboBox -> IO (ListStore ComboBoxText)
forall self.
ComboBoxClass self =>
self -> IO (ListStore ComboBoxText)
comboBoxSetModelText ComboBox
cbComorphism
  ConnectId ComboBox
shC <- ComboBox
-> Signal ComboBox (IO ()) -> IO () -> IO (ConnectId ComboBox)
forall object callback.
object
-> Signal object callback -> callback -> IO (ConnectId object)
after ComboBox
cbComorphism Signal ComboBox (IO ())
forall self. ComboBoxClass self => Signal self (IO ())
changed
    (IO () -> IO (ConnectId ComboBox))
-> IO () -> IO (ConnectId ComboBox)
forall a b. (a -> b) -> a -> b
$ TreeView -> ListStore Finder -> ComboBox -> IO ()
setSelectedComorphism TreeView
trvFinder ListStore Finder
listFinder ComboBox
cbComorphism

  -- setup view selection actions
  let update :: IO ()
update = do
        Maybe (Int, Finder)
mf <- TreeView -> ListStore Finder -> IO (Maybe (Int, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvFinder ListStore Finder
listFinder
        TreeView
-> ListStore Finder -> ComboBox -> ConnectId ComboBox -> IO ()
updateComorphism TreeView
trvFinder ListStore Finder
listFinder ComboBox
cbComorphism ConnectId ComboBox
shC
        Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck (Bool -> IO ()) -> Bool -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe (Int, Finder) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Int, Finder)
mf
  TreeView -> IO () -> IO (ConnectId TreeSelection)
setListSelectorSingle TreeView
trvFinder IO ()
update

  let upd :: IO ()
upd = TreeView
-> ListStore FNode
-> (G_sublogics -> IO ())
-> IO ()
-> IO ()
-> IO ()
updateNodes TreeView
trvNodes ListStore FNode
listNodes
              (\ s :: G_sublogics
s -> do
                Label -> String -> IO ()
forall self string.
(LabelClass self, GlibString string) =>
self -> string -> IO ()
labelSetLabel Label
lblSublogic (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
s
                TreeView -> ListStore Finder -> G_sublogics -> IO ()
updateFinder TreeView
trvFinder ListStore Finder
listFinder G_sublogics
s )
              (do
                Label -> String -> IO ()
forall self string.
(LabelClass self, GlibString string) =>
self -> string -> IO ()
labelSetLabel Label
lblSublogic "No sublogic"
                ListStore Finder -> IO ()
forall a. ListStore a -> IO ()
listStoreClear ListStore Finder
listFinder
                [Widget] -> Bool -> IO ()
activate [Widget]
widgets Bool
False
                Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
False)
              ([Widget] -> Bool -> IO ()
activate [Widget]
widgets Bool
True IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
True)

  ConnectId TreeSelection
shN <- TreeView
-> Button
-> Button
-> Button
-> IO ()
-> IO (ConnectId TreeSelection)
setListSelectorMultiple TreeView
trvNodes Button
btnNodesAll Button
btnNodesNone
    Button
btnNodesInvert IO ()
upd

  -- bindings

  {- this function handles the selction of nodes, getting as input parameter
  a function f (FNode -> Bool). -}
  let selectWith :: (FNode -> Bool) -> IO b -> IO b
selectWith f :: FNode -> Bool
f u :: IO b
u = do
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId TreeSelection
shN
        TreeSelection
sel <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvNodes
        TreeSelection -> IO ()
forall self. TreeSelectionClass self => self -> IO ()
treeSelectionSelectAll TreeSelection
sel
        [TreePath]
rs <- TreeSelection -> IO [TreePath]
forall self. TreeSelectionClass self => self -> IO [TreePath]
treeSelectionGetSelectedRows TreeSelection
sel
        (TreePath -> IO ()) -> [TreePath] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ ~p :: TreePath
p@(row :: Int
row : []) -> do
          FNode
fn <- ListStore FNode -> Int -> IO FNode
forall a. ListStore a -> Int -> IO a
listStoreGetValue ListStore FNode
listNodes Int
row
          (if FNode -> Bool
f FNode
fn then TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath else TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionUnselectPath)
            TreeSelection
sel TreePath
p) [TreePath]
rs
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId TreeSelection
shN
        IO b
u

  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnNodesUnchecked
    (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ (FNode -> Bool) -> IO () -> IO ()
forall b. (FNode -> Bool) -> IO b -> IO b
selectWith FNode -> Bool
unchecked IO ()
upd
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnNodesTimeout (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ (FNode -> Bool) -> IO () -> IO ()
forall b. (FNode -> Bool) -> IO b -> IO b
selectWith FNode -> Bool
timedout IO ()
upd

  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnResults (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelView MVar (IO ())
mView "Models" ListStore FNode
listNodes []
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnClose (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetDestroy Window
window
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnStop (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ MVar ThreadId -> IO ThreadId
forall a. MVar a -> IO a
takeMVar MVar ThreadId
threadId IO ThreadId -> (ThreadId -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ThreadId -> IO ()
killThread IO () -> (() -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
wait

  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnCheck (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
    [Widget] -> Bool -> IO ()
activate [Widget]
checkWidgets Bool
False
    Int
timeout <- SpinButton -> IO Int
forall self. SpinButtonClass self => self -> IO Int
spinButtonGetValueAsInt SpinButton
sbTimeout
    Bool
inclThms <- CheckButton -> IO Bool
forall self. ToggleButtonClass self => self -> IO Bool
toggleButtonGetActive CheckButton
cbInclThms
    (prgBar :: Double -> String -> IO ()
prgBar, exit :: IO ()
exit) <- String -> String -> IO (Double -> String -> IO (), IO ())
progressBar "Proving" "please wait..."
    [(Int, FNode)]
nodes' <- TreeView -> ListStore FNode -> IO [(Int, FNode)]
forall a. TreeView -> ListStore a -> IO [(Int, a)]
getSelectedMultiple TreeView
trvNodes ListStore FNode
listNodes
    Maybe (Int, Finder)
mf <- TreeView -> ListStore Finder -> IO (Maybe (Int, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvFinder ListStore Finder
listFinder
    Finder
f <- case Maybe (Int, Finder)
mf of
      Nothing -> String -> IO Finder
forall a. HasCallStack => String -> a
error "Automatic Proofs: internal error"
      Just (_, f :: Finder
f) -> Finder -> IO Finder
forall (m :: * -> *) a. Monad m => a -> m a
return Finder
f
    Bool -> IO ()
switch Bool
False
    ThreadId
tid <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ do
      GInfo
-> Bool
-> Int
-> (Double -> String -> IO ())
-> Finder
-> ListStore FNode
-> [(Int, FNode)]
-> IO ()
performAutoProof GInfo
ginf Bool
inclThms Int
timeout Double -> String -> IO ()
prgBar Finder
f ListStore FNode
listNodes [(Int, FNode)]
nodes'
      MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
wait ()
    MVar ThreadId -> ThreadId -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ThreadId
threadId ThreadId
tid
    IO () -> IO ()
forkIO_ (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
wait
      IO () -> IO ()
postGUIAsync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Bool -> IO ()
switch Bool
True
        MVar ThreadId -> IO (Maybe ThreadId)
forall a. MVar a -> IO (Maybe a)
tryTakeMVar MVar ThreadId
threadId
        MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelView MVar (IO ())
mView "Results of automatic proofs" ListStore FNode
listNodes []
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId TreeSelection
shN
        TreeView -> ListStore FNode -> IO ()
sortNodes TreeView
trvNodes ListStore FNode
listNodes
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId TreeSelection
shN
        IO ()
upd
        [Widget] -> Bool -> IO ()
activate [Widget]
checkWidgets Bool
True
        IO ()
exit

  {- after window is closed, the results are written back into the DGraph.
  for each node a DGChange object is created and applied to the DGraph. -}
  Window -> IO () -> IO (ConnectId Window)
forall w. WidgetClass w => w -> IO () -> IO (ConnectId w)
onDestroy Window
window (IO () -> IO (ConnectId Window)) -> IO () -> IO (ConnectId Window)
forall a b. (a -> b) -> a -> b
$ do
    [FNode]
nodes' <- ListStore FNode -> IO [FNode]
forall a. ListStore a -> IO [a]
listStoreToList ListStore FNode
listNodes
    let dg' :: DGraph
dg' = (DGraph -> FNode -> DGraph) -> DGraph -> [FNode] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ cs :: DGraph
cs fn :: FNode
fn ->
                      {- where the proving did not return anything, the node is
                      not updated -}
                      if FNode -> Bool
unchecked FNode
fn then DGraph
cs
                          else LibEnv
-> LibName -> DGraph -> LNode DGNodeLab -> G_theory -> DGraph
updateLabelTheory LibEnv
le LibName
ln DGraph
cs (FNode -> LNode DGNodeLab
node FNode
fn) (FNode -> G_theory
results FNode
fn)
                    ) DGraph
dg [FNode]
nodes'

    MVar LibEnv -> LibEnv -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar LibEnv
res (LibEnv -> IO ()) -> LibEnv -> IO ()
forall a b. (a -> b) -> a -> b
$ LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln (DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg (String -> DGRule
DGRule "autoproof") DGraph
dg') LibEnv
le

  -- setting up the selected items at startup
  (FNode -> Bool) -> IO () -> IO ()
forall b. (FNode -> Bool) -> IO b -> IO b
selectWith (Bool -> Bool
not (Bool -> Bool) -> (FNode -> Bool) -> FNode -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> Bool
allProved) IO ()
upd

  -- TODO select SPASS Prover if possible
  Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetShow Window
window


performAutoProof :: GInfo
                    -- include proven Theorems in subsequent proofs
                  -> Bool
                    -- Timeout (sec)
                  -> Int
                    -- Progress bar
                  -> (Double -> String -> IO ())
                    -- selcted Prover and Comorphism
                  -> Finder
                    -- Display function for node selection box
                  -> ListStore FNode
                    -- selected nodes
                  -> [(Int, FNode)]
                    {- no return value, since results are stored by changing
                    FNode data -}
                  -> IO ()
performAutoProof :: GInfo
-> Bool
-> Int
-> (Double -> String -> IO ())
-> Finder
-> ListStore FNode
-> [(Int, FNode)]
-> IO ()
performAutoProof gi :: GInfo
gi inclThms :: Bool
inclThms timeout :: Int
timeout update :: Double -> String -> IO ()
update (Finder _ pr :: G_prover
pr cs :: [AnyComorphism]
cs i :: Int
i) listNodes :: ListStore FNode
listNodes nodes :: [(Int, FNode)]
nodes =
  let count' :: Double
count' = Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Double) -> Int -> Double
forall a b. (a -> b) -> a -> b
$ [(Int, FNode)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, FNode)]
nodes
      c :: AnyComorphism
c = [AnyComorphism]
cs [AnyComorphism] -> Int -> AnyComorphism
forall a. [a] -> Int -> a
!! Int
i
  in (Double -> (Int, FNode) -> IO Double)
-> Double -> [(Int, FNode)] -> IO ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (\ count :: Double
count (row :: Int
row, fn :: FNode
fn) -> do
           IO () -> IO ()
forall a. IO a -> IO a
postGUISync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Double -> String -> IO ()
update (Double
count Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
count') (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ FNode -> String
name FNode
fn
           Maybe G_theory
res <- IO (Maybe G_theory)
-> (G_theory -> IO (Maybe G_theory))
-> Maybe G_theory
-> IO (Maybe G_theory)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Maybe G_theory -> IO (Maybe G_theory)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe G_theory
forall a. Maybe a
Nothing) (\ g_th :: G_theory
g_th -> do
                    Result ds :: [Diagnosis]
ds ms :: Maybe (G_theory, [(String, String, String)])
ms <- ResultT IO (G_theory, [(String, String, String)])
-> IO (Result (G_theory, [(String, String, String)]))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT
                        (do
                          (a :: (G_theory, [(String, String, String)])
a, b :: (ProofState, [ProofStatus G_proof_tree])
b) <- Bool
-> Int
-> [String]
-> [String]
-> G_theory
-> (G_prover, AnyComorphism)
-> ResultT
     IO
     ((G_theory, [(String, String, String)]),
      (ProofState, [ProofStatus G_proof_tree]))
autoProofAtNode Bool
inclThms Int
timeout [] [] G_theory
g_th
                            (G_prover
pr, AnyComorphism
c)
                          IO () -> ResultT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ IORef IntState
-> ProofState
-> Maybe (G_prover, AnyComorphism)
-> [ProofStatus G_proof_tree]
-> String
-> (Bool, Int)
-> IO ()
forall proof_tree.
IORef IntState
-> ProofState
-> Maybe (G_prover, AnyComorphism)
-> [ProofStatus proof_tree]
-> String
-> (Bool, Int)
-> IO ()
addCommandHistoryToState (GInfo -> IORef IntState
intState GInfo
gi)
                            ((ProofState, [ProofStatus G_proof_tree]) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, [ProofStatus G_proof_tree])
b) ((G_prover, AnyComorphism) -> Maybe (G_prover, AnyComorphism)
forall a. a -> Maybe a
Just (G_prover
pr, AnyComorphism
c)) ((ProofState, [ProofStatus G_proof_tree])
-> [ProofStatus G_proof_tree]
forall a b. (a, b) -> b
snd (ProofState, [ProofStatus G_proof_tree])
b) (FNode -> String
name FNode
fn)
                            (Bool
True, Int
timeout)
                          (G_theory, [(String, String, String)])
-> ResultT IO (G_theory, [(String, String, String)])
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory, [(String, String, String)])
a)
                    IO (Maybe G_theory)
-> ((G_theory, [(String, String, String)]) -> IO (Maybe G_theory))
-> Maybe (G_theory, [(String, String, String)])
-> IO (Maybe G_theory)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> IO (Maybe G_theory)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> IO (Maybe G_theory)) -> String -> IO (Maybe G_theory)
forall a b. (a -> b) -> a -> b
$ Int -> [Diagnosis] -> String
showRelDiags 1 [Diagnosis]
ds) (Maybe G_theory -> IO (Maybe G_theory)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe G_theory -> IO (Maybe G_theory))
-> ((G_theory, [(String, String, String)]) -> Maybe G_theory)
-> (G_theory, [(String, String, String)])
-> IO (Maybe G_theory)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_theory -> Maybe G_theory
forall a. a -> Maybe a
Just (G_theory -> Maybe G_theory)
-> ((G_theory, [(String, String, String)]) -> G_theory)
-> (G_theory, [(String, String, String)])
-> Maybe G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_theory, [(String, String, String)]) -> G_theory
forall a b. (a, b) -> a
fst) Maybe (G_theory, [(String, String, String)])
ms)
                  (Maybe G_theory -> IO (Maybe G_theory))
-> Maybe G_theory -> IO (Maybe G_theory)
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Maybe G_theory
globalTheory (DGNodeLab -> Maybe G_theory) -> DGNodeLab -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd (LNode DGNodeLab -> DGNodeLab) -> LNode DGNodeLab -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ FNode -> LNode DGNodeLab
node FNode
fn
           case Maybe G_theory
res of
             Just gt :: G_theory
gt -> IO () -> IO ()
forall a. IO a -> IO a
postGUISync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ ListStore FNode -> Int -> FNode -> IO ()
forall a. ListStore a -> Int -> a -> IO ()
listStoreSetValue ListStore FNode
listNodes Int
row
               FNode
fn { results :: G_theory
results = G_theory -> G_theory -> G_theory
propagateProofs (FNode -> G_theory
results FNode
fn) G_theory
gt }
             Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           Double -> IO Double
forall (m :: * -> *) a. Monad m => a -> m a
return (Double -> IO Double) -> Double -> IO Double
forall a b. (a -> b) -> a -> b
$ Double
count Double -> Double -> Double
forall a. Num a => a -> a -> a
+ 1) 0 [(Int, FNode)]
nodes

sortNodes :: TreeView -> ListStore FNode -> IO ()
sortNodes :: TreeView -> ListStore FNode -> IO ()
sortNodes trvNodes :: TreeView
trvNodes listNodes :: ListStore FNode
listNodes = do
  [(Int, FNode)]
sel <- TreeView -> ListStore FNode -> IO [(Int, FNode)]
forall a. TreeView -> ListStore a -> IO [(Int, a)]
getSelectedMultiple TreeView
trvNodes ListStore FNode
listNodes
  [FNode]
nodes <- ListStore FNode -> IO [FNode]
forall a. ListStore a -> IO [a]
listStoreToList ListStore FNode
listNodes
  let sn :: [FNode]
sn = [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort [FNode]
nodes
  ListStore FNode -> [FNode] -> IO ()
forall a. ListStore a -> [a] -> IO ()
updateListData ListStore FNode
listNodes [FNode]
sn
  TreeSelection
selector <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvNodes
  ((Int, FNode) -> IO ()) -> [(Int, FNode)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (_, FNode { name :: FNode -> String
name = String
n }) -> TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath TreeSelection
selector
      [Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error "Node not found!") (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ (FNode -> Bool) -> [FNode] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ((String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (FNode -> String) -> FNode -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> String
name) [FNode]
sn]
    ) [(Int, FNode)]
sel

-- | Called when node selection is changed. Updates finder list
updateNodes :: TreeView -> ListStore FNode -> (G_sublogics -> IO ())
            -> IO () -> IO () -> IO ()
updateNodes :: TreeView
-> ListStore FNode
-> (G_sublogics -> IO ())
-> IO ()
-> IO ()
-> IO ()
updateNodes view :: TreeView
view listNodes :: ListStore FNode
listNodes update :: G_sublogics -> IO ()
update lock :: IO ()
lock unlock :: IO ()
unlock = do
  [(Int, FNode)]
nodes <- TreeView -> ListStore FNode -> IO [(Int, FNode)]
forall a. TreeView -> ListStore a -> IO [(Int, a)]
getSelectedMultiple TreeView
view ListStore FNode
listNodes
  if [(Int, FNode)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, FNode)]
nodes then IO ()
lock
    else let sls :: [G_sublogics]
sls = ((Int, FNode) -> G_sublogics) -> [(Int, FNode)] -> [G_sublogics]
forall a b. (a -> b) -> [a] -> [b]
map (FNode -> G_sublogics
sublogic (FNode -> G_sublogics)
-> ((Int, FNode) -> FNode) -> (Int, FNode) -> G_sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, FNode) -> FNode
forall a b. (a, b) -> b
snd) [(Int, FNode)]
nodes in
      IO () -> (G_sublogics -> IO ()) -> Maybe G_sublogics -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
lock (\ sl :: G_sublogics
sl -> IO ()
unlock IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> G_sublogics -> IO ()
update G_sublogics
sl)
            (Maybe G_sublogics -> IO ()) -> Maybe G_sublogics -> IO ()
forall a b. (a -> b) -> a -> b
$ (Maybe G_sublogics -> G_sublogics -> Maybe G_sublogics)
-> Maybe G_sublogics -> [G_sublogics] -> Maybe G_sublogics
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ ma :: Maybe G_sublogics
ma b :: G_sublogics
b -> case Maybe G_sublogics
ma of
                      Just a :: G_sublogics
a -> G_sublogics -> G_sublogics -> Maybe G_sublogics
joinSublogics G_sublogics
b G_sublogics
a
                      Nothing -> Maybe G_sublogics
forall a. Maybe a
Nothing) (G_sublogics -> Maybe G_sublogics
forall a. a -> Maybe a
Just (G_sublogics -> Maybe G_sublogics)
-> G_sublogics -> Maybe G_sublogics
forall a b. (a -> b) -> a -> b
$ [G_sublogics] -> G_sublogics
forall a. [a] -> a
head [G_sublogics]
sls) ([G_sublogics] -> Maybe G_sublogics)
-> [G_sublogics] -> Maybe G_sublogics
forall a b. (a -> b) -> a -> b
$ [G_sublogics] -> [G_sublogics]
forall a. [a] -> [a]
tail [G_sublogics]
sls

-- | Update the list of finder
updateFinder :: TreeView -> ListStore Finder -> G_sublogics -> IO ()
updateFinder :: TreeView -> ListStore Finder -> G_sublogics -> IO ()
updateFinder view :: TreeView
view list :: ListStore Finder
list sl :: G_sublogics
sl = do
  [Finder]
old <- ListStore Finder -> IO [Finder]
forall a. ListStore a -> IO [a]
listStoreToList ListStore Finder
list
  [(G_prover, AnyComorphism)]
ps <- ProverKind
-> G_sublogics -> LogicGraph -> IO [(G_prover, AnyComorphism)]
getUsableProvers ProverKind
ProveCMDLautomatic G_sublogics
sl LogicGraph
logicGraph
  let new :: [Finder]
new = Map String Finder -> [Finder]
forall k a. Map k a -> [a]
Map.elems (Map String Finder -> [Finder]) -> Map String Finder -> [Finder]
forall a b. (a -> b) -> a -> b
$ ((G_prover, AnyComorphism)
 -> Map String Finder -> Map String Finder)
-> Map String Finder
-> [(G_prover, AnyComorphism)]
-> Map String Finder
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (pr :: G_prover
pr, c :: AnyComorphism
c) m :: Map String Finder
m ->
              let n :: String
n = G_prover -> String
getProverName G_prover
pr
                  f :: Finder
f = Finder -> String -> Map String Finder -> Finder
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> G_prover -> [AnyComorphism] -> Int -> Finder
Finder String
n G_prover
pr [] 0) String
n Map String Finder
m
              in String -> Finder -> Map String Finder -> Map String Finder
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
n (Finder
f { comorphism :: [AnyComorphism]
comorphism = AnyComorphism
c AnyComorphism -> [AnyComorphism] -> [AnyComorphism]
forall a. a -> [a] -> [a]
: Finder -> [AnyComorphism]
comorphism Finder
f}) Map String Finder
m) Map String Finder
forall k a. Map k a
Map.empty
              [(G_prover, AnyComorphism)]
ps
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Finder]
old [Finder] -> [Finder] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Finder]
new) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    -- update list and try to select previous finder
    Maybe (Int, Finder)
selected' <- TreeView -> ListStore Finder -> IO (Maybe (Int, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
view ListStore Finder
list
    TreeSelection
sel <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
view
    ListStore Finder -> IO ()
forall a. ListStore a -> IO ()
listStoreClear ListStore Finder
list
    (Finder -> IO Int) -> [Finder] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ListStore Finder -> Finder -> IO Int
forall a. ListStore a -> a -> IO Int
listStoreAppend ListStore Finder
list) ([Finder] -> IO ()) -> [Finder] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Finder] -> [Finder] -> [Finder]
mergeFinder [Finder]
old [Finder]
new
    IO () -> ((Int, Finder) -> IO ()) -> Maybe (Int, Finder) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TreeView -> IO ()
selectFirst TreeView
view)
      (\ (_, f :: Finder
f) -> let i :: Maybe Int
i = (Finder -> Bool) -> [Finder] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ((Finder -> String
fName Finder
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (Finder -> String) -> Finder -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finder -> String
fName) [Finder]
new in
        IO () -> (Int -> IO ()) -> Maybe Int -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TreeView -> IO ()
selectFirst TreeView
view) (TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath TreeSelection
sel (TreePath -> IO ()) -> (Int -> TreePath) -> Int -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> TreePath -> TreePath
forall a. a -> [a] -> [a]
: [])) Maybe Int
i
      ) Maybe (Int, Finder)
selected'

-- | Try to select previous selected comorphism if possible
mergeFinder :: [Finder] -> [Finder] -> [Finder]
mergeFinder :: [Finder] -> [Finder] -> [Finder]
mergeFinder old :: [Finder]
old new :: [Finder]
new = let m' :: Map String Finder
m' = [(String, Finder)] -> Map String Finder
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, Finder)] -> Map String Finder)
-> [(String, Finder)] -> Map String Finder
forall a b. (a -> b) -> a -> b
$ (Finder -> (String, Finder)) -> [Finder] -> [(String, Finder)]
forall a b. (a -> b) -> [a] -> [b]
map (\ f :: Finder
f -> (Finder -> String
fName Finder
f, Finder
f)) [Finder]
new in
  Map String Finder -> [Finder]
forall k a. Map k a -> [a]
Map.elems (Map String Finder -> [Finder]) -> Map String Finder -> [Finder]
forall a b. (a -> b) -> a -> b
$ (Map String Finder -> Finder -> Map String Finder)
-> Map String Finder -> [Finder] -> Map String Finder
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map String Finder
m (Finder { fName :: Finder -> String
fName = String
n, comorphism :: Finder -> [AnyComorphism]
comorphism = [AnyComorphism]
cc, selected :: Finder -> Int
selected = Int
i}) ->
      case String -> Map String Finder -> Maybe Finder
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
n Map String Finder
m of
        Nothing -> Map String Finder
m
        Just f :: Finder
f@(Finder { comorphism :: Finder -> [AnyComorphism]
comorphism = [AnyComorphism]
cc' }) -> let c :: AnyComorphism
c = [AnyComorphism]
cc [AnyComorphism] -> Int -> AnyComorphism
forall a. [a] -> Int -> a
!! Int
i in
          String -> Finder -> Map String Finder -> Map String Finder
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
n (Finder
f { selected :: Int
selected = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ AnyComorphism -> [AnyComorphism] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex AnyComorphism
c [AnyComorphism]
cc' }) Map String Finder
m
    ) Map String Finder
m' [Finder]
old

updateComorphism :: TreeView -> ListStore Finder -> ComboBox
                 -> ConnectId ComboBox -> IO ()
updateComorphism :: TreeView
-> ListStore Finder -> ComboBox -> ConnectId ComboBox -> IO ()
updateComorphism view :: TreeView
view list :: ListStore Finder
list cbComorphism :: ComboBox
cbComorphism sh :: ConnectId ComboBox
sh = do
  ConnectId ComboBox -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId ComboBox
sh
  ListStore ComboBoxText
model <- ComboBox -> IO (ListStore ComboBoxText)
forall self.
ComboBoxClass self =>
self -> IO (ListStore ComboBoxText)
comboBoxGetModelText ComboBox
cbComorphism
  ListStore ComboBoxText -> IO ()
forall a. ListStore a -> IO ()
listStoreClear ListStore ComboBoxText
model
  Maybe (Int, Finder)
mfinder <- TreeView -> ListStore Finder -> IO (Maybe (Int, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
view ListStore Finder
list
  case Maybe (Int, Finder)
mfinder of
    Just (_, f :: Finder
f) -> do
      (ComboBoxText -> IO Int) -> [ComboBoxText] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ComboBox -> ComboBoxText -> IO Int
forall self. ComboBoxClass self => self -> ComboBoxText -> IO Int
comboBoxAppendText ComboBox
cbComorphism) ([ComboBoxText] -> IO ()) -> [ComboBoxText] -> IO ()
forall a b. (a -> b) -> a -> b
$ Finder -> [ComboBoxText]
expand Finder
f
      ComboBox -> Int -> IO ()
forall self. ComboBoxClass self => self -> Int -> IO ()
comboBoxSetActive ComboBox
cbComorphism (Int -> IO ()) -> Int -> IO ()
forall a b. (a -> b) -> a -> b
$ Finder -> Int
selected Finder
f
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  ConnectId ComboBox -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId ComboBox
sh

expand :: Finder -> [ComboBoxText]
expand :: Finder -> [ComboBoxText]
expand = [AnyComorphism] -> [ComboBoxText]
forall a. Show a => [a] -> [ComboBoxText]
toComboBoxText ([AnyComorphism] -> [ComboBoxText])
-> (Finder -> [AnyComorphism]) -> Finder -> [ComboBoxText]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finder -> [AnyComorphism]
comorphism

setSelectedComorphism :: TreeView -> ListStore Finder -> ComboBox -> IO ()
setSelectedComorphism :: TreeView -> ListStore Finder -> ComboBox -> IO ()
setSelectedComorphism view :: TreeView
view list :: ListStore Finder
list cbComorphism :: ComboBox
cbComorphism = do
  Maybe (Int, Finder)
mfinder <- TreeView -> ListStore Finder -> IO (Maybe (Int, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
view ListStore Finder
list
  case Maybe (Int, Finder)
mfinder of
    Just (i :: Int
i, f :: Finder
f) -> do
      Int
sel <- ComboBox -> IO Int
forall self. ComboBoxClass self => self -> IO Int
comboBoxGetActive ComboBox
cbComorphism
      ListStore Finder -> Int -> Finder -> IO ()
forall a. ListStore a -> Int -> a -> IO ()
listStoreSetValue ListStore Finder
list Int
i Finder
f { selected :: Int
selected = Int
sel }
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Displays the model view window
showModelViewAux :: MVar (IO ()) -> String -> ListStore FNode -> [FNode]
                 -> IO ()
showModelViewAux :: MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelViewAux lock :: MVar (IO ())
lock title :: String
title list :: ListStore FNode
list other :: [FNode]
other = do
  Builder
builder <- (String, String) -> IO Builder
getGTKBuilder (String, String)
ConsistencyChecker.get
  -- get objects
  Window
window <- Builder -> (GObject -> Window) -> String -> IO Window
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Window
forall obj. GObjectClass obj => obj -> Window
castToWindow "ModelView"
  Button
btnClose <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnResClose"
  Frame
frNodes <- Builder -> (GObject -> Frame) -> String -> IO Frame
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Frame
forall obj. GObjectClass obj => obj -> Frame
castToFrame "frResNodes"
  TreeView
trvNodes <- Builder -> (GObject -> TreeView) -> String -> IO TreeView
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> TreeView
forall obj. GObjectClass obj => obj -> TreeView
castToTreeView "trvResNodes"
  TextView
tvModel <- Builder -> (GObject -> TextView) -> String -> IO TextView
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> TextView
forall obj. GObjectClass obj => obj -> TextView
castToTextView "tvResModel"

  Window -> String -> IO ()
forall self string.
(WindowClass self, GlibString string) =>
self -> string -> IO ()
windowSetTitle Window
window String
title

  -- setup text view
  TextBuffer
buffer <- TextView -> IO TextBuffer
forall self. TextViewClass self => self -> IO TextBuffer
textViewGetBuffer TextView
tvModel
  TextBuffer -> String -> IO ()
forall self string.
(TextBufferClass self, GlibString string) =>
self -> string -> IO ()
textBufferInsertAtCursor TextBuffer
buffer ""

  TextTagTable
tagTable <- TextBuffer -> IO TextTagTable
forall self. TextBufferClass self => self -> IO TextTagTable
textBufferGetTagTable TextBuffer
buffer
  TextTag
font <- Maybe ComboBoxText -> IO TextTag
textTagNew Maybe ComboBoxText
forall a. Maybe a
Nothing
  TextTag -> [AttrOp TextTag] -> IO ()
forall o. o -> [AttrOp o] -> IO ()
set TextTag
font [ Attr TextTag String
forall self string.
(TextTagClass self, GlibString string) =>
Attr self string
textTagFont Attr TextTag String -> String -> AttrOp TextTag
forall o a b. ReadWriteAttr o a b -> b -> AttrOp o
:= "FreeMono" ]
  TextTagTable -> TextTag -> IO ()
forall self tag.
(TextTagTableClass self, TextTagClass tag) =>
self -> tag -> IO ()
textTagTableAdd TextTagTable
tagTable TextTag
font
  TextIter
start <- TextBuffer -> IO TextIter
forall self. TextBufferClass self => self -> IO TextIter
textBufferGetStartIter TextBuffer
buffer
  TextIter
end <- TextBuffer -> IO TextIter
forall self. TextBufferClass self => self -> IO TextIter
textBufferGetEndIter TextBuffer
buffer
  TextBuffer -> TextTag -> TextIter -> TextIter -> IO ()
forall self tag.
(TextBufferClass self, TextTagClass tag) =>
self -> tag -> TextIter -> TextIter -> IO ()
textBufferApplyTag TextBuffer
buffer TextTag
font TextIter
start TextIter
end

  -- setup list view
  let filterNodes :: a -> a
filterNodes = a -> a
forall a. a -> a
id

  [FNode]
nodes <- ListStore FNode -> IO [FNode]
forall a. ListStore a -> IO [a]
listStoreToList ListStore FNode
list
  ListStore FNode
listNodes <- TreeView -> (FNode -> String) -> [FNode] -> IO (ListStore FNode)
forall a. TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData TreeView
trvNodes FNode -> String
forall a. Show a => a -> String
show ([FNode] -> IO (ListStore FNode))
-> [FNode] -> IO (ListStore FNode)
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort ([FNode] -> [FNode]) -> [FNode] -> [FNode]
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
forall a. a -> a
filterNodes ([FNode] -> [FNode]) -> [FNode] -> [FNode]
forall a b. (a -> b) -> a -> b
$ [FNode]
other [FNode] -> [FNode] -> [FNode]
forall a. [a] -> [a] -> [a]
++ [FNode]
nodes

  TreeView -> IO () -> IO (ConnectId TreeSelection)
setListSelectorSingle TreeView
trvNodes (IO () -> IO (ConnectId TreeSelection))
-> IO () -> IO (ConnectId TreeSelection)
forall a b. (a -> b) -> a -> b
$ do
    Maybe (Int, FNode)
mn <- TreeView -> ListStore FNode -> IO (Maybe (Int, FNode))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvNodes ListStore FNode
listNodes
    case Maybe (Int, FNode)
mn of
      Nothing -> TextBuffer -> String -> IO ()
forall self string.
(TextBufferClass self, GlibString string) =>
self -> string -> IO ()
textBufferSetText TextBuffer
buffer ""
      Just (_, n :: FNode
n) -> TextBuffer -> String -> IO ()
forall self string.
(TextBufferClass self, GlibString string) =>
self -> string -> IO ()
textBufferSetText TextBuffer
buffer (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ FNode -> String
showStatus FNode
n

  -- setup actions
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnClose (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetDestroy Window
window
  Window -> IO () -> IO (ConnectId Window)
forall w. WidgetClass w => w -> IO () -> IO (ConnectId w)
onDestroy Window
window (IO () -> IO (ConnectId Window)) -> IO () -> IO (ConnectId Window)
forall a b. (a -> b) -> a -> b
$ MVar (IO ()) -> IO (IO ())
forall a. MVar a -> IO a
takeMVar MVar (IO ())
lock IO (IO ()) -> (IO () -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO () -> IO () -> IO ()
forall a b. a -> b -> a
const (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())

  MVar (IO ()) -> IO () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar (IO ())
lock (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Maybe (Int, FNode)
sel' <- TreeView -> ListStore FNode -> IO (Maybe (Int, FNode))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvNodes ListStore FNode
listNodes
    TreeSelection
sel <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvNodes
    [FNode]
nodes'' <- ListStore FNode -> IO [FNode]
forall a. ListStore a -> IO [a]
listStoreToList ListStore FNode
list
    let nodes' :: [FNode]
nodes' = [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort ([FNode] -> [FNode]) -> [FNode] -> [FNode]
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
forall a. a -> a
filterNodes [FNode]
nodes''
    ListStore FNode -> [FNode] -> IO ()
forall a. ListStore a -> [a] -> IO ()
updateListData ListStore FNode
listNodes ([FNode] -> IO ()) -> [FNode] -> IO ()
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort ([FNode]
other [FNode] -> [FNode] -> [FNode]
forall a. [a] -> [a] -> [a]
++ [FNode]
nodes')
    IO () -> (Int -> IO ()) -> Maybe Int -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TreeView -> IO ()
selectFirst TreeView
trvNodes) (TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath TreeSelection
sel (TreePath -> IO ()) -> (Int -> TreePath) -> Int -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> TreePath -> TreePath
forall a. a -> [a] -> [a]
: []))
      (Maybe Int -> IO ()) -> Maybe Int -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe Int
-> ((Int, FNode) -> Maybe Int) -> Maybe (Int, FNode) -> Maybe Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe Int
forall a. Maybe a
Nothing (\ (_, n :: FNode
n) -> (FNode -> Bool) -> [FNode] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ((FNode -> String
name FNode
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (FNode -> String) -> FNode -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> String
name) [FNode]
nodes') Maybe (Int, FNode)
sel'

  TreeView -> IO ()
selectFirst TreeView
trvNodes

  Window -> Int -> Int -> IO ()
forall self. WidgetClass self => self -> Int -> Int -> IO ()
widgetSetSizeRequest Window
window 800 600
  Frame -> Int -> Int -> IO ()
forall self. WidgetClass self => self -> Int -> Int -> IO ()
widgetSetSizeRequest Frame
frNodes 250 (-1)

  Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetShow Window
window

-- | Displays the model view window
showModelView :: MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelView :: MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelView lock :: MVar (IO ())
lock title :: String
title list :: ListStore FNode
list other :: [FNode]
other = do
  Bool
isNotOpen <- MVar (IO ()) -> IO Bool
forall a. MVar a -> IO Bool
isEmptyMVar MVar (IO ())
lock
  if Bool
isNotOpen then MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelViewAux MVar (IO ())
lock String
title ListStore FNode
list [FNode]
other
    else IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (MVar (IO ()) -> IO (IO ())
forall a. MVar a -> IO a
readMVar MVar (IO ())
lock)