Language.hs revision d8a1a2163331f183fa32476c797a56c55506e6bd
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher parseFromFile,
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport Text.ParserCombinators.Parsec (ParseError, CharParser)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport Text.ParserCombinators.Parsec.Prim ((<|>))
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport Text.ParserCombinators.Parsec.Combinator
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport qualified Text.ParserCombinators.Parsec.Token as Token
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport qualified Text.ParserCombinators.Parsec.Language as Language
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport qualified Text.ParserCombinators.Parsec as Parsec (parseFromFile)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport qualified Data.Set as Set
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport Data.Maybe (fromJust, isNothing)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher--- The types we use for our parsers
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherdata NamedSpec = Module String
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce | Theory String
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce | View String
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce deriving (Eq)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghertype Parsed = Either ParseError
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- Result of a single component
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghertype TempResult = Maybe (Either FilePath NamedSpec)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghertype TempParser = CharParser () TempResult
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghertype TempListResult = [TempResult]
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghertype TempListParser = CharParser () TempListResult
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- Result during module tree recursion
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghertype RecResult = (Set FilePath, MaudeResult)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- Result for a module tree
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghertype MaudeResult = [NamedSpec]
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher--- Generic parser combinators
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Run the given |parser| but return unit
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghervoid :: (Monad m) => m a -> m ()
e2ac9be4f293b96f3c8992f1171e44bc1da5cfcaMichal Zidekvoid parser = parser >> return ()
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Run the given |parser| but return Nothing
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherignore :: (Monad m) => m a -> m (Maybe b)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherignore parser = parser >> return Nothing
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce-- | Wrap the result of a successful parse
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghersucceed :: (Monad m) => a -> m (Maybe (Either b a))
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashovsucceed = return . Just . Right
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher--- A few helpers we need for Parsec.Language
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Run the given |parser| after ensuring we aren't looking at whitespace
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghernonSpace :: CharParser () a -> CharParser () a
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghernonSpace parser = notFollowedBy space >> parser
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov-- | Match a literal backquote character
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherbackquote :: CharParser () Char
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherbackquote = char '`'
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov-- | A list of characters Maude considers "special"
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherspecialChars :: String
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherspecialChars = "()[]{},"
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher--- The Parsec.Language definition of Maude
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai KondrashovmaudeLanguageDef :: Language.LanguageDef ()
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghermaudeLanguageDef = Language.emptyDef {
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher -- TODO: Get comments right.
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Language.commentLine = "---", -- also: "***"
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov Language.identStart = Token.opStart maudeLanguageDef,
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Language.identLetter = Token.opLetter maudeLanguageDef,
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher special = backquote >>= flip option (oneOf specialChars)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher other = noneOf specialChars
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher in nonSpace $ special <|> other
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghermaudeTokenParser :: Token.TokenParser ()
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghermaudeTokenParser = Token.makeTokenParser maudeLanguageDef
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- Yes, this is how Parsec.Language is _supposed_ to be used...
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagheridentifier :: CharParser () String
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagheridentifier = Token.identifier maudeTokenParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherreserved :: String -> CharParser () ()
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherreserved = Token.reserved maudeTokenParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherlexeme :: CharParser () a -> CharParser () a
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherlexeme = Token.lexeme maudeTokenParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherwhiteSpace :: CharParser () ()
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherwhiteSpace = Token.whiteSpace maudeTokenParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherdot :: CharParser () String
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherdot = Token.dot maudeTokenParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher--- A few more helpers for parsing Maude
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Match any of the given strings as a |reserved| word
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagheranyReserved :: [String] -> CharParser () ()
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagheranyReserved = choice . map reserved
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek-- | Match any identifier or operator
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov-- Identifiers and operators are identical currently.
21d485184df986e1a123f70c689517386e51a5ceMichal Zideksomething :: CharParser () String
21d485184df986e1a123f70c689517386e51a5ceMichal Zideksomething = identifier
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Match a |dot|-terminated statement
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherstatement :: CharParser () [String]
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorcestatement = manyTill something dot
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Match the rest of a line
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov-- TODO: Figure out how the characters are interpreted by Maude.
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashovline :: CharParser () String
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherline = manyTill anyChar $ eof <|> void (lexeme newline)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher--- Parsers for Maude source code and components
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce-- | Parse Maude source code
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorcetoplevel :: TempListParser
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov components = [systemCmd, otherCmd, debuggerCmd, modul, theory, view]
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov in whiteSpace >> many1 (choice components)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Parse a system command
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghersystemCmd :: TempParser
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo SorcesystemCmd = let
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek otherSym = anyReserved
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ["quit", "eof", "popd", "pwd", "cd", "push", "ls"]
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek other = ignore $ otherSym >> line
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek loadSym = anyReserved ["in", "load"]
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher load = do loadSym; name <- line; return $ Just $ Left name
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher in load <|> other
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Parse a command
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo SorceotherCmd :: TempParser
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov symbol = anyReserved
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher ["select", "parse", "debug", "reduce", "rewrite",
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher "frewrite", "erewrite", "match", "xmatch", "search",
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher "continue", "loop", "trace", "print", "break", "show",
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov in ignore $ symbol >> statement
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Parse a debugger command.
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherdebuggerCmd :: TempParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherdebuggerCmd = let symbol = anyReserved ["resume", "abort", "step", "where"]
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher in ignore $ symbol >> statement
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Parse a Maude module
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghermodul :: TempParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher modul' start stop = do
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher reserved start
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher name <- identifier
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher manyTill something $ reserved "is"
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher manyTill statement $ reserved stop
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov succeed $ Module name
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher in modul' "fmod" "endfm"
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher <|> modul' "mod" "endm"
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Parse a Maude theory
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallaghertheory :: TempParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher theory' start stop = do
3d8a87081a6cd197acbd355b5a39111669ec2aa6Jakub Hrozek reserved start
3d8a87081a6cd197acbd355b5a39111669ec2aa6Jakub Hrozek name <- identifier
3d8a87081a6cd197acbd355b5a39111669ec2aa6Jakub Hrozek reserved "is"
3d8a87081a6cd197acbd355b5a39111669ec2aa6Jakub Hrozek manyTill statement $ reserved stop
3d8a87081a6cd197acbd355b5a39111669ec2aa6Jakub Hrozek succeed $ Theory name
3d8a87081a6cd197acbd355b5a39111669ec2aa6Jakub Hrozek in theory' "fth" "endfth"
3d8a87081a6cd197acbd355b5a39111669ec2aa6Jakub Hrozek <|> theory' "th" "endth"
3d8a87081a6cd197acbd355b5a39111669ec2aa6Jakub Hrozek-- | Parse a Maude view
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherview :: TempParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher reserved "view"
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher name <- identifier
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher manyTill statement $ reserved "endv"
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher succeed $ View name
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher--- Parsers for Maude source files
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Parse Maude source code and clean up the results
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghermaudeParser :: TempListParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghermaudeParser = toplevel
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Parse a single Maude source file
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherparseFromFile :: FilePath -> IO (Parsed TempListResult)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherparseFromFile = Parsec.parseFromFile maudeParser
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Parse a Maude source file and the collect the results
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherparseFileAndCollect :: FilePath -> RecResult -> IO (Parsed RecResult)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherparseFileAndCollect path results@(done, syms)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher | Set.member path done = return $ Right results
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher | otherwise = do
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher parsed <- parseFromFile path
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher case parsed of
9f37bb2012faa136ef7c1f9fe93689ce2be85637Ondrej Kos Left err -> return $ Left err
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Right res -> collectParseResults res ((Set.insert path done), syms)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Collect the results from parsing a Maude source file
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghercollectParseResults :: TempListResult -> RecResult -> IO (Parsed RecResult)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghercollectParseResults todo results@(done, syms)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher | null todo = return $ Right results
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher | isNothing $ head todo = collectParseResults (tail todo) results
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher | otherwise = case fromJust $ head todo of
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Right symb -> collectParseResults (tail todo) (done, (symb:syms))
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Left path -> do
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher parsed <- parseFileAndCollect path results
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher case parsed of
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Right res -> collectParseResults (tail todo) res
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Left err -> return $ Left err
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Parse a Maude source tree
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherparse :: FilePath -> IO (Parsed MaudeResult)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherparse path = do
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher parsed <- parseFileAndCollect path (Set.empty, [])
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher case parsed of
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Left err -> return $ Left err
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Right res -> return $ Right $ nub $ reverse $ snd res