2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder{-# LANGUAGE CPP #-}
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederCopyright : (c) Uni Bremen 2003-2005
54ed6a6b1a6c7d27fadb39ec5b59d0806c81f7c8Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiStability : provisional
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiPortability : non-portable (imports Logic.Logic)
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederThe Main module of the Heterogeneous Tool Set.
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder It provides the main function to call (and not much more).
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder-- for interactice purposes use Test.hs
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedermodule Main where
91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maederimport Driver.ReadFn (showFileType)
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder#ifdef UNI_PACKAGE
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder#ifdef PROGRAMATICA
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroederimport CMDL.Interface (cmdlRunShell)
834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Grossimport PGIP.XMLstate (isRemote)
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühlimport Maude.Maude2DG (anaMaudeFile)
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakovaimport LF.Twelf2DG (anaTwelfFile)
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulzimport OMDoc.Import (anaOMDocFile)
14c89b2d830777bf4db2850f038c9f60acaca486Christian Maederimport HolLight.HolLight2DG (anaHolLightFile)
9175e29c044318498a40f323f189f9dfd50378efChristian Maederimport Isabelle.Isa2DG (anaIsaFile, anaThyFile)
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder getArgs >>= hetcatsOpts >>= \ opts -> let imode = interactive opts in
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa printOptionsWarnings opts >>
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder if serve opts then hetsServer opts else
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder if isRemote opts || imode
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross then cmdlRun opts >>= displayGraph "" opts . getMaybeLib . intState
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder putIfVerbose opts 3 $ "Options: " ++ show opts
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski if outputLogicList opts
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski then printLogics
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski case (infiles opts, outputLogicGraph opts) of
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder ([], lg) -> case guiType opts of
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder#ifdef UNI_PACKAGE
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder NoGui | lg -> writeLG opts
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder _ -> hetsIOError "supply option -G or -g and/or file arguments"
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder (fs, False) -> mapM_ (processFile opts) fs
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder _ -> hetsIOError
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder "option -G is illegal together with file arguments (use -g)"
9175e29c044318498a40f323f189f9dfd50378efChristian MaedernoUniPkg :: IO ()
9175e29c044318498a40f323f189f9dfd50378efChristian MaedernoUniPkg = fail $ "No graph display interface; \n"
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder ++ "UNI_PACKAGE option has been "
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder ++ "disabled during compilation of Hets"
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin KühlprocessFile :: HetcatsOpts -> FilePath -> IO ()
f63e7684d8db7503c22e5d8d499c94a9405f8f9eChristian MaederprocessFile opts file =
91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder if fileType opts then showFileType opts file else do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder putIfVerbose opts 3 ("Processing input: " ++ file)
f63e7684d8db7503c22e5d8d499c94a9405f8f9eChristian Maeder let doExit = guiType opts == UseGui
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder res <- case guess file (intype opts) of
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder#ifdef PROGRAMATICA
bdc103981a28a51938de98a956d8a3767f6cf43dAivaras Jakubauskas HaskellIn -> putStr "this is HaskellIn" >> anaHaskellFile opts file
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder HolLightIn -> anaHolLightFile opts file
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder IsaIn -> anaIsaFile opts file
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder ThyIn -> anaThyFile opts file
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder PrfIn -> anaLibReadPrfs opts file
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ProofCommand -> do
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder st <- cmdlProcessFile doExit opts file
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder liftM (getMaybeLib . intState)
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder $ (if interactive opts then cmdlRunShell else return) st
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl MaudeIn -> anaMaudeFile opts file
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova TwelfIn -> anaTwelfFile opts file
72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulz OmdocIn -> anaOMDocFile opts file
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder _ -> anaLib opts file
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder Just (ln, nEnv) ->
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder writeSpecFiles opts file nEnv ln $ lookupDGraph ln nEnv
1c4dfa148603d4fcf4cdd2ed66c8b6e1de0dd696Till Mossakowski _ -> hetsIOError ""
bb63f684c4f5f33ffcd1dcc02c58d6a703900fafJonathan von Schroeder if guess file (intype opts) /= ProofCommand && interactive opts
b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder then cmdlRun opts >> return ()
b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder else displayGraph file opts res
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus GrossdisplayGraph :: FilePath -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
d56ece59c372cb887355825901222b9f3377f7e6Thiemo WiedemeyerdisplayGraph file opts res = case guiType opts of
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer NoGui -> return ()
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder#ifdef UNI_PACKAGE
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder showGraph file opts res