maude 0.3.0 → 0.6.1

raw patch · 7 files changed

+448/−307 lines, 7 filesdep +filepathdep +process-extrasdep +temporarydep −parsecPVP ok

version bump matches the API change (PVP)

Dependencies added: filepath, process-extras, temporary, xml

Dependencies removed: parsec

API changes (from Hackage documentation)

Files

• README.md +10/−0
• maude.cabal +24/−4
• src/Foreign/Maude.hs +0/−303
• src/Language/Maude/Exec.hs +133/−0
• src/Language/Maude/Exec/Types.hs +125/−0
• src/Language/Maude/Exec/XML.hs +119/−0
• src/Language/Maude/Syntax.hs +37/−0

@@ -0,0 +1,10 @@+# About++This package provides a simple interface for doing [Maude](http://maude.cs.uiuc.edu/) rewrites from within Haskell.+See the [Haddock documentation](http://hackage.haskell.org/packages/archive/maude/latest/doc/html/Foreign-Maude.html) for examples.++# Contributing++This project is available on [GitHub](https://github.com/davidlazar/maude-hs) and [Bitbucket](https://bitbucket.org/davidlazar/maude-hs/). You may contribute changes using either.++Please report bugs and feature requests using the [GitHub issue tracker](https://github.com/davidlazar/maude-hs/issues).

@@ -1,5 +1,5 @@ Name:               maude-Version:            0.3.0+Version:            0.6.1 Synopsis:           An interface to the Maude rewriting system. Description:        This package provides a simple interface for doing Maude                     rewrites from within Haskell.@@ -8,15 +8,35 @@ License-file:       LICENSE Author:             David Lazar Maintainer:         David Lazar <lazar6@illinois.edu>-Category:           Foreign+Category:           Language Build-type:         Simple Cabal-version:      >=1.6+Extra-source-files:+  README.md  source-repository head   Type:             git   Location:         https://github.com/davidlazar/maude-hs  Library+  ghc-options:      -Wall+   Hs-source-dirs:   src-  Exposed-modules:  Foreign.Maude-  Build-depends:    base >= 4 && < 5, process, directory, text, parsec >= 3.1.2++  Exposed-modules:+    Language.Maude.Exec+    Language.Maude.Exec.Types+    Language.Maude.Syntax++  Other-modules:+    Language.Maude.Exec.XML++  Build-depends:+    base >= 4 && < 5,+    process,+    process-extras,+    filepath,+    directory,+    temporary,+    text,+    xml

@@ -1,303 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}--------------------------------------------------------------------------------- |--- Module      :  Foreign.Maude--- Copyright   :  (c) David Lazar, 2011--- License     :  MIT------ Maintainer  :  lazar6@illinois.edu--- Stability   :  experimental--- Portability :  unknown------ 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.--------------------------------------------------------------------------------module Foreign.Maude-    (-    -- * Configuration-      MaudeConf(..)-    , defaultConf--    -- * Maude commands-    , Term-    , Pattern-    , MaudeCommand(..)--    -- * Invoking Maude-    , RewriteResult(..)-    , SearchResult(..)-    , rewrite-    , search-    , runMaude--    -- * Parsing Maude's output-    , parseRewriteResult-    , parseSearchResults--    -- * Examples-    -- $examples--    -- * Future Work-    -- $future-    ) where--import Control.Applicative ((<$>))-import Control.Monad (when)-import Data.Char (digitToInt)-import Data.Text (Text)-import qualified Data.Text as T-import qualified Data.Text.IO as T-import System.IO (hPutStr, hPutStrLn, hClose, openTempFile)-import System.Directory (getCurrentDirectory, removeFile)-import System.Process (readProcess)-import Text.Parsec-import Text.Parsec.Text---- | Configuration of Maude's execution.-data MaudeConf = MaudeConf-    { maudeCmd    :: FilePath   -- ^ Path to the Maude executable.-    , loadFiles   :: [FilePath] -- ^ Files to load before running a command.-    , printParens :: Bool       -- ^ Whether Maude should print with parentheses.-    } deriving (Eq, Show)---- | The default Maude configuration.-defaultConf :: MaudeConf-defaultConf = MaudeConf-    { maudeCmd    = "maude"-    , loadFiles   = []-    , printParens = False-    }---- | Maude option flags which force Maude's output to be as relevant as--- possible.-maudeArgs :: [String]-maudeArgs =-    [ "-no-banner"-    , "-no-advise"-    , "-no-wrap"-    , "-no-ansi-color"-    ]---- | Synonym for text to be manipulated by Maude.-type Term = Text---- | Synonym for text representing a search pattern; see 'search'.-type Pattern = Text---- Commands used in Maude.-data MaudeCommand-    = Rewrite Term-    | Search Term Pattern-    deriving (Show)---- | The result of a Maude rewrite.-data RewriteResult = RewriteResult-    { resultSort :: Text  -- ^ The sort of the rewritten term.-    , resultTerm :: Text  -- ^ The rewritten term.-    , statistics :: Text  -- ^ Statistics printed by Maude.-    } deriving (Show)---- | A single Maude search result.-data SearchResult = SearchResult-    { searchResultState :: Integer-    , searchStatistics  :: Text-    , searchResultTerm  :: Text-    } deriving (Show)---- | @rewrite files term@ performs a single Maude rewrite command on--- @term@ with @files@ loaded.-rewrite :: [FilePath] -> Term -> IO (Maybe RewriteResult)-rewrite files term = parseRewriteResult-                 <$> runMaude defaultConf{ loadFiles = files } (Rewrite term)---- | @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"----search :: [FilePath] -> Term -> Pattern -> IO (Maybe [SearchResult])-search files term pattern = parseSearchResults-                        <$> runMaude defaultConf{ loadFiles = files } cmd-    where cmd = Search term pattern---- | @runMaude conf cmd@ runs the Maude using the configuration @conf@--- and performs the command @cmd@.-runMaude :: MaudeConf -> MaudeCommand -> IO Text-runMaude conf cmd = do-    runner <- newRunnerFile conf cmd-    let args = maudeArgs ++ [runner]-    out <- readProcess (maudeCmd conf) args []-    removeFile runner-    return $ T.pack out---- | Parse Maude's output into a RewriteResult.  The current implementation--- does very little sanity checking and can not parse Maude failures.-parseRewriteResult :: Text -> Maybe RewriteResult-parseRewriteResult txt =-    case parse pRewriteResult "" txt of-        Left _ -> Nothing-        Right r -> Just r---- | Parse the output of a successful @search@ command.-parseSearchResults :: Text -> Maybe [SearchResult]-parseSearchResults txt =-    case parse pSearchResults "" txt of-        Left _ -> Nothing-        Right r -> Just r---- | Parsec parser that parses the output of a successful Maude--- rewrite command.-pRewriteResult :: Parser RewriteResult-pRewriteResult = do-    optional (string "Maude>")-    spaces-    stats <- pLine-    string "result"-    spaces-    sort <- many1 (satisfy (/= ':'))-    char ':'-    spaces-    lines <- many1 pLine-    let term = T.concat . filter (/= "Bye.") $ lines-    return $ RewriteResult-        { resultSort = T.pack sort-        , resultTerm = term-        , statistics = stats-        }---- | Parsec parser that parses the output of a successful Maude--- search command.-pSearchResults :: Parser [SearchResult]-pSearchResults = do-    optional (symbol "Maude>")-    spaces-    pSearchResult `endBy1` newline---- | Parsec parser that parses a single search result.-pSearchResult :: Parser SearchResult-pSearchResult = do-    symbol "Solution"-    integer-    spaces-    state <- parens (symbol "state" >> integer)-    newline-    stats <- pLine-    var <- many1 (satisfy (/= ' '))-    spaces-    symbol "-->"-    lines <- many1 pLine-    let term = T.concat lines-    return $ SearchResult-        { searchResultState = state-        , searchStatistics = stats-        , searchResultTerm = term-        }---- | Parse a single line.-pLine :: Parser Text-pLine = do-    x <- many1 (satisfy (/= '\n'))-    newline-    return $ T.pack x---- | Create a temporary file which contains the commands Maude should run at--- startup: load file commands, formatting commands, the command to execute,--- and the quit command.-newRunnerFile :: MaudeConf -> MaudeCommand -> IO FilePath-newRunnerFile conf cmd = do-    currDir <- getCurrentDirectory-    (tmpf, tmph) <- openTempFile currDir "runner.maude"-    mapM_ (\f -> T.hPutStr tmph "load " >> hPutStrLn tmph f) (loadFiles conf)-    when (printParens conf) $-        T.hPutStrLn tmph "set print with parentheses on ."-    T.hPutStrLn tmph "set show command off ."-    T.hPutStr tmph (toTxt cmd)-    T.hPutStrLn tmph " ."-    T.hPutStrLn tmph "quit"-    hClose tmph-    return tmpf-    where toTxt (Rewrite term) = T.append "rewrite " term-          toTxt (Search term pat) = T.intercalate " " ["search", term, pat]----- Lexers:--integer = number 10 digit--parens = between (char '(') (char ')')--symbol s = do { x <- string s; spaces; return x }---- copied from Parsec:-number base baseDigit-    = do { digits <- many1 baseDigit-         ; let n = foldl (\x d -> base * x + toInteger (digitToInt d)) 0 digits-         ; seq n (return n)-         }--{- $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--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.--}

@@ -0,0 +1,133 @@+{-# LANGUAGE OverloadedStrings #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Language.Maude.Exec+-- Copyright   :  (c) David Lazar, 2012+-- License     :  MIT+--+-- Maintainer  :  lazar6@illinois.edu+-- Stability   :  experimental+-- Portability :  unknown+--+-- This package provides a simple interface to the Maude executable for+-- doing Maude rewrites from within Haskell.+--+-- Note: Maude is considered to have failed if it ever prints to stderr.+-----------------------------------------------------------------------------++module Language.Maude.Exec+    (+      module Language.Maude.Exec.Types++    -- * High-level interface+    , rewrite+    , search++    -- * Low-level interface+    , runMaude+    , defaultConf+    ) where++import Control.Exception+import Control.Monad (when)+import Data.Text (Text)+import qualified Data.Text as T+import qualified Data.Text.IO as T+import System.IO (hClose)+import System.IO.Temp+import System.Directory (getCurrentDirectory)+import System.Exit+import System.Process.Text (readProcessWithExitCode)+import Text.XML.Light (parseXMLDoc)++import Language.Maude.Exec.Types+import Language.Maude.Exec.XML++-- | @rewrite files term@ rewrites @term@ using Maude (with @files@ loaded).+--+-- This function may throw a 'MaudeException'.+rewrite :: [FilePath] -> Text -> IO RewriteResult+rewrite files term = do+    let cmd = Rewrite term+    maudeResult <- runMaude defaultConf{ loadFiles = files } cmd+    let maybeXml = parseXMLDoc $ maudeXmlLog maudeResult+    xml <- maybe (throwIO LogToXmlFailure) return maybeXml+    case parseRewriteResult xml of+        ParseError e s -> throwIO $ XmlToResultFailure s e+        Ok a -> return a++-- | @search files term pattern@ uses Maude (with @files@ loaded) 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"+--+-- runs the Maude command @search term =>! N:Nat@.+--+-- This function may throw a 'MaudeException'.+search :: [FilePath] -> Text -> Text -> IO SearchResults+search files term pattern = do+    let cmd = Search term pattern+    maudeResult <- runMaude defaultConf{ loadFiles = files } cmd+    let maybeXml = parseXMLDoc $ maudeXmlLog maudeResult+    xml <- maybe (throwIO LogToXmlFailure) return maybeXml+    case parseSearchResults xml of+        ParseError e s -> throwIO $ XmlToResultFailure s e+        Ok a -> return a++-- | @runMaude conf cmd@ performs the Maude command @cmd@ using the+-- configuration @conf@.+--+-- This function may throw a 'MaudeException'.+runMaude :: MaudeConf -> MaudeCommand -> IO MaudeResult+runMaude conf cmd = do+    currDir <- getCurrentDirectory+    withTempFile currDir "maudelog.xml" $ \xmlFile xmlHandle -> do+        hClose xmlHandle -- we don't need it+        let exe = maudeCmd conf+        let args = maudeArgs xmlFile ++ (loadFiles conf)+        let input = mkMaudeInput cmd+        (exitCode, out, err) <- readProcessWithExitCode exe args input+        when (not (T.null err) || exitCode /= ExitSuccess) $+            throwIO $ MaudeFailure+                { maudeFailureExitCode = exitCode+                , maudeFailureStderr = err+                , maudeFailureStdout = out+                }+        xmlText <- T.readFile xmlFile+        return $ MaudeResult+            { maudeStdout = out+            , maudeXmlLog = xmlText+            }++-- | Default Maude configuration+defaultConf :: MaudeConf+defaultConf = MaudeConf+    { maudeCmd  = "maude"+    , loadFiles = []+    }++-- | Maude flags which force its output to be as relevant as possible+maudeArgs :: FilePath -> [String]+maudeArgs xmlFile =+    [ "-no-banner"+    , "-no-advise"+    , "-no-wrap"+    , "-no-ansi-color"+    , "-xml-log=" ++ xmlFile+    ]++-- | Constructs the text that is sent to Maude.+mkMaudeInput :: MaudeCommand -> Text+mkMaudeInput cmd = T.unlines $+    [ "set show command off ."+    , showCommand cmd+    , " ."+    , "quit"+    ]++showCommand :: MaudeCommand -> Text+showCommand (Rewrite term) = "rewrite " `T.append` term+showCommand (Erewrite term) = "erewrite " `T.append` term+showCommand (Search term pattern) = T.concat ["search ", term, " ", pattern]

@@ -0,0 +1,125 @@+{-# LANGUAGE DeriveDataTypeable #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Language.Maude.Exec.Types+-- Copyright   :  (c) David Lazar, 2012+-- License     :  MIT+--+-- Maintainer  :  lazar6@illinois.edu+-- Stability   :  experimental+-- Portability :  unknown+--+-- Types shared between modules in the Language.Maude.Exec namespace+-----------------------------------------------------------------------------+module Language.Maude.Exec.Types+    (+    -- * Error handling+      MaudeException(..)++    -- * Configuring Maude's execution+    , MaudeCommand(..)+    , MaudeConf(..)++    -- * Result types+    , MaudeResult(..)+    , RewriteResult(..)+    , SearchResult(..)+    , SearchResults+    , Substitution(..)+    , MaudeStatistics(..)+    ) where++import Control.Exception+import Data.Data+import Data.Text (Text)+import System.Exit (ExitCode)+import qualified Text.XML.Light as XML++import Language.Maude.Syntax++data MaudeException+    = MaudeFailure+        { maudeFailureExitCode :: ExitCode+        , maudeFailureStderr   :: Text+        , maudeFailureStdout   :: Text+        }+    -- ^ Thrown when the @maude@ executable fails+    | LogToXmlFailure+    -- ^ Thrown when the log produced by Maude is not parseable as XML+    | XmlToResultFailure String XML.Element+    -- ^ Thrown when the XML can't be parsed/translated to+    -- one of the result types below+    deriving (Typeable)++instance Exception MaudeException++instance Show MaudeException where+    showsPrec _ (MaudeFailure e err out)+        = showString "MaudeFailure (exitCode = " . showsPrec 0 e+        . showString ") (stderr = " . showsPrec 0 err+        . showString ") (stdout = " . showsPrec 0 out . showChar ')'+    showsPrec _ LogToXmlFailure = showString "LogToXmlFailure"+    showsPrec _ (XmlToResultFailure s e)+        = showString "XmlToResultFailure " . showsPrec 0 s+        . showString "\n" . showString (take n xml)+        . showString (if length xml > n then "..." else "")+      where+        n = 100+        xml = XML.showElement e++-- | Commands performed by Maude+data MaudeCommand+    = Rewrite Text+    | Erewrite Text+    | Search Text Text+    deriving (Eq, Ord, Show, Data, Typeable)++-- | Configuration of Maude's execution+data MaudeConf = MaudeConf+    { maudeCmd    :: FilePath+    -- ^ Path to the Maude executable+    , loadFiles   :: [FilePath]+    -- ^ Files to load before running a command+    } deriving (Eq, Ord, Show, Data, Typeable)++-- | Low-level Maude result+data MaudeResult+    = MaudeResult+        { maudeStdout :: Text+        -- ^ Text printed to standard out during execution+        , maudeXmlLog :: Text+        -- ^ XML log obtained via Maude's @--xml-log@ option+        }+    deriving (Eq, Ord, Show, Data, Typeable)++-- | High-level (e)rewrite result+data RewriteResult = RewriteResult+    { resultTerm        :: Term+    -- ^ The rewritten term+    , rewriteStatistics :: MaudeStatistics+    -- ^ Statistics about the rewrite performed+    } deriving (Eq, Ord, Show, Data, Typeable)++-- | High-level search result+data SearchResult = SearchResult+    { searchSolutionNumber :: Integer+    , searchStatistics     :: MaudeStatistics+    , searchResult         :: Substitution+    } deriving (Eq, Ord, Show, Data, Typeable)++-- | Several search results+type SearchResults = [SearchResult]++-- | Search result substitution+data Substitution = Substitution Term Term+    deriving (Eq, Ord, Show, Data, Typeable)++-- | Statistics returned by Maude after a successful command+data MaudeStatistics = MaudeStatistics+    { totalRewrites :: Integer+    -- ^ Total rewrites performed+    , realTime      :: Integer+    -- ^ Real time (milliseconds)+    , cpuTime       :: Integer+    -- ^ CPU time (milliseconds)+    } deriving (Eq, Ord, Show, Data, Typeable)

@@ -0,0 +1,119 @@+module Language.Maude.Exec.XML+    ( Parser(..)+    , parseRewriteResult+    , parseSearchResults+    ) where++import Control.Monad+import Text.XML.Light++import Language.Maude.Syntax+import Language.Maude.Exec.Types++data Parser a+    = ParseError Element String+    | Ok a+    deriving (Show)++instance Functor Parser where+    fmap _ (ParseError e s) = ParseError e s+    fmap f (Ok r) = Ok (f r)++instance Monad Parser where+    return = Ok+    ParseError e s >>= _ = ParseError e s+    Ok r >>= k = k r++-- <maudeml> (root)+parseRewriteResult :: Element -> Parser RewriteResult+parseRewriteResult e = parseRewriteResult' =<< child "result" e++-- <maudeml> (root)+parseSearchResults :: Element -> Parser SearchResults+parseSearchResults e = case results of+    [] -> ParseError e "no search results found"+    _  -> mapM parseSearchResult =<< actualResults+  where+    results = findChildren (unqual "search-result") e+    actualResults = filterM notNone results+    notNone e' = attr "solution-number" e' >>= return . (/= "NONE")++-- <result>+parseRewriteResult' :: Element -> Parser RewriteResult+parseRewriteResult' e = do+    stats <- parseStatistics e+    term <- case elChildren e of+        [e'] -> parseTerm e'+        _ -> ParseError e "expecting exactly one result child"+    return $ RewriteResult+        { resultTerm = term+        , rewriteStatistics = stats+        }++-- <result>+parseStatistics :: Element -> Parser MaudeStatistics+parseStatistics e = do+    rews <- readattr "total-rewrites" e+    real <- readattr "real-time-ms" e+    cpu  <- readattr "cpu-time-ms" e+    return $ MaudeStatistics rews real cpu++-- <search-result>+parseSearchResult :: Element -> Parser SearchResult+parseSearchResult e = do+    solution <- readattr "solution-number" e+    stats <- parseStatistics e+    subst <- parseSubstitution =<< child "substitution" e+    return $ SearchResult+        { searchSolutionNumber = solution+        , searchStatistics = stats+        , searchResult = subst+        }++-- <substitution>+parseSubstitution :: Element -> Parser Substitution+parseSubstitution e = do+    assignment <- child "assignment" e+    -- TODO: better error handling+    [s, t] <- mapM parseTerm (elChildren assignment)+    return $ Substitution s t++-- <term>+parseTerm :: Element -> Parser Term+parseTerm e = do+    sort <- parseSort e+    op <- attr "op" e+    children <- mapM parseTerm (elChildren e)+    case findAttr (unqual "number") e of+        Nothing -> return $ Term sort op children+        Just i -> return $ IterTerm sort op children (read i)++-- <term>+parseSort :: Element -> Parser String+parseSort e = fromMaybeM err $ sort `mplus` synt+  where+    sort = findAttr (unqual "sort") e+    synt = findAttr (unqual "syntactic-sort") e+    err = ParseError e "key 'sort' or 'syntactic-sort' not found"++{- utility functions -}++child :: String -> Element -> Parser Element+child tag e = fromMaybeM err $ findChild (unqual tag) e+  where+    err = ParseError e $ "child not found: <" ++ tag ++ ">"++attr :: String -> Element -> Parser String+attr key e = fromMaybeM err $ findAttr (unqual key) e+  where+    err = ParseError e $ "key not found: " ++ key++readattr :: Read a => String -> Element -> Parser a+readattr key e = do+    s <- attr key e+    case reads s of+        [(a, "")] -> return a+        _ -> ParseError e $ "failed to read value of key: " ++ key++fromMaybeM :: Monad m => m a -> Maybe a -> m a+fromMaybeM err = maybe err return

@@ -0,0 +1,37 @@+{-# LANGUAGE DeriveDataTypeable #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Language.Maude.Syntax+-- Copyright   :  (c) David Lazar, 2012+-- License     :  MIT+--+-- Maintainer  :  lazar6@illinois.edu+-- Stability   :  experimental+-- Portability :  unknown+--+-- Types representing Maude syntax and terms+-----------------------------------------------------------------------------+module Language.Maude.Syntax+    ( Term(..)+    ) where++import Data.Data++-- TODO: handle kinds++data Term+    = Term+        { termSort     :: String+        , termOp       :: String+        , termChildren :: [Term]+        }+    -- ^ Generic representation of terms in Maude+    | IterTerm+        { termSort     :: String+        , termOp       :: String+        , termChildren :: [Term]+        , iterations   :: Integer+        }+    -- ^ Term constructed from an iterated (@iter@) operator,+    -- for example, the @s_@ constructor for Nats+    deriving (Eq, Ord, Show, Data, Typeable)