Portability	unknown
Stability	experimental
Maintainer	lazar6@illinois.edu

Foreign.Maude

Contents

Configuration
Maude commands
Invoking Maude
Parsing Maude's output
Examples
Future Work

Description

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:

A temporary file is created that contains the necessary commands.
The temporary file (with any other input files) is executed by Maude.
The temporary file is removed.
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.

Synopsis

Configuration

data MaudeConf Source

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 Source

The default Maude configuration.

Maude commands

type Term = Text Source

Synonym for text to be manipulated by Maude.

type Pattern = Text Source

Synonym for text representing a search pattern; see search.

data MaudeCommand Source

Constructors

Rewrite Term
Search Term Pattern

Instances

Show MaudeCommand

Invoking Maude

data RewriteResult Source

The result of a Maude rewrite.

Constructors

RewriteResult
Fields resultSort :: Text The sort of the rewritten term. resultTerm :: Text The rewritten term. statistics :: Text Statistics printed by Maude.

Instances

Show RewriteResult

data SearchResult Source

A single Maude search result.

Constructors

SearchResult
Fields searchResultState :: Integer searchStatistics :: Text searchResultTerm :: Text

Instances

Show SearchResult

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 Text Source

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

Parsing Maude's output

parseRewriteResult :: Text -> Maybe RewriteResult Source

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.

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