{- |
Module      :  ./MMT/Hets2mmt.hs
Description :  interface for MMT jar
Copyright   :
License     :
Maintainer  :  a.jakubauskas@jacobs-university.de
Stability   :  experimental
Portability :
-}
module MMT.Hets2mmt (
    mmtRes,
    callSpec
    )
    where

import System.Process
import System.IO
import Common.Result
import Common.Id
import Static.DevGraph
import Common.LibName
import Framework.Analysis (addLogic2LogicList)
import System.FilePath
import Common.Utils
-- import MMT.XMLtoPT

{- import System.IO.Unsafe
import Text.ParserCombinators.Parsec -}

jar :: String
jar :: String
jar = "hets-mmt-standalone.jar"

staloneclass :: String
staloneclass :: String
staloneclass = "com.simontuffs.onejar.Boot"

calljar :: FilePath -> IO (String, Maybe String)
calljar :: String -> IO (String, Maybe String)
calljar fileName :: String
fileName = do
  (_, Just hout :: Handle
hout, maybeErr :: Maybe Handle
maybeErr, _) <- CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess (
              String -> [String] -> CreateProcess
proc "java" ["-cp",
                           String
jar,
                           String
staloneclass,
                           "-newLogic",
                           String
fileName])
              { std_out :: StdStream
std_out = StdStream
CreatePipe }
  String
cont <- Handle -> IO String
hGetContents Handle
hout
  case Maybe Handle
maybeErr of
    (Just hErr :: Handle
hErr) -> do
            String
err <- Handle -> IO String
hGetContents Handle
hErr
            String -> IO ()
putStr String
err
            (String, Maybe String) -> IO (String, Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
cont, String -> Maybe String
forall a. a -> Maybe a
Just String
err)
    Nothing -> (String, Maybe String) -> IO (String, Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
cont, Maybe String
forall a. Maybe a
Nothing)

callSpec :: FilePath -> IO (String, Maybe String)
callSpec :: String -> IO (String, Maybe String)
callSpec fileName :: String
fileName = do
  String -> IO ()
putStr "creating process\n"
  (_, Just hout :: Handle
hout, maybeErr :: Maybe Handle
maybeErr, _) <- CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess (
              String -> [String] -> CreateProcess
proc "java" ["-cp",
                           String
jar,
                           String
staloneclass,
                           "-readSpec",
                           String
fileName])
              { std_out :: StdStream
std_out = StdStream
CreatePipe }
  String
cont <- Handle -> IO String
hGetContents Handle
hout
  -- putStr cont
  case Maybe Handle
maybeErr of
    (Just hErr :: Handle
hErr) -> do
            String
err <- Handle -> IO String
hGetContents Handle
hErr
            String -> IO ()
putStr String
err
            (String, Maybe String) -> IO (String, Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
cont, String -> Maybe String
forall a. a -> Maybe a
Just String
err)
    Nothing -> (String, Maybe String) -> IO (String, Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
cont, Maybe String
forall a. Maybe a
Nothing)

callMMT :: FilePath -> IO [Diagnosis]
callMMT :: String -> IO [Diagnosis]
callMMT fp :: String
fp = do
    (out :: String
out, maybeErr :: Maybe String
maybeErr) <- String -> IO (String, Maybe String)
calljar String
fp
    case Maybe String
maybeErr of
      (Just err :: String
err) -> [Diagnosis] -> IO [Diagnosis]
forall (m :: * -> *) a. Monad m => a -> m a
return [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning String
out Range
nullRange,
                            DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error String
err Range
nullRange]
      Nothing -> [Diagnosis] -> IO [Diagnosis]
forall (m :: * -> *) a. Monad m => a -> m a
return [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning String
out Range
nullRange]

mmtRes :: FilePath -> IO (Result (LibName, LibEnv))
mmtRes :: String -> IO (Result (LibName, LibEnv))
mmtRes fname :: String
fname = do
          String
libDir <- String -> String -> IO String
getEnvDef "HETS_LIB" ""
          String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "HETS_LIB at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
libDir
          String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "calling MMT on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
libDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fname
          [Diagnosis]
dgs <- String -> IO [Diagnosis]
callMMT (String
libDir String -> String -> String
</> String
fname)
          String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> String
forall a. Show a => a -> String
show [Diagnosis]
dgs
          String -> IO ()
addLogic2LogicList (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String
dropExtension String
fname
          Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> [Diagnosis] -> Result (LibName, LibEnv)
emptyRes (String -> String
dropExtension String
fname) [Diagnosis]
dgs)

emptyRes :: String -> [Diagnosis] -> Result (LibName, LibEnv)
emptyRes :: String -> [Diagnosis] -> Result (LibName, LibEnv)
emptyRes lname :: String
lname = ([Diagnosis] -> Maybe (LibName, LibEnv) -> Result (LibName, LibEnv)
forall a. [Diagnosis] -> Maybe a -> Result a
`Result` (LibName, LibEnv) -> Maybe (LibName, LibEnv)
forall a. a -> Maybe a
Just (String -> LibName
emptyLibName String
lname, LibEnv
emptyLibEnv))