Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | lazar6@illinois.edu |
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:
- 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.
- data MaudeResult = MaudeResult {
- resultSort :: String
- resultTerm :: String
- statistics :: String
- rewrite :: [FilePath] -> String -> IO (Maybe MaudeResult)
Invoking Maude
data MaudeResult Source
The result of a Maude rewrite.
MaudeResult | |
|
rewrite :: [FilePath] -> String -> IO (Maybe MaudeResult)Source
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 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.