{-# LANGUAGE TemplateHaskell, DeriveDataTypeable, DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts, NamedFieldPuns, BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
-- |
-- Copyright : (c) 2010, 2011 Benedikt Schmidt & Simon Meier
-- License : GPL v3 (see LICENSE)
--
-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>
--
-- AC-unification of DH terms using Maude as a backend.
module Term.Maude.Process (
-- * Handle to a maude process
MaudeHandle(..)
, startMaude
, getMaudeStats
-- * Unification using Maude
, unifyViaMaude
-- * Matching using Maude
, matchViaMaude
-- * Normalization using Maude
, normViaMaude
-- * Managing the persistent Maude process
, 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
-- Unification using a persistent Maude process
-----------------------------------------------------------------------
-- | A handle to a Maude process. It requires the Maude path for Signatures to
-- be serializable. If we also add the string for the Maude config file, then
-- it would even be serializable on its own.
data MaudeHandle = MaudeHandle { mhFilePath :: FilePath
, mhMaudeSig :: MaudeSig
, mhProc :: MVar MaudeProcess }
-- | @getMaudeStats@ returns the maude stats formatted as a string.
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@ starts a new instance of Maude and returns a Handle to it.
startMaude :: FilePath -> MaudeSig -> IO MaudeHandle
startMaude maudePath maudeSig = do
mv <- newMVar =<< startMaudeProcess maudePath maudeSig
-- Add a finalizer to the MVar that stops maude.
addMVarFinalizer mv $ withMVar mv $ \mp -> do
terminateProcess (mProc mp) <* waitForProcess (mProc mp)
-- return the maude handle
return (MaudeHandle maudePath maudeSig mv)
-- | Start a Maude process.
startMaudeProcess :: FilePath -- ^ Path to Maude
-> MaudeSig
-> IO (MaudeProcess)
startMaudeProcess maudePath maudeSig = do
(hin,hout,herr,hproc) <- runInteractiveCommand maudeCmd
_ <- getToDelim hout
-- set maude flags
mapM_ (executeMaudeCommand hin hout) setupCmds
-- input the maude theory
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"
-- | Restart the Maude process on this handle.
restartMaude :: MaudeHandle -> IO ()
restartMaude (MaudeHandle maudePath maudeSig mv) = modifyMVar_ mv $ \mp -> do
terminateProcess (mProc mp) <* waitForProcess (mProc mp)
startMaudeProcess maudePath maudeSig
-- | @getToDelim ih@ reads input from @ih@ until the Maude delimitier is encountered.
-- It returns the 'ByteString' up to (not including) the delimiter.
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 cmd@ sends the command @cmd@ to Maude and returns Maude's
-- output up to the next prompt sign.
callMaude :: MaudeHandle
-> (MaudeProcess -> MaudeProcess) -- ^ Statistics updater.
-> ByteString -> IO ByteString
callMaude hnd updateStatistics cmd = do
-- Ensure that the command is fully evaluated and therefore does not depend
-- on another call to Maude anymore. Otherwise, we could end up in a
-- deadlock.
evaluate (rnf cmd)
-- If there was an exception, then we might be out of sync with the current
-- persistent Maude process: restart the process.
(`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)
-- | Compute a result via Maude.
computeViaMaude ::
(Show a, Show b, Ord c)
=> MaudeHandle
-> (MaudeProcess -> MaudeProcess) -- ^ Update statistics
-> (a -> BindT (Lit c LVar) MaudeLit Fresh ByteString) -- ^ Conversion to Maude command
-> (M.Map MaudeLit (Lit c LVar) -> ByteString -> Either String b) -- ^ Conversion from Maude reply
-> 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++"'"
------------------------------------------------------------------------------
-- Unification modulo AC
------------------------------------------------------------------------------
-- | @unifyCmd eqs@ returns the Maude command to solve the unification problem @eqs@.
-- Expects a nonempty list of equations
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 hnd eqs@ computes all AC unifiers of @eqs@ using the
-- Maude process @hnd@.
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 }
------------------------------------------------------------------------------
-- Matching modulo AC
------------------------------------------------------------------------------
-- | @matchCmd p t@ returns the Maude command to match the terms @t@ to the
-- pattern @p@.
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 (t, p)@ computes a complete set of AC matchers of the term
-- @t@ to the pattern @p@ via Maude.
matchViaMaude :: (IsConst c , Show (Lit c LVar), Ord c)
=> MaudeHandle
-> (c -> LSort)
-> [Match (VTerm c LVar)]
-> IO [Subst c LVar]
matchViaMaude _ _ [] = return [emptySubst]
matchViaMaude hnd sortOf matcheqs =
computeViaMaude hnd incMatchCount toMaude fromMaude eqs
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 }
eqs = [Equal t p | MatchWith t p <- matcheqs ]
------------------------------------------------------------------------------
-- Normalization of terms
------------------------------------------------------------------------------
-- | @normCmd t@ returns the Maude command to normalize the term @t@
-- pattern @p@.
normCmd :: MTerm -> ByteString
normCmd tm = "reduce " <> ppMaude tm <> " .\n"
-- | @normViaMaude t@ normalizes the term t via Maude.
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 }
-- Passing the Handle to Maude via a Reader monad
-------------------------------------------------
-- | Values that depend on a 'MaudeHandle'.
type WithMaude = Reader MaudeHandle