{-# LANGUAGE CPP #-}
{- |
Module      :  $Id$
Description :  main Hets module (providing binary executable)
Copyright   :  (c) Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

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

The Main module of the Heterogeneous Tool Set.
   It provides the main function to call (and not much more).

-}

-- for interactice purposes use Test.hs

module Main where

import System.Environment (getArgs)

import Control.Monad
import qualified Control.Monad.Fail as Fail

import Driver.Options
import Driver.ReadFn (showFileType)
import Driver.ReadMain
import Driver.WriteFn

import Static.DevGraph
import Logic.PrintLogics

#ifdef UNI_PACKAGE
import GUI.ShowGraph
import GUI.ShowLogicGraph
#endif

#ifdef PROGRAMATICA
import Haskell.Haskell2DG
#endif

import Common.LibName
import Interfaces.DataTypes
import CMDL.ProcessScript
import CMDL.Interface (cmdlRunShell)
import CMDL.DataTypes
import PGIP.XMLparsing
import PGIP.XMLstate (isRemote)
#ifdef SERVER
import PGIP.Server
#endif


main :: IO ()
main :: IO ()
main =
  IO [String]
getArgs IO [String] -> ([String] -> IO HetcatsOpts) -> IO HetcatsOpts
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [String] -> IO HetcatsOpts
hetcatsOpts IO HetcatsOpts -> (HetcatsOpts -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ opts :: HetcatsOpts
opts -> let imode :: Bool
imode = HetcatsOpts -> Bool
interactive HetcatsOpts
opts in
    HetcatsOpts -> IO ()
printOptionsWarnings HetcatsOpts
opts IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
#ifdef SERVER
     if HetcatsOpts -> Bool
serve HetcatsOpts
opts then HetcatsOpts -> IO ()
hetsServer HetcatsOpts
opts else
#endif
     if HetcatsOpts -> Bool
isRemote HetcatsOpts
opts Bool -> Bool -> Bool
|| Bool
imode
       then HetcatsOpts -> IO CmdlState
cmdlRun HetcatsOpts
opts IO CmdlState -> (CmdlState -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
displayGraph "" HetcatsOpts
opts (Maybe (LibName, LibEnv) -> IO ())
-> (CmdlState -> Maybe (LibName, LibEnv)) -> CmdlState -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntState -> Maybe (LibName, LibEnv)
getMaybeLib (IntState -> Maybe (LibName, LibEnv))
-> (CmdlState -> IntState) -> CmdlState -> Maybe (LibName, LibEnv)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlState -> IntState
intState
       else do
         HetcatsOpts -> Int -> String -> IO ()
putIfVerbose HetcatsOpts
opts 3 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Options: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ HetcatsOpts -> String
forall a. Show a => a -> String
show HetcatsOpts
opts
         if HetcatsOpts -> Bool
outputLogicList HetcatsOpts
opts
            then IO ()
printLogics
         else  
          case (HetcatsOpts -> [String]
infiles HetcatsOpts
opts, HetcatsOpts -> Bool
outputLogicGraph HetcatsOpts
opts) of
           ([], lg :: Bool
lg) -> case HetcatsOpts -> GuiType
guiType HetcatsOpts
opts of
             UseGui ->
#ifdef UNI_PACKAGE
               IO ()
showPlainLG
#else
               noUniPkg
#endif
             NoGui | Bool
lg -> HetcatsOpts -> IO ()
writeLG HetcatsOpts
opts
             _ -> String -> IO ()
forall a. String -> IO a
hetsIOError "supply option -G or -g and/or file arguments"
           (fs :: [String]
fs, False) -> (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HetcatsOpts -> String -> IO ()
processFile HetcatsOpts
opts) [String]
fs
           _ -> String -> IO ()
forall a. String -> IO a
hetsIOError
             "option -G is illegal together with file arguments (use -g)"

noUniPkg :: IO ()
noUniPkg :: IO ()
noUniPkg = String -> IO ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "No graph display interface; \n"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ "UNI_PACKAGE option has been "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ "disabled during compilation of Hets"

processFile :: HetcatsOpts -> FilePath -> IO ()
processFile :: HetcatsOpts -> String -> IO ()
processFile opts :: HetcatsOpts
opts file :: String
file = if HetcatsOpts -> Bool
fileType HetcatsOpts
opts then HetcatsOpts -> String -> IO ()
showFileType HetcatsOpts
opts String
file else do
    HetcatsOpts -> Int -> String -> IO ()
putIfVerbose HetcatsOpts
opts 3 ("Processing input: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file)
    let doExit :: Bool
doExit = HetcatsOpts -> GuiType
guiType HetcatsOpts
opts GuiType -> GuiType -> Bool
forall a. Eq a => a -> a -> Bool
== GuiType
UseGui
    Maybe (LibName, LibEnv)
res <- if String -> InType -> InType
guess String
file (HetcatsOpts -> InType
intype HetcatsOpts
opts) InType -> InType -> Bool
forall a. Eq a => a -> a -> Bool
== InType
ProofCommand then do
                CmdlState
st <- Bool -> HetcatsOpts -> String -> IO CmdlState
cmdlProcessFile Bool
doExit HetcatsOpts
opts String
file
                (CmdlState -> Maybe (LibName, LibEnv))
-> IO CmdlState -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (IntState -> Maybe (LibName, LibEnv)
getMaybeLib (IntState -> Maybe (LibName, LibEnv))
-> (CmdlState -> IntState) -> CmdlState -> Maybe (LibName, LibEnv)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlState -> IntState
intState)
                 (IO CmdlState -> IO (Maybe (LibName, LibEnv)))
-> IO CmdlState -> IO (Maybe (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ (if HetcatsOpts -> Bool
interactive HetcatsOpts
opts then CmdlState -> IO CmdlState
cmdlRunShell else CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return) CmdlState
st
           else String -> HetcatsOpts -> IO (Maybe (LibName, LibEnv))
readAndAnalyse String
file HetcatsOpts
opts
    case Maybe (LibName, LibEnv)
res of
      Just (ln :: LibName
ln, nEnv :: LibEnv
nEnv) ->
        HetcatsOpts -> String -> LibEnv -> LibName -> DGraph -> IO ()
writeSpecFiles HetcatsOpts
opts String
file LibEnv
nEnv LibName
ln (DGraph -> IO ()) -> DGraph -> IO ()
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
nEnv
      _ -> String -> IO ()
forall a. String -> IO a
hetsIOError ""
    if String -> InType -> InType
guess String
file (HetcatsOpts -> InType
intype HetcatsOpts
opts) InType -> InType -> Bool
forall a. Eq a => a -> a -> Bool
/= InType
ProofCommand Bool -> Bool -> Bool
&& HetcatsOpts -> Bool
interactive HetcatsOpts
opts
      then HetcatsOpts -> IO CmdlState
cmdlRun HetcatsOpts
opts IO CmdlState -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () else String -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
displayGraph String
file HetcatsOpts
opts Maybe (LibName, LibEnv)
res

displayGraph :: FilePath -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
displayGraph :: String -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
displayGraph _ (HcOpt {guiType :: HetcatsOpts -> GuiType
guiType = GuiType
NoGui}) _ = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
#ifdef UNI_PACKAGE
displayGraph file :: String
file opts :: HetcatsOpts
opts res :: Maybe (LibName, LibEnv)
res = String -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
showGraph String
file HetcatsOpts
opts Maybe (LibName, LibEnv)
res
#else
displayGraph _ _ _ = noUniPkg
#endif