Foreign.Maude

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.

Configuration

data MaudeConf

Configuration of Maude's execution.

Constructors

MaudeConf

Fields

maudeCmd :: FilePath

Path to the Maude executable.

loadFiles :: [FilePath]

Files to load before running a command.

printParens :: Bool

Whether Maude should print with parentheses.

Instances

Eq MaudeConf

Show MaudeConf

defaultConf :: MaudeConf

The default configuration used by the rewrite function.

Invoking Maude

data MaudeResult

The result of a Maude rewrite.

Constructors

MaudeResult

Fields

resultSort :: Text

The sort of the rewritten term.

resultTerm :: Text

The rewritten term.

statistics :: Text

Statistics printed by Maude.

Instances

Show MaudeResult

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

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

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

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

Parsing Maude's output

parseMaudeResult :: Text -> Maybe MaudeResult

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

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