{- |
Module      :  ./GUI/GtkAddSentence.hs
Description :  Gtk GUI for adding a sentence
Copyright   :  (c) C. Maeder DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports existential types)

This module provides a GUI to add a sentence
-}

module GUI.GtkAddSentence where

import Graphics.UI.Gtk

import GUI.GtkUtils
import qualified GUI.Glade.TextField as TextField
import GUI.GraphTypes
import GUI.GraphLogic

import Interfaces.Utils

import Static.DevGraph
import Static.GTheory
import Static.FromXmlUtils (BasicExtResponse (..), extendByBasicSpec)

import Common.GlobalAnnotations

import Control.Monad
import Data.IORef

gtkAddSentence :: GInfo -> Int -> DGraph -> IO ()
gtkAddSentence :: GInfo -> Int -> DGraph -> IO ()
gtkAddSentence gi :: GInfo
gi n :: Int
n dg :: DGraph
dg = IO () -> IO ()
postGUIAsync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  Builder
builder <- (String, String) -> IO Builder
getGTKBuilder (String, String)
TextField.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 "TextField"
  Button
btnAbort <- 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 "abort"
  Button
btnAdd <- 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 "add"
  Entry
entry <- Builder -> (GObject -> Entry) -> String -> IO Entry
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Entry
forall obj. GObjectClass obj => obj -> Entry
castToEntry "entry"
  let lbl :: DGNodeLab
lbl = DGraph -> Int -> DGNodeLab
labDG DGraph
dg Int
n
      name :: String
name = DGNodeLab -> String
getDGNodeName DGNodeLab
lbl
  Window -> String -> IO ()
forall self string.
(WindowClass self, GlibString string) =>
self -> string -> IO ()
windowSetTitle Window
window (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Add sentence to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnAbort (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
btnAdd (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
    String
sen <- Entry -> IO String
forall self string.
(EntryClass self, GlibString string) =>
self -> IO string
entryGetText Entry
entry
    Bool
abort <- GInfo -> GlobalAnnos -> Int -> DGNodeLab -> String -> IO Bool
anaSentence GInfo
gi (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) Int
n DGNodeLab
lbl String
sen
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
abort (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetDestroy Window
window
  Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetShow Window
window

errorFeedback :: Bool -> String -> IO Bool
errorFeedback :: Bool -> String -> IO Bool
errorFeedback abort :: Bool
abort msg :: String
msg =
   String -> String -> IO ()
errorDialog "Error" String
msg IO () -> IO Bool -> IO Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
abort

anaSentence :: GInfo -> GlobalAnnos -> Int -> DGNodeLab -> String -> IO Bool
anaSentence :: GInfo -> GlobalAnnos -> Int -> DGNodeLab -> String -> IO Bool
anaSentence gi :: GInfo
gi ga :: GlobalAnnos
ga n :: Int
n lbl :: DGNodeLab
lbl sen :: String
sen = case GlobalAnnos -> String -> G_theory -> (BasicExtResponse, String)
extendByBasicSpec GlobalAnnos
ga String
sen (G_theory -> (BasicExtResponse, String))
-> G_theory -> (BasicExtResponse, String)
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl of
  (Success gTh :: G_theory
gTh num :: Int
num _ sameSig :: Bool
sameSig, str :: String
str)
    | Bool -> Bool
not Bool
sameSig -> Bool -> String -> IO Bool
errorFeedback Bool
False (String -> IO Bool) -> String -> IO Bool
forall a b. (a -> b) -> a -> b
$ "signature must not change\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str
    | Int
num Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 -> Bool -> String -> IO Bool
errorFeedback Bool
False "no sentence recognized"
    | Int
num Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 -> Bool -> String -> IO Bool
errorFeedback Bool
False (String -> IO Bool) -> String -> IO Bool
forall a b. (a -> b) -> a -> b
$ "multiple sentences recognized\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str
    | Bool
otherwise -> do
         GInfo -> Int -> DGNodeLab -> G_theory -> IO ()
addSentence GInfo
gi Int
n DGNodeLab
lbl G_theory
gTh
         Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  (Failure b :: Bool
b, str :: String
str) -> Bool -> String -> IO Bool
errorFeedback Bool
b String
str

addSentence :: GInfo -> Int -> DGNodeLab -> G_theory -> IO ()
addSentence :: GInfo -> Int -> DGNodeLab -> G_theory -> IO ()
addSentence gi :: GInfo
gi n :: Int
n lbl :: DGNodeLab
lbl th :: G_theory
th = do
      let ln :: LibName
ln = GInfo -> LibName
libName GInfo
gi
          iSt :: IORef IntState
iSt = GInfo -> IORef IntState
intState GInfo
gi
      IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef IORef IntState
iSt
      let (ost' :: IntState
ost', hist :: [DGChange]
hist) = LibName
-> IntState
-> LNode DGNodeLab
-> G_theory
-> (IntState, [DGChange])
updateNodeProof LibName
ln IntState
ost (Int
n, DGNodeLab
lbl) G_theory
th
      IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef IntState
iSt IntState
ost'
      GInfo -> IO () -> IO ()
runAndLock GInfo
gi (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> [DGChange] -> IO ()
updateGraph GInfo
gi [DGChange]
hist