{- |
Module : ./CMDL/ParseProofScript.hs
Description : parse a heterogeneous proof script
Copyright : (c) Christian Maeder, DFKI GmbH 2009
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
-}
module CMDL.ParseProofScript where
import Interfaces.Command
import CMDL.DataTypes
import CMDL.Commands
import Text.ParserCombinators.Parsec.Pos (initialPos)
import Data.Char
data WhiteWord = WhiteWord
{ leading :: String -- ^ leading white space
, word :: String }
data LitCommand = LitCommand
{ commandWW :: WhiteWord
, argumentWW :: Maybe WhiteWord
, trailing :: String -- ^ trailing white space
, command :: CmdlCmdDescription }
parseLine :: [CmdlCmdDescription] -> FilePath -> Int -> Parser LitCommand
parseLine cl fp i = do
setPosition $ setSourceLine (initialPos fp) i
s1 <- many space
(eof >> return LitCommand
{ commandWW = WhiteWord "" ""
, argumentWW = Nothing
, trailing = s1
, command = cmdlIgnoreFunc "" }) <|> do
(cs, cm) <- choice (map (\ (c, sl) -> do
s <- try $ parseCommand sl
return (s, c)) $ (proveAll, ["prove-all"])
: map (\ c -> (c, words $ cmdNameStr $ cmdDescription c)) cl)
<|> do
h <- char '#'
r <- many anyChar
return (h : r, cmdlIgnoreFunc r)
s2 <- many space
(eof >> return LitCommand
{ commandWW = WhiteWord s1 cs
, argumentWW = Nothing
, trailing = s2
, command = cm }) <|> do
(arg, s3) <- parseArgument
return LitCommand
{ commandWW = WhiteWord s1 cs
, argumentWW = Just $ WhiteWord s2 arg
, trailing = s3
, command = cm
{ cmdDescription = setInputStr arg $ cmdDescription cm } }
parseArgument :: Parser (String, String)
parseArgument = do
arg <- many1 (satisfy $ not . isSpace)
sp <- many space
(eof >> return (arg, sp)) <|> do
(rargs, s) <- parseArgument
return (arg ++ sp ++ rargs, s)
parseCommand :: [String] -> Parser String
parseCommand cmd = case cmd of
[] -> fail ""
[c] -> string c
c : r -> do
string c
s <- many1 space
t <- parseCommand r
return $ c ++ s ++ t
parseSingleLine :: FilePath -> Int -> String -> Either String LitCommand
parseSingleLine fp i str =
case parse (parseLine getCommands fp i) fp str of
Left e -> Left $ show e
Right r -> Right r