hets.hs revision c63ebf815c8a874525cf18670ad74847f7fc7b26
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder{-# OPTIONS -cpp #-}
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian MaederModule : $Id$
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian MaederCopyright : (c) Uni Bremen 2003-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian MaederMaintainer : Christian.Maeder@dfki.de
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian MaederStability : provisional
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian MaederPortability : non-portable (imports Logic.Logic)
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian MaederThe Main module of the Heterogeneous Tool Set.
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder It provides the main function to call (and not much more).
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder-}
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder-- for interactice purposes use Test.hs
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maedermodule Main where
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maederimport System.Environment (getArgs)
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maederimport Driver.Options
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maederimport Driver.ReadFn
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder
51a70608c77400c4779e0ed000a2aedd0adecd14Christian Maeder#ifdef CASLEXTENSIONS
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maederimport OWL_DL.OWLAnalysis
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder#endif
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maederimport OMDoc.OMDocInput
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maederimport Static.AnalysisLibrary
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder#ifdef UNI_PACKAGE
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maederimport GUI.ShowGraph
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder#endif
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder#ifdef PROGRAMATICA
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maederimport Haskell.Haskell2DG
63bfead0a5fff45fd048df7cdae2c8b51574c6ecChristian Maeder#endif
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport System.Exit (ExitCode(ExitSuccess), exitWith)
5dc4eccbc2a3a60f46c200d8b337a6c2f1d54144Christian Maeder
import PGIP.Interface
main :: IO ()
main = do
opts <- getArgs >>= hetcatsOpts
if (interactive opts)
then do
cmdlRunShell (infiles opts)
return ()
else do
putIfVerbose opts 3 ("Options: " ++ show opts)
mapM_ (processFile opts) (infiles opts)
processFile :: HetcatsOpts -> FilePath -> IO ()
processFile opts file =
do putIfVerbose opts 3 ("Processing input: " ++ file)
case guess file (intype opts) of
s -> do
res <- case s of
#ifdef PROGRAMATICA
HaskellIn -> anaHaskellFile opts file
#endif
#ifdef CASLEXTENSIONS
OWL_DLIn -> do
ontoMap <- parseOWL file
structureAna file opts ontoMap
#endif
OmdocIn -> do
mLibEnvFromOMDocFile opts file
PrfIn -> do
m <- anaLib (removePrfOut opts) file
case m of
Nothing -> return Nothing
Just (ln, libEnv) -> do
proofStatus <- readPrfFiles opts libEnv
return $ Just (ln, proofStatus)
ProofCommand -> do
putStrLn "Start processing a proof command file"
cmdlProcessFile file
return Nothing
_ -> anaLib opts file
case gui opts of
Not -> return ()
_ -> do
#ifdef UNI_PACKAGE
showGraph file opts res
exitWith ExitSuccess
#else
fail $ "No graph display interface; \n" ++
"UNI_PACKAGE option has been "++
"disabled during compilation of Hets"
#endif