2665d7759e63acff0bcd4135678f2cc6f2041d46Christian Maeder{- |

934473566cf3a8e4044ed10e408b4c44079684b1Christian Maeder a.jakubauskas@jacobs-university.de

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder A wrapper/interface for MMT

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder-}

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maedermodule MMT.Hets2mmt (

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu mmtRes

934473566cf3a8e4044ed10e408b4c44079684b1Christian Maeder )

1d581e55c7ec020a445684310394c3a5fc056e96Christian Maeder where

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maederimport System.Process

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederimport GHC.IO.Handle

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederimport Common.Result

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Common.Id

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Static.DevGraph

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Common.LibName

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Framework.Analysis(addLogic2LogicList)

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport System.FilePath

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Common.Utils

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskijar :: String

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskijar = "hets-mmt-standalone.jar"

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskistaloneclass :: String

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskistaloneclass = "com.simontuffs.onejar.Boot"

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskicalljar :: FilePath -> IO (String, Maybe String)

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowskicalljar fileName = do

7ff59aa438d7a210789cad2c2c745bc9967eff82Till Mossakowski (_, Just hout, maybeErr, _) <- createProcess (

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski proc "java" ["-cp",

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski jar,

1d581e55c7ec020a445684310394c3a5fc056e96Christian Maeder staloneclass,

bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski "-newLogic",

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski fileName])

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski { std_out = CreatePipe }

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski cont <- hGetContents hout

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski case maybeErr of

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (Just hErr) -> do

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski err <- hGetContents hErr

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder putStr err

ebe4d5a8e51f6009d6e7ca465f5963ce46a07fd2Christian Maeder return (cont, Just err)

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder Nothing -> return (cont, Nothing)

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder

6a00a2b0961b1553d4f5106d655f6f90bb6c1777Christian MaedercallMMT :: FilePath -> IO [Diagnosis]

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescucallMMT fp = do

342beb91d58bcf41178240c37d0f6c0c4f83c53eMihai Codescu (out, maybeErr) <- calljar fp

aa4679922a8363b4e494079f53aaf4f64554aae0Christian Maeder case maybeErr of

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (Just err) -> return [Diag Warning out nullRange,

2add146602f6eb47058b67142bd91ae40a32fd66Christian Maeder Diag Error err nullRange]

2add146602f6eb47058b67142bd91ae40a32fd66Christian Maeder Nothing -> return [Diag Warning out nullRange]

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski

934473566cf3a8e4044ed10e408b4c44079684b1Christian MaedermmtRes :: FilePath -> IO (Result (LibName, LibEnv))

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskimmtRes fname = do

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder libDir <- getEnvDef "HETS_LIB" ""

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder putStr $ "HETS_LIB at " ++ libDir

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder putStr $ "calling MMT on " ++ libDir ++ fname

cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder dgs <- callMMT (libDir </> fname)

96f0ef61a405144ff30a9d77963881dc32113750Klaus Luettich putStr $ show dgs

f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski addLogic2LogicList $ dropExtension fname

18a4d5cb6828f080db9c5f9551785c5151027271Christian Maeder return (emptyRes (dropExtension fname) dgs)

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski

6d9f68d2b5fafea0b5e0fc59a1d557174e032c02Christian MaederemptyRes :: String -> [Diagnosis] -> Result (LibName, LibEnv)

b565cd55a13dbccc4e66c344316da525c961e4caTill MossakowskiemptyRes lname = (`Result` Just (emptyLibName lname, emptyLibEnv))

b4e40b91734dc997c7edbe5676d0408e49f65f0bChristian Maeder