module Term.Maude.Process (
MaudeHandle(..)
, startMaude
, getMaudeStats
, unifyViaMaude
, matchViaMaude
, normViaMaude
, WithMaude
) where
import Data.Traversable hiding ( mapM )
import qualified Data.Map as M
import Term.Term
import Term.LTerm
import Term.Rewriting.Definitions
import Term.Maude.Signature
import Term.Maude.Types
import Term.Maude.Parser
import Term.Substitution
import Control.Applicative
import Control.Monad.Reader
import Control.Monad.Fresh
import Control.Concurrent
import Control.Exception (onException, evaluate)
import Control.DeepSeq (rnf)
import Control.Monad.Bind
import qualified Data.ByteString as B
import Data.ByteString (ByteString)
import qualified Data.ByteString.Char8 as BC
import System.Process
import System.IO
import Utils.Misc
import Extension.Data.Monoid
data MaudeHandle = MaudeHandle { mhFilePath :: FilePath
, mhMaudeSig :: MaudeSig
, mhProc :: MVar MaudeProcess }
getMaudeStats :: MaudeHandle -> IO String
getMaudeStats (MaudeHandle {mhProc = maude}) =
withMVar maude $ \mp -> do
let mc = matchCount mp
uc = unifCount mp
return $ "Maude has been called "++show (mc+uc)++ " times ("
++show uc++" unifications and "++show mc++" matchings)."
data MaudeProcess = MP {
mIn :: !Handle
, mOut :: !Handle
, _mErr :: !Handle
, mProc :: !ProcessHandle
, unifCount :: !Int
, matchCount :: !Int
, normCount :: !Int
}
startMaude :: FilePath -> MaudeSig -> IO MaudeHandle
startMaude maudePath maudeSig = do
mv <- newMVar =<< startMaudeProcess maudePath maudeSig
addMVarFinalizer mv $ withMVar mv $ \mp -> do
terminateProcess (mProc mp) <* waitForProcess (mProc mp)
return (MaudeHandle maudePath maudeSig mv)
startMaudeProcess :: FilePath
-> MaudeSig
-> IO (MaudeProcess)
startMaudeProcess maudePath maudeSig = do
(hin,hout,herr,hproc) <- runInteractiveCommand maudeCmd
_ <- getToDelim hout
mapM_ (executeMaudeCommand hin hout) setupCmds
executeMaudeCommand hin hout (ppTheory maudeSig)
return (MP hin hout herr hproc 0 0 0)
where
maudeCmd
| dEBUGMAUDE = "sh -c \"tee /tmp/maude.input | "
++ maudePath ++ " -no-tecla -no-banner -no-wrap -batch "
++ "\" | tee /tmp/maude.output"
| otherwise =
maudePath ++ " -no-tecla -no-banner -no-wrap -batch "
executeMaudeCommand hin hout cmd =
B.hPutStr hin cmd >> hFlush hin >> getToDelim hout >> return ()
setupCmds = [ "set show command off .\n"
, "set show timing off .\n"
, "set show stats off .\n" ]
dEBUGMAUDE = envIsSet "DEBUG_MAUDE"
restartMaude :: MaudeHandle -> IO ()
restartMaude (MaudeHandle maudePath maudeSig mv) = modifyMVar_ mv $ \mp -> do
terminateProcess (mProc mp) <* waitForProcess (mProc mp)
startMaudeProcess maudePath maudeSig
getToDelim :: Handle -> IO ByteString
getToDelim ih =
go BC.empty
where
go !acc = do
bs <- BC.append acc <$> B.hGetSome ih 8096
case BC.breakSubstring mDelim bs of
(before, after) | after == mDelim -> return before
(_, after) | after == "" -> go bs
_ -> error $ "Too much maude output" ++ BC.unpack bs
mDelim = "Maude> "
callMaude :: MaudeHandle
-> (MaudeProcess -> MaudeProcess)
-> ByteString -> IO ByteString
callMaude hnd updateStatistics cmd = do
evaluate (rnf cmd)
(`onException` restartMaude hnd) $ modifyMVar (mhProc hnd) $ \mp -> do
let inp = mIn mp
out = mOut mp
B.hPut inp cmd
hFlush inp
mp' <- evaluate (updateStatistics mp)
res <- getToDelim out
return (mp', res)
computeViaMaude ::
(Show a, Show b, Ord c)
=> MaudeHandle
-> (MaudeProcess -> MaudeProcess)
-> (a -> BindT (Lit c LVar) MaudeLit Fresh ByteString)
-> (M.Map MaudeLit (Lit c LVar) -> ByteString -> Either String b)
-> a
-> IO b
computeViaMaude hnd updateStats toMaude fromMaude inp = do
let (cmd, bindings) = runConversion $ toMaude inp
reply <- callMaude hnd updateStats cmd
case fromMaude bindings reply of
Right res -> return res
Left e -> fail $ "\ncomputeViaMaude:\nParse error: `" ++ e ++"'"++
"\nFor Maude Output: `" ++ BC.unpack reply ++"'"++
"\nFor query: `" ++ BC.unpack cmd++"'"
unifyCmd :: [Equal MTerm] -> ByteString
unifyCmd [] = error "unifyCmd: cannot create cmd for empty list of equations."
unifyCmd eqs =
"unify in MSG : " <> seqs <> " .\n"
where
ppEq (Equal t1 t2) = ppMaude t1 <> " =? " <> ppMaude t2
seqs = B.intercalate " /\\ " $ map ppEq eqs
unifyViaMaude
:: (IsConst c , Show (Lit c LVar), Ord c)
=> MaudeHandle
-> (c -> LSort) -> [Equal (VTerm c LVar)] -> IO [SubstVFresh c LVar]
unifyViaMaude _ _ [] = return [emptySubstVFresh]
unifyViaMaude hnd sortOf eqs =
computeViaMaude hnd incUnifCount toMaude fromMaude eqs
where
msig = mhMaudeSig hnd
toMaude = fmap unifyCmd . mapM (traverse (lTermToMTerm sortOf))
fromMaude bindings reply =
map (msubstToLSubstVFresh bindings) <$> parseUnifyReply msig reply
incUnifCount mp = mp { unifCount = 1 + unifCount mp }
matchCmd :: [Equal MTerm] -> ByteString
matchCmd eqs =
"match in MSG : " <> ppTerms t2s <> " <=? " <> ppTerms t1s <> " .\n"
where
(t1s,t2s) = unzip [ (a,b) | Equal a b <- eqs ]
ppTerms = ppMaude . fAppList
matchViaMaude :: (IsConst c , Show (Lit c LVar), Ord c)
=> MaudeHandle
-> (c -> LSort)
-> Match (VTerm c LVar)
-> IO [Subst c LVar]
matchViaMaude hnd sortOf matchProblem =
case flattenMatch matchProblem of
Nothing -> return []
Just [] -> return [emptySubst]
Just ms -> computeViaMaude hnd incMatchCount toMaude fromMaude
(uncurry Equal <$> ms)
where
msig = mhMaudeSig hnd
toMaude = fmap matchCmd . mapM (traverse (lTermToMTerm sortOf))
fromMaude bindings reply =
map (msubstToLSubstVFree bindings) <$> parseMatchReply msig reply
incMatchCount mp = mp { matchCount = 1 + matchCount mp }
normCmd :: MTerm -> ByteString
normCmd tm = "reduce " <> ppMaude tm <> " .\n"
normViaMaude :: (IsConst c , Show (Lit c LVar), Ord c)
=> MaudeHandle
-> (c -> LSort)
-> VTerm c LVar
-> IO (VTerm c LVar)
normViaMaude hnd sortOf t =
computeViaMaude hnd incNormCount toMaude fromMaude t
where
msig = mhMaudeSig hnd
toMaude = fmap normCmd . (lTermToMTerm sortOf)
fromMaude bindings reply =
(\mt -> (mTermToLNTerm "z" mt `evalBindT` bindings) `evalFresh` nothingUsed)
<$> parseReduceReply msig reply
incNormCount mp = mp { normCount = 1 + normCount mp }
type WithMaude = Reader MaudeHandle