hets.hs revision 9f85afecbd79b3df5a0bb17bd28cd0b288dc3213
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert Wapshott{-# LANGUAGE CPP #-}
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert WapshottCopyright : (c) Uni Bremen 2003-2005
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert WapshottLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert WapshottMaintainer : Christian.Maeder@dfki.de
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert WapshottStability : provisional
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert WapshottPortability : non-portable (imports Logic.Logic)
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert WapshottThe Main module of the Heterogeneous Tool Set.
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert Wapshott It provides the main function to call (and not much more).
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert Wapshott-- for interactice purposes use Test.hs
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert Wapshottmodule Main where
eba2b2ec966be265972d5fc47fa408a628a7139cTom Rumsey#ifndef NOOWLLOGIC
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey#ifdef HXTFILTER
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey#ifdef UNI_PACKAGE
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumseyimport Control.Monad ( when )
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey#ifdef PROGRAMATICA
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumseyimport PGIP.XMLstate (isRemote)
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumseyimport Maude.Maude2DG (anaMaudeFile)
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumseyimport LF.Twelf2DG (anaTwelfFile)
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumseymain :: IO ()
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey getArgs >>= hetcatsOpts >>= \ opts ->
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert Wapshott if isRemote opts || interactive opts
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert Wapshott then cmdlRun opts >>= displayGraph "" opts . getMaybeLib . intState
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey putIfVerbose opts 3 $ "Options: " ++ show opts
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey mapM_ (processFile opts) (infiles opts)
ef28ad515cc0858ccbfba09e17a844052ed79356Tom RumseyprocessFile :: HetcatsOpts -> FilePath -> IO ()
ef28ad515cc0858ccbfba09e17a844052ed79356Tom RumseyprocessFile opts file = do
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey putIfVerbose opts 3 ("Processing input: " ++ file)
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey res <- case guess file (intype opts) of
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey#ifdef PROGRAMATICA
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey HaskellIn -> anaHaskellFile opts file
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey#ifndef NOOWLLOGIC
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey OWLIn -> parseOWL file >>= structureAna file opts
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey#ifdef HXTFILTER
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey OmdocIn -> mLibEnvFromOMDocFile opts file
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey PrfIn -> anaLibReadPrfs opts file
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey ProofCommand -> do
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey st <- cmdlProcessFile opts file
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey return . getMaybeLib $ intState st
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey MaudeIn -> anaMaudeFile opts file
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey TwelfIn -> anaTwelfFile opts file
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey _ -> anaLib opts file
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey Just (ln, nEnv) -> writeSpecFiles opts file nEnv ln $ lookupDGraph ln nEnv
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert Wapshott _ -> return ()
d244c4a5c5ef6a408d1b44b95810a05368f33aaeRobert Wapshott displayGraph file opts res
ef28ad515cc0858ccbfba09e17a844052ed79356Tom RumseydisplayGraph :: FilePath -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey#ifdef UNI_PACKAGE
ef28ad515cc0858ccbfba09e17a844052ed79356Tom RumseydisplayGraph file opts res = case guiType opts of
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey NoGui -> return ()
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey UseGui -> showGraph file opts res
ef28ad515cc0858ccbfba09e17a844052ed79356Tom RumseydisplayGraph _ opts _ = when (guiType opts == UseGui)
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey $ fail $ "No graph display interface; \n"
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey ++ "UNI_PACKAGE option has been "
ef28ad515cc0858ccbfba09e17a844052ed79356Tom Rumsey ++ "disabled during compilation of Hets"