maude-0.2.0: An interface to the Maude rewriting system.





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.



data MaudeConf Source

Configuration of Maude's execution.




maudeCmd :: FilePath

Path to the Maude executable.

loadFiles :: [FilePath]

Files to load before running a command.

printParens :: Bool

Whether Maude should print with parentheses.

defaultConf :: MaudeConfSource

The default configuration used by the rewrite function.

Invoking Maude

data MaudeResult Source

The result of a Maude rewrite.




resultSort :: Text

The sort of the rewritten term.

resultTerm :: Text

The rewritten term.

statistics :: Text

Statistics printed by Maude.


rewrite :: [FilePath] -> Text -> IO (Maybe MaudeResult)Source

rewrite files term performs a single Maude rewrite command on term using the defaultConf configuration loaded with files.

rewriteWith :: MaudeConf -> Text -> IO (Maybe MaudeResult)Source

rewriteWith conf term performs a single Maude rewrite command on term using the configuration conf.

Parsing Maude's output

parseMaudeResult :: Text -> Maybe MaudeResultSource

Parse Maude's output into a MaudeResult. The current implementation does very little sanity checking and can not parse Maude failures.


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 Work

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.