diff --git a/Foreign/Maude.hs b/Foreign/Maude.hs deleted file mode 100644 --- a/Foreign/Maude.hs +++ /dev/null @@ -1,198 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} ------------------------------------------------------------------------------ --- | --- Module : Foreign.Maude --- Copyright : (c) David Lazar, 2011 --- License : MIT --- --- Maintainer : lazar6@illinois.edu --- Stability : experimental --- Portability : unknown --- --- This package provides a simple interface (via the 'rewrite' functions) --- for doing Maude rewrites from within Haskell. The following steps are --- performed every time the 'rewrite' functions are executed: --- --- 1. A temporary file is created that contains the necessary commands. --- --- 2. The temporary file (with any other input files) is executed by Maude. --- --- 3. The temporary file is removed. --- --- 4. The output from step 2 is parsed and returned. --- --- This is a simple way to perform a single rewrite command, but it is --- inefficient for performing many rewrite commands. See /Future Work/ --- below. ------------------------------------------------------------------------------ - -module Foreign.Maude - ( - -- * Configuration - MaudeConf(..) - , defaultConf - - -- * Invoking Maude - , MaudeResult(..) - , rewrite - , rewriteWith - - -- * Parsing Maude's output - , parseMaudeResult - - -- * Examples - -- $examples - - -- * Future Work - -- $future - ) where - -import Control.Monad (when) -import Data.Char (isSpace) -import Data.Text (Text) -import qualified Data.Text as T -import qualified Data.Text.IO as T -import System.IO (hPutStr, hPutStrLn, hClose, openTempFile) -import System.Directory (getCurrentDirectory, removeFile) -import System.Process (readProcess) - --- | Configuration of Maude's execution. -data MaudeConf = MaudeConf - { maudeCmd :: FilePath -- ^ Path to the Maude executable. - , loadFiles :: [FilePath] -- ^ Files to load before running a command. - , printParens :: Bool -- ^ Whether Maude should print with parentheses. - } deriving (Eq, Show) - --- | The default configuration used by the 'rewrite' function. -defaultConf :: MaudeConf -defaultConf = MaudeConf - { maudeCmd = "maude" - , loadFiles = [] - , printParens = False - } - --- | Maude option flags which force Maude's output to be as relevant as --- possible. -maudeArgs :: [String] -maudeArgs = - [ "-no-banner" - , "-no-advise" - , "-no-wrap" - , "-no-ansi-color" - ] - --- | The result of a Maude rewrite. -data MaudeResult = MaudeResult - { resultSort :: Text -- ^ The sort of the rewritten term. - , resultTerm :: Text -- ^ The rewritten term. - , statistics :: Text -- ^ Statistics printed by Maude. - } deriving (Show) - --- | @rewrite files term@ performs a single Maude rewrite command on --- @term@ using the 'defaultConf' configuration loaded with @files@. -rewrite :: [FilePath] -> Text -> IO (Maybe MaudeResult) -rewrite files term = rewriteWith defaultConf{ loadFiles = files } term - --- | @rewriteWith conf term@ performs a single Maude rewrite command on --- @term@ using the configuration @conf@. -rewriteWith :: MaudeConf -> Text -> IO (Maybe MaudeResult) -rewriteWith conf term = do - runner <- newRunnerFile conf term - let args = maudeArgs ++ [runner] - out <- readProcess (maudeCmd conf) args [] - removeFile runner - return $ parseMaudeResult (T.pack out) - --- | Parse Maude's output into a MaudeResult. The current implementation --- does very little sanity checking and can not parse Maude failures. -parseMaudeResult :: Text -> Maybe MaudeResult -parseMaudeResult str = do - let (stats, rest) = T.break (== '\n') str - r <- T.stripPrefix "\nresult " rest - let (sort, rest') = T.break (== ':') r - let term = parseTerm rest' - return $ MaudeResult - { resultSort = sort - , resultTerm = term - , statistics = stats - } - where parseTerm = trim - . T.concat - . filter (/= "Bye.") - . T.lines - . T.drop 1 -- Remove the ':' - --- | Create a temporary file which contains the commands Maude should run at --- startup: load file commands, formatting commands, the rewrite command, --- and the quit command. -newRunnerFile :: MaudeConf -> Text -> IO FilePath -newRunnerFile conf term = do - currDir <- getCurrentDirectory - (tmpf, tmph) <- openTempFile currDir "runner.maude" - mapM_ (\f -> T.hPutStr tmph "load " >> hPutStrLn tmph f) (loadFiles conf) - when (printParens conf) $ - T.hPutStrLn tmph "set print with parentheses on ." - T.hPutStrLn tmph "set show command off ." - T.hPutStr tmph "rewrite " - T.hPutStr tmph term - T.hPutStrLn tmph " ." - T.hPutStrLn tmph "quit" - hClose tmph - return tmpf - --- | Remove leading and trailing whitespace from a string. -trim :: Text -> Text -trim = f . f - where f = T.reverse . T.dropWhile isSpace - -{- $examples - -Maude's standard prelude is loaded by default, even when no input files are -specified: - ->>> rewrite [] "not (A:Bool or B:Bool) implies (not A:Bool) and (not B:Bool)" -Just (MaudeResult - { resultSort = "Bool" - , resultTerm = "true" - , statistics = "rewrites: 13 in 0ms cpu (0ms real) (~ rewrites/second)" - }) - -The name of the module in which to reduce a term can be given explicitly: - ->>> rewrite [] "in NAT-LIST : reverse(1 2 3 4)" -Just (MaudeResult - { resultSort = "NeNatList" - , resultTerm = "4 3 2 1" - , statistics = "rewrites: 6 in 0ms cpu (0ms real) (~ rewrites/second)" - }) - -Using a naive implementation of primes in Maude: - ->>> rewrite ["primes.maude"] "2 .. 20" -Just (MaudeResult - { resultSort = "PrimeSet" - , resultTerm = "2 3 5 7 11 13 17 19" - , statistics = "rewrites: 185 in 0ms cpu (0ms real) (~ rewrites/second)" - }) - -If we are only interested in the statistics: - ->>> liftM statistics <$> rewrite ["primes.maude"] "2 .. 1000" -Just "rewrites: 409905 in 839ms cpu (856ms real) (488014 rewrites/second)" --} - -{- $future - -This Maude interface is very minimal first step. It could be extended in the -following ways: - -* Better handling of Maude failures. Failure messages should be parsed and - returned to the user. - -* Support for other Maude commands besides @rewrite@. - -* A Maude monad that handles failure and multiple Maude commands efficiently - is a long-term goal for this package. - -* Consider taking of advantage of Maude's -xml-log option. --} diff --git a/maude.cabal b/maude.cabal --- a/maude.cabal +++ b/maude.cabal @@ -1,9 +1,9 @@ Name: maude -Version: 0.2.1 +Version: 0.3.0 Synopsis: An interface to the Maude rewriting system. Description: This package provides a simple interface for doing Maude rewrites from within Haskell. -Homepage: https://code.google.com/p/maude-hs/ +Homepage: https://github.com/davidlazar/maude-hs License: MIT License-file: LICENSE Author: David Lazar @@ -13,9 +13,10 @@ Cabal-version: >=1.6 source-repository head - Type: mercurial - Location: https://maude-hs.googlecode.com/hg/ + Type: git + Location: https://github.com/davidlazar/maude-hs Library + Hs-source-dirs: src Exposed-modules: Foreign.Maude - Build-depends: base >= 4 && < 5, process, directory, text + Build-depends: base >= 4 && < 5, process, directory, text, parsec >= 3.1.2 diff --git a/src/Foreign/Maude.hs b/src/Foreign/Maude.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Maude.hs @@ -0,0 +1,303 @@ +{-# LANGUAGE OverloadedStrings #-} +----------------------------------------------------------------------------- +-- | +-- Module : Foreign.Maude +-- Copyright : (c) David Lazar, 2011 +-- License : MIT +-- +-- Maintainer : lazar6@illinois.edu +-- Stability : experimental +-- Portability : unknown +-- +-- This package provides a simple interface (via the 'rewrite' and 'search' +-- functions) for doing Maude rewrites from within Haskell. The following +-- steps are performed every time Maude is executed by this library: +-- +-- 1. A temporary file is created that contains the necessary commands. +-- +-- 2. The temporary file (with any other input files) is executed by Maude. +-- +-- 3. The temporary file is removed. +-- +-- 4. The output from step 2 is parsed and returned. +-- +-- This is a simple way to perform a single rewrite command, but it is +-- inefficient for performing many rewrite commands. See /Future Work/ +-- below. +----------------------------------------------------------------------------- + +module Foreign.Maude + ( + -- * Configuration + MaudeConf(..) + , defaultConf + + -- * Maude commands + , Term + , Pattern + , MaudeCommand(..) + + -- * Invoking Maude + , RewriteResult(..) + , SearchResult(..) + , rewrite + , search + , runMaude + + -- * Parsing Maude's output + , parseRewriteResult + , parseSearchResults + + -- * Examples + -- $examples + + -- * Future Work + -- $future + ) where + +import Control.Applicative ((<$>)) +import Control.Monad (when) +import Data.Char (digitToInt) +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Text.IO as T +import System.IO (hPutStr, hPutStrLn, hClose, openTempFile) +import System.Directory (getCurrentDirectory, removeFile) +import System.Process (readProcess) +import Text.Parsec +import Text.Parsec.Text + +-- | Configuration of Maude's execution. +data MaudeConf = MaudeConf + { maudeCmd :: FilePath -- ^ Path to the Maude executable. + , loadFiles :: [FilePath] -- ^ Files to load before running a command. + , printParens :: Bool -- ^ Whether Maude should print with parentheses. + } deriving (Eq, Show) + +-- | The default Maude configuration. +defaultConf :: MaudeConf +defaultConf = MaudeConf + { maudeCmd = "maude" + , loadFiles = [] + , printParens = False + } + +-- | Maude option flags which force Maude's output to be as relevant as +-- possible. +maudeArgs :: [String] +maudeArgs = + [ "-no-banner" + , "-no-advise" + , "-no-wrap" + , "-no-ansi-color" + ] + +-- | Synonym for text to be manipulated by Maude. +type Term = Text + +-- | Synonym for text representing a search pattern; see 'search'. +type Pattern = Text + +-- Commands used in Maude. +data MaudeCommand + = Rewrite Term + | Search Term Pattern + deriving (Show) + +-- | The result of a Maude rewrite. +data RewriteResult = RewriteResult + { resultSort :: Text -- ^ The sort of the rewritten term. + , resultTerm :: Text -- ^ The rewritten term. + , statistics :: Text -- ^ Statistics printed by Maude. + } deriving (Show) + +-- | A single Maude search result. +data SearchResult = SearchResult + { searchResultState :: Integer + , searchStatistics :: Text + , searchResultTerm :: Text + } deriving (Show) + +-- | @rewrite files term@ performs a single Maude rewrite command on +-- @term@ with @files@ loaded. +rewrite :: [FilePath] -> Term -> IO (Maybe RewriteResult) +rewrite files term = parseRewriteResult + <$> runMaude defaultConf{ loadFiles = files } (Rewrite term) + +-- | @search files term pattern@ uses Maude to search for all reachable +-- states starting from @term@ and matching the given @pattern@. Note that +-- @pattern@ should also include the search type. For example, +-- +-- >>> search [] term "=>! N:Nat" +-- +search :: [FilePath] -> Term -> Pattern -> IO (Maybe [SearchResult]) +search files term pattern = parseSearchResults + <$> runMaude defaultConf{ loadFiles = files } cmd + where cmd = Search term pattern + +-- | @runMaude conf cmd@ runs the Maude using the configuration @conf@ +-- and performs the command @cmd@. +runMaude :: MaudeConf -> MaudeCommand -> IO Text +runMaude conf cmd = do + runner <- newRunnerFile conf cmd + let args = maudeArgs ++ [runner] + out <- readProcess (maudeCmd conf) args [] + removeFile runner + return $ T.pack out + +-- | Parse Maude's output into a RewriteResult. The current implementation +-- does very little sanity checking and can not parse Maude failures. +parseRewriteResult :: Text -> Maybe RewriteResult +parseRewriteResult txt = + case parse pRewriteResult "" txt of + Left _ -> Nothing + Right r -> Just r + +-- | Parse the output of a successful @search@ command. +parseSearchResults :: Text -> Maybe [SearchResult] +parseSearchResults txt = + case parse pSearchResults "" txt of + Left _ -> Nothing + Right r -> Just r + +-- | Parsec parser that parses the output of a successful Maude +-- rewrite command. +pRewriteResult :: Parser RewriteResult +pRewriteResult = do + optional (string "Maude>") + spaces + stats <- pLine + string "result" + spaces + sort <- many1 (satisfy (/= ':')) + char ':' + spaces + lines <- many1 pLine + let term = T.concat . filter (/= "Bye.") $ lines + return $ RewriteResult + { resultSort = T.pack sort + , resultTerm = term + , statistics = stats + } + +-- | Parsec parser that parses the output of a successful Maude +-- search command. +pSearchResults :: Parser [SearchResult] +pSearchResults = do + optional (symbol "Maude>") + spaces + pSearchResult `endBy1` newline + +-- | Parsec parser that parses a single search result. +pSearchResult :: Parser SearchResult +pSearchResult = do + symbol "Solution" + integer + spaces + state <- parens (symbol "state" >> integer) + newline + stats <- pLine + var <- many1 (satisfy (/= ' ')) + spaces + symbol "-->" + lines <- many1 pLine + let term = T.concat lines + return $ SearchResult + { searchResultState = state + , searchStatistics = stats + , searchResultTerm = term + } + +-- | Parse a single line. +pLine :: Parser Text +pLine = do + x <- many1 (satisfy (/= '\n')) + newline + return $ T.pack x + +-- | Create a temporary file which contains the commands Maude should run at +-- startup: load file commands, formatting commands, the command to execute, +-- and the quit command. +newRunnerFile :: MaudeConf -> MaudeCommand -> IO FilePath +newRunnerFile conf cmd = do + currDir <- getCurrentDirectory + (tmpf, tmph) <- openTempFile currDir "runner.maude" + mapM_ (\f -> T.hPutStr tmph "load " >> hPutStrLn tmph f) (loadFiles conf) + when (printParens conf) $ + T.hPutStrLn tmph "set print with parentheses on ." + T.hPutStrLn tmph "set show command off ." + T.hPutStr tmph (toTxt cmd) + T.hPutStrLn tmph " ." + T.hPutStrLn tmph "quit" + hClose tmph + return tmpf + where toTxt (Rewrite term) = T.append "rewrite " term + toTxt (Search term pat) = T.intercalate " " ["search", term, pat] + + +-- Lexers: + +integer = number 10 digit + +parens = between (char '(') (char ')') + +symbol s = do { x <- string s; spaces; return x } + +-- copied from Parsec: +number base baseDigit + = do { digits <- many1 baseDigit + ; let n = foldl (\x d -> base * x + toInteger (digitToInt d)) 0 digits + ; seq n (return n) + } + +{- $examples + +Maude's standard prelude is loaded by default, even when no input files are +specified: + +>>> rewrite [] "not (A:Bool or B:Bool) implies (not A:Bool) and (not B:Bool)" +Just (RewriteResult + { resultSort = "Bool" + , resultTerm = "true" + , statistics = "rewrites: 13 in 0ms cpu (0ms real) (~ rewrites/second)" + }) + +The name of the module in which to reduce a term can be given explicitly: + +>>> rewrite [] "in NAT-LIST : reverse(1 2 3 4)" +Just (RewriteResult + { resultSort = "NeNatList" + , resultTerm = "4 3 2 1" + , statistics = "rewrites: 6 in 0ms cpu (0ms real) (~ rewrites/second)" + }) + +Using a naive implementation of primes in Maude: + +>>> rewrite ["primes.maude"] "2 .. 20" +Just (RewriteResult + { resultSort = "PrimeSet" + , resultTerm = "2 3 5 7 11 13 17 19" + , statistics = "rewrites: 185 in 0ms cpu (0ms real) (~ rewrites/second)" + }) + +If we are only interested in the statistics: + +>>> liftM statistics <$> rewrite ["primes.maude"] "2 .. 1000" +Just "rewrites: 409905 in 839ms cpu (856ms real) (488014 rewrites/second)" +-} + +{- $future + +This Maude interface is very minimal first step. It could be extended in the +following ways: + +* Better handling of Maude failures. Failure messages should be parsed and + returned to the user. + +* Support for other Maude commands besides @rewrite@. + +* A Maude monad that handles failure and multiple Maude commands efficiently + is a long-term goal for this package. + +* Consider taking of advantage of Maude's -xml-log option. +-}