Foreign.Maude

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.

Invoking Maude

data MaudeResult

The result of a Maude rewrite.

Constructors

MaudeResult

Fields

resultSort :: String

The sort of the rewritten term.

resultTerm :: String

The rewritten term.

statistics :: String

Statistics printed by Maude.

Instances

Show MaudeResult

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

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 is located somewhere in $PATH.

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