{-# LANGUAGE CPP #-}

module Driver.ReadMain where


import Control.Monad

import Common.LibName

import Interfaces.DataTypes


import CMDL.ProcessScript
import CMDL.Interface (cmdlRunShell)
import CMDL.DataTypes

import Driver.AnaLib
import Driver.Options

import Static.DevGraph


import Maude.Maude2DG (anaMaudeFile)
import LF.Twelf2DG (anaTwelfFile)
import OMDoc.Import (anaOMDocFile)
#ifdef HEXPAT
import HolLight.HolLight2DG (anaHolLightFile)
#endif

#ifdef HAXML
import Isabelle.Isa2DG (anaIsaFile, anaThyFile)
#endif

readAndAnalyse :: FilePath -> HetcatsOpts -> IO (Maybe (LibName, LibEnv))
readAndAnalyse :: FilePath -> HetcatsOpts -> IO (Maybe (LibName, LibEnv))
readAndAnalyse file :: FilePath
file opts :: HetcatsOpts
opts = 
    let doExit :: Bool
doExit = HetcatsOpts -> GuiType
guiType HetcatsOpts
opts GuiType -> GuiType -> Bool
forall a. Eq a => a -> a -> Bool
== GuiType
UseGui in case FilePath -> InType -> InType
guess FilePath
file (HetcatsOpts -> InType
intype HetcatsOpts
opts) of
#ifdef PROGRAMATICA
      HaskellIn -> putStr "this is HaskellIn" >> anaHaskellFile opts file
#endif
#ifdef HEXPAT
      HolLightIn -> HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaHolLightFile HetcatsOpts
opts FilePath
file
#endif
#ifdef HAXML
      IsaIn -> HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaIsaFile HetcatsOpts
opts FilePath
file
      ThyIn -> HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaThyFile HetcatsOpts
opts FilePath
file
#endif
      PrfIn -> HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaLibReadPrfs HetcatsOpts
opts FilePath
file
      ProofCommand -> do 
        CmdlState
st <- Bool -> HetcatsOpts -> FilePath -> IO CmdlState
cmdlProcessFile Bool
doExit HetcatsOpts
opts FilePath
file
        (CmdlState -> Maybe (LibName, LibEnv))
-> IO CmdlState -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (IntState -> Maybe (LibName, LibEnv)
getMaybeLib (IntState -> Maybe (LibName, LibEnv))
-> (CmdlState -> IntState) -> CmdlState -> Maybe (LibName, LibEnv)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlState -> IntState
intState)
          (IO CmdlState -> IO (Maybe (LibName, LibEnv)))
-> IO CmdlState -> IO (Maybe (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ (if HetcatsOpts -> Bool
interactive HetcatsOpts
opts then CmdlState -> IO CmdlState
cmdlRunShell else CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return) CmdlState
st
      MaudeIn -> HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaMaudeFile HetcatsOpts
opts FilePath
file
      TwelfIn -> HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaTwelfFile HetcatsOpts
opts FilePath
file
      OmdocIn -> HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaOMDocFile HetcatsOpts
opts FilePath
file
      _ -> HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaLib HetcatsOpts
opts FilePath
file