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





This package provides a simple interface (via the rewrite and search functions) for doing Maude rewrites from within Haskell. The following steps are performed every time Maude is executed by this library:

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

Maude commands

type Term = TextSource

Synonym for text to be manipulated by Maude.

type Pattern = TextSource

Synonym for text representing a search pattern; see search.

Invoking Maude

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


data SearchResult Source

A single Maude search result.


rewrite :: [FilePath] -> Term -> IO (Maybe RewriteResult)Source

rewrite files term performs a single Maude rewrite command on term with files loaded.

search :: [FilePath] -> Term -> Pattern -> IO (Maybe [SearchResult])Source

search files term pattern uses Maude to search for all reachable states starting from term and matching the given pattern. Note that pattern should also include the search type. For example,

>>> search [] term "=>! N:Nat"

runMaude :: MaudeConf -> MaudeCommand -> IO TextSource

runMaude conf cmd runs the Maude using the configuration conf and performs the command cmd.

Parsing Maude's output

parseRewriteResult :: Text -> Maybe RewriteResultSource

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

parseSearchResults :: Text -> Maybe [SearchResult]Source

Parse the output of a successful search command.


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 (RewriteResult
    { 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 (RewriteResult
    { 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 (RewriteResult
    { 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.