hets.hs revision bdc103981a28a51938de98a956d8a3767f6cf43d
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher{-# LANGUAGE CPP #-}
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen GallagherCopyright : (c) Uni Bremen 2003-2005
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen GallagherLicense : GPLv2 or higher, see LICENSE.txt
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen GallagherMaintainer : Christian.Maeder@dfki.de
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen GallagherStability : provisional
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen GallagherPortability : non-portable (imports Logic.Logic)
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen GallagherThe Main module of the Heterogeneous Tool Set.
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher It provides the main function to call (and not much more).
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher-- for interactice purposes use Test.hs
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallaghermodule Main where
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher#ifdef UNI_PACKAGE
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher#ifdef PROGRAMATICA
728a1812b7c5f70febb522342c5b357da598acfeJakub Hrozekimport PGIP.XMLstate (isRemote)
728a1812b7c5f70febb522342c5b357da598acfeJakub Hrozek#ifdef SERVER
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagherimport Maude.Maude2DG (anaMaudeFile)
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagherimport LF.Twelf2DG (anaTwelfFile)
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagherimport OMDoc.Import (anaOMDocFile)
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagherimport HolLight.HolLight2DG (anaHolLightFile)
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagherimport Isabelle.Isa2DG (anaIsaFile,anaThyFile)
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher getArgs >>= hetcatsOpts >>= \ opts ->
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher if serve opts then hetsServer opts else
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher if isRemote opts || interactive opts
5f879ab8b6c1cefbc63e1c2303f79b09b6246ca3Stephen Gallagher then cmdlRun opts >>= displayGraph "" opts . getMaybeLib . intState
5f879ab8b6c1cefbc63e1c2303f79b09b6246ca3Stephen Gallagher putIfVerbose opts 3 $ "Options: " ++ show opts
5f879ab8b6c1cefbc63e1c2303f79b09b6246ca3Stephen Gallagher mapM_ (processFile opts) (infiles opts)
5f879ab8b6c1cefbc63e1c2303f79b09b6246ca3Stephen GallagherprocessFile :: HetcatsOpts -> FilePath -> IO ()
5f879ab8b6c1cefbc63e1c2303f79b09b6246ca3Stephen GallagherprocessFile opts file = do
5f879ab8b6c1cefbc63e1c2303f79b09b6246ca3Stephen Gallagher putIfVerbose opts 3 ("Processing input: " ++ file)
5f879ab8b6c1cefbc63e1c2303f79b09b6246ca3Stephen Gallagher res <- case guess file (intype opts) of
4343b618051d295cbb1a805a85feb117a91c6945Jakub Hrozek#ifdef PROGRAMATICA
4343b618051d295cbb1a805a85feb117a91c6945Jakub Hrozek HaskellIn -> putStr "this is HaskellIn" >> anaHaskellFile opts file
4343b618051d295cbb1a805a85feb117a91c6945Jakub Hrozek#ifdef HEXPAT
4343b618051d295cbb1a805a85feb117a91c6945Jakub Hrozek HolLightIn -> anaHolLightFile opts file
c7a4383b3b5549d0627c21bb02bd5f0bd46a3531Jakub Hrozek IsaIn -> anaIsaFile opts file
5f879ab8b6c1cefbc63e1c2303f79b09b6246ca3Stephen Gallagher ThyIn -> anaThyFile opts file
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher PrfIn -> anaLibReadPrfs opts file
65a8e6e655c22027d3e02ea697972111f2a33e33Jakub Hrozek ProofCommand -> do
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher st <- cmdlProcessFile opts file
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher return . getMaybeLib $ intState st
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher MaudeIn -> anaMaudeFile opts file
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher TwelfIn -> anaTwelfFile opts file
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher OmdocIn -> anaOMDocFile opts file
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher DgXml | not (defLogicIsDMU opts) -> readDGXml opts file
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher _ -> anaLib opts file
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher Just (ln, nEnv) ->
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher writeSpecFiles opts file nEnv ln $ lookupDGraph ln nEnv
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher _ -> return ()
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher displayGraph file opts res
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen GallagherdisplayGraph :: FilePath -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher#ifdef UNI_PACKAGE
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen GallagherdisplayGraph file opts res = case guiType opts of
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher NoGui -> return ()
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen Gallagher UseGui -> showGraph file opts res
03532fb1cbb7e8c1d5cf2e93aa3719f926631cabStephen GallagherdisplayGraph _ opts _ = when (guiType opts == UseGui)
4cdaf239d4504966bed8ecd5e3fa07def74c7302Sumit Bose $ fail $ "No graph display interface; \n"
4cdaf239d4504966bed8ecd5e3fa07def74c7302Sumit Bose ++ "UNI_PACKAGE option has been "
4cdaf239d4504966bed8ecd5e3fa07def74c7302Sumit Bose ++ "disabled during compilation of Hets"