diff --git a/Foreign/Maude.hs b/Foreign/Maude.hs new file mode 100644 --- /dev/null +++ b/Foreign/Maude.hs @@ -0,0 +1,165 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Foreign.Maude +-- Copyright : (c) David Lazar, 2010 +-- License : BSD3 +-- +-- Maintainer : lazar6@illinois.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- This package provides a simple interface (via the 'rewrite' function) for +-- doing Maude rewrites from within Haskell. The following steps are +-- performed every time the 'rewrite' function is 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 + ( + -- * Invoking Maude + MaudeResult(..) + , rewrite + + -- * Examples + -- $examples + + -- * Future Work + -- $future + ) where + +import Data.List (break, stripPrefix) +import System.IO (hPutStrLn, hClose, openTempFile) +import System.Directory (getCurrentDirectory, removeFile) +import System.Process (readProcess) + + +-- | The result of a Maude rewrite. +data MaudeResult = MaudeResult + { resultSort :: String -- ^ The sort of the rewritten term. + , resultTerm :: String -- ^ The rewritten term. + , statistics :: String -- ^ Statistics printed by Maude. + } deriving (Show) + +-- | The name of the Maude executable. It should be in $PATH. +maudeCmd :: FilePath +maudeCmd = "maude" + +-- | 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 'rewrite' function takes a list of Maude file names and a term, and +-- attempts to rewrite the term in the context of those files. It assumes +-- the command to run Maude is \"maude\" and that it located somewhere in +-- @$PATH@. +rewrite :: [FilePath] -> String -> IO (Maybe MaudeResult) +rewrite files term = do + runner <- newRunnerFile term + let args = maudeArgs ++ files ++ [runner] + out <- readProcess maudeCmd args [] + removeFile runner + return $ parseMaudeResult out + +-- | Parse Maude's output into a MaudeResult. The current implementation does +-- very little sanity checking and can not parse Maude failures. +parseMaudeResult :: String -> Maybe MaudeResult +parseMaudeResult str = case lines str of + (stats : res : _) -> do + r <- stripPrefix "result " res + let (sort, term) = break (==':') r + return $ MaudeResult + { resultSort = sort + , resultTerm = drop 2 term + , statistics = stats + } + _ -> Nothing + + +-- | Create a temporary file which contains the commands Maude should run at +-- startup, namely some formatting commands, the rewrite command, and quit. +newRunnerFile :: String -> IO FilePath +newRunnerFile term = do + currDir <- getCurrentDirectory + (tmpf, tmph) <- openTempFile currDir "runner.maude" + hPutStrLn tmph "set print with parentheses on ." + hPutStrLn tmph "set show command off ." + hPutStrLn tmph $ "rewrite " ++ term ++ " ." + hPutStrLn tmph "quit" + hClose tmph + return tmpf + +{- $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)" + }) + +Notice that the resulting list is given in parenthesized form. This is because + +> set print with parentheses on . + +is executed before every rewrite. + +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. + +* The rewriting environment should be configurable. This would allow + parenthesized mode to be turned off and for the location of the Maude + binary to be customized. + +* 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. +-} diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c)2010, David Lazar + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of David Lazar nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/maude.cabal b/maude.cabal new file mode 100644 --- /dev/null +++ b/maude.cabal @@ -0,0 +1,18 @@ +Name: maude +Version: 0.1.0 +Synopsis: An interface to the Maude rewriting system. +Description: This package provides a simple interface for doing Maude + rewrites from within Haskell. +Homepage: http://git.mzero.org/maude/ +License: BSD3 +License-file: LICENSE +Author: David Lazar +Maintainer: David Lazar +Category: Foreign +Build-type: Simple +Cabal-version: >=1.2 + + +Library + Exposed-modules: Foreign.Maude + Build-depends: base >= 4 && < 5, process, directory