content: {-# LANGUAGE CPP #-}
  {- |
  Module      :  ./GUI/GenericATP.hs
  Description :  Generic Prover GUI.
  Copyright   :  (c) Thiemo Wiedemeyer, Uni Bremen 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  raider@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  needs POSIX
  
  Generic GUI for automatic theorem provers. CPP between HTk and Gtk.
  -}
  
  module GUI.GenericATP (genericATPgui) where
  
  import Interfaces.GenericATPState
  
  import Logic.Prover
  
  #ifdef GTKGLADE
  import qualified GUI.GtkGenericATP as Gtk
  #elif defined UNI_PACKAGE
  import qualified GUI.HTkGenericATP as HTk
  #endif
  
  {- |
    Invokes the prover GUI. Users may start the batch prover run on all goals,
    or use a detailed GUI for proving each goal manually.
  -}
  genericATPgui :: (Show sentence, Ord proof_tree, Ord sentence)
                => ATPFunctions sign sentence mor proof_tree pst
                -- ^ prover specific -- functions
                -> Bool -- ^ prover supports extra options
                -> String -- ^ prover name
                -> String -- ^ theory name
                -> Theory sign sentence proof_tree {- ^ theory consisting of a
                   signature and a list of Named sentence -}
                -> [FreeDefMorphism sentence mor] -- ^ freeness constraints
                -> proof_tree -- ^ initial empty proof_tree
                -> IO [ProofStatus proof_tree] -- ^ proof status for each goal
  #ifdef GTKGLADE
  genericATPgui = Gtk.genericATPgui
  #elif defined UNI_PACKAGE
  genericATPgui = HTk.genericATPgui
  #else
  genericATPgui = error "not implemented"
  #endif
  