{-# 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 :: ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
genericATPgui = ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
Gtk.genericATPgui
#elif defined UNI_PACKAGE
genericATPgui = HTk.genericATPgui
#else
genericATPgui = error "not implemented"
#endif