hets.hs revision 005e0f0c6b0cc898003b03801158c208f3071fc5
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# LANGUAGE CPP #-}
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Uni Bremen 2003-2005
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Christian.Maeder@dfki.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : non-portable (imports Logic.Logic)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederThe Main module of the Heterogeneous Tool Set.
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder It provides the main function to call (and not much more).
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder-- for interactice purposes use Test.hs
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedermodule Main where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder#ifndef NOOWLLOGIC
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder#ifdef UNI_PACKAGE
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder#ifdef PROGRAMATICA
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport PGIP.XMLstate (isRemote)
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maederimport Maude.Maude2DG (anaMaudeFile)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederimport LF.Twelf2DG (anaTwelfFile)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederimport OMDoc.Import (anaOMDocFile)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder getArgs >>= hetcatsOpts >>= \ opts ->
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder if isRemote opts || interactive opts
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder then cmdlRun opts >>= displayGraph "" opts . getMaybeLib . intState
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder putIfVerbose opts 3 $ "Options: " ++ show opts
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder mapM_ (processFile opts) (infiles opts)
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederprocessFile :: HetcatsOpts -> FilePath -> IO ()
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian MaederprocessFile opts file = do
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder putIfVerbose opts 3 ("Processing input: " ++ file)
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder res <- case guess file (intype opts) of
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder#ifdef PROGRAMATICA
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder HaskellIn -> anaHaskellFile opts file
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder#ifndef NOOWLLOGIC
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maeder OWLIn -> parseOWL file >>= structureAna file opts
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder PrfIn -> anaLibReadPrfs opts file
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder ProofCommand -> do
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder st <- cmdlProcessFile opts file
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder return . getMaybeLib $ intState st
498aa48bdb931ab50990d3b74318a5db2312186cChristian Maeder MaudeIn -> anaMaudeFile opts file
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder TwelfIn -> anaTwelfFile opts file
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder OmdocIn -> anaOMDocFile opts file
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder CommonLogicIn -> anaLibExt (opts { defLogic = "CommonLogic" }) file
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder emptyLibEnv emptyDG
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder _ -> anaLib opts file
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Just (ln, nEnv) ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeSpecFiles opts file nEnv ln $ lookupDGraph ln nEnv
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder _ -> return ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder displayGraph file opts res
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederdisplayGraph :: FilePath -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder#ifdef UNI_PACKAGE
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederdisplayGraph file opts res = case guiType opts of
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder NoGui -> return ()
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder UseGui -> showGraph file opts res
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederdisplayGraph _ opts _ = when (guiType opts == UseGui)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $ fail $ "No graph display interface; \n"
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder ++ "UNI_PACKAGE option has been "
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder ++ "disabled during compilation of Hets"