maude (empty) → 0.1.0

raw patch · 4 files changed

+215/−0 lines, 4 filesdep +basedep +directorydep +processsetup-changed

Dependencies added: base, directory, process

Files

Foreign/Maude.hs +165/−0
LICENSE +30/−0
Setup.hs +2/−0
maude.cabal +18/−0

+ Foreign/Maude.hs view

@@ -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.+-}

+ LICENSE view

@@ -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.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ maude.cabal view

@@ -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 <lazar6@illinois.edu>+Category:           Foreign+Build-type:         Simple+Cabal-version:      >=1.2+++Library+  Exposed-modules:  Foreign.Maude+  Build-depends:    base >= 4 && < 5, process, directory