Portability | unknown |
---|---|
Stability | experimental |
Maintainer | lazar6@illinois.edu |
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:
- 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 MaudeConf = MaudeConf {}
- defaultConf :: MaudeConf
- data MaudeResult = MaudeResult {
- resultSort :: Text
- resultTerm :: Text
- statistics :: Text
- rewrite :: [FilePath] -> Text -> IO (Maybe MaudeResult)
- rewriteWith :: MaudeConf -> Text -> IO (Maybe MaudeResult)
- parseMaudeResult :: Text -> Maybe MaudeResult
Configuration
Configuration of Maude's execution.
defaultConf :: MaudeConfSource
The default configuration used by the rewrite
function.
Invoking Maude
data MaudeResult Source
The result of a Maude rewrite.
MaudeResult | |
|
rewrite :: [FilePath] -> Text -> IO (Maybe MaudeResult)Source
rewrite files term
performs a single Maude rewrite command on
term
using the defaultConf
configuration loaded with files
.
rewriteWith :: MaudeConf -> Text -> IO (Maybe MaudeResult)Source
rewriteWith conf term
performs a single Maude rewrite command on
term
using the configuration conf
.
Parsing Maude's output
parseMaudeResult :: Text -> Maybe MaudeResultSource
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.