Commits

David Lazar  committed 072bcb8

Major rewrite:

* Foreign.Maude is now Language.Maude.Exec.

* This package now reads results from Maude's XML log, which is far less
error-prone than parsing Maude's standard output.

* The 'Term' type provides a representation of Maude terms in Haskell.

* Improve error reporting.

* Add support for the 'erewrite' command.

* Bump to version 0.6.0 to indicate major change.

  • Participants
  • Parent commits 235830c
  • Tags v0.6.0

Comments (0)

Files changed (6)

 Name:               maude
-Version:            0.3.0
+Version:            0.6.0
 Synopsis:           An interface to the Maude rewriting system.
 Description:        This package provides a simple interface for doing Maude
                     rewrites from within Haskell.
 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:
   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
+
+  Build-depends:
+    base >= 4 && < 5,
+    process,
+    process-extras,
+    filepath,
+    directory,
+    temporary,
+    text,
+    xml

File src/Foreign/Maude.hs

-{-# 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.
--}

File src/Language/Maude/Exec.hs

+{-# 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]

File src/Language/Maude/Exec/Types.hs

+{-# 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)

File src/Language/Maude/Exec/XML.hs

+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

File src/Language/Maude/Syntax.hs

+{-# 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)