{- |
Module      :  ./Maude/Language.hs
Description :  Parsing the Maude Language
Copyright   :  (c) Martin Kuehl, Uni Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  mkhl@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Parsing the Maude language with Haskell and "Parsec".
-}

module Maude.Language (
    -- * Types

    -- ** The Named Spec type
    NamedSpec (..),
    -- ** Parser Result types
    ParseResult,
    RawResult,

    -- * Parsers for Maude

    -- ** The Abstract Parser
    maudeParser,
    -- ** The Raw Parser
    parseFromFile,
    -- ** The Refined Parser
    parse,
) where

import Text.ParserCombinators.Parsec hiding (parseFromFile, parse)
import qualified Text.ParserCombinators.Parsec as Parsec (parseFromFile)

import Maude.Parse

import Common.Parsec ((<:>), (<<), single)

import Data.Set (Set)
import qualified Data.Set as Set

import Data.Char (isSpace)
import Data.List (nub)
import Data.Maybe (fromJust, isNothing)

-- * Types

-- ** The Named Spec type
data NamedSpec = ModName String     -- ^ A Module or Theory
               | ViewName String    -- ^ A View
               deriving (Int -> NamedSpec -> ShowS
[NamedSpec] -> ShowS
NamedSpec -> String
(Int -> NamedSpec -> ShowS)
-> (NamedSpec -> String)
-> ([NamedSpec] -> ShowS)
-> Show NamedSpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NamedSpec] -> ShowS
$cshowList :: [NamedSpec] -> ShowS
show :: NamedSpec -> String
$cshow :: NamedSpec -> String
showsPrec :: Int -> NamedSpec -> ShowS
$cshowsPrec :: Int -> NamedSpec -> ShowS
Show, ReadPrec [NamedSpec]
ReadPrec NamedSpec
Int -> ReadS NamedSpec
ReadS [NamedSpec]
(Int -> ReadS NamedSpec)
-> ReadS [NamedSpec]
-> ReadPrec NamedSpec
-> ReadPrec [NamedSpec]
-> Read NamedSpec
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [NamedSpec]
$creadListPrec :: ReadPrec [NamedSpec]
readPrec :: ReadPrec NamedSpec
$creadPrec :: ReadPrec NamedSpec
readList :: ReadS [NamedSpec]
$creadList :: ReadS [NamedSpec]
readsPrec :: Int -> ReadS NamedSpec
$creadsPrec :: Int -> ReadS NamedSpec
Read, NamedSpec -> NamedSpec -> Bool
(NamedSpec -> NamedSpec -> Bool)
-> (NamedSpec -> NamedSpec -> Bool) -> Eq NamedSpec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NamedSpec -> NamedSpec -> Bool
$c/= :: NamedSpec -> NamedSpec -> Bool
== :: NamedSpec -> NamedSpec -> Bool
$c== :: NamedSpec -> NamedSpec -> Bool
Eq)

-- ** Parser Result types

-- | Parsed Result for a module tree
type ParseResult = [NamedSpec]
-- | Parsed Result for a single declaration
type RawResult = Maybe (Either FilePath NamedSpec)
-- | Intermediate Result during module tree recursion
type RecResult = (Set FilePath, ParseResult)

-- * Generic Parser combinators

-- | Run the argument but return 'Nothing'
ignore :: (Monad m) => m a -> m (Maybe b)
ignore :: m a -> m (Maybe b)
ignore parser :: m a
parser = m a
parser m a -> m (Maybe b) -> m (Maybe b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe b -> m (Maybe b)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe b
forall a. Maybe a
Nothing

-- | Wrap the result of a successful parse
succeed :: (Monad m) => a -> m (Maybe (Either b a))
succeed :: a -> m (Maybe (Either b a))
succeed = Maybe (Either b a) -> m (Maybe (Either b a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Either b a) -> m (Maybe (Either b a)))
-> (a -> Maybe (Either b a)) -> a -> m (Maybe (Either b a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either b a -> Maybe (Either b a)
forall a. a -> Maybe a
Just (Either b a -> Maybe (Either b a))
-> (a -> Either b a) -> a -> Maybe (Either b a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either b a
forall a b. b -> Either a b
Right

-- | A list of characters Maude considers special
specialChars :: String
specialChars :: String
specialChars = "()[]{},"

opLetter :: CharParser () Char
opLetter :: CharParser () Char
opLetter = let
  special :: ParsecT String u Identity Char
special = Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '`' ParsecT String u Identity Char
-> (Char -> ParsecT String u Identity Char)
-> ParsecT String u Identity Char
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Char
 -> ParsecT String u Identity Char
 -> ParsecT String u Identity Char)
-> ParsecT String u Identity Char
-> Char
-> ParsecT String u Identity Char
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char
-> ParsecT String u Identity Char -> ParsecT String u Identity Char
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option (String -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf String
specialChars)
  in CharParser () Char
forall u. ParsecT String u Identity Char
special CharParser () Char -> CharParser () Char -> CharParser () Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Char -> Bool) -> CharParser () Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (\ c :: Char
c -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c String
specialChars)

identifier :: CharParser () String
identifier :: CharParser () String
identifier = CharParser () String -> CharParser () String
forall a. CharParser () a -> CharParser () a
lexeme (CharParser () String -> CharParser () String)
-> CharParser () String -> CharParser () String
forall a b. (a -> b) -> a -> b
$ CharParser () Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar CharParser () Char -> CharParser () String -> CharParser () String
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> CharParser () Char -> CharParser () String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many CharParser () Char
opLetter

reserved :: String -> CharParser () ()
reserved :: String -> CharParser () ()
reserved n :: String
n = CharParser () () -> CharParser () ()
forall a. CharParser () a -> CharParser () a
lexeme (CharParser () () -> CharParser () ())
-> CharParser () () -> CharParser () ()
forall a b. (a -> b) -> a -> b
$ CharParser () () -> CharParser () ()
forall tok st a. GenParser tok st a -> GenParser tok st a
try (String -> CharParser () String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
n CharParser () String -> CharParser () () -> CharParser () ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser () Char -> CharParser () ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy CharParser () Char
opLetter)

lexeme :: CharParser () a -> CharParser () a
lexeme :: CharParser () a -> CharParser () a
lexeme = (CharParser () a -> CharParser () () -> CharParser () a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< CharParser () ()
whiteSpace)

whiteSpace :: CharParser () ()
whiteSpace :: CharParser () ()
whiteSpace = CharParser () String -> CharParser () ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany (CharParser () String -> CharParser () ())
-> CharParser () String -> CharParser () ()
forall a b. (a -> b) -> a -> b
$ CharParser () Char -> CharParser () String
forall (m :: * -> *) a. Monad m => m a -> m [a]
single CharParser () Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space CharParser () String
-> CharParser () String -> CharParser () String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser () String
forall st. CharParser st String
blockComment CharParser () String
-> CharParser () String -> CharParser () String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser () String
forall st. CharParser st String
lineComment

-- * Helper functions for parsing Maude

-- | Match any of the arguments as 'reserved' words
anyReserved :: [String] -> CharParser () ()
anyReserved :: [String] -> CharParser () ()
anyReserved = [CharParser () ()] -> CharParser () ()
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([CharParser () ()] -> CharParser () ())
-> ([String] -> [CharParser () ()]) -> [String] -> CharParser () ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> CharParser () ()) -> [String] -> [CharParser () ()]
forall a b. (a -> b) -> [a] -> [b]
map String -> CharParser () ()
reserved

-- | Match any 'identifier' or 'operator'
something :: CharParser () String
something :: CharParser () String
something = CharParser () String
identifier
-- Identifiers and operators are identical currently.

-- | Match a dot-terminated statement
statement :: CharParser () [String]
statement :: CharParser () [String]
statement = CharParser () [String] -> CharParser () [String]
forall a. CharParser () a -> CharParser () a
lexeme (CharParser () [String] -> CharParser () [String])
-> CharParser () [String] -> CharParser () [String]
forall a b. (a -> b) -> a -> b
$ CharParser () String
-> CharParser () Char -> CharParser () [String]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill CharParser () String
something (CharParser () Char -> CharParser () [String])
-> CharParser () Char -> CharParser () [String]
forall a b. (a -> b) -> a -> b
$ Char -> CharParser () Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.'

-- | Match the rest of a line
line :: CharParser () String
line :: CharParser () String
line = CharParser () String -> CharParser () String
forall a. CharParser () a -> CharParser () a
lexeme (CharParser () String -> CharParser () String)
-> CharParser () String -> CharParser () String
forall a b. (a -> b) -> a -> b
$ CharParser () Char -> CharParser () String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (CharParser () Char -> CharParser () String)
-> CharParser () Char -> CharParser () String
forall a b. (a -> b) -> a -> b
$ String -> CharParser () Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
noneOf "\n"

-- * Parsers for Maude source code and components

-- | Parse Maude source code
toplevel :: CharParser () [RawResult]
toplevel :: CharParser () [RawResult]
toplevel = let
    components :: [CharParser () RawResult]
components = [CharParser () RawResult
systemCmd, CharParser () RawResult
otherCmd, CharParser () RawResult
debuggerCmd, CharParser () RawResult
modul, CharParser () RawResult
theory, CharParser () RawResult
view]
    in CharParser () ()
whiteSpace CharParser () ()
-> CharParser () [RawResult] -> CharParser () [RawResult]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser () RawResult -> CharParser () [RawResult]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ([CharParser () RawResult] -> CharParser () RawResult
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice [CharParser () RawResult]
components)

-- | Parse a system command
systemCmd :: CharParser () RawResult
systemCmd :: CharParser () RawResult
systemCmd = let
    otherSym :: CharParser () ()
otherSym = [String] -> CharParser () ()
anyReserved
               ["quit", "eof", "popd", "pwd", "cd", "push", "ls"]
    other :: ParsecT String () Identity (Maybe b)
other = CharParser () String -> ParsecT String () Identity (Maybe b)
forall (m :: * -> *) a b. Monad m => m a -> m (Maybe b)
ignore (CharParser () String -> ParsecT String () Identity (Maybe b))
-> CharParser () String -> ParsecT String () Identity (Maybe b)
forall a b. (a -> b) -> a -> b
$ CharParser () ()
otherSym CharParser () () -> CharParser () String -> CharParser () String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser () String
line
    loadSym :: CharParser () ()
loadSym = [String] -> CharParser () ()
anyReserved ["in", "load"]
    load :: ParsecT String () Identity (Maybe (Either String b))
load = CharParser () ()
loadSym CharParser () ()
-> ParsecT String () Identity (Maybe (Either String b))
-> ParsecT String () Identity (Maybe (Either String b))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (String -> Maybe (Either String b))
-> CharParser () String
-> ParsecT String () Identity (Maybe (Either String b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Either String b -> Maybe (Either String b)
forall a. a -> Maybe a
Just (Either String b -> Maybe (Either String b))
-> (String -> Either String b) -> String -> Maybe (Either String b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String b
forall a b. a -> Either a b
Left) CharParser () String
line
    in CharParser () RawResult
forall b. ParsecT String () Identity (Maybe (Either String b))
load CharParser () RawResult
-> CharParser () RawResult -> CharParser () RawResult
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser () RawResult
forall b. ParsecT String () Identity (Maybe b)
other

-- | Parse a command
otherCmd :: CharParser () RawResult
otherCmd :: CharParser () RawResult
otherCmd = let
    symbol :: CharParser () ()
symbol = [String] -> CharParser () ()
anyReserved
             ["select", "parse", "debug", "reduce", "rewrite",
              "frewrite", "erewrite", "match", "xmatch", "search",
              "continue", "loop", "trace", "print", "break", "show",
              "do", "set"]
    in CharParser () [String] -> CharParser () RawResult
forall (m :: * -> *) a b. Monad m => m a -> m (Maybe b)
ignore (CharParser () [String] -> CharParser () RawResult)
-> CharParser () [String] -> CharParser () RawResult
forall a b. (a -> b) -> a -> b
$ CharParser () ()
symbol CharParser () ()
-> CharParser () [String] -> CharParser () [String]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser () [String]
statement

-- | Parse a debugger command.
debuggerCmd :: CharParser () RawResult
debuggerCmd :: CharParser () RawResult
debuggerCmd = let symbol :: CharParser () ()
symbol = [String] -> CharParser () ()
anyReserved ["resume", "abort", "step", "where"]
              in CharParser () [String] -> CharParser () RawResult
forall (m :: * -> *) a b. Monad m => m a -> m (Maybe b)
ignore (CharParser () [String] -> CharParser () RawResult)
-> CharParser () [String] -> CharParser () RawResult
forall a b. (a -> b) -> a -> b
$ CharParser () ()
symbol CharParser () ()
-> CharParser () [String] -> CharParser () [String]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser () [String]
statement

-- | Parse a Maude module
modul :: CharParser () RawResult
modul :: CharParser () RawResult
modul = let
    modul' :: String
-> String
-> ParsecT String () Identity (Maybe (Either b NamedSpec))
modul' start :: String
start stop :: String
stop = do
        String -> CharParser () ()
reserved String
start
        String
name <- CharParser () String
identifier
        CharParser () String -> CharParser () () -> CharParser () [String]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill CharParser () String
something (CharParser () () -> CharParser () [String])
-> CharParser () () -> CharParser () [String]
forall a b. (a -> b) -> a -> b
$ String -> CharParser () ()
reserved "is"
        CharParser () [String]
-> CharParser () () -> ParsecT String () Identity [[String]]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill CharParser () [String]
statement (CharParser () () -> ParsecT String () Identity [[String]])
-> CharParser () () -> ParsecT String () Identity [[String]]
forall a b. (a -> b) -> a -> b
$ String -> CharParser () ()
reserved String
stop
        NamedSpec
-> ParsecT String () Identity (Maybe (Either b NamedSpec))
forall (m :: * -> *) a b. Monad m => a -> m (Maybe (Either b a))
succeed (NamedSpec
 -> ParsecT String () Identity (Maybe (Either b NamedSpec)))
-> NamedSpec
-> ParsecT String () Identity (Maybe (Either b NamedSpec))
forall a b. (a -> b) -> a -> b
$ String -> NamedSpec
ModName String
name
    in String -> String -> CharParser () RawResult
forall b.
String
-> String
-> ParsecT String () Identity (Maybe (Either b NamedSpec))
modul' "fmod" "endfm"
    CharParser () RawResult
-> CharParser () RawResult -> CharParser () RawResult
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> String -> CharParser () RawResult
forall b.
String
-> String
-> ParsecT String () Identity (Maybe (Either b NamedSpec))
modul' "mod" "endm"

-- | Parse a Maude theory
theory :: CharParser () RawResult
theory :: CharParser () RawResult
theory = let
    theory' :: String
-> String
-> ParsecT String () Identity (Maybe (Either b NamedSpec))
theory' start :: String
start stop :: String
stop = do
        String -> CharParser () ()
reserved String
start
        String
name <- CharParser () String
identifier
        String -> CharParser () ()
reserved "is"
        CharParser () [String]
-> CharParser () () -> ParsecT String () Identity [[String]]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill CharParser () [String]
statement (CharParser () () -> ParsecT String () Identity [[String]])
-> CharParser () () -> ParsecT String () Identity [[String]]
forall a b. (a -> b) -> a -> b
$ String -> CharParser () ()
reserved String
stop
        NamedSpec
-> ParsecT String () Identity (Maybe (Either b NamedSpec))
forall (m :: * -> *) a b. Monad m => a -> m (Maybe (Either b a))
succeed (NamedSpec
 -> ParsecT String () Identity (Maybe (Either b NamedSpec)))
-> NamedSpec
-> ParsecT String () Identity (Maybe (Either b NamedSpec))
forall a b. (a -> b) -> a -> b
$ String -> NamedSpec
ModName String
name
    in String -> String -> CharParser () RawResult
forall b.
String
-> String
-> ParsecT String () Identity (Maybe (Either b NamedSpec))
theory' "fth" "endfth"
    CharParser () RawResult
-> CharParser () RawResult -> CharParser () RawResult
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> String -> CharParser () RawResult
forall b.
String
-> String
-> ParsecT String () Identity (Maybe (Either b NamedSpec))
theory' "th" "endth"

-- | Parse a Maude view
view :: CharParser () RawResult
view :: CharParser () RawResult
view = do
    String -> CharParser () ()
reserved "view"
    String
name <- CharParser () String
identifier
    CharParser () [String]
-> CharParser () () -> ParsecT String () Identity [[String]]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill CharParser () [String]
statement (CharParser () () -> ParsecT String () Identity [[String]])
-> CharParser () () -> ParsecT String () Identity [[String]]
forall a b. (a -> b) -> a -> b
$ String -> CharParser () ()
reserved "endv"
    NamedSpec -> CharParser () RawResult
forall (m :: * -> *) a b. Monad m => a -> m (Maybe (Either b a))
succeed (NamedSpec -> CharParser () RawResult)
-> NamedSpec -> CharParser () RawResult
forall a b. (a -> b) -> a -> b
$ String -> NamedSpec
ViewName String
name

-- * Parsers for Maude source files

-- | Parse Maude source code
maudeParser :: CharParser () [RawResult]
maudeParser :: CharParser () [RawResult]
maudeParser = CharParser () [RawResult]
toplevel

-- | Parse a single Maude source file
parseFromFile :: FilePath ->
                 IO (Either ParseError [RawResult])
parseFromFile :: String -> IO (Either ParseError [RawResult])
parseFromFile = CharParser () [RawResult]
-> String -> IO (Either ParseError [RawResult])
forall a. Parser a -> String -> IO (Either ParseError a)
Parsec.parseFromFile CharParser () [RawResult]
maudeParser

-- | Parse a Maude source file and the collect the results
parseFileAndCollect :: FilePath -> RecResult ->
                       IO (Either ParseError RecResult)
parseFileAndCollect :: String -> RecResult -> IO (Either ParseError RecResult)
parseFileAndCollect path :: String
path results :: RecResult
results@(done :: Set String
done, syms :: [NamedSpec]
syms)
    | String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
path Set String
done = Either ParseError RecResult -> IO (Either ParseError RecResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ParseError RecResult -> IO (Either ParseError RecResult))
-> Either ParseError RecResult -> IO (Either ParseError RecResult)
forall a b. (a -> b) -> a -> b
$ RecResult -> Either ParseError RecResult
forall a b. b -> Either a b
Right RecResult
results
    | Bool
otherwise = do
        Either ParseError [RawResult]
parsed <- String -> IO (Either ParseError [RawResult])
parseFromFile String
path
        case Either ParseError [RawResult]
parsed of
            Left err :: ParseError
err -> Either ParseError RecResult -> IO (Either ParseError RecResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ParseError RecResult -> IO (Either ParseError RecResult))
-> Either ParseError RecResult -> IO (Either ParseError RecResult)
forall a b. (a -> b) -> a -> b
$ ParseError -> Either ParseError RecResult
forall a b. a -> Either a b
Left ParseError
err
            Right res :: [RawResult]
res -> [RawResult] -> RecResult -> IO (Either ParseError RecResult)
collectParseResults [RawResult]
res (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
path Set String
done, [NamedSpec]
syms)

-- | Collect the results from parsing a Maude source file
collectParseResults :: [RawResult] -> RecResult ->
                       IO (Either ParseError RecResult)
collectParseResults :: [RawResult] -> RecResult -> IO (Either ParseError RecResult)
collectParseResults list :: [RawResult]
list results :: RecResult
results@(done :: Set String
done, syms :: [NamedSpec]
syms)
    | [RawResult] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RawResult]
list = Either ParseError RecResult -> IO (Either ParseError RecResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ParseError RecResult -> IO (Either ParseError RecResult))
-> Either ParseError RecResult -> IO (Either ParseError RecResult)
forall a b. (a -> b) -> a -> b
$ RecResult -> Either ParseError RecResult
forall a b. b -> Either a b
Right RecResult
results
    | RawResult -> Bool
forall a. Maybe a -> Bool
isNothing (RawResult -> Bool) -> RawResult -> Bool
forall a b. (a -> b) -> a -> b
$ [RawResult] -> RawResult
forall a. [a] -> a
head [RawResult]
list = [RawResult] -> RecResult -> IO (Either ParseError RecResult)
collectParseResults ([RawResult] -> [RawResult]
forall a. [a] -> [a]
tail [RawResult]
list) RecResult
results
    | Bool
otherwise = case RawResult -> Either String NamedSpec
forall a. HasCallStack => Maybe a -> a
fromJust (RawResult -> Either String NamedSpec)
-> RawResult -> Either String NamedSpec
forall a b. (a -> b) -> a -> b
$ [RawResult] -> RawResult
forall a. [a] -> a
head [RawResult]
list of
        Right symb :: NamedSpec
symb -> [RawResult] -> RecResult -> IO (Either ParseError RecResult)
collectParseResults ([RawResult] -> [RawResult]
forall a. [a] -> [a]
tail [RawResult]
list) (Set String
done, NamedSpec
symb NamedSpec -> [NamedSpec] -> [NamedSpec]
forall a. a -> [a] -> [a]
: [NamedSpec]
syms)
        Left path :: String
path -> do
            Either ParseError RecResult
parsed <- String -> RecResult -> IO (Either ParseError RecResult)
parseFileAndCollect String
path RecResult
results
            case Either ParseError RecResult
parsed of
                Right res :: RecResult
res -> [RawResult] -> RecResult -> IO (Either ParseError RecResult)
collectParseResults ([RawResult] -> [RawResult]
forall a. [a] -> [a]
tail [RawResult]
list) RecResult
res
                Left err :: ParseError
err -> Either ParseError RecResult -> IO (Either ParseError RecResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ParseError RecResult -> IO (Either ParseError RecResult))
-> Either ParseError RecResult -> IO (Either ParseError RecResult)
forall a b. (a -> b) -> a -> b
$ ParseError -> Either ParseError RecResult
forall a b. a -> Either a b
Left ParseError
err

-- | Parse a Maude source tree
parse :: FilePath ->
         IO (Either ParseError ParseResult)
parse :: String -> IO (Either ParseError [NamedSpec])
parse path :: String
path = do
    Either ParseError RecResult
parsed <- String -> RecResult -> IO (Either ParseError RecResult)
parseFileAndCollect String
path (Set String
forall a. Set a
Set.empty, [])
    case Either ParseError RecResult
parsed of
        Left err :: ParseError
err -> Either ParseError [NamedSpec] -> IO (Either ParseError [NamedSpec])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ParseError [NamedSpec]
 -> IO (Either ParseError [NamedSpec]))
-> Either ParseError [NamedSpec]
-> IO (Either ParseError [NamedSpec])
forall a b. (a -> b) -> a -> b
$ ParseError -> Either ParseError [NamedSpec]
forall a b. a -> Either a b
Left ParseError
err
        Right res :: RecResult
res -> Either ParseError [NamedSpec] -> IO (Either ParseError [NamedSpec])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ParseError [NamedSpec]
 -> IO (Either ParseError [NamedSpec]))
-> Either ParseError [NamedSpec]
-> IO (Either ParseError [NamedSpec])
forall a b. (a -> b) -> a -> b
$ [NamedSpec] -> Either ParseError [NamedSpec]
forall a b. b -> Either a b
Right ([NamedSpec] -> Either ParseError [NamedSpec])
-> [NamedSpec] -> Either ParseError [NamedSpec]
forall a b. (a -> b) -> a -> b
$ [NamedSpec] -> [NamedSpec]
forall a. Eq a => [a] -> [a]
nub ([NamedSpec] -> [NamedSpec]) -> [NamedSpec] -> [NamedSpec]
forall a b. (a -> b) -> a -> b
$ [NamedSpec] -> [NamedSpec]
forall a. [a] -> [a]
reverse ([NamedSpec] -> [NamedSpec]) -> [NamedSpec] -> [NamedSpec]
forall a b. (a -> b) -> a -> b
$ RecResult -> [NamedSpec]
forall a b. (a, b) -> b
snd RecResult
res