hets.hs revision 57026bc09337d158b89775048a9bcc9c17d825ca
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose{-# LANGUAGE CPP #-}
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseModule : $Id$
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseCopyright : (c) Uni Bremen 2003-2005
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseLicense : GPLv2 or higher, see LICENSE.txt
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseMaintainer : Christian.Maeder@dfki.de
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseStability : provisional
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosePortability : non-portable (imports Logic.Logic)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseThe Main module of the Heterogeneous Tool Set.
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose It provides the main function to call (and not much more).
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- for interactice purposes use Test.hs
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bosemodule Main where
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport System.Environment (getArgs)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose#ifdef UNI_PACKAGE
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport Control.Monad ( when )
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose#ifdef PROGRAMATICA
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport PGIP.XMLstate (isRemote)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose#ifdef SERVER
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport Maude.Maude2DG (anaMaudeFile)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport LF.Twelf2DG (anaTwelfFile)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport OMDoc.Import (anaOMDocFile)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose#ifdef HEXPAT
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport HolLight.HolLight2DG (anaHolLightFile)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport Isabelle.Isa2DG (anaIsaFile)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bosemain :: IO ()
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose getArgs >>= hetcatsOpts >>= \ opts ->
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose#ifdef SERVER
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose if serve opts then hetsServer opts else
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose if isRemote opts || interactive opts
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose then cmdlRun opts >>= displayGraph "" opts . getMaybeLib . intState
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose putIfVerbose opts 3 $ "Options: " ++ show opts
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose mapM_ (processFile opts) (infiles opts)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseprocessFile :: HetcatsOpts -> FilePath -> IO ()
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseprocessFile opts file = do
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose putIfVerbose opts 3 ("Processing input: " ++ file)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose res <- case guess file (intype opts) of
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose#ifdef PROGRAMATICA
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose HaskellIn -> anaHaskellFile opts file
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose#ifdef HEXPAT
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose HolLightIn -> anaHolLightFile opts file
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose IsaIn -> anaIsaFile opts file
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose PrfIn -> anaLibReadPrfs opts file
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose ProofCommand -> do
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose st <- cmdlProcessFile opts file
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return . getMaybeLib $ intState st
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose MaudeIn -> anaMaudeFile opts file
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose TwelfIn -> anaTwelfFile opts file
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose OmdocIn -> anaOMDocFile opts file
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose DgXml | not (defLogicIsDMU opts) -> readDGXml opts file
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose _ -> anaLib opts file
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose Just (ln, nEnv) ->
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose writeSpecFiles opts file nEnv ln $ lookupDGraph ln nEnv
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose _ -> return ()
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose displayGraph file opts res
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosedisplayGraph :: FilePath -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose#ifdef UNI_PACKAGE
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosedisplayGraph file opts res = case guiType opts of
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose NoGui -> return ()
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose UseGui -> showGraph file opts res
885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosedisplayGraph _ opts _ = when (guiType opts == UseGui)
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose $ fail $ "No graph display interface; \n"
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose ++ "UNI_PACKAGE option has been "
885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose ++ "disabled during compilation of Hets"