hets.hs revision 8a77240a809197c92c0736c431b4b88947a7bac1
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{-# LANGUAGE CPP #-}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright : (c) Uni Bremen 2003-2005
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMaintainer : Christian.Maeder@dfki.de
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannStability : provisional
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannPortability : non-portable (imports Logic.Logic)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannThe Main module of the Heterogeneous Tool Set.
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann It provides the main function to call (and not much more).
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- for interactice purposes use Test.hs
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannmodule Main where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann#ifndef NOOWLLOGIC
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann#ifdef UNI_PACKAGE
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann#ifdef PROGRAMATICA
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport PGIP.XMLstate (isRemote)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Maude.Maude2DG (anaMaudeFile)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport LF.Twelf2DG (anaTwelfFile)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport OMDoc.Import (anaOMDocFile)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann getArgs >>= hetcatsOpts >>= \ opts ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann if isRemote opts || interactive opts
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann then cmdlRun opts >>= displayGraph "" opts . getMaybeLib . intState
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann putIfVerbose opts 3 $ "Options: " ++ show opts
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann mapM_ (processFile opts) (infiles opts)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprocessFile :: HetcatsOpts -> FilePath -> IO ()
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannprocessFile opts file = do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann putIfVerbose opts 3 ("Processing input: " ++ file)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann res <- case guess file (intype opts) of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann#ifdef PROGRAMATICA
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann HaskellIn -> anaHaskellFile opts file
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann#ifndef NOOWLLOGIC
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann OWLIn -> parseOWL file >>= structureAna file opts
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann PrfIn -> anaLibReadPrfs opts file
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ProofCommand -> do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann st <- cmdlProcessFile opts file
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return . getMaybeLib $ intState st
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann MaudeIn -> anaMaudeFile opts file
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann TwelfIn -> anaTwelfFile opts file
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann OmdocIn -> anaOMDocFile opts file
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann CommonLogicIn -> anaLibExt (opts { defLogic = "CommonLogic" }) file
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann emptyLibEnv emptyDG
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> anaLib opts file
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just (ln, nEnv) ->
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann writeSpecFiles opts file nEnv ln $ lookupDGraph ln nEnv
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> return ()
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann displayGraph file opts res
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanndisplayGraph :: FilePath -> HetcatsOpts -> Maybe (LibName, LibEnv) -> IO ()
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann#ifdef UNI_PACKAGE
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanndisplayGraph file opts res = case guiType opts of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann NoGui -> return ()
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann UseGui -> showGraph file opts res
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanndisplayGraph _ opts _ = when (guiType opts == UseGui)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann $ fail $ "No graph display interface; \n"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "UNI_PACKAGE option has been "
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ++ "disabled during compilation of Hets"