{-# LANGUAGE CPP #-}
{- |
Module      :  ./GUI/GraphMenu.hs
Description :  Menu creation functions for the Graphdisplay
Copyright   :  (c) Thiemo Wiedemeyer, Uni Bremen 2002-2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  raider@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic)

Menu creation
-}

module GUI.GraphMenu (createGraph) where

import qualified GUI.GraphAbstraction as GA
import GUI.GraphTypes
import GUI.GraphLogic
import GUI.Utils
import GUI.UDGUtils
#ifdef GTKGLADE
import GUI.GtkDisprove
import GUI.GtkConsistencyChecker
import GUI.GtkAutomaticProofs
import GUI.GtkAddSentence
#endif

import Data.IORef
import qualified Data.Map as Map

import System.Directory (getCurrentDirectory)
import System.FilePath

import Static.DevGraph
import Static.DgUtils
import Static.PrintDevGraph ()

import Static.ComputeTheory (computeTheory)
import Static.ConsInclusions
import qualified Proofs.VSE as VSE

import Common.DocUtils
import qualified Control.Monad.Fail as Fail

import Driver.Options (HetcatsOpts, rmSuffix, prfSuffix)
import Driver.ReadFn (libNameToFile)

import Interfaces.DataTypes
import Interfaces.Command
import Interfaces.CmdAction

import GUI.ShowRefTree

-- | Adds to the DGNodeType list style options for each type
nodeTypes :: HetcatsOpts
          -> [( DGNodeType -- Nodetype
              , Shape GA.NodeValue -- Shape
              , String -- Color
              )]
nodeTypes :: HetcatsOpts -> [(DGNodeType, Shape NodeValue, String)]
nodeTypes opts :: HetcatsOpts
opts = (DGNodeType -> (DGNodeType, Shape NodeValue, String))
-> [DGNodeType] -> [(DGNodeType, Shape NodeValue, String)]
forall a b. (a -> b) -> [a] -> [b]
map
  ((\ (n :: DGNodeType
n, s :: Shape NodeValue
s) -> if DGNodeType -> Bool
isProvenNode DGNodeType
n then -- Add color
      if DGNodeType -> Bool
isProvenCons DGNodeType
n
      then (DGNodeType
n, Shape NodeValue
s, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Green Bool
True Bool
False)
      else (DGNodeType
n, Shape NodeValue
s, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Yellow Bool
False Bool
True)
     else (DGNodeType
n, Shape NodeValue
s, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Coral Bool
False (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ DGNodeType -> Bool
isProvenCons DGNodeType
n))
  ((DGNodeType, Shape NodeValue)
 -> (DGNodeType, Shape NodeValue, String))
-> (DGNodeType -> (DGNodeType, Shape NodeValue))
-> DGNodeType
-> (DGNodeType, Shape NodeValue, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ n :: DGNodeType
n -> (DGNodeType
n, if DGNodeType -> Bool
isRefType DGNodeType
n then Shape NodeValue
forall value. Shape value
Box else Shape NodeValue
forall value. Shape value
Ellipse) -- Add shape
  ) [DGNodeType]
listDGNodeTypes

-- | A Map of all nodetypes and their properties.
mapNodeTypes :: HetcatsOpts -> Map.Map DGNodeType (Shape GA.NodeValue, String)
mapNodeTypes :: HetcatsOpts -> Map DGNodeType (Shape NodeValue, String)
mapNodeTypes = [(DGNodeType, (Shape NodeValue, String))]
-> Map DGNodeType (Shape NodeValue, String)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(DGNodeType, (Shape NodeValue, String))]
 -> Map DGNodeType (Shape NodeValue, String))
-> (HetcatsOpts -> [(DGNodeType, (Shape NodeValue, String))])
-> HetcatsOpts
-> Map DGNodeType (Shape NodeValue, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((DGNodeType, Shape NodeValue, String)
 -> (DGNodeType, (Shape NodeValue, String)))
-> [(DGNodeType, Shape NodeValue, String)]
-> [(DGNodeType, (Shape NodeValue, String))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: DGNodeType
n, s :: Shape NodeValue
s, c :: String
c) -> (DGNodeType
n, (Shape NodeValue
s, String
c))) ([(DGNodeType, Shape NodeValue, String)]
 -> [(DGNodeType, (Shape NodeValue, String))])
-> (HetcatsOpts -> [(DGNodeType, Shape NodeValue, String)])
-> HetcatsOpts
-> [(DGNodeType, (Shape NodeValue, String))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetcatsOpts -> [(DGNodeType, Shape NodeValue, String)]
nodeTypes

-- | Adds to the DGEdgeType list style options for each type
edgeTypes :: HetcatsOpts
          -> [( DGEdgeType -- Edgetype
              , EdgePattern GA.EdgeValue -- Lineformat
              , String -- Color
              , Bool -- has conservativity
              )]
edgeTypes :: HetcatsOpts -> [(DGEdgeType, EdgePattern EdgeValue, String, Bool)]
edgeTypes opts :: HetcatsOpts
opts = (DGEdgeType -> (DGEdgeType, EdgePattern EdgeValue, String, Bool))
-> [DGEdgeType]
-> [(DGEdgeType, EdgePattern EdgeValue, String, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map
  ( (\ (e :: DGEdgeType
e, l :: EdgePattern EdgeValue
l, c :: String
c) -> case DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc DGEdgeType
e of -- Add menu options
      ThmType { thmEdgeType :: DGEdgeTypeModInc -> ThmTypes
thmEdgeType = GlobalOrLocalThm _ _ } -> (DGEdgeType
e, EdgePattern EdgeValue
l, String
c, Bool
True)
      GlobalDef -> (DGEdgeType
e, EdgePattern EdgeValue
l, String
c, Bool
True)
      HetDef -> (DGEdgeType
e, EdgePattern EdgeValue
l, String
c, Bool
True)
      LocalDef -> (DGEdgeType
e, EdgePattern EdgeValue
l, String
c, Bool
True)
      _ -> (DGEdgeType
e, EdgePattern EdgeValue
l, String
c, Bool
False)
    )
  ((DGEdgeType, EdgePattern EdgeValue, String)
 -> (DGEdgeType, EdgePattern EdgeValue, String, Bool))
-> (DGEdgeType -> (DGEdgeType, EdgePattern EdgeValue, String))
-> DGEdgeType
-> (DGEdgeType, EdgePattern EdgeValue, String, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ (e :: DGEdgeType
e, l :: EdgePattern EdgeValue
l) -> case DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc DGEdgeType
e of -- Add colors
      HidingDef -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Blue Bool
True (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
      FreeOrCofreeDef _ -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Blue Bool
False (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
      ThmType { thmEdgeType :: DGEdgeTypeModInc -> ThmTypes
thmEdgeType = ThmTypes
thmType
              , isProvenEdge :: DGEdgeTypeModInc -> Bool
isProvenEdge = Bool
False } -> case ThmTypes
thmType of
        GlobalOrLocalThm { thmScope :: ThmTypes -> Scope
thmScope = Scope
Local, isHomThm :: ThmTypes -> Bool
isHomThm = Bool
False }
                      -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Coral Bool
True (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
        HidingThm -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Yellow Bool
False (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
        _ -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Coral Bool
False (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
      ThmType { thmEdgeType :: DGEdgeTypeModInc -> ThmTypes
thmEdgeType = ThmTypes
thmType
              , isConservativ :: DGEdgeTypeModInc -> Bool
isConservativ = Bool
False } -> case ThmTypes
thmType of
        GlobalOrLocalThm { thmScope :: ThmTypes -> Scope
thmScope = Scope
Local, isHomThm :: ThmTypes -> Bool
isHomThm = Bool
False }
                      -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Yellow Bool
True (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
        _ -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Yellow Bool
False (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
      ThmType { thmEdgeType :: DGEdgeTypeModInc -> ThmTypes
thmEdgeType = ThmTypes
thmType
              , isPending :: DGEdgeTypeModInc -> Bool
isPending = Bool
True } -> case ThmTypes
thmType of
        GlobalOrLocalThm { thmScope :: ThmTypes -> Scope
thmScope = Scope
Local, isHomThm :: ThmTypes -> Bool
isHomThm = Bool
False }
                      -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Yellow Bool
True (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
        _ -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Yellow Bool
False (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
      ThmType { thmEdgeType :: DGEdgeTypeModInc -> ThmTypes
thmEdgeType = ThmTypes
thmType } -> case ThmTypes
thmType of
        GlobalOrLocalThm { thmScope :: ThmTypes -> Scope
thmScope = Scope
Local, isHomThm :: ThmTypes -> Bool
isHomThm = Bool
False }
                      -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Green Bool
True (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
        HidingThm -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Green Bool
True (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
        _ -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Green Bool
False (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
      _ -> (DGEdgeType
e, EdgePattern EdgeValue
l, HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor HetcatsOpts
opts Colors
Black Bool
False (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DGEdgeType -> Bool
isInc DGEdgeType
e)
    )
  ((DGEdgeType, EdgePattern EdgeValue)
 -> (DGEdgeType, EdgePattern EdgeValue, String))
-> (DGEdgeType -> (DGEdgeType, EdgePattern EdgeValue))
-> DGEdgeType
-> (DGEdgeType, EdgePattern EdgeValue, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ e :: DGEdgeType
e -> case DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc DGEdgeType
e of -- Add lineformat
      ThmType { thmEdgeType :: DGEdgeTypeModInc -> ThmTypes
thmEdgeType = GlobalOrLocalThm { thmScope :: ThmTypes -> Scope
thmScope = Scope
Local
                                               , isHomThm :: ThmTypes -> Bool
isHomThm = Bool
True } }
                   -> (DGEdgeType
e, EdgePattern EdgeValue
forall value. EdgePattern value
Dashed)
      ThmType { thmEdgeType :: DGEdgeTypeModInc -> ThmTypes
thmEdgeType = GlobalOrLocalThm { isHomThm :: ThmTypes -> Bool
isHomThm = Bool
False } }
                   -> (DGEdgeType
e, EdgePattern EdgeValue
forall value. EdgePattern value
Double)
      LocalDef -> (DGEdgeType
e, EdgePattern EdgeValue
forall value. EdgePattern value
Dashed)
      HetDef -> (DGEdgeType
e, EdgePattern EdgeValue
forall value. EdgePattern value
Double)
      _ -> (DGEdgeType
e, EdgePattern EdgeValue
forall value. EdgePattern value
Solid)
    )
  ) [DGEdgeType]
listDGEdgeTypes

-- | A Map of all edgetypes and their properties.
mapEdgeTypes
  :: HetcatsOpts -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
mapEdgeTypes :: HetcatsOpts -> Map DGEdgeType (EdgePattern EdgeValue, String)
mapEdgeTypes =
  [(DGEdgeType, (EdgePattern EdgeValue, String))]
-> Map DGEdgeType (EdgePattern EdgeValue, String)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(DGEdgeType, (EdgePattern EdgeValue, String))]
 -> Map DGEdgeType (EdgePattern EdgeValue, String))
-> (HetcatsOpts -> [(DGEdgeType, (EdgePattern EdgeValue, String))])
-> HetcatsOpts
-> Map DGEdgeType (EdgePattern EdgeValue, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((DGEdgeType, EdgePattern EdgeValue, String, Bool)
 -> (DGEdgeType, (EdgePattern EdgeValue, String)))
-> [(DGEdgeType, EdgePattern EdgeValue, String, Bool)]
-> [(DGEdgeType, (EdgePattern EdgeValue, String))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (e :: DGEdgeType
e, l :: EdgePattern EdgeValue
l, c :: String
c, _) -> (DGEdgeType
e, (EdgePattern EdgeValue
l, String
c))) ([(DGEdgeType, EdgePattern EdgeValue, String, Bool)]
 -> [(DGEdgeType, (EdgePattern EdgeValue, String))])
-> (HetcatsOpts
    -> [(DGEdgeType, EdgePattern EdgeValue, String, Bool)])
-> HetcatsOpts
-> [(DGEdgeType, (EdgePattern EdgeValue, String))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetcatsOpts -> [(DGEdgeType, EdgePattern EdgeValue, String, Bool)]
edgeTypes

-- | Creates the graph. Runs makegraph
createGraph :: GInfo -> String -> ConvFunc -> LibFunc -> IO ()
createGraph :: GInfo -> String -> ConvFunc -> LibFunc -> IO ()
createGraph gi :: GInfo
gi title :: String
title convGraph :: ConvFunc
convGraph showLib :: LibFunc
showLib = do
  IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gi
  case IntState -> Maybe IntIState
i_state IntState
ost of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just _ -> do
      let ln :: LibName
ln = GInfo -> LibName
libName GInfo
gi
          opts :: IORef Flags
opts = GInfo -> IORef Flags
options GInfo
gi
          file :: String
file = LibName -> String
libNameToFile LibName
ln String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
prfSuffix
      IORef [String]
deselectEdgeTypes <- [String] -> IO (IORef [String])
forall a. a -> IO (IORef a)
newIORef []
      [GlobalMenu]
globMenu <- GInfo -> LibFunc -> IORef [String] -> IO [GlobalMenu]
createGlobalMenu GInfo
gi LibFunc
showLib IORef [String]
deselectEdgeTypes
      GraphInfo
-> String
-> Maybe (IO ())
-> Maybe (IO ())
-> Maybe (IO ())
-> IO Bool
-> Maybe (IO ())
-> [GlobalMenu]
-> [(DGNodeType, DaVinciNodeTypeParms NodeValue)]
-> [(DGEdgeType, DaVinciArcTypeParms EdgeValue)]
-> String
-> IO ()
-> IO ()
GA.makeGraph (GInfo -> GraphInfo
graphInfo GInfo
gi)
                   String
title
                   (GInfo -> String -> ConvFunc -> LibFunc -> Maybe (IO ())
createOpen GInfo
gi String
file ConvFunc
convGraph LibFunc
showLib)
                   (GInfo -> String -> Maybe (IO ())
createSave GInfo
gi String
file)
                   (GInfo -> String -> Maybe (IO ())
createSaveAs GInfo
gi String
file)
                   (GInfo -> IO Bool
createClose GInfo
gi)
                   (IO () -> Maybe (IO ())
forall a. a -> Maybe a
Just (LibFunc
exitGInfo GInfo
gi))
                   [GlobalMenu]
globMenu
                   (GInfo
-> ConvFunc
-> LibFunc
-> [(DGNodeType, DaVinciNodeTypeParms NodeValue)]
createNodeTypes GInfo
gi ConvFunc
convGraph LibFunc
showLib)
                   (GInfo -> [(DGEdgeType, DaVinciArcTypeParms EdgeValue)]
createEdgeTypes GInfo
gi)
                   (HetcatsOpts -> Colors -> Bool -> Bool -> String
getColor (GInfo -> HetcatsOpts
hetcatsOpts GInfo
gi) Colors
Purple Bool
False Bool
False)
                   (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> IO () -> IO ()
runAndLock GInfo
gi (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                       Flags
flags <- IORef Flags -> IO Flags
forall a. IORef a -> IO a
readIORef IORef Flags
opts
                       IORef Flags -> Flags -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Flags
opts (Flags -> IO ()) -> Flags -> IO ()
forall a b. (a -> b) -> a -> b
$ Flags
flags { flagHideNodes :: Bool
flagHideNodes = Bool
False}
                       GInfo -> [DGChange] -> IO ()
updateGraph GInfo
gi []

-- | Returns the open-function
createOpen :: GInfo -> FilePath -> ConvFunc -> LibFunc -> Maybe (IO ())
createOpen :: GInfo -> String -> ConvFunc -> LibFunc -> Maybe (IO ())
createOpen gi :: GInfo
gi file :: String
file convGraph :: ConvFunc
convGraph showLib :: LibFunc
showLib = IO () -> Maybe (IO ())
forall a. a -> Maybe a
Just (
  do
    Maybe String
maybeFilePath <- String
-> [(String, [String])]
-> Maybe (String -> IO ())
-> IO (Maybe String)
fileOpenDialog String
file [ ("Proof", ["*.prf"])
                                         , ("All Files", ["*"])] Maybe (String -> IO ())
forall a. Maybe a
Nothing
    case Maybe String
maybeFilePath of
      Just fPath :: String
fPath -> do
        GInfo -> String -> ConvFunc -> LibFunc -> IO ()
openProofStatus GInfo
gi String
fPath ConvFunc
convGraph LibFunc
showLib
        () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Nothing -> String -> IO ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Could not open file."
  )

-- | Returns the save-function
createSave :: GInfo -> FilePath -> Maybe (IO ())
createSave :: GInfo -> String -> Maybe (IO ())
createSave gi :: GInfo
gi = IO () -> Maybe (IO ())
forall a. a -> Maybe a
Just (IO () -> Maybe (IO ()))
-> (String -> IO ()) -> String -> Maybe (IO ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo -> String -> IO ()
saveProofStatus GInfo
gi

-- | Returns the saveas-function
createSaveAs :: GInfo -> FilePath -> Maybe (IO ())
createSaveAs :: GInfo -> String -> Maybe (IO ())
createSaveAs gi :: GInfo
gi file :: String
file = IO () -> Maybe (IO ())
forall a. a -> Maybe a
Just (
  do
    Maybe String
maybeFilePath <- String
-> [(String, [String])]
-> Maybe (String -> IO ())
-> IO (Maybe String)
fileSaveDialog String
file [ ("Proof", ["*.prf"])
                                         , ("All Files", ["*"])] Maybe (String -> IO ())
forall a. Maybe a
Nothing
    case Maybe String
maybeFilePath of
      Just fPath :: String
fPath -> GInfo -> String -> IO ()
saveProofStatus GInfo
gi String
fPath
      Nothing -> String -> IO ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Could not save file."
  )

-- | Returns the close-function
createClose :: GInfo -> IO Bool
createClose :: GInfo -> IO Bool
createClose gi :: GInfo
gi = do
   let oGrRef :: IORef (Map LibName GInfo)
oGrRef = GInfo -> IORef (Map LibName GInfo)
openGraphs GInfo
gi
   GInfo -> (Int -> Int) -> IO ()
updateWindowCount GInfo
gi Int -> Int
forall a. Enum a => a -> a
pred
   Map LibName GInfo
oGraphs <- IORef (Map LibName GInfo) -> IO (Map LibName GInfo)
forall a. IORef a -> IO a
readIORef IORef (Map LibName GInfo)
oGrRef
   IORef (Map LibName GInfo) -> Map LibName GInfo -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Map LibName GInfo)
oGrRef (Map LibName GInfo -> IO ()) -> Map LibName GInfo -> IO ()
forall a b. (a -> b) -> a -> b
$ LibName -> Map LibName GInfo -> Map LibName GInfo
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (GInfo -> LibName
libName GInfo
gi) Map LibName GInfo
oGraphs
   Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

-- | Creates the global menu
createGlobalMenu :: GInfo -> LibFunc -> IORef [String]
                 -> IO [GlobalMenu]
createGlobalMenu :: GInfo -> LibFunc -> IORef [String] -> IO [GlobalMenu]
createGlobalMenu gi :: GInfo
gi showLib :: LibFunc
showLib _ = do
 IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gi
 case IntState -> Maybe IntIState
i_state IntState
ost of
  Nothing -> [GlobalMenu] -> IO [GlobalMenu]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  Just _ -> do
   let ln :: LibName
ln = GInfo -> LibName
libName GInfo
gi
       opts :: HetcatsOpts
opts = GInfo -> HetcatsOpts
hetcatsOpts GInfo
gi
       ral :: IO () -> IO ()
ral = GInfo -> IO () -> IO ()
runAndLock GInfo
gi
       performProofMenuAction :: Command -> (LibEnv -> IO (Result LibEnv)) -> IO ()
performProofMenuAction cmd :: Command
cmd =
           IO () -> IO ()
ral (IO () -> IO ())
-> ((LibEnv -> IO (Result LibEnv)) -> IO ())
-> (LibEnv -> IO (Result LibEnv))
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo -> Command -> (LibEnv -> IO (Result LibEnv)) -> IO ()
proofMenu GInfo
gi Command
cmd
       mkGlobProofButton :: GlobCmd
-> (LibEnv -> IO (Result LibEnv)) -> MenuPrim subMenuValue (IO ())
mkGlobProofButton cmd :: GlobCmd
cmd =
         String -> IO () -> MenuPrim subMenuValue (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button (GlobCmd -> String
menuTextGlobCmd GlobCmd
cmd) (IO () -> MenuPrim subMenuValue (IO ()))
-> ((LibEnv -> IO (Result LibEnv)) -> IO ())
-> (LibEnv -> IO (Result LibEnv))
-> MenuPrim subMenuValue (IO ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Command -> (LibEnv -> IO (Result LibEnv)) -> IO ()
performProofMenuAction (GlobCmd -> Command
GlobCmd GlobCmd
cmd)
   [GlobalMenu] -> IO [GlobalMenu]
forall (m :: * -> *) a. Monad m => a -> m a
return
    [MenuPrim (Maybe String) (IO ()) -> GlobalMenu
GlobalMenu (Maybe String
-> [MenuPrim (Maybe String) (IO ())]
-> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
Menu Maybe String
forall a. Maybe a
Nothing
     [ String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Undo" (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
ral (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> Bool -> IO ()
undo GInfo
gi Bool
True
     , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Redo" (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
ral (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> Bool -> IO ()
undo GInfo
gi Bool
False
     , Maybe String
-> [MenuPrim (Maybe String) (IO ())]
-> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
Menu (String -> Maybe String
forall a. a -> Maybe a
Just "Hide/Show names/nodes/edges")
        [ String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Hide/Show internal node names"
                 (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
ral (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ LibFunc
toggleHideNames GInfo
gi
        , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Hide/Show unnamed nodes without open proofs"
                 (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
ral (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ LibFunc
toggleHideNodes GInfo
gi
        , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Hide/Show newly added proven edges"
                 (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
ral (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ LibFunc
toggleHideEdges GInfo
gi
      ]
     , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Focus node" (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
ral (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ LibFunc
focusNode GInfo
gi
#ifdef GTKGLADE
     , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Consistency checker"
         (Command -> (LibEnv -> IO (Result LibEnv)) -> IO ()
performProofMenuAction (GlobCmd -> Command
GlobCmd GlobCmd
CheckConsistencyCurrent)
           ((LibEnv -> IO (Result LibEnv)) -> IO ())
-> (LibEnv -> IO (Result LibEnv)) -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe Int -> GInfo -> LibEnv -> IO (Result LibEnv)
showConsistencyChecker Maybe Int
forall a. Maybe a
Nothing GInfo
gi)
     , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Automatic proofs"
         (Command -> (LibEnv -> IO (Result LibEnv)) -> IO ()
performProofMenuAction (String -> Command
CommentCmd "generated by \"automatic proofs\"")
           ((LibEnv -> IO (Result LibEnv)) -> IO ())
-> (LibEnv -> IO (Result LibEnv)) -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> LibEnv -> IO (Result LibEnv)
showAutomaticProofs GInfo
gi)
#endif
     , Maybe String
-> [MenuPrim (Maybe String) (IO ())]
-> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
Menu (String -> Maybe String
forall a. a -> Maybe a
Just "Proofs") ([MenuPrim (Maybe String) (IO ())]
 -> MenuPrim (Maybe String) (IO ()))
-> [MenuPrim (Maybe String) (IO ())]
-> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ ((GlobCmd, LibName -> LibEnv -> LibEnv)
 -> MenuPrim (Maybe String) (IO ()))
-> [(GlobCmd, LibName -> LibEnv -> LibEnv)]
-> [MenuPrim (Maybe String) (IO ())]
forall a b. (a -> b) -> [a] -> [b]
map (\ (cmd :: GlobCmd
cmd, act :: LibName -> LibEnv -> LibEnv
act) ->
        GlobCmd
-> (LibEnv -> IO (Result LibEnv))
-> MenuPrim (Maybe String) (IO ())
forall subMenuValue.
GlobCmd
-> (LibEnv -> IO (Result LibEnv)) -> MenuPrim subMenuValue (IO ())
mkGlobProofButton GlobCmd
cmd ((LibEnv -> IO (Result LibEnv)) -> MenuPrim (Maybe String) (IO ()))
-> (LibEnv -> IO (Result LibEnv))
-> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ Result LibEnv -> IO (Result LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result LibEnv -> IO (Result LibEnv))
-> (LibEnv -> Result LibEnv) -> LibEnv -> IO (Result LibEnv)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv)
-> (LibEnv -> LibEnv) -> LibEnv -> Result LibEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> LibEnv -> LibEnv
act LibName
ln) [(GlobCmd, LibName -> LibEnv -> LibEnv)]
globLibAct
        [MenuPrim (Maybe String) (IO ())]
-> [MenuPrim (Maybe String) (IO ())]
-> [MenuPrim (Maybe String) (IO ())]
forall a. [a] -> [a] -> [a]
++ ((GlobCmd, LibName -> LibEnv -> Result LibEnv)
 -> MenuPrim (Maybe String) (IO ()))
-> [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
-> [MenuPrim (Maybe String) (IO ())]
forall a b. (a -> b) -> [a] -> [b]
map (\ (cmd :: GlobCmd
cmd, act :: LibName -> LibEnv -> Result LibEnv
act) -> GlobCmd
-> (LibEnv -> IO (Result LibEnv))
-> MenuPrim (Maybe String) (IO ())
forall subMenuValue.
GlobCmd
-> (LibEnv -> IO (Result LibEnv)) -> MenuPrim subMenuValue (IO ())
mkGlobProofButton GlobCmd
cmd ((LibEnv -> IO (Result LibEnv)) -> MenuPrim (Maybe String) (IO ()))
-> (LibEnv -> IO (Result LibEnv))
-> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ Result LibEnv -> IO (Result LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result LibEnv -> IO (Result LibEnv))
-> (LibEnv -> Result LibEnv) -> LibEnv -> IO (Result LibEnv)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> LibEnv -> Result LibEnv
act LibName
ln)
           [(GlobCmd, LibName -> LibEnv -> Result LibEnv)]
globLibResultAct
        [MenuPrim (Maybe String) (IO ())]
-> [MenuPrim (Maybe String) (IO ())]
-> [MenuPrim (Maybe String) (IO ())]
forall a. [a] -> [a] -> [a]
++ [ Maybe String
-> [MenuPrim (Maybe String) (IO ())]
-> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
Menu (String -> Maybe String
forall a. a -> Maybe a
Just "Flattening") ([MenuPrim (Maybe String) (IO ())]
 -> MenuPrim (Maybe String) (IO ()))
-> [MenuPrim (Maybe String) (IO ())]
-> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ ((GlobCmd, LibEnv -> Result LibEnv)
 -> MenuPrim (Maybe String) (IO ()))
-> [(GlobCmd, LibEnv -> Result LibEnv)]
-> [MenuPrim (Maybe String) (IO ())]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (cmd :: GlobCmd
cmd, act :: LibEnv -> Result LibEnv
act) ->
           GlobCmd
-> (LibEnv -> IO (Result LibEnv))
-> MenuPrim (Maybe String) (IO ())
forall subMenuValue.
GlobCmd
-> (LibEnv -> IO (Result LibEnv)) -> MenuPrim subMenuValue (IO ())
mkGlobProofButton GlobCmd
cmd ((LibEnv -> IO (Result LibEnv)) -> MenuPrim (Maybe String) (IO ()))
-> (LibEnv -> IO (Result LibEnv))
-> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ Result LibEnv -> IO (Result LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result LibEnv -> IO (Result LibEnv))
-> (LibEnv -> Result LibEnv) -> LibEnv -> IO (Result LibEnv)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibEnv -> Result LibEnv
act) [(GlobCmd, LibEnv -> Result LibEnv)]
globResultAct ]
     , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Dump Development Graph" (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ do
          IntState
ost2 <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gi
          case IntState -> Maybe IntIState
i_state IntState
ost2 of
            Nothing -> String -> IO ()
putStrLn "no lib"
            Just ist2 :: IntIState
ist2 -> Doc -> IO ()
forall a. Show a => a -> IO ()
print (Doc -> IO ()) -> (LibEnv -> Doc) -> LibEnv -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Doc
forall a. Pretty a => a -> Doc
pretty (DGraph -> Doc) -> (LibEnv -> DGraph) -> LibEnv -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> LibEnv -> DGraph
lookupDGraph (IntIState -> LibName
i_ln IntIState
ist2)
              (LibEnv -> IO ()) -> LibEnv -> IO ()
forall a b. (a -> b) -> a -> b
$ IntIState -> LibEnv
i_libEnv IntIState
ist2
     , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Dump Cons Inclusions" (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ do
          IntState
ost2 <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gi
          case IntState -> Maybe IntIState
i_state IntState
ost2 of
            Nothing -> String -> IO ()
putStrLn "no lib"
            Just ist2 :: IntIState
ist2 -> HetcatsOpts -> DGraph -> IO ()
dumpConsInclusions (GInfo -> HetcatsOpts
hetcatsOpts GInfo
gi)
                          (DGraph -> IO ()) -> DGraph -> IO ()
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph (IntIState -> LibName
i_ln IntIState
ist2) (LibEnv -> DGraph) -> LibEnv -> DGraph
forall a b. (a -> b) -> a -> b
$ IntIState -> LibEnv
i_libEnv IntIState
ist2
     , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Show Library Graph" (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
ral (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> LibFunc -> IO ()
showLibGraph GInfo
gi LibFunc
showLib
     , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Show RefinementTree" (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
ral (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> LibFunc -> IO ()
showLibGraph GInfo
gi LibFunc
showRefTree
     , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Save Graph for uDrawGraph" (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
ral
              (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo
-> Map DGNodeType (Shape NodeValue, String)
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> IO ()
forall value.
GInfo
-> Map DGNodeType (Shape value, String)
-> Map DGEdgeType (EdgePattern EdgeValue, String)
-> IO ()
saveUDGraph GInfo
gi (HetcatsOpts -> Map DGNodeType (Shape NodeValue, String)
mapNodeTypes HetcatsOpts
opts) (Map DGEdgeType (EdgePattern EdgeValue, String) -> IO ())
-> Map DGEdgeType (EdgePattern EdgeValue, String) -> IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Map DGEdgeType (EdgePattern EdgeValue, String)
mapEdgeTypes HetcatsOpts
opts
     , String -> IO () -> MenuPrim (Maybe String) (IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Save proof-script" (IO () -> MenuPrim (Maybe String) (IO ()))
-> IO () -> MenuPrim (Maybe String) (IO ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
ral
              (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GraphInfo -> IORef IntState -> IO ()
askSaveProofScript (GInfo -> GraphInfo
graphInfo GInfo
gi) (IORef IntState -> IO ()) -> IORef IntState -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gi
     ])
    ]

-- | A list of all Node Types
createNodeTypes :: GInfo -> ConvFunc -> LibFunc
                -> [(DGNodeType, DaVinciNodeTypeParms GA.NodeValue)]
createNodeTypes :: GInfo
-> ConvFunc
-> LibFunc
-> [(DGNodeType, DaVinciNodeTypeParms NodeValue)]
createNodeTypes gi :: GInfo
gi cGraph :: ConvFunc
cGraph showLib :: LibFunc
showLib = ((DGNodeType, Shape NodeValue, String)
 -> (DGNodeType, DaVinciNodeTypeParms NodeValue))
-> [(DGNodeType, Shape NodeValue, String)]
-> [(DGNodeType, DaVinciNodeTypeParms NodeValue)]
forall a b. (a -> b) -> [a] -> [b]
map
  (\ (n :: DGNodeType
n, s :: Shape NodeValue
s, c :: String
c) -> (DGNodeType
n, if DGNodeType -> Bool
isRefType DGNodeType
n
    then Shape NodeValue
-> String
-> GInfo
-> ConvFunc
-> LibFunc
-> Bool
-> DaVinciNodeTypeParms NodeValue
createMenuNodeRef Shape NodeValue
s String
c GInfo
gi ConvFunc
cGraph LibFunc
showLib (Bool -> DaVinciNodeTypeParms NodeValue)
-> Bool -> DaVinciNodeTypeParms NodeValue
forall a b. (a -> b) -> a -> b
$ DGNodeType -> Bool
isInternalSpec DGNodeType
n
    else Shape NodeValue
-> String -> GInfo -> Bool -> DaVinciNodeTypeParms NodeValue
createMenuNode Shape NodeValue
s String
c GInfo
gi (Bool -> DaVinciNodeTypeParms NodeValue)
-> Bool -> DaVinciNodeTypeParms NodeValue
forall a b. (a -> b) -> a -> b
$ DGNodeType -> Bool
isInternalSpec DGNodeType
n)) ([(DGNodeType, Shape NodeValue, String)]
 -> [(DGNodeType, DaVinciNodeTypeParms NodeValue)])
-> [(DGNodeType, Shape NodeValue, String)]
-> [(DGNodeType, DaVinciNodeTypeParms NodeValue)]
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [(DGNodeType, Shape NodeValue, String)]
nodeTypes (HetcatsOpts -> [(DGNodeType, Shape NodeValue, String)])
-> HetcatsOpts -> [(DGNodeType, Shape NodeValue, String)]
forall a b. (a -> b) -> a -> b
$ GInfo -> HetcatsOpts
hetcatsOpts GInfo
gi

-- | the edge types (share strings to avoid typos)
createEdgeTypes :: GInfo -> [(DGEdgeType, DaVinciArcTypeParms GA.EdgeValue)]
createEdgeTypes :: GInfo -> [(DGEdgeType, DaVinciArcTypeParms EdgeValue)]
createEdgeTypes gi :: GInfo
gi =
  ((DGEdgeType, EdgePattern EdgeValue, String, Bool)
 -> (DGEdgeType, DaVinciArcTypeParms EdgeValue))
-> [(DGEdgeType, EdgePattern EdgeValue, String, Bool)]
-> [(DGEdgeType, DaVinciArcTypeParms EdgeValue)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (title :: DGEdgeType
title, look :: EdgePattern EdgeValue
look, color :: String
color, hasCons :: Bool
hasCons) ->
        (DGEdgeType
title, EdgePattern EdgeValue
look
          EdgePattern EdgeValue
-> DaVinciArcTypeParms EdgeValue -> DaVinciArcTypeParms EdgeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ String -> Color EdgeValue
forall value. String -> Color value
Color String
color
          Color EdgeValue
-> DaVinciArcTypeParms EdgeValue -> DaVinciArcTypeParms EdgeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ (if Bool
hasCons then GInfo -> LocalMenu EdgeValue
createEdgeMenuConsEdge GInfo
gi
                else GInfo -> LocalMenu EdgeValue
createEdgeMenu GInfo
gi)
          LocalMenu EdgeValue
-> DaVinciArcTypeParms EdgeValue -> DaVinciArcTypeParms EdgeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ (if Bool
hasCons then ValueTitle EdgeValue
createMenuValueTitleShowConservativity
                ValueTitle EdgeValue
-> DaVinciArcTypeParms EdgeValue -> DaVinciArcTypeParms EdgeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ DaVinciArcTypeParms EdgeValue
forall (arcTypeParms :: * -> *) value.
(ArcTypeParms arcTypeParms, Typeable value) =>
arcTypeParms value
emptyArcTypeParms :: DaVinciArcTypeParms GA.EdgeValue
                else DaVinciArcTypeParms EdgeValue
forall (arcTypeParms :: * -> *) value.
(ArcTypeParms arcTypeParms, Typeable value) =>
arcTypeParms value
emptyArcTypeParms :: DaVinciArcTypeParms GA.EdgeValue))
      ) ([(DGEdgeType, EdgePattern EdgeValue, String, Bool)]
 -> [(DGEdgeType, DaVinciArcTypeParms EdgeValue)])
-> [(DGEdgeType, EdgePattern EdgeValue, String, Bool)]
-> [(DGEdgeType, DaVinciArcTypeParms EdgeValue)]
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [(DGEdgeType, EdgePattern EdgeValue, String, Bool)]
edgeTypes (HetcatsOpts
 -> [(DGEdgeType, EdgePattern EdgeValue, String, Bool)])
-> HetcatsOpts
-> [(DGEdgeType, EdgePattern EdgeValue, String, Bool)]
forall a b. (a -> b) -> a -> b
$ GInfo -> HetcatsOpts
hetcatsOpts GInfo
gi

-- * methods to create the local menus of the different nodetypes

titleNormal :: ValueTitle (String, t)
titleNormal :: ValueTitle (String, t)
titleNormal = ((String, t) -> IO String) -> ValueTitle (String, t)
forall value. (value -> IO String) -> ValueTitle value
ValueTitle (((String, t) -> IO String) -> ValueTitle (String, t))
-> ((String, t) -> IO String) -> ValueTitle (String, t)
forall a b. (a -> b) -> a -> b
$ String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String)
-> ((String, t) -> String) -> (String, t) -> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, t) -> String
forall a b. (a, b) -> a
fst

titleInternal :: GInfo -> ValueTitleSource (String, t)
titleInternal :: GInfo -> ValueTitleSource (String, t)
titleInternal gi :: GInfo
gi =
  ((String, t) -> IO (SimpleSource String))
-> ValueTitleSource (String, t)
forall value.
(value -> IO (SimpleSource String)) -> ValueTitleSource value
ValueTitleSource (\ (s :: String
s, _) -> do
                     SimpleBroadcaster String
b <- String -> IO (SimpleBroadcaster String)
forall x. x -> IO (SimpleBroadcaster x)
newSimpleBroadcaster ""
                     let updaterIORef :: IORef [(String, (String -> String) -> IO ())]
updaterIORef = GInfo -> IORef [(String, (String -> String) -> IO ())]
internalNames GInfo
gi
                     [(String, (String -> String) -> IO ())]
updater <- IORef [(String, (String -> String) -> IO ())]
-> IO [(String, (String -> String) -> IO ())]
forall a. IORef a -> IO a
readIORef IORef [(String, (String -> String) -> IO ())]
updaterIORef
                     let upd :: (String, (String -> String) -> IO ())
upd = (String
s, SimpleBroadcaster String -> (String -> String) -> IO ()
forall x. SimpleBroadcaster x -> (x -> x) -> IO ()
applySimpleUpdate SimpleBroadcaster String
b)
                     IORef [(String, (String -> String) -> IO ())]
-> [(String, (String -> String) -> IO ())] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef [(String, (String -> String) -> IO ())]
updaterIORef ([(String, (String -> String) -> IO ())] -> IO ())
-> [(String, (String -> String) -> IO ())] -> IO ()
forall a b. (a -> b) -> a -> b
$ (String, (String -> String) -> IO ())
upd (String, (String -> String) -> IO ())
-> [(String, (String -> String) -> IO ())]
-> [(String, (String -> String) -> IO ())]
forall a. a -> [a] -> [a]
: [(String, (String -> String) -> IO ())]
updater
                     SimpleSource String -> IO (SimpleSource String)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleSource String -> IO (SimpleSource String))
-> SimpleSource String -> IO (SimpleSource String)
forall a b. (a -> b) -> a -> b
$ SimpleBroadcaster String -> SimpleSource String
forall hasSource x.
HasSimpleSource hasSource x =>
hasSource -> SimpleSource x
toSimpleSource SimpleBroadcaster String
b)

-- | local menu for the nodetypes spec and locallyEmpty_spec
createMenuNode :: Shape GA.NodeValue -> String -> GInfo -> Bool
               -> DaVinciNodeTypeParms GA.NodeValue
createMenuNode :: Shape NodeValue
-> String -> GInfo -> Bool -> DaVinciNodeTypeParms NodeValue
createMenuNode shape :: Shape NodeValue
shape color :: String
color gi :: GInfo
gi internal :: Bool
internal = Shape NodeValue
shape
  Shape NodeValue
-> DaVinciNodeTypeParms NodeValue -> DaVinciNodeTypeParms NodeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ String -> Color NodeValue
forall value. String -> Color value
Color String
color
  Color NodeValue
-> DaVinciNodeTypeParms NodeValue -> DaVinciNodeTypeParms NodeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ (if Bool
internal then ValueTitleSource NodeValue -> Maybe (ValueTitleSource NodeValue)
forall a. a -> Maybe a
Just (ValueTitleSource NodeValue -> Maybe (ValueTitleSource NodeValue))
-> ValueTitleSource NodeValue -> Maybe (ValueTitleSource NodeValue)
forall a b. (a -> b) -> a -> b
$ GInfo -> ValueTitleSource NodeValue
forall t. GInfo -> ValueTitleSource (String, t)
titleInternal GInfo
gi else Maybe (ValueTitleSource NodeValue)
forall a. Maybe a
Nothing)
  Maybe (ValueTitleSource NodeValue)
-> DaVinciNodeTypeParms NodeValue -> DaVinciNodeTypeParms NodeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
Maybe (option value) -> configuration value -> configuration value
$$$? (if Bool
internal then Maybe (ValueTitle NodeValue)
forall a. Maybe a
Nothing else ValueTitle NodeValue -> Maybe (ValueTitle NodeValue)
forall a. a -> Maybe a
Just ValueTitle NodeValue
forall t. ValueTitle (String, t)
titleNormal)
  Maybe (ValueTitle NodeValue)
-> DaVinciNodeTypeParms NodeValue -> DaVinciNodeTypeParms NodeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
Maybe (option value) -> configuration value -> configuration value
$$$? MenuPrim (Maybe String) (NodeValue -> IO ()) -> LocalMenu NodeValue
forall value.
MenuPrim (Maybe String) (value -> IO ()) -> LocalMenu value
LocalMenu (Maybe String
-> [MenuPrim (Maybe String) (NodeValue -> IO ())]
-> MenuPrim (Maybe String) (NodeValue -> IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
Menu Maybe String
forall a. Maybe a
Nothing (((GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ()))
 -> MenuPrim (Maybe String) (NodeValue -> IO ()))
-> [GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())]
-> [MenuPrim (Maybe String) (NodeValue -> IO ())]
forall a b. (a -> b) -> [a] -> [b]
map ((GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ()))
-> GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
forall a b. (a -> b) -> a -> b
$ GInfo
gi)
        [ GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonShowNodeInfo
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonShowTheory
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonTranslateTheory
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuTaxonomy
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonShowProofStatusOfNode
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonProveAtNode
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonProveStructured
#ifdef GTKGLADE
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonDisproveAtNode
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonAddSentence
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonCCCAtNode
#endif
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonCheckCons
        ]))
  LocalMenu NodeValue
-> DaVinciNodeTypeParms NodeValue -> DaVinciNodeTypeParms NodeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ DaVinciNodeTypeParms NodeValue
forall (nodeTypeParms :: * -> *) value.
(NodeTypeParms nodeTypeParms, Typeable value) =>
nodeTypeParms value
emptyNodeTypeParms


-- | local menu for the nodetypes dg_ref and locallyEmpty_dg_ref
createMenuNodeRef :: Shape GA.NodeValue -> String -> GInfo -> ConvFunc
                  -> LibFunc -> Bool -> DaVinciNodeTypeParms GA.NodeValue
createMenuNodeRef :: Shape NodeValue
-> String
-> GInfo
-> ConvFunc
-> LibFunc
-> Bool
-> DaVinciNodeTypeParms NodeValue
createMenuNodeRef shape :: Shape NodeValue
shape color :: String
color gi :: GInfo
gi convGraph :: ConvFunc
convGraph showLib :: LibFunc
showLib internal :: Bool
internal = Shape NodeValue
shape
  Shape NodeValue
-> DaVinciNodeTypeParms NodeValue -> DaVinciNodeTypeParms NodeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ String -> Color NodeValue
forall value. String -> Color value
Color String
color
  Color NodeValue
-> DaVinciNodeTypeParms NodeValue -> DaVinciNodeTypeParms NodeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ (if Bool
internal then ValueTitleSource NodeValue -> Maybe (ValueTitleSource NodeValue)
forall a. a -> Maybe a
Just (ValueTitleSource NodeValue -> Maybe (ValueTitleSource NodeValue))
-> ValueTitleSource NodeValue -> Maybe (ValueTitleSource NodeValue)
forall a b. (a -> b) -> a -> b
$ GInfo -> ValueTitleSource NodeValue
forall t. GInfo -> ValueTitleSource (String, t)
titleInternal GInfo
gi else Maybe (ValueTitleSource NodeValue)
forall a. Maybe a
Nothing)
  Maybe (ValueTitleSource NodeValue)
-> DaVinciNodeTypeParms NodeValue -> DaVinciNodeTypeParms NodeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
Maybe (option value) -> configuration value -> configuration value
$$$? (if Bool
internal then Maybe (ValueTitle NodeValue)
forall a. Maybe a
Nothing else ValueTitle NodeValue -> Maybe (ValueTitle NodeValue)
forall a. a -> Maybe a
Just ValueTitle NodeValue
forall t. ValueTitle (String, t)
titleNormal)
  Maybe (ValueTitle NodeValue)
-> DaVinciNodeTypeParms NodeValue -> DaVinciNodeTypeParms NodeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
Maybe (option value) -> configuration value -> configuration value
$$$? MenuPrim (Maybe String) (NodeValue -> IO ()) -> LocalMenu NodeValue
forall value.
MenuPrim (Maybe String) (value -> IO ()) -> LocalMenu value
LocalMenu (Maybe String
-> [MenuPrim (Maybe String) (NodeValue -> IO ())]
-> MenuPrim (Maybe String) (NodeValue -> IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
Menu Maybe String
forall a. Maybe a
Nothing
        [ GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonShowNodeInfo GInfo
gi
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonShowTheory GInfo
gi
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonShowProofStatusOfNode GInfo
gi
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonProveAtNode GInfo
gi
#ifdef GTKGLADE
        , GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonDisproveAtNode GInfo
gi
#endif
        , String
-> (NodeValue -> IO ())
-> MenuPrim (Maybe String) (NodeValue -> IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Show referenced library"
            (\ (_, n :: Int
n) -> Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
showReferencedLibrary Int
n GInfo
gi ConvFunc
convGraph LibFunc
showLib)
        ])
  LocalMenu NodeValue
-> DaVinciNodeTypeParms NodeValue -> DaVinciNodeTypeParms NodeValue
forall (option :: * -> *) (configuration :: * -> *) value.
(HasConfigValue option configuration, Typeable value) =>
option value -> configuration value -> configuration value
$$$ DaVinciNodeTypeParms NodeValue
forall (nodeTypeParms :: * -> *) value.
(NodeTypeParms nodeTypeParms, Typeable value) =>
nodeTypeParms value
emptyNodeTypeParms

type ButtonMenu a = MenuPrim (Maybe String) (a -> IO ())

-- | menu button for local menus
createMenuButton :: String -> (Int -> DGraph -> IO ())
                 -> GInfo -> ButtonMenu GA.NodeValue
createMenuButton :: String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton title :: String
title menuFun :: Int -> DGraph -> IO ()
menuFun gi :: GInfo
gi = String
-> (NodeValue -> IO ())
-> MenuPrim (Maybe String) (NodeValue -> IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button String
title
  ((NodeValue -> IO ())
 -> MenuPrim (Maybe String) (NodeValue -> IO ()))
-> (NodeValue -> IO ())
-> MenuPrim (Maybe String) (NodeValue -> IO ())
forall a b. (a -> b) -> a -> b
$ \ (_, descr :: Int
descr) -> do
    IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gi
    case IntState -> Maybe IntIState
i_state IntState
ost of
      Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just ist :: IntIState
ist -> do
        let le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
ist
            dGraph :: DGraph
dGraph = LibName -> LibEnv -> DGraph
lookupDGraph (GInfo -> LibName
libName GInfo
gi) LibEnv
le
        Int -> DGraph -> IO ()
menuFun Int
descr DGraph
dGraph
        () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

createMenuButtonShowTheory :: GInfo -> ButtonMenu GA.NodeValue
createMenuButtonShowTheory :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonShowTheory gi :: GInfo
gi =
  String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Show theory" (GInfo -> Int -> DGraph -> IO ()
getTheoryOfNode GInfo
gi) GInfo
gi

createMenuButtonTranslateTheory :: GInfo -> ButtonMenu GA.NodeValue
createMenuButtonTranslateTheory :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonTranslateTheory gi :: GInfo
gi =
  String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Translate theory" (GInfo -> Int -> DGraph -> IO ()
translateTheoryOfNode GInfo
gi) GInfo
gi

-- | create a sub menu for taxonomy visualisation
createMenuTaxonomy :: GInfo -> ButtonMenu GA.NodeValue
createMenuTaxonomy :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuTaxonomy gi :: GInfo
gi = let
  passTh :: (String -> G_theory -> IO ()) -> Int -> p -> IO ()
passTh displayFun :: String -> G_theory -> IO ()
displayFun descr :: Int
descr _ = do
    IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef (IORef IntState -> IO IntState) -> IORef IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ GInfo -> IORef IntState
intState GInfo
gi
    case IntState -> Maybe IntIState
i_state IntState
ost of
      Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just ist :: IntIState
ist -> case LibEnv -> LibName -> Int -> Maybe G_theory
computeTheory (IntIState -> LibEnv
i_libEnv IntIState
ist) (GInfo -> LibName
libName GInfo
gi) Int
descr of
        Just th :: G_theory
th -> String -> G_theory -> IO ()
displayFun (Int -> String
forall a. Show a => a -> String
show Int
descr) G_theory
th
        Nothing -> String -> String -> IO ()
errorDialog "Error"
          (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "no global theory for node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
descr
  in Maybe String
-> [MenuPrim (Maybe String) (NodeValue -> IO ())]
-> MenuPrim (Maybe String) (NodeValue -> IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
Menu (String -> Maybe String
forall a. a -> Maybe a
Just "Taxonomy graphs")
    [ String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Subsort graph" ((String -> G_theory -> IO ()) -> Int -> DGraph -> IO ()
forall p. (String -> G_theory -> IO ()) -> Int -> p -> IO ()
passTh String -> G_theory -> IO ()
displaySubsortGraph) GInfo
gi
    , String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Concept graph" ((String -> G_theory -> IO ()) -> Int -> DGraph -> IO ()
forall p. (String -> G_theory -> IO ()) -> Int -> p -> IO ()
passTh String -> G_theory -> IO ()
displayConceptGraph) GInfo
gi ]

createMenuButtonShowProofStatusOfNode :: GInfo -> ButtonMenu GA.NodeValue
createMenuButtonShowProofStatusOfNode :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonShowProofStatusOfNode gi :: GInfo
gi =
  String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Show proof status" (GInfo -> Int -> DGraph -> IO ()
showProofStatusOfNode GInfo
gi) GInfo
gi

createMenuButtonProveAtNode :: GInfo -> ButtonMenu GA.NodeValue
createMenuButtonProveAtNode :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonProveAtNode gi :: GInfo
gi =
  String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Prove" (GInfo -> Int -> DGraph -> IO ()
proveAtNode GInfo
gi) GInfo
gi

createMenuButtonProveStructured :: GInfo -> ButtonMenu GA.NodeValue
createMenuButtonProveStructured :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonProveStructured gi :: GInfo
gi =
  String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Prove VSE Structured" (\ descr :: Int
descr _ ->
    GInfo -> Command -> (LibEnv -> IO (Result LibEnv)) -> IO ()
proofMenu GInfo
gi (SelectCmd -> String -> Command
SelectCmd SelectCmd
Prover (String -> Command) -> String -> Command
forall a b. (a -> b) -> a -> b
$ "VSE structured: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
descr)
              ((LibEnv -> IO (Result LibEnv)) -> IO ())
-> (LibEnv -> IO (Result LibEnv)) -> IO ()
forall a b. (a -> b) -> a -> b
$ (LibName, Int) -> LibEnv -> IO (Result LibEnv)
VSE.proveVSE (GInfo -> LibName
libName GInfo
gi, Int
descr)) GInfo
gi

#ifdef GTKGLADE
createMenuButtonDisproveAtNode :: GInfo -> ButtonMenu GA.NodeValue
createMenuButtonDisproveAtNode :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonDisproveAtNode gi :: GInfo
gi =
  String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Disprove" (GInfo -> Int -> DGraph -> IO ()
disproveAtNode GInfo
gi) GInfo
gi

createMenuButtonCCCAtNode :: GInfo -> ButtonMenu GA.NodeValue
createMenuButtonCCCAtNode :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonCCCAtNode gi :: GInfo
gi =
  String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Check consistency" (GInfo -> Int -> DGraph -> IO ()
consCheckNode GInfo
gi) GInfo
gi

consCheckNode :: GInfo -> Int -> DGraph -> IO ()
consCheckNode :: GInfo -> Int -> DGraph -> IO ()
consCheckNode gi :: GInfo
gi descr :: Int
descr _ = GInfo -> Command -> (LibEnv -> IO (Result LibEnv)) -> IO ()
proofMenu GInfo
gi (GlobCmd -> Command
GlobCmd GlobCmd
CheckConsistencyCurrent)
  ((LibEnv -> IO (Result LibEnv)) -> IO ())
-> (LibEnv -> IO (Result LibEnv)) -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe Int -> GInfo -> LibEnv -> IO (Result LibEnv)
showConsistencyChecker (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
descr) GInfo
gi

createMenuButtonAddSentence :: GInfo -> ButtonMenu GA.NodeValue
createMenuButtonAddSentence :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonAddSentence gi :: GInfo
gi =
  String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Add sentence" (GInfo -> Int -> DGraph -> IO ()
gtkAddSentence GInfo
gi) GInfo
gi
#endif

createMenuButtonCheckCons :: GInfo -> ButtonMenu GA.NodeValue
createMenuButtonCheckCons :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonCheckCons gi :: GInfo
gi =
  String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Check conservativity"
    (GInfo -> Int -> DGraph -> IO ()
checkconservativityOfNode GInfo
gi) GInfo
gi

createMenuButtonShowNodeInfo :: GInfo -> ButtonMenu GA.NodeValue
createMenuButtonShowNodeInfo :: GInfo -> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButtonShowNodeInfo =
  String
-> (Int -> DGraph -> IO ())
-> GInfo
-> MenuPrim (Maybe String) (NodeValue -> IO ())
createMenuButton "Show node info" Int -> DGraph -> IO ()
showNodeInfo

-- * methods to create the local menus for the edges

createEdgeMenu :: GInfo -> LocalMenu GA.EdgeValue
createEdgeMenu :: GInfo -> LocalMenu EdgeValue
createEdgeMenu = MenuPrim (Maybe String) (EdgeValue -> IO ()) -> LocalMenu EdgeValue
forall value.
MenuPrim (Maybe String) (value -> IO ()) -> LocalMenu value
LocalMenu (MenuPrim (Maybe String) (EdgeValue -> IO ())
 -> LocalMenu EdgeValue)
-> (GInfo -> MenuPrim (Maybe String) (EdgeValue -> IO ()))
-> GInfo
-> LocalMenu EdgeValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo -> MenuPrim (Maybe String) (EdgeValue -> IO ())
createMenuButtonShowEdgeInfo

createEdgeMenuConsEdge :: GInfo -> LocalMenu GA.EdgeValue
createEdgeMenuConsEdge :: GInfo -> LocalMenu EdgeValue
createEdgeMenuConsEdge gi :: GInfo
gi = MenuPrim (Maybe String) (EdgeValue -> IO ()) -> LocalMenu EdgeValue
forall value.
MenuPrim (Maybe String) (value -> IO ()) -> LocalMenu value
LocalMenu (MenuPrim (Maybe String) (EdgeValue -> IO ())
 -> LocalMenu EdgeValue)
-> MenuPrim (Maybe String) (EdgeValue -> IO ())
-> LocalMenu EdgeValue
forall a b. (a -> b) -> a -> b
$ Maybe String
-> [MenuPrim (Maybe String) (EdgeValue -> IO ())]
-> MenuPrim (Maybe String) (EdgeValue -> IO ())
forall subMenuValue value.
subMenuValue
-> [MenuPrim subMenuValue value] -> MenuPrim subMenuValue value
Menu Maybe String
forall a. Maybe a
Nothing
  [ GInfo -> MenuPrim (Maybe String) (EdgeValue -> IO ())
createMenuButtonShowEdgeInfo GInfo
gi
  , GInfo -> MenuPrim (Maybe String) (EdgeValue -> IO ())
createMenuButtonCheckconservativityOfEdge GInfo
gi]

createMenuButtonShowEdgeInfo :: GInfo -> ButtonMenu GA.EdgeValue
createMenuButtonShowEdgeInfo :: GInfo -> MenuPrim (Maybe String) (EdgeValue -> IO ())
createMenuButtonShowEdgeInfo _ = String
-> (EdgeValue -> IO ())
-> MenuPrim (Maybe String) (EdgeValue -> IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Show info"
  (\ (_, EdgeId descr :: Int
descr, maybeLEdge :: Maybe (LEdge DGLinkLab)
maybeLEdge) -> Int -> Maybe (LEdge DGLinkLab) -> IO ()
showEdgeInfo Int
descr Maybe (LEdge DGLinkLab)
maybeLEdge)

createMenuButtonCheckconservativityOfEdge :: GInfo -> ButtonMenu GA.EdgeValue
createMenuButtonCheckconservativityOfEdge :: GInfo -> MenuPrim (Maybe String) (EdgeValue -> IO ())
createMenuButtonCheckconservativityOfEdge gi :: GInfo
gi =
  String
-> (EdgeValue -> IO ())
-> MenuPrim (Maybe String) (EdgeValue -> IO ())
forall subMenuValue value.
String -> value -> MenuPrim subMenuValue value
Button "Check conservativity"
    (\ (_, EdgeId descr :: Int
descr, maybeLEdge :: Maybe (LEdge DGLinkLab)
maybeLEdge) ->
      Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
checkconservativityOfEdge Int
descr GInfo
gi Maybe (LEdge DGLinkLab)
maybeLEdge)

createMenuValueTitleShowConservativity :: ValueTitle GA.EdgeValue
createMenuValueTitleShowConservativity :: ValueTitle EdgeValue
createMenuValueTitleShowConservativity = (EdgeValue -> IO String) -> ValueTitle EdgeValue
forall value. (value -> IO String) -> ValueTitle value
ValueTitle
  (\ (_, _, maybeLEdge :: Maybe (LEdge DGLinkLab)
maybeLEdge) -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ case Maybe (LEdge DGLinkLab)
maybeLEdge of
    Just (_, _, edgelab :: DGLinkLab
edgelab) -> ConsStatus -> String
showConsStatus (ConsStatus -> String) -> ConsStatus -> String
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> ConsStatus
getEdgeConsStatus DGLinkLab
edgelab
    Nothing -> "")

-- Suggests a proof-script filename.
getProofScriptFileName :: String -> IO FilePath
getProofScriptFileName :: String -> IO String
getProofScriptFileName f :: String
f = let fn :: String
fn = String
f String -> String -> String
<.> "hpf" in
  if String -> Bool
isAbsolute String
fn then String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
fn else
     (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> String -> String
</> String
fn) IO String
getCurrentDirectory

-- | Displays a Save-As dialog and writes the proof-script.
askSaveProofScript :: GA.GraphInfo -> IORef IntState -> IO ()
askSaveProofScript :: GraphInfo -> IORef IntState -> IO ()
askSaveProofScript gi :: GraphInfo
gi ch :: IORef IntState
ch = do
  IntState
h <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef IORef IntState
ch
  case IntHistory -> [CmdHistory]
undoList (IntHistory -> [CmdHistory]) -> IntHistory -> [CmdHistory]
forall a b. (a -> b) -> a -> b
$ IntState -> IntHistory
i_hist IntState
h of
   [] -> String -> String -> IO ()
infoDialog "Information" "The history is empty. No file written."
   _ -> do
     String
ff <- String -> IO String
getProofScriptFileName (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String -> String
rmSuffix (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ IntState -> String
filename IntState
h
     Maybe String
maybeFilePath <- String
-> [(String, [String])]
-> Maybe (String -> IO ())
-> IO (Maybe String)
fileSaveDialog String
ff [ ("Proof Script", ["*.hpf"])
                                        , ("All Files", ["*"])] Maybe (String -> IO ())
forall a. Maybe a
Nothing
     case Maybe String
maybeFilePath of
       Just fPath :: String
fPath -> do
         GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi "Saving proof script ..."
         IORef IntState -> String -> IO ()
saveCommandHistory IORef IntState
ch String
fPath
         GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Proof script saved to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fPath String -> String -> String
forall a. [a] -> [a] -> [a]
++ "!"
       Nothing -> GraphInfo -> String -> IO ()
GA.showTemporaryMessage GraphInfo
gi "Aborted!"

-- Saves the history of commands in a file.
saveCommandHistory :: IORef IntState -> String -> IO ()
saveCommandHistory :: IORef IntState -> String -> IO ()
saveCommandHistory c :: IORef IntState
c f :: String
f = do
  IntState
h <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef IORef IntState
c
  let history :: [String]
history = [ "# automatically generated hets proof-script", ""
                , "use " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IntState -> String
filename IntState
h, ""]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> [String]
forall a. [a] -> [a]
reverse ((CmdHistory -> String) -> [CmdHistory] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Command -> String
showCmd (Command -> String)
-> (CmdHistory -> Command) -> CmdHistory -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdHistory -> Command
command) ([CmdHistory] -> [String]) -> [CmdHistory] -> [String]
forall a b. (a -> b) -> a -> b
$ IntHistory -> [CmdHistory]
undoList (IntHistory -> [CmdHistory]) -> IntHistory -> [CmdHistory]
forall a b. (a -> b) -> a -> b
$ IntState -> IntHistory
i_hist IntState
h)
  String -> String -> IO ()
writeFile String
f (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
history